formalization: totalize Ix.Tc and extend soundness proofs through WHNF K1h

[johnchandlerburnham]

Summary

This PR establishes the formal-verification foundation for the reference Lean Ix.Tc kernel against Lean4Lean.Theory, totalizes the production checker call graph, and advances the WHNF proof through K1h.

The proof strategy is deliberately staged: prove properties over Ix.Tc first, then transport them to the Rust kernel with Aeneas or prove them directly for Aiur IxVM in later work.

What changed

Non-circular trust model

• Separates the immutable declaration catalog from the trusted Theory world.
• Distinguishes raw/pending declarations from successfully promoted trusted declarations.
• Requires successful checking—not the precondition—to provide declaration well-formedness.
• Adds explicit self-lookup and untrusted-cache barriers.
• Introduces an ambient-inductive oracle with exact translation, lookup, environment-extension, and recursor-rule obligations.
• Provides an inhabited Nat fixture containing both a valid promoted declaration and an independently loaded, ill-typed pending declaration.

Execution, support, and caches

• Defines constructive finite support for interning, lifting, substitution, universe instantiation, and related walkers.
• Indexes execution certificates by the actual computation and initial checker state.
• Proves the required intern-table and checker-state frame properties.
• Gives all 18 semantic KEnv cache fields explicit provenance and validity contracts.
• Proves cache validity is preserved across trusted-world extension.
• Makes checkConst errors transactional for subject-sensitive caches while preserving previous warm entries and newly cached block errors.

K0 totalization

• Replaces the recursive checker knot with the total six-field methodsOut/methodsN approximation.
• Preserves separate full/stuck WHNF and full/cheap structural-WHNF policies across recursive back-edges.
• Removes production partial def, while, and repeat sites from the TcM.checkConst kernel graph.
• Adds explicit structural measures or checked bounds for formerly unbounded loops.
• Adds exact equations and exhaustion regressions for the new totalization seams.

Malformed inputs that could previously diverge now terminate with the documented exhaustion result, generally .maxRecDepth.

WHNF verification through K1h

• Defines Theory-level WhnfMeaning, fixed-world WhnfStateInv, and the conditional Methods.WF interface.
• Connects cache keys to executed, context-reconciled WhnfContextKeys.Matches witnesses.
• Keeps the five WHNF cache policies semantically distinct.
• Proves production structural steps for beta, legacy/fvar zeta, projection, and iota.
• Adds execution-indexed WhnfCoreTrace, WhnfNoDeltaTrace, and WhnfFullTrace certificates over the real bounded loops.
• Proves exact hit, miss, transient, stuck-successor, and native-no-insert equations.
• Requires universal CacheProvenance before every semantic insertion.
• Proves cold-to-warm behavior for structural, no-delta, cheap, and full-WHNF caches.
• Demonstrates that a cold public whnf call consumes exactly one fuel unit, while the resulting warm hit preserves the complete state.

Auditable trust boundary

• CI now builds IxTcVerify.
• The local sorry frontier is fixed at the four intended headline statement skeletons.
• The completed manifest checks exact transitive axioms and direct upstream sorryAx origins for 518 theorem roots.
• Four statement-frontier roots are audited separately.
• Consumer fixtures are mechanically forbidden from depending on the legacy whole-environment translation path.

Claim boundary

This PR does not claim complete Ix.Tc, Rust, or Aiur soundness.

K1 remains in progress. The next step is conditional RecM.WF closure for the public no-delta/full-WHNF drivers, including trace construction and explicit error/exhaustion outcomes. K2 must then close the tied methodsN table with Infer/DefEq and prove general suffix-context transport.

The remaining upstream Lean4Lean proof debt and all conditional oracle boundaries are listed explicitly in the trust manifests.

No Rust-kernel or Aiur IxVM implementation is claimed verified by this PR; those require later refinement chains from the completed Ix.Tc theorem.

Validation

• lake build IxTcVerify
• Exact four-theorem sorry-frontier check
• 518-root completed trust audit
• 4-root statement-frontier audit
• nix flake check
• Rust clippy and nextest checks
• Lean Ix and IxTests derivations

All checks pass on top of current main.