From 7f9b2f7afb35c03897635cc967e61c356e4a1240 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 13:55:42 +0000 Subject: [PATCH 1/3] docs(architecture): Aeneas translations as a default ECHIDNA learning corpus MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Records the owner direction of 2026-11-09 in the same form as the PWG ruling box: first-party Rust verified with Creusot/Pearlite and Verus is also translated with Aeneas by default, as a correspondence corpus for ECHIDNA's mathematical-object arbitration. No proof status rises (the model/Rust correspondence stays ASSUMED, PROOF-POLICY §4.1); backend axioms and Mathlib keep the output out of any PWG count; evidence stays in home repos. Names the PROOF-POLICY §4.1 amendment this needs (to be filed in standards with the ATS2 amendment) and the open design for a shared canonical mathesis record mirrored locally under deed/k9 guard. Verified: asciidoctor --failure-level=WARN renders clean. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01KtYYb2239tLbYa19bmeJAk --- .../estate-mathematical-architecture.adoc | 53 +++++++++++++++++++ 1 file changed, 53 insertions(+) diff --git a/docs/proposals/estate-mathematical-architecture.adoc b/docs/proposals/estate-mathematical-architecture.adoc index c6b7ffa..57ed3a0 100644 --- a/docs/proposals/estate-mathematical-architecture.adoc +++ b/docs/proposals/estate-mathematical-architecture.adoc @@ -62,6 +62,59 @@ per-verb coaptation grades (`.machine_readable/coaptation/`), and the estate uses it for CRG, TRG, ARG and FRG. None of those is a PWG. ==== +[IMPORTANT] +.Aeneas translations as a default learning route for ECHIDNA (owner direction 2026-11-09) +==== +*Default.* First-party Rust that is verified with Creusot/Pearlite and +Verus (PROOF-POLICY §1.2) is also translated with *Aeneas* (via Charon) into +a Lean or Rocq model by default, starting with the security cores. A repo +opts out by saying so in its proof-status file. The owner names the +occasions where it does not apply. + +*Purpose.* The translations are a corpus for ECHIDNA, not proof evidence. +Each translation pairs: + +* the Rust source; +* its Creusot and Verus contracts; +* the Aeneas model; +* where one exists, the Agda theorem and its Rocq or Lean recheck. + +ECHIDNA learns from these pairs how statements correspond across systems. +That is the groundwork for *mathematical-object arbitration*: deciding +whether two artefacts in different systems state the same thing, which is +the estate's equivalence-as-identity through-line. The corpus also exercises +ECHIDNA's cross-prover exchange (OpenTheory, Dedukti) on real estate code. + +*What it does not change.* + +* *No proof status rises.* The theorem about an Aeneas model may be +`PROVEN`. The correspondence between the model and the Rust (Aeneas's +translation) is a separate `ASSUMED` row (PROOF-POLICY §4.1). A Creusot or +Verus result on the code itself is still what establishes implementation +correctness. +* *Backend axioms.* Aeneas's Rocq backend carries an axiom from which +`False` is derivable (its `mk_array` axiom, Aeneas issue #1116). Its Lean +backend depends on Mathlib, which §2 rules out for theory rechecks. Neither +backend's output may stand as a theory witness or count toward a PWG. +Corpus use is unaffected, because nothing in the corpus is counted. +* *Evidence stays home.* Each translation and its receipt live in the home +repository. Mathesis catalogues them as correspondence records, not as +receipts of proof. + +*Policy gap.* PROOF-POLICY §4.1 currently allows Aeneas "only where Rust +code implements a theorem proved in Agda". Making it a default, even for +corpus use, needs an amendment in `metadatastician/standards`. File it +together with the ATS2 amendment (also owner direction 2026-11-09). Until +then, translations outside §4.1's scope are corpus artefacts only and are +recorded as such. + +*Related direction (design open).* Mathesis becomes the shared, canonical +centre for this record. Each participating repository keeps a local copy +that is attested by its deed and kept in line by k9 and coordination +runners. Any drift from, or attempt to change, the canonical record raises +an alert. Fable's restart session sets the mechanism. +==== + == Original working brief (preserved) [literal] From f22faaf2e5d0a50537376add4657fb3b80722b4f Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 14:22:13 +0000 Subject: [PATCH 2/3] chore(canon): adopt canon 2.1.5 (gate table 0.3.1; criteria unchanged) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Canon lockstep is red on main and on every PR: the deed pins canon 2.1.3 while standards canon.lock is 2.1.5 (2.1.4 was an editorial patch; 2.1.5 records gate table 0.3.1 from standards #1419, which only widens accepted layouts). Same change as hyperpolymath/rsr-template-repo#296: version 2.1.5, gates-sha256 5c510bba…, criteria-sha256 unchanged. The (provenance) clause keeps its mint-time 2.1.2 record. Verified: deed-field.sh reads 2.1.5 and 5c510bba…; the gates file on standards main hashes to 5c510bba…; validate-deed.sh with deed_lint.js reports 0 failing. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01KtYYb2239tLbYa19bmeJAk --- mathesis_chora.deed | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/mathesis_chora.deed b/mathesis_chora.deed index 5b1c733..ddb2e29 100644 --- a/mathesis_chora.deed +++ b/mathesis_chora.deed @@ -30,9 +30,9 @@ ; equal canon.lock [canon.artifacts]; canon.lock [canon.lockstep].order is ; spine-adopts-then-canon-releases, so this clause moves FIRST. (canon - :version "2.1.3" + :version "2.1.5" :criteria-sha256 "6a5aa8857bd0d0d58ef48827938ca17c251b6b854dacf59d306388d61694d82a" - :gates-sha256 "2f31f46d4753432e0aa8c9c28f339e18e062c98dc6e6ef4ecbb76993cf37638b" + :gates-sha256 "5c510bba025be718deebb12d0333bfe7db2da43c66578b728b1a334df65290b1" :lockstep-since "2026-09-17" ; A canon change this repo cannot satisfy is a change made in the WRONG ; ORDER, not a rejected change: land the spine's adoption first, then the From 8d280cb9259c841084b170d52f3834bc7dd9447b Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 14:23:09 +0000 Subject: [PATCH 3/3] chore(map): regenerate REPOSITORY-MAP.adoc for applied-systems/ estate-rules' repo_map_determinism_test fails on main: applied-systems/ (owner-requested 2026-11-07) landed without regenerating the map. This is the output of `just repo-map`, unedited. Verified: tests/shape/repo_map_determinism_test.sh passes; scripts/check-root-shape.sh passes. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01KtYYb2239tLbYa19bmeJAk --- docs/architecture/REPOSITORY-MAP.adoc | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/docs/architecture/REPOSITORY-MAP.adoc b/docs/architecture/REPOSITORY-MAP.adoc index d28ba7e..e2cc583 100644 --- a/docs/architecture/REPOSITORY-MAP.adoc +++ b/docs/architecture/REPOSITORY-MAP.adoc @@ -117,6 +117,10 @@ predecessors did. | yes | - +| `applied-systems/` +| yes +| owner-requested reusable applications area (2026-11-07) + | `benches/` | optional | Cargo-conventional at package root @@ -204,6 +208,11 @@ your own repo - but do not read their emptiness as neglect here. | `.machine_readable/bot_directives/` | `.machine_readable/descriptiles/anchors/` | `.machine_readable/scripts/verification/` +| `applied-systems/decision-science/` +| `applied-systems/finance/` +| `applied-systems/finance/cohort-economics/` +| `applied-systems/finance/liquidity/` +| `applied-systems/organisational-design/` | `docs/governance/audit/` | `docs/governance/audit/compliance/` | `docs/governance/audit/effects/`