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/` 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] 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