diff --git a/.machine_readable/coaptation/receipts/latest.toml b/.machine_readable/coaptation/receipts/latest.toml index f51a5288..c97cd1ce 100644 --- a/.machine_readable/coaptation/receipts/latest.toml +++ b/.machine_readable/coaptation/receipts/latest.toml @@ -6,13 +6,13 @@ [receipt] schema = "hyperpolymath.coaptation/1" repo = "mathesis" -band = "green" -proposed-action = "none — the descriptile self-model coapts with the contractile set-point within tolerance." +band = "amber" +proposed-action = "advisory — soft drift within bands (posture/intend). Open an advisory issue; no re-anchor." [coverage] -clauses-total = 52 +clauses-total = 57 descriptile-witnessed = 2 -probe-deferred-to-hunt = 26 +probe-deferred-to-hunt = 32 must-trust-unmeasured-gaps = 0 note = "Yard sees descriptile evidence only; probe-deferred obligations need a Hunt-tier run for a full hard-gate." @@ -21,7 +21,7 @@ grade = "boolean_gate / boolean_gate_provenance" witnessed = 1 refuted = 0 unmeasured-gaps = 0 -probe-deferred = 26 +probe-deferred = 32 gate = "pass" [reading.adjust] @@ -31,9 +31,9 @@ posture-ok = true [reading.intend] grade = "tropical (min-plus distance-to-north-star; wishes excluded)" -committed-intents = 3 -distance = 2 -within-tolerance = true +committed-intents = 6 +distance = 3 +within-tolerance = false [reading.bust] grade = "alarm (recognised break)" @@ -44,13 +44,12 @@ grade = "expected (planned exnovation)" items = 7 [clauses] -intend.repo-initialization = "intent:done" -intend.contractile-completeness = "intent:in_progress" -intend.automation-scripts = "intent:in_progress" -intend.cross-repo-validation = "wish:declared" -intend.automated-substitution = "wish:declared" -intend.formal-verification = "wish:declared" -intend.ecosystem-visualization = "wish:declared" +intend.stage-0-stop-the-conflicts = "intent:done" +intend.stage-1-close-the-holes = "intent:done" +intend.stage-2-one-pipeline = "intent:done" +intend.stage-3-tell-the-truth = "intent:in_progress" +intend.stage-4-three-shelves = "intent:declared" +intend.stage-5-scale = "intent:declared" must.license-present = "probe-deferred" must.readme-present = "probe-deferred" must.security-policy = "probe-deferred" @@ -66,6 +65,12 @@ must.self-validating-structure = "probe-deferred" must.no-placeholder-values = "probe-deferred" must.no-untracked-contractiles = "probe-deferred" must.signed-commits = "probe-deferred" +must.views-current = "probe-deferred" +must.no-private-name = "probe-deferred" +must.no-hand-typed-grade = "probe-deferred" +must.receipts-stay-home = "probe-deferred" +must.home-theorem-has-receipt = "probe-deferred" +must.rows-have-provenance = "probe-deferred" trust.no-secrets-committed = "probe-deferred" trust.no-private-keys = "probe-deferred" trust.no-tokens-in-source = "probe-deferred" @@ -98,5 +103,5 @@ bust.sync-drift-between-repos = "latent" bust.contractile-parse-error = "latent" [provenance] -contractiles = "intend@7439f6b04d89 must@3ace42669b5d trust@9cf409076c92 adjust@f7e9bafc614e dust@bdb7dea20424 bust@4de1f1b3bc91" +contractiles = "intend@89c97164fbff must@b2888ac670fb trust@484d6509ce86 adjust@f7e9bafc614e dust@bdb7dea20424 bust@4de1f1b3bc91" descriptiles = "deed@7182c2cc6635 anchor@11df55a6aaeb" diff --git a/.machine_readable/coaptation/witness-map.ncl b/.machine_readable/coaptation/witness-map.ncl index 32d53700..d7f71136 100644 --- a/.machine_readable/coaptation/witness-map.ncl +++ b/.machine_readable/coaptation/witness-map.ncl @@ -48,12 +48,10 @@ # The `boolean_gate_provenance` grade (a witness carrying its source hash) is a # declared capability awaiting a descriptile that actually carries such evidence. - # --- INTEND: a committed intent realised by the descriptive self-model --- - "intend.repo-initialization" = { - kind = "descriptile", - witnesses = [{ fact = "ecosystem.type", op = 'equals, arg = "repository-template" }], - note = "the deed (ecosystem :position-type) declares this repo IS a template ⇒ the init intent is realised", - }, + # --- INTEND: no descriptile witness. The Mathesis intents are the stages of + # the re-anchoring plan (WO 3.3); each done stage carries its own probe, and + # no deed fact attests a stage. The template intent "repo-initialization", + # witnessed by (ecosystem :position-type "repository-template"), was removed. # --- ADJUST: accessibility/hygiene posture (advisory; never gates) --- # The ANCHOR identity block still carries Mathesis; for the template diff --git a/.machine_readable/contractiles/intend/intend.k9.ncl b/.machine_readable/contractiles/intend/intend.k9.ncl index 67fd5d41..52e30cf8 100644 --- a/.machine_readable/contractiles/intend/intend.k9.ncl +++ b/.machine_readable/contractiles/intend/intend.k9.ncl @@ -114,80 +114,65 @@ let base = import "../_base.ncl" in # ------------------------------------------------------------------- declaration = { preamble = "# SPDX-License-Identifier: MPL-2.0\n# Intentfile — north-star contractile for mathesis\n# Author: Jonathan D.A. Jewell \n#\n# Paired runner: intend.ncl\n# Verb: intend\n#\n# Semantics: North-star contractile. Declares BOTH concrete committed\n# next-actions AND horizon aspirations the project wishes to\n# become. Two sections share one file because they answer\n# the same question at different ranges:\n# [[intents]] — \"we WILL do this; track progress\"\n# status: declared → in_progress → done |\n# deferred | retired\n# [[wishes]] — \"we WISH this were true; revisit later\"\n# status: declared → in_progress → achieved |\n# abandoned\n# grouped by horizon: near / mid / far.\n# Non-gating — this is a report, not a gate. See the `must`\n# contractile for hard gates.\n", - abstract = "North-star contractile for mathesis. This repository is the\ncanonical template for Rhodium Standard Repository compliance. It provides\nthe scaffold that all hyperpolymath repos should copy and customize.", + abstract = "North-star contractile for Mathesis, the maths section of the estate:\nan atlas of the mathematics in other repositories, the theory that no single\nsystem owns, and methods that apply mathematics to decisions. The intents are\nthe stages of the re-anchoring plan (docs/proposals/mathesis-re-anchoring.adoc).", prose = [ { section = "Purpose", - text = "The mathesis serves as the master template for all hyperpolymath\nrepositories. It contains the complete set of contractile files, machine-readable\nspecifications, and governance documentation that define the Rhodium Standard.\n\nEvery new repository in the hyperpolymath estate should be initialized by\ncopying this template and substituting the placeholder values with\nrepo-specific content.", + text = "Mathesis describes what is proved in the estate, where, and how strongly.\nEach statement carries its evidence. Mathesis derives status from the\nreceipts of the home repositories and does not assert it. The standards\nrepository prescribes; the home repositories prove; Mathesis describes.", }, { section = "Anti-Purpose", - text = "This repository is NOT:\n- A general-purpose project scaffold for external use (hyperpolymath-only)\n- A replacement for per-repo customization (all files must be bespoke)\n- A static template that never changes (evolves with RSR spec)\n- A runtime library or framework (build-time only)", + text = "Mathesis is NOT:\n- a prover or a proof kernel: the checker of the home repository decides\n- the proof policy: PROOF-POLICY in standards decides\n- the identity registry: gv-clade-index decides\n- a copy of the proofs or receipts of other repositories\n- a grade authority: it derives a grade and does not assign one\n- a store for private or organisation-specific case material\n- the RSR template: the template is its lineage only", }, { section = "If In Doubt", - text = "If you are unsure whether a change is in scope, ask. Sensitive areas:\n- .machine_readable/ contractile definitions\n- RSR specification files\n- Governance templates\n- License policy documents", + text = "If you are unsure whether a change is in scope, ask. Sensitive areas:\n- .machine_readable/ contractile definitions\n- the census data and the claim pins\n- the receipt of Mathesis (verification/receipts/)\n- License policy documents", }, ], intents = [ { - id = "repo-initialization", - section = "Committed Next-Actions", - description = "Provide just copy-and-substitute template for new repos", - probe = "test -f scripts/init-repo.sh", + id = "stage-0-stop-the-conflicts", + section = "Re-anchoring stages", + description = "Stage 0: triage the open pull requests, and name one writer for census data", + probe = "bash scripts/deed-field.sh --has mathesis_chora.deed bot-directives/census-writer", status = 'done, - notes = "Run with source scripts/init-repo.sh ", }, { - id = "contractile-completeness", - section = "Committed Next-Actions", - description = "Every RSR contractile has a k9 declaration and an ncl implementation", - probe = "ls .machine_readable/contractiles/*/*.k9.ncl | wc -l | grep -q \"^6$\"", - status = 'in_progress, - notes = "Currently 6 contractile verbs: intend, must, trust, adjust, bust, dust", - }, - { - id = "automation-scripts", - section = "Committed Next-Actions", - description = "All repetitive tasks have just recipes", - probe = "grep -c \"^# \" Justfile | grep -q \"^[6-9][0-9]*$\"", - status = 'in_progress, + id = "stage-1-close-the-holes", + section = "Re-anchoring stages", + description = "Stage 1: gate the catalogue and the arrival pack, close the proof gate gap, run Agda, Rocq and Lean in CI, write the receipt of Mathesis", + probe = "test -f verification/receipts/theory_praxis.deed && test -f tests/proofs/gate_controls_test.sh", + status = 'done, }, - ], - wishes = [ { - id = "cross-repo-validation", - section = "Wishes", - group = "Near Horizon", - description = "Tooling to validate all repos against RSR spec", - horizon = 'near, - status = 'declared, + id = "stage-2-one-pipeline", + section = "Re-anchoring stages", + description = "Stage 2: census data as JSON Lines with provenance, the canon reader in the registry, the docs/atlas/ paths, the bridge view, `just check` as the golden path", + probe = "test -f docs/atlas/census/rows.jsonl && test -f docs/atlas/claims/bridges.jsonl && grep -q '^check:' Justfile", + status = 'done, }, { - id = "automated-substitution", - section = "Wishes", - group = "Near Horizon", - description = "Script to automate repo-specific substitution in template", - horizon = 'near, - status = 'declared, + id = "stage-3-tell-the-truth", + section = "Re-anchoring stages", + description = "Stage 3: a true deed, declared capabilities, Mathesis contracts, true entry documents, no private names, a signed affirmation", + status = 'in_progress, + notes = "WO 3.1 to WO 3.6. WO 3.5 ran before WO 3.3 (owner ruling 2026-11-11).", }, { - id = "formal-verification", - section = "Wishes", - group = "Mid Horizon", - description = "Idris2 proofs for all critical contractile invariants", - horizon = 'mid, + id = "stage-4-three-shelves", + section = "Re-anchoring stages", + description = "Stage 4: the admission rule of the theory shelf, the applied shelf tied to the evidence spine, the published atlas", status = 'declared, + notes = "WO 4.3 (publication) needs an owner ruling.", }, { - id = "ecosystem-visualization", - section = "Wishes", - group = "Far Horizon", - description = "Interactive graph of all hyperpolymath repos and dependencies", - horizon = 'far, + id = "stage-5-scale", + section = "Re-anchoring stages", + description = "Stage 5: receipts in the home repositories, a pilot of the bridge lock, a scheduled census, a view of what each repository owes", status = 'declared, }, ], + wishes = [], }, # ------------------------------------------------------------------- diff --git a/.machine_readable/contractiles/must/must.k9.ncl b/.machine_readable/contractiles/must/must.k9.ncl index 812fda6d..b57b9739 100644 --- a/.machine_readable/contractiles/must/must.k9.ncl +++ b/.machine_readable/contractiles/must/must.k9.ncl @@ -125,7 +125,7 @@ let base = import "../_base.ncl" in # ------------------------------------------------------------------- declaration = { preamble = "# SPDX-License-Identifier: MPL-2.0\n# Mustfile — Physical state contract for mathesis\n# Author: Jonathan D.A. Jewell \n#\n# What MUST be true about this repository. Hard requirements.\n# Run with: must check\n# Fix with: must fix (where a deterministic fix exists)\n", - abstract = "Physical-state invariants for mathesis. This is the canonical\nRSR template repository. These are hard requirements — CI and pre-commit\nhooks fail if any check fails.", + abstract = "Physical-state invariants for Mathesis. The template invariants come\nfirst. The section \"Mathesis Invariants\" states the rules of the atlas and\nthe theory shelf. No runner executes these probes yet: the contractile CLI\nhas never been built, so the CI gate named in each note enforces the rule.", prose = [ { section = "Template Integrity", @@ -239,6 +239,52 @@ let base = import "../_base.ncl" in probe = "git verify-commit HEAD", severity = 'critical, }, + { + id = "views-current", + section = "Mathesis Invariants", + description = "Each generated view matches its data", + probe = "bash scripts/census/render-catalogue.sh docs/atlas/census | diff -q docs/atlas/generated/catalogue.adoc - >/dev/null && bun scripts/atlas/census-atlas.mjs check >/dev/null", + severity = 'critical, + notes = "The probe checks the catalogue and the atlas offline. The registry and bridge views need network access and a standards checkout, so `just check` covers them in CI (agda-proof-policy.yml).", + }, + { + id = "no-private-name", + section = "Mathesis Invariants", + description = "No private repository is named: the frame holds public records only, and each row and each not-reached entry belongs to the frame", + probe = "[ \"$(jq -s 'map(select(.visibility != \"public\")) | length' docs/atlas/census/repos.jsonl)\" = 0 ] && bun scripts/atlas/census-atlas.mjs check >/dev/null", + severity = 'critical, + notes = "Ruling D-2 (a): private repositories are a count in docs/atlas/census/private-count.json. The probe prints no name. just atlas-check enforces the same rule in CI.", + }, + { + id = "no-hand-typed-grade", + section = "Mathesis Invariants", + description = "No grade is typed by hand: claim pins and bridge records carry no PWG grade; the registry derives each grade from a receipt", + probe = "! grep -q 'PWG-' docs/atlas/claims/claims.jsonl docs/atlas/claims/bridges.jsonl", + severity = 'critical, + notes = "ADR 0004 and re-anchoring plan WO 2.2 and WO 2.4. A receipt of a home repository records its own grade; Mathesis reads it through the canon reader.", + }, + { + id = "receipts-stay-home", + section = "Mathesis Invariants", + description = "Receipts stay in their homes: the only proof receipt in this repository is the receipt of Mathesis", + probe = "[ \"$(git ls-files -z '*.deed' | xargs -0 grep -l '^ *:profile proof-receipt')\" = verification/receipts/theory_praxis.deed ]", + severity = 'critical, + }, + { + id = "home-theorem-has-receipt", + section = "Mathesis Invariants", + description = "Each theorem whose home is Mathesis has a receipt: each claim of the receipt has a claim pin, and each Mathesis claim pin names a claim of its receipt", + probe = "R=verification/receipts/theory_praxis.deed; C=docs/atlas/claims/claims.jsonl; grep -o '(claim :id \"[^\"]*\"' \"$R\" | cut -d'\"' -f2 | while read -r c; do jq -e --arg id \"hyperpolymath/mathesis#$c\" 'select(.id == $id)' \"$C\" >/dev/null || exit 1; done && jq -r 'select(.repo == \"hyperpolymath/mathesis\") | \"\\(.receipt.path) \\(.id | sub(\"^.*#\"; \"\"))\"' \"$C\" | while read -r p c; do grep -q \"(claim :id \\\"$c\\\"\" \"$p\" || exit 1; done", + severity = 'critical, + }, + { + id = "rows-have-provenance", + section = "Mathesis Invariants", + description = "Each census row names the commit it read and the time it read it", + probe = "[ \"$(jq -s 'map(select((.commit | test(\"^[0-9a-f]{40}$\") | not) or (.censused_at | test(\"^[0-9]{4}-[0-9]{2}-[0-9]{2}T[0-9]{2}:[0-9]{2}:[0-9]{2}Z$\") | not))) | length' docs/atlas/census/rows.jsonl)\" = 0 ]", + severity = 'critical, + notes = "Re-anchoring plan WO 2.1. A row without either field makes jq fail, and the probe fails closed.", + }, ], }, diff --git a/.machine_readable/contractiles/trust/trust.k9.ncl b/.machine_readable/contractiles/trust/trust.k9.ncl index 6847e6b6..cb0af0ce 100644 --- a/.machine_readable/contractiles/trust/trust.k9.ncl +++ b/.machine_readable/contractiles/trust/trust.k9.ncl @@ -131,11 +131,15 @@ let base = import "../_base.ncl" in # ------------------------------------------------------------------- declaration = { preamble = "# SPDX-License-Identifier: MPL-2.0\n# Trustfile — Trust boundaries and integrity invariants for mathesis\n# Author: Jonathan D.A. Jewell \n#\n# Defines what LLM/SLM agents are trusted to do without asking, and\n# integrity invariants that verify the repo has not been tampered with.\n", - abstract = "Trust boundaries and integrity checks for mathesis. This file\ncombines the trust-level definitions from the original TRUST.contractile\nwith the integrity invariants from the old Trustfile.a2ml. It defines\nwhat AI agents may do autonomously and what requires human approval,\nplus checks that verify repository integrity.", + abstract = "Trust boundaries and integrity checks for Mathesis. This file\ncombines the trust-level definitions from the original TRUST.contractile\nwith the integrity invariants from the old Trustfile.a2ml. It defines\nwhat AI agents may do autonomously and what requires human approval,\nplus checks that verify repository integrity.", prose = [ { section = "Trust Levels", - text = "The mathesis operates at trust level: maximal\n\nTrust levels:\n- maximal: Agent may read, build, test, lint, format, heal freely.\n Only destructive/external actions require approval.\n- standard: Agent may read and build. Test/lint need approval.\n- restricted: Agent may read only. All modifications need approval.\n- minimal: Agent may read specific files only. Everything else blocked.\n\nCurrent trust level: maximal", + text = "Mathesis operates at trust level: maximal\n\nTrust levels:\n- maximal: Agent may read, build, test, lint, format, heal freely.\n Only destructive/external actions require approval.\n- standard: Agent may read and build. Test/lint need approval.\n- restricted: Agent may read only. All modifications need approval.\n- minimal: Agent may read specific files only. Everything else blocked.\n\nCurrent trust level: maximal", + }, + { + section = "Writers", + text = "Who writes which record in Mathesis (re-anchoring plan WO 3.3):\n- Census rows and the not-reached list: only `just census` and `just update-rows`; nobody edits them by hand (deed bot-directives census-writer).\n- The frame repos.jsonl and private-count.json: a person refreshes them from the GitHub listing; the frame holds public records only (ruling D-2 (a)).\n- Claim pins (claims.jsonl) and bridge records (bridges.jsonl): authored by a person or an agent, and reviewed in a pull request; they hold no grade.\n- Generated views (docs/atlas/generated/): only their generators; `just check` fails on a stale view.\n- Grades: no writer in Mathesis. The registry derives each grade from a receipt through the canon reader.\n- Receipts of other repositories: their home repositories only. Mathesis pins and reads them.\n- The receipt of Mathesis (verification/receipts/): written from observed checker runs only.\n- The deed: only scripts/deed-clause.sh.\n- CLAUDE.md and the coaptation receipt: only `just claude-md` and `just coapt`.\n- Contractiles: the owner reviews each clause before it lands.", }, ], verifications = [