feat: verify primitive-model conservation through declaration checking

[kim-em]

This PR adds an end-to-end addDecl.WF theorem showing that successful declaration checking preserves a verified environment for the currently modeled fragment. It replaces ad hoc recognition of non-structural Nat primitives with checked reduction certificates, proves conservation of VEnv.HasPrimitives, and rebuilds the declaration-level verification around those results. The diff contains 24,247 insertions and 1,264 deletions across 33 files.

The final theorem is deliberately restricted by Declaration.SupportedByModel:

def Declaration.SupportedByModel : Declaration → Prop
  | .inductDecl .. => False
  | .mutualDefnDecl vs => (vs.map (fun v => v.name)).Nodup
  | _ => True

Inductive declarations are therefore out of scope entirely. For mutual definitions, addMutual.WF takes name uniqueness as a hypothesis. Master derived that fact from the executable name checker; this branch still rejects duplicate names, but its proof interface no longer derives the fact from that check.

This does not mean that the kernel is verified. The branch removes one admitted proof and adds none, but addDecl.WF still depends on sorryAx through admitted lemmas elsewhere in Lean4Lean/Verify/ that are already present on master. #print axioms Lean4Lean.addDecl.WF reports 34 dependencies, including sorryAx and two bv_decide axioms originating in Lean4Lean/Verify/Expr.lean, with no native_decide axiom.

The executable certificate checker narrows the alternative preludes that lean4lean accepts. The Nat.gcd and Nat.bitwise certificates require their two-Nat well-founded state to use PSigma.mk. Execution with Lean 4.33.0-rc2 confirms that the shipped Nat.gcd uses that representation, so the shipped prelude is unaffected. Ordinary user declarations cannot reach this difference because checkPrimitiveDefCore dispatches on the reserved declaration names Nat.gcd and Nat.bitwise. An alternative prelude can reach it by defining one of those constants through a one-argument well-founded helper over another state type such as Nat × Nat. doc/wf-certificate-design.md describes the comparison and proposes the corresponding divergences.md entry.

Review the change top-down in this order:

1. Read Lean4Lean/Primitive.lean first. Commit 2fc4f84 changes that file by 1,223 insertions and 127 deletions and contains the executable acceptance delta: the generic well-founded reduction record, the GCD and bitwise specializations, and the closed equations for the fuel-based mod and div helpers.
2. Read the bottom of Lean4Lean/Verify/Environment.lean next, especially Declaration.SupportedByModel, addMutual.WF, and addDecl.WF, to see the final claim and every additional hypothesis.
3. Follow Nat.gcd end to end through NatGcdFixCertificate, checkNatGcdFixCertificate.WF, NatGcdFixCertificate.NormalizedValid.reflects, and the GCD branch of primitive conservation. This is the representative well-founded case.
4. Read the shared translation, type-checker, condition-reflection, and mod/div infrastructure. Commit 27304be adds 9,808 lines across the nine reflection-toolbox files.
5. Read the remaining primitive cases in Lean4Lean/Verify/Primitive.lean. Commit b2d9169 adds 8,957 lines covering the per-primitive conservation development; the bitwise proof is the largest specialization, while the direct-equation primitives follow the same checker-to-model pattern.

Validation on the exact pushed tree succeeds with:

• lake build: 161 jobs
• lake build Lean4Lean.Experimental: 68 jobs
• lake build Lean4Lean.Tests: 63 jobs
• lake exe lean4lean Init.Core: 1,035 declarations checked
• lake exe lean4lean --fresh Init.Core: 3,953 declarations checked

All commands exit successfully.

🤖 Prepared with Claude Code