hyperpolymath · hyperpolymath · Jul 29, 2026 · Jul 29, 2026
@@ -6,16 +6,16 @@
 [metadata]
 project = "systemet"
 version = "0.1.0"
-last-updated = "2026-07-21"
+last-updated = "2026-07-29"
 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."
-# 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
+# 46, not higher: ET-2 is CLOSED (conversion decidable, axiom-clean) and
+# ADR-0002 fixes ET-14 item (3), but the eta normalizer, the gates beyond L2,
+# tropes, and TEA (ET-14) itself are all open. See docs/status/PROOF-STATUS.adoc.
+completion-percentage = 46
 
 [position]
 phase = "implementation"   # design | implementation | testing | maintenance | archived
@@ -25,16 +25,19 @@ maturity = "experimental"  # experimental | alpha | beta | production | lts
 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 = 95 },
-  { name = "Phase 2: Formal spec of L1 (equality = conversion) + totality obligation", completion = 65 },
+  { name = "Phase 2: Formal spec of L1 (equality = conversion) + totality obligation", completion = 88 },
   { 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 2 at 88: spec written (docs/theory/02 + OBLIGATIONS ET-1..3); mechanized in
+#   Lean 4: hereditary substitution + normalizer total (ET-1), stability nf_emb,
+#   and MECH-1 milestone 2 COMPLETE -- soundness, completeness, defEq_iff_nf,
+#   decEqNf/decEqSp, decDefEq all proven (ET-2 closed for the core calculus,
+#   axiom audit 22/22). Remaining 12%: the eta extension is half-landed
+#   (eta-long forms, DefEqE + embedding, DecidableEq) but the eta-long
+#   normalizer nfE is open -- issue #32.
 # 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);
@@ -43,15 +46,18 @@ milestones = [
 [blockers-and-issues]
 issues = [
   { id = 18, title = "descriptiles/6a2 migration (blocked: contractiles.mjs needs Node, estate-denied here)" },
+  { id = 30, title = "K9 gate now real and red: content debt here + the K9!-vs-nickel spec catch-22 upstream" },
+  { id = 32, title = "eta extension: normalizer open; four diagnosed defects in EtaExpand block it" },
 ]
 # 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 = [
-  "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.",
+  "eta extension (issue #32): clear the four EtaExpand defects -- start at adjSwp (smaller cast problem, same rem/vs reshaping idiom as adjWkv), attack wkNfE_etaNe in parallel (independent of the Adj machinery) -- then build the never-written cluster (etaSubstHit, etaLaw, etaSubstAdj, appSpEtaNe, nappEtaNe) and finally nfE.",
+  "Then Structural Gate soundness (ET-6/7), which reuses the same normal-form machinery.",
+  "ET-14 remains OPEN and owner-gated on the remaining ADR items (L4 handler syntax, the T/E/A predicates, the erasure translation); ADR-0002 fixed only item (3).",
+  "Keep README/EXPLAINME/AFFIRMATION claims inside what is proven; TEA-erasure stays a target.",
   "One worked per-API trope instance (ET-12/13) after the gate work.",
 ]
 

@@ -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 2026-07-21T14:43Z
+= AFFIRMATION — systemet, as of 2026-07-29T07:27Z
 :toc: macro
 :toclevels: 2
 
@@ -27,18 +27,28 @@ command in the session that filled this anchor, against the anchor SHA.
 | 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`
+| 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` (**22/22**), `Systemet/Audit.lean`
+| *ET-2 is CLOSED for the core calculus*: `soundness : DefEq t (embNf (nf t))`, `completeness : DefEq t u → nf t = nf u`, `defEq_iff_nf`, hand-rolled `decEqNf`/`decEqSp`, and `decDefEq : Decidable (DefEq t u)` are proven — conversion is decidable | affirmed-ran | `verification/proofs/lean4/Systemet/L1/{SubstLemmas,Soundness,Completeness,Decidable}.lean`; `#print axioms` → `[propext, Quot.sound]` only
+| The η extension is *partially* landed: η-long forms `NfE`/`SpE` (neutrals only at `★`), `DefEqE` (β **+ a real η rule**), the embedding `defEq_to_defEqE`, and `DecidableEq` for `NfE`/`SpE` | affirmed-ran | `Systemet/L1/Eta{Normal,Conversion,SubstLemmas,Hsub,DecEq}.lean`; same gate run
+| *ADR-0002 is accepted*: ET-14's item (3) — the L0 observational equivalence — is fixed as the `≈` of a parametric `L0Observation`, and ET-16 enters the ledger narrowly | affirmed | `docs/decisions/0002-…adoc` (Status: Accepted), `docs/theory/OBLIGATIONS.adoc`
 | 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
 
-* *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".
+* *ET-2's scope is β only.* `DefEq` is β + equivalence + congruence; **η is not
+  included**, so ET-3 is untouched. "Conversion is decidable" here means
+  *β-conversion on the core calculus*, nothing wider.
+* *The η extension is NOT finished.* Landed: η-long forms, `DefEqE`, the β→βη
+  embedding, decidable equality. **Open: the η-long normalizer `nfE`**, and with
+  it soundness, completeness, `defEqE_iff_nfE`, `decDefEqE`, and the
+  anti-vacuity example. Four defects in `EtaExpand` block it (issue #32). Do not
+  read the landed half as βη-decidability.
+* *ADR-0002 decides a definition, not a theorem.* Accepting the parametric
+  `L0Observation` lets ET-14 be *stated*; it is not progress toward proving it,
+  and ET-16 names an obligation it does not discharge.
 * *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.
@@ -65,9 +75,9 @@ link:https://github.com/hyperpolymath/anytype[anytype]; the profile is AffineScr
 |===
 | Project | systemet
 | Repository | https://github.com/hyperpolymath/systemet
-| Commit (SHA) | `a11c98774c8c4a1b35c1e3bd9145a191dffb3840` (main = merge of PR #17)
+| Commit (SHA) | `662b17217f38fd2058a7ef227083281d4ba3e421` (branch `docs/state-refresh-2026-07-29`, cut from main)
 | Branch | main
-| Timestamp (UTC) | 2026-07-21T14:43:22Z
+| Timestamp (UTC) | 2026-07-29T07:27Z
 | 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>
 |===

@@ -1,4 +1,6 @@
 #!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 set -euo pipefail
 
 SCRIPT_DIR="$(cd -- "$(dirname -- "${BASH_SOURCE[0]}")" && pwd)"

@@ -152,8 +152,6 @@ REQUIRED_WORKFLOWS=(
     "security-policy.yml"
     "wellknown-enforcement.yml"
     "workflow-linter.yml"
-    "npm-bun-blocker.yml"
-    "ts-blocker.yml"
     "secret-scanner.yml"
 )
 

@@ -1,3 +1,5 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 import Systemet.L1.Syntax
 import Systemet.L1.Normal
 import Systemet.L1.Hsub