formalization(tc): verify WHNF, inference, DefEq, and the recursive method knot

[johnchandlerburnham]

Summary

This PR substantially expands the formal verification of the production Ix.Tc kernel. It completes the K1 WHNF layer and the K2 inference/
definitional-equality layer, then assembles all six recursive methods into a single fixed-universe closure theorem.

The principal result is RecursiveMethodClosureContext.closedAt, which combines:

• the four WHNF contracts from K1ClosureContext.closedAt; and
• the infer and isDefEq contracts from InferDefEqClosureContext.closedAt.

This proves every finite methodsN approximation selected by the production recursive runner satisfies the six-method Methods.WFAt
contract. The proof is non-circular: each unfolded method-table layer may assume correctness only of the strictly smaller predecessor table.

The formalization remains over Ix.Tc. Transporting these results to the Rust kernel through Aeneas, or directly to the Aiur IxVM
implementation, remains later work.

WHNF verification

The K1 portion verifies the structural, no-delta, full-WHNF, and trusted-delta reducer layers, including:

• single- and multi-argument beta reduction;
• dependent substitution and application-spine rebuilding;
• iota reduction, constructor selection, and rule instantiation;
• projection success, failure, and application cases;
• structure eta classification and rebuilding;
• Nat, symbolic Nat-offset, string, native, decidable, and BitVec reductions;
• quotient reduction;
• lazy ingress and callback error preservation;
• cache hit, miss, insertion, and stable-cache behavior;
• cycle detection, stuck results, and delta unfolding; and
• the four public WHNF method-table fields.

The WHNF proof is organized by semantic responsibility under directories such as Beta/, Iota/, Structural/, NoDelta/, Driver/,
Delta/, Projection/, StructEta/, and Runtime/.

Inference verification

The K2 inference layer provides an exhaustive proof of the production uncached dispatcher and its public cache shell. It covers:

• sorts, bound variables, free variables, and constants;
• applications and function-domain checking;
• lambdas, forall expressions, and let declarations;
• Nat and string literals;
• projection classification, constructor telescopes, parameter instantiation, and field-type synthesis;
• binder opening and closing;
• scoped local-context restoration on both success and error;
• substitution and cheap beta reduction;
• trusted constant-type and finite-support provenance; and
• inference cache hits, misses, writes, and inferOnly behavior.

Successful inference returns a supported kernel expression whose translation is a valid Theory type for the translated source. Partial errors
preserve the checker invariant.

Definitional-equality verification

The K2 DefEq layer follows the production reducer in its exact phase order and verifies:

• direct and equivalence-root cache lookup;
• cache partitioning and failure-cache provenance;
• structural quick equality and congruence;
• same-head application-spine and universe comparison;
• proof irrelevance and proposition classification;
• Bool, Nat, symbolic Nat-offset, string, unit-like, and projection reductions;
• eta expansion and structure eta;
• core and no-delta normalization passes;
• one-sided and two-sided delta unfolding;
• definition ranking and equal-rank dispatch;
• projection-directed lazy-delta reduction;
• stopped-continuation and final-WHNF fallback; and
• the guarded public isDefEq cache shell.

A successful isDefEq result is connected to VEnv.IsDefEqU for the translated operands.

Cache and context-key soundness

The PR adds a joint K1/K2 cache model for WHNF, inference, DefEq, and proposition-classifier entries.

Notable changes include:

• operational proofs for the production WHNF, inference, and DefEq key computations;
• suffix-context representation at the exact requested local-binding radius;
• finite, run-scoped context-digest models;
• explicit semantic transport contracts for all four cache families;
• context- and radius-aware DefEq equivalence keys; and
• separate tracking of an expression’s intrinsic radius and the shared comparison radius.

The Lean and Rust equivalence managers now retain both radii in EqKey. Root-cache reuse is accepted only when the representatives
reconstruct the requested comparison scope.

The distinction between expression-address collision freedom and collision freedom of the composite context digest is documented in docs/tc- context-digest-collision-boundary.md.

Recursive closure

The final assembly adds:

• Methods.WhnfLayerWFAt for the four K1 fields;
• Methods.InferDefEqLayerWFAt for the two K2 fields;
• Methods.ClosedAt.of_parts for their exact composition;
• InferDefEqClosureContext.closedAt;
• RecursiveMethodClosureContext.closedAt;
• correctness of every finite methodsN approximation; and
• TcM.runRec_wfAt for transporting a reader-level proof to the concrete finite method table selected by the production state.

No field assumes the correctness of the method-table layer it is currently proving.

Production hardening surfaced by the proof

The proof effort also produced several aligned Lean/Rust kernel changes:

• DefEq and inference reducers are decomposed into named semantic stages, making their production ordering explicit.
• Binder-local contexts are restored on both successful and failing inference/DefEq paths.
• abstractFVars no longer takes the no-free-variable fast path when loose bound variables still require shifting.
• DefEq union-find entries are isolated by context digest, requested radius, and intrinsic expression radius.
• Regression tests cover radius isolation, binder-error cleanup, and loose-bound-variable abstraction.
• Nat fixtures and production WHNF tests are expanded across successful, absent, stuck, and partial-error executions.

Explicit remaining boundaries

This PR closes the fixed-universe K1/K2 recursive core under explicitly named semantic resources. It does not yet claim the final end-to-end
checker theorem.

The remaining boundaries are intentionally visible:

• TcM.whnf.wf, TcM.infer.wf, TcM.isDefEq.wf, and TcM.checkConst.wf remain the four separately audited public statement-frontier roots.
• The compact tryNatOffsetStuck stage remains an explicit OptionalReduction.WFAt premise until its callbacks and intern operations are
  instantiated from finite run-scoped contracts.
• Composite context-digest collision freedom and the corresponding declarative suffix transports remain explicit assumptions. Expression-
  address collision freedom alone is not sufficient.
• Trusted constant, primitive, callback, projection, and finite-run-support facts remain named resource fields rather than hidden axioms.
• Existing upstream Lean4Lean typing and projection debt remains enumerated in the trust manifest.
• The TcM.WF results establish invariant preservation and semantic correctness of successful results; they do not assert that every checker
  invocation succeeds.
• Rust/Aeneas and Aiur transport are outside this PR.

Verification

• lake build IxTcVerify
• lake build Ix.Tc.Verify.Audit.Completed Ix.Tc.Verify.Audit.Statements
• perl .github/scripts/check_tc_verify_sorries.pl
• lake lint -- --wfail -v

The completed trust manifest currently enumerates 1,510 theorem roots. The four public statement-frontier roots are audited separately, and
legacy whole-environment and broad delta-authority dependencies are forbidden from the completed closure surface.

The branch is two commits ahead of main and is published as jcb/formalization.