certified inductive environments, projections, and semantic-inversion groundwork - #4
Merged
Conversation
* chore: bump Lean toolchain to v4.32.2 Exactly two commits touch `src/kernel` in v4.31.0..v4.32.2, and both are fixes: * leanprover/lean4#14498, "fix: kernel to check opaque values for fvars", adds a `check_no_metavar_no_fvar` call to `environment::add_opaque`. `addOpaque` now makes the same call in the same position, between `checkConstantVal` and the `checkType` of the value. * leanprover/lean4#14577, "fix: missing check at kernel inductive declaration", is already mirrored: `Lean4Lean/Inductive/Add.lean` type checks the nested applications against the post-declaration environment, covered by `Lean4Lean.Tests.NestedInductive`. lean4lean had the #14498 bug verbatim, not merely by transcription. `addOpaque` runs `checkConstantVal` and the value's `checkType` inside one `M.run`, so they share one `TypeChecker.State` exactly as C++ shares one `type_checker`. A type that beta-reduces to `False` but whose inference pushes a free variable through the local context leaves that variable in `inferTypeI`; the value can then name it, inference answers from the cache rather than the popped local context, and the declaration is accepted. The leaked variable is `_kernel_fresh.2`, the same name as in the lean4 test for this issue, since `TypeChecker.State.ngen` uses the same prefix and starts at the same index. `Lean4Lean.Tests.OpaqueFVar` pins both directions and is a real regression test: with the `checkNoMVarNoFVar` line removed it fails with "opaque value containing a free variable was accepted". The rest of the diff is not a kernel change. leanprover/lean4#13305 made the new `do` elaborator the default in v4.32.0, which reshapes the terms that `do` notation produces. The `Verify` proofs are written against the legacy shape, and `Lean4Lean/Experimental/ShapeLogRel.lean` proves things about `Option`-monad `do`/`return` definitions the same way, so those four files pin `backward.do.legacy true` with a comment saying why. That keeps the elaborated implementation identical to v4.31.0, which is the conservative choice for a kernel. Migrating the proofs to the new elaborator is follow-up work. Also refresh the toolchain-pinned `Lean.Level` divergence link, and make `stringProof` a `theorem` for the new `linter.defProp`. Validated with `lake build`, `lake build Lean4Lean.Experimental`, and both CI replay commands: `lean4lean Init.Core` checked 1036 declarations and `lean4lean --fresh Init.System.IO` checked 43721. No statement changes and no new `sorry`s. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RFCAQgoGN4ndJA1rxNx9RE * fix: check declaration values for free variables in all three places `check_no_metavar_no_fvar` is called on the value in three places in the C++ kernel: `add_definition` (safe branch, environment.cpp:184), `add_theorem` (:203), and, since leanprover/lean4#14498, `add_opaque` (:217). This branch added the third; the first two were removed deliberately, and `divergences.md` recorded them as redundant. That argument is wrong, and all three are soundness bugs. A free variable in the value is harmless only while inference always consults the local context, and inference also answers from its cache: the type and then the value are checked by the same `TypeChecker.State`, exactly as C++ shares one `type_checker`, so a declaration whose *type* is inferred by pushing a free variable through the local context leaves that variable's type in `inferTypeI`. The value can then name the variable, inference answers from the cache instead of the already popped local context, and the declaration is accepted. With a type that beta-reduces to `False`, the result is a proof of `False` -- confirmed against the v4.31.0 tree, where `theorem Bad : (fun _ => False) id := _kernel_fresh.2` was accepted and `theorem FalseFromBad : False := Bad` then went through on top of it. `addTheorem` is the more serious of the two, being both the common path and, unlike the opaque case, not an upstream bug: lean4 has always had this call. `Lean4Lean.Tests.DeclFVar` replaces `Tests.OpaqueFVar` and pins all three sites, in both directions, and asserts that the rejection comes from the free variable check rather than from some other path, so that it cannot quietly stop testing the cache route. Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com> Co-authored-by: Mario Carneiro <di.gama@gmail.com>
* refactor: migrate to the new do elaborator * refactor: address independent review feedback * refactor: leave ShapeLogRel on legacy do elaborator * tweak formatting --------- Co-authored-by: Mario Carneiro <di.gama@gmail.com>
* chore: bump Lean toolchain to v4.33.0-rc2 * chore: clarify projection comparison names * review: drop speculative kernel checks and document the divergences The kernel hardening in the v4.32.2..v4.33.0-rc2 range splits into fixes for reachable bugs and checks that defend against mistakes elsewhere in the kernel. Lean4lean keeps the former and declines the latter: a check that establishes no precondition of a later step adds proof obligations without contributing an invariant, and the correctness proof is what discharges "we might have a bug". Removed, each with a `divergences.md` entry: * The projection structure-name comparison in `isEquiv`, `isDefEqCore'` and `reduceProj` (lean4#14631). `inferProj` already rejects `.proj S i e` unless the type of `e` whnfs to an application of `S`, so comparison and reduction only ever see projections that have been through inference. Upstream's own test has to plant the declaration under `debug.skipKernelTC` to reach the difference. * The kernel exceptions in `restoreNested` and `restoreCtorName` (lean4#14632), back to `unreachable!` and `assert!`. Upstream states that nothing in that PR is reachable from ordinary Lean code, and the motivation given there -- out of bounds reads once the assertions vanish in a release build -- does not apply to total `Array`/`Option` accesses. * The `_nested` scan on inductive types (lean4#14616). The rewrite touches constructor types only, and an auxiliary is neither in scope while the block's own types are checked nor present afterwards. The constructor scan is kept: it guards a hole that is reachable. * The recheck of the restored constructor and recursor declarations (lean4#14621), which upstream describes as redundant sanity checking. `Lean4Lean.Tests.KernelHardening` now runs the counterexamples upstream shipped with the fixes -- #14577, #14607, #14608, #14613 and the duplicate mutual name -- and replaces the ported `_nested` case with one naming an auxiliary the kernel really generates, so it fails when the check is removed instead of passing either way. Also simplifies the v4.33.0-rc2 compatibility workarounds in `ShapeLogRel`, `Verify/Axioms`, `Verify/Expr`, `Verify/Level` and `Level`. Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
Adds the mathlib-ci Zulip emoji reconciler so PR state (open/closed/ merged) and CI status are mirrored as emoji reactions on Zulip messages that mention lean4lean PRs. Triggers: hourly sweep, manual dispatch, PR close/reopen events, and CI workflow runs. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
* docs: document defeq and type inference related functions Squash merge of PR #2 by rish987. Reference: digama0#2 Adds documentation for defeq and type-inference related functions to improve codebase understandability. * docs: restyle to match the codebase Reflow the docstrings added in the previous commit to the style used in the rest of the codebase: text starts on the `/--` line, `-/` closes the last line, and lines are wrapped at 100 columns (also applied to the new `--` comments, four of which ran to 100-187 columns). Incidental fixes while rewrapping: backtick and modernize the `cheapBetaReduce` example (Lean 3 `λ x, x` -> `fun x => x`, and the body is `xᵢ`, not `x₁`); `inferConstant` documents `.const name ls`, not `.const e ls`; `->` -> `→` and `cheapProj = true` -> `cheapProj := true`. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> * docs: correct the claims that don't match the code The docstrings added two commits ago were written against an older lean4lean and describe several things the code does not do. Rewritten against the current implementation: * `unfoldDefinitionCore` takes a `.const`, not an application with a constant head (that is `unfoldDefinition`); its doc had been copied from `isDelta`. * `isDelta` also requires the right number of universe levels, and the question of which constants delta-reduce is already settled by `ConstantInfo.deltaValue?`, so point at it rather than restating it. * `quickIsDefEq` defers constants and free variables too, not just applications and projections, and it refutes as well as confirms. Same correction in the `lazyDeltaReductionStep` and `lazyDeltaReduction` docs, which reused the wording. * `lazyDeltaReductionStep` hands `.unknown` back to `isDefEqCore'`, not `isDefEq`. * `reduceNat` was missing `Nat.succ`, `land`, `lor`, `xor`, `shiftLeft` and `shiftRight`, and `Nat.beq`/`Nat.ble` yield `Bool`, not `Nat`, literals. * `isDefEqOffset` decides `0 ≡ 0` before looking at successors. * `cheapBetaReduce` also reduces a body with no loose bvars, and leaves `e` alone in every other case, which is the point of the name. * `toCtorWhenStruct`'s `String` example predates `String` becoming a two-field structure over `ByteArray`; use `Prod`. Likewise `tryStringLitExpansionCore` matches `String.ofList`, which is no longer the constructor. * `inductiveReduceRec` applies the rule to the motives and minor premises as well as the parameters, accepts literal major premises, and re-applies the arguments past the major premise. * `inferType` also throws on resource exhaustion, so not "if and only if". * `isDefEqCore` referred to a `check` function; it is `checkType`. * `whnfFVar` uses `whnfCore`, and `whnfCore`'s `cheapRec` is never set. * `RecM.run` and `lazyDeltaReduction` take their limits from `FuelConfig`. All three `FIXME(kernel)` comments are rewritten as statements: each asked a question the code answers -- `cheapProj := true` leaves head projections unreduced, the recursive `whnfCore` call does reach `reduceRecursor`, and the eta-struct case is redundant work that the kernel performs identically -- so none of them is a divergence, and none stays a FIXME. Co-authored-by: Mario Carneiro <marioc@chalmers.se> Co-authored-by: Claude Opus 5 <noreply@anthropic.com> Co-authored-by: Rishikesh Vaishnav <rishhvaishnav@gmail.com>
`whnfCore`'s `cheapRec` flag has never been set to `true` anywhere in this repo, so every `if cheapRec then ... else whnf e` took the `whnf` branch and the flag only cost us an argument to thread through eight functions. It is dead upstream too, so this does not diverge from kernel behavior. The flag was added in 2019 for one caller outside the kernel, `csimp`'s `is_stuck_at_cases`, which wanted to look through recursor applications without paying for delta-reduction. When lean4 commit 14260f454b split `cheap` into `cheap_rec`/`cheap_proj` so `is_def_eq` could use lazy projections alone, that caller moved to a new `whnf_core_cheap` wrapper; lean4#9275 then deleted the old compiler, and with it the only thing that ever passed `cheap_rec = true`. The wrapper survives in `type_checker.h` with no callers. Dropping it makes `reduceRecursor`'s `cheapProj` unused as well, since its sole use was inside the `cheapRec` branch, so that goes too. The `whnfCore` docstring added in digama0#12 loses its `cheapRec` half, keeping a note that the kernel still carries the flag. The `Verify` proofs about these functions go through unchanged apart from the dropped argument, which is the check that behavior is unaffected. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
* fix: match kernel declaration checks * refactor: model verified environment entries faithfully * verify declaration checker correctness * verify front-end environment extension and dispatch * verify: strengthen the front-end statements and restore the model Reworks the environment front-end verification so that the abstract model matches the kernel rather than the other way round, and so that the `add*` lemmas say which constant a step added. Model: * `TrEnv'.opaque` carries the body again (`VDefVal`/`TrDefVal`). `checkOpaque.WF` already established the body translation and typing -- it returned them beside a header-only `VConstVal` -- so it now packages them and `addOpaque.WF` is proved against the restored constructor. * `TrThmVal` is dropped: `TrDefVal` covers theorems once `TrDefVal` uses `ci.value! (allowOpaque := true)`. Without that flag `value!` `panic!`s on `.thmInfo` and `.opaqueInfo`, and since Lean panics return `Inhabited.default` rather than aborting, it silently related `ci'.value` to a junk `Expr`. * `Declaration.IsModelled` is dropped. Nothing consumed it; it only narrowed `addDecl.WF` below the statement `master` already had. The declaration forms that are genuinely outstanding are now `sorry`s in the proof. Statements: * `VEnv.AddConst` and `VEnv.AddDef` record the step an abstract environment takes, including the invisible case, and `addConstCore.WF`/`addDef.WF` conclude them. `AddConst.le`/`AddDef.le` recover the old extension-only conclusion. * `addDefinition.WF` takes no `≠ .unsafe` precondition; the `AddDef` step is claimed under that hypothesis while extension holds unconditionally. An unsafe definition is added before its body is checked, so `AddDef` -- which relates the body to the pre-addition environment -- is false of it, not merely unproven. Construction: * `VEnvs.axiom_of_choice` assembles a `VEnvs` from a pointwise existential by splitting on the three `DefinitionSafety` values. Both extension lemmas build their successor with it instead of `Classical.choose`, and `Verify/Environment` no longer mentions `classical` at all. Implementation: * `addMutual` checks the block under one `M.run` with fixed level parameters, and now requires the members' level parameters to agree (as lean4#14608 does), rather than rebinding `lparams` per member inside a single run. * `checkPrimitiveDef` rejects non-safe definitions. Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
`addDecl.WF` now covers every declaration form except inductives. A recursive `unsafe`/`partial` body is checked in an environment holding the block, so the block's constants are added as axioms rather than as definitions: with the values present a body can delta-unfold the constant being defined, and the resulting judgment has no type-preserving model. `VDecl.mutualDef` adds a block's constants without their defining equations and `TrEnv'.mutualDef` relates it to the real environment, so a member may only be unfolded once the whole block is present. The temporary environment a `partial` block is checked in has no model at every safety level -- its members are present as axioms tagged `safe`, since an `AxiomVal` cannot be tagged `partial`, and their types were only checked at `partial`. `VEnvAt` is the single-level model the type checker actually consumes; `VContext.mk'` and `M.WF.run` are now wrappers over the `VEnvAt` forms. Also adds the three `forIn` rules `addMutual`'s loops need, and `NameSet.contains_insert` on top of the existing `TransCmp Name.quickCmp` instance -- the header loop's `found` set is what supplies the block's `Nodup`. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
* prove soundness of the standard library level operations * level: replace the normalize axiom with a total copy `Lean.Level.normalize` and four of its helpers are `partial def`s. Add `Lean.Level.Total`, a clause-by-clause total copy of them, so the trust assumption in `Verify/Axioms.lean` is the syntactic `normalize_eq : normalize = Total.normalize` rather than a semantic claim about an opaque constant. `eval_normalize` is now an ordinary (still open) theorem. Termination is by `3 * size l + tag l`, where `tag l` is 1 iff `l.getLevelOffset` is an `imax`; that is what makes the `imax` branch's recursion on `mkLevelMax l₁ l₂` decrease when the offset is 0. `Lean4Lean.Tests.LevelStd` checks `normalize = Total.normalize` on all 7320 levels of depth at most 2 over 5 atoms, plus 28920 depth-3 samples. Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
annotatedPiReplay07 and the two aggregator lists it feeds compile fine without the marker; every data field is a plain def. Leftover from an earlier revision where the annotatedPi environment chain was still choice-based.
Add buildExecution totality lemmas at every trace level (positivity, positivity mode, constructor telescope, constructor list, singleton run): a successful checker execution guarantees the transparent decomposition returns .ok. ConstructorValidationRun.of_run now replays buildExecution and discharges the impossible error branch with the totality lemma, replacing its Classical.choice selection. Axiom guards are unchanged; the singleton fixture layer loses its only value-level choice root.
ConstructorCandidateAlignmentTrace.build and
buildConstructorPreFamilySafety already execute the exact audits their
check wrappers erase, so give each a totality lemma (a successful check
guarantees the builder returns .ok) and let the staged D2/D3 owners
match on the builder, discharging the impossible error branch with the
lemma. Both StagedNormalizationCandidate{Post,Pre}FamilyInput.ofRun drop
their Classical.choice selections and become computable.
With of_run and the staged D2/D3 ofRun packagers now replaying their builders, every fixture definition rooted in them compiles: the staged universe/post-family/pre-family inputs, their positivity-alignment helpers, and the cvm/prb test aliases across IndexedVecSemanticReplay, InductiveFixtures, and ConstructorValidityReplay. The definitions still selected through Classical.choice ..._exists generation packages keep their markers; making those computable needs a pure verified Expr-to- VExpr translator.
TrExprS's semantic premises only validate a translation, they never select between candidates, so the strict Theory translation of any IsUnique-fragment expression is computable syntactically. trExprS? is that computation: an env-free structural function over VLCtx that fails only on proj (whose Theory endpoint is an open design decision) and mvar. Agreement replaces soundness: TrExprS.trExprS?_eq proves any derivation's value is exactly the computed one, generalized over the existing value-preserving context alignment so let-bound types stay unconstrained, with literal spines pinned by new toConstructor_eq inversions. The trExprS?_isSome/of_trExprS?_eq wrappers are the replay API for de-choicing the semantic packagers: compute the translation, then transfer the Nonempty witness onto it.
…nslator Assemble the singleton semantic hierarchy choice-free: semanticOfUnique lifts thread trExprS?-computed views from the candidate-expression leaf through constructor, list, family, and normalization layers, with the executable D3 strict-view gate supplying the uniqueness certificates from the staged owner's safety trace. ProducedGenerationShapeCandidate.exactProducedPackage closes the package as data, and all five fixture packages (indexedVec, aliasFormer, annotatedPi, cvm, prb) replay it instead of choosing from their _exists theorems. IndexedVecSemanticReplay, InductiveFixtures, and ConstructorValidityReplay drop every remaining noncomputable marker; the project's survivors are the Experimental classical developments and the recursor-defined spec shims.
johnchandlerburnham
force-pushed
the
jcb/formalization2
branch
from
August 9, 2026 11:29
b7781f6 to
ea73301
Compare
L4L-09A checkpoint. Audit how the implementation stores nested inductives, commit the design decision, and pin both with build-failing probes in Lean4Lean/Verify/Environment/NestedRepresentation.lean; no acceptance behavior changes. The audit: Environment.addInductive flattens nested occurrences into auxiliary families, runs the ordinary mutual path, then restores - the final environment keeps only source families (all = source names, numNested = auxiliary count), restored constructor types, and one recursor per source family plus one per auxiliary family named by appendIndexAfter, all with flattened motive/minor counts and auxiliary rules keyed by previously declared inductives' constructors. No _nested.* constant survives, and the final metadata is independent of auxiliary-name collisions. The decision: the stored Theory payload stays the source VInductDecl with no new field; nested support is an additive artifact coupling the flattened block - which probes show the existing arbitrary-block machinery already accepts - with per-auxiliary specifications (the Theory analog of aux2nested) and a restoration substitution sigma. Probes verify on rose-tree, nested-indexed, and constant-universe fixtures that the port's nested path reproduces Lean's stored metadata exactly and that sigma over the existing flat-block generation artifacts reproduces every stored recursor type and rule RHS, using declaration-world values for constructor types and an instL elimination-offset splice for recursor-world artifacts. Source declarations remain rejected by every current analyzer. Gates: focused, aggregate, and default Lake builds, sorry frontier unchanged (25 known entries), Theory import boundary empty, whitespace clean; Nix proof/dependency build and flake checks run on this committed checkpoint.
L4L-09B checkpoint. Implement the Theory mirror of the kernel's ElimNestedInductive transformation per the committed L4L-09A design. VInductDecl.nestedElimination? (Theory/NestedInductive.lean) flattens a source declaration against caller-supplied, environment-free copies of the nested-into blocks (NestedTargetBlock; NestedTargetBlock.WF ties a copy to a VEnv): target recognition on application spines, the kernel's local-variable rejection for parametric arguments, rewrite without descending into replacements, value-keyed deduplication, auxiliary creation for every family of the target block with level instantiation and simultaneous parameter substitution, canonical appendIndexAfter naming, and a fueled fixpoint over queued auxiliary constructors. nestedStage3 gates acceptance by flattening success plus generation readiness of the flattened block through the unchanged L4L-08 block analyzers; no generated recursor, rule, or replay is claimed. Theory fixtures pin the exact flattened blocks and auxiliary specifications for the rose-tree and nested-indexed fixtures plus four structural negatives. The Verify differential (Verify/Environment/NestedTransformation.lean) proves the Theory flattening equal to the port's ElimNestedInductive output on the three real fixtures - families, constructors, specifications, and stored numNested - ties the hand-written List target block to Lean's stored metadata, and matches kernel accept/reject on the four nearest negatives, pinning the kernel's exact local-variable diagnostic. Gates: focused, aggregate, and default Lake builds, sorry frontier unchanged (25 known entries), Theory import boundary empty, whitespace clean; Nix proof/dependency build and flake checks run on this committed checkpoint.
…saction First L4L-09C sub-checkpoint: the complete generic nested layer. Theory: the total restoration substitution restoreExpr fires bottom-up at each auxiliary spine that completes its block-parameter count - coinciding with restoreNested's top-down pass on generated artifacts - with recursor renaming checked before the constructor-prefix case. NestedBlockChecked.recursors/generatedRules restore the flattened block's generation artifacts onto the appendIndexAfter inventory with declaration-world values instL-spliced by the elimination offset. VEnv.addInductNested inserts source families, source constructors, restored recursors, and restored rules in the four block phases; AddInductNestedTrace pins the exact phase boundaries, and the lemma suite (trace recovery, atomicity, le, freshness, family/ctor/rec lookup, rule membership) mirrors the block transaction through ctorFold_spec/rulesFold_spec. NestedBlockChecked.WF chains per-insertion constant and rule well-formedness along the deterministic phase folds; addInductNested_WF folds it into Ordered preservation, and the new VDecl.WF.inductNested case discharges through VEnv.WF.ordered. Verify: AddInductNestedTrace/AddInductNested alignment mirrors the block trace (real ConstantInfo insertions, TrConstVal translation, RecursorMapKMatches, rule fold), TrEnv' gains the inductNested case, and TrEnv'.wf/aligned/of_value/map_wf/sf_mono are extended. The restoration-parity differential proves the product sigma equal to Lean's stored metadata - every restored recursor name, universe count, and type, and every rule RHS in globally flattened order - on the rose-tree, nested-indexed, and constant-universe fixtures, and the Theory fixtures pin restored names, cleanliness (no auxiliary constant survives), rule counts, and the transaction's final lookups. Environment replay of real Inductive.Add.run output through the new alignment trace remains the open L4L-09C obligation. Gates: focused, aggregate, and default Lake builds, sorry frontier unchanged (25 known entries), Theory import boundary empty, whitespace clean; Nix proof/dependency build and flake checks run on this committed checkpoint.
Second L4L-09C sub-checkpoint. The real-output round-trip runs the port's complete Environment.addInductive on dependency-only kernel environments and compares its entire output - not the ambient elaborator metadata - against the Theory nested artifacts: stored payload families and constructors (universe counts and translated types), numNested against the artifact's auxiliary count, and every emitted recursor's name, universe count, type, K flag, and rule RHSs against the restored inventory in order, on the rose-tree, nested-indexed, and constant-universe fixtures. Nothing on either side is hand-authored: the left side is real Inductive.Add.run-derived output and the right side is computed by nestedBlockChecked?. The roadmap records the L4L-09C position: the generic layer and the metadata round-trip are landed; inhabiting NestedBlockChecked.WF for both ladder fixtures (checker-run certificates on restored artifacts or the general sigma-transport theorem) and driving the replay through TrEnv'.inductNested remain open. Gates: focused, aggregate, and default Lake builds, sorry frontier unchanged (25 known entries), Theory import boundary empty, whitespace clean; Nix proof/dependency build and flake checks run on this committed checkpoint.
Third L4L-09C sub-checkpoint: the sigma-transport core from the L4L-09A design note. Theory/Typing/NestedTransport.lean defines the clean compositional substitution substConst (each interpreted constant replaced by a closed value, level-instantiated per occurrence) with its full commutation calculus against liftN, inst, and instL, plus context-lookup transport. The ConstInterp environment morphism packages what nested restoration provides: interpreted constants become closed values typed at their sigma-image types in the target environment, surviving constants and registered defeqs are sigma-imaged, and the target is Ordered. IsDefEq.substConst proves the typed transport: every Theory judgment of the interpreted environment holds of the sigma-images in the target, with the interpreted-constant case discharged through IsDefEq.instL_r and closed-term weakening, and the extra case through the defeq clause. HasType/IsType/VConstant.WF/VDefEq.WF corollaries give exactly the field shapes of NestedBlockChecked.WF. Remaining transport obligations, recorded in the module docstring and plans/l4l-09c-replay-plan.md: the beta-collapse bridge from substConst to the spine-collapsed restoreExpr on generated artifacts, the per-phase morphism construction for a staged flattened block, and the fixture replays through TrEnv'.inductNested. Gates: focused, aggregate, and default Lake builds, sorry frontier unchanged (25 known entries), Theory import boundary empty, whitespace clean; Nix proof/dependency build and flake checks run on this committed checkpoint.
Fourth L4L-09C sub-checkpoint: the first real nested environment replay. Verify/Environment/NestedReplay.lean replays the stored rose-tree metadata (RoseTree, RoseTree.node, RoseTree.rec, RoseTree.rec_1) over the completed List replay environment. The NestedBlockChecked.WF package is proved outright: every phase constant and every restored rule is typed by direct concrete derivations (type_tac over the staged environments), with the printed artifact literals tied to the computed nestedBlockChecked? artifact by native_decide observations, so the package closure is the standard logical baseline plus the persistent-map container axioms and the named native observations - no sorryAx. The alignment trace inserts the real ConstantInfos with tr_type_expr_tac translations, exact freshness chains, the K-flag agreement, and the literal rule fold, and TrEnv'.inductNested drives the final map and environment into alignment, with Ordered derived and the exact transitional closure guarded. The nested-indexed fixture replay and the milestone close-out remain. Gates: focused, aggregate, and default Lake builds, sorry frontier unchanged (25 known entries), whitespace clean; Nix gates run on this committed checkpoint.
L4L-09C closure checkpoint. The second ladder fixture - the nested-indexed family through PVec - replays from real stored metadata: the PVec family and constructors are staged over the completed Nat replay through TrEnv'.inductStaging (with concrete WF and tr_type_expr_tac translations), and the stored NVTree metadata then drives TrEnv'.inductNested with the complete NestedBlockChecked.WF package proved by direct concrete typing derivations over the exact phase environments, printed artifact literals tied to the computed nestedBlockChecked? artifact by named native_decide observations, exact freshness chains, K-flag agreement, and the literal rule fold. Both package closures carry no sorryAx; the TrEnv' roots carry the usual transitional checker closure, exactly guarded. With both fixtures round-tripping real Inductive.Add.run output through generic packaging and environment replay - comparing every family, constructor, and recursor type and every rule RHS against stored metadata rather than hand-authored declarations - the L4L-09C exit is met and the milestone is pruned from the roadmap ladder: L4L-10A is active. The roadmap records the nested coverage boundary (single-target nesting; breadth belongs to L4L-11) and the proved sigma-hat transport as the generic justification layer. Gates: focused, aggregate, and default Lake builds, sorry frontier unchanged (25 known entries), Theory import boundary empty, whitespace clean; Nix proof/dependency build and flake checks run on this committed checkpoint.
L4L-10A. Every certified mutual block's iota rules are exact SimplePattern.iota patterns, and the block supplies the complete generic Params pattern facts at standard Theory axiom closure. Theory/Typing/Pattern.lean gains the implementation-independent shape layer: HeadConstN/HeadConst spines, of_varN_matches and HeadConstN.matches (varN-tower match inversion/construction), varNPaths capture paths, RecursorIotaPattern with matches_shape/matches_of, bounded subpattern classification (Subpattern.varN_const_le, subpattern_inv, app_subpattern), tower intersection laws (varN_const_inter_some/none, app_inter_varN_const_some, RecursorIotaPattern.inter_some/ inter_varN_const_some), component injectivity (varN_const_inj, RecursorIotaPattern.inj), and Pattern.RHS.appN. Theory/Typing/InductivePattern.lean names the generated rule anatomy (ruleBinders/ruleLhsBody/ruleCtorApp/ruleIdx, rule_lhs by rfl), defines rulePattern (major arity: parameters, motives, minors, and the constructor's result indices; argument arity: parameters plus fields), and matches the exact generated left body against it at the rule's recursor levels (ruleLhsBody_matches). The name-freshness inputs come from the certified blockGeneratedNames nodup bit transported across the normalization boundary (sameTypeHeaders name transport); the major-arity agreement between same-recursor rules is extracted from the analyzer's terminal blockTarget? arity equation through the checked family spine (view_resultIndices_length, env-free). IotaPat couples each rule pattern with an RHS template (the registered right tower applied to the captured common arguments and fields) and a check list (parameter and result-index agreement), closed under a decidable RuleClosure bundle. pat_simple, recover, rule distinctness (rulePattern_inj), pat_uniq, pat_app_l, pat_app_l_uniq, and pat_app_uniq are exactly the Params obligations for the block set, with guarded propext/Quot.sound closures (pat_uniq additionally Classical.choice). No open-environment Params instance is installed. Theory/Typing/InductivePatternFixtures.lean pins two literal-name certified blocks by kernel evaluation: a mutual tree/forest pair (majors 6/6/6, arguments 3/1/3) and a Nat-indexed vector (majors 5/5, arguments 1/4), including RuleClosure by decide and exact pattern inventories. Gates: lake build Lean4Lean.Theory Lean4Lean.Verify, SorryFrontier (25 known, unchanged), and the default build are green; nix gates run on this checkpoint before the bookmark advances. plans/roadmap.md moves the ladder to L4L-10B (pattern soundness and environment assembler).
L4L-10B. A successful match of a certified block rule whose checks hold is definitionally equal to its instantiated RHS template, through the exact rule defeq registered by addInduct, and a block-local assembler builds environments whose defeq sets are exactly generated rules plus separately certified extensions. Theory/Typing/InductivePatternWF.lean builds the typed β-collapse layer at a sorry-free propext/Quot.sound closure: IsDefEq.appN_lamN collapses a lambda telescope applied to a full well-typed spine to the iterated instantiation (instRev) of its body, via instN_lamN/instL_lamN pushes, Ctx.InstN.consTel, OnTel.instN, SpineDefEq with appN_defEq/appN_congr pointwise application congruence, SpineWF.defEq_of_pointwise, and the lamN_wf/forallN_wf tower inversions (clean lam_inv/forallE_inv only). varN_matches_paths reads a match's captures back as the spine arguments; instRev_bvar_lt and map_instRev_bvarRevRange_seg compute instantiation images of reverse bound-variable segments. pat_wf then derives pattern soundness: the redex, decomposed into recursor and constructor spines with spine-form typing and source-pinned major levels (exactly what a verified reduction site holds), is defeq to the applied right tower — by the registered defeq (.extra), spine congruence along the capture spine, per-index tower collapses composed with the parameter/index agreement checks, and the capture computation of the L4L-10A templates. Its guarded closure is exactly the Church-Rosser development's transitional unique-typing closure (propext, sorryAx, Classical.choice, Quot.sound), shedding sorryAx automatically when L4L-16/17 land. Theory/Typing/InductivePatternEnv.lean adds the assembler: CertifiedExtension couples a defeq with its simple pattern, payload, and the spine-level extra_pat coverage equation; assembleEnv runs the block's four insertion phases over a base and folds the extension defeqs; assembleEnv_defeqs/assembleEnv_defeq_cases invert the assembled defeq set exactly (constant phases preserve defeqs, rule and extension folds add exactly their lists); assembleEnv_WF preserves ordering via the block preservation theorem and the rule-fold WF lemma; AssembledPat is the union pattern set with pat_simple and per-extension ext_covers. No global open-environment Params instance is installed: upstream extra_pat demands syntactic pattern matches of registered defeqs, which lambda-tower registrations (including quotDefEq) never satisfy, so the assembler exposes spine-level coverage and pat_wf-derived reduction instead. Fixtures assemble both L4L-10A blocks over the empty base and pin their defeq sets to the generated rules. Gates: lake build Lean4Lean.Theory Lean4Lean.Verify, SorryFrontier (25 known, unchanged), and the default build are green; nix gates run on this checkpoint before the bookmark advances. plans/roadmap.md prunes L4L-10 and moves the ladder to L4L-11.
Closes the last gap in the soundness of Lean's own level operations: eval_normalize (hence isEquiv_wf and geq_wf) is now proved, so those no longer depend on sorryAx — only on the syntactic Total.normalize patch axioms, as the axiom tests now record. The proof is a strong induction on Total.size. The mutual recursion with getMaxArgsAux is untangled by two standalone lemmas parameterized by the induction hypothesis for normalize. The max branch needs two facts about the sort: that it permutes, and that entries with equal level base come out ordered by offset; everything else (mkMaxAux dropping an entry when the next has the same base, and skipExplicit/isExplicitSubsumed dropping subsumed constants) follows from those. Supporting files: * Verify/QSort.lean: verification of Array.qsort, adapted from leanprover/lean4#14658, which the standard library does not yet ship. * Verify/NormLt.lean: normLt is a strict weak order, as qsort_sorted requires. normLt is identified with an Ordering-valued normCmp that compares levels by (base, offset) lexicographically, bases compared structurally; normCmp carries the Std order instances (ReflCmp, TransCmp, LawfulEqCmp), from which normLt's properties follow. * Std/Ord.lean: Rot, the lexicographic-product device transitivity needs. Transitivity of a lexicographic product requires knowing the first components are equal in both directions before consulting the second, so a recursion that visits components in different orders must carry all three rotations of transitivity at a triple. This was already being done by hand for Name.cmp; both now share it. * Verify/Name.lean: the Name.cmp/quickCmp order instances and the NameSet lemmas, split out of Verify/Level.lean so both level files can use them. Name.cmp's TransCmp instance loses its bespoke copy of the above, including the manual rotation shuffling, since Rot.then produces all three rotations of a product at once. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
IsDefEq.trans-prime is sort-restricted, closing the last free composition route. Record the complete impossibility map: eliminating the constructor-observation free closure for higher-order (lam-shaped) constructor fields requires weak heterogeneous transitivity in every branch (raw, semantic, per-link sites, telescope descent), which is the L4L-17 frontier; first-order fields compose with available machinery. Recommend staging: close the L4L-16 leaf for first-order-constructor environments (the whole D0-D2 fixture ladder; Acc is the known exception) behind an explicit stage predicate with a rejection fixture, lifting at L4L-17 — flagged for review before implementation.
Record the 2026-08-13 decision (second resolution in the sort-inversion decision note): instead of staging the leaf claim to first-order constructor fields, merge the L4L-16 and L4L-17 research gates into one mutually founded development. The shape-level stratification supplies the well-founded structure the originally rejected joint route lacked: a level-indexed limited uniqueness is co-proved with adequacy, each level derived from adequacy at that level and consumed by the lam-field composition one level up. The roadmap dissolves L4L-17 into L4L-16 as co-deliverables, the L4L-16 exit absorbs them, and the completion plan marks the staging recommendation superseded. Publication continues to hold until the joint leaf closes.
Rewrite the L4L-16 ladder entry per the roadmap convention that completed narratives live in git history: slices 16A and 16B-prime compress to checkpoint pointers, the active 16C-prime slice states the current five-step joint plan (joint-induction design with the reflection decision moved to design time, chain normalization, InferType bootstrap, recR fixed-tower head, leaf fold and measurement), 16E absorbs the joint co-deliverables and the digama boundary decision, and the dissolved L4L-17 entry is removed with all cross-references updated. Compress the duplicated measured-closure text in the live-debt section to a pointer plus the admission surface, refresh the ladder position row through checkpoint mvmrxuus, and replace the research-branch-optimism risk with the two live hazards (joint induction well-foundedness, with the recorded staging fallback; the never-executed 16D segment). Net -52 lines.
Record the U_n dead end (level-indexed raw domain interchange is not derivable from adequacy: semantic outputs cannot supply the raw argument retyping the lam-field composition consumes) and select the principal-type discipline as the working hypothesis: InferType completeness constructs per-derivation raw defeq chains to the principal type without uniqueness, and syntactic InferType.determ then gives shared-term type agreement by determinism, with trans-prime composing the sort-typed chain steps. Three verification questions (completeness closure, semantic conversion along chains, principal anchoring vs Pi extraction) are recorded; the InferType bootstrap consequently moves ahead of the joint-induction finalization.
Landed in the working tree following the joint-route design (plans/l4l-16-completion-plan.md; verified green this checkpoint): - Joint recursion interfaces: LR.AdequacyAt / LR.JointAt / LR.JointBuilder order the combined recursion (adequacy at 0, uniqueness at n consumed by adequacy at n+1, uniqueness derived at n+1), LogRel.LimitedUniq names the per-level uniqueness contract, and the SExpr-side inversions are parameterized by AdequacyAt. - Reflection decision implemented: SExpr.mk is conservative modulo VEnv.EqUpToLevels (of_mk_eq / reify_mk), fixing the mk-faithfulness story for the joint co-deliverables. - Chain normalization, sorry-free: CtorExact (finite native leaf), CtorFrame (mono/lift/unlift transport retained as data back to the root, never lowering high-level fields pointwise), CtorLink, nonempty CtorPath (no free transitivity), root CtorView (isolated weak-head expansion); CtorDefEq.toChain covers all nine constructors via WHRedS.ctorSpine_determ at shared midpoints, and CtorChain.toCtorDefEq closes the round trip. Verified: Lean4Lean.Experimental green; ShapeLogRel.lean zero sorry tokens including the new 350-line layer; adequacy still exactly the one leaf sorry; SExpr.lean still its four documented admissions; 22-entry frontier unchanged; whitespace clean. The active dependency is the InferType principal-types bootstrap.
Adds the union-level non-overlap laws for a generated inductive block's AssembledPat, in the exact shapes the SExpr Params fields demand: pat_uniq, pat_app_l, pat_app_l_uniq, pat_app_uniq. Three take a single ExtSeparation hypothesis (self/block/uniqueness/pairwise head separation); pat_app_l needs none. Rule-vs-rule cases delegate to the existing block-local IotaPat laws. The cross-term engine is HeadSep.inter_subpattern_none: under head separation a simple pattern intersects no subpattern of another. Its (rule, ext) corollaries app_l_uniq/app_uniq are exported so consumers need not re-derive them, and AssembledPat.recover supplies the inversion that cases cannot perform at a concrete iota pattern. separation_is_necessary witnesses that the hypothesis is not removable: a defn extension whose head collides with a block recursor name refutes the hypothesis-free pat_uniq. A scope note records that one AssembledPat covers exactly one block, since ext_sep is unsatisfiable for two rules sharing a recursor. All proofs are kernel-decide only and axiom-pinned via #guard_msgs; the fixtures file carries the discharge on the mutual PatTree/PatForest block plus the quot extension.
… uniqueness Replaces the level-polymorphic adequacy tower with a fixpoint indexed by stratified typing depth, and repairs the constructor-chain fold that the depth rung audit proved unreachable. Depth tower: IotaWitnessStepAtDepth/ContextualIotaWitnessStepAtDepth state the per-rung leaf obligation, contextualAdequacyAtDepth_of_ iotaSteps produces AdequacyAtDepth by strong Nat induction (forwarding the untouched predecessor family through the step interface, never assembling it inside the induction), and the level-indexed tower becomes a facade over it. SelfAdequateConstStep.of_steps remakes the constant case from the witness's own children/lower data rather than derivation induction, conditional on two named leaf obligations. Chain repair: the fold's per-link uniqueness never types a trans middle term -- after the first link the anchor travels with the term, so the call reconciles that link's own SpineWF result type against the inherited anchor. CtorRetype and the path-valued CtorSpineTypeUniqPath retain that reconciliation at the constructor observation, and the raw consumer surface (foldRaw, rawDefEqAt across CtorPath/CtorChain/ CtorDefEq) is re-landed without RawTypeUniq. The residual therefore carries no depth index and leaves the fixpoint, so it is reachable by a generation-side argument instead of by inversion at a depth no premise names. Additive throughout: no constructor gained a premise and no structure gained a field. Also lands the replayable conversion-path certificate so the fallback legs stop erasing the focused seed, the closed-valuation leaf consumer, and a proof-carrying IsDefEqStrong.defn rule. One admission remains, at the iota leaf.
First instantiations of the SExpr Params/Params.Semantic interfaces on checked declaration histories, staged so each slice adds one kind of declaration. D0: the generated Nat block's two iota rules plus a checked definition, with complete Params and Params.Semantic values and the end-to-end d0SortInvS endpoint. D1: a mutual definition block (VDecl.WF.mutualDef, with a genuine forward reference and a three-layer unfolding chain), the D0-to-D1 transport functor, and d1SortInvS. The quotient half delivers the environment layer and a forcing lemma only: any classifier admitting the quot pattern must class Quot.mk as a constructor, and CtorBundle.hu0 then fails at Prop instantiations. The obstruction is recorded in-source rather than worked around. D2: a checked mutual inductive block step over Tree/TreeList and the first complete structural Params for a live block-inductive environment, with all four non-overlap obligations discharged through the new Theory union laws by kernel decide. Semantic's per-rule replay is left open and pinned by forcing lemmas. Endpoint axiom closures are pinned in-source with #guard_msgs; the only sorryAx any endpoint carries is inherited from the open iota leaf.
Records the design passes that ran against the remaining L4L-16 ladder and the decisions they force. weakN_iff (forward): every shortcut route is refuted with machine- checked evidence -- a proved trans-midpoint re-lift witness, semantic descent impossible by relation design, and Theory Church-Rosser circular down to the Params oracle fields. The surviving route is de-circularized stratified standardization; its W2/W3 rungs are proved and strengthened, leaving the coupled NormalEq/CR cores. Recommends re-scoping the co-deliverable off the 16E gate. Generic instance: a conditional instance is refuted as a route, the D-ladder's transport pattern is shown to be the induction step, and the arbitrary-environment promotion is recommended as its own milestone. CtorBundle.hu0 is recommended for deletion, the Prop wall being intrinsic and general rather than specific to Quot.mk. Promotion map: both 16E co-deliverables already exist as sorried statements, two fields of registeredStructureHeadInversion are false as stated and need a head-classification premise, and promotion is gated on four off-path SExpr admissions plus regeneration of the audit import block. Also folds the 16C-prime rung audit into the roadmap, adds the D1/D2 build templates to the slice map, and tracks the new design docs.
Five sessions of work on the sole remaining admission. The leaf did not close; what changed is that its residual is now a small, named, and correctly located obligation instead of an open-ended fold. The chain wall collapses. `HasTypeStratifiedS.to_core` was discarding the outer conversions of a stratified typing, and those conversions already are a type path -- retaining them (`to_core_path`, the `SpineWF.*_path` family, `constTypeUniqPath`) reduces both fields of `MajorChainAnchorStep` to one statement: Pi injectivity for type paths, `LRS.PiPathInv`. No stratification index, no universe alignment, no collapse. `rootRed` needed no re-certifying subject-reduction lemma after all -- once the per-step lemma names no depth, the induction has nothing to lose -- and it holds in the general form. The fixed-head half lands. The N2 premise change replaces the context-free typed-lower-head existential with a named spine, a telescope, and a registered-type witness at one universally quantified index; `hcap` becomes provably dead weight. `CoherentFixedHeadStep` then follows, conditional on one hypothesis: its application fold spends adequacy at the rung's own depth (an instance the step already holds) and at depth-1 through `isType`, never at the same rung. `FixedHeadTypeValidStep` is discharged outright from the step's strict-predecessor family, with depth zero free because every stratified constructor but two carries a successor index. Two obligations turned out to be false, and both are refuted here rather than assumed. `FixedHeadTerminalRetarget` is `HasType` functionality in disguise, and `FixedHeadTerminalLink` forces the bottom observation -- so the earlier producer discharge was vacuous twice over. Shared cause: a terminal fact stated as a law quantified over observations dies at the bottom observation. The replacement, `FixedHeadTerminalDominance`, is continuation-passing over the reached observation, is implied by the old demand, and is inhabited at exactly the instance where the old one yields False. Also: `Pattern.IotaRule.typeClosed` from `Ordered.closed`, which discharges the nil-valuation side condition without touching the rule structure; `WithCapturesLE` and the telescope retarget; the missing `SpineWF.ret_path`; and a sharpened spine bound. Every change is additive -- no existing statement was altered.
Records five machine-checked verdicts that move the L4L-16C-prime endgame, three of them negative and all of them load-bearing. The leaf cannot close inside 16C-prime as scoped. `PiPathInv` is not provable by path-, spine-, or depth-level argument: the chain-wall repair removed exactly one field of the old inversion package and nothing more, and the depth-indexed escape route dies twice over -- the layer transport needs bounded output where a rung yields bare output (the gap is equivalent to a uniform stratification bound that would make the depth induction vacuous), and the chain leaf cannot supply anchors that grow per conversion edge along an unbounded chain. Route yield: spines of length one. Church-Rosser is a hard dependency but not a sufficient one, and the expensive branch was never necessary. `TypeWHNFEx` -- normalization -- is not needed: `PiHeadNorm` follows from confluence plus standardization by transporting a Pi that already exists, and Theory already proves the analogue via `ParRedS.standard`. What confluence cannot supply is sort/Pi shape disjointness, which the leaf provably entails in four lines, so no scoping of 18A-prime escapes it. The 12-rung ladder is 8/12 machine-checked; implement by transport, not by porting. For the definitional-unfold budget, both rung-local routes are refuted (the depth measure does not decrease along delta, and producer-side retention is bounded by what the seed already carries). The fix is a third well-founded component ordered rank-outermost, indexing derivations rather than subjects -- and the rank cannot be derived, because `VEnv.WF` admits delta-cycles: mutualDef adds every block constant before checking any value. That also constrains the generic instance construction, and is a point where the model is more permissive than the kernel it models. Adds the 18A-prime scoping doc, folds the D1/D2 templates and the 16E recon into the ladder, and corrects a stale claim in SExpr that nothing on the gate path consumes CRDefEq.trans.
Discharges the first of the two Church-Rosser .extra holes -- the case where a parallel step meets a proof-carrying user-defeq pattern step at a constant head. Only two of the four predicted lemmas were needed. The key one is `EqUpToLevels.instL_equiv`, a purely syntactic level congruence: the existing `EqUpToLevels.instL` demands an `IsDefEqStrong` derivation for the term, which a closed `Pattern.RHS.fixed` template does not have and cannot be given. Around it, `EqUpToLevels` gains the symmetry it was missing, `apply_instL` lifts the congruence through `Pattern.RHS.apply`, `normalEq`/`normalEq_r` bridge to `NormalEq` on either typing side, and `Check.OK.instL_equiv` transports pattern checks along equivalent level lists. The surviving hole, the appDF overlap, is left untouched: it is false as stated under `[Params]` alone. With a Prop-typed argument position, an application of a registered contraction is reduction-normal on one side while the other contracts, and no `NormalEq` constructor relates the results -- `structural` is uninhabited without structure-eta, and `proofIrrel` would need the result type in Prop. Lean's own large-eliminating Prop inductives realise this shape; for `Eq` the kernel recovers by K-style reduction, which the pattern language cannot express. Closing it needs a semantic side condition relating the sort of a contraction's argument position to that of its result. The predicted blocker was wrong in an instructive way: proof irrelevance at a pattern head is already handled, and the difficulty is at a pattern argument.
Two results that shrink the leaf's obligation set rather than discharge it. R11: Pi injectivity for a single conversion edge, from the Church-Rosser ladder. It is cheaper than the ladder recorded -- it needs no weak-head reduction, so it sits strictly below that rung rather than beside it, and it costs only the proof-irrelevance disjointness fact, because knowing both endpoints are Pis makes the eta cases structural. The conclusion must stay path-valued: parallel-reduction Pi inversion cannot be iterated along a chain, since codomains live in shifting contexts and there is no context-conversion lemma, so each step is converted to a typed equality and the codomain walked one edge at a time. Collapsing instead would charge raw type uniqueness. The Pi component transport turns out not to be an obligation at all. Its two reducts reduce the same subject, so weak-head determinism collapses them; and its remaining conjuncts are the same statement one shape level down, not new data. Written as an induction on the shape level, three constructors are trivial, sort is level-uniform, forallE recurses, and only the inductive-type head is left -- a head-form transport with no upstream analogue, since Theory's reduction family stops at sort and Pi. So the convert step demands nothing beyond the leaf itself. With those in place the constructor-spine type discipline and both fields of the chain anchor step close end to end from the leaf, with no adequacy rung and no raw type uniqueness. Docstrings throughout now record that the ladder is interderivable with the leaf rather than a reduction of it: the parallel-reduction facts depend on sort inversion and stratified Pi inversion, which are the milestone's own deliverables, so the route closes a loop. The essential uses are the two beta cases, each reconciling an application's domain with its abstraction's own -- subject reduction for beta needs Pi injectivity.
Corrects a claim recorded here earlier today. The parallel-reduction facts do not depend on weakN_iff; measured with a dependency-closure walker (print axioms reports that a sorryAx exists, never which), their roots are sort inversion and stratified Pi inversion -- the milestone's own deliverables. The leaf's residual is definitionally the theorem that gets promoted into the latter, so the Church-Rosser route closes a loop and cannot discharge the milestone. weakN_iff remains a real obligation but gates confluence, not these facts. Also records the appDF counterexample, the shape-disjointness result (three of four facts need no adequacy rung, the fourth needs rung zero), and the delta-cycle finding that constrains the generic instance.
The Church-Rosser ladder and the 16C-prime leaf are interderivable, so the ladder cannot discharge the leaf. This lands the other direction, which is useful: the moment the leaf lands, the whole ladder follows natively, and the sorryAx that Theory's parallel-reduction facts carry retires with it. Moves TypeDefEqPath and its API from the shape-relation module into SExpr, where its dependencies actually live -- every existing consumer re-elaborated unchanged. On top of it, three structural inversions: app_inv', lam_inv' and forallE_inv_path. Each returns the type path from the subject's own type to the declared type, which is what removes the type-uniqueness fixups needed wherever a typing is inverted at a converted type. None of them reaches IsDefEq.strong. The consumer direction turns out to need no side conditions. The pattern-action step is a uniqueness step in content, but every such redex is a constant-headed spine and spine uniqueness already reduces to the leaf, so it follows from the leaf directly -- and with it the rung, the single-edge inversion, and the rest of the ladder. The path collapse is landed too, with its trade recorded: collapsing a path to a single edge costs raw type uniqueness, so the single-edge framing exchanges this milestone's leaf for the L4L-17 co-deliverable rather than avoiding it. Also banks the closure records for the routes measured dead today: the beta congruence needs no Pi-inversion, the contraction does; sort typedness constrains the result type and never the domain; and the stratified ladder's anchor demand is equivalent to a uniform stratification bound, so a perfectly stratified rung still could not be consumed.
Records the proved interderivability of the ladder and the leaf, the three corrections that came with it, and an explicit instruction not to open the stratification work: its producer-side obstruction does not apply, but the consumer-side one does, verbatim. Leaves the joint/adequacy route as the only one standing for the leaf.
…▷-island half The hu0 discriminating experiment ran to completion and REFUTES the recorded deletion recommendation: the ADQ consumption site is free (u ≠ .zero is derivable there, probe P4), but build_spine's post-deletion statement is false for Prop-sorted ctor-classified pattern-argument heads — the shape algebra's proof-irrelevance law (WShape.HasType.proofIrrel) requires .indTy non-Prop-sortedness, and hu0 is that law's syntactic mirror. Landing a deletion needs a Prop-branch at the Matches/classification level or exclusion of Prop-recursor iota patterns from Pat. Probe preserved at plans/probes/probeA1-hu0.lean (local). Deleted with zero-consumer evidence: Params.ctor_ty; InferType.hasType and InferTypeS.hasType (both sorried); InferTypeS.weakU_inv; LRS.iotaDefEq_of_exactAt; LR.iotaActions_of_exact. WHRed(S).weakU_inv kept: live via InferType.weakU_inv and LogRel.lean's LRIsType.weak' stuck case. WHRedS.defeq live sites reduced 11 → 3, all on the adequacy trunk. SExpr.lean sorries 4 → 2; gates: Experimental 143 jobs, default 212 jobs.
…and its soundness core Triage: all five IndTyHeadNorm consumers are CR-conditional (convertStepAt_all, PiComponentTransport.of_crLadder, FixedHeadConvert*.of_crLadder*), so the Prop is not on the mandatory leaf path — correcting the premortem's 'only such residual' framing. Landed the soundness-derivable middle factor LRS.indTyShapeTransport (additive, pinned clean); the two flanks (whr-expansion = SubjectRedS; the indTy adequacy observation) are leaf-equivalent and stay with the banked consumer direction. Also banked locally (untracked probes): probeD-deltarank2.lean — δ-rank fields shaped to LR.ConstDefnDeepInstStep's consumption, D0/D1 inhabitation with literal ranks (D1 inverts declaration order inside the mutual block), constDefnDeepInstStep_of_rank produced outright; residual pinned to the rank-outermost recursion for the un-narrowed ConstDefnDeepStepR. Wiring plan: a new class Params.DeltaRank [Params], one instance per D-ladder rung. RectFrame index-upgrade assessment: ~50+ declarations, parked; material finding — the type shape is recoverable (always indTy at ctor observations, lift-stable), so an additive CtorFrame.toRectFrame bridge at a := q := indTy plus a ~10-line WShape.le_ctor inversion should retire the recorded non-additive obstruction.
…he measured D2/sorry-count corrections - probeA1: the recorded CtorBundle.hu0 deletion is refuted at build_spine (the shape proof-irrelevance law is hu0's semantic mirror); ADQ site free; D1 quot stays design-blocked. Completion plan + roadmap corrected. - The stratification axis for the 16C' leaf is machine-refuted and banked: plans/l4l-16-stratified-observation-design.md (now tracked) + plans/probes/probeT-stratpi.lean — chainAnchorAt_false, uniformStratBound_false, transMiddleCertAt_false, valTyPi2D_iff_bare; L1 re-indexing inherits the wall at trans middles. - D2 record corrected: the per-rule iota 'checked' is 18A'-strength (stuck inductive-application injectivity at Tree's parameter), and the true per-rule volume is ~1400-1700 lines incl. the registered tower. - Promotion map addendum: deletions landed (SExpr sorries 4->2), the weakU_inv 'dead chain' claim corrected (live via LogRel.lean:210), WHRedS.defeq trunk sites now 3.
…tion's type shape is recoverable Banks probe R13's residual as additive machinery instead of the recorded non-additive index change: WShape.le_ctor (the missing right-hand inversion, full iff), hasType_indTy_of_le, hasType_indTy_lift, the live LRS.RectFrame with rect/symm_rect/trans and a non-vacuity witness, and the bridge LRS.CtorFrame.toRectFrame at a := q := .indTy with its end-to-end corollary CtorFrame.rect — at a ctor observation the type shape is not a choice to thread but a fact to recover, so no frame producer changes. All pins sorryAx-free. Remaining well-scoped follow-up: thread a RectFrame at the rec-app observation (out, outTy) for the CoherentIotaLeafStep mechanical layer; probeR13 is superseded.
…ay engine Convert the rule-independent part of the D-ladder's Params.Semantic work into two generic modules and make D2 their first consumer. R1 (SExprTransport.lean): transportLevel/transportExpr generic in univs agreement, with congruences, roundtrips, and lift'/subst/inst/mkInst/applyS/ defeqsS/MatchesS/Lookup commutation. Proof-complete at [propext, Quot.sound]. R2 (SExprGenericReplay.lean): the Replay certificate, the generic type-uniqueness and spine-view tower, and ruleCollapse — the entire reify/instL_lamN/lamN_wf/retarget/appN_lamN/mkS chain that D0 and D1 inline once per rule, proved once and sorryAx-free — plus the site assembler iotaSiteOf. D2: d1StrongToD2 on top of R1, then unconditional Semantic.ctor (with all five Tree/TreeList constructor bundles, hu0 supplied — nonzero imax towers) and Semantic.defn, and the inherited half of Semantic.registered. The block half is parked as one named premise D2BlockStep, whose checked component is L4L-18A'-gated (stuck inductive-application injectivity) and whose other three components are per-rule volume the engine takes as input, as Theory's own generic block-rule theorem does. Endpoint d2SortInvS is conditional on that premise and pinned; its sorryAx enters only via the pre-existing 16C' leaf. Corrects the in-file record: the residual is not pure volume, and the D1->D2 transport functor is no longer missing. Capture spines are an interface boundary (Theory's generic theorem takes them as hypotheses too), and reduction sites do not transport downward — D2BlockStep therefore also re-covers the two inherited Nat rules, where checked is trivially true.
…nd the D2 generic-engine status Roadmap 16C': the stratification lever is machine-refuted (probeT + tracked design doc), and the registered-endpoint narrowing (probeU + tracked design doc) collapses the chain-fold interior — general PiPathInv demands drop to the two root callbacks, both provably outside the registered class; PiPathInvReg is not path-inductable (U8). The typed-constructor-view probe decides the endgame shape. 16D D2 row: generic R1/R2 engines landed, endpoint conditional on D2BlockStep with the 18A'-gated checked component. D1 quot row re-pointed at the Prop-wall design (hu0 deletion refuted).
johnchandlerburnham
changed the title
samuelburnham
approved these changes
Aug 16, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
6 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
This PR develops the proof-carrying path from Lean4Lean's executable
inductive checker to its implementation-independent Theory.
It adds:
generation;
certificates;
D0-D2 environments and replay infrastructure;
sorry-frontier audit.
This is a development integration PR, not a claim that Lean4Lean is already
proof-complete or kernel-complete. Supported
Theory/Verifyadditions aregated and audited; unfinished semantic-inversion work remains under
Experimentaland is not imported by a supported root.At head
06f13e02, the PR contains 83 commits affecting 142 files, withapproximately 79k additions and 6k deletions relative to
dev.Motivation
A successful executable inductive check should produce enough evidence for
downstream checkers to recover, without additional oracles:
The branch establishes that vertical slice while keeping implementation
metadata and checker-run evidence in
Verify. It also records the remainingtrust and metatheory obligations explicitly instead of hiding them behind broad
semantic assumptions.
Main changes
Lean 4.33 and reproducible builds
v4.33.0final and the new do elaborator.b292275c.including soundness and completeness for
normalize',isEquiv', andgeq'.downstream-consumer fixture.
Certified inductive generation
The Theory layer now models inductive processing as one proof-carrying
artifact path:
The resulting certificates cover:
GenerationCertificate,ValidationCertificate,BlockCertificate, andNestedBlockCertificateexpose the resulting Theory consequences withoutcarrying
Lean.Expr, checker state, or Verify-specific normalization evidence.Mutual and nested inductives
Mutual blocks share one validated parameter prefix and semantic result
universe while retaining family-specific indices and constructor inventories.
Supported nested declarations use a dedicated path:
nestedElimination?;Rose-tree, nested-indexed, and deep two-parameter fixtures compare restored
Theory metadata with actual kernel output and replay the resulting transactions
through
TrEnv'.inductNested.Generated iota patterns and reduction certificates
Certified generated rules now carry:
SimplePattern.iotadescriptions;The block-local assembler constructs an environment whose registered equations
are exactly the generated block rules plus explicitly certified extensions.
L4L-18B separates three formerly conflated responsibilities:
IsDefEqUcertificate carried by every operational contraction;Params.Extension.joinobligation for raw registered equations.This avoids treating pattern coverage or registration as an implicit soundness
oracle.
Verify alignment and differential fixtures
Checker-run certificates retain the exact operational evidence needed to
connect executable processing to Theory, including:
The regression surface includes:
nested blocks;
closure.
Theory-only consumer APIs
Consumer-neutral definitions and lemmas now live under
Lean4Lean.Theory:VEnv.PreludeReady;Tests/TheoryConsumerSurface.leanverifies that these APIs are availablewithout importing
Lean4Lean.Verify.Projection semantics and checker verification
Theory/Projection.leanmodels projections as recursor programs derived fromthe same checked structure artifact used by inductive generation.
It provides:
universe instantiation;
TrProj.structuralLawsinterface.Verify's projection translation is constrained by a concrete registered
structure view. The former projection specification placeholder is removed,
and
inferProj.WFplus constructor/string branches ofreduceProj.WFareproved.
Registered structure eta
L4L-15B adds an explicit
VStructEtadescriptor and monotone environmentregistry for the nonrecursive, single-constructor, zero-index structures
accepted by the kernel's structure-eta path.
The new Theory equality rule retains:
Weakening, substitution, strong typing, standardization, nested transport,
parallel reduction, and exhaustive equality consumers carry the new case. The
executable
tryEtaStructCore.WFandisDefEqUnitLike.WFroots are consequentlyproved.
This is a deliberate semantic divergence tracked as D019 in
upstream-divergence.md.Experimental L4L-16/17 route
The former L4L-17 work has been merged into the joint L4L-16 route.
The current experimental stack includes:
D2BlockStepExact/d2SortInvSExactresidual boundary.These declarations compile, but they are not promoted into the supported
Theory/Verify surface.
The remaining boundary is explicit:
RectFramesynchronization and terminal fixed-head dominance underLRS.PiPathInv;seven beta-collapses, and five registered towers.
No conditional endpoint is presented as unconditional.
Trust and proof status
Lean4Lean/Audit/SorryFrontier.leaninspects compiled declarations rather thansource text. It accepts exactly 22 declarations:
recovery introduces
sorryAx.Any added, removed, or renamed entry fails the audit until the allowlist is
deliberately updated.
The 16 genuine obligations are split between:
results.
The repository also retains 34 classified project-specific axioms. Their
ownership, reachability, and intended retirement are recorded in source-level
axiom guards and
upstream-divergence.md. They remain transitionalimplementation contracts, not a claimed final foundation.
Important boundaries:
contracts;
Experimentalis outside Lake's default targets and cannot silently enterthe supported proof surface.
Compatibility and behavioral notes
leanprover/lean4:v4.33.0.VEnv.IsDefEqgains the registered structure-eta constructor, so exhaustivedownstream consumers must handle it.
deriving soundness merely from pattern membership.
addInductSingletonremains as a deprecated migration wrapper; newconsumers should use block certificates.
exact executions provable.
widen accepted input.
Deferred upstream integration
This branch includes digama0's upstream history through
b292275c.Five later upstream commits are intentionally deferred to the start of
L4L-19:
aaeeb156- stage-2 replay performance;3f6e8f92- level-algorithm wiring, partially convergent with this branch;62441418- lazy delta/projection reduction;4b60e53d- K-target ordering and divergence documentation;e0e3f6bc- level-equivalence coNP-hardness.The projection-reduction change overlaps the branch's independently proved
reduceProj.WFarchitecture. Reconciling it at L4L-19 avoids rewriting thecurrent semantic-inversion work against a moving checker implementation.
Review guide
779c51fthrough99a7f8ac0b04d7through0587b91958d03bthroughc62085d97cab5dthrough7c1e89f96aeab59aa2a4fthrough06f13e0The highest-value semantic review points are:
registered-equation joins;
The large replay files are primarily executable evidence for those interfaces.
Not claimed by this PR
b292275ccommits.These remain follow-up work and are not prerequisites silently assumed by any
claimed endpoint above.
Verification
Current head
06f13e02passes:The flake checks include the supported proofs, tests, downstream-consumer
build, and CLI smoke tests on
x86_64-linux.Tracked review anchors
upstream-divergence.md- per-delta ownership and removal conditionsLean4Lean/Audit/SorryFrontier.lean- exact supported sorry frontierLean4Lean/Theory/Inductive.lean- checked block and generation artifactsLean4Lean/Theory/Typing/InductiveCertificate.lean- consumer certificatesLean4Lean/Theory/Projection.lean- consumer-neutral projection semanticsLean4Lean/Experimental/SExprParamsD2.lean- exact current D2 boundary