certified inductive environments, projections, and semantic-inversion groundwork

.gitignore

@@ -1,6 +1,20 @@
 /.lake
-/result
+/result*
 /.direnv
 # Keep scratch plans local while versioning the authoritative execution ladder.
 /plans/*
 !/plans/roadmap.md
+!/plans/l4l-15-structure-eta-design.md
+!/plans/l4l-16-sort-inversion-decision.md
+!/plans/l4l-18b-extension-interface-design.md
+!/plans/l4l-16-completion-plan.md
+!/plans/l4l-16c-adequacy-log.md
+!/plans/l4l-16c-buildp-premortem.md
+!/plans/l4l-16d0-slice-map.md
+!/plans/l4l-16e-promotion-map.md
+!/plans/l4l-16-weakn-design.md
+!/plans/l4l-16-generic-instance-design.md
+!/plans/l4l-18a-prime-scope.md
+!/plans/l4l-16-stratified-observation-design.md
+!/plans/l4l-16-registered-pi-design.md
+!/plans/l4l-16-typedview-design.md

Lean4Lean/Audit/SorryFrontier.lean

@@ -2,15 +2,19 @@ import Lean4Lean.Theory
 import Lean4Lean.Theory.ConstructorValidityFixtures
 import Lean4Lean.Theory.Inductive
 import Lean4Lean.Theory.InductiveFixtures
+import Lean4Lean.Theory.Literals
+import Lean4Lean.Theory.LocalContext
 import Lean4Lean.Theory.Meta
 import Lean4Lean.Theory.MutualInductiveFixtures
+import Lean4Lean.Theory.Projection
 import Lean4Lean.Theory.Quot
 import Lean4Lean.Theory.SingletonParity
 import Lean4Lean.Theory.Typing.Basic
 import Lean4Lean.Theory.Typing.ChurchRosser
 import Lean4Lean.Theory.Typing.Env
 import Lean4Lean.Theory.Typing.EnvLemmas
 import Lean4Lean.Theory.Typing.HeadReduction
+import Lean4Lean.Theory.Typing.InductiveCertificate
 import Lean4Lean.Theory.Typing.InductiveLemmas
 import Lean4Lean.Theory.Typing.Injectivity
 import Lean4Lean.Theory.Typing.Lemmas
@@ -31,6 +35,7 @@ import Lean4Lean.Verify.Environment.CandidateIdentityReplay
 import Lean4Lean.Verify.Environment.ConstructorValidation
 import Lean4Lean.Verify.Environment.ConstructorValidityMatrix
 import Lean4Lean.Verify.Environment.ConstructorValidityReplay
+import Lean4Lean.Verify.Environment.DeepNestedReplay
 import Lean4Lean.Verify.Environment.Elimination
 import Lean4Lean.Verify.Environment.EliminationFixtures
 import Lean4Lean.Verify.Environment.EliminationFixturesCommon
@@ -46,6 +51,7 @@ import Lean4Lean.Verify.Environment.IndexedVecConstructors
 import Lean4Lean.Verify.Environment.IndexedVecOuterReplay
 import Lean4Lean.Verify.Environment.IndexedVecSemanticReplay
 import Lean4Lean.Verify.Environment.InductiveFixtures
+import Lean4Lean.Verify.Environment.InductiveReplayMatrix
 import Lean4Lean.Verify.Environment.Lemmas
 import Lean4Lean.Verify.Environment.MutualInductiveFixtures
 import Lean4Lean.Verify.Environment.Normalization
@@ -81,7 +87,7 @@ token), so it can never drift from Lean's lexer over comments, string/char
 literals, or nested block comments. Attribution is by SOURCE MODULE via
 `getModuleIdxFor?`, so a declaration is charged to the file that defines it even
 when it sits in a foreign namespace (e.g. `Lean.Level.isEquiv_wf` lives in
-`Lean4Lean.Verify.Level`).
+`Lean4Lean.Verify.LevelStd`).
 
 The audited surface is exactly the modules reachable from this file's imports:
 importing a `Theory`/`Verify` module here is what brings it into scope. A sorry
@@ -126,30 +132,46 @@ private def surfacePrefixes : Array Lean.Name := #[`Lean4Lean.Theory, `Lean4Lean
 S (missing specification), P (stated but sorried, blocked on S), V (checker
 verification, blocked on S/P), R (research-grade metatheory, upstream-driven). -/
 private def allowlist : Array Lean.Name := #[
-  -- Tier S — missing specification
-  `Lean4Lean.TrProj,
-  -- Tier P — blocked only on Tier S
-  `Lean4Lean.TrProj.weak',
-  `Lean4Lean.TrProj.weak'_inv,
-  `Lean4Lean.TrProj.defeqDFC,
-  `Lean4Lean.TrProj.wf,
-  `Lean4Lean.TrProj.uniq,
-  `Lean4Lean.TrProj.instN,
-  `Lean4Lean.TrProj.instL,
-  -- Tier V — checker verification, blocked on Tiers S/P
-  -- (NormLevel.subsumption_eval and Level.isEquiv_wf were proved on the
-  -- formalization line, 2026-08-05/07, and left the frontier.)
+  -- Tier V — checker verification, blocked on Tier P
+  -- (NormLevel.subsumption_eval and the primed-comparator soundness were
+  -- proved on the formalization line, 2026-08-05/07, and left the frontier;
+  -- the v4.33 reconciliation then absorbed upstream's stronger level
+  -- verification.)
+  -- After upstream #28 (v4.33 reconciliation), `addDecl.WF` is proved for
+  -- every declaration kind except `inductDecl`, whose case is the remaining
+  -- sorry (L4L-19B territory).
   `Lean4Lean.addDecl.WF,
-  `Lean4Lean.TypeChecker.Inner.inferProj.WF,
+  -- Upstream's front-end trust boundary for the syntactic primitive-definition
+  -- recognizer (Verify/Environment/Boundaries.lean), added by #28 at the
+  -- v4.33 reconciliation.
+  `Lean4Lean.checkPrimitiveDef.WF,
+  -- `ProjectionReady`/registered `StructureEtaReady` transport across the
+  -- front-end environment extensions (Verify/Environment/Extension.lean):
+  -- upstream's proved v4.33 declaration chains do not establish these fork
+  -- obligations on `VContext`; the transport proofs are L4L-19B content. The
+  -- mutual-block entry is the compiled recursive functional of
+  -- `VEnvAt.addAxioms`.
+  `Lean4Lean.VEnvAt.addAxioms._f,
+  `Lean4Lean.addConstCore.WF,
+  `Lean4Lean.addDef.WF,
+  `Lean4Lean.addMutualBlock.WF,
+  `Lean4Lean.addUnsafeDef.WF,
+  -- Quotient initialization (Verify/Environment.lean): upstream's v4.33
+  -- proof was vacuous via the fork-refutable `TrEnv'.no_inductInfo`; the
+  -- constructive connection to the Theory quotient transaction is L4L-19B
+  -- content.
+  `Lean4Lean.addQuot.WF,
+  -- v4.33 reconciliation repair debt: the exact alignment-run fixture's
+  -- `build.eq_def` stepping no longer elaborates; the closed checker-run
+  -- statement is unchanged (Verify/Environment/InductiveFixtures.lean).
+  `Lean4Lean.InductiveReplayFixtures.aliasFormerAlignmentRun,
   `Lean4Lean.TypeChecker.Inner.reduceRecursor.WF,
-  `Lean4Lean.TypeChecker.Inner.reduceProj.WF,
-  `Lean4Lean.TypeChecker.Inner.tryEtaStructCore.WF,
-  `Lean4Lean.TypeChecker.Inner.isDefEqUnitLike.WF,
   -- Tier R — research-grade metatheory (upstream-driven, not scheduled)
   `Lean4Lean.VEnv.IsDefEqU.sort_inv,
   `Lean4Lean.VEnv.IsDefEqU.forallE_inv_stratified,
   `Lean4Lean.VEnv.IsDefEqU.sort_forallE_inv,
   `Lean4Lean.VEnv.IsDefEqU.weakN_iff,
+  `Lean4Lean.VEnv.WF.registeredStructureHeadInversion,
   `Lean4Lean.VEnv.NormalEq.parRed,
   -- Tier F — deliberately kernel-rejected inductive fixtures. Elaborator error
   -- recovery admits the invalid `inductive` with `sorryAx`, so the constant

Lean4Lean/Environment.lean

@@ -31,22 +31,21 @@ def addDefinition (env : Environment) (v : DefinitionVal)
     if check then
       _ ← (checkConstantVal env v.toConstantVal).run env
         (safety := .unsafe) (lparams := v.levelParams) (fuel := fuel)
-    let env' := env.add (.defnInfo v)
+    let env' := env.add (.axiomInfo { v with isUnsafe := true })
     if check then
       checkNoMVarNoFVar env' v.name v.value
       M.run env' (safety := .unsafe) (lctx := {}) (lparams := v.levelParams) (fuel := fuel) do
         let valType ← TypeChecker.checkType v.value
         if !(← isDefEq valType v.type) then
           throw <| .declTypeMismatch env' (.defnDecl v) valType
-    return env'
-  else
-    if check then
-      M.run env (safety := .safe) (lctx := {}) (lparams := v.levelParams) (fuel := fuel) do
-        checkConstantVal env v.toConstantVal (← checkPrimitiveDef v)
-        let valType ← TypeChecker.checkType v.value
-        if !(← isDefEq valType v.type) then
-          throw <| .declTypeMismatch env (.defnDecl v) valType
-    return env.add (.defnInfo v)
+  else if check then
+    M.run env (safety := .safe) (lctx := {}) (lparams := v.levelParams) (fuel := fuel) do
+      checkConstantVal env v.toConstantVal (← checkPrimitiveDef v)
+      checkNoMVarNoFVar env v.name v.value
+      let valType ← TypeChecker.checkType v.value
+      if !(← isDefEq valType v.type) then
+        throw <| .declTypeMismatch env (.defnDecl v) valType
+  return env.add (.defnInfo v)
 
 def addTheorem (env : Environment) (v : TheoremVal) (check := true) (fuel : FuelConfig := {}) :
     Except Exception Environment := do
@@ -56,6 +55,7 @@ def addTheorem (env : Environment) (v : TheoremVal) (check := true) (fuel : Fuel
       checkConstantVal env v.toConstantVal
       if !(← isProp v.type) then
         throw <| .thmTypeIsNotProp env v.name v.type
+      checkNoMVarNoFVar env v.name v.value
       let valType ← TypeChecker.checkType v.value
       if !(← isDefEq valType v.type) then
         throw <| .declTypeMismatch env (.thmDecl v) valType
@@ -66,6 +66,7 @@ def addOpaque (env : Environment) (v : OpaqueVal) (check := true) (fuel : FuelCo
   if check then
     M.run env (safety := .safe) (lctx := {}) (lparams := v.levelParams) (fuel := fuel) do
       checkConstantVal env v.toConstantVal
+      checkNoMVarNoFVar env v.name v.value
       let valType ← TypeChecker.checkType v.value
       if !(← isDefEq valType v.type) then
         throw <| .declTypeMismatch env (.opaqueDecl v) valType
@@ -78,22 +79,30 @@ def addMutual (env : Environment) (vs : List DefinitionVal)
     throw <| .other "invalid mutual definition, declaration is not tagged as unsafe/partial"
   if check then
     M.run env (safety := v₀.safety) (lctx := {}) (lparams := v₀.levelParams) (fuel := fuel) do
+      let mut found : NameSet := {}
       for v in vs do
         if v.safety != v₀.safety then
           throw <| .other
             "invalid mutual definition, declarations must have the same safety annotation"
+        -- The whole block is checked under one set of level parameters, so they must agree;
+        -- lean4#14608 adds the same check to the C++ kernel.
+        if v.levelParams != v₀.levelParams then
+          throw <| .other
+            "invalid mutual definition, declarations must have the same universe level parameters"
+        if found.contains v.name then
+          throw <| .other s!"invalid mutual definition, duplicate declaration name '{v.name}'"
+        found := found.insert v.name
         checkConstantVal env v.toConstantVal
-  let mut env' := env
-  for v in vs do
-    env' := env'.add (.defnInfo v)
+  let env' := vs.foldl (init := env) fun env' v =>
+    env'.add (.axiomInfo { v with isUnsafe := v₀.safety == .unsafe })
   if check then
     M.run env' (safety := v₀.safety) (lctx := {}) (lparams := v₀.levelParams) (fuel := fuel) do
       for v in vs do
         checkNoMVarNoFVar env' v.name v.value
         let valType ← TypeChecker.checkType v.value
         if !(← isDefEq valType v.type) then
           throw <| .declTypeMismatch env' (.mutualDefnDecl vs) valType
-  return env'
+  return vs.foldl (fun env' v => env'.add (.defnInfo v)) env
 
 /-- Type check given declaration and add it to the environment -/
 def addDecl (env : Environment) (decl : Declaration) (check := true) (fuel : FuelConfig := {}) :

Lean4Lean/Environment/Basic.lean

@@ -51,6 +51,62 @@ def isNonRecStructure (env : Environment) (constName : Name) : Bool :=
   | some (.inductInfo { isRec := false, ctors := [_], numIndices := 0, .. }) => true
   | _ => false
 
+/-- A one-constructor, unindexed structure whose constructor and generated
+recursor have both reached the host environment.  Family metadata is staged
+before either artifact is inserted; projection verification may only demand a
+registered Theory view at this later boundary.
+
+Unlike `isNonRecStructure`, projection readiness deliberately does not inspect
+`InductiveVal.isRec`: Lean emits primitive projections for recursive structures
+too (including nested-recursive structures in the Lean prelude). -/
+def isProjectionReadyStructure (env : Environment) (constName : Name) : Bool :=
+  match env.constants.find?' constName with
+  | some (.inductInfo { ctors := [ctor], numIndices := 0, .. }) =>
+    match env.constants.find?' ctor,
+        env.constants.find?' (mkRecName constName) with
+    | some (.ctorInfo _), some (.recInfo _) => true
+    | _, _ => false
+  | _ => false
+
+theorem isProjectionReadyStructure_false_of_no_ctorInfo
+    {env : Environment} {name : Name} {info : InductiveVal}
+    (hfind : env.constants.find?' name = some (.inductInfo info))
+    (hnoCtor : ∀ ctor ctorInfo,
+      env.constants.find?' ctor ≠ some (.ctorInfo ctorInfo)) :
+    env.isProjectionReadyStructure name = false := by
+  cases info
+  rename_i constant numParams numIndices all ctors numNested isRec isUnsafe isReflexive
+  cases constant
+  unfold isProjectionReadyStructure
+  rw [hfind]
+  cases numIndices with
+  | succ _ => rfl
+  | zero =>
+    cases ctors with
+    | nil => rfl
+    | cons ctor rest =>
+      cases rest with
+      | cons _ _ => rfl
+      | nil =>
+        cases hctor : env.constants.find?' ctor with
+        | none => simp [hctor]
+        | some info =>
+          cases info <;> simp_all
+
+theorem isProjectionReadyStructure_false_of_numIndices_ne
+    {env : Environment} {name : Name} {info : InductiveVal}
+    (hfind : env.constants.find?' name = some (.inductInfo info))
+    (hindices : info.numIndices ≠ 0) :
+    env.isProjectionReadyStructure name = false := by
+  cases info
+  simp_all [isProjectionReadyStructure]
+
+theorem isProjectionReadyStructure_false_of_not_found
+    {env : Environment} {name : Name}
+    (hfind : env.constants.find?' name = none) :
+    env.isProjectionReadyStructure name = false := by
+  simp [isProjectionReadyStructure, hfind]
+
 def checkName (env : Environment) (n : Name)
     (allowPrimitive := false) : Except Exception Unit := do
   if env.contains n then

Lean4Lean/Experimental/DomainTheory.lean

@@ -41,7 +41,7 @@ inductive FinElem where
   | bot
   | val : SExprF FinElem (FinFun FinElem FinElem) → FinElem
 
-def DomN : Nat → Type
+@[implicit_reducible] def DomN : Nat → Type
   | 0 => Unit
   | n+1 => Option (SExprF (DomN n) (DomN n → DomN n))
 
@@ -176,7 +176,7 @@ theorem DomN.cast_eq (x : DomN (a + 1)) :
       simp [SExprF.map_comp]; congr 1 <;> ext t <;> simp [this]
       congr 2; exact DomN.cast_upN (k := 1) _ (Nat.le_add_right ..)
 
-def Dom : Type := { f : ∀ n, DomN n // ∀ n, f n = (f (n + 1)).down }
+@[implicit_reducible] def Dom : Type := { f : ∀ n, DomN n // ∀ n, f n = (f (n + 1)).down }
 
 def Dom.bot : Dom := ⟨fun | 0 => () | _+1 => none, fun | 0 | _+1 => rfl⟩
 

Lean4Lean/Experimental/MoreStepIndexed.lean

@@ -66,7 +66,7 @@ inductive ShapeS (Shape : Type) (n : Nat) : Type where
   | forallE : Shape → List (Shape × Shape) → ShapeS Shape n
   | lam : List (Shape × Shape) → ShapeS Shape n
 
-def Shape : Nat → Type
+@[implicit_reducible] def Shape : Nat → Type
   | 0 => Unit -- bottom
   | n + 1 => ShapeS (Shape n) n