From 8e22fe553a5b8ef740349a0faa938fdf1d3b6ad6 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 21 Jul 2026 15:47:27 +0100 Subject: [PATCH] chore(state): truth-sync STATE + fill the AFFIRMATION anchor + wire the golden path MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit STATE.a2ml: completion 15 -> 32 (spec + ledger + L2 proven + L1 totality core; MECH-1 milestone 2, gates beyond L2, tropes, TEA all still open); phase design -> implementation; blockers echo issues #18/#19 and the anytype audit (#13-#19 there); critical-next-actions = finish ET-2. AFFIRMATION.adoc: anchor filled in the same session that re-ran every check against main @ a11c9877 (merge of #17): check-proofs (PASS, axiom audit 12/12), scan-dangerous (PASS), check-proof-status (PASS), validate-template (PASS, 4 warnings), just test + just quality (PASS). Claims table now separates affirmed-ran from affirmed; NOT-claims spell out exactly what remains open (ET-2 closure, ET-6..14). Justfile: test/lint/fmt-check were template echo-stubs ("Tests passed!" over commented-out commands — fake green). test now runs the proof gates + drift gate; lint runs scan-dangerous, md-in-docs, root-shape, validate-template; fmt-check states explicitly that nothing is checked. check-no-vlang.sh deferred to #19 (115 template zig refs + policy question). Root-allow updated for entries landed by #14/#17. README: badge and Status section updated to the mechanized-core truth. Co-Authored-By: Claude Fable 5 --- .machine_readable/6a2/STATE.a2ml | 41 +++++++++++++++++------- .machine_readable/root-allow.txt | 8 +++++ AFFIRMATION.adoc | 54 +++++++++++++++++++------------- Justfile | 31 ++++++------------ README.adoc | 16 +++++++--- scripts/check-no-md-in-docs.sh | 0 scripts/check-no-vlang.sh | 0 scripts/check-root-shape.sh | 0 8 files changed, 90 insertions(+), 60 deletions(-) mode change 100644 => 100755 scripts/check-no-md-in-docs.sh mode change 100644 => 100755 scripts/check-no-vlang.sh mode change 100644 => 100755 scripts/check-root-shape.sh diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index b783caf..a1dd01e 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -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] diff --git a/.machine_readable/root-allow.txt b/.machine_readable/root-allow.txt index 45d39fd..a432c99 100644 --- a/.machine_readable/root-allow.txt +++ b/.machine_readable/root-allow.txt @@ -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) diff --git a/AFFIRMATION.adoc b/AFFIRMATION.adoc index 525fa3a..85dc617 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 += 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) | +| Commit (SHA) | `a11c98774c8c4a1b35c1e3bd9145a191dffb3840` (main = merge of PR #17) | Branch | main -| Timestamp (UTC) | -| Toolchain | +| 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 |=== -_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._ diff --git a/Justfile b/Justfile index 9f28b06..d74d4b2 100644 --- a/Justfile +++ b/Justfile @@ -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 diff --git a/README.adoc b/README.adoc index 1398edf..5fff620 100644 --- a/README.adoc +++ b/README.adoc @@ -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. diff --git a/scripts/check-no-md-in-docs.sh b/scripts/check-no-md-in-docs.sh old mode 100644 new mode 100755 diff --git a/scripts/check-no-vlang.sh b/scripts/check-no-vlang.sh old mode 100644 new mode 100755 diff --git a/scripts/check-root-shape.sh b/scripts/check-root-shape.sh old mode 100644 new mode 100755