Surface type-system soundness: type-check = expr bodies + cycle guard + Lean cardinality preservation

[chessai]

Discovers and fixes two soundness holes in the surface type checker (theseus-check), with reproducing tests, and adds the corresponding Lean type-soundness property. Grounded in the Pi (James–Sabry, Information Effects, POPL'12) and Theseus (RC'14) type theory: a well-typed iso f : A <-> B must denote a bijection, which requires |A| = |B| and that the body's synthesized type equals the declared boundary.

Bug 1 — = expr iso bodies were never type-checked

The Typing stage (T0102) only walked clause patterns. A combinator/composition body (= f ; g, = iter T h, = p, = ~q) was never checked — neither internally nor against the declared signature — so check accepted, silently:

iso f : Bit <-> Bit = swap2          -- body is Bit*Bit<->Bit*Bit  (|.| = 4 != 2)
iso f : Bit <-> Bit = notb ; swap2   -- ill-typed composition (out(notb) != in(swap2))
iso f : Bit <-> Bit = iter Bit notb  -- non-numeral counter (T0601 existed but was never surfaced)

The declared signature — used for value marshaling and as the iso's type for downstream composition — was thus unchecked, so eval/compile could crash or produce out-of-domain values.

Fix: after the clause checks, elaborate each = expr body and require type_of(body) == (lower(lhs), lower(rhs)); an internally ill-typed body or a signature mismatch is T0102, and the combinator diagnostics (T06xx) the elaborator already localizes are now surfaced. Reuses the core type_of so id / iter / fold rules are handled once, authoritatively.

This immediately caught a real latent bug in the checker's own prelude test: tofMid = asc ; (toffoli * idb) ; ~asc was asserted clean but is ill-typed — asc yields a 2-bit group while toffoli needs 3 (cardinality 8 vs 16). Replaced with a well-typed tofUse = toffoli ; toffoli that still exercises prelude toffoli in an = expr body.

Bug 2 — ill-founded = expr recursion crashed the checker

A reversible iso may only recurse through a structural combinator (iter/fold); naming itself in an = expr body — directly (iso f = f) or mutually (f = g ; g = f) — is ill-founded. Elaboration recursed with no guard and stack-overflowed / SIGABRTed. Harmless before (check never elaborated = expr bodies) but reachable now, and a latent crash for any direct elaborate caller.

Fix: thread a visiting stack of iso names through elaboration; re-entering one is reported as T0102 instead of looping.

Lean — cardinality preservation (theseus-proofs)

Adds the Pi/Theseus structural type-soundness fact to Reversibility.lean:

• card_preserved : (i : Iso a b) -> Fintype.card (denoteTy a) = Fintype.card (denoteTy b) — every combinator relates equinumerous types (a corollary of denote_bijective via Fintype.card_congr).
• card_unit/card_bit/card_prod/card_sum — denoteTy realizes the type-level semiring on cardinalities.
• no_iso_of_card_ne — the sharp contrapositive: there is no iso between types of different cardinality. This is precisely the obligation the checker fix enforces on = expr bodies; accepting f : Bit <-> Bit = swap2 would assert an iso this theorem proves cannot exist.

lake build green; AxiomGuard clean (propext / Classical.choice / Quot.sound only).

Tests / verification

• 6 reproducing cases in typing.rs (cardinality mismatch, ill-typed composition, surfaced T0601, valid bodies stay clean, self-recursion, mutual recursion).
• nix flake check green (fmt + clippy --all-targets --deny warnings + nextest); conformance green.

Not fixed (reported for a later, careful pass)

The clause path (Typing + Coverage + Linearity) looks sound — each side is partitioned, forcing a bijection and hence |A| = |B|. Not exhaustively audited: linearity.rs (var drop/duplication) and a cosmetic is_un_type laxness in typing.rs (not exploitable — Names gates it).