docs: document defeq and type inference related functions - #2
Open
rish987 wants to merge 7 commits into
Open
Conversation
digama0
reviewed
May 18, 2024
digama0
reviewed
May 18, 2024
| pure e | ||
| else | ||
| let r := f.mkAppRevRange 0 rargs.size rargs | ||
| -- FIXME replace with reduceRecursor? adding arguments can only result in further normalization if the head reduced to a partial recursor application |
Owner
There was a problem hiding this comment.
Couldn't it also reduce to a lambda?
Contributor
Author
There was a problem hiding this comment.
Yes, but in that case it would have went into the first branch of the conditional.
rish987
changed the title
digama0
reviewed
Jul 11, 2024
digama0
added a commit
that referenced
this pull request
Aug 4, 2026
* docs: document defeq and type inference related functions Squash merge of PR #2 by rish987. Reference: #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>
samuelburnham
added a commit
to argumentcomputer/lean4lean
that referenced
this pull request
Aug 16, 2026
… groundwork (#4) * chore: bump Lean toolchain to v4.32.2 (#30) * 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 (#33) * 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 (#34) * 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> * ci: add Zulip emoji reconcile workflow (#35) 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 (#12) * docs: document defeq and type inference related functions Squash merge of PR #2 by rish987. Reference: https://github.com/digama0/lean4lean/pull/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> * refactor: remove the dead `cheapRec` parameter `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 #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> * Verify front-end declaration checking (#28) * 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> * verify: model unsafe and mutual definition blocks `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> * Verify the standard library universe level operations (#23) * 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> * verify: drop spurious noncomputable markers on singleton replay rows 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. * inductive: compute of_run by replaying the transparent decomposition 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. * verify: compute staged ofRun packagers by replaying their builders 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. * verify: drop noncomputable markers freed by computable staged owners 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. * verify: add trExprS?, the deterministic shadow of strict translation 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. * verify: compute the generation packages through the deterministic translator 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. * verify: decide the nested inductive representation 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. * theory: flatten nested inductives against target metadata 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. * theory+verify: restore nested generation artifacts and align the transaction 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. * verify: round-trip real nested addInductive output through the artifacts 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. * theory: prove typed transport along constant interpretations 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. * verify: replay the rose nested declaration through TrEnv'.inductNested 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. * verify: replay the nested-indexed fixture and close nested generation 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. * theory: prove the generated iota pattern core for certified blocks 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). * theory: prove pattern soundness and add the block-local 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. * theory+verify: close L4L-11 replay and certificate API * theory+verify: close L4L-12A API extraction * theory+verify: close L4L-12B literal readiness * theory+verify: close L4L-13A/B projection semantics * verify: prove soundness of the standard library normalize 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> * theory+verify: close L4L-14 projection structural laws * fix: make level normalization reconstruction canonical The reconstruction of a Level from a NormLevel picked the imax chain for each sublevel condition set via parent pointers into the key set of the map (findParent/buildPaths). But the keys record which imax chains appeared syntactically in the input, and are not canonical: equivalent levels can produce the same sublevels with different scaffolding keys, yielding different parent choices and hence different reified levels, e.g. max v (max w (imax (imax (imax u v) w) x)) max v (max w (imax (imax (imax u w) v) x)) normalized to distinct levels (and isEquiv' answered false). Replace the parent-pointer scheme with a chain computation that depends only on the sublevels: an edge adding v to condition set S is admissible iff some V(T, v+k) with T ⊆ S is among the sublevels, and each condition set is built by its lexicographically least admissible chain (greedy, with a feasibility check on the remainder; admissibility is monotone in the condition set, so greedy search is complete). Empty nodes are gone from normal forms, so that BEq, and hence isEquiv', cannot see scaffolding keys. There were two sources. `normalize` seeded the map with `[] => default`, because `addConst` used `modify`, which silently drops the constant when the key is absent; it uses `alter` now, as `addNode` already did, and starts from the empty map, so every insertion carries content (measured over all levels of size <= 7 in 4 parameters, `normalizeAux` adds no empty node at all). The other source is inherent: subsumption drains a node when every sublevel at its key is dominated, so that key is erased rather than left empty. This is load-bearing -- at 4356 of those same levels a node drains, the smallest being `imax u (max u v)`, where keeping the key makes `isEquiv'` reject it against `max u v`. NormLevel.le now compares per sublevel rather than per node, which is what Theorem 39 says: a node bundles a constant sublevel with several variable ones, and they may need different dominators. For imax 2 v <= max 2 v the left side is the single node {v} => { const := 2, var := [v+0] } whose sublevels C({v},2) and V({v},v+0) are dominated at different keys of the right side, so geq' answered false. This is reachable: geq' has one caller, the constructor universe check in Inductive/Add.lean, and it made lean4lean reject inductive Foo.{v} (b : Sort v) : Sort (max 2 v) | mk : (Type -> b) -> Foo b which Lean accepts. Rather than searching l2 for one dominator, carry the sublevels still outstanding and let each entry of l2 discharge what it can -- the same domination step minimization performs, so Node.subsume is split into the test that the condition sets are comparable and Node.subsumeBy, which does the discharging and is shared. Its `same` flag distinguishes the two callers, since a node being minimized must not have its variables discharge themselves. Nothing is left to discharge exactly when the node is dominated, so the fold stops there, recovering the early exit of the old single-pass search. leVars is no longer needed: subsumeVars already removes dominated variables in one O(n) merge. Also: fix a typo in the constant subsumption rule, which compared the constant against the node's own variable offsets instead of the subsuming node's (C(E, L) <= V(F, x, K) iff F subseteq E and L <= K + 1); and factor the subsumption step into Node.subsume and NormLevel.minimize, which is behavior-preserving but lets the proofs name the steps. Proof side: `addConst_eval` no longer needs `acc.contains path`, since `alter` creates the entry. In exchange the invariant threaded through `normalizeAux_eval` weakens to `path = [] or acc.contains path`: the root is no longer a key until something is written there, and `addVar`, the one step that still needs the key to exist, is only reached with `path` nonempty. Fuzzed: exhaustive over all levels of size <= 7 (4 params) for soundness of normalize' and round-tripping; exhaustive cross-comparison of all equivalent pairs of size <= 7 (3 params) for canonicity of normalize' and completeness of isEquiv'; exhaustive geq' vs semantic order on all pairs of size <= 5 (3 params), 0 unsound and 0 incomplete; 100k random levels closed under random equivalence-preserving rewrites. Regressions for all of the above go in Tests/Level.lean, together with a bounded exhaustive check that equivalent levels of size at most 5 reify to the same level and are accepted by isEquiv' -- canonicity and completeness are what the proofs do not cover. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * verify: prove soundness of level normalization up to reification normalize_eval, that a level and its normal form evaluate the same under every valuation, is now proved, and with it isEquiv'_wf; neither depends on sorryAx. The reification step normalize' = toTree.reify is still unverified, so this covers everything except turning the normal form back into a Level. The invariant carrying the proof is NormLevel.WF: every variable recorded at a key is an element of that key, and every nonempty key extends another key by a single variable recorded at it. The second half is what makes addConst sound in dropping C(p, 1) for a nonempty p, since along a path whose variables are all nonzero that recorded variable is at least 1; it is also the expressibility property the reconstruction relies on. Since normalize starts from the empty map, a key's parent may be the root while the root is not yet present, so the invariant threaded through normalizeAux is `path = [] or acc.contains path` and WF's parent clause is likewise `p' = [] or s.contains p'`; addVar, the one step needing the key to exist, only runs when path already contains the variable and so is never at the root. subsumption_eval is proved from a fold invariant tracking, for each sublevel of the node being minimized, either a dominating sublevel still present in the node or one at another key of the map. Erasing a drained key is handled together with insertion by a single characterization of the step's lookup, since an absent key and an empty node have the same eval. Node.subsume is characterized through Node.subsumeBy, matching the split the algorithm makes, so the same lemmas serve both minimization and NormLevel.le. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * verify: prove soundness of geq' geq'_wf: if geq' u v reports true then v' <= u' in every valuation, so the constructor universe check in Inductive/Add.lean only accepts levels that really are below the declared one. Completeness is not proved (and is only fuzz-tested); it is not needed for soundness of the checker. The work is in NormLevel.le_eval, which is Theorem 39 of the paper read in the direction the algorithm computes it. For each entry of l1 the algorithm folds over l2 carrying the sublevels that are still outstanding, and reports domination when the fold bails out with none. The proof runs that fold backwards: the bail-out point has an empty node, whose eval is 0, and each step is undone by subsumeBy_eval_iff, which says that discharging against n2 preserves a bound m as long as n2 itself evaluates to at most m. That hypothesis holds because the fold only discharges against keys that are subsets of the key being checked, so on a valuation making the checked key live those entries are live too and bounded by the total of l2. Domination of a constant by a variable (C(E,L) <= V(F,x,K) needs only L <= K+1) is where the condition set has to be all-nonzero: x is an element of F by the WF invariant, so it evaluates to at least 1 there. Since geq' compares normal forms, that half of WF has to survive subsumption; subsumption_vars proves it does, minimization only shrinking variable lists at unchanged keys. The domination step lemmas are stated for subsumeBy rather than subsume, so subsume_const_drop, subsume_eval_le and friends now derive from them instead of repeating the case analysis. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * verify: prove soundness of normalize' normalize' reifies a normal form by building a Tree and turning it into a Level; normalize'_eval says the result evaluates like the input under every valuation, which was the last unverified step of normalization. Tree.eval gives a Tree the value its reification has: the node's own sublevels, plus every child under the imax guard of the variable labelling the edge into it. Tree.reify_eval proves that is the value of the level, the only interesting case being reify's shortcut for a child reifying to zero, where imax 0 a and a agree. Tree.eval_le_iff then characterizes that value: a tree is bounded by m exactly when the sublevels recorded at its nodes are, and so is the V(p, a, 0) that the edge into each node contributes on its own. The edge half is the reason a tree shape is not free: an imax chain built to carry a sublevel adds sublevels of its own. So a chain is only usable if each of its edges is dominated (Dom), and a key is only expressible if its elements can be ordered so that all of them are (Feas). lexChain searches for such an order greedily, which is complete because Dom is monotone in the conditions accumulated so far (the exchange argument), and its feasibility lookahead is exact (feasible_sound, feasible_complete); lexChain_spec concludes that it returns an admissible chain whenever one exists, so its fallback branch is unreachable for normal forms. normalize_feas supplies the hypothesis: WF.feas builds a chain for the map normalizeAux produces, out of the WF parent clause, and Feas transfers to the subsumed map along Covers, since minimization drops a variable only in favour of one with the same name at a strictly smaller key. Covers is what is left of WF after subsumption, which does not preserve WF itself: for `max (imax d b) (imax (imax c b) a)` the key [a, b] drains and is erased, leaving [a, b, c] with no parent key. WF wants the witness at the key; Dom accepts one at a subset of it. The reconstruction itself is characterized rather than bounded. Tree.At relates a path to the subtree at its end, and toTree_spec makes a single pass over the map establishing that every entry is recorded at the end of its chain (WrittenAt) and that everything in the tree comes from an entry (Accounted). A write puts its own entry there and leaves the others alone, either because it lands on a different path, distinct keys having distinct chains since lexChain only permutes a sorted key, or because it lands on the same key and writes the same data. No duplicate-freedom assumption on the child lists is needed: modifyAt_eq decomposes a modify as one entry replaced or one inserted, so an entry either survives it or is the one modified, whichever entry it matched first. toTree_le_iff reads both halves off as one biconditional, and toTree_eval is ext_le over that and NormLevel.eval_le, so the equality comes from dividing the bound over the maxes on both sides. What is left is per-entry: the node the tree records is part of the entry, the sublevel it omits is the edge into it, and an edge is dominated because the chain is admissible. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> * verify: prove completeness of isEquiv' and geq' Semantically equal levels have equal normal forms, and NormLevel.le accepts every valid semantic inequality. The key is a converse to Theorem 39 (separation): evaluating at a valuation tailored to a single sublevel forces a syntactic dominator among the sublevels of the bounding form. Completeness of le then follows from exactness of the subsumeBy fold, and canonicity from the fact that subsumption leaves no sublevel dominated by another slot (Reduced), so mutual domination pins the two maps to be equal. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * verify: prove completeness of normalize' Semantically equal levels reconstruct to syntactically equal levels: the normal forms are BEq-equal, BEq-equal maps have equal toLists (TreeMap equality itself does not follow, since the tree shape depends on insertion order), and the reconstruction depends on the map only through its entry list (addable/feasible/lexChain/toTree congruence). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * fix: absorb the node constant into plain children when reifying An edge labelled `a` whose subtree holds nothing but `V(_, a, k)` contributes `imax (a+k) a`, which differs from the plain `a+k` only at `a = 0`, where the plain form gives `k` instead of `0`. So the guard can be dropped whenever the node's constant is at least `k`, and the constant itself dropped when some child's offset reaches it. Both stay functions of the normal form, so canonicity is unaffected (normalize'_complete is unchanged); only reify_eval needs the new argument, via plainOffset?_eval and reifyChild_ge. Without this, every offset in the input doubled the size of its normal form: u+1 reified to max 1 (imax (u+1) u). Measured over the 522k level occurrences reaching lean4lean's comparison sites while checking Lean+Std+Batteries, the share of levels already in normal form rises from 51% to 67%, the share whose normal form is larger than the input falls from 37% to 17%, and the mean normalized size falls from 5.69 to 3.07 against a mean input size of 2.97. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * perf: use core's isEquiv/geq as the fast path for isEquiv'/geq' Core's versions are sound but incomplete, which is exactly what a fast path needs: when they accept, the levels really are equivalent (isEquiv_wf/geq_wf), and when they reject we fall back to the complete check, so completeness is still supplied entirely by normalize_complete/le_complete and the fast path contributes nothing to it. Replaying the 261k level comparisons performed while checking Lean+Std+ Batteries, core's filter decided every one of the 260894 real equivalences and left only the 340 genuinely inequivalent calls to the fallback. isEquiv' drops from 2941ms to 192ms and geq' from 3728ms to 198ms over that workload, within 2x of core's own routines net of harness overhead. Note this makes isEquiv'/geq' depend on the patch axioms for core's normalize, which the checker already relied on: isEquivList is List.all2 isEquiv, so isEquivList_wf went through isEquiv_wf regardless. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * docs: refresh formalization roadmap for L4L-14 * theory+verify: certify projection inference * theory: certify generated projector iota * verify: certify primitive projection reduction * theory: expose consumer-neutral verification lemmas Move generic spine, primitive-environment, literal-typing, containment, and elimination-mode APIs from Verify into Theory. Preserve deprecated compatibility shims, add a Theory-only import/axiom audit, and record the L4L-15B structure-eta decision gate. * theory: stage structure eta typing infrastructure * verify: prove structure eta roots behind capability * perf: skip the NormLevel for levels with no essential imax A level built from zero/succ/max/param alone normalizes to a map with the constant at the empty key and one single-variable node per parameter, so it can be collected by a sorted merge and the tree read off directly, without building a TreeMap. normalize' dispatches on flat?, and normalize'_eq shows the dispatch is transparent, so normalize'_eval and normalize'_complete go through unchanged. The proof characterizes the map pointwise (NormLevel.Flat): normalizeAux builds it by addConst/addNode, subsumption is the identity on it (a condition set is empty or a singleton and the constant-carrying node has no variables, so nothing subsumes anything), and each singleton key's lexChain is forced, leaving toTree to add one child per parameter in name order. 3.8x on normalize' over an exhaustive corpus of flat levels. Note the kernel does not call normalize' on its hot path -- level comparison goes through isEquiv'/geq', which 5aa2add handles -- so this speeds up canonical-form production rather than checking. sorted_pairs_eq and its helper move up verbatim (plus a docstring), since the new section needs them. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * docs: activate L4L-15R reconciliation and eta divergence policy Roadmap: schedule the v4.33 upstream reconciliation as the active integration-only milestone L4L-15R (merge upstream master 1a16b72d, v4.31 precedent 7f864b45); requeue L4L-15B with the former upstream-approval gate replaced by the documented-divergence protocol (design note, ledger entry, implementation; approved 2026-08-11); retire all jcb/induct references — origin/jcb/formalization2 is the sole publication bookmark. * docs: record v4.33 reconciliation publication origin/jcb/formalization2 was pushed to the L4L-15R merge checkpoint 99a7f8ae; the roadmap's publication wording follows. * docs: approve registered structure eta divergence * feat: verify registered structure eta * feat: implement proof-carrying extension reductions * experimental: land L4L-16A semantic bridge, partial 16B/16C L4L-16A is complete in this change (audited 2026-08-13, plan in plans/l4l-16-completion-plan.md): - The SExpr Params class is proof-carrying: the extra_pat project axiom is deleted, and each ParRed/WHRed/IsDefEqStrong .extra step consumes a Pattern.Action certificate carrying the exact local equality. - Params.Semantic packages the six environment obligations (structureEta, ctor, defn, iotaRule, iotaSite, registered). - VEnv.IsDefEqStrong.mkS translates the current Theory strong judgment, including IsDefEq.structEta, at [propext, Quot.sound]. - The endpoint VEnv.IsDefEqU.sort_invS closes at [propext, sorryAx, Classical.choice, Quot.sound] with no project axiom; the sorryAx sources are exactly the adequacy iota leaf and the WHRedS.defeq accumulator obligation. - SExpr-side forallE_inv and sort_forallE_inv are stated and proved modulo the same leaf. - The four pre-broken prototypes (Stratified, StratifiedUntyped, Stronger, ParallelReduction) are parked as import-compatible stubs; Experimental/UniqueTyping.lean exposes only the valid strong-judgment sort-uniqueness endpoint. - Partial 16B: Ctx.Subst/Ctx.SubstEq container repair, NormalEq.appDF codomain, WHRed.subst .extra, SpineDefEq, LiftEquiv, CtorSpineDefEq and the PatternLeafSpine.aligned refactor are kernel-checked. Gates: default 212-job build, Theory+Verify, 22-entry sorry frontier, whitespace. Lean4Lean.Experimental builds green with the seven known SExpr admissions plus the single adequacy leaf. * experimental+docs: L4L-16B-prime cleanup, milestone re-cut Narrow the Experimental admission set to the measured L4L-16 gate path (plans/l4l-16-completion-plan.md): - Delete the unsound IsDefEqLift.subst: its free section-variable HasType premise admitted the trivial relation, so it claimed lift-stable substitution for arbitrary substitutions. The proved substDefEq remains as the sound form. InferType.subst/inst go with it since their app/lam cases consumed the unsound lemma at HasType := InferType, and their only consumer was InferType.whRed. - Delete the false-as-stated InferType.whRed: the syntax-directed inference judgment has no conversion rule, so all three open cases (major/beta/extra) were unprovable as written. - Delete the unconsumed sorried CRDefEq.trans with an L4L-18A deferral note: its Theory counterpart is five lines from ParRedS.church_rosser, NormalEq.parRedS, and NormalEq.trans, none of which exist SExpr-side, so the joining argument lands once against the finished Theory script. - Delete the never-elaborated Shape.WF.plift comment block in ShapeLogRel.lean (the "stop hides an admission" ledger item was stale; the file is live-sorry-free) and leave a tombstone documenting the rejected principle and its LiftEquiv replacement. - Document the four remaining SExpr admissions in-source: WHRedS.defeq is the one gate-path item (closed by the 16C-prime narrowed form); WHRed.weakU_inv .extra and InferType(S).hasType are off-path deferrals. Roadmap: record the 2026-08-13 re-cut, move the L4L-16C attempt narrative to plans/l4l-16c-adequacy-log.md, correct the stale claims (six-field Params.Semantic, plift, measured sorryAx sources), stage L4L-16D as D0-D4 scoped to the SExpr instances, and move the Theory-side Params.Extension.join instance to L4L-18A. Track the two new ladder-referenced plan files and mirror the tracked set as explicit .gitignore negations. Gates: default 212-job build, 22-entry sorry frontier, whitespace; Lean4Lean.Experimental green with 5 admissions (4 SExpr + adequacy leaf). * experimental: prove classified constructor spines weak-head normal Kernel-checked, sorry-free additions to SExpr.lean on the L4L-16C gate path (plans/l4l-16-completion-plan.md, O1 design addendum): - Pattern.WF.arity_head: descending a pattern arity chain to its head constant classification; with the registered defaults every pattern head classifies as a symbol of the pattern arity. - spine_inj: constant-headed application spines decompose uniquely. - Params.matchesS_symb_head: the subject of any registered-pattern match is a spine whose head classifies as a symbol. - WHNF.ctorSpine: a fully applied spine headed by a .ctor-classified constant is weak-head normal (no pattern match, no major premise, no beta redex at any prefix). - WHRedS.ctorSpine_eq / ctorSpine_determ: such spines only reduce to themselves, and two weak-head reductions of one term onto classified constructor spines land on the same syntactic spine. ctorSpine_determ is the midpoint-agreement fact for the decided root-anchored chain normalization of constructor observations: it makes CtorDefEq trans-node middles syntactically shared, so chain concatenation needs no midpoint typing and no relation composition. The plan addendum records the full architecture and the remaining sub-designs (chain constructor bookkeeping across mono/lift nodes; the InferType principal-types bootstrap that replaces the generic WHRedS.defeq on the gate path). Gates: Lean4Lean.Experimental green, 22-entry sorry frontier unchanged, whitespace clean. * docs: record chain implementation status and S3 bootstrap revision Update the completion plan after checkpoint wolxmups: the syntactic midpoint-agreement layer is landed and kernel-checked; the remaining chain work is enumerated with its one open sub-design (mono/lift bookkeeping). Supersede the "S3-narrow" certificate-carrying route with the InferType principal-types bootstrap after reading the site contracts: the root sites irreducibly need the typed major collapse, which the syntax-directed inference layer provides without uniqueness. * experimental: carry the mirror-aligned spine in exact observations Add the right-anchored aligned spine (CtorSpineDefEq at the primed head and result, with the columns swapped) as a premise of LRS.CtorDefEq.exact, the Algebra exact handler, the fold, and both of_exact_ctor_spines builders. Both real construction sites supply it for free: the constDefEq ctor case uses the same head and result type for both columns, so the mirror is the aligned spine symm, and the nullary case is nil. This is the chain-normalization prerequisite recorded in the plan: a CtorLink can now be reversed (chain symm / left extraction) without re-anchoring a left-anchored relation semantically. Also record the sharpened unlift obstruction: spines at lifted element-shapes may bind non-lift type-shapes, so pointwise spine lowering is not derivable and the chain-level connection design must be decided before toChain. Gates: Lean4Lean.Experimental green, 22-entry frontier unchanged, whitespace clean. * docs: close the chain-level transport design The HasTypeU inversion characterization settles pointwise spine lowering negatively: lam-shaped fields admit arbitrary Pi type-shapes with no payload-preserving lift-shaped form below them, so per-link semantic transport to the root level is impossible in general (the rejected Shape.WF.plift boundary, met from a new direction). Record the forced design: chains glue at the raw layer through the syntactically shared middle spines, cross-link alignment descends from weak constant-type coherence (lemma C), and C needs one new Params.Semantic coherence field (registered lhs heads classify as symbols) to discharge its extra case. toChain execution order updated accordingly. * docs: map the composition impossibility, recommend first-order staging IsDefEq.trans-prime is sort-restricted, closing the last free composition route. Record the complete impossibility map: eliminating the constructor-observat…
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
2 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.
Hi, I've been adding some documentation while trying to understand this implementation better. Regarding the FIXMEs, I've left them in for now just because I was curious if you have any thoughts on them (I think I will also do a bit of experimentation regarding them), but I can remove them before merging. I plan to add some docs for the type-inference functions next.