Model the type system in Lean, and check the solver's subtyping and bound merge against it

[dpmills]

The ground subtype relation and the solver's bound merge exist only operationally — constrain_go and CompactType::merge implement them without ever writing them down — so their properties (is subtyping transitive? is the merge associative? does the checker decide the relation?) have been readings of code, not statements. This PR adds formal/, a Lean 4 model that states both declaratively over the index coordinate the stack below establishes, proves the metatheory sorry-free, and pins the model to the implementation with a differential oracle per operation. The headline theorem for subtyping is transitivity with no fragment restriction and no environment side conditions: earlier editions of this model (developed on the retired name-coordinate stack, #79) proved it only for a canonical-spelling fragment under six identity-acting rename environments, and the σ-gap they reconciled never forms here — the measured sense in which the coordinate below is the right design. For the merge it is associativity with no side condition, and uniqueness: the merge is the only way the induced order admits of combining two bounds.

Each oracle earned its keep before landing. The subtype oracle's first sweep caught a real capture in the solver's Fun/Fun opening, fixed below in the telescope PR with the mechanism it repairs. The merge oracle's first sweep caught the model intersecting away refinements a hole should have passed through, fixed here.

The model

Ty/Pred mirror the ground fragment of Type, with Pred.piBound mirroring Name::PiBound and refined carrying a refinement set (grammar and adjudications). Sub is one constructor per constrain_go arm; deliberate departures (no trivial-equality short-circuit, no partition-collapse arm, no binder-correspondence edge) are each recorded as tracked decisions in CclFormal/Sub.lean. Proved: Sub.refl under the uniquely-keyed Ty.WF (naming a builder invariant the Rust leaves implicit), checker soundness/completeness giving decidability (Equiv.lean), sub_trans for well-formed types (Transitivity.lean), refinement-order unobservability, and the M2 safety battery — progress, preservation, refinement soundness (Safety.lean).

The merge algebra

Merge.lean mirrors compact.rs's bound-merging: CTy for the ground fragment of CompactType, merge for the polar CompactType::merge/CompactFun::merge, and eqv for CompactType's own PartialEq, so every theorem is quotient-compatible by construction. Proved: eqv is an equivalence, merge is commutative, idempotent under the input-bound invariant wf, a congruence, and associative unconditionally at both polarities — the kinds join in the flat semilattice unknown < {data, compute} < conflict (joinKind) and the domains are combined by polarity alone, so no fold step reads a value a later step can change. The fold is therefore invariant under permutation and duplication of the bound list, and merge pol is the least upper bound of the order it induces (le) and the only one up to eqv (join_unique), with the empty position as the least element.

Associativity was a non-theorem when this model first stated it, and the counterexample was real: the solver selected a function slot's domain combination from a kind that was not settled, so bound arrival order decided accept-vs-reject and one association accepted a collection whose domain was the meet of two others'. The PR below defers that choice to the resolved kind at coalesce, which is what removes the side condition here.

The differential oracles

lake build produces the oracle binary; each case is one JSONL line tagged by "op", and tests/differential_oracle.rs generates cases with the seeded generator it shares with the type-merge fuzz (tests/type_gen/mod.rs), computes the solver's answer, and diffs. The harness is an integration test rather than a #[cfg(test)] module in the library: it is a test, and the only solver internal it cannot otherwise reach is CompactType::merge, which the test-helpers feature opens for it.

• "sub": seeded ground pairs, each closed into the ground fragment (close_all — every arrow's own-binder references as indices), diffed against subCheck. 150k pairs across five seeds, zero mismatches, roughly one pair in twelve index-bearing.
• "merge": bound lists folded through CompactType::merge exactly as compact_go folds a variable's bounds, every step diffed against merge up to eqv. Each step's left operand is the previous step's result, so the conflicted and multi-alternative states only merging produces are operands too; operands sometimes carry a kind variable, the only route to KindMerge::Unknown. Clean at 40k steps.

CoErr has no emptyProduct: the empty product is IncompatibleBounds on both sides, since bounds with no common shape is what that error already says.

Both skip loudly when the oracle binary is absent, so machines without a Lean toolchain stay green, and ./ci.sh oracle builds the model and runs them where lake exists — without that gate nothing notices the model drifting from the solver, in either direction. CAMBRA_DIFF_SEED/CAMBRA_DIFF_N/CAMBRA_DIFF_DUMP control runs.

Reading order

formal/design.md (the plan, adjudications, and findings — every claim in it is true of the code beneath this PR), then Ty.lean → Sub.lean → Decide.lean/Equiv.lean → Transitivity.lean, with Term.lean/Safety.lean and Merge.lean as independent limbs. In Merge.lean, read the refinement-slot laws and joinKind before the merge theorems that use them; the order and uniqueness section is last and depends only on the semilattice laws. The model's development history, including the name-coordinate editions this replaces, is on closed #79.