Formalize singleton and mutual inductive generation

[johnchandlerburnham]

Summary

This PR advances dev through the completed L4L-08C milestone. It formalizes the supported inductive pipeline end to end: retaining the ordinary producer/checker execution, proving the corresponding Theory generation and environment transactions well formed, comparing generated metadata with Lean’s kernel output, and replaying it into aligned Verify environments.

Highlights

• Retains exact normalization, family/constructor validation, elimination-mode, and K-target execution traces from AddInductive.

• Proves level subsumption/equivalence and constructor validity, including dependent fields, recursive functions, positivity, universe
  constraints, and normalization through reducible aliases.

• Adds proof-carrying singleton and block generation APIs:

  • addInductGeneration / addInductCertified
  • addInductBlockGeneration / addInductBlockCertified

• Generalizes public VEnv.addInduct to supported non-nested mutual blocks. The former singleton behavior remains available temporarily as
  deprecated VEnv.addInductSingleton.

• Establishes exact singleton kernel parity for 14 standard families and 19 actual-metadata replay transactions, plus a consolidated 32-case
  rejection matrix.

• Implements mutual generation for Tree/TreeList and IndexedTree/IndexedTreeList:

  • one motive and recursor per family;
  • globally ordered constructor minors and rules;
  • recursive calls routed by target-family ordinal;
  • families, constructors, recursors, and rules inserted in distinct ordered phases.

• Compares every represented InductiveVal, ConstructorVal, RecursorVal, and RecursorRule field with kernel metadata, including universe order, flags, K behavior, field counts, and every iota RHS.

• Replays singleton and mutual metadata through TrEnv'/Aligned, proving final ordering, lookups, freshness, rule membership, and atomicity.

Trust boundary

The exact sorry audit passes with 25 compiled allowlist entries: 20 source sorry tokens across 19 proof declarations, plus six deliberately rejected fixture-recovery declarations. This PR discharges the previous level-subsumption and level-equivalence obligations, adds no axiom declarations, and preserves the Theory→Verify import boundary.

Validation

All completion gates pass:

lake build Lean4Lean.Verify.Environment.MutualInductiveFixtures
lake build Lean4Lean.Verify.Environment.SingletonParityMatrix
lake build Lean4Lean.Theory Lean4Lean.Verify
lake build Lean4Lean.Audit.SorryFrontier
lake build
nix build --accept-flake-config .#lean4lean .#lake-dependency
nix flake check --accept-flake-config --print-build-logs
nix fmt --accept-flake-config -- --check flake.nix
git diff --check

Remaining scope

This covers singleton and non-nested mutual inductives. Nested flattening and auxiliary families, generated patterns, projections, and the remaining checker/metatheory proof frontier remain future work.