From c6ffc8e7ad8b35da02a689e392e15bd4d4fc287b Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" Date: Mon, 12 Oct 2026 15:56:05 +0000 Subject: [PATCH 1/3] Family map: register resource-algebra, occupancy, katagoria; connection statuses after 2026-10-12; proof-kernel decision record --- docs/TYPE-CONNECTIONS.adoc | 27 +++++++++ .../D-2026-10-12-proof-kernel-ruling.adoc | 55 +++++++++++++++++++ 2 files changed, 82 insertions(+) create mode 100644 docs/decisions/D-2026-10-12-proof-kernel-ruling.adoc diff --git a/docs/TYPE-CONNECTIONS.adoc b/docs/TYPE-CONNECTIONS.adoc index 6cbd55f..0003625 100644 --- a/docs/TYPE-CONNECTIONS.adoc +++ b/docs/TYPE-CONNECTIONS.adoc @@ -273,3 +273,30 @@ The graphic is a checked-in SVG so it displays in the AsciiDoc README without JavaScript or a diagram service. Its editable source is link:images/type-connections.dot[type-connections.dot]. Rebuild it with `just type-map` (Graphviz required). + + +== Additions 2026-10-12 + +Registered this day, pending merge into the tables above. + +[cols="1,3",options="header"] +|=== +| Member | What it establishes +| https://github.com/hyperpolymath/resource-algebra[Resource Algebra] (kernel module) | The parametric grade algebra: alternatives an idempotent commutative monoid, sequence a monoid; order, dioid and annihilation as layers. Instances: echo Loss (min-plus), tropical MaxPlus, HWM (occupancy). Loss and cost have opposite induced orders (checked). +| https://github.com/hyperpolymath/occupancy-types[Occupancy Types] | High-water-mark occupancy; reclamation at a cut; occupancy ≤ cost with equality iff nothing is reclaimed; independent threads have order-dependent peaks invisible locally. +| https://github.com/hyperpolymath/katagoria[Katagoria] (incubator, not a family) | Graduation rule to be written: an idea leaves only when a family repo holds its kernel-checked core theorem. +|=== + +[cols="1,2,2",options="header"] +|=== +| Connection | Status | Established +| Resource Algebra → Choreographic | PROVEN (fragment) | K-CUT-LOSS parametric; needs only ⊕-idempotence and ⊗-left-unit. +| Epistemic → Choreographic | PROVEN (fragment) | K-CUT-WARRANT bound and transport; Kripke frame over consistent cuts; SoundWarrant instantiated. +| Tropical → Choreographic | PROVEN via MaxPlus instance | Lean provenance bridge (M-2) a review obligation. +| Echo → Choreographic | PROVEN via Loss instance | RoleGraded base case recovered; import direction (L-2) open. +| Occupancy → Choreographic | PROVEN (A-3) | Two-thread diamond: projections swap, occupancy does not. +| Residual → Epistemic | DECIDED: family | Dependence is not a function of the candidate set. +| Secret → (none yet) | OPEN | TINI proved; the Echo reading of noninterference is a conjecture. +|=== + +Decision record: link:decisions/D-2026-10-12-proof-kernel-ruling.adoc[] (proof kernel for the family). diff --git a/docs/decisions/D-2026-10-12-proof-kernel-ruling.adoc b/docs/decisions/D-2026-10-12-proof-kernel-ruling.adoc new file mode 100644 index 0000000..754162a --- /dev/null +++ b/docs/decisions/D-2026-10-12-proof-kernel-ruling.adoc @@ -0,0 +1,55 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Place at nextgen-typing/docs/decisions/ and renumber to the local sequence. += D-2026-10-12 — Proof kernel for the type family +:revdate: 2026-10-12 + +== Status + +Ruled by the owner, 2026-10-12, after a comparison recorded in the +accompanying session. Supersedes per-repo prover choice for the family. + +== Decision + +. *Agda `--safe --without-K` is the proof kernel of the type family* + (echo-types, epistemic-types, residual-evidence-types, choreographic-types, + secret-types, resource-algebra; absolute-zero's active CNO/OND/EchoBridge + stack). +. *Idris2 is the ABI/runtime layer*, not a kernel candidate (QTT linearity is + the right tool there; `believe_me`/`assert_total` make it the wrong one for + theorems). +. *Lean 4 is provenance*: jtv keeps its existing proof layer; tropical-types' + Lean and Isabelle developments remain as the Mathlib/AFP-facing record and + are *ported*, not imported, into Agda where the family needs them. +. *Isabelle/HOL only for AFP submissions.* Coq, Mizar: archived (absolute-zero + ruling 2026-10-10 stands). + +== Evidence weighed + +* Investment: ≈47.7k lines of Agda across the family, every file + `--safe --without-K`, 3 postulates total; ≈6.4k active Lean; 7.1k Isabelle + (tropical only); Idris2 almost entirely RSR ABI scaffolding. +* K: the equivalence-as-identity programme needs a kernel without UIP. Lean's + Prop proof-irrelevance gives K by construction; Idris2 has no without-K + mode; Agda has `--without-K` and `--cubical`. +* Discipline: `--safe` is the strictest mechanical falsifier in the estate and + is already uniform. +* Cost: consolidating on Idris2 or Lean would mean re-proving the Agda + corpus; not viable this quarter. + +== Falsifier + +resource-algebra (the first repo written under the ruling) had to reach a +postulate-free `ResourceAlgebra` record with three instances under the flags +within a week. It did on day one (`just check`, Agda 2.6.3), so the ruling +stands; it is revisited if a family theorem is later found unstateable under +`--without-K`. + +== Consequences + +* absolute-zero `LANGUAGE-POLICY.adoc` v1.6.0 ("Idris2 is the only + formal-verification language") needs an exception record (see T1); the + constitution's change procedure applies. +* katagoria's Idris2 research sketches remain the incubator's prototypes; + graduation into a family repo means an Agda formalisation. +* Creusot and SPARK are implementation-verification questions for januskey's + and jtv's Rust surfaces, outside this ruling. From a92f5db9d80900ecac918785be9074f82f90b2a1 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 12 Oct 2026 21:14:35 +0100 Subject: [PATCH 2/3] Update docs/decisions/D-2026-10-12-proof-kernel-ruling.adoc Co-authored-by: coderabbitai[bot] <136622811+coderabbitai[bot]@users.noreply.github.com> Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com> --- docs/decisions/D-2026-10-12-proof-kernel-ruling.adoc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/decisions/D-2026-10-12-proof-kernel-ruling.adoc b/docs/decisions/D-2026-10-12-proof-kernel-ruling.adoc index 754162a..b7bb2d5 100644 --- a/docs/decisions/D-2026-10-12-proof-kernel-ruling.adoc +++ b/docs/decisions/D-2026-10-12-proof-kernel-ruling.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-License-Identifier: MPL-2.0 // Place at nextgen-typing/docs/decisions/ and renumber to the local sequence. = D-2026-10-12 — Proof kernel for the type family :revdate: 2026-10-12 From 3b2f6e26ae58dcbf528ee803d047c682e8dca022 Mon Sep 17 00:00:00 2001 From: "coderabbitai[bot]" <136622811+coderabbitai[bot]@users.noreply.github.com> Date: Mon, 12 Oct 2026 20:18:26 +0000 Subject: [PATCH 3/3] docs(proof-kernel): correct postulate counts and qualify safe-check claims --- .../D-2026-10-12-proof-kernel-ruling.adoc | 29 +++++++++++++++---- 1 file changed, 23 insertions(+), 6 deletions(-) diff --git a/docs/decisions/D-2026-10-12-proof-kernel-ruling.adoc b/docs/decisions/D-2026-10-12-proof-kernel-ruling.adoc index b7bb2d5..9c0c1d5 100644 --- a/docs/decisions/D-2026-10-12-proof-kernel-ruling.adoc +++ b/docs/decisions/D-2026-10-12-proof-kernel-ruling.adoc @@ -1,5 +1,4 @@ // SPDX-License-Identifier: MPL-2.0 -// Place at nextgen-typing/docs/decisions/ and renumber to the local sequence. = D-2026-10-12 — Proof kernel for the type family :revdate: 2026-10-12 @@ -25,14 +24,32 @@ accompanying session. Supersedes per-repo prover choice for the family. == Evidence weighed -* Investment: ≈47.7k lines of Agda across the family, every file - `--safe --without-K`, 3 postulates total; ≈6.4k active Lean; 7.1k Isabelle - (tropical only); Idris2 almost entirely RSR ABI scaffolding. +* Investment: the comparison reported ≈47.7k lines of Agda across the + family; ≈6.4k active Lean; 7.1k Isabelle (tropical only); Idris2 almost + entirely RSR ABI scaffolding. These estimates are not a safe-check receipt. +* Postulate inventory: at echo-types commit + `e38fd465c4269ab9e9940802525630d7aae1e848`, three `postulate` blocks + declare *six* assumptions: +** https://github.com/hyperpolymath/echo-types/blob/e38fd465c4269ab9e9940802525630d7aae1e848/proofs/agda/EchoImageFactorizationPropPostulated.agda[EchoImageFactorizationPropPostulated.agda]: + `Trunc-pos`, `∣_∣-pos`, `is-prop-pos`, and `rec-pos` (one block). +** https://github.com/hyperpolymath/echo-types/blob/e38fd465c4269ab9e9940802525630d7aae1e848/proofs/agda/Ordinal/Buchholz/Fidelity.agda[Ordinal/Buchholz/Fidelity.agda]: + `denotation` and `ordinal-upper-bound` (two blocks). ++ +Both modules use `--without-K` only, are excluded from `All.agda` and +`Smoke.agda`, and are exempted by Echo's foundation guardrail. They are +outside the `--safe --without-K` checks; `--safe` rejects these postulates. +This is not a family-wide total: choreographic-types also contains the +https://github.com/hyperpolymath/choreographic-types/blob/a0f647531a8cacad10294703ade2b6c8cec3255c/applications/rapidnj-two-thread.agda[standalone RapidNJ interface/conjecture sketch], +with postulates and no safe-check flags, outside its repository build. +The earlier “3 postulates total” and “every file” claims are withdrawn. +The link:../TYPE-CONNECTIONS.adoc[existing proof receipts] cover bounded +checks; the complete constituent suites were not rerun for this record. * K: the equivalence-as-identity programme needs a kernel without UIP. Lean's Prop proof-irrelevance gives K by construction; Idris2 has no without-K mode; Agda has `--without-K` and `--cubical`. -* Discipline: `--safe` is the strictest mechanical falsifier in the estate and - is already uniform. +* Discipline: `--safe --without-K` is required for the selected proof kernel. + This requirement does not establish uniform compliance across exploratory + files or constitute an estate-wide verification result. * Cost: consolidating on Idris2 or Lean would mean re-proving the Agda corpus; not viable this quarter.