WIP: Jcb/formalization2

.github/workflows/zulip_emoji_reconcile.yml

@@ -0,0 +1,90 @@
+name: Zulip emoji reconcile
+
+on:
+  schedule:
+    - cron: "37 * * * *"   # hourly sweep: the self-healing safety net
+  workflow_dispatch:
+    inputs:
+      pr:
+        description: "PR number(s), space-separated; leave empty to sweep recent messages"
+        required: false
+        default: ""
+      dry-run:
+        description: "Log planned reaction changes without writing to Zulip"
+        type: boolean
+        default: false
+  pull_request_target:      # close/merge/reopen changes, within seconds
+    types: [closed, reopened]
+  workflow_run:             # CI start/finish, so the CI emoji updates promptly
+    workflows: ["CI"]
+    types: [requested, completed]
+
+concurrency:
+  # Serialize runs: the reconciler reads live PR state and then writes
+  # reactions, so two interleaved runs could re-assert stale state. GitHub
+  # keeps only the newest queued run per group (earlier pending runs are
+  # canceled), which suits a level-triggered tool — the last run recomputes
+  # everything from live state and converges to the final answer.
+  group: ${{ github.workflow }}
+  cancel-in-progress: false
+
+permissions:
+  contents: read
+  pull-requests: read
+
+jobs:
+  reconcile:
+    runs-on: ubuntu-latest
+    if: github.repository == 'digama0/lean4lean'   # skip runs on forks
+    steps:
+      # On pull_request_target / workflow_run this checks out the *default*
+      # branch, so the config (and everything else that runs in this job) is
+      # never PR-controlled.
+      - name: Check out this repo's config
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+        with:
+          sparse-checkout: .github/zulip-emoji-config.json
+          sparse-checkout-cone-mode: false
+
+      - name: Determine PR number(s)
+        id: target
+        env:
+          GH_TOKEN: ${{ github.token }}
+          EVENT: ${{ github.event_name }}
+          INPUT_PR: ${{ inputs.pr }}
+          EVENT_PR: ${{ github.event.pull_request.number }}
+          HEAD_SHA: ${{ github.event.workflow_run.head_sha }}
+        run: |
+          set -euo pipefail
+          case "$EVENT" in
+            workflow_dispatch) pr="$INPUT_PR" ;;
+            pull_request_target) pr="$EVENT_PR" ;;
+            workflow_run)
+              # PR(s) at the CI run's head commit (works for fork PRs too).
+              pr=$(gh api "repos/${GITHUB_REPOSITORY}/commits/${HEAD_SHA}/pulls" \
+                     --jq 'map(.number) | join(" ")')
+              ;;
+            *) pr="" ;;  # schedule -> sweep
+          esac
+          echo "pr=${pr}" >> "$GITHUB_OUTPUT"
+
+      - name: Reconcile
+        # Skip only a workflow_run whose head commit no longer maps to a PR;
+        # schedule and PR-less dispatches sweep instead.
+        if: steps.target.outputs.pr != '' || github.event_name == 'schedule' || github.event_name == 'workflow_dispatch'
+        uses: leanprover-community/mathlib-ci/.github/actions/zulip-emoji-reconcile@5668fbbccf0fecefdfcddf539b8406db197dfc59
+        with:
+          config: .github/zulip-emoji-config.json
+          pr: ${{ steps.target.outputs.pr }}
+          sweep: ${{ !steps.target.outputs.pr }}
+          dry-run: ${{ inputs.dry-run == true }}
+          zulip-api-key: ${{ secrets.ZULIP_API_KEY }}
+          github-token: ${{ github.token }}
+
+  workflow-keepalive:
+    if: github.repository == 'digama0/lean4lean' && github.event_name == 'schedule'
+    runs-on: ubuntu-latest
+    permissions:
+      actions: write
+    steps:
+      - uses: liskin/gh-workflow-keepalive@f72ff1a1336129f29bf0166c0fd0ca6cf1bcb38c # v1.2.1

.github/zulip-emoji-config.json

@@ -0,0 +1,23 @@
+{
+  "_comment": "Reconcile config for digama0/lean4lean: open/closed/merged plus CI status, using standard unicode emoji. See docs/zulip-emoji-quickstart.md in leanprover-community/mathlib-ci for setup, and docs/zulip-emoji-reconcile.md there for the full schema.",
+
+  "github_repo": "digama0/lean4lean",
+
+  "zulip": {
+    "site": "https://leanprover.zulipchat.com",
+    "email": "leanprover-community-repo-update-bot@leanprover.zulipchat.com"
+  },
+
+  "channels": {
+    "pr_reviews": "lean4lean"
+  },
+
+  "states": [
+    {"name": "merged", "group": "pr", "priority": 30, "source": {"state": "merged"}, "emoji": "merge"},
+    {"name": "closed", "group": "pr", "priority": 20, "source": {"state": "closed"}, "emoji": "closed-pr", "emoji_code": "61293", "reaction_type": "realm_emoji"},
+
+    {"name": "ci-running", "group": "ci", "source": {"ci": "running"}, "emoji": "yellow"},
+    {"name": "ci-success", "group": "ci", "source": {"ci": "success"}, "emoji": "check"},
+    {"name": "ci-failure", "group": "ci", "source": {"ci": "failure"}, "emoji": "cross_mark"}
+  ]
+}

.gitignore

@@ -4,3 +4,4 @@
 # Keep scratch plans local while versioning the authoritative execution ladder.
 /plans/*
 !/plans/roadmap.md
+!/plans/l4l-15-structure-eta-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⟩