proofs(lean4): mechanize the L1/L2 core (MECH-1 totality+stability, MECH-2 complete) with hard gates - #17
Merged
Merged
Conversation
…ade algebras, hard gates
MECH-2 (complete): GradeAlgebra as the ET-4 ordered-semiring law set
(16 laws as proof fields) with instances Affine {0,1,w}, tropical Cost
(min/+), the generic bounded-distributive-lattice theorem instantiated
at Level (Low<=High), and the componentwise product R x S (ET-5:
composite disciplines are composition of algebras, proven once).
MECH-1 (totality core + stability): intrinsically-kinded type-level
STLC with the Keller-Altenkirch rem/wkv/eqv toolkit; beta-normal forms
with LEFT-NESTED spines (append is cons, the spine fold is structural);
hereditary substitution + normalizer total by a (kindSize, tag, size)
lexicographic measure — the Totality Gate (ET-1) discharged by
construction. DefEq stated; stability nf_emb : nf (embNf n) = n proven.
Soundness/completeness (defEq_iff_nf, decDefEq) recorded OPEN in
PROOF-STATUS — stated, never stubbed.
Gates (wire-first, watched to fail before trusted):
- scripts/check-proofs.sh: MANIFEST-driven; absent prover = FAIL;
per-module lake build; whole-package build; mandatory axiom audit
pinned to Lean's three-axiom trusted base (a smuggled user axiom
fails the gate even though it compiles green).
- scripts/scan-dangerous.sh: comment-aware scan incl. axiom/admit/
native_decide; FIXED Lean block-comment stripping ({- -} -> /- -/).
- scripts/check-proof-status.sh: drift gate — PROOF-STATUS.adoc must
match MANIFEST ground truth or CI fails.
- .github/workflows/proofs.yml: sha-pinned actions, elan 4.2.3 from a
checksum-verified release tarball, toolchain from lean-toolchain,
cache keyed on the toolchain pin. No floating setup actions.
All 11 modules gated; audit 12/12 within the trusted base; zero sorry,
zero user axioms. Verified failure modes: broken proof, smuggled axiom,
absent prover, unlisted file, status drift.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
|
hyperpolymath
added a commit
that referenced
this pull request
Jul 21, 2026
…h (PR-6, closes the sequence) (#21) Final PR of the completion sequence (#11 → #12 → #13 → #15 → #16 → #17 → this). - **STATE.a2ml** — completion 15→32 with per-phase justification comments; blockers echo #18/#19 + the anytype audit trail (anytype #13–#19, PR #20). - **AFFIRMATION.adoc** — anchor filled (main @ `a11c9877`, 2026-07-21T14:43Z, Lean 4.32.0/elan 4.2.3) in the same session that re-ran every check listed; every "affirmed-ran" row corresponds to a command actually executed. NOT-claims list keeps ET-2 closure, ET-6..9, ET-10..13, ET-14 explicitly open. - **Justfile** — `test`/`lint`/`fmt-check` were template echo-stubs (fake green). Now: `test` = proof gate + drift gate; `lint` = dangerous-construct scan, md-in-docs, root-shape, template validation; `fmt-check` honestly reports that nothing is checked. `check-no-vlang.sh` deferred to #19 (tracked, not silently skipped). `.machine_readable/root-allow.txt` updated for root entries landed by #14/#17. - **README** — badge `theory_(no_proofs_yet)` → `theory_(L2_proven, L1_core_proven, rest_OPEN)`; Status section states precisely what is machine-checked vs open. Verification (all run in this session at the anchor SHA): `./scripts/check-proofs.sh lean4` PASS (audit 12/12); `./scripts/scan-dangerous.sh` PASS; `./scripts/check-proof-status.sh` PASS; `./scripts/validate-template.sh` PASS (4 warnings); `just test && just quality` PASS end-to-end. 🤖 Generated with [Claude Code](https://claude.com/claude-code)
hyperpolymath
added a commit
that referenced
this pull request
Jul 27, 2026
Brings the branch up to date with main (was 14 behind) so the ET-2 proof can be promoted to main with a green check roster. Five conflicts, all resolved by inspection rather than a blanket --ours/--theirs. Four were add/add artefacts of main having received a SQUASHED copy of this branch via PR #17, which makes git see both sides as independent additions: MANIFEST, Systemet.lean, Systemet/Audit.lean Verified main's content is byte-identical to the branch's and the branch is a strict superset (adds exactly the four ET-2 entries/imports/audit lines). Took the branch side. docs/status/PROOF-STATUS.adoc Every difference is this branch's ET-2 update (gated 11 -> 15, ET-2 row proven, MECH-1 row landed, stale "ET-2 (finish)" OPEN row dropped); main carried no independent edits. Took the branch side. .github/workflows/proofs.yml Genuine two-sided merge -- the two sides differ in OPPOSITE directions: main has actions/checkout@3d3c42e (v7.0.1, from dependabot #26) branch has curl --proto '=https' --tlsv1.2 (Sonar S6506 fix, 1f2a81a) Took main's newer pin and re-applied the branch's https hardening on top, so neither is regressed. Both verified present after resolution. Verified on the merged tree (measured, not assumed): cold rebuild (rm -rf .lake/build) Build completed successfully (16 jobs) scripts/check-proofs.sh lean4 PASS, real exit 0 audit 20/20 in the trusted base scripts/scan-dangerous.sh PASS, real exit 0 scripts/check-proof-status.sh PASS, real exit 0 (15 gated, doc agrees) forbidden-token scan on the four new proof files: clean Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
hyperpolymath
added a commit
that referenced
this pull request
Jul 27, 2026
Promotes the **ET-2 closure** (decidability of L1 conversion) onto `main`. ## Why this PR exists ET-2 was proven and merged in **PR #24** — but into `proofs/lean4-l1-l2`, **not `main`**. PR #17 had squash-merged that branch to `main` *before* ET-2 existed, so `main` holds the L1/L2 mechanization content while the ET-2 work sits only on the branch. No second PR to `main` was ever opened. Measured before this PR: `main...proofs/lean4-l1-l2` was **diverged, 4 ahead / 14 behind**, and all four ET-2 proof files returned **404 on `main`**. Anything reading `main` today correctly concludes ET-2 is still open. ## What lands on `main` | File | Contents | |---|---| | `Systemet/L1/SubstLemmas.lean` | substitution/weakening exchange family, incl. `nf_substTy` — normalization commutes with hereditary substitution (the whole content of the β case) | | `Systemet/L1/Soundness.lean` | `soundness : DefEq t (embNf (nf t))` | | `Systemet/L1/Completeness.lean` | `completeness : DefEq t u → nf t = nf u`; `defEq_iff_nf : DefEq t u ↔ nf t = nf u` | | `Systemet/L1/Decidable.lean` | `decEqNf` / `decEqSp` (hand-rolled mutual `DecidableEq` — `deriving` does not work across the `Nf`/`Sp` pair); `decDefEq : (t u : Ty Γ k) → Decidable (DefEq t u)` | Plus the `PROOF-STATUS.adoc` truth pass (`gated` 11 → 15, ET-2 row proven, MECH-1 row landed, the satisfied `ET-2 (finish)` OPEN row removed) and append-only `MANIFEST` / `Systemet.lean` / `Audit.lean` entries. ## Conflict resolution — read this bit The pre-PR sync merge (`0104c9c`) hit five conflicts. **Four were `add/add` artefacts of the squash in #17**, which makes git treat both sides as independent additions. None were resolved by a blanket `--ours`/`--theirs`: - `MANIFEST`, `Systemet.lean`, `Audit.lean` — verified `main`'s content is **byte-identical** to the branch's and the branch is a **strict superset** (adds exactly the four ET-2 entries). Branch side taken. - `PROOF-STATUS.adoc` — every difference is this branch's ET-2 update; `main` carried no independent edits. Branch side taken. - **`.github/workflows/proofs.yml` — a genuine two-sided merge.** The sides differed in *opposite* directions: `main` had the newer `actions/checkout@3d3c42e` (v7.0.1, from dependabot #26) while the branch had `curl --proto '=https' --tlsv1.2` (the Sonar S6506 fix). Took main's newer pin **and** re-applied the branch's https hardening, so neither is regressed. Both confirmed present post-resolution. ## Evidence (measured on the merged tree, not inherited from #24) - Cold rebuild after `rm -rf .lake/build` → **Build completed successfully (16 jobs)** - `scripts/check-proofs.sh lean4` → **PASS** (real exit 0); audit reports **20/20 headline items within the trusted base** - `scripts/scan-dangerous.sh` → **PASS** (real exit 0) - `scripts/check-proof-status.sh` → **PASS** (real exit 0) — 15 gated, document agrees - Forbidden-token scan on the four new proof files → clean - `#print axioms` on `soundness`, `completeness`, `defEq_iff_nf`, `decDefEq`, `decEqNf`, `decEqSp`, `nf_substTy` → **`[propext, Quot.sound]` only**; no `sorryAx`, no user axioms, not even `Classical.choice` Real exit codes were checked directly — piping a gate through `tail` and reading `$?` reports *tail's* status, which is how a red gate can look green. ## Scope — what this does *not* claim `DefEq` here is **β + equivalence + congruence. η is not included** and remains an OPEN row. **ET-3 is unaffected** — its η and model directions stay open. `PROOF-STATUS.adoc` marks ET-2 proven *for the L1 core calculus*, under the core-vs-full-theory caveat that file already carries. **ET-14 (TEA erasure) is untouched and remains the headline open problem**, gated on the owner's ET-16 / L0-lowering ADR. ## Merge notes Per the base ruleset, **squash is the only merge that works** here (rebase merges cannot be signed by GitHub bots), and the phantom required `Dependabot` context means this will need `--admin`. Not merged by me — that call is yours. 🤖 Generated with [Claude Code](https://claude.com/claude-code)
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
1 participant
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.
PR-5 of the completion sequence (#11 → #12 → #13 → #15 → #16 → this).
What is proven (all under Lean 4.32.0, hermetic, no mathlib, no
sorry, no user axioms)MECH-2 — complete.
Systemet.L2.GradeAlgebrais the precise ET-4 statement: an ordered-semiring law set whose 16 fields are the proof obligations. Instances:Affine{0,1,ω}, tropicalCost(min/+, ∞ identity), the generic theorem that every bounded distributive lattice is a grade algebra (instantiated atLevel= Low≤High), and the componentwise productR × S— ET-5's "same rules, different algebra", proven once.MECH-1 — totality core + stability. Intrinsically-kinded type-level STLC (Keller–Altenkirch toolkit); β-normal forms with left-nested spines; hereditary substitution and the normalizer are total by a
(kindSize, tag, size)lexicographic measure — the Totality Gate (ET-1) discharged by construction.DefEqstated; stabilitynf_emb : nf (embNf n) = nproven. Soundness/completeness (defEq_iff_nf,decDefEq) are OPEN, stated inConversion.lean's docstring and PROOF-STATUS — never stubbed.Gates (wire-first; every one watched to fail before its green was trusted)
check-proofs.sh lean4— MANIFEST-driven, absent prover = FAIL, per-module + package buildSystemet/Audit.lean, 12#print axioms) pinned to the three-axiom trusted baseaxiom cheat : Falsecompiles green and still fails the gate, named in outputscan-dangerous.sh(comment-aware; incl.axiom/admit/native_decide){- -}→/- -/) — was false-positive-prone; canary-tested both directionscheck-proof-status.sh— PROOF-STATUS.adoc must match MANIFEST countsCI (
proofs.yml): sha-pinnedactions/checkout+actions/cache, elan 4.2.3 from a checksum-verified release tarball, toolchain from the committedlean-toolchain, cache keyed on that pin. Note: the sha9c091bb2…used across this repo's workflows is actually v7.0.0 (some existing comments mislabel it v6.0.1).Honesty ledger
lake buildclean, audit 12/12, drift gate PASS.🤖 Generated with Claude Code