chore: purge template residue (ABI seam out, status files localized, IS-NOT enforced)#16
Merged
Merged
Conversation
… stubs, localize status files systemet's IS-NOT says no runnable code lives here; the kernel is anytype. Accordingly: - Remove src/ (Idris2 ABI stubs + Zig FFI template), root abi.ipkg, and docs/developer/ABI-FFI-README.adoc. Git history is the quarantine. - Remove the five generic template proof stubs (idris2 Types.idr + ABI/, lean4 ApiTypes.lean, agda, coq, tlaplus) — several were quarantined as broken in the template's own manifests and none proved systemet. verification/proofs/README.adoc now describes the MANIFEST-gated Lean4 development the mechanization PR targets. - validate-template.sh: the ABI/FFI checks are INVERTED — absence of src/ and abi.ipkg is now enforced (IS-NOT check); build-verification phase defers to the forthcoming scripts/check-proofs.sh; SPDX scan repointed at scripts/ + verification/. - docs/status rewritten for systemet: ROADMAP (real milestones M1-M4), PROOF-NEEDS (tier T1, master list = the ET ledger by reference, ABI category retired), PROOF-STATUS (ET rows, MECH-1/MECH-2 slots, honest "0% proven"), TEST-NEEDS (the actual verifiable surfaces), READINESS (grade X→E with real scan values, dated 2026-07-21, pending owner countersign). - root-allow.txt: src/ + abi.ipkg entries removed (src/ now a documented refusal); .gitignore ttc comment updated; eclexiaiser config drops the two functions that pointed into src/. AFFIRMATION.adoc anchor fields are deliberately untouched — they are filled at signing time in the final anchor PR. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
|
hyperpolymath
added a commit
that referenced
this pull request
Jul 21, 2026
…ECH-2 complete) with hard gates (#17) 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.GradeAlgebra` is the precise ET-4 statement: an ordered-semiring law set whose 16 fields *are* the proof obligations. Instances: `Affine` {0,1,ω}, tropical `Cost` (min/+, ∞ identity), the **generic theorem** that every bounded distributive lattice is a grade algebra (instantiated at `Level` = Low≤High), and the componentwise product `R × 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. `DefEq` stated; stability `nf_emb : nf (embNf n) = n` proven. Soundness/completeness (`defEq_iff_nf`, `decDefEq`) are **OPEN**, stated in `Conversion.lean`'s docstring and PROOF-STATUS — never stubbed. ## Gates (wire-first; every one watched to fail before its green was trusted) | Gate | Verified failure mode | |---|---| | `check-proofs.sh lean4` — MANIFEST-driven, absent prover = FAIL, per-module + package build | broken proof → FAIL; prover off PATH → FAIL; unlisted file on disk → FAIL | | mandatory axiom audit (`Systemet/Audit.lean`, 12 `#print axioms`) pinned to the three-axiom trusted base | a smuggled `axiom cheat : False` **compiles green and still fails the gate**, named in output | | `scan-dangerous.sh` (comment-aware; incl. `axiom`/`admit`/`native_decide`) | fixed Lean block-comment stripping (`{- -}` → `/- -/`) — was false-positive-prone; canary-tested both directions | | `check-proof-status.sh` — PROOF-STATUS.adoc must match MANIFEST counts | doctored count → FAIL | CI (`proofs.yml`): sha-pinned `actions/checkout` + `actions/cache`, elan 4.2.3 from a checksum-verified release tarball, toolchain from the committed `lean-toolchain`, cache keyed on that pin. Note: the sha `9c091bb2…` used across this repo's workflows is actually **v7.0.0** (some existing comments mislabel it v6.0.1). ## Honesty ledger - ET-1 ✓ (for the mechanized calculus) · ET-4 ✓ · ET-5 ✓ · ET-2 partial (stability only) · ET-14 and everything else remain OPEN, listed in PROOF-STATUS. - Local run: 11/11 modules PASS, coverage clean, `lake build` clean, audit 12/12, drift gate PASS. 🤖 Generated with [Claude Code](https://claude.com/claude-code) 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)
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.
Summary
PR-4 of the completion sequence (after #11, #12, #13, #15). systemet's IS-NOT says no runnable code lives here — this PR makes the repo match:
src/+abi.ipkg+ ABI-FFI doc removed (git history is the quarantine).validate-template.shnow enforces their absence — the ABI checks are inverted into IS-NOT checks, and it requiresdocs/theory/OBLIGATIONS.adocinstead.ApiTypes.leanthat never compiled, agda/coq/tlaplus placeholders).verification/proofs/README.adocnow specifies the MANIFEST-gated Lean4 layout the mechanization PR fills.docs/status/localized to systemet: ROADMAP (M1–M4 real milestones), PROOF-NEEDS (tier T1; master list = the ET ledger by reference; ABI category retired), PROOF-STATUS (ET obligation rows + MECH-1/MECH-2 slots; honest 0% proven), TEST-NEEDS (actual verifiable surfaces), READINESS (X→E, real scan values, pending owner countersign).AFFIRMATION anchor fields intentionally untouched — filled at signing time in the final anchor PR.
Verification
bash -n scripts/validate-template.shclean; Phase 4 requirements (docs/theory present, src/ absent) hold on post-docs(theory): formal spec per layer/gate + citable ET-1..ET-15 obligation ledger #15 main.grep -rn "sorry|believe_me|Admitted|assert_total"over proof files: none exist (prose lists only).🤖 Generated with Claude Code