From c6dee2dd02840f8271aa0c1e01a161fb57fed144 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 29 Jul 2026 08:30:38 +0100 Subject: [PATCH] docs(state): refresh AFFIRMATION + STATE.a2ml; resync the template validator Human receipt and machine state were both stale at 2026-07-21 -- they still described ET-2 as open, months of work after it closed. AFFIRMATION.adoc (the dated, signed receipt -- claims re-run at this SHA): * axiom audit 12/12 -> 22/22 * NEW affirmed-ran: ET-2 CLOSED for the core calculus (soundness, completeness, defEq_iff_nf, decEqNf/decEqSp, decDefEq; #print axioms -> [propext, Quot.sound] only) * NEW affirmed-ran: the eta extension is PARTIALLY landed (eta-long NfE/SpE with neutrals only at star, DefEqE with a real eta rule, defEq_to_defEqE, DecidableEq) * NEW affirmed: ADR-0002 accepted -- ET-14 item (3) fixed as the parametric L0Observation; ET-16 in the ledger narrowly * "What we do NOT claim" rewritten so the new results cannot be over-read: ET-2 is BETA-ONLY (eta excluded, ET-3 untouched); the eta extension is NOT finished (normalizer open, four diagnosed defects, issue #32); and ADR-0002 decides a DEFINITION, not a theorem -- it lets ET-14 be stated, which is not progress toward proving it. STATE.a2ml (machine-readable): * completion 32 -> 46; Phase 2 65 -> 88 with the remaining 12% explained * issues 30 and 32 added to blockers * critical-next-actions rewritten: milestone 2 is done, so the next action is the eta cluster, with the ATTACK ORDER recorded (adjSwp before adjWkv -- same rem/vs reshaping idiom, smaller instance; wkNfE_etaNe in parallel) scripts/validate-template.sh: dropped npm-bun-blocker.yml and ts-blocker.yml from REQUIRED_WORKFLOWS. PR #35 deliberately retired both under the Bun-first runtime policy, but the validator still demanded them -- so the repo's own template check contradicted its own ruling and exited 1. Now PASSES. Also added the two missing SPDX headers the validator warned about (Systemet.lean, scripts/invariant-path.sh) -- both pre-existing. Verified at this SHA: cold rebuild 21 jobs; check-proofs (22/22 audit), scan-dangerous, check-proof-status, check-root-shape, validate-template all real exit 0. Co-Authored-By: Claude Opus 5 --- .machine_readable/6a2/STATE.a2ml | 32 +++++++++++++++---------- AFFIRMATION.adoc | 26 +++++++++++++------- scripts/invariant-path.sh | 2 ++ scripts/validate-template.sh | 2 -- verification/proofs/lean4/Systemet.lean | 2 ++ 5 files changed, 41 insertions(+), 23 deletions(-) diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index 21f8ef7..8298e8b 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -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.", ] diff --git a/AFFIRMATION.adoc b/AFFIRMATION.adoc index 85dc617..f3127c1 100644 --- a/AFFIRMATION.adoc +++ b/AFFIRMATION.adoc @@ -1,6 +1,6 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 // SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell -= AFFIRMATION — systemet, as of 2026-07-21T14:43Z += AFFIRMATION — systemet, as of 2026-07-29T07:27Z :toc: macro :toclevels: 2 @@ -27,7 +27,10 @@ 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) @@ -35,10 +38,17 @@ command in the session that filled this anchor, against the anchor SHA. == 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 |=== diff --git a/scripts/invariant-path.sh b/scripts/invariant-path.sh index 3f7c05b..8214587 100755 --- a/scripts/invariant-path.sh +++ b/scripts/invariant-path.sh @@ -1,4 +1,6 @@ #!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) set -euo pipefail SCRIPT_DIR="$(cd -- "$(dirname -- "${BASH_SOURCE[0]}")" && pwd)" diff --git a/scripts/validate-template.sh b/scripts/validate-template.sh index 6a8ba69..97ba0f2 100755 --- a/scripts/validate-template.sh +++ b/scripts/validate-template.sh @@ -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" ) diff --git a/verification/proofs/lean4/Systemet.lean b/verification/proofs/lean4/Systemet.lean index a20b75b..2b53c9c 100644 --- a/verification/proofs/lean4/Systemet.lean +++ b/verification/proofs/lean4/Systemet.lean @@ -1,3 +1,5 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) import Systemet.L1.Syntax import Systemet.L1.Normal import Systemet.L1.Hsub