hyperpolymath · hyperpolymath · Jul 21, 2026 · Jul 21, 2026
@@ -6,37 +6,54 @@
 [metadata]
 project = "systemet"
 version = "0.1.0"
-last-updated = "2026-06-28"
+last-updated = "2026-07-21"
 status = "active"  # active | paused | archived
 
 [project-context]
 name = "systemet"
 purpose = "Equality Theory — the stratified type theory (L1 equality-is-conversion cut, three refusal gates, roles-as-tropes, TEA-erasure obligation) that the anytype kernel implements."
-completion-percentage = 15
+# 32, not higher: the spec + ledger + L2 mechanization + L1 totality core are
+# real, but MECH-1 milestone 2 (soundness/completeness/decDefEq), the gates
+# beyond L2, tropes, and TEA (ET-14) are all open. See docs/status/PROOF-STATUS.adoc.
+completion-percentage = 32
 
 [position]
-phase = "design"           # design | implementation | testing | maintenance | archived
+phase = "implementation"   # design | implementation | testing | maintenance | archived
 maturity = "experimental"  # experimental | alpha | beta | production | lts
 
 [route-to-mvp]
 milestones = [
   { name = "Phase 0: Split theory out of the EveryType draft; instantiate RSR repo", completion = 100 },
-  { name = "Phase 1: Specify the five layers and the three gates in prose", completion = 90 },
-  { name = "Phase 2: Formal spec of L1 (equality = conversion) + totality obligation", completion = 0 },
-  { name = "Phase 3: L2 grade-algebra laws stated precisely enough to check a candidate", completion = 0 },
-  { name = "Phase 4: Trope-preservation statement and per-API obligations", completion = 0 },
+  { name = "Phase 1: Specify the five layers and the three gates in prose", completion = 95 },
+  { name = "Phase 2: Formal spec of L1 (equality = conversion) + totality obligation", completion = 65 },
+  { name = "Phase 3: L2 grade-algebra laws stated precisely enough to check a candidate", completion = 100 },
+  { name = "Phase 4: Trope-preservation statement and per-API obligations", completion = 35 },
   { name = "Phase 5 (OPEN-A): Formal TEA-erasure proof", completion = 0 },
 ]
+# Phase 1 at 95: L3 guarded recursion is sketched, not fully specified (docs/theory/06).
+# Phase 2 at 65: spec written (docs/theory/02 + OBLIGATIONS ET-1..3); mechanized in Lean 4
+#   (verification/proofs/lean4/Systemet/L1/): hereditary substitution + normalizer total
+#   (ET-1 discharged for the core calculus), stability nf_emb proven; soundness/
+#   completeness/decDefEq remain (MECH-1 milestone 2).
+# Phase 3 at 100: GradeAlgebra law set (ET-4) + Affine/Cost/Lattice(Level)/Product
+#   instances (ET-5) proven in Lean 4, gated in CI (proofs.yml).
+# Phase 4 at 35: statement + worked file-handle machine specified (docs/theory/07);
+#   no per-API instances, no mechanization.
 
 [blockers-and-issues]
-# No external blockers. Proofs are unstarted, not blocked.
+issues = [
+  { id = 18, title = "descriptiles/6a2 migration (blocked: contractiles.mjs needs Node, estate-denied here)" },
+  { id = 19, title = "wire check-no-vlang.sh into lint after clearing template zig residue (owner: confirm the script's premise vs Zig-first directive)" },
+]
+# Downstream tracking: anytype issues #13-#19 (ET-obligation audit, 2026-07-21) +
+# anytype PR #20 echoing them; anytype #13 = refresh its systemet pin past the ET ledger.
 
 [critical-next-actions]
 actions = [
-  "Write a precise L1 specification (conversion-as-equality) and name the totality assumption.",
-  "State the L2 grade-algebra laws (semiring + ordering) a candidate grade must satisfy.",
-  "Formalise the trope-preservation obligation; pick one real API as a worked finite machine.",
-  "Keep README/EXPLAINME claims inside what is proven; TEA-erasure stays 'OPEN' until proved.",
+  "MECH-1 milestone 2: soundness (DefEq t (embNf (nf t))), completeness (DefEq t u -> nf t = nf u), decidable Nf equality => defEq_iff_nf + decDefEq (closes ET-2 for the core calculus).",
+  "Then eta-laws (ET-1..3 eta extension), then Structural Gate soundness statement (ET-6/7).",
+  "Keep README/EXPLAINME claims inside what is proven; TEA-erasure (ET-14) stays OPEN until proved.",
+  "One worked per-API trope instance (ET-12/13) after the gate work.",
 ]
 
 [maintenance-status]

@@ -68,3 +68,11 @@ container/                 # may host Containerfile if not at build/
 .pre-commit-config.yaml    # TODO: relocate to ci/.pre-commit-config.yaml after invocation pattern decided
 affinescript/              # AffineScript source subtree consumed by this template
 tools/                     # TODO: consolidate with scripts/ or document the split (pending decision)
+
+# ─── Landed by merged PRs #14 (governance sweep) and #17 (mechanization) ─────
+build/                     # just modules for the proof gates (build/just/proofs.just)
+flake.nix                  # standards#505 packaging (conflicts with Guix-only CI gate — tracked repo-wide)
+ARCHITECTURE.md            # standards#505 governance sweep (PR #14)
+GOVERNANCE.md              # standards#505 governance sweep (PR #14)
+MAINTAINERS                # standards#505 governance sweep (PR #14)
+mise.toml                  # toolchain pinning from the governance sweep (PR #14)
@@ -1,6 +1,6 @@
 // SPDX-License-Identifier: CC-BY-SA-4.0
 // SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
-= AFFIRMATION — systemet, as of <UTC timestamp at signing>
+= AFFIRMATION — systemet, as of 2026-07-21T14:43Z
 :toc: macro
 :toclevels: 2
 
@@ -15,33 +15,41 @@ about *systemet* (Equality Theory) at one exact commit. The README is the vision
 `EXPLAINME.adoc` is the mechanism; this file is the receipt. It is our best honest
 belief at a stamped instant, binding on our honesty, not a claim of infallibility.
 
-[NOTE]
-====
-The anchor below carries `<…>` fields (commit SHA, timestamp, toolchain) that are
-filled in *at signing time*, in the same session that runs the checks. Until then
-this file is a draft.
-====
-
 == What we affirm
 
+Every "affirmed-ran" row below was produced by actually running the named
+command in the session that filled this anchor, against the anchor SHA.
+
 [cols="3,1,3",options="header"]
 |===
 | Claim | Status | Evidence
-| The repository is RSR-shaped and validates | affirmed-pending-run | `just validate` at the anchor SHA
-| Equality Theory is *specified* (five layers, three gates, the wager) | affirmed | `README.adoc`, `EXPLAINME.adoc`
-| The theory is the semantic authority; `anytype` is the implementation | affirmed | `.machine_readable/6a2/anchors/ANCHOR.a2ml`, `ECOSYSTEM.a2ml`
+| The repository is RSR-shaped and validates | affirmed-ran | `./scripts/validate-template.sh` — PASS (4 warnings)
+| Equality Theory is *specified*: five layers, three gates, the wager, formal spec per layer/gate, and the citable obligation ledger ET-1..ET-15 | affirmed | `README.adoc`, `EXPLAINME.adoc`, `docs/theory/` incl. `OBLIGATIONS.adoc`
+| The L2 grade-algebra law set (ET-4) and four instances + the product construction (ET-5) are *machine-checked* | affirmed-ran | Lean 4.32.0, `verification/proofs/lean4/Systemet/L2/`; `./scripts/check-proofs.sh lean4` — PASS
+| L1 hereditary substitution and the normalizer are *total by construction* (ET-1, core calculus) and stability `nf_emb : nf (embNf n) = n` is proven | affirmed-ran | `verification/proofs/lean4/Systemet/L1/`; same gate run
+| Every gated theorem depends on nothing outside Lean's three-axiom trusted base; no `sorryAx`, no user axioms | affirmed-ran | axiom audit in `./scripts/check-proofs.sh lean4` (12/12), `Systemet/Audit.lean`
+| The proof gate FAILS on: broken proof, smuggled `axiom`, absent prover, unlisted proof file, status drift | affirmed-ran | watched-to-fail runs recorded in PR #17; drift gate `./scripts/check-proof-status.sh` — PASS
+| The golden path is real: `just test && just quality` runs the proof gates, scans, shape checks — no echo-stub greens | affirmed-ran | Justfile recipes wired to `scripts/*` (this PR); both PASS at the anchor SHA
+| The theory is the semantic authority; `anytype` is the implementation | affirmed | `.machine_readable/6a2/anchors/ANCHOR.a2ml`, `ECOSYSTEM.a2ml`; anytype pins systemet (its issue #13 tracks the pin refresh)
 |===
 
 == What we do NOT claim
 
-* *No completed formal proofs.* `verification/proofs/` holds prover *scaffolding*
-  (Agda/Coq/Idris2/Lean4/TLA+), not finished systemet developments.
-* *L4 TEA-erasure is OPEN.* It is a target, not a theorem. Do not cite it as proven.
+* *ET-2 is not closed.* `DefEq` is stated and stability is proven, but soundness
+  (`DefEq t (embNf (nf t))`), completeness (`DefEq t u → nf t = nf u`), and
+  `decDefEq` are OPEN — MECH-1 milestone 2. "Totality + stability" is not
+  "decidability of conversion".
+* *Mechanization scope is the core calculus* (type-level STLC with base
+  constants and the object arrow; grade algebras as ordered semirings) — not
+  the full-theory ET statements.
+* *L4 TEA-erasure (ET-14) is OPEN.* It is a target, not a theorem. Do not cite
+  it as proven.
+* *The Structural and Polarity gates (ET-6..9), L3 (ET-10/11), and tropes
+  (ET-12/13) have no mechanization* — statements only, in `docs/theory/`.
+* *`just fmt-check` checks nothing* (no formatter is configured for
+  AsciiDoc/Lean); the recipe says so explicitly rather than claiming a pass.
 * *No compiler or checker lives here.* The reference kernel is the separate
   link:https://github.com/hyperpolymath/anytype[anytype] repository, itself early.
-* *L1 totality* is currently a specified requirement, not a discharged proof.
-* The `src/`, `tests/`, and most `docs/` trees are RSR *scaffolding* inherited from
-  the template, not systemet-specific content yet.
 
 == Provenance note
 
@@ -57,12 +65,14 @@ link:https://github.com/hyperpolymath/anytype[anytype]; the profile is AffineScr
 |===
 | Project | systemet
 | Repository | https://github.com/hyperpolymath/systemet
-| Commit (SHA) | <full commit SHA at time of signing>
+| Commit (SHA) | `a11c98774c8c4a1b35c1e3bd9145a191dffb3840` (main = merge of PR #17)
 | Branch | main
-| Timestamp (UTC) | <ISO-8601 UTC timestamp>
-| Toolchain | <provers / tools / versions used to ground the claims>
+| Timestamp (UTC) | 2026-07-21T14:43:22Z
+| Toolchain | Lean 4.32.0 (leanprover/lean4:v4.32.0, commit 8c9756b2, via elan 4.2.3); gates: `scripts/check-proofs.sh` · `scripts/scan-dangerous.sh` · `scripts/check-proof-status.sh` · `scripts/validate-template.sh`
 | Affirmed by | Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 |===
 
-_Landed by a signed git commit. Verify with `git log --show-signature` that the
-anchor SHA above matches the commit that introduced this affirmation._
+_The anchor SHA is the `main` commit whose checked-out tree the commands above
+ran against; this affirmation lands as the next signed commit on top of it.
+Verify the signature with `git log --show-signature` on the commit that
+introduced this file's anchor._
@@ -102,16 +102,12 @@ clean-all: clean
 # TEST & QUALITY
 # ═══════════════════════════════════════════════════════════════════════════════
 
-# Run all tests
+# Run all tests. For a theory repo the test suite IS the proof gates:
+# compile every MANIFESTed module, package build, axiom audit, status drift.
+# An absent prover FAILS (never skips) — see scripts/check-proofs.sh.
 test *args:
-    @echo "Running tests..."
-    # TODO: Replace with your test command
-    # Examples:
-    #   cargo test {{args}}
-    #   mix test {{args}}
-    #   zig build test {{args}}
-    #   deno test {{args}}
-    @echo "Tests passed!"
+    ./scripts/check-proofs.sh lean4
+    ./scripts/check-proof-status.sh
 
 # Run tests with verbose output
 test-verbose:
@@ -214,21 +210,14 @@ fmt:
 
 # Check formatting without changes
 fmt-check:
-    @echo "Checking formatting..."
-    # TODO: Replace with your format check
-    # Examples:
-    #   cargo fmt --check
-    #   mix format --check-formatted
-    #   gleam format --check
+    @echo "fmt-check: no formatter is configured for AsciiDoc/Lean sources — NOTHING is checked here (honest no-op, not a pass)."
 
 # Run linter
 lint:
-    @echo "Linting source files..."
-    # TODO: Replace with your linter
-    # Examples:
-    #   cargo clippy -- -D warnings
-    #   mix credo --strict
-    #   gleam check
+    ./scripts/scan-dangerous.sh
+    ./scripts/check-no-md-in-docs.sh
+    ./scripts/check-root-shape.sh
+    ./scripts/validate-template.sh
 
 # ═══════════════════════════════════════════════════════════════════════════════
 # RUN & EXECUTE

@@ -9,7 +9,7 @@ Equality Theory: one relation at the bottom, discipline in the layers.
 image:https://img.shields.io/badge/License-MPL_2.0-blue.svg[License: MPL-2.0,link="https://opensource.org/licenses/MPL-2.0"]
 image:https://img.shields.io/badge/Docs-CC--BY--SA--4.0-blue.svg[Docs: CC-BY-SA-4.0,link="https://creativecommons.org/licenses/by-sa/4.0/"]
 image:https://img.shields.io/badge/RSR-Rhodium_Standard-9C27B0[Rhodium Standard Repository,link="https://github.com/hyperpolymath/rhodium-standard-repositories"]
-image:https://img.shields.io/badge/status-theory_(no_proofs_yet)-orange[Status: theory, proofs open]
+image:https://img.shields.io/badge/status-theory_(L2_proven%2C_L1_core_proven%2C_rest_OPEN)-orange[Status: theory, core mechanized, rest open]
 
 *systemet* is a stratified type **theory**. The name is `system` + `ET`, where *ET*
 stands for **Equality Theory** — because the one primitive relation the whole system
@@ -242,7 +242,8 @@ graded substrate — which is the whole wager restated.
 
 == Status — read this honestly
 
-systemet is, at this commit, a *theory written down*, not a proven one.
+systemet is, at this commit, a *theory written down with its tractable core
+machine-checked* — not a proven theory.
 
 * The semantics, the layering, the three gates, and the wager are *specified* in
   this repository — prose orientation in this README and `EXPLAINME.adoc`, formal
@@ -251,9 +252,14 @@ systemet is, at this commit, a *theory written down*, not a proven one.
   link:docs/theory/OBLIGATIONS.adoc[`docs/theory/OBLIGATIONS.adoc`] (ET-1..ET-15).
   L3 guarded recursion is *sketched*, not fully specified — see
   link:docs/theory/06-l3-guarded-recursion.adoc[docs/theory/06].
-* The formal proofs are *open*. The `verification/proofs/` tree holds prover
-  scaffolding, not completed systemet proofs; `docs/status/PROOF-STATUS.adoc`
-  is the dated evidence table.
+* The *mechanized core* (Lean 4, hermetic, no mathlib, gated in CI): the L2
+  grade-algebra law set (ET-4) with four instances + the product construction
+  (ET-5) is proven; L1 hereditary substitution and the normalizer are total by
+  construction (ET-1, core calculus) with stability `nf_emb` proven. ET-2's
+  soundness/completeness/`decDefEq` are *open* (statements recorded, never
+  stubbed). Every gated theorem passes an axiom audit (nothing outside Lean's
+  three-axiom trusted base); `docs/status/PROOF-STATUS.adoc` is the dated
+  evidence table, and CI fails if it drifts from the proof MANIFEST.
 * L4 TEA-erasure is an *open problem*, not a result. Do not cite it as proven.
 * There is *no compiler here*. The reference kernel is link:https://github.com/hyperpolymath/anytype[anytype],
   and it is itself at an early stage.