From b0cbf1087a930232b09f7ff3495f08bd04ffc4cb Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 13 Oct 2026 14:27:45 +0000 Subject: [PATCH 01/15] =?UTF-8?q?docs(spec):=20consolidate=20the=20calculu?= =?UTF-8?q?s=20at=20v0.2=20=E2=80=94=20one=20normative=20document=20on=20t?= =?UTF-8?q?he=20ratified=20carrier?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit spec/calculus.adoc was a v0.1 document (revnumber 0.1, 2026-06-22) with the 2026-07-07 ratification spliced in as notes, a separate never-merged v0.2 addendum (spec/calculus-v0.2-draft.adoc, 2026-06-23), and two design notes carrying the operational model and the L4 analysis. It still said "seven effects" while the vocabulary, EffectAtoms.lean and the IR say nine. A reader — or an agent — following the spec alone got the pre-ratification world. This folds the four into one v0.2 spec. What changed, section by section: - §1: the object is stated as "property-instances as particulars", which every instance ontology supplies (tropes, modes, moments, qualities, SDCs), rather than as a commitment to one-category trope theory; §2 names the two constructs (attenuate, detach/FloatingQuality) that need instances to be particulars and would not survive a change of ontology. - §3: the fate chain, bond fibring (HC-4) and merge are stated on the ratified carrier with A1–A3 inline; new §3.5 gives the nine-effect / nine-atom-family table (EffectAtoms.lean) and the two structure theorems, so "seven" and "nine" are reconciled: nine families, six writable, three faults. - §4: L3 and L5 cover all three deceptive bottoms (two-sided zeros, A1); L4 is stated as holding in full with the Idris2/Lean/Agda lemma names; L6 (commutativity) is new; the addendum's R-2026-06-23-02..04 become the cancellation structure C1–C3 with the ratified lemma names; the tropical factorisation re-run is recorded as (B′) sighted, with the pre-ratification (B) result kept as history. - §5 T-Fuse: ⊔ is written ⊓ — the retention-order meet, "no better than its worse constituent" — matching the CO-1 note. Same meaning, one symbol. - §6: the prevent/detect decision now names all three deceptive duals. - §7: restated as greatest post-fixed point in the retention order with the decidable T-Fix-Decl rule, from the CO-1 note; the operational model is marked DESIGNED and its mechanisation OPEN. - §8: each soundness result carries its status (exact lowering and β/let PROVED; conservative lowering and fix OPEN); the third firewall now cites a defined O5. - §9.3: prover roles per the 2026-10-12 kernel ruling (Agda kernel, Idris2 executable reference, Lean provenance, Rust fast core) — see ADR 0005. - §10: O1 split into O1-carrier (PROVED) and O1-coord (OPEN, with the bond-transfer probe recorded as the live falsifier); O4 RESOLVED (ADR 0004); O5 DEFINED (adopted from the workbench proposal of 2026-07-17); O6 (ceiling verdict) newly opened; CO-1 listed with its DESIGNED/OPEN split. Every lemma name cited in the spec was checked against the source files on this branch (Idris2 Trope.*, Agda TB.*, Lean grade-boundary/* and grade-factorisation/*). No normative rule changes semantics; the IR stays 0.2. The README's repo map, firewall 3 and Status paragraph are brought into step; INTEGRATION-REPORT.adoc gets a header note marking it historical rather than being rewritten. CHANGELOG, ADR 0003 and PROOF-STATUS's dated history keep their references to the addendum as records of what was true when written. --- README.adoc | 34 +- spec/calculus-v0.2-draft.adoc | 410 --------------- spec/calculus.adoc | 520 +++++++++++++------- verification/proofs/INTEGRATION-REPORT.adoc | 11 + 4 files changed, 372 insertions(+), 603 deletions(-) delete mode 100644 spec/calculus-v0.2-draft.adoc diff --git a/README.adoc b/README.adoc index d1d8967..1bec043 100644 --- a/README.adoc +++ b/README.adoc @@ -45,8 +45,10 @@ an existing language could emit the same IR and be checked by the same checker. (calculus O2), discharged per front-end, not here. . *Veridicality is declared and propagated, not checked.* Detecting that a value claimed faithful is in fact false needs a ground-truth oracle the checker does - not have (calculus O5). The checker guarantees only that deception does not - compose away and that deceptive grades fail every honest floor. + not have — and cannot have: veridicality is undecidable relative to the IR + (calculus §10-O5, Remark O5-a). The checker guarantees only that deception does + not compose away and that deceptive grades fail every honest floor; a deployment + MAY bind an external oracle under the O5-1..3 conditions. == Deploy variant: prevent (R-2026-06-22) @@ -62,8 +64,7 @@ rejects them at validation, naming the offending coordinate. The alternative [cols="1,3",options="header"] |=== | Path | What lives there -| `spec/calculus.adoc` | The normative calculus (source of truth, `:revnumber: 0.1`). -| `spec/calculus-v0.2-draft.adoc` | v0.2 *draft addendum*: the proved grade-algebra obligations `R-2026-06-23-01..04` (non-commutative product monoid; conicality; three-tier cancellation boundary; `Dropped`/`Total` honest). Does not edit v0.1. +| `spec/calculus.adoc` | The normative calculus (source of truth, `:revnumber: 0.2` — consolidated 2026-10-13: ratified carrier, nine effects, O5 defined, O6 opened). | `spec/trope-ir.adoc` | The normative IR spec: nodes, edges, grade algebra, verdict. | `schemas/trope-ir.schema.json` | The Trope IR JSON Schema — the trust boundary (prevent profile). | `src/idris2/` | The executable checker (Idris2): JSON parser + IR decoder + checker, reusing the verified core; plus `Main` → the `tropecheck` binary. @@ -142,15 +143,22 @@ https://github.com/hyperpolymath/trope-checker/tree/8f58d2409227b065fed01a898c02 == Status -Alpha. The schema, executable checker, and conformance suite are green; the -verified core typechecks with no axioms behind its claimed lemmas. The grade-algebra -*honest/deceptive cancellation boundary* is now proved in Lean (sorry-free, -axiom-clean) and its metatheory developed in Agda (Theorem B). Grade soundness (the -full `g ⊑ ρ` theorem) and the *operational model for `fix`/routing* (the central open -problem, CO-1, gated by O4) remain the named open problems in -`docs/status/PROOF-STATUS.adoc`; see `verification/proofs/INTEGRATION-REPORT.adoc` for -the full proved-vs-missing picture. A Rust fast-core is drafted in `src/rust/` -(dep-free, validated against the Idris2 reference via the conformance corpus). +Alpha. The IR schema, the executable checker and the conformance suite are green, +and the verified developments carry no axioms behind their claimed lemmas. On the +ratified carrier (ADR 0004, R-2026-07-07) the grade algebra is a commutative +monoid with the three deceptive bottoms as two-sided zeros; L1–L6, conicality, the +cancellation boundary (left-cancellative iff ε), the Honest Generation and +Veridicality theorems, the atom factorisation (O1's carrier half) and a +veridicality-sighted tropical factorisation are proved across Agda, Idris2 and +Lean; Theorem B gives grade-exact substitution and β/let subject reduction. The +named open problems are *CO-1* — the operational model for `fix` is designed +(`spec/notes/2026-07-07-co1-operational-model.adoc`) and awaits mechanisation, +which is what stands between the exact-lowering soundness already proved and +full grade soundness — plus O2 (per producer), O3, O5's mechanisation, O6 and +O1-coord, all listed in `spec/calculus.adoc §10` with their status. Ground truth: +`AFFIRMATION.adoc`; the proved-vs-open table: `docs/status/PROOF-STATUS.adoc`. The +Rust fast core in `src/rust/` (dependency-free) agrees with the Idris2 reference +over the conformance corpus. == Licence diff --git a/spec/calculus-v0.2-draft.adoc b/spec/calculus-v0.2-draft.adoc deleted file mode 100644 index 03cde08..0000000 --- a/spec/calculus-v0.2-draft.adoc +++ /dev/null @@ -1,410 +0,0 @@ -// SPDX-FileCopyrightText: © 2026 Jonathan D.A. Jewell (hyperpolymath) -// SPDX-License-Identifier: MPL-2.0 -// SPDX-License-Identifier: CC-BY-SA-4.0 -= The Trope-Particularity Calculus — v0.2 grade-algebra addendum (proved obligations) -:revnumber: 0.2-draft -:revdate: 2026-06-23 -:toc: macro -:sectnums: -:sectnumlevels: 2 -:stem: latexmath -:icons: font - -[abstract] -This is a *draft addendum* to the trope-particularity calculus v0.1 -(`spec/calculus.adoc`, `:revnumber: 0.1`). It records, as dated normative -obligations, four facts about the grade algebra that are now *machine-proved* in -the Lean 4 + Mathlib development at `verification/proofs/lean4/grade-boundary/` -(sorry-free; `#print axioms` = `propext`/`Quot.sound` only). The work here is -*documentation only*: the algebra is already established; this document lifts it -into normative spec text and binds each new obligation to its governing theorem. -It does *not* edit v0.1 — it is written as a separate file precisely so the merge -step can diff it against v0.1 — and it neither re-derives the theorems nor reopens -the proved algebra; it binds each fact to its Lean name. v0.1's open obligation -*O1* (completeness of the seven -effects) is untouched and remains open throughout. - -The key words *MUST*, *MUST NOT*, *SHALL*, *SHALL NOT*, *SHOULD*, *MAY*, and -*OPTIONAL* are to be interpreted as in RFC 2119/8174. - -toc::[] - -== Provenance, and what is being recorded (invent nothing) - -The four obligations below are *not* new claims. Each is a lift, in substance, of a -green theorem from the grade-boundary harness, which is itself the single source -of truth for the algebra. The carrier the theorems range over is, exactly: - -* fidelity `Delta = WithTop (WithTop ℕ)` (`dplus = (+)`, unit `Q 0 = 0`); -* `Fate = Present | Atten Delta | Predicated | Dropped | Falsified`; -* `Bond = Intact | Withheld | Severed | Misbound`; -* `Merge = Single | Fused | Conflated`; -* `Grade` = the flat record `Fate⁴ × Bond × Merge`, with *independent* fields. - -[IMPORTANT] -.Two firewalls carried forward in substance from the harness, not to be laundered -==== -. *No Frobenius / cancellative / conical framing exists in v0.1.* A grep of -`calculus.adoc` finds none (its only near-hit, *O3*, is the unrelated -produce/demand *adjunction* conjecture). The obligations below are therefore *new -recordings of proved structure*, not transcriptions of existing v0.1 prose. - -. *"CF" (cancellative + conical ⇒ a lossless special-Frobenius split/merge) is -refuted as universal*, and this document MUST NOT be read as reinstating it. It is -ruled out twice over: by left-absorption of the deceptive bottoms -(R-2026-06-23-03, *L5*, `grade_not_leftCancel`) and, independently, by -non-commutativity of the full operation (R-2026-06-23-01, `grade_mul_not_comm`). -What survives CF's refutation is *cancellation on the finite-fidelity core* -(R-2026-06-23-03) — that algebraic fact alone, and no splitting or merging law, -global or core-local. -==== - -=== Existing numbering recorded (the non-collision basis) - -So that the new ids are demonstrably consistent and non-colliding, v0.1's scheme -is recorded here as it stands at the time of writing: - -[cols="1,3",options="header"] -|=== -| Namespace (v0.1 / siblings) | Meaning, and its status under this addendum - -| `L1`–`L5` (v0.1 §4) | The composition laws. *Untouched.* `L5` is *constrained and - sharpened* by R-2026-06-23-03 (this addendum's §4), not replaced. -| `O1`–`O4` (v0.1 §10) | The open obligations/falsifiers. *Untouched and still open*; - `O1` (seven-effects completeness) in particular is out of scope here. -| `R-2026-06-22` (v0.1 §6.1) | The sole v0.1 decision-log id (the conflation-as-fault - decision). The `R-YYYY-MM-DD` shape is reused below. -| `HC-*`, `L-*` | Reserved by the grade-boundary README for the *separate Agda* - development (Honest Generation; Veridicality). *Not touched, not collided with.* -|=== - -New obligations take the form *`R-2026-06-23-NN`*: the same `R-YYYY-MM-DD` -decision-log prefix as `R-2026-06-22`, with a two-digit sequence suffix that -extends the one-entry-per-date convention to carry several same-date records. -This collides with none of `L\d`, `O\d`, `R-2026-06-22`, `HC-*`, or `L-*`. - -[NOTE] -==== -*Source-of-truth toolchain.* All five primary governing theorems (`instMonoid`, -`grade_mul_not_comm`, `grade_conical`, `grade_not_leftCancel`, -`honest_fidelity_cancel`) are discharged under Lean `v4.16.0` + Mathlib `v4.16.0`, -sorry-free, with `#print axioms` reporting `propext`/`Quot.sound` only — no -`sorryAx`, no user `axiom`, no `native_decide`. The R-id ↔ theorem table in §7 -below (where one R-id binds a pair) is the claims-match-proofs contract; it is the -artifact the merge step keys on. -==== - -== R-2026-06-23-01 — the grade is a *non-commutative* product monoid - -[cols="1,4",options="header"] -|=== -| ID | Obligation (normative) - -| *R-2026-06-23-01* | The grade carrier under composition stem:[\triangleright] is -a *monoid*, formed as the *componentwise product* of its coordinate monoids -(`Fate⁴ × Bond × Merge`); this is the *degenerate-to-product* structure, confirmed -constructively (`instMonoid`). That product *MUST NOT* be assumed commutative: it -is *non-commutative* (`grade_mul_not_comm`). Consequently any algebraic model of -the operation stem:[\triangleright] *MUST* treat it as order-sensitive, and -*SHALL NOT* assume `CommMonoid`, `AddCommMonoid`, or special-Frobenius structure -for it. The non-commutativity is a property of the *full* operation, witnessed by -elements outside the cancellative core (the disagreeing heads `Dropped` and -`Falsified`); special-Frobenius is moreover unavailable across the honest region, -whose non-cancellative honest-but-lossy tier obstructs its comonoid leg -(R-2026-06-23-03). -|=== - -This records v0.1 *L1–L2* (monoid) at full strength while adding the order -discipline v0.1 left implicit. The witness to non-commutativity is intrinsic to -the `Fate` coordinate: it carries *two* distinct left-absorbing heads, `Dropped` -and `Falsified`, which disagree (`Dropped ▷ Falsified = Dropped` but -`Falsified ▷ Dropped = Falsified`), so swapping operands changes the result -(`Fate.not_comm`, lifted to the `fQuality` field by `grade_mul_not_comm`). - -[IMPORTANT] -==== -*Order matters, not merely grade-sum.* Because stem:[\triangleright] is -non-commutative, two effect sequences with the *same multiset* of per-step grades -*MAY* compose to *different* total grades. A checker, an IR producer, or any -optimiser *MUST NOT* reorder effect edges (v0.1 §9) under the assumption that -composition is symmetric. This is the precise sense in which special-Frobenius — -which presupposes a commutative comonoid/monoid interaction — is *unavailable*: -the obstruction is structural (order-sensitivity), independent of, and additional -to, the cancellation obstruction of R-2026-06-23-03. -==== - -== R-2026-06-23-02 — conicality of the full grade - -[cols="1,4",options="header"] -|=== -| ID | Obligation (normative) - -| *R-2026-06-23-02* | The full grade carrier is *conical*: for all grades -stem:[a, b], if stem:[a \triangleright b = \varepsilon] then stem:[a = \varepsilon] -*and* stem:[b = \varepsilon] (`grade_conical`). The unit grade stem:[\varepsilon] -(full presence, intact bond, single merge) *MUST NOT* be treated as reachable -under composition by any pair other than stem:[\varepsilon \triangleright \varepsilon]. -|=== - -Conicality holds on the *entire* carrier (not only the core), and is proved -fieldwise from per-coordinate conicality (`Fate.conical`, `Bond.conical`, -`Merge.conical`). Operationally: no amount of loss can be *manufactured from* the -unit, and the loss-free state cannot be *re-attained* except from itself. A -verdict engine *MAY* rely on this — a final grade of stem:[\varepsilon] -witnesses a genuinely loss-free pipeline, never an accidental cancellation of -losses against gains, because there are no gains. - -== R-2026-06-23-03 — the three-tier cancellation boundary (headline) - -[cols="1,4",options="header"] -|=== -| ID | Obligation (normative) - -| *R-2026-06-23-03* | The carrier is stratified by cancellability into *three -strict tiers*. Write stem:[\mathcal{C}] for the *cancellative core*, -stem:[\mathcal{H}] for the *honest* region, and stem:[\mathcal{G}] for the *full* -carrier. Then the inclusions are *strict*: -stem:[\mathcal{C} \subsetneq \mathcal{H} \subsetneq \mathcal{G}]. *Cancellation -holds ONLY on the finite-fidelity core stem:[\mathcal{C}]* -(`honest_fidelity_cancel`), and *fails everywhere above it* — on the -honest-but-lossy tier and on the deceptive tier alike; the full carrier is -*non-left-cancellative* (`grade_not_leftCancel`). Accordingly, *should* a future -revision introduce a lossless fractional split, rejoin, or routing operator (none -exists today — see OPEN-A), that operator *MUST* be licensed *ONLY* on -stem:[\mathcal{C}], the sole region carrying the cancellation it would rely on; -on stem:[\mathcal{H} \setminus \mathcal{C}] and on -stem:[\mathcal{G} \setminus \mathcal{H}] it *MUST* be treated as lossy and -irreversible, and *MUST NOT* be presented as recoverable. -|=== - -The three tiers, by their inhabitants: - -[cols="1,1,3",options="header"] -|=== -| Tier | Region | Inhabitants and cancellation status - -| *1* | *Cancellative core* stem:[\mathcal{C}] -| The finite-fidelity region — `Atten(Q n)` with stem:[n \in \mathbb{N}], where - `Delta.Q` embeds stem:[(\mathbb{N}, +, 0)] injectively and additively — together - with the coordinate units (`Present`, `Intact`, `Single`). *Cancellation holds* - here and *only* here (`honest_fidelity_cancel`). - -| *2* | *Honest-but-lossy* stem:[\mathcal{H} \setminus \mathcal{C}] -| `Dropped`, `Predicated`, `Severed`, `Withheld`, `Fused`, and `Total` (honest - stem:[\infty]). These are *honest* — they tell no lie about what was lost — yet - they are *non-cancellative* (`Fate.predicated_honest_not_cancel`, - `Bond.severed_honest_not_cancel`, `fidelity_total_honest_not_cancel`; `Withheld` - and `Fused` belong here by the carrier's order structure but carry no individual - witness yet — OPEN-C). Honest loss is still loss: it cannot be undone. - -| *3* | *Deceptive, absorbing bottoms* stem:[\mathcal{G} \setminus \mathcal{H}] -| `Falsified` (fate), `Misbound` (bond), `Conflated` (merge), and `Unknown` - (fidelity). Each is a *left zero* (`Fate.falsified_absorbing`, - `Bond.misbound_absorbing`, `Merge.conflated_absorbing`, - `Delta.unknown_absorbing`): it absorbs everything composed after it, so it - cannot be cancelled back out. This is *L5*. -|=== - -[WARNING] -.Two strict inclusions, two distinct witnesses — do not collapse them -==== -The boundary is *three-tier, not two-tier*: the non-cancellative set is -*strictly larger* than the deceptive set. - -. stem:[\mathcal{C} \subsetneq \mathcal{H}] is witnessed by an *honest* element -that nonetheless fails to cancel — e.g. `Total`, `Severed`, or `Predicated` -(`fidelity_total_honest_not_cancel`, `Bond.severed_honest_not_cancel`, -`Fate.predicated_honest_not_cancel`). "Honest" does *not* imply "cancellative". - -. stem:[\mathcal{H} \subsetneq \mathcal{G}] is witnessed by a *deceptive* element -— e.g. `Falsified` — at which left-cancellation fails outright -(`grade_not_leftCancel`). - -Conflating these two would mis-state the algebra: it would either (wrongly) license -splitting on honest-but-lossy elements, or (wrongly) brand honest loss as -deception. Both are forbidden. -==== - -[IMPORTANT] -.The split / rejoin / routing constraint is a constraint-in-advance -==== -The licensing constraint above is the frozen consequence both the calculus and its -proof harness must respect: any fractional split / rejoin / routing is licensed -*only* on the cancellative core stem:[\mathcal{C}] (tier 1), is order-sensitive -(F2 / R-2026-06-23-01), and is *forbidden* on tiers 2 and 3. The order-sensitivity -attaches to the routing *operation*, not to the internal composition of core -grades: within stem:[\mathcal{C}] the grade product reduces to fidelity addition -(`Delta.Q_add`), which is commutative *and* cancellative, so the core licenses -*both* losslessness and commutative reassembly. It is the operation's general form -— which may move grades between coordinates and tiers — that the order discipline -of R-2026-06-23-01 governs. - -This addendum *defines no split / rejoin / routing operator* — none exists in -v0.1. The obligation here *constrains in advance* any such operator a future -revision may introduce; the operator itself is listed as OPEN-A in §8. -==== - -== R-2026-06-23-04 — partition correction: `Dropped` and `Total` are *honest* - -[cols="1,4",options="header"] -|=== -| ID | Correction (normative, dated for the decision-log) - -| *R-2026-06-23-04* | `Dropped` and `Total` *MUST* be classified as *honest*, not -deceptive. `Dropped` is *honest withholding* — a field withheld entirely, the -clean omission whose *deceptive dual* is the distinct fate `Falsified`. `Total` -is the *honest* stem:[\infty] — total quantified loss — whose deceptive -counterpart is the fidelity bottom `Unknown` (loss of *unknown* amount). -Documentation, taxonomy tables, and tooling *MUST NOT* enumerate `Dropped` or -`Total` in the deceptive tier (tier 3 of R-2026-06-23-03). -|=== - -This correction is recorded explicitly because it *contradicts informal -phrasings* that treat any absorbing or bottom-like element as deceptive. Both -`Dropped` and `Total` are *absorbing* in their coordinate yet *truthful*: -`Dropped` is left-absorbing on `Fate` (`Fate.dropped_absorbing`) while remaining -an honest omission; `Total` absorbs finite fidelity (`Delta.total_add_Q`) and is -itself absorbed only by the deceptive `Unknown` (`Delta.total_add_unknown`), -yet asserts no falsehood. The distinction *absorbing-but-honest* versus -*absorbing-and-deceptive* is the whole reason the boundary is three-tier -(R-2026-06-23-03): it is *precisely* because `Dropped`, `Total`, `Severed`, and -`Predicated` are honest-yet-non-cancellative that "cancellation fails stem:[\iff] -deception" is *false*. - -[NOTE] -==== -*Carrier reconciliation.* The proved `Fate` coordinate has *five* inhabitants — -it includes `Falsified`, the deceptive fate-bottom dual to honest `Dropped`. v0.1 -§3.1's fate table lists only *four* (`Present`, `Attenuated(δ)`, `Predicated(P)`, -`Dropped`) and predates `Falsified`. This addendum records `Falsified` as -established by the carrier; whether v0.1 §3.1 should be amended to introduce it is -a documentation-reconciliation decision for the merge author, logged as OPEN-B -(§8). Nothing here edits v0.1 §3.1. -==== - -== Relationship to the v0.1 obligations - -*R-2026-06-23-03 constrains, and does not replace, L5.* v0.1's *L5* ("conflation -infectiousness": once the merge coordinate is `Conflated`, no composition restores -`Fused` or `Single`) stands unchanged. R-2026-06-23-03 makes L5's irreversibility -*precise* — it is *left-absorption of the deceptive bottom* — and *generalises* it -from the merge coordinate alone to *every* coordinate's deceptive bottom -(`Falsified`, `Misbound`, `Conflated`, `Unknown`), with the full-carrier -consequence `grade_not_leftCancel`. Read together: v0.1's L5 is the merge-coordinate -instance of the general left-absorption fact that R-2026-06-23-03 records. - -*L1–L3 are reinforced; the L4 relationship is sharpened.* R-2026-06-23-01 records -the L1–L2 monoid at full strength and adds the order discipline (non-commutativity) -that L1's associativity alone does not capture. L3 (bottom-absorption) is the -per-coordinate left-absorption that R-2026-06-23-03 makes precise. The tier -stratification, however, is a *cancellation* property and does *not* presuppose the -retention order: strict *L4 monotonicity is only lax — it fails on the fate -coordinate* (machine-proved downstream as `fate-L4-fails`, the same F2×F4 -phenomenon), so tier-preservation is set-membership *closure*, not an -order-homomorphism, and v0.1 §7's appeal to *strict* L4 to justify the `fix` grade -needs the lax/closure route (part of CO-1, below). - -*O1 is untouched and remains open.* v0.1's *O1* — that the seven effects are -*exhaustive* — is a separate completeness question and is *not* addressed, -advanced, or closed here. The algebraic facts recorded in this addendum concern -the *structure of the grade monoid*, not the *enumeration of the effects that -populate it*; the two are orthogonal. O2–O4 are likewise untouched. - -== Interface table — the claims-match-proofs contract - -This table is the keystone artifact: each new obligation is bound *1:1 where -possible* to its governing theorem(s) in -`verification/proofs/lean4/grade-boundary/GradeBoundary.lean` (namespace -`Trope`, sub-namespaces `Trope.Grade`, `Trope.Fate`, `Trope.Bond`, -`Trope.Merge`, `Trope.Delta`). An implementation claiming conformance to an R-id -below *MUST* be checkable against the named theorem(s). - -[cols="1,2,3",options="header"] -|=== -| R-id | Established fact (frozen interface) | Governing Lean theorem(s) - -| *R-2026-06-23-01* | F1 + F2 — non-commutative product monoid -| `Trope.Grade.instMonoid` (degenerate-to-product); `Trope.Grade.grade_mul_not_comm` - (non-commutative). _Coordinate witness:_ `Trope.Fate.not_comm`. - -| *R-2026-06-23-02* | F3 — conicality of the full grade -| `Trope.Grade.grade_conical`. _Fieldwise:_ `Trope.Fate.conical`, - `Trope.Bond.conical`, `Trope.Merge.conical`. - -| *R-2026-06-23-03* | F4 — three-tier strict cancellation boundary -| _Core (cancellation):_ `Trope.Grade.honest_fidelity_cancel`. _Upper inclusion - (L5, non-left-cancellative):_ `Trope.Grade.grade_not_leftCancel`. _Deceptive - left-zeros:_ `Trope.Fate.falsified_absorbing`, `Trope.Bond.misbound_absorbing`, - `Trope.Merge.conflated_absorbing`, `Trope.Delta.unknown_absorbing`. _Honest-but- - lossy witnesses (lower strict inclusion):_ `Trope.Fate.predicated_honest_not_cancel`, - `Trope.Bond.severed_honest_not_cancel`, `Trope.Grade.fidelity_total_honest_not_cancel`. - -| *R-2026-06-23-04* | Partition correction — `Dropped`, `Total` honest -| `Trope.Fate.dropped_absorbing` (honest yet absorbing); `Trope.Grade.fidelity_total_honest_not_cancel` - and `Trope.Delta.total_add_Q`, `Trope.Delta.total_add_unknown` (`Total` honest - yet absorbing, absorbed only by `Unknown`). _Embedding of the honest core:_ - `Trope.Delta.Q_add`, `Trope.Delta.Q_injective`, `Trope.Delta.Q_zero`. -|=== - -R-2026-06-23-01, -02, and -04 are 1:1 on a primary theorem; R-2026-06-23-03 (the -headline) is intrinsically a *pair* of primaries — `grade_not_leftCancel` -(the upper strict inclusion / L5) and `honest_fidelity_cancel` (the core) — with -the absorbing and honest-not-cancel lemmas as supporting witnesses for the two -strict inclusions. - -== OPEN, for author review - -The following surfaced while authoring and are *genuine gaps* that F1–F4 and the -partition correction do *not* settle. In line with the brief, they are *recorded, -not filled*. - -* *OPEN-A — the split / rejoin / routing operator is referenced but undefined.* - R-2026-06-23-03 (and the frozen consequence it records) governs the - cancellability of *fractional split / rejoin / routing*, yet no such operator is - defined in v0.1 or in the grade-boundary harness. The obligation constrains an - operation that does not yet exist. Whether to introduce it — and if so, with what - typing rule — is for author review; until then R-2026-06-23-03 stands as a - *constraint-in-advance*. _Now elevated:_ integrating this addendum with the Agda - metatheory (Theorem B) showed OPEN-A and Theorem B's unreached `fix`/lfp - subject-reduction case to be *one and the same* underspecification — the calculus - defines no operational (reduction) model for its grade-routing / iterating - constructs beyond the β/let core — now tracked as the repository's central open - problem *CO-1* (itself gated by v0.1's O4, the limit carrier). See - `verification/proofs/INTEGRATION-REPORT.adoc` §4 and ADR 0003. - -* *OPEN-B — `Falsified` is absent from v0.1 §3.1.* The proved `Fate` coordinate is - five-ary, but v0.1 §3.1's fate table lists four inhabitants and does not mention - `Falsified` (the deceptive dual of `Dropped`). This addendum records `Falsified` - as carrier-established; whether the eventual v0.2 should amend v0.1 §3.1 to - introduce it normatively — and how that interacts with the v0.1 §6.1 - conflation-as-fault story - for the *fate* coordinate — is a documentation-reconciliation decision, not one - fixed by F1–F4. - -* *OPEN-B′ — `Misbound` is absent from v0.1 §3.2.* Surfaced when this addendum was - swept against the Agda metatheory (Theorem B): the bond coordinate carries a - *deceptive dual* `Misbound` — bond's order-bottom, the dual of honest `Severed` — - exactly as the fate coordinate carries `Falsified`, yet v0.1 §3.2 lists only three - bonds (`Intact`, `Withheld`, `Severed`) and omits it. This is the precise analogue - of OPEN-B for the bond coordinate; merge's deceptive bottom `Conflated` is, by - contrast, already present in v0.1 §3.3. The Idris2 core both enumerates the three - deceptive duals (`Trope.Veridicality.deceptiveDuals` = `(Falsified, Misbound, - Conflated)`) and proves each the *unique* deceptive inhabitant of its coordinate - (`Trope.Veridicality.bondDeceptiveUnique` for `Misbound`). Whether to amend v0.1 - §3.2 is the same documentation-reconciliation decision as OPEN-B, to be taken - together with it. - -* *OPEN-C — tier-2 membership is recorded, not exhaustively proved.* The harness - proves *representative* honest-but-lossy elements non-cancellative (`Predicated`, - `Severed`, `Total`). That `Withheld` and `Fused` also sit in tier 2 (honest, - non-cancellative) is asserted here from the carrier's order structure but is not - individually witnessed by a named theorem in the current harness. Whether to add - those witnesses, or to prove tier-2 membership uniformly, is for author review. - -''' -_Suggested CHANGELOG line:_ `docs: draft trope-particularity calculus v0.2 -addendum (proved grade algebra: non-commutative product monoid [R-2026-06-23-01]; -full-carrier conicality [R-2026-06-23-02]; three-tier strict cancellation boundary, -cancellation only on the finite-fidelity core [R-2026-06-23-03]; Dropped/Total -honest-not-deceptive partition correction [R-2026-06-23-04]; R-id↔Lean-theorem -contract; L5 sharpened not replaced; O1 untouched).` diff --git a/spec/calculus.adoc b/spec/calculus.adoc index 68d87bd..89ba35b 100644 --- a/spec/calculus.adoc +++ b/spec/calculus.adoc @@ -1,9 +1,8 @@ -// SPDX-FileCopyrightText: © 2026 Jonathan D.A. Jewell (hyperpolymath) -// SPDX-License-Identifier: CC-BY-SA-4.0 // SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell = The Trope-Particularity Calculus — a normative core -:revnumber: 0.1 (draft for review) -:revdate: 2026-06-22 +:revnumber: 0.2 (consolidated; ratified carrier R-2026-07-07, ADR 0004; O5 adopted per ADR 0005) +:revdate: 2026-10-13 :toc: macro :sectnums: :sectnumlevels: 2 @@ -14,15 +13,20 @@ This document specifies the type-level discipline of *trope-particularity*: a graded effect system over a Turing-complete term language, in which each operation on a property-instance carries a declared *loss-shape* grade, grades -compose by fixed algebra, and a declared *use-model* yields a decidable verdict. -It pins the loss-shape category, gives the seven effects as typing rules, states -the composition and order laws normatively, fixes the interaction with general -recursion, defines the verdict, states the soundness target with its firewalls, -and defines a language-neutral interchange (the Trope IR) so that a *tropechecker* -can be implemented portably and independently of any one source language. - -The key words *MUST*, *MUST NOT*, *SHALL*, *SHOULD*, *MAY*, and *OPTIONAL* are to -be interpreted as in RFC 2119/8174. +compose by a fixed algebra, and a declared *use-model* yields a decidable +verdict. It pins the loss-shape carrier, names the nine effects of the +vocabulary and gives the six writable ones as typing rules, states the +composition and order laws normatively, fixes the interaction with general +recursion, defines the verdict, states the soundness results with their +firewalls, defines the language-neutral interchange (the Trope IR) so that a +*tropechecker* can be implemented portably, and lists the open obligations. + +This is the v0.2 consolidation: it folds the v0.1 text (2026-06-22), the +grade-algebra addendum (2026-06-23) and the two ratification notes of +2026-07-07 into one normative document. Where a law or result is machine-checked +it is cited by its name in the proof developments (§9.3); where it is open it is +listed in §10. The key words *MUST*, *MUST NOT*, *SHALL*, *SHOULD*, *MAY*, and +*OPTIONAL* are to be interpreted as in RFC 2119/8174. toc::[] @@ -38,7 +42,7 @@ conflating them is itself a modelling error this calculus exists to forbid. | trope-the-valuation | The bottleneck (max–min) grading of a path by its weakest link, with the argmin locating the edge to repair. (The *invariant-path* sense.) Used below - only by analogy, for the verdict witness. + only by analogy, for the verdict witness (§6.2). | trope-the-residual | A residual treated as a sum-typed object rather than a scalar error term, @@ -46,9 +50,12 @@ conflating them is itself a modelling error this calculus exists to forbid. (The *typed-residual* sense.) Reused below as the grade. | *trope-the-particular* -| An *abstract particular* in the sense of Williams and Campbell: a property - considered as a non-repeatable, situated instance — *this* quality, here, - borne by *this* bearer. *This is the object of the present calculus.* +| A *property-instance*: a property considered as a non-repeatable, situated + instance — *this* quality, here, borne by *this* bearer. The classical home + of the notion is trope theory (Williams, Campbell); the calculus needs only + what every instance ontology supplies — that property-instances are + particulars — and not the further theses of any one of them (bundle theory, + one-category ontology). *This is the object of the present calculus.* |=== A classical trope is _quality borne by a bearer_. This calculus works on a @@ -62,7 +69,8 @@ explicitly so that downstream readers do not attribute it to Williams. content_ of a property-instance: how much of its being-this-one-in-this-situation survives an operation. It is *graded and use-relative*, not binary and absolute. Classical particularity is the limiting case where the only admissible verdicts -are "identical" and "not identical"; this calculus refines that to a lattice. +are "identical" and "not identical"; this calculus refines that to a chain per +coordinate. ==== == The object: property-instances @@ -82,40 +90,50 @@ A trope whose quality has been severed from its bearer is a distinct type, `FloatingQuality`, with no bearer field. Collapse of a quality to a predicate yields a non-trope type — the predicate's codomain (typically `Bool`). -== The grade: the loss-shape category +Two of the calculus's constructs are the ones that require property-instances +to be particulars rather than universals: *attenuation* (only an instance can +lose fidelity; a universal is exact) and *detaching* (a quality that survives +severance as a free-standing `FloatingQuality` is an instance with no bearer; +severing a universal from its instance leaves the universal, which was never +_this_). Everything else in the calculus would survive a change of ontology; +these two would not. + +== The grade: the loss-shape carrier A grade records what an operation did to a trope. It is *not a scalar*: two operations can lose the same _amount_ yet differ in _kind_ and in _honesty_. -A grade stem:[g] is a record of three orthogonal coordinates, +A grade stem:[g] is a record of three coordinate *kinds*, [stem] ++++ g \;=\; (\mathsf{fate},\ \mathsf{bond},\ \mathsf{merge}), ++++ -each living in its own lattice. Composition (§4) and the order (§5) act -*componentwise*, which is what keeps the algebra decidable while the term -language stays Turing complete (§7). +where `fate` is itself indexed by the four fields of stem:[\Phi]. A grade +therefore has *six slots* (four fates, one bond, one merge) over *three +coordinate kinds*; both descriptions are used in the stack and mean the same +carrier. Composition (§4) and the order (§5) act *slot-wise*, which is what +keeps the algebra decidable while the term language stays Turing complete (§7). === Coordinate 1 — field fate A *fate* records, per field, what survived. Let stem:[\delta \in \mathbb{N}\cup\{\infty,\top\}] be a fidelity element, where finite stem:[\delta] is a quantified loss in the -tropical (min-plus) order, stem:[\infty] is total quantified loss, and -stem:[\top] is loss of *unknown amount*. +tropical (min-plus) order, stem:[\infty] (`Total`) is total quantified loss, +and stem:[\top] (`Unknown`) is loss of *unknown amount*. [cols="1,3",options="header"] |=== | Fate | Reading -| `Present` | The field survives faithfully. (Lattice top.) -| `Attenuated(δ)` | Survives, fidelity degraded by stem:[\delta]. `Attenuated(0) = Present`. +| `Present` | The field survives faithfully. (Chain top.) +| `Attenuated(δ)` | Survives, fidelity degraded by stem:[\delta]. `Attenuated(0)` is identified with `Present` by normalization (A3, below). | `Predicated(P)` | (`quality` only.) Survives *only* as the value of predicate `P` over it — the checkbox. | `Dropped` | Withheld entirely. (Honest bottom.) -| `Falsified` | *Deceptive dual:* a value asserted faithful that is in fact false. (Lattice bottom; fails every honest floor. Not writable in source — a lowering fault, §6.) +| `Falsified` | *Deceptive dual:* a value asserted faithful that is in fact false. (Chain bottom; fails every honest floor. Not writable in source — a lowering fault, §6.) |=== -The fate order is a *chain* (R-2026-07-07 (A2); originally a lattice with a +The fate order is a *complete chain* (R-2026-07-07 (A2); v0.1 had a `Predicated ∥ Dropped` antichain): [stem] @@ -127,7 +145,7 @@ The fate order is a *chain* (R-2026-07-07 (A2); originally a lattice with a `Present` is top; `Attenuated(δ)` decreases as stem:[\delta] increases; `Predicated(P)` sits below every attenuation and above `Dropped` — a checkbox -retains at least as much of the quality as nothing at all. What the original +retains at least as much of the quality as nothing at all. What the v0.1 incomparability protected is preserved: a use-model needing the full quality rejects both `Predicated(P)` and `Dropped`; a use-model needing only the predicate accepts `Predicated(P)` but rejects `Dropped`. @@ -135,12 +153,16 @@ predicate accepts `Predicated(P)` but rejects `Dropped`. [NOTE] ==== *Ratification record (R-2026-07-07, ADR 0004; analysis in -`spec/notes/2026-07-07-l4-boundary-and-atoms.adoc`).* (A2) `Dropped ⊑ -Predicated` dissolves the antichain — one of the two machine-proved sources of -L4 failure — and makes the fate order a complete chain. (A3) the -`Attenuated(0) = Present` identification is *imposed by normalization at IR -ingest* (validators rewrite `Attenuated(Q 0)` to `Present`; composition -preserves normal forms), so carrier datatypes stay as-is. +`spec/notes/2026-07-07-l4-boundary-and-atoms.adoc`).* (A1) each deceptive +bottom is a *two-sided* zero of its coordinate's composition — in particular +`Dropped ▷ Falsified = Falsified`, replacing the v0.1 clause +`Dropped ▷ Falsified = Dropped` that let an upstream honest drop erase a +downstream lie and was the sole source of the algebra's non-commutativity. +(A2) `Dropped ⊑ Predicated`, dissolving the antichain. (A3) `Attenuated(0) = +Present` is *imposed by normalization at IR ingest*: validators rewrite +`Attenuated(Q 0)` to `Present` before grading, and composition preserves normal +forms (finite tropical addition reaches 0 only from 0+0), so carrier datatypes +stay as-is and stored and composed grades are normal forms. ==== `Predicated` is well-formed *only* on the `quality` field. A grade asserting @@ -157,15 +179,18 @@ The *bond* records the constitutive quality–bearer tie. | `Intact` | Bearer present, tie holds. (Top.) | `Withheld` | Bearer field dropped by projection; tie *recoverable in principle*. | `Severed` | Tie cut, quality asserted free-standing; *irrecoverable*. (Honest bottom.) -| `Misbound` | *Deceptive dual:* the quality presented as borne by a bearer that is not in fact its bearer. (Lattice bottom; fails every honest floor. Not writable in source — a lowering fault, §6.) +| `Misbound` | *Deceptive dual:* the quality presented as borne by a bearer that is not in fact its bearer. (Chain bottom; fails every honest floor. Not writable in source — a lowering fault, §6.) |=== -Ordered `Intact ⊐ Withheld ⊐ Severed ⊐ Misbound`. The distinction between `Withheld` and -`Severed` is the whole content of detaching versus projecting-away-the-bearer: -both leave no bearer, but the former is a clean named drop and the latter is a -constitutive severance. *This distinction surfaces in the type, not only the -grade* — detaching changes `Trope[S]` to `FloatingQuality`, so any downstream -operation needing a bearer fails to typecheck. +Ordered `Intact ⊐ Withheld ⊐ Severed ⊐ Misbound`. The distinction between +`Withheld` and `Severed` is the whole content of detaching versus +projecting-away-the-bearer: both leave no bearer, but the former is a clean +named drop and the latter a constitutive severance. *This distinction surfaces +in the type, not only the grade* — detaching changes `Trope[S]` to +`FloatingQuality`, so any downstream operation needing a bearer fails to +typecheck. The bond coordinate is *fibred over the bearer's fate* (HC-4): a +grade with the bearer `Present` and the bond `Severed`, or the bearer absent and +the bond `Intact`, is incoherent and unrepresentable at the validation boundary. === Coordinate 3 — merge (cardinality and honesty) @@ -184,17 +209,18 @@ honestly. Ordered `Single ⊐ Fused(τ) ⊐ Conflated` by recoverable plurality. `Conflated` is the *deceptive* collapse — the tag that would reveal the merge is discarded, so downstream is silently wrong about at least one constituent; `Fused(τ)` is -the *faithful* collapse. This is precisely the faithful/deceptive veridicality -axis of the typed-residual framework, instantiated on cardinality. +the *faithful* collapse. This is the faithful/deceptive veridicality axis of +the typed-residual framework, instantiated on cardinality. [IMPORTANT] ==== -*`Conflated` is reachable in the grade lattice but not by well-formed terms.* -The lattice is complete — it has its bottom — because the soundness story and the -use-model order require it as a formal element, and because a front end that -lowers some source operation to an untagged merge must have its output *named* -as `Conflated` when the validator rejects it (§6, §9). But no well-formed term -of the source language produces it: see the conflation decision in §6. +*`Conflated` is reachable in the grade carrier but not by well-formed terms.* +The carrier is complete — it has its bottom — because the soundness story and +the use-model order require it as a formal element, and because a front end +that lowers some source operation to an untagged merge must have its output +*named* as `Conflated` when the validator rejects it (§6, §9). But no +well-formed term of the source language produces it: see the conflation +decision in §6.1. ==== === The unit @@ -208,69 +234,151 @@ The unit grade is — full presence on every field, intact bond, no merge. `preserve` introduces it. +=== The nine effects and the nine atom families + +The vocabulary (`trope-particularity-workbench`) names *nine* effects. The +calculus realises them as follows. An *atom* is a grade that differs from +stem:[\varepsilon] in exactly one slot; atoms come in nine families, one per +non-unit coordinate value kind, and *every grade factors as a ▷-product of its +single-slot projections* (`EffectAtoms.lean`: `atom_factorization`, +`nine_families`, `family_realized`, `families_disjoint` — this is O1's +carrier-relative half, §10). + +[cols="2,1,1,2,1",options="header"] +|=== +| Vocabulary effect | Coordinate | Value | Calculus status | Veridicality + +| `p-preserving` | — | stem:[\varepsilon] | writable (`preserve`) | faithful +| `p-projecting` | fate / bond | `Dropped` / `Withheld` | writable (`project[S]`); composite of the `drop` atoms | faithful +| `p-collapsing` | fate | `Predicated(P)` | writable (`collapse[P]`); composite of `predicate` + `drop` | faithful +| `p-detaching` | bond | `Severed` | writable (`detach`); composite of `sever` + `drop` | faithful +| `p-attenuating` | fate | `Attenuated(δ)` | writable (`attenuate[δ]`); the `attenuate` atom | faithful +| `p-fusing` | merge | `Fused(τ)` | writable (`fuse[τ]`); the `fuse` atom | faithful +| `p-falsifying` | fate | `Falsified` | *not writable* — validation fault | deceptive +| `p-misbinding` | bond | `Misbound` | *not writable* — validation fault | deceptive +| `p-conflating` | merge | `Conflated` | *not writable* — validation fault (R-2026-06-22) | deceptive +|=== + +Two structure theorems fix this table rather than leaving it a list: + +* *Honest Generation.* The five atomic moves `attenuate`, `predicate`, `drop`, + `sever`, `fuse` together with stem:[\varepsilon] generate exactly the honest + fragment of each coordinate, and never produce a deceptive dual + (`Trope.Generation.{genFate,genBond,genMerge}`; Agda `TB.Honest.genFate` etc., + `honest-closed-▷`). +* *Veridicality Derivation.* The deceptive fragment has exactly three + inhabitants, one per coordinate kind — `Falsified`, `Misbound`, `Conflated` — + each the unique deceptive element of its coordinate + (`Trope.Veridicality.{fate,bond,merge}DeceptiveUnique`; Agda + `TB.Honest.{fate,bond,merge}DeceptiveUnique`). One cannot deceptively assert + a loss; the only deceptions are false value, false bearer, false singleness. + +So "seven effects" (six writable plus the conflation fault), which earlier +versions of this document used, and "nine effects" (the vocabulary) describe the +same carrier: nine atom families, of which six are writable surface effects +and three are faults. This document uses *nine* throughout. + == Composition and order — the normative laws === Composition Sequencing two effects (apply the second to the residual of the first) composes -grades by stem:[\triangleright], defined componentwise. +grades by stem:[\triangleright], defined slot-wise. -*Fate composition* (per field), the partial operation stem:[f_1 \triangleright f_2]: +*Fate composition* (per field), stem:[f_1 \triangleright f_2], on the ratified carrier: [source] ---- Present ▷ f = f f ▷ Present = f -Attenuated(δ₁) ▷ Attenuated(δ₂)= Attenuated(δ₁ + δ₂) -- tropical: losses add -Attenuated(_) ▷ Predicated(P) = Predicated(P) -- collapse subsumes prior fidelity loss -Attenuated(_) ▷ Dropped = Dropped +Attenuated(δ₁) ▷ Attenuated(δ₂)= Attenuated(δ₁ + δ₂) -- tropical: losses add; ⊤ absorbs ∞ absorbs finite +Attenuated(_) ▷ Predicated(P) = Predicated(P) -- collapse subsumes prior fidelity loss (and symmetrically) +Attenuated(_) ▷ Dropped = Dropped -- (and symmetrically) Predicated(_) ▷ Predicated(Q) = Predicated(Q) -- predicate of the bit; rare, defined for totality -Predicated(_) ▷ Dropped = Dropped -Dropped ▷ _ = Dropped -- nothing further can be lost from nothing +Predicated(_) ▷ Dropped = Dropped -- (and symmetrically) +Dropped ▷ Dropped = Dropped +Falsified ▷ _ = Falsified -- two-sided zero (A1) +_ ▷ Falsified = Falsified ---- -*Bond composition* — meet in `Intact ⊐ Withheld ⊐ Severed`, `Severed` absorbing. -*Merge composition* — meet in `Single ⊐ Fused ⊐ Conflated`, with -`Fused(τ₁) ▷ Fused(τ₂) = Fused(τ₁ ⊗ τ₂)` (nested honest merge, label is the -pair), and `Conflated` absorbing. +*Bond composition* — meet in `Intact ⊐ Withheld ⊐ Severed`, with `Misbound` a +two-sided zero. *Merge composition* — meet in `Single ⊐ Fused ⊐ Conflated`, +with `Fused(τ₁) ▷ Fused(τ₂) = Fused(τ₁ ⊗ τ₂)` (nested honest merge, label is the +pair) and `Conflated` a two-sided zero. -The laws stem:[g] must satisfy, to be enforced by the verified core (§8): +The laws the grade MUST satisfy, each enforced by the verified developments (§9.3): [cols="1,4",options="header"] |=== | ID | Law -| *L1 (associativity)* | stem:[(g_1 \triangleright g_2)\triangleright g_3 = g_1 \triangleright (g_2 \triangleright g_3)]. -| *L2 (unit)* | stem:[\varepsilon \triangleright g = g = g \triangleright \varepsilon]. -| *L3 (bottom-absorption)* | In each coordinate, the *deceptive* lattice bottom is a *two-sided zero* of that coordinate's composition (R-2026-07-07 (A1)): `Falsified`, `Misbound`, and `Conflated` absorb from both sides — no honest absorber launders deception. The *honest* bottoms (`Dropped`, `Severed`) absorb from the left *within the honest fragment*, and `Attenuated(⊤)` is absorbing within the fidelity dimension. -| *L4 (monotonicity)* | stem:[\triangleright] is monotone in each argument w.r.t. the retention order stem:[\sqsubseteq] (§5). Composing after more loss never yields more retention. (*Holds in full on the ratified carrier* — R-2026-07-07 (A1)+(A2) removed the two machine-proved failure points of the original v0.1 carrier, the `Predicated ∥ Dropped` antichain and the `Dropped ▷ Falsified` clause; the §7 least-fixed-point argument is thereby restored. History and proofs: `spec/notes/2026-07-07-l4-boundary-and-atoms.adoc`, `verification/proofs/lean4/grade-boundary/L4Monotonicity.lean`.) -| *L5 (conflation infectiousness)* | Once the merge coordinate is `Conflated`, no composition restores `Fused` or `Single`. (A corollary of L3, stated separately because it is the non-compositionality-of-deceptive-channels result and the moral core.) +| *L1 (associativity)* | stem:[(g_1 \triangleright g_2)\triangleright g_3 = g_1 \triangleright (g_2 \triangleright g_3)]. (`Trope.Laws.gradeAssoc`; Agda `gmonoid-assoc`; Lean `GradeR.instCommMonoid`.) +| *L2 (unit)* | stem:[\varepsilon \triangleright g = g = g \triangleright \varepsilon]. (`Trope.Grade.{gradeUnitL,gradeUnitR}`; Agda `gmonoid-unit{L,R}`.) +| *L3 (bottom-absorption)* | Each *deceptive* bottom — `Falsified`, `Misbound`, `Conflated`, and fidelity's `Unknown` — is a *two-sided zero* of its coordinate's composition (R-2026-07-07 (A1)): no honest absorber launders deception, in either composition order. (Lean `FateA.falsified_two_sided_zero`, `GradeR.gBotR_two_sided_zero`; Agda `falsified-absorb{L,R}`, `misbound-absorbL`, `conflated-absorbL`, `deceptive-absorbs-▷`.) The *honest* bottoms (`Dropped`, `Severed`) absorb within the honest fragment, and `Attenuated(⊤)` within the fidelity dimension. +| *L4 (monotonicity)* | stem:[\triangleright] is monotone in each argument with respect to the retention order stem:[\sqsubseteq] (§5): composing after more loss never yields more retention. *Holds in full on the ratified carrier.* (Idris2 `Trope.Soundness.{fateL4MonoR,fateL4MonoL}`, `Trope.Order.{bondComposeMono,mergeComposeMono}`; Lean `FateA.comp_mono_{right,left}`; Agda `TB.Order.fateL4Mono{R,L}`.) History: strict L4 failed on the v0.1 carrier at exactly the two points (A1)/(A2) amended — `spec/notes/2026-07-07-l4-boundary-and-atoms.adoc`, `L4Monotonicity.lean` (`comp_not_monotone_{right,left}`, retained as theorems about the pre-ratification carrier). +| *L5 (deception infectiousness)* | Once any coordinate is at its deceptive bottom, no composition restores an honest value. A corollary of L3, stated separately because it is the non-compositionality-of-deceptive-channels result and the moral core; it covers `Conflated` (v0.1's statement), `Falsified` and `Misbound` alike. +| *L6 (commutativity)* | stem:[g_1 \triangleright g_2 = g_2 \triangleright g_1]. New at v0.2: on the ratified carrier the grade monoid is *commutative* (Lean `GradeR.instCommMonoid`, `FateA.comp_comm`; Agda `grade-comm`). The v0.1 non-commutativity (`GradeBoundary.grade_mul_not_comm`) was an artefact of the clause (A1) removed. Order-sensitivity, where a producer wants it, MUST come from DAG structure (§9.1), never from stem:[\triangleright]. |=== [NOTE] ==== -L1–L2 make stem:[(\text{grades}, \triangleright, \varepsilon)] a monoid, hence -the effect system is a *graded monad* on the term category with this monoid as -its grade object. L4 makes the order a *lax* compatibility, which is what the -verdict subsumption (§5, §6) needs. None of L1–L5 is novel as a _shape_; the -content is that the three-coordinate loss-shape monoid is the right grade object -for trope-particularity, which §10-O1 marks as the open completeness question. +L1–L2 make stem:[(\text{grades}, \triangleright, \varepsilon)] a monoid, L6 a +commutative one; the effect system is a *graded monad* on the term category +with this monoid as its grade object. L4 is what the verdict subsumption +(§5–§6) and the recursion rule (§7) need. None of L1–L6 is novel as a _shape_; +the content is that this carrier is the right grade object for +trope-particularity, which §10-O1 marks as the open adequacy question. ==== +=== The cancellation structure + +Three further facts about the carrier are normative because downstream designs +(splitting, rejoining, any cut) must respect them (R-2026-06-23-02..04, as +amended by R-2026-07-07): + +[cols="1,4",options="header"] +|=== +| ID | Fact + +| *C1 (conicality)* | stem:[g_1 \triangleright g_2 = \varepsilon \Rightarrow g_1 = g_2 = \varepsilon]: nothing lossy composes back to no-loss. (Lean `GradeR.conical`, `FateA.conical`; Agda `grade-conical`.) +| *C2 (the cancellation boundary)* | Cancellation holds *only* on the finite-fidelity core stem:[\mathcal{C}] (the additive submonoid `Q ℕ ≅ (ℕ,+,0)` of the fidelity dimension) and fails on the honest-but-lossy and deceptive tiers alike: an element of the grade monoid is left-cancellative *iff* it is stem:[\varepsilon]. (Lean `Grade.grade_leftCancel_iff`, `GradeR.gradeR_leftCancel_iff`, with the per-element witnesses of `TierTwoComplete.lean`; Agda `TB.Tier.Q-cancelʳ` and the six `*-not-cancel` lemmas.) Consequence: a lossless *split / rejoin* can be cancellative only inside stem:[\mathcal{C}]; any such operator (§10, CO-1) MUST be stated against this boundary. +| *C3 (partition)* | `Dropped`, `Total` (stem:[\infty]), `Severed`, `Predicated`, `Withheld` and `Fused` are *honest* non-cancellative elements; `Falsified`, `Misbound`, `Conflated` and `Unknown` (stem:[\top]) are the *deceptive* ones. Absorbing is not the same as lying. (Lean `dropped_absorbing`, `fidelity_total_honest_not_cancel`; Agda `TB.Tier` classifiers.) Tier preservation under composition is *closure*, not a homomorphism: `tierOf (g ▷ h) = tierOf g ⊓ tierOf h` is false on fate even on the ratified carrier (`TB.Tier.fate-tier-meet-hom-fails`). +|=== + +=== The tropical factorisation + +A nontrivial monoid homomorphism stem:[\pi_R : (\mathrm{GradeR}, \triangleright, \varepsilon) \to (\Delta, +, Q\,0)] +onto the commutative tropical fidelity carrier exists and is +*veridicality-sighted*: `Dropped ↦ ∞` and `Falsified ↦ ⊤`, so the hom is blind +to *which honest* absorber acted but not to *whether the absorber was honest* +(`GradeFactorisationR.lean`: `piR_hom`, `piR_nontrivial`, `piR_surjective`, +`piR_sighted`). The naive hom that reads the attenuation payload off verbatim is +*not* a homomorphism on the ratified carrier (`phiId_not_hom`); the repair +squashes `Unknown` to the deceptive top. On the v0.1 carrier every such hom was +forced to collapse `Dropped` with `Falsified` (`GradeFactorisation.lean`, +`forced_collapse_general`) — a theorem about the pre-ratification carrier only. +This factorisation is a *precondition*, not a recursion result: whether a +fixpoint's grade lives in the commutative part is a CO-1 question (§10). + === The retention order and use-models Define stem:[\sqsubseteq] as the *retention order*: stem:[x \sqsubseteq y] means "stem:[y] retains at least as much particularity as stem:[x]" — i.e. stem:[y] is -higher (less lossy) in every coordinate lattice. stem:[\sqsubseteq] is the -componentwise product order; it is decidable because each coordinate lattice has -decidable order (finite, except the fidelity dimension stem:[\mathbb{N}\cup\{\infty,\top\}], -which is a decidable linear order with two adjoined tops). +higher (less lossy) in every slot. stem:[\sqsubseteq] is the slot-wise product +order; it is decidable because each coordinate is a decidable chain (the +fidelity dimension stem:[\mathbb{N}\cup\{\infty,\top\}] is a decidable linear +order with two adjoined tops). (`Trope.Laws.decGradeLte`; reflexivity and +transitivity in `Trope.Coords`/`Trope.Order`, `gradeLteTrans`.) A *use-model* stem:[U] declares a *floor* stem:[\mathrm{floor}(U)] — the minimum -retained particularity the use requires, possibly specified per field. The floor +retained particularity the use requires, possibly specified per slot. The floor is data the author *declares*; it is the only place a use enters the calculus. +The floor is a partial per-slot demand, not a grade value; HC-4 coherence is +enforced on edge grades, and an author MAY write an incoherent floor (each +demanded slot is then checked independently — harmless, but an author-error +surface, not covered by the unrepresentability claim). -== The seven effects as typing rules +== The six writable effects as typing rules The typing judgement is @@ -283,8 +391,8 @@ The typing judgement is types carry latent grade: stem:[A \xrightarrow{g} B] is "applying produces loss stem:[g]." The structural rules (variable, abstraction, application, `let`, `fix`) are standard; `let` is where composition enters and `fix` is in §7. The -six *writable* effects and the subsumption rule follow. (The seventh, -conflation, is treated in §6.1.) +six *writable* effects and the subsumption rule follow; the three deceptive +duals are not term formers (§6.1). .T-Preserve [%hardbreaks] @@ -346,13 +454,14 @@ leaves `bond` and `merge` unchanged. .... Γ ⊢ e₁ : A ! g₁ Γ ⊢ e₂ : A ! g₂ ───────────────────────────────────────────────────── -Γ ⊢ fuse[τ] e₁ e₂ : A ! (g₁ ⊔ g₂) ▷ label(τ) +Γ ⊢ fuse[τ] e₁ e₂ : A ! (g₁ ⊓ g₂) ▷ label(τ) .... where `label(τ)` sets `merge = Fused(τ)`, fates `Present` (the labelled blend is -faithful), `bond` the meet of the inputs'. The `⊔` joins the two input grades -(the fused value is no better than its worse constituent in any coordinate). The -tag `τ` is *required*: a fusion term with no tag does not parse (§6.1). +faithful), `bond` the meet of the inputs'. The stem:[\sqcap] meets the two input +grades in the retention order (the fused value is no better than its worse +constituent in any slot). The tag `τ` is *required*: a fusion term with no tag +does not parse (§6.1). .T-Sub — conservative weakening: you MAY always claim more loss than occurred [%hardbreaks] @@ -364,40 +473,44 @@ tag `τ` is *required*: a fusion term with no tag does not parse (§6.1). [NOTE] ==== -T-Sub weakens *downward* in retention only. Claiming *less* loss than occurred is -unsound and has no rule. This one-sidedness is what makes the verdict (§6) a -safe over-approximation. +T-Sub weakens *downward* in retention only. Claiming *less* loss than occurred +is unsound and has no rule. This one-sidedness is what makes the verdict (§6) a +safe over-approximation — and it is also why the calculus, as it stands, +certifies *sufficiency* (enough retained) and not *discretion* (no more than a +ceiling retained): a declared grade is a lower bound on retention, never an +upper bound. A ceiling verdict needs the dual theorem (§10, O6). ==== == The conflation decision, and the verdict -=== Decision: conflation is not a source primitive +=== Decision: deception is not a source primitive [cols="1,4",options="header"] |=== | ID | Decision (dated, for the decision-log) -| *R-2026-06-22* | Conflation SHALL NOT be a writable primitive. `fuse[τ]` *requires* a tag; an untagged merge is a syntax error and does not elaborate. `Conflated` exists only as the absorbing bottom of the merge coordinate (§3.3); a well-formed term never produces it. Conflation therefore arises *only* as a *lowering fault*: when a front end lowers a source operation to a merge and fails to supply a tag, the resulting IR is malformed and the validator (§9) rejects it, *naming* the offending node's merge as `Conflated`. The tropechecker is, operationally, a *conflation detector at the lowering boundary*. +| *R-2026-06-22* | Conflation SHALL NOT be a writable primitive. `fuse[τ]` *requires* a tag; an untagged merge is a syntax error and does not elaborate. `Conflated` exists only as the absorbing bottom of the merge coordinate (§3.3); a well-formed term never produces it. Conflation therefore arises *only* as a *lowering fault*: when a front end lowers a source operation to a merge and fails to supply a tag, the resulting IR is malformed and the validator (§9) rejects it, *naming* the offending node's merge as `Conflated`. The same holds, by construction, for `Falsified` and `Misbound` (the validator rejects them as not writable in the *prevent* profile). The tropechecker is, operationally, a *deception detector at the lowering boundary*. |=== This is the door-too-small reading: the dangerous state exists in the semantics but is structurally unreachable by well-formed terms. It makes the moral content -— _do not silently merge particulars_ — a validation error rather than a -guideline. +— _do not silently merge particulars, do not misattribute, do not substitute_ — +a validation error rather than a guideline. [IMPORTANT] -.Normative variant (conflation as a verdict-boundary primitive) +.Normative variant (deception as a verdict-boundary primitive) ==== Implementations MAY instead admit conflation as a writable primitive caught at the verdict rather than at validation. Exactly three things change, and nothing else: -. *Add* a rule `T-Conflate : Γ ⊢ e₁ : A ! g₁, Γ ⊢ e₂ : A ! g₂ ⟹ Γ ⊢ conflate e₁ e₂ : A ! (g₁ ⊔ g₂) ▷ unlabel`, where `unlabel` sets `merge = Conflated`. +. *Add* a rule `T-Conflate : Γ ⊢ e₁ : A ! g₁, Γ ⊢ e₂ : A ! g₂ ⟹ Γ ⊢ conflate e₁ e₂ : A ! (g₁ ⊓ g₂) ▷ unlabel`, where `unlabel` sets `merge = Conflated`. . *Relax* T-Fuse so an untagged merge is well-formed and elaborates to `conflate`. . *Move* the conflation check from the validation boundary (§9) to the verdict (§6.2): a `Conflated` grade is then rejected only when `floor(U)` demands `merge ⊒ Fused`. The recommended reading (R-2026-06-22) is _prevent_; the variant is _detect_. -An implementation MUST pick one and state which in its conformance profile. +An implementation MUST pick one and state which in its conformance profile. The +reference and fast cores ship *prevent*. ==== === The verdict @@ -412,7 +525,7 @@ Given a closed program with final grade stem:[g] and a use-model stem:[U]: If the check fails, the verdict is `p-insufficient`, and the report MUST carry a *witness*: the operation (DAG edge, §9) whose composition first pushed the -running grade below stem:[\mathrm{floor}(U)] in some coordinate. This witness is +running grade below stem:[\mathrm{floor}(U)] in some slot. This witness is the trope-particularity analogue of the invariant-path argmin — it names the edge to repair, not merely that repair is needed. @@ -430,57 +543,74 @@ comonad form an adjunction whose unit/counit are exactly produce/demand is a == General recursion, and why it does not break the checker -`fix` is what makes the term language Turing complete. Its grade rule takes the -*least fixed-point grade* of the body's grade functional: +`fix` is what makes the term language Turing complete. Its grade is the +*tightest declaration the rule can certify*: in the retention order, the +*greatest post-fixed point* of the body's grade functional (equivalently, the +least fixed point in the loss order — v0.1's phrasing). The functional +stem:[F(\gamma)] — the body's derived latent grade under the assumption that the +recursive binder has latent grade stem:[\gamma] — is computable, and monotone in +stem:[\gamma] by L4; each coordinate is a complete chain; so Knaster–Tarski gives +stem:[\mathrm{gfp}\,F = \bigsqcup\{\gamma : \gamma \sqsubseteq F(\gamma)\}]. -[%hardbreaks] -.... -Γ, x : (A ─g→ B) ⊢ e : (A ─g→ B) g = lfp(λγ. grade-of(e)[γ]) -───────────────────────────────────────────────────────────────── -Γ ⊢ fix x. e : (A ─g→ B) ! ε -.... +*The rule (T-Fix-Decl).* The author declares stem:[\gamma]; the checker accepts +iff + +[stem] +++++ +\gamma \;\sqsubseteq\; F(\gamma) +++++ -The least fixed point exists because each coordinate lattice is complete and, by -*L4*, the grade functional is monotone. A recursive trope-transformer that can -attenuate without bound has fidelity grade stem:[\top] — and that is *correct*, -not a failure: an unbounded loop of lossy steps yields an unknown residual, the -checker reports stem:[\top], and any use-model demanding better than stem:[\top] -rejects it. +— decidable (stem:[F] is computable on grades, stem:[\sqsubseteq] is +decidable), and no fixed point is ever computed. Kleene iteration and +ω-continuity are not needed: existence by Knaster–Tarski, checking by the +post-fixed-point test, soundness by induction on call depth of a terminating +run (`spec/notes/2026-07-07-co1-operational-model.adoc` §4). + +A recursive trope-transformer that can attenuate without bound has fidelity +grade stem:[\top] — and that is *correct*, not a failure: no finite-δ +signature is a post-fixed point, the strongest accepted signatures sit at +`Attenuated(∞)`/`Attenuated(⊤)`, the checker reports stem:[\top], and any +use-model demanding better rejects it. [IMPORTANT] ==== *Turing-completeness does not break the checker; it means some grades are stem:[\top], and stem:[\top] is an honest answer.* The checker stays total -because it computes on the grade lattice, never on the term. The undecidability +because it computes on the grade carrier, never on the term. The undecidability that Rice's theorem guarantees is discharged honestly into the stem:[\top] -element, exactly as the Aletheia design discharges it into an honest "cannot -guarantee." +element. ==== *Inference versus checking.* Synthesising the minimal grade of an arbitrary fixpoint is undecidable. The checker SHALL therefore be *bidirectional*: grades are *checked* against *declared* loss-signatures at every recursive and effectful -boundary (the author annotates the loss signature of a recursive -trope-transformer, as one annotates an effect signature), and *inferred* only -through the straight-line, non-recursive fragment (decidable, convenient). -Declared signatures at the boundaries; inference in between. +boundary, and *inferred* only through the straight-line, non-recursive fragment. +Declared signatures at the boundaries; inference in between. The T-Fix-Decl side +condition is an obligation of the *front end* at its recursive boundaries; the +IR checker sees only the declared signature. + +*Status.* The operational model this section relies on — the core language +λ-trope, its instrumented small-step semantics with tagged values, and observed +retention stem:[\rho] read off the output tag — is DESIGNED +(`spec/notes/2026-07-07-co1-operational-model.adoc`). Its mechanisation is OPEN +(§10, CO-1): Theorem B's `fix` case is NOT-REACHED and not postulated. == Soundness, and the firewalls Let stem:[\rho(\text{in}, \text{out})] be the *observed retention* of one -execution: the grade read off by comparing the input and output trope records. -The verified core (§9) targets: +execution: the grade read off by comparing the input and output trope records +(in λ-trope, the output value's tag). The results, with their status: -[cols="1,4",options="header"] +[cols="1,4,1",options="header"] |=== -| ID | Statement +| ID | Statement | Status -| *Grade soundness* | If stem:[\Gamma \vdash e : A \mathbin{!} g] then for every well-typed input, stem:[g \sqsubseteq \rho(\text{in}, \text{out})]: the declared grade never claims more retention than the execution delivers (equivalently, it over-approximates loss). -| *Verdict soundness* (corollary) | If the checker reports `p-sufficient` (i.e. stem:[\mathrm{floor}(U)\sqsubseteq g]) then by transitivity stem:[\mathrm{floor}(U)\sqsubseteq \rho], so the real residual meets the use-model. +| *Grade soundness* | If stem:[\Gamma \vdash e : A \mathbin{!} g] then for every well-typed input, stem:[g \sqsubseteq \rho(\text{in}, \text{out})]: the declared grade never claims more retention than the execution delivers (it over-approximates loss). | *Exact lowering:* PROVED (`Trope.Soundness.soundFromExact`). *β/let core:* PROVED, with the grade preserved exactly (Agda `TB.Reduction`, `TB.Substitution.cut-preserves-grade`). *Conservative lowering and `fix`:* OPEN — CO-1 mechanisation (§10). +| *Verdict soundness* (corollary) | If the checker reports `p-sufficient` (i.e. stem:[\mathrm{floor}(U)\sqsubseteq g]) then by transitivity stem:[\mathrm{floor}(U)\sqsubseteq \rho], so the real residual meets the use-model. | PROVED, given grade soundness (`Trope.Soundness.verdictSound`; `subSound` for T-Sub). |=== [WARNING] -.Two firewalls — state both, do not let the theorem launder them +.Three firewalls — state all three, do not let the theorems launder them ==== . *Soundness, not completeness.* The checker MAY be conservative: it MAY report `p-insufficient` where the true residual would in fact have sufficed. This is the @@ -490,9 +620,13 @@ safe direction and is acceptable. No completeness is claimed. *IR-level* grades. It does *not* prove that a front end's claim "this source operation _is_ a `collapse[P]`" is true. *Lowering correctness is a separate, per-front-end proof obligation* (§10-O2) and is NOT discharged by this theorem. -This is the same firewall as "the analogy is not an instance": the core's -guarantee is conditional on faithful lowering, and that conditionality lives in -the spec, in the open, not hidden in a footnote. + +. *Veridicality is declared and propagated, not checked.* The checker cannot +decide whether a value claimed faithful is in fact false; that needs ground +truth the IR does not carry. What the calculus guarantees instead is L3/L5: +deceptive grades are two-sided zeros, do not compose away, and fail every honest +floor. The precise statement, and the interface a deployment may bind to do +better, is §10-O5. ==== == The portable tropechecker @@ -502,7 +636,7 @@ depends only on a language-neutral interchange. === The Trope IR -The portable artifact is a *Trope IR*: a labelled DAG. +The portable artefact is a *Trope IR*: a labelled DAG. * *Nodes* are property-instances, each carrying its field-presence over stem:[\Phi] and its type tag (`Trope[S]`, `FloatingQuality`, or a collapse @@ -511,70 +645,94 @@ codomain). * A distinguished *use-model node* carries stem:[\mathrm{floor}(U)]. The IR's *canonical wire format SHALL be a JSON-schema-validated document* -(`schemas/trope-ir.schema.json`); an AsciiDoc normative spec accompanies it; an -*OPTIONAL* Nickel authoring contract MAY be offered front-side. (This mirrors, -deliberately and verbatim, the invariant-path I/O-contract decision: -author-side contracts are courtesy, generated from the schema; the schema is the -trust boundary.) The grade algebra — stem:[\triangleright], stem:[\sqsubseteq], -and stem:[\mathrm{floor}] — SHALL be specified *in the IR spec itself*, -language-neutrally, so that two independent checker implementations agree by -construction. +(`schemas/trope-ir.schema.json`; normative prose in `spec/trope-ir.adoc`, +version 0.2 — R-2026-07-07 changed verdict semantics only, and implementations +MUST accept `0.1` and `0.2` documents and grade both under 0.2 semantics after +normalization). An *OPTIONAL* Nickel authoring contract MAY be offered +front-side; the schema is the trust boundary. The grade algebra — +stem:[\triangleright], stem:[\sqsubseteq], and stem:[\mathrm{floor}] — is +specified in the IR spec itself, language-neutrally, so that two independent +checker implementations agree by construction. Order-sensitivity, where a +producer needs it, lives in the DAG (routing, multi-parent nodes), not in +stem:[\triangleright] (L6). === The checker as a pure function The tropechecker is a *pure function from Trope IR to a verdict object*: `p-sufficient` / `p-insufficient`, plus the witness edge (§6.2). It performs -grade composition over the DAG and the final floor-subsumption. *It MUST NOT -parse, execute, or otherwise depend on source.* That independence is what makes -it portable: it is a checker *of the IR*, and the IR is the contract. +normalization (A3), validation (HC-4 coherence; the prevent profile's rejection +of deceptive values), grade composition over the DAG, and the final +floor-subsumption. *It MUST NOT parse, execute, or otherwise depend on source.* [cols="1,3",options="header"] |=== | Property | Consequence -| *Independence* | Own repository, own versioned IR schema, own conformance suite. The Turing-complete language is the *first* front end that lowers to the IR — dogfooding without coupling. -| *Multi-producer* | A static analyser for an *existing* language MAY emit Trope IR for code it did not author (e.g. lowering a dataframe pipeline's operations to `project` / `collapse` / `fuse` edges). The same checker then trope-checks it. -| *Honest trust boundary* | Front-end grade annotations are *claims*. The checker validates the *composition* of claims; it cannot validate that a source operation truly *is* a given effect. That is lowering correctness (§10-O2), per front end. +| *Independence* | Own repository, own versioned IR schema, own conformance suite. The Turing-complete language (Haec) is the *first* front end that lowers to the IR — dogfooding without coupling. +| *Multi-producer* | A static analyser for an *existing* language MAY emit Trope IR for code it did not author (e.g. lowering a dataframe pipeline's operations to `project` / `collapse` / `fuse` edges). The same checker then trope-checks it. The store (`vocarium`) and the query layer (`hermeneia`) are producers of this kind. +| *Honest trust boundary* | Front-end grade annotations are *claims*. The checker validates the *composition* of claims; it cannot validate that a source operation truly *is* a given effect (O2) or that a claimed-faithful value is true (O5). |=== -=== Verified core, fast core, conformance suite - -The *reference* tropechecker SHOULD be an Agda development that *defines* the -loss-shape category, *proves* L1–L5 and the decidability of stem:[\sqsubseteq], -and *proves* grade soundness (§8). That Agda artifact is the portable -*semantics*. The *shipping* checker (Rust is the recommended target, continuing -the shape-IR lineage, for speed) is validated against the Agda reference by a -*conformance suite*: a corpus of `IR-fragment → expected-verdict` pairs that any -implementation MUST pass. The particularity trainer is, in effect, a *human* +=== Verified kernel, executable reference, fast core, conformance suite + +Per the estate's proof-kernel ruling of 2026-10-12 (ADR 0005), the roles are: + +* *Normative kernel — Agda* (`verification/proofs/agda/theorem-b/`, `--safe + --without-K`, zero postulates): the carrier, the laws, the cancellation + boundary, the intrinsic calculus, substitution and β/let subject reduction + (Theorem B); the CO-1 mechanisation extends it. This is the portable + *semantics*: "portable" means *means-the-same-everywhere* because the meaning + is a checked artefact. +* *Executable reference — Idris2* (`verification/proofs/idris2/`, `src/idris2/`): + the same carrier and laws in quantitative types, and the reference + `tropecheck` executable built on them. The verified core + (`verification/proofs/idris2/Trope/*`) is `%default total`; the executable’s + JSON parser, decoder and checker driver (`src/idris2/`) are `%default covering`, + because a parser is not structurally total without fuel. Neither uses + `believe_me`, `assert_total` or `postulate`. +* *Provenance — Lean 4 + Mathlib* (`verification/proofs/lean4/`): the + grade-algebra boundary and its ratified mirror, the atom factorisation and the + tropical factorisation probe — the Mathlib-facing results, retained with + their axiom audits (`propext`/`Quot.sound` only). +* *Fast core — Rust* (`src/rust/`, dependency-free): the shipping checker, + validated against the reference bit-for-bit over the conformance corpus. + +The *conformance suite* (`tests/conformance/`) is a corpus of +`IR-fragment → expected-verdict` pairs plus schema-invalid documents that MUST be +rejected at the named slot; any implementation claiming conformance MUST pass it +in its declared profile. The particularity trainer is, in effect, a *human* conformance suite for the taxonomy; the machine suite is its formal sibling. -"Portable" thereby means *means-the-same-everywhere* — because the meaning is a -checked Agda artifact and the suite enforces agreement — not merely -*runs-everywhere*. == Open obligations and falsifiers -[cols="1,4",options="header"] +[cols="1,4,1",options="header"] |=== -| ID | Obligation / falsifier - -| *O1 (completeness of the seven)* | The claim that the writable effects are _exhaustive_ is, at present, a well-chosen list, not a theorem. *Falsifier:* exhibit a particularity-affecting operation that is none of the six writable forms (plus the conflation fault). *Upgrade path:* if the three axes — loss-structure × bond-integrity × cardinality/honesty — are the true generators, *derive* the typology as the inhabited cells of their product and *prove* exhaustiveness relative to those axes, turning the list into a theorem (the same move that turned "three layers in a pipeline" into "one substrate, two analyses, one law"). This decision SHOULD be taken *before* the IR schema is frozen. -| *O2 (lowering correctness)* | Per front end: a proof that each source construct it lowers to an effect edge *is* that effect. Separate from grade soundness (§8, firewall 2). Not dischargeable by the core. -| *O3 (the produce/demand adjunction)* | Whether the producing graded monad and the demanding graded comonad form an adjunction with produce/demand as unit/counit. Conjecture; requires the grade category pinned (O1) and the triangle laws checked. Until then, the verdict is a subsumption, *not* an adjunction cancellation. -| *O4 (fidelity carrier)* | Whether the fidelity dimension stem:[\mathbb{N}\cup\{\infty,\top\}] suffices, or a transfinite/coinductive carrier is needed once iterated attenuation must be ordered beyond stem:[\omega] (the standing `Conat`-vs-tag fork from the choreographic-typing line). Defer until a second instance demands it. +| ID | Obligation / falsifier | Status + +| *O1-carrier (exhaustiveness relative to the carrier)* | Every grade factors as a ▷-product of single-slot projections drawn from the nine atom families; the effect typology is exhaustive *relative to the three-coordinate carrier*. | PROVED (`EffectAtoms.lean`: `atom_factorization`, `nine_families`, `family_realized`, `families_disjoint`). +| *O1-coord (metaphysical adequacy)* | Are `fate`, `bond`, `merge` themselves exhaustive as ways to individuate-and-lose? A claim about the world, not the algebra. *Falsifier:* a particularity-affecting operation that no atom family captures. *Live probe:* the transposition of a quality between bearers (the classic *swapping* problem) is not expressible — it is neither `sever` nor `fuse` nor any bond value — and a *bond-transfer* move with an honest (labelled) and a deceptive (`Misbound`) form is the candidate tenth family. Either it reduces to the existing atoms or it is a fourth generator; the adequacy argument must say which. | OPEN (workbench WP-5). +| *O2 (lowering correctness)* | Per front end: a proof that each source construct it lowers to an effect edge *is* that effect. Separate from grade soundness (§8, firewall 2). Not dischargeable by the core. | OPEN per producer; no producer has discharged it. +| *O3 (the produce/demand adjunction)* | Whether the producing graded monad and the demanding graded comonad form an adjunction with produce/demand as unit/counit. Requires the triangle laws checked against the ratified carrier (now pinned, so no longer gated by O1-carrier). Until then, the verdict is a subsumption, *not* an adjunction cancellation. | OPEN (conjecture). +| *O4 (fidelity carrier)* | Whether stem:[\mathbb{N}\cup\{\infty,\top\}] suffices for ordering iterated attenuation. | RESOLVED (ADR 0004): it does — transfinite carriers would require transfinitely deep `fix` nesting, which finitary syntax cannot express. Whether the carrier should be a *parameter* (any resource algebra with two adjoined tops) rather than this one instance is a separate design question recorded in ADR 0005. +| *O5 (the veridicality oracle)* | *Remark O5-a (IR-relative undecidability).* A valid Trope IR is a set of claims. For any IR document stem:[D] and any slot, there exist two worlds — one in which the claimed value is the value the trope in fact had, one in which it is not — inducing the same stem:[D]; since the checker is a pure function of stem:[D], no checker can decide veridicality. What is guaranteed instead is L3/L5. *Interface.* An implementation MAY bind a *veridicality oracle*, an external judgement `Oracle ⊨ record r faithful-to trope t` (per slot), subject to: *O5-1 (soundness)* if the oracle affirms a slot, the honest grade claimed for it is true of the world, and the oracle MUST NOT affirm a `Falsified`, `Misbound` or `Conflated` situation; *O5-2 (attestation)* every oracle verdict MUST be carried as evidence — who checked, against what access to the world, when — and that attestation enters the `record` slot's provenance, not the quality's value; *O5-3 (no laundering)* an oracle verdict upgrades *confidence*, never *grade*: a checked `Attenuated(δ)` is still `Attenuated(δ)`. *Falsifier:* a deployment where an interface satisfying O5-1..3 lets a deceptive grade reach `p-sufficient` against an honest floor. *Upgrade path:* mechanise O5-1 as a side condition on an `Oracle`-indexed variant of the verdict judgement. Vocarium's warrants are O5-2 attestations; Hermeneia's *licensed* band is the verdict band O5-backed claims occupy. | DEFINED (adopted from the workbench proposal of 2026-07-17 by ADR 0005); mechanisation OPEN. +| *O6 (the ceiling verdict)* | New at v0.2. The verdict certifies sufficiency only. A *ceiling* use-model — "no more than this may be retained" (the privacy direction: a `Withheld` bond is a recoverable, hence still-personal, record; `Severed` is not) — needs the dual theorem stem:[\rho \sqsubseteq g_{\mathrm{ceiling}}], which T-Sub's one-sidedness does not give for conservative lowering. *Deliverable:* either the dual verdict proved for the exact-lowering fragment and stated as unavailable for the conservative one, or a second, upper-bound grade on edges. | OPEN. +| *CO-1 (the operational model)* | The calculus's reduction dynamics for `fix` and routing. The grade algebra is not at fault (the gfp endpoint is ▷-fixed and tier-stable). | DESIGNED (λ-trope, tagged values, T-Fix-Decl: `spec/notes/2026-07-07-co1-operational-model.adoc`); MECHANISATION OPEN (Agda, steps 1–5 of that note's §6; closes Theorem B Target 3 and conservative grade soundness). |=== == Provenance of the ideas (so nothing is overclaimed) Graded monads, coeffects, and effect rows are established machinery -(Katsumata; Gaboardi; Petricek, Orchard, Mycroft; Uustalu). Tropes as abstract -particulars are established metaphysics (Williams; Campbell). The -graded-monad-for-loss reading is the echo-types line. What is assembled *here* — -a graded effect discipline tracking *which kind* of particularity-loss an -operation inflicts on a provenance-enriched metaphysical trope, with -conflating/fusing as the deceptive/faithful collapse, checked against a -use-model coeffect demand, lowered to a language-neutral IR — is, as a *named -combination*, the contribution. The atoms are mostly already named; the -unclaimed ground is the unification and the three-coordinate loss-shape grade. +(Katsumata; Gaboardi; Petricek, Orchard, Mycroft; Uustalu). Property-instances +as particulars are established metaphysics (Williams; Campbell) and established +applied ontology (UFO's moments, DOLCE's qualities, BFO's specifically dependent +continuants). The graded-monad-for-loss reading is the echo-types line. What is +assembled *here* — a graded effect discipline tracking *which kind* of +particularity-loss an operation inflicts on a provenance-enriched +property-instance, with the three deceptive duals as faults rather than moves, +checked against a use-model coeffect demand, lowered to a language-neutral IR — +is, as a *named combination*, the contribution. The atoms are mostly already +named; the unclaimed ground is the unification, the three-coordinate loss-shape +grade, and the structure theorems (§3.5, §4.2) that fix it. == Worked check (the duck, end to end) @@ -583,15 +741,17 @@ This is `collapse[isQuack]`: the residual grade has `fate(quality)=Predicated(isQuack)`, all other fields `Dropped`, `bond=Withheld`, `merge=Single`. Against a use-model whose floor demands the call's spectral content — `floor(U)` requires `quality ⊒ Attenuated(δ)` for some finite stem:[\delta] -— we check `floor(U) ⊑ g`. Since `Predicated(isQuack)` is *incomparable to and -below* any `Attenuated(δ)` in the fate lattice (§3.1), the check fails: verdict -`p-insufficient`, witness = the `collapse` edge. The same call recorded losslessly -with ring number, pond, date and weather is `preserve`, grade stem:[\varepsilon], -which dominates every floor: `p-sufficient`. The trainer's intuition and the +— we check `floor(U) ⊑ g`. Since `Predicated(isQuack)` sits *strictly below* +every `Attenuated(δ)` in the fate chain (§3.1), the check fails: verdict +`p-insufficient`, witness = the `collapse` edge (conformance fixture +`duck-collapse`). The same call recorded losslessly with ring number, pond, date +and weather is `preserve`, grade stem:[\varepsilon], which dominates every +floor: `p-sufficient` (`duck-preserve`). The trainer's intuition and the calculus agree, which is the point. ''' -_Suggested CHANGELOG line:_ `docs: pin trope-particularity calculus v0.1 -(three-coordinate loss-shape grade; six writable effects + conflation-as-fault -[R-2026-06-22]; composition laws L1–L5; verdict = floor-subsumption; grade -soundness target + lowering firewall; portable Trope IR)._` +_CHANGELOG line:_ `docs(spec): consolidate the calculus at v0.2 — nine effects +with the atom table, ratified carrier inline (A1–A3), L6 commutativity and the +cancellation structure as laws, the tropical factorisation recorded as sighted, +§7 restated as greatest post-fixed point with T-Fix-Decl, O5 defined and O6 +(ceiling verdict) opened, prover roles per ADR 0005._ diff --git a/verification/proofs/INTEGRATION-REPORT.adoc b/verification/proofs/INTEGRATION-REPORT.adoc index 6bd5f0c..2444b8e 100644 --- a/verification/proofs/INTEGRATION-REPORT.adoc +++ b/verification/proofs/INTEGRATION-REPORT.adoc @@ -9,6 +9,17 @@ :sectnumlevels: 2 :stem: latexmath +[NOTE] +==== +*Historical report (2026-06-29).* This reconciles the two proof streams against +the *pre-ratification* carrier. It is kept unchanged as the record of that +integration. Since then: ADR 0004 (R-2026-07-07) amended the carrier — the +non-commutativity, the lax L4 and OPEN-B/B′/C below are all resolved on the +ratified carrier — and the v0.2 addendum it cites (`spec/calculus-v0.2-draft.adoc`) +was folded into `spec/calculus.adoc` v0.2 on 2026-10-13. Current status lives in +`docs/status/PROOF-STATUS.adoc` and `AFFIRMATION.adoc`. +==== + [abstract] This report integrates two independently-produced work-streams into one coherent contribution, each measured against the same authoritative algebra: From 44020f98dc60d4f67229eef5f0a203d83b7e30ae Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 13 Oct 2026 14:29:07 +0000 Subject: [PATCH 02/15] ci(proofs): pin Agda 2.7.0.1 + stdlib 2.0 by checksum; gate every Lean source The `agda-theorem-b` job installed Agda from the runner's apt. ubuntu-latest is 24.04, whose agda-stdlib is 1.7.3, and Theorem B imports Data.Product.Base (stdlib >= 2.0): the job fails at scope checking (exit 42). Reproduced here 2026-10-13 with Agda 2.6.3 / stdlib 1.7.3, exactly the runner's pair. The workflow's own comment records a green run "under 2.6.4.3", which was a Debian machine, not the runner. Because the workflow is paths-filtered to verification/proofs/**, it has not run since the last proof change and the red was never seen. Fix: fetch the Agda 2.7.0.1 release binary and the agda-stdlib v2.0 archive, verify both SHA-256 sums, register the stdlib under the name theorem-b.agda-lib depends on (`standard-library`; the 2.0 archive calls itself `standard-library-2.0`), set Agda_datadir and a UTF-8 locale. Verified 2026-10-13 with exactly these artefacts and sums: All.agda and Smoke.agda typecheck under --safe --without-K, exit 0 (~100 s cold). The stdlib sum is of the GitHub-generated tag archive (no release asset exists); if GitHub ever regenerates it the checksum step fails loudly instead of testing something else. Also: `lean-source-honesty` and the mirroring `verify-all` recipe gated only the two v0.1 files (GradeBoundary, GradeFactorisation). The spec now cites GradeRatified, L4Monotonicity, TierTwoComplete, EffectAtoms and GradeFactorisationR, so both now iterate every tracked Lean source. All eight files pass the gate's regexes as they stand (run here). actionlint -shellcheck= on proofs.yml: clean. The job's real run is still needed: this sandbox has no Lean, so the lean-build matrix was not exercised. --- .github/workflows/proofs.yml | 66 +++++++++++++++++++++--------------- build/just/proofs.just | 6 ++-- 2 files changed, 42 insertions(+), 30 deletions(-) diff --git a/.github/workflows/proofs.yml b/.github/workflows/proofs.yml index 03ed992..36074cb 100644 --- a/.github/workflows/proofs.yml +++ b/.github/workflows/proofs.yml @@ -53,8 +53,10 @@ jobs: run: | set -euo pipefail fail=0 - for f in verification/proofs/lean4/grade-boundary/GradeBoundary.lean \ - verification/proofs/lean4/grade-factorisation/GradeFactorisation.lean; do + # Every Lean source, not only the two v0.1 files: the ratified-carrier + # results (GradeRatified, L4Monotonicity, TierTwoComplete, EffectAtoms, + # GradeFactorisationR) are what the current spec cites. + for f in $(git ls-files 'verification/proofs/lean4/*.lean' 'verification/proofs/lean4/*/*.lean'); do if [ ! -f "$f" ]; then echo "::error::gated file is missing: $f"; fail=1; continue fi @@ -73,41 +75,49 @@ jobs: # so this is a real check of postulate-freedom and not a word-grep (a grep would # false-positive on the honest "postulate-free" prose in the comments). # - # NOTE ON THE VERSION PIN: theorem-b.agda-lib is developed against Agda 2.8.0 - # (ADR 0003). The runner's packaged Agda is older. The version is printed, not - # asserted, because asserting a version the runner cannot supply produces a - # permanently-red gate rather than a signal — and the substantive guarantee here - # comes from --safe --without-K, which holds across versions. Verified locally - # under 2.6.4.3: All.agda and Smoke.agda both typecheck, exit 0. + # TOOLCHAIN: pinned release artefacts, not the runner's apt. ubuntu-latest is + # 24.04, whose agda-stdlib is 1.7.3; Theorem B imports Data.Product.Base, which + # exists from stdlib 2.0, so `apt-get install agda agda-stdlib` there fails at + # scope checking (exit 42) — reproduced 2026-10-13. The job now fetches the + # Agda 2.7.0.1 release binary and the stdlib v2.0 source archive, verifies + # both SHA-256 sums, and registers the stdlib under the name the .agda-lib + # depends on. Verified 2026-10-13 with exactly these artefacts: All.agda and + # Smoke.agda typecheck under --safe --without-K, exit 0 (~100 s). A checksum + # mismatch fails loudly rather than silently testing a different stdlib. agda-theorem-b: name: "Agda Theorem B (--safe --without-K)" runs-on: ubuntu-latest timeout-minutes: 30 steps: - uses: actions/checkout@v7.0.1 - - name: Install Agda and register the standard library + - name: Install Agda 2.7.0.1 and agda-stdlib 2.0 (pinned, checksummed) shell: bash + env: + AGDA_URL: https://github.com/agda/agda/releases/download/v2.7.0.1/Agda-v2.7.0.1-linux.tar.xz + AGDA_SHA256: 975b515a14877ab6bce5bfc641e16c4a3ee52ca5d7f846577dee80aa2145db8a + STDLIB_URL: https://github.com/agda/agda-stdlib/archive/refs/tags/v2.0.tar.gz + STDLIB_SHA256: 14eecb83d62495f701e1eb03ffba59a2f767491f728a8ab8c8bb9243331399d8 run: | set -euo pipefail - sudo apt-get update -qq - sudo apt-get install -y -qq --no-install-recommends agda agda-stdlib - echo "agda --version -> $(agda --version | head -1)" - echo "ratified pin (ADR 0003) is Agda 2.8.0; --safe --without-K is the substantive check" - - # Installing the package is not enough: Agda only sees a library that is - # listed in its `libraries` file, and a fresh runner has none. WHICH path - # that file lives at is VERSION-DEPENDENT (~/.agda vs ~/.config/agda), so - # point AGDA_DIR at a directory we control rather than guessing, and - # resolve the .agda-lib from the package rather than hardcoding it. - lib="$(dpkg -L agda-stdlib | grep -m1 'standard-library\.agda-lib$' || true)" - if [ -z "$lib" ]; then - echo "::error::agda-stdlib is installed but standard-library.agda-lib was not found" - exit 1 - fi - mkdir -p "${RUNNER_TEMP}/agda" - echo "$lib" > "${RUNNER_TEMP}/agda/libraries" - echo "AGDA_DIR=${RUNNER_TEMP}/agda" >> "$GITHUB_ENV" - echo "registered standard-library at: $lib" + mkdir -p "${RUNNER_TEMP}/agda-toolchain" && cd "${RUNNER_TEMP}/agda-toolchain" + curl -sSL -o agda.tar.xz "$AGDA_URL" + echo "$AGDA_SHA256 agda.tar.xz" | sha256sum -c - + curl -sSL -o stdlib.tar.gz "$STDLIB_URL" + echo "$STDLIB_SHA256 stdlib.tar.gz" | sha256sum -c - + tar -xJf agda.tar.xz && tar -xzf stdlib.tar.gz + # theorem-b.agda-lib depends on `standard-library`; the 2.0 archive names + # itself `standard-library-2.0`, so register a lib file under the depended-on name. + printf 'name: standard-library\ninclude: src\nflags:\n --warning=noUnsupportedIndexedMatch\n' \ + > agda-stdlib-2.0/standard-library.agda-lib + mkdir -p "${RUNNER_TEMP}/agda-dir" + echo "$PWD/agda-stdlib-2.0/standard-library.agda-lib" > "${RUNNER_TEMP}/agda-dir/libraries" + { + echo "AGDA_DIR=${RUNNER_TEMP}/agda-dir" + echo "Agda_datadir=$PWD/Agda-v2.7.0.1/data" + echo "LC_ALL=C.UTF-8" + } >> "$GITHUB_ENV" + echo "$PWD/Agda-v2.7.0.1/bin" >> "$GITHUB_PATH" + "$PWD/Agda-v2.7.0.1/bin/agda" --version - name: Typecheck Theorem B shell: bash working-directory: verification/proofs/agda/theorem-b diff --git a/build/just/proofs.just b/build/just/proofs.just index 6850a3f..8d1d63a 100644 --- a/build/just/proofs.just +++ b/build/just/proofs.just @@ -191,6 +191,8 @@ build-agda: #!/usr/bin/env bash set -euo pipefail echo "=== build-agda: Theorem B metatheory (--safe --without-K) ===" + # Needs Agda >= 2.6.4 and agda-stdlib >= 2.0 (Data.Product.Base); the CI job + # pins Agda 2.7.0.1 + stdlib 2.0 by checksum — see proofs.yml agda-theorem-b. cd verification/proofs/agda/theorem-b agda --safe --without-K All.agda agda --safe --without-K Smoke.agda @@ -204,8 +206,8 @@ verify-all: build-lean build-agda #!/usr/bin/env bash set -euo pipefail echo "=== verify-all: Lean source honesty gate ===" - for f in verification/proofs/lean4/grade-boundary/GradeBoundary.lean \ - verification/proofs/lean4/grade-factorisation/GradeFactorisation.lean; do + # Every Lean source (mirrors proofs.yml lean-source-honesty; keep the two in step). + for f in $(git ls-files 'verification/proofs/lean4/*.lean' 'verification/proofs/lean4/*/*.lean'); do echo "--- gating $f ---" if grep -nE '(:=|by|;|<;>|=>|\|)[[:space:]]*(sorry|admit)\b|\bnative_decide\b' "$f"; then echo "FAIL: forbidden Lean tactic (sorry/admit/native_decide) in $f"; exit 1; fi From f23092692d4c02cce0f11a439240443c6f70de9f Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 27 Oct 2026 07:55:10 +0000 Subject: [PATCH 03/15] docs(status): rewrite PROOF-STATUS to the ratified world MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit What was wrong: PROOF-STATUS.adoc (revdate 2026-06-23) described the v0.1 carrier — a non-commutative ▷, a lax L4 that "fails on fate", CO-1 "gated by O4", the OPEN-B/B′/C documentation gaps, "10/10" conformance — and listed as open several results (O1 exhaustiveness, L4/L5 as lemmas) that are now proved. A reader following it alone got the pre-ratification world. What changed: one "Proved" table on the ratified carrier (Carrier & laws / Cancellation / Factorisation / Metatheory / Soundness), citing only lemma names that exist in the Idris2, Agda and Lean sources; one "Open" list matching spec/calculus.adoc §10 (CO-1 mechanisation, O1-coord, O2, O3, O5 mechanisation, O6) with where each is specified; the four modelling notes carried over; the 06-22 / 06-23 / 06-29 sections collapsed to one dated paragraph each under "History", prefixed as superseded by R-2026-07-07 where they disagree. What I ran: every cited identifier checked present by grep over verification/proofs/{idris2/Trope,agda/theorem-b/TB,lean4} (38 + 43 + 44 names, none missing); the acceptance grep for the stale phrases outside "== History" returns nothing. What I did not run: no prover in this commit (the AFFIRMATION commit carries the runs). Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01J4QvDh3p24SCUjyM9HHT31 --- docs/status/PROOF-STATUS.adoc | 376 +++++++++++++++++----------------- 1 file changed, 190 insertions(+), 186 deletions(-) diff --git a/docs/status/PROOF-STATUS.adoc b/docs/status/PROOF-STATUS.adoc index c6cfe66..c84ecd4 100644 --- a/docs/status/PROOF-STATUS.adoc +++ b/docs/status/PROOF-STATUS.adoc @@ -1,210 +1,214 @@ // SPDX-FileCopyrightText: © 2026 Jonathan D.A. Jewell (hyperpolymath) // SPDX-License-Identifier: CC-BY-SA-4.0 -// SPDX-License-Identifier: CC-BY-SA-4.0 -= Proof status — trope-checker verified core -:revdate: 2026-06-23 += Proof status — trope-checker +:revdate: 2026-10-27 :toc: macro :stem: latexmath -What is *proved* (machine-checked, no axioms), *stubbed-and-named* (an open -problem stated, never asserted as done — HC-5), and *deferred*. Ground-truth: -`idris2 --typecheck verification/proofs/idris2/trope.ipkg` (exit 0). No -`believe_me`, `assert_total`, or `postulate` stands behind any claim below. +What is *proved* (machine-checked, no axioms beyond `propext`/`Quot.sound` in +Lean; `--safe --without-K` in Agda; `%default total` with no escape hatch in +Idris2) and what is *open* (named, specified, not asserted), on the ratified +carrier of `spec/calculus.adoc` v0.2 (R-2026-07-07, ADR 0004). Prover roles per +ADR 0005: Agda is the normative kernel, Idris2 the executable reference, Lean the +provenance development, Rust the fast core. Ground truth is the latest entry of +`AFFIRMATION.adoc`; every name below is a definition in the proof sources. toc::[] -== Proved (machine-checked) +== Proved -[cols="1,2,2",options="header"] -|=== -| Lemma | Statement | Where -| Fidelity L1 | `dplus` (tropical loss addition, ⊤ absorbs ∞ absorbs finite) is associative | `Trope.Fidelity.dplusAssoc` -| Fidelity unit/refl | `Q 0` right-unit of `dplus`; `dLte` reflexive | `Trope.Fidelity.dplusZeroR`, `dLteRefl` -| Coordinate L1 | `▷` associative on fate, bond, merge | `Trope.Coords.{fateAssoc,bondAssoc,mergeAssoc}` -| Coordinate L2 | unit of `▷` on each coordinate | `Trope.Coords.{fateUnitL/R,bondUnitL/R,mergeUnitL/R}` -| Coordinate ⊑ refl | retention order reflexive on each coordinate | `Trope.Coords.{fateLteRefl,bondLteRefl,mergeLteRefl}` -| Grade L1 (assoc) | `▷` associative on the full three-coordinate grade | `Trope.Laws.gradeAssoc` -| Grade L2 (unit) | `ε ▷ g = g = g ▷ ε` | `Trope.Grade.{gradeUnitL,gradeUnitR}` -| Decidability of ⊑ | `⊑` is decidable on grades | `Trope.Laws.decGradeLte` -| Veridicality Derivation | exactly three deceptive duals, one per coordinate (Falsified/Misbound/Conflated), each the unique deceptive inhabitant | `Trope.Veridicality.{fate,bond,merge}DeceptiveUnique`, `deceptiveDuals` -| Honest Generation | the five atoms (attenuate/predicate/drop/sever/fuse) + ε generate exactly the honest fragment of each coordinate; the atoms never produce a deceptive dual | `Trope.Generation.{genFate,genBond,genMerge,movesHonest*}` -| ε honest & coherent | ε is non-deceptive and HC-4-coherent | `Trope.Veridicality.epsilonHonest`, `Trope.Grade.epsilonCoherent` +[cols="1,3,3",options="header"] |=== +| Result | Statement | Where -== Stubbed-and-named (open problems — NOT asserted) +3+^| _Carrier and laws_ -[cols="1,3",options="header"] -|=== -| ID | Open problem -| *Grade soundness* (calculus §8) | `Γ ⊢ e : A ! g ⟹ g ⊑ ρ(in,out)` — the declared grade never claims more retention than execution delivers. Requires an operational model of execution (`ρ`); the term language is out of the verified core's scope this pass. Stated in the calculus; *not* claimed proved here. PARTIAL ADVANCE 2026-06-22 (see "Soundness advance" below): the verdict corollary, T-Sub soundness, and grade soundness for EXACT faithful lowering are now machine-checked; what remains open is the term-language/fix operational model and conservative composition over fate. -| *L4 monotonicity / L5 infectiousness as theorems* | Hold by the bottom/absorbing structure of each coordinate (used implicitly); not yet extracted as standalone Idris lemmas. Tractable; deferred to the next pass. -| *O1 exhaustiveness of the effects* | That the five atoms (plus the three duals) are the _true generators_ of all particularity-affecting operations is a well-chosen list, not yet a theorem derived from the three axes. Calculus O1. Philosophy-of-individuation question O1-coord is logged, not coded. +| L1 (associativity) +| stem:[(g_1 \triangleright g_2)\triangleright g_3 = g_1 \triangleright (g_2 \triangleright g_3)] on the full three-coordinate grade; per coordinate and on the fidelity dimension. +| Idris2 `Trope.Laws.gradeAssoc`, `Trope.Coords.{fateAssoc,bondAssoc,mergeAssoc}`, `Trope.Fidelity.dplusAssoc`; Agda `TB.Grade.gmonoid-assoc`; Lean `GradeR.instCommMonoid` (`GradeRatified.lean`), `FateA.comp_assoc` (`L4Monotonicity.lean`). + +| L2 (unit) +| stem:[\varepsilon \triangleright g = g = g \triangleright \varepsilon]. +| Idris2 `Trope.Grade.{gradeUnitL,gradeUnitR}`, `Trope.Coords.fateUnitL`, `Trope.Fidelity.dplusZeroR`; Agda `TB.Grade.{gmonoid-unitL,gmonoid-unitR}`. + +| L3 (bottom absorption) +| Each deceptive bottom (`Falsified`, `Misbound`, `Conflated`, fidelity `Unknown`) is a two-sided zero of its coordinate's composition (A1). `Total` absorbs within fidelity. +| Agda `TB.Grade.{falsified-absorbL,falsified-absorbR,misbound-absorbL,conflated-absorbL,unknown-absorbL,total-absorb-Q}`, `TB.Tier.deceptive-absorbs-▷`; Lean `FateA.falsified_two_sided_zero`, `GradeR.gBotR_two_sided_zero`. + +| L4 (monotonicity), in full +| stem:[\triangleright] is monotone in both arguments w.r.t. stem:[\sqsubseteq] on every coordinate of the ratified carrier. +| Idris2 `Trope.Soundness.{fateL4MonoR,fateL4MonoL}`, `Trope.Order.{bondComposeMono,mergeComposeMono}`; Agda `TB.Order.{fateL4MonoR,fateL4MonoL}`; Lean `FateA.{comp_mono_right,comp_mono_left}`. + +| L5 (deception infectiousness) +| Once a coordinate is at its deceptive bottom no composition restores an honest value; applying any further effect to a deceptive term keeps it deceptive. A corollary of L3. +| Agda `TB.Tier.deceptive-absorbs-▷`, `TB.Reduction.{attenuate-stays-deceptive,project-stays-deceptive}`. + +| L6 (commutativity) +| stem:[g_1 \triangleright g_2 = g_2 \triangleright g_1] on the ratified carrier. +| Lean `GradeR.instCommMonoid`, `FateA.comp_comm`; Agda `TB.Grade.grade-comm`. + +| Retention order is a decidable preorder +| stem:[\sqsubseteq] is decidable, reflexive and transitive on grades. +| Idris2 `Trope.Laws.decGradeLte`, `Trope.Coords.{fateLteRefl,bondLteRefl,mergeLteRefl}`, `Trope.Fidelity.dLteRefl`, `Trope.Order.{fateLteTrans,bondLteTrans,mergeLteTrans,dLteTrans}`, `Trope.Soundness.gradeLteTrans`. + +| Fate is a chain (A2) +| `Dropped ⊑ Predicated` and `Predicated ⋢ Dropped`; the v0.1 antichain is dissolved in the stated direction only. +| Idris2 `Trope.Soundness.{fateDroppedLtePredicated,fatePredicatedNotLteDropped}`; Agda `TB.Order.{fateDroppedLtePredicated,fatePredicatedNotLteDropped}`. + +| Veridicality Derivation +| Exactly three deceptive duals, one per coordinate kind (`Falsified`, `Misbound`, `Conflated`), each the unique deceptive inhabitant of its coordinate. +| Idris2 `Trope.Veridicality.{fateDeceptiveUnique,bondDeceptiveUnique,mergeDeceptiveUnique,deceptiveDuals}`; Agda `TB.Honest.{fateDeceptiveUnique,bondDeceptiveUnique,mergeDeceptiveUnique,deceptiveDuals}`. + +| Honest Generation +| The five atoms `attenuate`, `predicate`, `drop`, `sever`, `fuse` with stem:[\varepsilon] generate exactly the honest fragment of each coordinate and never produce a deceptive dual; honesty is closed under stem:[\triangleright]. +| Idris2 `Trope.Generation.{genFate,genBond,genMerge}`; Agda `TB.Honest.{genFate,genBond,genMerge}`, `TB.Honest.honest-closed-▷`. + +| stem:[\varepsilon] is honest and coherent +| The unit is non-deceptive and HC-4-coherent. +| Idris2 `Trope.Veridicality.epsilonHonest`, `Trope.Grade.epsilonCoherent`. + +3+^| _Cancellation_ + +| C1 (conicality) +| stem:[g_1 \triangleright g_2 = \varepsilon \Rightarrow g_1 = g_2 = \varepsilon]. +| Lean `GradeR.conical`, `FateA.conical`; Agda `TB.Grade.grade-conical`. + +| C2 (the cancellation boundary) +| An element is left-cancellative iff it is stem:[\varepsilon]; cancellation holds only on the finite-fidelity core and fails on the honest-but-lossy and deceptive tiers alike. +| Lean `GradeR.{gradeR_leftCancel_iff,gradeR_not_leftCancel,gDroppedR_not_cancel}`; Agda `TB.Tier.{Q-cancelʳ,core-closed-▷}`, `TB.Tier.{dropped,predicated,severed,total}-honest-not-cancel`, `TB.Tier.{falsified,unknown}-not-cancel`. + +| Tier-2 membership, exhaustive +| Every honest-but-lossy element is individually witnessed non-cancellative, `Withheld` and `Fused` included; the per-element witnesses feed the iff. +| Lean `TierTwoComplete.lean`: `Bond.withheld_honest_not_cancel`, `Merge.fused_honest_not_cancel`, `Fate.atten_not_cancel`, the `*.leftCancelWitness` family, `Grade.grade_leftCancel_iff`. + +| C3 (partition; tier closure is not a homomorphism) +| `Dropped`, `Total`, `Severed`, `Predicated`, `Withheld`, `Fused` are honest non-cancellative elements; `Falsified`, `Misbound`, `Conflated`, `Unknown` are the deceptive ones. `tierOf (g ▷ h) = tierOf g ⊓ tierOf h` is false on fate; tier preservation is closure. +| Lean `dropped_absorbing`, `fidelity_total_honest_not_cancel` (`GradeBoundary.lean`); Agda `TB.Tier.fate-tier-meet-hom-fails`, the `TB.Tier` classifiers. + +3+^| _Factorisation_ + +| O1-carrier (atom factorisation) +| Every grade is the stem:[\triangleright]-product of its single-slot projections; nine atom families, each realised, pairwise disjoint. +| Lean `EffectAtoms.lean`: `Trope.Grade.atom_factorization`, `Trope.nine_families`, `Trope.family_realized`, `Trope.families_disjoint`, `fateFamily_none_iff`. + +| Tropical factorisation, (B′) sighted +| A nontrivial surjective monoid homomorphism stem:[\pi_R] onto the commutative tropical fidelity carrier exists and distinguishes `Dropped` (stem:[\infty]) from `Falsified` (stem:[\top]); the verbatim-payload map is not a homomorphism, and any sighted homomorphism squashes `Unknown` to the deceptive top. +| Lean `GradeFactorisationR.lean`: `piR_hom`, `piR_one`, `piRHom`, `piR_nontrivial`, `piR_surjective`, `piR_sighted`, `phiR_sighted`, `phiId_not_hom`, `sighted_forces_squash`. + +3+^| _Metatheory (Theorem B, Agda `--safe --without-K`, zero postulates)_ + +| Target 1 — intrinsic graded calculus +| The typing judgement stem:[\Gamma \vdash e : A \mathbin{!} g] over the ratified grade monoid, with the F4 tiers as closures. +| Agda `TB.Syntax`, `TB.Grade`, `TB.Tier`. + +| Target 2 — grade-exact substitution +| Cut preserves the grade exactly; grade commutes with cut. +| Agda `TB.Substitution.{cut-preserves-grade,cut-grade-comm}`. + +| Target 3 — subject reduction, β/let core +| β and `let` steps preserve type and grade exactly; the redex grade is the contractum grade; the tier is preserved; sequencing two core computations stays in the core. +| Agda `TB.Reduction.{β-app,β-let,let-redex-grade,let-tier-preserved,seq-stays-core}`. (The `fix` case is open: see CO-1 below.) + +| Target 4 — Honest Generation and Veridicality +| As in the carrier rows above, at the level of terms. +| Agda `TB.Honest`. + +3+^| _Soundness_ + +| Grade soundness, exact lowering +| If the declared grade equals the observed retention, stem:[g \sqsubseteq \rho]. +| Idris2 `Trope.Soundness.soundFromExact`. + +| T-Sub soundness +| stem:[g' \sqsubseteq g \wedge g \sqsubseteq \rho \Rightarrow g' \sqsubseteq \rho]. +| Idris2 `Trope.Soundness.subSound`. + +| Verdict soundness (corollary) +| stem:[\mathrm{floor}(U) \sqsubseteq g \wedge g \sqsubseteq \rho \Rightarrow \mathrm{floor}(U) \sqsubseteq \rho]. +| Idris2 `Trope.Soundness.verdictSound`. + +| Grade soundness, β/let core +| Reduction in the exact fragment preserves the grade (Theorem B Target 3 above). +| Agda `TB.Reduction`, `TB.Substitution.cut-preserves-grade`. |=== -== Deferred (named, not attempted this pass) +The Rust fast core (`src/rust/`) is not a proof; it agrees with the Idris2 +reference over the whole conformance corpus (`just trope-rust`). + +== Open -* Full Haec compiler / codegen / runtime (scaffolded in the `haec` repo). -* A Rust fast-core — *DRAFTED 2026-06-22* (`src/rust/`, dep-free, std-only; agrees with the Idris2 reference bit-for-bit over the conformance corpus, via `just trope-rust`). Further hardening (fuzzing, perf) deferred. -* The produce/demand adjunction (calculus O3); the fidelity-carrier question (O4). +Each is specified; none is asserted. Status words follow `spec/calculus.adoc §10`. -== Modelling notes (faithful-but-simplified, recorded for honesty) +* *CO-1 mechanisation* — the operational model (λ-trope, tagged values, + T-Fix-Decl) is DESIGNED in `spec/notes/2026-07-07-co1-operational-model.adoc`; + its mechanisation in Agda, steps 1–5 of that note's §6 extending `TB.Reduction`, + is OPEN. It closes Theorem B Target 3 (`fix`, NOT-REACHED, no postulate) and + grade soundness for conservative lowering (`spec/calculus.adoc §7–§8`). +* *O1-coord* — whether `fate`, `bond`, `merge` are exhaustive ways to + individuate-and-lose; live probe: the bond-transfer move (`spec/calculus.adoc + §10`; workbench WP-5). +* *O2* — lowering correctness, per producer; no producer has discharged it + (`spec/calculus.adoc §8` firewall 2, `§10`). +* *O3* — the produce/demand adjunction; the verdict is a subsumption until the + triangle laws are checked (`spec/calculus.adoc §6.2`, `§10`). +* *O5 mechanisation* — O5 is DEFINED (`spec/calculus.adoc §10`, ADR 0005); + mechanising O5-1 as a side condition on an `Oracle`-indexed verdict is OPEN. +* *O6* — the ceiling verdict, stem:[\rho \sqsubseteq g_{\mathrm{ceiling}}], for + the privacy direction (`spec/calculus.adoc §5` note on T-Sub, `§10`). + +== Modelling notes + +Faithful-but-simplified choices, recorded for honesty: * *Provenance tags on `Fused` are erased* in the verified core (they are metadata that does not affect the lattice laws); the executable checker carries them. * *Deceptive duals are modelled as each coordinate's bottom* (worst retention, absorbing), which is how the calculus orders `Conflated`; this makes every honest floor fail against a deceptive grade (HC-2) by construction. -* *L2 is stated with ε's literal value* in Idris (a bare top-level `epsilon` as a - function argument does not reduce under the unifier); since - `epsilon = MkGrade Present Present Present Present Intact Single` definitionally, - the statement is `ε ▷ g = g`. -* *The use-model floor is a partial per-coordinate demand, not a grade value.* HC-4 - (the Σ-coherence: bond⊣bearer-fate) is enforced on edge grade VALUES, where it - makes incoherent states unrepresentable; the floor is a set of independent +* *L2 is stated with stem:[\varepsilon]'s literal value* in Idris (a bare top-level + `epsilon` as a function argument does not reduce under the unifier); since + `epsilon = MkGrade Present Present Present Present Intact Single` + definitionally, the statement is stem:[\varepsilon \triangleright g = g]. +* *The use-model floor is a partial per-coordinate demand, not a grade value.* + HC-4 (the Σ-coherence: bond⊣bearer-fate) is enforced on edge grade VALUES, where + it makes incoherent states unrepresentable; the floor is a set of independent minimum-demands (each coordinate optional), so an author CAN write an incoherent floor (e.g. bearer-Dropped + bond-Intact). This is harmless — each demanded - coordinate is checked independently — but is an author-error surface, not covered - by the HC-4 unrepresentability claim. (Audit 2026-06-22.) - -== Soundness advance (2026-06-22) - -Newly machine-checked in `Trope.Order` + `Trope.Soundness` (no axioms): - -* *⊑ is a preorder* — reflexivity (Trope.Coords) + *transitivity* (`fateLteTrans`, - `bondLteTrans`, `mergeLteTrans`, `dLteTrans`, assembled to `gradeLteTrans`). -* *Verdict-soundness corollary* (`verdictSound`) — `floor ⊑ g ∧ g ⊑ ρ ⟹ floor ⊑ ρ`. - This is the calculus §8 corollary, now proved (it is exactly transitivity of ⊑). -* *T-Sub soundness* (`subSound`) — `g' ⊑ g ∧ g ⊑ ρ ⟹ g' ⊑ ρ`. -* *Grade soundness for EXACT faithful lowering* (`soundFromExact`) — if the declared - grade equals the observed retention (the strongest faithful lowering, O2), then - `g ⊑ ρ`, via congruence of ▷ + reflexivity. No L4 needed. -* *L4 monotonicity holds for the chain coordinates* bond and merge - (`bondComposeMono`, `mergeComposeMono`). - -=== FINDING: strict L4 monotonicity FAILS for the fate coordinate - -`Trope.Soundness.fateL4MonotonicityFails` machine-checks a counterexample: -`Dropped ⊑ Present` and `Predicated ⊑ Predicated`, yet -`Dropped ▷ Predicated = Dropped` while `Present ▷ Predicated = Predicated`, and -`Dropped ⋢ Predicated` (Predicated and Dropped are *intentionally incomparable*, -calculus §3.1). So strict L4 does not hold for fate; the calculus's "L4 is a *lax* -compatibility" (§5 note) is load-bearing. Consequence: grade soundness for -*conservative* (inexact) steps cannot be composed by naive L4 over the fate -coordinate; the *exact* route (`soundFromExact`) sidesteps it, and bond/merge remain -monotone. - -=== Still open (narrowed) - -* Grade soundness for *conservative* lowering over fate — needs the lax argument the - calculus hints at, not strict L4. -* The operational model of the term language + `fix` (calculus §7) and a definition - of observed retention `ρ` over executions — the deeper part of the open problem. - *This is now named CO-1, the repository's central open problem (see the next - section); the two streams converge on it.* - -== Grade-algebra boundary + Theorem B metatheory (2026-06-23) - -Two work-streams landed against the *authoritative Lean ground truth* -`verification/proofs/lean4/grade-boundary/GradeBoundary.lean` (Lean 4 v4.16.0 + -Mathlib, sorry-free; `#print axioms` = `propext`/`Quot.sound` only — built green this -date, no `sorryAx`/user-`axiom`/`native_decide`): - -* *Stream A* — `spec/calculus-v0.2-draft.adoc`: a v0.2 spec addendum lifting the - proved algebra into obligations `R-2026-06-23-01..04`. -* *Stream B* — `verification/proofs/agda/theorem-b/` (Agda `--safe --without-K`, - *zero postulates*; `All.agda`/`Smoke.agda` green this date): the calculus - metatheory (Theorem B). - -Full reconciliation — the unified R-id ↔ Lean ↔ Agda ↔ status table, the convergence -analysis, and the divergence adjudication — is in -`verification/proofs/INTEGRATION-REPORT.adoc`. Headlines: - -=== Proved (this date) - -[cols="1,3",options="header"] -|=== -| Result | Where - -| *Three-tier strict cancellation boundary* stem:[\mathcal{C} \subsetneq \mathcal{H} - \subsetneq \mathcal{G}] — cancellation holds *only* on the finite-fidelity core and - fails on the honest-but-lossy and deceptive tiers alike (the non-cancellative set - *strictly* contains the deceptive set) -| Lean `honest_fidelity_cancel` (core) + `grade_not_leftCancel` (L5) + absorbing & - honest-not-cancel witnesses; Agda `TB.Tier` (`core-closed-▷`, `Q-cancelʳ`, six - `*-not-cancel`, `deceptive-absorbs-▷`). (A: R-2026-06-23-03; B: F4.) - -| *F2 — `▷` is non-commutative* (witness `dropped`/`falsified`), so `CommMonoid` / - special-Frobenius cannot model it — *now strengthened* by B's impossibility result: - *symmetric (orientation-free) computational cut is impossible* -| Lean `grade_mul_not_comm`, `Fate.not_comm`; Agda `grade-not-comm`, - `cut-symmetric-fails` (= `grade-not-comm`), `cut-orientation-matters`. (A: - R-2026-06-23-01; B: F2 + Target 2 refutation.) - -| *F2×F4 interaction — tier-preservation is CLOSURE, not a homomorphism.* The naïve - `tierOf (g ▷ h) ≡ tierOf g ⊓ tierOf h` is *false* on fate (`dropped ▷ falsified = - dropped` honest, shielding a later deceptive `falsified`); same phenomenon as the - strict-L4 failure -| Agda `TB.Tier.fate-tier-meet-hom-fails`, guarded by `fate-L4-fails` - (≡ Idris `Soundness.fateL4MonotonicityFails`). (B: F2×F4 finding.) - -| *Partition correction — `Dropped` and `Total` are HONEST*, not deceptive (absorbing - yet truthful). The non-cancellative set partitions as honest-but-lossy - (`dropped`/`predicated`/`severed`/`total`, +`withheld`/`fused`) versus deceptive - (`falsified`/`misbound`/`conflated`/`unknown`) -| Lean `dropped_absorbing`, `fidelity_total_honest_not_cancel`, `total_add_Q`, - `total_add_unknown`; Agda `TB.Tier` classifiers. (A: R-2026-06-23-04; B: F4.) - -| *Value substitution is grade-exact* ("tropes follow values through cut"); *honesty - is closed under ▷* so deceptive grades are unreachable from honest terms (HC-3) -| Agda `TB.Substitution.subst`/`cut-preserves-grade` (Target 2); - `TB.Honest.honest-closed-▷` + atom-honesty (Target 4). -|=== - -=== Theorem B — true per-target status (NOT rounded up) - -[cols="1,3",options="header"] -|=== -| Target | Status - -| *1* — encode the grade as a non-commutative graded structure (intrinsic calculus) | *PROVED* -| *2* — substitution-admissibility / reindexing | *PROVED* (+ `cut-symmetric-fails` refutation) -| *3* — subject reduction respecting the F4 boundary | *PARTIAL — INCOMPLETE.* β/let core PROVED (intrinsic SR; tier preserved exactly); *`fix`/lfp NOT-REACHED* (no postulate), blocked on CO-1 + O4. *There is no full subject reduction and no operational model yet.* -| *4* — Honest Generation (HC-*) + Veridicality (L*) | *PROVED* -|=== - -=== CO-1 — CENTRAL OPEN PROBLEM (the repository's headline gap) - -*The calculus has no operational model (reduction dynamics) for its grade-routing / -iterating constructs.* v0.1 is a pure type-and-grade discipline; reduction beyond the -β/let core is undefined. The two streams *converge on this single hole* from opposite -sides — recorded as ONE item, not two: - -* *Spec face (= A's OPEN-A):* the lossless fractional *split / rejoin / routing* - operator whose cancellability R-2026-06-23-03 constrains-in-advance is referenced - but *undefined* (no typing rule, no dynamics). -* *Proof face (= B's Target-3 fixpoint case):* `fix`/lfp subject reduction is - *NOT-REACHED* — no ↝ rule for `fix`, no observed-retention `ρ`. -* *Additionally gated by v0.1 O4* (the `Conat`-vs-tag limit carrier for ordering - iterated attenuation beyond stem:[\omega]) — B's second missing piece, which *is* - v0.1's pre-existing O4. - -The grade algebra is *not* at fault (the lfp endpoint stem:[\{total, unknown\}] is -already ▷-fixed and tier-stable). *Entanglement:* v0.1 §7 justifies the `fix` lfp -grade "by L4 monotonicity", but strict L4 is machine-proved to *fail on fate* -(`fate-L4-fails`) — so even the grade-side `fix` justification rests on a monotonicity -now known only to be lax. - -=== Documentation-reconciliation gaps (recorded, not filled — for the merge author) - -* *OPEN-A* — folded into CO-1 above. -* *OPEN-B* — `Falsified` (fate's deceptive bottom, dual of honest `Dropped`) is in the - proved carrier but absent from v0.1 §3.1's four-inhabitant fate table. *OPEN-B′ - (surfaced during integration)* — the analogous gap holds for `Misbound` (bond's - deceptive bottom), absent from v0.1 §3.2's three-inhabitant bond table. (Merge's - `Conflated` is already in v0.1 §3.3.) Whether to amend v0.1 §3.1/§3.2 normatively is - a documentation decision, not fixed by F1–F4. -* *OPEN-C* — tier-2 membership is recorded, not exhaustively proved: the harness - witnesses *representative* honest-but-lossy elements non-cancellative - (`predicated`/`severed`/`total`, +`dropped`); `Withheld` and `Fused` sit in tier 2 - by the carrier's order structure but carry no individual named non-cancellation - witness in either development. + coordinate is checked independently — but is an author-error surface, not + covered by the HC-4 unrepresentability claim. (Audit 2026-06-22.) + +== History + +Superseded by R-2026-07-07 (ADR 0004) where they disagree. The pre-ratification +theorems are retained in their files under provenance notes and remain true of +the v0.1 carrier. + +*2026-06-22.* First verified core (Idris2): L1, L2, decidability of ⊑, +Veridicality Derivation, Honest Generation, ε honest and coherent. Soundness +advance: ⊑ a preorder, `verdictSound`, `subSound`, `soundFromExact`, +monotonicity for bond and merge. A machine-checked FINDING that strict L4 fails +on the v0.1 fate coordinate (`fateL4MonotonicityFails`, since removed with the +carrier it described) made L4 lax and blocked conservative grade soundness; +both are resolved on the ratified carrier (L4 row above). O1 exhaustiveness and +L4/L5 as standalone lemmas were listed open; both are now proved (O1-carrier, +L4, L5 rows). + +*2026-06-23.* Grade-algebra boundary in Lean (`GradeBoundary.lean`: +`grade_mul_not_comm`, `grade_conical`, `grade_not_leftCancel`, +`honest_fidelity_cancel`, `fidelity_unknown_not_cancel`, +`fidelity_total_honest_not_cancel`, `dropped_absorbing`) and Theorem B in Agda +(Targets 1, 2, 4 proved; Target 3 partial). The v0.1 carrier's ▷ was shown not +commutative, symmetric cut impossible, and tier preservation closure rather than +a homomorphism; the first two were artefacts of the clause (A1) removed and the +third survives (C3 row). CO-1 was named the central open problem and recorded as +additionally gated by the limit-carrier question O4, which ADR 0004 resolved. +Documentation gaps on the v0.1 fate and bond tables and on tier-2 witnesses were +recorded; the tables are complete in spec v0.2 §3 and the witnesses are +`TierTwoComplete.lean`. + +*2026-06-29.* Tropical factorisation probe on the v0.1 carrier +(`GradeFactorisation.lean`: `forced_collapse_general`, `forced_collapse_grade`): +a homomorphism onto the commutative tropical carrier existed but every such map +was forced to identify `Dropped` with `Falsified`. Re-run on the ratified +carrier the verdict is (B′) sighted (Factorisation row above). The probe was and +is a precondition, not a recursion result. From 444e4cf8e29cf375d7af60a96d5d466526b4a097 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 27 Oct 2026 07:55:11 +0000 Subject: [PATCH 04/15] =?UTF-8?q?docs(status):=20ROADMAP=20=E2=80=94=20shi?= =?UTF-8?q?p=20v0.2,=20point=20open=20problems=20at=20spec=20=C2=A710?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit What was wrong: ROADMAP listed v0.2 as "in progress" with the v0.1 vocabulary (CO-1 "gated by O4", the lax-L4 argument, OPEN-B/B′/C, a separate spec addendum) although the carrier was ratified on 2026-07-07 and the spec consolidated at v0.2. What changed: "Shipped (v0.2)" lists the ratified carrier (ADR 0004), the Agda carrier migration, L4 in full and L6, the atom factorisation (O1-carrier), TierTwoComplete, the sighted factorisation re-run and the spec consolidation; "Open problems" defers to spec/calculus.adoc §10 by reference and names CO-1 mechanisation as the next proof work; Deferred items kept. What I ran: grep for "gated by O4|lax|OPEN-B|OPEN-C" over the file — no hits. What I did not run: nothing else; documentation-only. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01J4QvDh3p24SCUjyM9HHT31 --- docs/status/ROADMAP.adoc | 61 +++++++++++++++++++--------------------- 1 file changed, 29 insertions(+), 32 deletions(-) diff --git a/docs/status/ROADMAP.adoc b/docs/status/ROADMAP.adoc index 3c78303..a9736a6 100644 --- a/docs/status/ROADMAP.adoc +++ b/docs/status/ROADMAP.adoc @@ -4,12 +4,11 @@ == Current status -Alpha. The schema, executable checker (Idris2), and conformance suite are green; the -verified core typechecks with no axioms behind its claimed lemmas. The grade-algebra -*honest/deceptive cancellation boundary* is proved in Lean (sorry-free, axiom-clean) -and its metatheory partially developed in Agda (Theorem B). Ground truth and true -statuses: `docs/status/PROOF-STATUS.adoc`, `AFFIRMATION.adoc`, -`verification/proofs/INTEGRATION-REPORT.adoc`. +Alpha. The schema, the Idris2 reference checker, the Rust fast core and the +conformance suite are green; the verified developments carry no axioms behind +their claimed lemmas. Spec v0.2 is the normative document; what is proved and +what is open: `docs/status/PROOF-STATUS.adoc`, `AFFIRMATION.adoc`, +`spec/calculus.adoc §10`. == Shipped (v0.1) @@ -19,34 +18,32 @@ statuses: `docs/status/PROOF-STATUS.adoc`, `AFFIRMATION.adoc`, * [x] Soundness advance: ⊑-preorder, verdict-soundness corollary, T-Sub soundness, grade soundness for *exact* faithful lowering (machine-checked). -== In progress (v0.2 — grade algebra + metatheory) - -* [x] Grade-algebra boundary proved in Lean 4 + Mathlib (`grade-boundary/`): non-commutative - product monoid; full-carrier conicality; three-tier strict cancellation boundary. -* [x] Spec v0.2 addendum: obligations `R-2026-06-23-01..04` bound to the governing Lean theorems. -* [x] Theorem B (Agda, `--safe --without-K`, zero postulates): Targets 1/2/4 PROVED. -* [~] Theorem B Target 3 (subject reduction respecting the boundary): *PARTIAL* — β/let proved; - `fix`/lfp NOT-REACHED (blocked on CO-1). -* [x] Tropical factorisation probe (`grade-factorisation/`, Lean 4 + Mathlib): verdict *(B) factors but - veridicality-blind* — a nontrivial commutative cost-quotient exists, but every commutative-target hom - is forced to collapse honest `dropped` / deceptive `falsified` (blindness co-located with the fate-axis - non-commutativity). A *precondition only*; recursion stays parked behind CO-1 (issue #10). - -== Open problems (named, not solved) - -* *CO-1 (central):* the calculus has *no operational model* for `fix`/routing dynamics — there is - no reduction rule for `fix` and no observed-retention `ρ`. Gated additionally by v0.1's *O4* (the - limit carrier for ordering iterated attenuation beyond ω, the `Conat`-vs-tag fork). Resolving CO-1 - unblocks full subject reduction (Theorem B Target 3). -* Grade soundness for *conservative* (inexact) lowering over fate — needs the lax-L4 argument - (strict L4 is machine-proved to fail on fate). -* *O1* exhaustiveness of the seven effects; *O2* per-front-end lowering correctness; *O3* the - produce/demand adjunction. -* Documentation reconciliation: *OPEN-B/B′* (`Falsified`/`Misbound` absent from v0.1 §3.1/§3.2); - *OPEN-C* (`Withheld`/`Fused` tier-2 membership not individually witnessed). +== Shipped (v0.2) + +* [x] Ratified carrier (ADR 0004, R-2026-07-07): two-sided deceptive zeros (A1), the fate + chain (A2), `Attenuated(0)` normalisation at ingest (A3); IR 0.2 semantics. +* [x] Agda Theorem B migrated to the ratified carrier (`--safe --without-K`, zero postulates): + Targets 1, 2, 4 proved; Target 3 β/let proved. +* [x] L4 monotonicity in full, both arguments, every coordinate (Idris2, Lean, Agda); L6 + commutativity. +* [x] Atom factorisation — O1-carrier proved (`EffectAtoms.lean`): nine atom families. +* [x] Tier-2 cancellation membership exhaustive (`TierTwoComplete.lean`). +* [x] Tropical factorisation re-run on the ratified carrier: (B′) factors and + veridicality-sighted (`GradeFactorisationR.lean`). +* [x] Spec consolidated at v0.2: one normative document on the ratified carrier; O5 defined, + O6 opened; prover roles per ADR 0005 (Proposed). + +== Open problems + +The authoritative list is `spec/calculus.adoc §10` — O1-coord, O2, O3, O5 mechanisation, +O6, CO-1 mechanisation — each with its status word; `docs/status/PROOF-STATUS.adoc` "Open" +restates it with where each is specified. CO-1 mechanisation (Agda, steps 1–5 of +`spec/notes/2026-07-07-co1-operational-model.adoc §6`) is the next proof work; it closes +Theorem B Target 3 and conservative grade soundness. == Deferred * Full Haec compiler / codegen / runtime (the `haec` repo). -* Rust fast-core hardening (drafted in `src/rust/`, dep-free, validated against the Idris2 reference). +* Rust fast-core hardening (fuzzing, perf); it already agrees with the Idris2 reference over + the conformance corpus (`just trope-rust`). * Filing the panic-attack signed-suppression proposal (`docs/proposals/`) upstream. From e59ef9c2a6680ad5ecf603a79402887b38ee007e Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 27 Oct 2026 08:15:39 +0000 Subject: [PATCH 05/15] docs(affirmation): add the 2026-10-27 entry from a full re-run MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit What was wrong: the newest AFFIRMATION entry (2026-06-29) described the v0.1 carrier and cited 10/10 conformance cases and 8 schema-invalid fixtures; the corpus has been 13 + 9 for months and the carrier was ratified on 2026-07-07. What changed: a dated entry with an anchor (branch, commit, UTC time, exact toolchain), one bullet per command, a short proved/open paragraph naming only identifiers that exist, and two findings; :revdate: bumped. What I ran (all in this session, on this branch): idris2 --typecheck verification/proofs/idris2/trope.ipkg -> exit 0 just trope-build && bash tests/conformance/run.sh -> 13 + 9, all pass just trope-rust -> 13 + 9, all pass just build-agda -> PASS (All + Smoke) apt agda 2.6.3 + agda-stdlib 1.7.3 on All.agda -> exit 42 (finding 1) lean-source-honesty regexes over 8 .lean files -> clean What I did not run: just build-lean (no lake / Mathlib reachable here) — written as NOT RUN with the command named; the proofs.yml lean-build job is the attestation and is cited in the PR. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01J4QvDh3p24SCUjyM9HHT31 --- AFFIRMATION.adoc | 52 +++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 51 insertions(+), 1 deletion(-) diff --git a/AFFIRMATION.adoc b/AFFIRMATION.adoc index 153f531..3cf8e88 100644 --- a/AFFIRMATION.adoc +++ b/AFFIRMATION.adoc @@ -2,7 +2,7 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 // SPDX-License-Identifier: CC-BY-SA-4.0 = AFFIRMATION — trope-checker -:revdate: 2026-06-24 +:revdate: 2026-10-27 A dated, ground-truthed honesty snapshot (the README/EXPLAINME/AFFIRMATION trio). This is the brief's "STATUS" deliverable: what is proved, what is stubbed-and-named, @@ -78,3 +78,53 @@ Documentation gaps OPEN-B/B′ (`Falsified`/`Misbound` absent from v0.1 §3.1/§ proved-vs-missing picture: `verification/proofs/INTEGRATION-REPORT.adoc`. — Authored by the build agent under owner direction; signed in git history. + +== As of 2026-10-27 — Phase 0 re-run on the ratified world + +*Anchor.* Branch `claude/new-session-snuoro` at `444e4cf` (`main` 216f23b + the v0.2 +consolidation + the `proofs.yml` pin), 2026-10-27T07:56Z, in an Ubuntu 24.04 cloud +container. Toolchain: Agda 2.7.0.1 + agda-stdlib 2.0 (tag `v2.0`, commit `2b8fff1`); +Idris2 0.8.0 (built from tag `v0.8.0` on Chez Scheme 9.5.8); rustc 1.97.0; just 1.40.0. + +*Ground truth (commands run here):* + +* `idris2 --typecheck verification/proofs/idris2/trope.ipkg` → exit 0; 8 modules, all + `%default total`; no `believe_me` / `assert_total` / `postulate` in + `verification/proofs/idris2` or `src/idris2`. +* `just trope-build && bash tests/conformance/run.sh` → the reference `tropecheck` + builds; *13* verdict cases pass with the expected witness edge and coordinate; *9* + schema-invalid documents are rejected at the named slot; "conformance: all pass". +* `just trope-rust` → `tropecheck-rs` builds; the same 13 + 9 pass — the Rust fast core + and the Idris2 reference agree over the whole corpus. +* `just build-agda` → `agda --safe --without-K All.agda` and `Smoke.agda` exit 0 + (77 s and 5 s cold; 12 s together with cached interfaces). +* `just build-lean` → *NOT RUN here*: `lake` is not installed and the Lean toolchain + and Mathlib cache hosts were unreachable from this container. The + `lean-source-honesty` regexes of `proofs.yml` were run by hand over all 8 tracked + `.lean` files: no `sorry` / `admit` / `native_decide`, no user `axiom`. The build and + axiom audit are the `proofs.yml` `lean-build` job; its run on this branch is cited in + the Phase 0 pull request. + +*Proved* (machine-checked; names in `docs/status/PROOF-STATUS.adoc`): L1–L6 on the +ratified carrier, L4 in full (`fateL4MonoR/L`, `bondComposeMono`, `mergeComposeMono`); +the decidable retention preorder; the Veridicality Derivation and Honest Generation; +C1–C3 (`GradeR.conical`, `gradeR_leftCancel_iff`, `TierTwoComplete`, +`fate-tier-meet-hom-fails`); O1-carrier (`atom_factorization`); the sighted tropical +factorisation (`piR_sighted`); Theorem B Targets 1, 2, 4 and the β/let case of 3 +(`cut-preserves-grade`, `β-app`, `β-let`); grade soundness for exact lowering, +T-Sub and verdict soundness (`soundFromExact`, `subSound`, `verdictSound`). *Open* +(`spec/calculus.adoc §10`): CO-1 mechanisation (the `fix` case; designed, not +mechanised), O1-coord, O2, O3, O5 mechanisation, O6. + +*Two findings.* (1) Ubuntu 24.04's apt pair (Agda 2.6.3, agda-stdlib 1.7.3) cannot +typecheck Theorem B: `agda --safe --without-K All.agda` exits 42, `Data.Product.Base` +not found — stdlib ≥ 2.0 is required, which is why `proofs.yml` now pins Agda 2.7.0.1 ++ stdlib 2.0 by checksum (reproduced here, 58 s). (2) The 2026-06-22 entry's "10/10" +and "8 schema-invalid" were stale: the corpus is 13 + 9. Also observed: `just +proof-check-all` is red for reasons that predate this pass (per-file `idris2 --check` +and `agda --safe` from the repo root cannot resolve module names; the ABI/Types Idris2 +mint templates do not typecheck) — recorded as an issue, not fixed here; the gates +that mean something are `just check`, `just build-agda`, `just trope-rust` and +`verify-all`. + +— Run by the Phase 0 agent; the owner signs on landing. From 2cee6704f6a167e3d0663cacdbeacfec89136e19 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 27 Oct 2026 08:15:39 +0000 Subject: [PATCH 06/15] =?UTF-8?q?proofs(agda):=20Reduction=20footer=20?= =?UTF-8?q?=E2=80=94=20O4=20is=20resolved;=20the=20fix=20case=20waits=20on?= =?UTF-8?q?=20CO-1=20alone?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit What was wrong: the NOT-REACHED footer of TB/Reduction.agda listed two obstructions to fix-subject-reduction, the second being "a LIMIT CARRIER … the open O4 fork (Conat-vs-tag)". ADR 0004 resolved O4 on 2026-07-07 (the finitary carrier suffices; transfinitely deep fix is inexpressible), and the operational model has since been designed. What changed (comment only, no code): the footer now states one obstruction — the operational model — DESIGNED in spec/notes/2026-07-07-co1-operational-model.adoc (λ-trope, tagged values, T-Fix-Decl) with its mechanisation plan (that note's §6, steps 1–5, extending this module), records O4 as RESOLVED by ADR 0004, and keeps "NOT-REACHED, NO postulate" and the tier-stability remark. What I ran: just build-agda (agda --safe --without-K All.agda + Smoke.agda) with this edit in the tree -> PASS, exit 0. What I did not run: nothing else applies. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01J4QvDh3p24SCUjyM9HHT31 --- .../proofs/agda/theorem-b/TB/Reduction.agda | 45 +++++++++++-------- 1 file changed, 27 insertions(+), 18 deletions(-) diff --git a/verification/proofs/agda/theorem-b/TB/Reduction.agda b/verification/proofs/agda/theorem-b/TB/Reduction.agda index 3b52555..19e08de 100644 --- a/verification/proofs/agda/theorem-b/TB/Reduction.agda +++ b/verification/proofs/agda/theorem-b/TB/Reduction.agda @@ -113,28 +113,37 @@ seq-stays-core : ∀ {Γ A B g₁ g₂} → Γ ⊢ A ! g₁ → (Γ , A) ⊢ B ! seq-stays-core {g₁ = g₁} {g₂ = g₂} _ _ c₁ c₂ = core-closed-▷ g₁ g₂ c₁ c₂ -------------------------------------------------------------------------------- --- fix / lfp — NOT-REACHED (precise statement; NO postulate). +-- fix — NOT-REACHED (precise statement; NO postulate). -------------------------------------------------------------------------------- --- The calculus's general recursion (`fix`, §7) grades a recursive trope- --- transformer by the LEAST FIXED POINT of its grade functional. Subject --- reduction for the fix-unfold step +-- The calculus's general recursion (`fix`, spec §7) grades a recursive trope- +-- transformer by the greatest post-fixed point of its grade functional in the +-- retention order (the least fixed point in the loss order), checked by the +-- declared-signature rule T-Fix-Decl. Subject reduction for the fix-unfold step -- -- fix x. e ↝ e [ fix x. e / x ] -- --- is NOT-REACHED here, and is NOT postulated. Two things are genuinely missing, --- exactly as flagged by the spec (§7, O4) and PROOF-STATUS: +-- is NOT-REACHED here, and is NOT postulated. One thing is missing: -- --- (1) an OPERATIONAL model: there is no ↝ rule for fix and no definition of --- the observed retention ρ against which grade soundness for the unfold --- would be stated. (The spec is a type DISCIPLINE; reduction beyond β/let --- is not given.) --- (2) a LIMIT CARRIER for the lfp grade: ordering iterated unbounded --- attenuation beyond ω is the open O4 fork (Conat-vs-tag). The lfp's --- fidelity lands in the absorbing tops {total, unknown}, which ARE --- ▷-fixed (TB.Grade.total-absorb-Q, unknown-absorbL) — so the GRADE is --- tier-stable — but the operational unfold-preserves-tier step needs (1)+(2). +-- (1) the OPERATIONAL model: there is no ↝ rule for fix in this module and no +-- definition of the observed retention ρ against which grade soundness +-- for the unfold would be stated. The model is DESIGNED in +-- spec/notes/2026-07-07-co1-operational-model.adoc — the core language +-- λ-trope, an instrumented small-step semantics with tagged values v@h +-- (ρ is read off the output tag), and T-Fix-Decl (accept iff γ ⊑ F(γ); +-- no fixed point is computed). Its mechanisation plan is that note's §6, +-- steps 1–5, extending THIS module: tag erasure commutes with reduction; +-- each atomic-move step emits exactly the typing rule's grade; T-Sub and +-- application via TB.Order.fateL4Mono{R,L}; F monotone in the assumed +-- latent grade; T-Fix-Decl soundness by induction on call depth. +-- +-- What used to be listed as a second obstruction — a LIMIT CARRIER for ordering +-- iterated attenuation beyond ω, the O4 fork (Conat-vs-tag) — is RESOLVED by +-- ADR 0004: the finitary carrier ℕ ∪ {∞, ⊤} suffices, because transfinitely +-- deep `fix` nesting is inexpressible in finitary syntax. The gfp's fidelity +-- lands in the absorbing tops {total, unknown}, which ARE ▷-fixed +-- (TB.Grade.total-absorb-Q, unknown-absorbL), so the GRADE is tier-stable; only +-- the operational unfold-preserves-tier step, item (1), remains. -- -- The honest verdict for fix-subject-reduction is therefore NOT-REACHED, with --- the obstruction characterised: it is the missing operational semantics + the --- O4 limit carrier, NOT a defect of the grade algebra (whose lfp endpoint is --- already tier-stable). +-- the obstruction characterised: the mechanisation of the designed operational +-- model (CO-1), NOT a defect of the grade algebra. From a5958454f46588da3cf18dfbb453ec735ac5dd26 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 27 Oct 2026 08:15:39 +0000 Subject: [PATCH 07/15] chore(proofs): remove the three never-instantiated prover templates MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit What was wrong: verification/proofs carried TypeSafety.v (Coq), StateMachine.tla (TLA+) and Properties.agda — mint templates whose own text says "Replace with your project's …", never instantiated — and the trees, usage lines and recipes advertised a fourth and fifth prover the roles ruling does not assign here. What changed: git rm of the three files; their lines dropped from the verification/proofs/README.adoc and docs/status/PROOF-NEEDS.adoc trees and the `just proof-check-coq` usage line; proof-check-coq removed from proof-check-all and the Coq/TLA+ lines from proof-status (proof-scan-dangerous keeps its harmless -name '*.v'); the awk's historical false-positive note no longer names the removed file by path. The INTEGRATION-REPORT mention stays as history. What I ran: git grep -n "TypeSafety\|StateMachine\|Properties.agda" -> only INTEGRATION-REPORT.adoc; just proof-status -> runs (Idris2 14, Lean4 8, Agda 9 files); just proof-check-all -> runs and is red for pre-existing reasons unrelated to this change (per-file idris2/agda checks from the repo root cannot resolve module names; the ABI/Types Idris2 mint templates do not typecheck) — recorded in AFFIRMATION and as an issue; just proof-scan-dangerous -> PASS. What I did not run: coqc / tlc (not installed, and no longer referenced). Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01J4QvDh3p24SCUjyM9HHT31 --- build/just/proofs.just | 8 +- docs/status/PROOF-NEEDS.adoc | 8 +- tests/lib/strip-proof-comments.awk | 2 +- verification/proofs/README.adoc | 14 +-- verification/proofs/agda/Properties.agda | 37 -------- verification/proofs/coq/TypeSafety.v | 73 ---------------- verification/proofs/tlaplus/StateMachine.tla | 91 -------------------- 7 files changed, 10 insertions(+), 223 deletions(-) delete mode 100644 verification/proofs/agda/Properties.agda delete mode 100644 verification/proofs/coq/TypeSafety.v delete mode 100644 verification/proofs/tlaplus/StateMachine.tla diff --git a/build/just/proofs.just b/build/just/proofs.just index 8d1d63a..6f3cb64 100644 --- a/build/just/proofs.just +++ b/build/just/proofs.just @@ -4,12 +4,12 @@ # FORMAL VERIFICATION (PROOFS) # # Imported by ../../Justfile via `import? "build/just/proofs.just"`. -# Recipes here check formal proofs across Idris2, Lean4, Agda, and Coq, plus +# Recipes here check formal proofs across Idris2, Lean4 and Agda, plus # scan for dangerous/unsafe constructs and report status. Run via # `just proof-check-all` for the full sweep. -# Check all formal proofs (Idris2 + Lean4 + Agda + Coq) -proof-check-all: proof-check-idris2 proof-check-lean4 proof-check-agda proof-check-coq proof-scan-dangerous +# Check all formal proofs (Idris2 + Lean4 + Agda) +proof-check-all: proof-check-idris2 proof-check-lean4 proof-check-agda proof-scan-dangerous @echo "=== All proof checks complete ===" # Check Idris2 proofs (ABI, types, dependent type proofs) @@ -150,8 +150,6 @@ proof-status: echo "Idris2: $(find verification/proofs/idris2 -name '*.idr' 2>/dev/null | wc -l) files" echo "Lean4: $(find verification/proofs/lean4 -name '*.lean' 2>/dev/null | wc -l) files" echo "Agda: $(find verification/proofs/agda -name '*.agda' 2>/dev/null | wc -l) files" - echo "Coq: $(find verification/proofs/coq -name '*.v' 2>/dev/null | wc -l) files" - echo "TLA+: $(find verification/proofs/tlaplus -name '*.tla' 2>/dev/null | wc -l) files" echo "" # PROOF-STATUS may live at root, docs/status/ (post-#20), .md or .adoc (post-#23) for candidate in docs/status/PROOF-STATUS.adoc docs/status/PROOF-STATUS.md PROOF-STATUS.adoc PROOF-STATUS.md; do diff --git a/docs/status/PROOF-NEEDS.adoc b/docs/status/PROOF-NEEDS.adoc index 11f5cc7..d571ecb 100644 --- a/docs/status/PROOF-NEEDS.adoc +++ b/docs/status/PROOF-NEEDS.adoc @@ -113,12 +113,8 @@ verification/proofs/ │ └── *.idr # Project-specific Idris2 proofs ├── lean4/ # Lean4 proofs (algebra, lattices) │ └── *.lean -├── agda/ # Agda proofs (induction, metatheory) -│ └── *.agda -├── coq/ # Coq proofs (type systems, compilation) -│ └── *.v -└── tlaplus/ # TLA+ specs (distributed protocols) - └── *.tla +└── agda/ # Agda proofs (induction, metatheory) + └── *.agda ---- == References diff --git a/tests/lib/strip-proof-comments.awk b/tests/lib/strip-proof-comments.awk index 2d8db02..ffad89f 100644 --- a/tests/lib/strip-proof-comments.awk +++ b/tests/lib/strip-proof-comments.awk @@ -2,7 +2,7 @@ # # Line-based filtering is not enough: a Coq (* ... *) or Lean /- ... -/ block # spans lines, and a CONTINUATION line carries no marker of its own. Measured -# 2026-07-29: verification/proofs/coq/TypeSafety.v:6 ("All proofs must be +# 2026-07-29: line 6 of the (since removed) Coq proof template ("All proofs must be # complete - NO Admitted allowed.") is line 6 of a block comment and was # reported as a dangerous construct -- i.e. the repo was failed for DOCUMENTING # that it forbids Admitted. diff --git a/verification/proofs/README.adoc b/verification/proofs/README.adoc index f1f0bc2..d2e0e69 100644 --- a/verification/proofs/README.adoc +++ b/verification/proofs/README.adoc @@ -25,14 +25,9 @@ proofs/ │ │ # boundary (Lean 4 + Mathlib; sorry-free; propext/Quot.sound only) │ └── grade-factorisation/ # tropical factorisation probe: imports the carrier; verdict (B) │ # factors but veridicality-blind (precondition only; not CO-1) -├── agda/ # Agda proofs (induction, metatheory) -│ ├── Properties.agda -│ └── theorem-b/ # Theorem B: calculus metatheory over the grade algebra -│ # (Agda --safe --without-K; zero postulates) -├── coq/ # Coq proofs (type systems, compilation) -│ └── TypeSafety.v -└── tlaplus/ # TLA+ specs (distributed protocols) - └── StateMachine.tla +└── agda/ # Agda proofs (induction, metatheory) + └── theorem-b/ # Theorem B: calculus metatheory over the grade algebra + # (Agda --safe --without-K; zero postulates) ---- == Verification Commands @@ -43,7 +38,6 @@ just proof-check-all # Run all proof checkers (per-file scan + dangerous-p just proof-check-idris2 # Idris2 only just proof-check-lean4 # Lean4 only just proof-check-agda # Agda only -just proof-check-coq # Coq only # The two pinned developments need a real build (lake+Mathlib / an All.agda entry), # not a bare per-file check — use these: @@ -75,7 +69,7 @@ is advisory, not a CI gate. CI enforcement is `panic-attack assail`. == Adding New Proofs 1. Choose the appropriate prover (see `../../docs/status/PROOF-NEEDS.adoc`) -2. Create the `.idr`/`.lean`/`.agda`/`.v`/`.tla` file in the right directory +2. Create the `.idr`/`.lean`/`.agda` file in the right directory 3. Ensure `%default total` (Idris2) or equivalent 4. Run the verification command 5. Update `../../docs/status/PROOF-STATUS.adoc` diff --git a/verification/proofs/agda/Properties.agda b/verification/proofs/agda/Properties.agda deleted file mode 100644 index d78d9d0..0000000 --- a/verification/proofs/agda/Properties.agda +++ /dev/null @@ -1,37 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) --- --- Agda Proof Template: Inductive and coinductive properties --- Replace with your project's domain-specific proofs. --- All proofs must be total (no postulate, no {-# TERMINATING #-}). - -module Properties where - -open import Data.Nat using (ℕ; zero; suc; _+_; _≤_; z≤n; s≤s; _<_) -open import Data.Nat.Properties using (+-comm; +-assoc; ≤-refl; ≤-trans) -open import Data.List using (List; []; _∷_; length; _++_) -open import Data.List.Properties using (length-++ ) -open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; sym; trans) - --- Example: Proof that list append preserves total length --- Replace with your project's domain proofs. - -append-length : ∀ {A : Set} (xs ys : List A) → - length (xs ++ ys) ≡ length xs + length ys -append-length xs ys = length-++ xs - --- Example: Monotonicity proof template --- Use for state machines, confidence scores, trust levels -record Monotone {A : Set} (_≤A_ : A → A → Set) (f : A → A) : Set where - field - preserves : ∀ {x y} → x ≤A y → f x ≤A f y - --- Example: Idempotence proof template --- Use for normalisation, deduplication, formatting -record Idempotent {A : Set} (_≡A_ : A → A → Set) (f : A → A) : Set where - field - idem : ∀ (x : A) → f (f x) ≡A f x - --- Example: Natural number successor is monotone -suc-monotone : Monotone _≤_ suc -suc-monotone = record { preserves = s≤s } diff --git a/verification/proofs/coq/TypeSafety.v b/verification/proofs/coq/TypeSafety.v deleted file mode 100644 index 8f5b418..0000000 --- a/verification/proofs/coq/TypeSafety.v +++ /dev/null @@ -1,73 +0,0 @@ -(* SPDX-License-Identifier: MPL-2.0 *) -(* Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) *) -(* - Coq Proof Template: Type system soundness - Replace with your project's type system proofs. - All proofs must be complete — NO Admitted allowed. -*) - -Require Import Coq.Lists.List. -Require Import Coq.Arith.Arith. -Require Import Coq.Bool.Bool. -Import ListNotations. - -(** * Example: Simple expression language with type safety *) -(** Replace this entire section with your project's type system. *) - -(** Types *) -Inductive ty : Type := - | TyNat : ty - | TyBool : ty. - -(** Expressions *) -Inductive expr : Type := - | EConst : nat -> expr - | ETrue : expr - | EFalse : expr - | EPlus : expr -> expr -> expr - | EEq : expr -> expr -> expr. - -(** Values *) -Inductive value : Type := - | VNat : nat -> value - | VBool : bool -> value. - -(** Typing relation *) -Inductive has_type : expr -> ty -> Prop := - | T_Const : forall n, has_type (EConst n) TyNat - | T_True : has_type ETrue TyBool - | T_False : has_type EFalse TyBool - | T_Plus : forall e1 e2, - has_type e1 TyNat -> has_type e2 TyNat -> - has_type (EPlus e1 e2) TyNat - | T_Eq : forall e1 e2, - has_type e1 TyNat -> has_type e2 TyNat -> - has_type (EEq e1 e2) TyBool. - -(** Evaluation *) -Inductive eval : expr -> value -> Prop := - | E_Const : forall n, eval (EConst n) (VNat n) - | E_True : eval ETrue (VBool true) - | E_False : eval EFalse (VBool false) - | E_Plus : forall e1 e2 n1 n2, - eval e1 (VNat n1) -> eval e2 (VNat n2) -> - eval (EPlus e1 e2) (VNat (n1 + n2)) - | E_Eq : forall e1 e2 n1 n2, - eval e1 (VNat n1) -> eval e2 (VNat n2) -> - eval (EEq e1 e2) (VBool (Nat.eqb n1 n2)). - -(** Value typing *) -Definition value_has_type (v : value) (t : ty) : Prop := - match v, t with - | VNat _, TyNat => True - | VBool _, TyBool => True - | _, _ => False - end. - -(** Type soundness: well-typed expressions evaluate to well-typed values *) -Theorem type_soundness : forall e t v, - has_type e t -> eval e v -> value_has_type v t. -Proof. - intros e t v Htype Heval. - induction Htype; inversion Heval; subst; simpl; auto. -Qed. diff --git a/verification/proofs/tlaplus/StateMachine.tla b/verification/proofs/tlaplus/StateMachine.tla deleted file mode 100644 index f348494..0000000 --- a/verification/proofs/tlaplus/StateMachine.tla +++ /dev/null @@ -1,91 +0,0 @@ ---------------------------- MODULE StateMachine ---------------------------- -(* SPDX-License-Identifier: MPL-2.0 *) -(* Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) *) -(* *) -(* TLA+ Specification Template: State Machine *) -(* Replace with your project's distributed protocol or state machine. *) -(* Use TLC model checker to verify properties. *) -(* *) -(* Example: A simple request pipeline with safety properties. *) -(* Replace States, Init, Next with your project's actual states. *) -(***************************************************************************) - -EXTENDS Naturals, Sequences, FiniteSets - -CONSTANTS - MaxRequests \* Upper bound on concurrent requests (for model checking) - -VARIABLES - state, \* Current pipeline state - processed, \* Number of processed requests - queue \* Request queue - -vars == <> - -\* Pipeline states — replace with your project's states -States == {"idle", "scanning", "routing", "dispatching", "done", "failed"} - -\* Valid transitions — replace with your project's transition rules -ValidTransition(from, to) == - \/ from = "idle" /\ to = "scanning" - \/ from = "scanning" /\ to = "routing" - \/ from = "scanning" /\ to = "failed" - \/ from = "routing" /\ to = "dispatching" - \/ from = "routing" /\ to = "failed" - \/ from = "dispatching" /\ to = "done" - \/ from = "dispatching" /\ to = "failed" - \/ from = "done" /\ to = "idle" - \/ from = "failed" /\ to = "idle" - -\* Initial state -Init == - /\ state = "idle" - /\ processed = 0 - /\ queue = <<>> - -\* Transition action -Transition(newState) == - /\ ValidTransition(state, newState) - /\ state' = newState - /\ IF newState = "done" - THEN processed' = processed + 1 - ELSE processed' = processed - /\ UNCHANGED queue - -\* Enqueue a request (only when idle or scanning) -Enqueue == - /\ state \in {"idle", "scanning"} - /\ Len(queue) < MaxRequests - /\ queue' = Append(queue, "request") - /\ UNCHANGED <> - -\* Next-state relation -Next == - \/ \E s \in States : Transition(s) - \/ Enqueue - -\* Fairness: the system must eventually process -Spec == Init /\ [][Next]_vars /\ WF_vars(Next) - -\* ---- SAFETY PROPERTIES ---- - -\* State is always valid -TypeInvariant == state \in States - -\* Processed count never decreases (monotonicity) -ProcessedMonotonic == processed >= 0 - -\* Queue never exceeds max -QueueBounded == Len(queue) <= MaxRequests - -\* No impossible transitions (e.g., idle -> done) -NoSkipStates == - [][state' # state => - ValidTransition(state, state')]_state - -\* ---- LIVENESS PROPERTIES ---- - -\* Every request eventually completes or fails -EventualCompletion == <>(state = "done" \/ state = "failed") - -============================================================================ From 8b46a59a5450449e85771bacd15b8c12a1ce1ce8 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 27 Oct 2026 08:15:39 +0000 Subject: [PATCH 08/15] =?UTF-8?q?docs(adr):=20ADR=200005=20=E2=80=94=20v0.?= =?UTF-8?q?2=20consolidation,=20O5=20adopted,=20O6=20opened,=20prover=20ro?= =?UTF-8?q?les=20(Proposed)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit What was wrong: the spec consolidation of 2026-10-13 adopted O5, opened O6, wrote the prover roles into §9.3 and cited "ADR 0005" for all of it, but no ADR 0005 existed; the carrier-as-parameter question had no recorded home. What changed: docs/decisions/0005-…adoc in the 0004 layout — Status (Proposed, owner to accept), Context, Decisions D1–D6 (D1 v0.2 normative; D2 O5 adopted from the workbench proposal of 2026-07-17 unchanged in substance; D3 O6 opened; D4 prover roles per the 2026-10-12 kernel ruling; D5 three provers, templates removed; D6 recorded-not-decided: fidelity carrier as a parameter, Phase 1A), Consequences, Rejected alternatives. What I ran: nothing to run; the referenced files and identifiers were checked present (workbench note path, spec §9.3/§10, the removed templates). What I did not run: n/a. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01J4QvDh3p24SCUjyM9HHT31 --- ...0.2-consolidation-o5-and-prover-roles.adoc | 118 ++++++++++++++++++ 1 file changed, 118 insertions(+) create mode 100644 docs/decisions/0005-v0.2-consolidation-o5-and-prover-roles.adoc diff --git a/docs/decisions/0005-v0.2-consolidation-o5-and-prover-roles.adoc b/docs/decisions/0005-v0.2-consolidation-o5-and-prover-roles.adoc new file mode 100644 index 0000000..9b58d5d --- /dev/null +++ b/docs/decisions/0005-v0.2-consolidation-o5-and-prover-roles.adoc @@ -0,0 +1,118 @@ +// SPDX-FileCopyrightText: © 2026 Jonathan D.A. Jewell (hyperpolymath) +// SPDX-License-Identifier: CC-BY-SA-4.0 += ADR 0005 — Spec v0.2 consolidation, O5 adopted, O6 opened, prover roles, template removal; the carrier-as-parameter question recorded +:revdate: 2026-10-27 + +== Status + +*Proposed — owner to accept.* Drafted in the Phase 0 pass ("make the status +surfaces true"); the spec consolidation it ratifies landed as +`docs(spec): consolidate the calculus at v0.2` (2026-10-13). Nothing here changes +a semantics; D6 is recorded, not decided. + +== Context + +After ADR 0004 (R-2026-07-07) the normative text was split across four +documents written against two different carriers: `spec/calculus.adoc` v0.1 +(2026-06-22) with the ratification spliced in as notes, the never-merged +addendum `spec/calculus-v0.2-draft.adoc` (2026-06-23), and the two design notes +of 2026-07-07 (the L4 boundary and atoms; the CO-1 operational model). The spec +still said "seven effects" while the vocabulary, `EffectAtoms.lean` and the IR +said nine. The third firewall ("veridicality is declared and propagated, not +checked") cited an obligation O5 that §10 never defined; the workbench proposed +the missing entry on 2026-07-17 +(`trope-particularity-workbench/docs/theory/formalisms/defining-o5-veridicality-oracle.adoc`). +T-Sub's one-sidedness means the verdict certifies sufficiency only, which the +privacy direction (a ceiling on retention) cannot use. The estate's proof-kernel +ruling of 2026-10-12 fixed the role of each prover across repositories, and this +repo still described itself as a "four-prover" stack and carried three +never-instantiated Coq / TLA+ / Agda templates from the repository mint. + +== Decisions + +[cols="1,3",options="header"] +|=== +| ID | Decision + +| *D1 (one normative document)* | `spec/calculus.adoc` v0.2 (the consolidation +of 2026-10-13) is the normative text. The addendum is folded in and removed; the +two 2026-07-07 notes and `verification/proofs/INTEGRATION-REPORT.adoc` are +history and analysis, cited from the spec where they carry the argument, never +the other way round. Where any older status surface disagrees with the spec, the +spec wins. + +| *D2 (O5 adopted)* | §10 gains O5, the veridicality oracle, adopted from the +workbench proposal of 2026-07-17 unchanged in substance: Remark O5-a +(IR-relative undecidability of veridicality), the oracle interface with O5-1 +soundness, O5-2 attestation and O5-3 no-laundering, the falsifier, and the +upgrade path (mechanise O5-1 as a side condition on an `Oracle`-indexed verdict +judgement). Status in §10: DEFINED; mechanisation OPEN. Vocarium's warrants are +O5-2 attestations; Hermeneia's _licensed_ band is where O5-backed claims sit. + +| *D3 (O6 opened)* | §10 gains O6, the ceiling verdict: the dual theorem +stem:[\rho \sqsubseteq g_{\mathrm{ceiling}}] that a "no more than this may be +retained" use-model needs, which T-Sub's downward-only weakening does not give for +conservative lowering. Deliverable: the dual verdict proved for the exact-lowering +fragment and stated as unavailable for the conservative one, or a second, +upper-bound grade on edges. Status: OPEN. + +| *D4 (prover roles)* | The estate kernel ruling of 2026-10-12 applied here +(§9.3): *Agda* is the normative kernel (Theorem B; CO-1 mechanisation targets it); +*Idris2* is the executable reference (the verified core and the reference +`tropecheck`); *Lean 4 + Mathlib* is provenance (the grade-algebra boundary, the +atom and tropical factorisations, kept with their axiom audits); *Rust* is the +fast core, validated against the reference over the conformance corpus. +Consequence: `docs/status/PROOF-STATUS.adoc` leads with Agda, and new +metatheory goes to Agda unless an ADR says otherwise. + +| *D5 (three provers; templates removed)* | `verification/proofs/coq/TypeSafety.v`, +`verification/proofs/tlaplus/StateMachine.tla` and +`verification/proofs/agda/Properties.agda` — mint templates whose own text says +"Replace with your project's …", never instantiated — are removed, with their +tree and recipe references. The repository describes itself as three provers +(Agda, Idris2, Lean) plus a Rust fast core. + +| *D6 (recorded, not decided)* | Whether the fidelity carrier should be a +*parameter* — any resource algebra with two adjoined tops, instantiated from +`hyperpolymath/resource-algebra` — rather than the one instance +stem:[\mathbb{N}\cup\{\infty,\top\}]. This would answer the "uncalibrated +ordinal arithmetic" objection (the finite part of the carrier adds losses whose +unit is unstated) by making the unit the instance's business. O4 is RESOLVED for +the instance (ADR 0004); the parameterisation is Phase 1A work and is *not* +decided by this ADR. +|=== + +== Consequences + +* One place to read the calculus; "nine effects" throughout, reconciled with + "seven" as nine atom families of which six are writable and three are faults. +* The third firewall now cites a defined obligation. O5 is dischargeable in + principle (mechanise O5-1) and refutable (its falsifier is stated). +* The privacy direction has a named obligation (O6) instead of an unstated gap; + the verdict's one-sidedness is written down as a limitation, not hidden. +* Status surfaces (`PROOF-STATUS`, `ROADMAP`, `AFFIRMATION`, the Agda `fix` + footer) are rewritten to the ratified world in the same pass; the Lean + honesty gate and `verify-all` cover every tracked Lean source. +* `just proof-check-all` no longer invokes the Coq recipe; `just proof-status` + reports three provers. The historical mention of the templates in + `INTEGRATION-REPORT.adoc` stays as the record of what was there. +* D6 leaves the carrier an instance; downstream (vocarium, hermeneia) may keep + reading `Attenuated(δ)` with stem:[\delta \in \mathbb{N}]. + +== Rejected alternatives + +* *Keep the addendum as a separate v0.2 document* — rejected: two normative + texts on two carriers is how readers and agents kept landing in the + pre-ratification world. +* *"Four-prover" wording, Rust as a prover* — rejected: the fast core proves + nothing; it is validated against the reference. Naming it a prover overclaims. +* *Keep the Coq / TLA+ / Agda templates as future placeholders* — rejected: they + were never instantiated, each advertises a prover the roles ruling does not + assign here, and `proof-check-coq` skipping silently is a gate that cannot fail. +* *Decide D6 now (make the carrier a parameter in this pass)* — rejected: it + changes the carrier every proof development is stated over; it belongs to + Phase 1A with `resource-algebra` as the instance supplier, after CO-1 + mechanisation lands on the fixed instance. +* *Leave O5 as the workbench proposal* — rejected: an obligation cited by the + checker's firewalls must live in the checker's spec, not in a proposal + downstream cannot cite as normative. From 0169a8cfcae17acb503f1867811d916f770c32a5 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 27 Oct 2026 08:15:39 +0000 Subject: [PATCH 09/15] docs(changelog): record the v0.2 consolidation and the Phase 0 pass MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit What was wrong: CHANGELOG [Unreleased] stopped at the IR 0.2 normalisation and the 2026-06 developments; the spec consolidation, the proofs.yml pin, the status rewrites, ADR 0005 and the template removal were unrecorded. What changed: the v0.2 consolidation line from the foot of spec/calculus.adoc; one line each for the status-surface rewrites (T1–T4), the proofs.yml pin, ADR 0005 (Added) and the template removal (Removed). docs/status/READINESS.adoc was grepped for the same stale phrases as PROOF-STATUS and has none, so it is untouched (it remains the unfilled CRG template, which is not false). What I ran: grep -nE "non-commutative|lax L4|L4 fails|OPEN-B|OPEN-C|gated by O4|10/10|8 schema" docs/status/READINESS.adoc -> no hits. What I did not run: n/a. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01J4QvDh3p24SCUjyM9HHT31 --- CHANGELOG.adoc | 33 +++++++++++++++++++++++++++++++++ 1 file changed, 33 insertions(+) diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index 9623b93..2a3e1b3 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -10,6 +10,25 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning]. ==== Changed +* *Spec v0.2 consolidation (2026-10-13).* `+docs(spec)+`: consolidate the calculus +at v0.2 — nine effects with the atom table, ratified carrier inline (A1–A3), L6 +commutativity and the cancellation structure as laws, the tropical factorisation +recorded as sighted, §7 restated as greatest post-fixed point with T-Fix-Decl, O5 +defined and O6 (ceiling verdict) opened, prover roles per ADR 0005. +`+spec/calculus-v0.2-draft.adoc+` folded in and removed; README and +INTEGRATION-REPORT aligned. +* *Phase 0 — status surfaces made true (2026-10-27).* +`+docs/status/PROOF-STATUS.adoc+` rewritten to the ratified carrier (one proved +table citing only existing lemma names; open list = spec §10; history collapsed); +`+docs/status/ROADMAP.adoc+` ships v0.2; `+AFFIRMATION.adoc+` gains a 2026-10-27 +entry from re-run checks (13 + 9 conformance on both checkers, Agda green, Lean +NOT RUN in that session); the `+fix+` footer of +`+verification/proofs/agda/theorem-b/TB/Reduction.agda+` names the designed CO-1 +model and records O4 as resolved. +* *`+proofs.yml+`* pins Agda 2.7.0.1 + agda-stdlib 2.0 by SHA-256 (the runner's apt +pair fails at `+Data.Product.Base+`); the Lean honesty gate and `+verify-all+` cover +every tracked `+.lean+` file. + * *IR 0.2 — A3 `+Attenuated(0)+` ingest normalization (R-2026-07-07-03, ADR 0004, #28).* Both checkers (Idris2 reference, Rust fast-core) rewrite `+Attenuated(0)+` to `+Present+` at the IR ingest boundary, @@ -25,6 +44,12 @@ fault. New conformance fixtures prove `+Atten(0)+` ≡ `+Present+` ==== Added +* *ADR 0005* (`+docs/decisions/0005-v0.2-consolidation-o5-and-prover-roles.adoc+`, +Proposed): spec v0.2 normative; O5 adopted from the workbench proposal of +2026-07-17; O6 opened; prover roles (Agda kernel, Idris2 reference, Lean +provenance, Rust fast core); templates removed; the carrier-as-parameter question +(D6) recorded, not decided. + * *Grade-algebra ground truth (Lean 4 + Mathlib).* `+verification/proofs/lean4/grade-boundary/+`: a sorry-free, axiom-clean (`+propext+`/`+Quot.sound+` only) formalisation of the honest/deceptive @@ -75,3 +100,11 @@ prose. central open problem. * `+.gitignore+` now excludes `+.lake/+` (Lean build artifacts + vendored Mathlib clones). + +==== Removed + +* The never-instantiated prover templates `+verification/proofs/coq/TypeSafety.v+`, +`+verification/proofs/tlaplus/StateMachine.tla+` and +`+verification/proofs/agda/Properties.agda+`, with their tree and recipe references +(`+proof-check-all+` no longer runs the Coq recipe; `+proof-status+` reports three +provers). From cb549c7c9e91731e0364730ce8dc0122e048e3bd Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 27 Oct 2026 08:27:22 +0000 Subject: [PATCH 10/15] docs: axiom audit says Classical.choice in three theorems; cite the CI Lean run MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit What was wrong: spec §9.3, PROOF-STATUS and verification/proofs/README said the Lean developments' axiom audits show "propext/Quot.sound only". The proofs.yml lean-build run on this branch (40472568287) prints the audit: Trope.nine_families (EffectAtoms.lean), FateA.Q_add_left_cancel and FateA.atten_cancel_on_normalForms (GradeRatified.lean) also depend on Classical.choice. GradeBoundary.lean's own footer had listed Classical.choice all along; the surfaces overclaimed. What changed: the three surfaces now say "no sorryAx, no user axiom; propext, Quot.sound and, in three theorems, Classical.choice"; the AFFIRMATION entry's Lean bullet cites the CI run (lake build succeeded for both packages; the job is red only in lean-action's optional nanoda step, which cannot compile its lean4export under the v4.16.0 toolchain, as on main — issue #104) and records this as finding (3). What I ran: read the job logs of run 40472568287 (both Lean jobs): "Build completed successfully", one axiom line per theorem, then "nanoda check failed". What I did not run: lake build locally (unchanged: no lake here). Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01J4QvDh3p24SCUjyM9HHT31 --- AFFIRMATION.adoc | 17 ++++++++++++----- docs/status/PROOF-STATUS.adoc | 4 ++-- spec/calculus.adoc | 4 +++- verification/proofs/README.adoc | 2 +- 4 files changed, 18 insertions(+), 9 deletions(-) diff --git a/AFFIRMATION.adoc b/AFFIRMATION.adoc index 3cf8e88..264d6e3 100644 --- a/AFFIRMATION.adoc +++ b/AFFIRMATION.adoc @@ -101,9 +101,12 @@ Idris2 0.8.0 (built from tag `v0.8.0` on Chez Scheme 9.5.8); rustc 1.97.0; just * `just build-lean` → *NOT RUN here*: `lake` is not installed and the Lean toolchain and Mathlib cache hosts were unreachable from this container. The `lean-source-honesty` regexes of `proofs.yml` were run by hand over all 8 tracked - `.lean` files: no `sorry` / `admit` / `native_decide`, no user `axiom`. The build and - axiom audit are the `proofs.yml` `lean-build` job; its run on this branch is cited in - the Phase 0 pull request. + `.lean` files: no `sorry` / `admit` / `native_decide`, no user `axiom`. On this + branch the `proofs.yml` `lean-build` job (run 40472568287, 2026-10-27T08:18Z) built + both packages — `lake build` "Build completed successfully", one axiom line per + theorem — and then failed in lean-action's optional `nanoda` step (its lean4export + does not compile under the v4.16.0 toolchain), exactly as on `main`; that step, not + the build, is why the job is red. *Proved* (machine-checked; names in `docs/status/PROOF-STATUS.adoc`): L1–L6 on the ratified carrier, L4 in full (`fateL4MonoR/L`, `bondComposeMono`, `mergeComposeMono`); @@ -116,7 +119,7 @@ T-Sub and verdict soundness (`soundFromExact`, `subSound`, `verdictSound`). *Ope (`spec/calculus.adoc §10`): CO-1 mechanisation (the `fix` case; designed, not mechanised), O1-coord, O2, O3, O5 mechanisation, O6. -*Two findings.* (1) Ubuntu 24.04's apt pair (Agda 2.6.3, agda-stdlib 1.7.3) cannot +*Three findings.* (1) Ubuntu 24.04's apt pair (Agda 2.6.3, agda-stdlib 1.7.3) cannot typecheck Theorem B: `agda --safe --without-K All.agda` exits 42, `Data.Product.Base` not found — stdlib ≥ 2.0 is required, which is why `proofs.yml` now pins Agda 2.7.0.1 + stdlib 2.0 by checksum (reproduced here, 58 s). (2) The 2026-06-22 entry's "10/10" @@ -125,6 +128,10 @@ proof-check-all` is red for reasons that predate this pass (per-file `idris2 --c and `agda --safe` from the repo root cannot resolve module names; the ABI/Types Idris2 mint templates do not typecheck) — recorded as an issue, not fixed here; the gates that mean something are `just check`, `just build-agda`, `just trope-rust` and -`verify-all`. +`verify-all`. (3) The CI axiom audit shows `Trope.nine_families` (`EffectAtoms.lean`), +`FateA.Q_add_left_cancel` and `FateA.atten_cancel_on_normalForms` (`GradeRatified.lean`) +depend on `Classical.choice` as well as `propext`/`Quot.sound`; the "`propext`/`Quot.sound` +only" wording in spec §9.3, PROOF-STATUS and the proofs README overclaimed and now reads +"no `sorryAx`, no user axiom". `GradeBoundary.lean`'s own footer had said so all along. — Run by the Phase 0 agent; the owner signs on landing. diff --git a/docs/status/PROOF-STATUS.adoc b/docs/status/PROOF-STATUS.adoc index c84ecd4..da3d50a 100644 --- a/docs/status/PROOF-STATUS.adoc +++ b/docs/status/PROOF-STATUS.adoc @@ -5,8 +5,8 @@ :toc: macro :stem: latexmath -What is *proved* (machine-checked, no axioms beyond `propext`/`Quot.sound` in -Lean; `--safe --without-K` in Agda; `%default total` with no escape hatch in +What is *proved* (machine-checked: in Lean no `sorryAx` and no user axiom — the +audits show `propext`, `Quot.sound` and, in three theorems, `Classical.choice`; `--safe --without-K` in Agda; `%default total` with no escape hatch in Idris2) and what is *open* (named, specified, not asserted), on the ratified carrier of `spec/calculus.adoc` v0.2 (R-2026-07-07, ADR 0004). Prover roles per ADR 0005: Agda is the normative kernel, Idris2 the executable reference, Lean the diff --git a/spec/calculus.adoc b/spec/calculus.adoc index 89ba35b..aebe102 100644 --- a/spec/calculus.adoc +++ b/spec/calculus.adoc @@ -693,7 +693,9 @@ Per the estate's proof-kernel ruling of 2026-10-12 (ADR 0005), the roles are: * *Provenance — Lean 4 + Mathlib* (`verification/proofs/lean4/`): the grade-algebra boundary and its ratified mirror, the atom factorisation and the tropical factorisation probe — the Mathlib-facing results, retained with - their axiom audits (`propext`/`Quot.sound` only). + their axiom audits: no `sorryAx`, no user axiom; `propext`, `Quot.sound` and, + in three theorems (`nine_families`, `Q_add_left_cancel`, + `atten_cancel_on_normalForms`), `Classical.choice`. * *Fast core — Rust* (`src/rust/`, dependency-free): the shipping checker, validated against the reference bit-for-bit over the conformance corpus. diff --git a/verification/proofs/README.adoc b/verification/proofs/README.adoc index d2e0e69..6ec622d 100644 --- a/verification/proofs/README.adoc +++ b/verification/proofs/README.adoc @@ -22,7 +22,7 @@ proofs/ ├── lean4/ # Lean4 proofs (algebra, lattices) │ ├── ApiTypes.lean │ ├── grade-boundary/ # grade-algebra GROUND TRUTH: the honest/deceptive cancellation -│ │ # boundary (Lean 4 + Mathlib; sorry-free; propext/Quot.sound only) +│ │ # boundary (Lean 4 + Mathlib; sorry-free; no user axiom) │ └── grade-factorisation/ # tropical factorisation probe: imports the carrier; verdict (B) │ # factors but veridicality-blind (precondition only; not CO-1) └── agda/ # Agda proofs (induction, metatheory) From 3d907be7d2ee781b38cc00216d820f85eb7544fa Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 27 Oct 2026 08:32:25 +0000 Subject: [PATCH 11/15] docs: qualify the gfp tier remark; bring PROOF-NEEDS' DOM rows to the ratified carrier MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit What was wrong (review findings on #102): the Reduction.agda footer said "the gfp's fidelity lands in the absorbing tops {total, unknown}" for every fix; that holds for a body that attenuates and recurses without bound, not for F(γ) = γ (gfp Present) or a body that ignores its binder (finite gfp). PROOF-NEEDS.adoc rows DOM-1/2/6/7/8 still described a non-commutative ▷, CO-1 "gated by O4", a "lax L4", and "propext/Quot.sound only". What changed: the footer restricts the absorbing-top argument to unbounded attenuation and names the other cases the fix proof must cover (comment only); DOM-1 marks non-commutativity historical and points at GradeRatified.lean, DOM-2 drops "non-commutative", DOM-6 records CO-1 as DESIGNED (O4 resolved) with mechanisation OPEN, DOM-7 drops the lax-L4 framing, DOM-8 records the (B′) re-run; "propext/Quot.sound only" becomes "no user axiom". What I ran: just build-agda after the footer edit -> PASS (All.agda + Smoke.agda); grep -n "non-commutative\|gated by O4\|lax L4\|Quot.sound" docs/status/PROOF-NEEDS.adoc -> none. What I did not run: n/a. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01J4QvDh3p24SCUjyM9HHT31 --- docs/status/PROOF-NEEDS.adoc | 10 +++++----- verification/proofs/agda/theorem-b/TB/Reduction.agda | 11 +++++++---- 2 files changed, 12 insertions(+), 9 deletions(-) diff --git a/docs/status/PROOF-NEEDS.adoc b/docs/status/PROOF-NEEDS.adoc index d571ecb..52a6eef 100644 --- a/docs/status/PROOF-NEEDS.adoc +++ b/docs/status/PROOF-NEEDS.adoc @@ -60,14 +60,14 @@ These proofs come from the rsr-template-repo and MUST be present in every repo: |=== | # | Proof Needed | Category | Prover | Priority | File(s) -| DOM-1 | Grade-algebra honest/deceptive cancellation boundary (non-commutative product monoid; full-carrier conicality; three-tier strict boundary, cancellation only on the finite-fidelity core) | DOM/ALG | Lean 4 | T1 | `verification/proofs/lean4/grade-boundary/GradeBoundary.lean` — *PROVED* (sorry-free; `propext`/`Quot.sound` only) -| DOM-2 | Theorem B Target 1 — intrinsic graded calculus over the non-commutative `▷` | DOM | Agda | T1 | `verification/proofs/agda/theorem-b/TB/{Grade,Syntax,Order}.agda` — *PROVED* +| DOM-1 | Grade-algebra honest/deceptive cancellation boundary (full-carrier conicality; three-tier strict boundary, cancellation only on the finite-fidelity core; the v0.1 carrier's non-commutativity is historical — the ratified carrier is commutative, L6) | DOM/ALG | Lean 4 | T1 | `verification/proofs/lean4/grade-boundary/GradeBoundary.lean` (v0.1 carrier) and `GradeRatified.lean` (ratified mirror) — *PROVED* (sorry-free; no user axiom) +| DOM-2 | Theorem B Target 1 — intrinsic graded calculus over `▷` | DOM | Agda | T1 | `verification/proofs/agda/theorem-b/TB/{Grade,Syntax,Order}.agda` — *PROVED* | DOM-3 | Theorem B Target 2 — grade-exact value substitution ("tropes follow values through cut"); symmetric cut impossible | DOM | Agda | T1 | `verification/proofs/agda/theorem-b/TB/Substitution.agda` — *PROVED (+ refutation)* | DOM-4 | Theorem B Target 3 — subject reduction respecting the three-tier boundary | DOM | Agda | T1 | `verification/proofs/agda/theorem-b/TB/{Reduction,Tier}.agda` — *PARTIAL* (β/let proved; `fix`/lfp NOT-REACHED, blocked on CO-1) | DOM-5 | Theorem B Target 4 — Honest Generation (HC-3): honesty closed under `▷`, deceptive grades unreachable | DOM | Agda | T1 | `verification/proofs/agda/theorem-b/TB/Honest.agda` — *PROVED* -| DOM-6 | CO-1 — operational model for `fix`/routing (gated by O4); enables full subject reduction | DOM | — | T2 | named in `docs/status/PROOF-STATUS.adoc` — *OPEN, not attempted* -| DOM-7 | Grade soundness for conservative lowering over fate (needs lax L4; strict L4 proved to fail) | ALG | — | T2 | named in `docs/status/PROOF-STATUS.adoc` — *OPEN* -| DOM-8 | Tropical factorisation precondition — the grade admits a *nontrivial* monoid homomorphism onto the *commutative* fidelity carrier `Δ`, and *every* such map is forced to identify honest `dropped` with deceptive `falsified` (the commutative cost-quotient is *veridicality-blind* on the fate axis; bond/merge deception stays separable) | DOM/ALG | Lean 4 | T1 | `verification/proofs/lean4/grade-factorisation/GradeFactorisation.lean` — *PROVED* (verdict B; sorry-free; `propext`/`Quot.sound` only; four theorems axiom-free). *Precondition only* — does not address CO-1. +| DOM-6 | CO-1 — operational model for `fix`/routing; enables full subject reduction | DOM | Agda | T2 | DESIGNED in `spec/notes/2026-07-07-co1-operational-model.adoc` (O4 resolved by ADR 0004); mechanisation — *OPEN* +| DOM-7 | Grade soundness for conservative lowering over fate (L4 holds in full on the ratified carrier; needs the CO-1 mechanisation) | ALG | Agda | T2 | named in `docs/status/PROOF-STATUS.adoc` — *OPEN* +| DOM-8 | Tropical factorisation precondition — the grade admits a *nontrivial* monoid homomorphism onto the *commutative* fidelity carrier `Δ`, and *every* such map is forced to identify honest `dropped` with deceptive `falsified` (the commutative cost-quotient is *veridicality-blind* on the fate axis; bond/merge deception stays separable) | DOM/ALG | Lean 4 | T1 | `verification/proofs/lean4/grade-factorisation/GradeFactorisation.lean` — *PROVED* (verdict B on the v0.1 carrier; sorry-free; no user axiom). Re-run on the ratified carrier in `GradeFactorisationR.lean`: verdict (B′) factors and veridicality-sighted — *PROVED*. *Precondition only* — does not address CO-1. |=== == Dangerous Patterns (BANNED) diff --git a/verification/proofs/agda/theorem-b/TB/Reduction.agda b/verification/proofs/agda/theorem-b/TB/Reduction.agda index 19e08de..5edbd7f 100644 --- a/verification/proofs/agda/theorem-b/TB/Reduction.agda +++ b/verification/proofs/agda/theorem-b/TB/Reduction.agda @@ -139,10 +139,13 @@ seq-stays-core {g₁ = g₁} {g₂ = g₂} _ _ c₁ c₂ = core-closed-▷ g₁ -- What used to be listed as a second obstruction — a LIMIT CARRIER for ordering -- iterated attenuation beyond ω, the O4 fork (Conat-vs-tag) — is RESOLVED by -- ADR 0004: the finitary carrier ℕ ∪ {∞, ⊤} suffices, because transfinitely --- deep `fix` nesting is inexpressible in finitary syntax. The gfp's fidelity --- lands in the absorbing tops {total, unknown}, which ARE ▷-fixed --- (TB.Grade.total-absorb-Q, unknown-absorbL), so the GRADE is tier-stable; only --- the operational unfold-preserves-tier step, item (1), remains. +-- deep `fix` nesting is inexpressible in finitary syntax. For a body that +-- attenuates and recurses without bound the gfp's fidelity lands in the +-- absorbing tops {total, unknown}, which ARE ▷-fixed (TB.Grade.total-absorb-Q, +-- unknown-absorbL), so that GRADE is tier-stable; a body that does not use its +-- binder, or F(γ) = γ, has a finite gfp (Present for the identity), which the +-- fix proof must cover separately. In every case only the operational +-- unfold-preserves-tier step, item (1), remains. -- -- The honest verdict for fix-subject-reduction is therefore NOT-REACHED, with -- the obstruction characterised: the mechanisation of the designed operational From 70a8109da14e144b5ffe35cd8131fa0fd17b8202 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 27 Oct 2026 08:47:34 +0000 Subject: [PATCH 12/15] proofs: comment-aware Lean honesty gate; say which carrier each cited theorem is on MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Review round 2 (Codex, CodeRabbit) on PR #102: - proofs.yml lean-source-honesty and the `verify-all` recipe strip comments with tests/lib/strip-proof-comments.awk and match the bare `sorry`/`admit` tokens, so `:= by` followed by an indented `sorry` on the next line fails the gate (the old line-anchored regex passed it; ApiTypes.lean is not built by either Lake package, so the gate was its only check). Tested: all eight tracked .lean files still PASS; synthetic multiline sorry/admit now FAIL; "sorry-free" prose in comments still PASSes. actionlint clean. - README / ROADMAP: "carry no axioms" -> "no `sorryAx` and no user axiom", the wording the axiom audit supports (propext, Quot.sound, Classical.choice x3). - PROOF-STATUS, README, AFFIRMATION: the atom factorisation (`EffectAtoms.lean`) imports GradeBoundary and is a theorem about the v0.1 `Grade`; no GradeR restatement exists. Recorded as Open (O1-carrier on GradeR) and as AFFIRMATION finding (4); the spec's §6/§10 wording is left for the owner. - PROOF-NEEDS DOM-3: symmetric cut holds on the ratified carrier (`cut-grade-comm`); the v0.1 refutation is historical. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01J4QvDh3p24SCUjyM9HHT31 --- .github/workflows/proofs.yml | 9 +++++++-- AFFIRMATION.adoc | 10 +++++++--- CHANGELOG.adoc | 3 ++- README.adoc | 9 +++++---- build/just/proofs.just | 6 ++++-- docs/status/PROOF-NEEDS.adoc | 2 +- docs/status/PROOF-STATUS.adoc | 7 ++++++- docs/status/ROADMAP.adoc | 4 ++-- 8 files changed, 34 insertions(+), 16 deletions(-) diff --git a/.github/workflows/proofs.yml b/.github/workflows/proofs.yml index 36074cb..15d1361 100644 --- a/.github/workflows/proofs.yml +++ b/.github/workflows/proofs.yml @@ -61,10 +61,15 @@ jobs: echo "::error::gated file is missing: $f"; fail=1; continue fi echo "--- gating $f ---" - if grep -nE '(:=|by|;|<;>|=>|\|)[[:space:]]*(sorry|admit)\b|\bnative_decide\b' "$f"; then + # Comment-aware and token-based: strip -- and /- -/ comments first + # (tests/lib/strip-proof-comments.awk; line numbers preserved), then match + # the bare tokens, so `:= by` with an indented `sorry` on the NEXT line is + # caught while the honest "sorry-free" prose in comments is not. + stripped=$(awk -f tests/lib/strip-proof-comments.awk "$f") + if grep -nE '(^|[^[:alnum:]_.])(sorry|admit)([^[:alnum:]_]|$)|\bnative_decide\b' <<<"$stripped"; then echo "::error file=$f::forbidden Lean tactic (sorry/admit/native_decide)"; fail=1 fi - if grep -nE '^[[:space:]]*axiom\b' "$f"; then + if grep -nE '^[[:space:]]*axiom\b' <<<"$stripped"; then echo "::error file=$f::user axiom declared"; fail=1 fi done diff --git a/AFFIRMATION.adoc b/AFFIRMATION.adoc index 264d6e3..2afafcc 100644 --- a/AFFIRMATION.adoc +++ b/AFFIRMATION.adoc @@ -112,14 +112,14 @@ Idris2 0.8.0 (built from tag `v0.8.0` on Chez Scheme 9.5.8); rustc 1.97.0; just ratified carrier, L4 in full (`fateL4MonoR/L`, `bondComposeMono`, `mergeComposeMono`); the decidable retention preorder; the Veridicality Derivation and Honest Generation; C1–C3 (`GradeR.conical`, `gradeR_leftCancel_iff`, `TierTwoComplete`, -`fate-tier-meet-hom-fails`); O1-carrier (`atom_factorization`); the sighted tropical +`fate-tier-meet-hom-fails`); O1-carrier (`atom_factorization`, stated on the v0.1 `Grade` — finding 4); the sighted tropical factorisation (`piR_sighted`); Theorem B Targets 1, 2, 4 and the β/let case of 3 (`cut-preserves-grade`, `β-app`, `β-let`); grade soundness for exact lowering, T-Sub and verdict soundness (`soundFromExact`, `subSound`, `verdictSound`). *Open* (`spec/calculus.adoc §10`): CO-1 mechanisation (the `fix` case; designed, not mechanised), O1-coord, O2, O3, O5 mechanisation, O6. -*Three findings.* (1) Ubuntu 24.04's apt pair (Agda 2.6.3, agda-stdlib 1.7.3) cannot +*Four findings.* (1) Ubuntu 24.04's apt pair (Agda 2.6.3, agda-stdlib 1.7.3) cannot typecheck Theorem B: `agda --safe --without-K All.agda` exits 42, `Data.Product.Base` not found — stdlib ≥ 2.0 is required, which is why `proofs.yml` now pins Agda 2.7.0.1 + stdlib 2.0 by checksum (reproduced here, 58 s). (2) The 2026-06-22 entry's "10/10" @@ -132,6 +132,10 @@ that mean something are `just check`, `just build-agda`, `just trope-rust` and `FateA.Q_add_left_cancel` and `FateA.atten_cancel_on_normalForms` (`GradeRatified.lean`) depend on `Classical.choice` as well as `propext`/`Quot.sound`; the "`propext`/`Quot.sound` only" wording in spec §9.3, PROOF-STATUS and the proofs README overclaimed and now reads -"no `sorryAx`, no user axiom". `GradeBoundary.lean`'s own footer had said so all along. +"no `sorryAx`, no user axiom". `GradeBoundary.lean`'s own footer had said so all along. (4) `EffectAtoms.lean` imports +`GradeBoundary`, so the atom factorisation cited for O1-carrier is a theorem about the +v0.1 `Grade`; no `GradeR` restatement exists. The factorisation is componentwise and +should transfer, but that is an argument, not a proof — recorded in PROOF-STATUS (Open) +and left for the owner where `spec/calculus.adoc §6/§10` cite it as ratified-carrier. — Run by the Phase 0 agent; the owner signs on landing. diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index 2a3e1b3..35758e8 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -27,7 +27,8 @@ NOT RUN in that session); the `+fix+` footer of model and records O4 as resolved. * *`+proofs.yml+`* pins Agda 2.7.0.1 + agda-stdlib 2.0 by SHA-256 (the runner's apt pair fails at `+Data.Product.Base+`); the Lean honesty gate and `+verify-all+` cover -every tracked `+.lean+` file. +every tracked `+.lean+` file and are comment-aware and token-based (a `+sorry+` on the +line after `+:= by+` is caught; "sorry-free" prose in comments is not). * *IR 0.2 — A3 `+Attenuated(0)+` ingest normalization (R-2026-07-07-03, ADR 0004, #28).* Both checkers (Idris2 reference, Rust fast-core) diff --git a/README.adoc b/README.adoc index 1bec043..c618248 100644 --- a/README.adoc +++ b/README.adoc @@ -144,12 +144,13 @@ https://github.com/hyperpolymath/trope-checker/tree/8f58d2409227b065fed01a898c02 == Status Alpha. The IR schema, the executable checker and the conformance suite are green, -and the verified developments carry no axioms behind their claimed lemmas. On the -ratified carrier (ADR 0004, R-2026-07-07) the grade algebra is a commutative +and the verified developments carry no `sorryAx` and no user axiom behind their +claimed lemmas (the Lean results rest on the standard library's `propext`/`Quot.sound`, +and `Classical.choice` in three theorems). On the ratified carrier (ADR 0004, R-2026-07-07) the grade algebra is a commutative monoid with the three deceptive bottoms as two-sided zeros; L1–L6, conicality, the cancellation boundary (left-cancellative iff ε), the Honest Generation and -Veridicality theorems, the atom factorisation (O1's carrier half) and a -veridicality-sighted tropical factorisation are proved across Agda, Idris2 and +Veridicality theorems, the atom factorisation (O1's carrier half — stated on the v0.1 `Grade`, +not yet restated on `GradeR`) and a veridicality-sighted tropical factorisation are proved across Agda, Idris2 and Lean; Theorem B gives grade-exact substitution and β/let subject reduction. The named open problems are *CO-1* — the operational model for `fix` is designed (`spec/notes/2026-07-07-co1-operational-model.adoc`) and awaits mechanisation, diff --git a/build/just/proofs.just b/build/just/proofs.just index 6f3cb64..03eb33b 100644 --- a/build/just/proofs.just +++ b/build/just/proofs.just @@ -207,9 +207,11 @@ verify-all: build-lean build-agda # Every Lean source (mirrors proofs.yml lean-source-honesty; keep the two in step). for f in $(git ls-files 'verification/proofs/lean4/*.lean' 'verification/proofs/lean4/*/*.lean'); do echo "--- gating $f ---" - if grep -nE '(:=|by|;|<;>|=>|\|)[[:space:]]*(sorry|admit)\b|\bnative_decide\b' "$f"; then + # Comment-aware, token-based (mirrors proofs.yml; keep the two in step). + stripped=$(awk -f tests/lib/strip-proof-comments.awk "$f") + if grep -nE '(^|[^[:alnum:]_.])(sorry|admit)([^[:alnum:]_]|$)|\bnative_decide\b' <<<"$stripped"; then echo "FAIL: forbidden Lean tactic (sorry/admit/native_decide) in $f"; exit 1; fi - if grep -nE '^[[:space:]]*axiom\b' "$f"; then + if grep -nE '^[[:space:]]*axiom\b' <<<"$stripped"; then echo "FAIL: user axiom declared in $f"; exit 1; fi done echo "PASS: verify-all — Lean green & axiom-clean (propext/Quot.sound only); Agda --safe --without-K green." diff --git a/docs/status/PROOF-NEEDS.adoc b/docs/status/PROOF-NEEDS.adoc index 52a6eef..0386936 100644 --- a/docs/status/PROOF-NEEDS.adoc +++ b/docs/status/PROOF-NEEDS.adoc @@ -62,7 +62,7 @@ These proofs come from the rsr-template-repo and MUST be present in every repo: | DOM-1 | Grade-algebra honest/deceptive cancellation boundary (full-carrier conicality; three-tier strict boundary, cancellation only on the finite-fidelity core; the v0.1 carrier's non-commutativity is historical — the ratified carrier is commutative, L6) | DOM/ALG | Lean 4 | T1 | `verification/proofs/lean4/grade-boundary/GradeBoundary.lean` (v0.1 carrier) and `GradeRatified.lean` (ratified mirror) — *PROVED* (sorry-free; no user axiom) | DOM-2 | Theorem B Target 1 — intrinsic graded calculus over `▷` | DOM | Agda | T1 | `verification/proofs/agda/theorem-b/TB/{Grade,Syntax,Order}.agda` — *PROVED* -| DOM-3 | Theorem B Target 2 — grade-exact value substitution ("tropes follow values through cut"); symmetric cut impossible | DOM | Agda | T1 | `verification/proofs/agda/theorem-b/TB/Substitution.agda` — *PROVED (+ refutation)* +| DOM-3 | Theorem B Target 2 — grade-exact value substitution ("tropes follow values through cut"); on the ratified carrier the cut is symmetric (`cut-grade-comm`, L6) — the v0.1 refutation `cut-symmetric-fails` is historical, retired with (A1) | DOM | Agda | T1 | `verification/proofs/agda/theorem-b/TB/Substitution.agda` — *PROVED* (refutation historical) | DOM-4 | Theorem B Target 3 — subject reduction respecting the three-tier boundary | DOM | Agda | T1 | `verification/proofs/agda/theorem-b/TB/{Reduction,Tier}.agda` — *PARTIAL* (β/let proved; `fix`/lfp NOT-REACHED, blocked on CO-1) | DOM-5 | Theorem B Target 4 — Honest Generation (HC-3): honesty closed under `▷`, deceptive grades unreachable | DOM | Agda | T1 | `verification/proofs/agda/theorem-b/TB/Honest.agda` — *PROVED* | DOM-6 | CO-1 — operational model for `fix`/routing; enables full subject reduction | DOM | Agda | T2 | DESIGNED in `spec/notes/2026-07-07-co1-operational-model.adoc` (O4 resolved by ADR 0004); mechanisation — *OPEN* diff --git a/docs/status/PROOF-STATUS.adoc b/docs/status/PROOF-STATUS.adoc index da3d50a..9930ab0 100644 --- a/docs/status/PROOF-STATUS.adoc +++ b/docs/status/PROOF-STATUS.adoc @@ -88,7 +88,7 @@ toc::[] 3+^| _Factorisation_ | O1-carrier (atom factorisation) -| Every grade is the stem:[\triangleright]-product of its single-slot projections; nine atom families, each realised, pairwise disjoint. +| Every grade is the stem:[\triangleright]-product of its single-slot projections; nine atom families, each realised, pairwise disjoint. Stated on the v0.1 `Grade` (`EffectAtoms.lean` imports `GradeBoundary`): the construction is componentwise and does not touch the clause (A1) changed, but a restatement on `GradeR` is not mechanised (see Open). | Lean `EffectAtoms.lean`: `Trope.Grade.atom_factorization`, `Trope.nine_families`, `Trope.family_realized`, `Trope.families_disjoint`, `fateFamily_none_iff`. | Tropical factorisation, (B′) sighted @@ -144,6 +144,11 @@ Each is specified; none is asserted. Status words follow `spec/calculus.adoc §1 its mechanisation in Agda, steps 1–5 of that note's §6 extending `TB.Reduction`, is OPEN. It closes Theorem B Target 3 (`fix`, NOT-REACHED, no postulate) and grade soundness for conservative lowering (`spec/calculus.adoc §7–§8`). +* *O1-carrier on `GradeR`* — `atom_factorization` and the nine-family results + (`EffectAtoms.lean`) are theorems about the v0.1 `Grade`; porting them to the + ratified `GradeR` — expected to be mechanical, the factorisation being + componentwise — is OPEN. Until then the ratified-carrier reading in + `spec/calculus.adoc §6` and `§10` rests on that transfer argument, not a proof. * *O1-coord* — whether `fate`, `bond`, `merge` are exhaustive ways to individuate-and-lose; live probe: the bond-transfer move (`spec/calculus.adoc §10`; workbench WP-5). diff --git a/docs/status/ROADMAP.adoc b/docs/status/ROADMAP.adoc index a9736a6..8fc5ff0 100644 --- a/docs/status/ROADMAP.adoc +++ b/docs/status/ROADMAP.adoc @@ -5,8 +5,8 @@ == Current status Alpha. The schema, the Idris2 reference checker, the Rust fast core and the -conformance suite are green; the verified developments carry no axioms behind -their claimed lemmas. Spec v0.2 is the normative document; what is proved and +conformance suite are green; the verified developments carry no `sorryAx` and no user +axiom behind their claimed lemmas. Spec v0.2 is the normative document; what is proved and what is open: `docs/status/PROOF-STATUS.adoc`, `AFFIRMATION.adoc`, `spec/calculus.adoc §10`. From dade336c7118ec903f32d9326bc2e00ddec37af1 Mon Sep 17 00:00:00 2001 From: "coderabbitai[bot]" <136622811+coderabbitai[bot]@users.noreply.github.com> Date: Tue, 27 Oct 2026 14:39:39 +0000 Subject: [PATCH 13/15] docs: clarify that grade algebra laws apply after erasing predicate and fusion labels --- spec/calculus.adoc | 31 +++++++++++++------ .../proofs/agda/theorem-b/TB/Grade.agda | 3 ++ verification/proofs/idris2/Trope/Coords.idr | 7 +++-- .../lean4/grade-boundary/GradeRatified.lean | 4 +++ .../lean4/grade-boundary/L4Monotonicity.lean | 4 ++- 5 files changed, 36 insertions(+), 13 deletions(-) diff --git a/spec/calculus.adoc b/spec/calculus.adoc index aebe102..1f36fd2 100644 --- a/spec/calculus.adoc +++ b/spec/calculus.adoc @@ -157,7 +157,8 @@ predicate accepts `Predicated(P)` but rejects `Dropped`. bottom is a *two-sided* zero of its coordinate's composition — in particular `Dropped ▷ Falsified = Falsified`, replacing the v0.1 clause `Dropped ▷ Falsified = Dropped` that let an upstream honest drop erase a -downstream lie and was the sole source of the algebra's non-commutativity. +downstream lie and was the sole source of the algebra's non-commutativity +after erasing predicate and fusion labels. (A2) `Dropped ⊑ Predicated`, dissolving the antichain. (A3) `Attenuated(0) = Present` is *imposed by normalization at IR ingest*: validators rewrite `Attenuated(Q 0)` to `Present` before grading, and composition preserves normal @@ -306,7 +307,17 @@ two-sided zero. *Merge composition* — meet in `Single ⊐ Fused ⊐ Conflated` with `Fused(τ₁) ▷ Fused(τ₂) = Fused(τ₁ ⊗ τ₂)` (nested honest merge, label is the pair) and `Conflated` a two-sided zero. -The laws the grade MUST satisfy, each enforced by the verified developments (§9.3): +The verified developments (§9.3) erase predicate and fusion labels: +`Predicated(P)` becomes `Predicated` and `Fused(τ)` becomes `Fused`, with all +other components unchanged. Erasure preserves composition. The laws below +apply to this erased grade carrier; equality of labels is outside the proof +contract. In particular, the right-predicate rule above need not commute on +labels: `Predicated(P) ▷ Predicated(Q) = Predicated(Q)`, whereas reversing the +operands gives `Predicated(P)`. Nested fusion pairs need neither commute nor +associate as literal labels: `(τ₁, τ₂)` differs from `(τ₂, τ₁)`, and +`((τ₁, τ₂), τ₃)` differs from `(τ₁, (τ₂, τ₃))`. + +The laws the erased grade MUST satisfy, each enforced by the verified developments: [cols="1,4",options="header"] |=== @@ -317,14 +328,16 @@ The laws the grade MUST satisfy, each enforced by the verified developments (§9 | *L3 (bottom-absorption)* | Each *deceptive* bottom — `Falsified`, `Misbound`, `Conflated`, and fidelity's `Unknown` — is a *two-sided zero* of its coordinate's composition (R-2026-07-07 (A1)): no honest absorber launders deception, in either composition order. (Lean `FateA.falsified_two_sided_zero`, `GradeR.gBotR_two_sided_zero`; Agda `falsified-absorb{L,R}`, `misbound-absorbL`, `conflated-absorbL`, `deceptive-absorbs-▷`.) The *honest* bottoms (`Dropped`, `Severed`) absorb within the honest fragment, and `Attenuated(⊤)` within the fidelity dimension. | *L4 (monotonicity)* | stem:[\triangleright] is monotone in each argument with respect to the retention order stem:[\sqsubseteq] (§5): composing after more loss never yields more retention. *Holds in full on the ratified carrier.* (Idris2 `Trope.Soundness.{fateL4MonoR,fateL4MonoL}`, `Trope.Order.{bondComposeMono,mergeComposeMono}`; Lean `FateA.comp_mono_{right,left}`; Agda `TB.Order.fateL4Mono{R,L}`.) History: strict L4 failed on the v0.1 carrier at exactly the two points (A1)/(A2) amended — `spec/notes/2026-07-07-l4-boundary-and-atoms.adoc`, `L4Monotonicity.lean` (`comp_not_monotone_{right,left}`, retained as theorems about the pre-ratification carrier). | *L5 (deception infectiousness)* | Once any coordinate is at its deceptive bottom, no composition restores an honest value. A corollary of L3, stated separately because it is the non-compositionality-of-deceptive-channels result and the moral core; it covers `Conflated` (v0.1's statement), `Falsified` and `Misbound` alike. -| *L6 (commutativity)* | stem:[g_1 \triangleright g_2 = g_2 \triangleright g_1]. New at v0.2: on the ratified carrier the grade monoid is *commutative* (Lean `GradeR.instCommMonoid`, `FateA.comp_comm`; Agda `grade-comm`). The v0.1 non-commutativity (`GradeBoundary.grade_mul_not_comm`) was an artefact of the clause (A1) removed. Order-sensitivity, where a producer wants it, MUST come from DAG structure (§9.1), never from stem:[\triangleright]. +| *L6 (commutativity)* | For grades with predicate and fusion labels erased, stem:[g_1 \triangleright g_2 = g_2 \triangleright g_1]. New at v0.2: on this ratified carrier the grade monoid is *commutative* (Lean `GradeR.instCommMonoid`, `FateA.comp_comm`; Agda `grade-comm`). These proofs carry no predicate or fusion labels and assert no equality between labelled grades. The v0.1 non-commutativity (`GradeBoundary.grade_mul_not_comm`) was an artefact of the clause (A1) removed. Order-sensitivity of erased loss-shapes MUST come from DAG structure (§9.1); label metadata may retain composition order. |=== [NOTE] ==== -L1–L2 make stem:[(\text{grades}, \triangleright, \varepsilon)] a monoid, L6 a -commutative one; the effect system is a *graded monad* on the term category -with this monoid as its grade object. L4 is what the verdict subsumption +L1–L2 make stem:[(\text{erased grades}, \triangleright, \varepsilon)] a monoid, +L6 a commutative one; the effect system is a *graded monad* on the term +category with this erased monoid as its grade object. Label metadata is +retained separately and is not covered by these monoid equalities. +L4 is what the verdict subsumption (§5–§6) and the recursion rule (§7) need. None of L1–L6 is novel as a _shape_; the content is that this carrier is the right grade object for trope-particularity, which §10-O1 marks as the open adequacy question. @@ -652,9 +665,9 @@ normalization). An *OPTIONAL* Nickel authoring contract MAY be offered front-side; the schema is the trust boundary. The grade algebra — stem:[\triangleright], stem:[\sqsubseteq], and stem:[\mathrm{floor}] — is specified in the IR spec itself, language-neutrally, so that two independent -checker implementations agree by construction. Order-sensitivity, where a -producer needs it, lives in the DAG (routing, multi-parent nodes), not in -stem:[\triangleright] (L6). +checker implementations agree by construction. Order-sensitivity of erased +loss-shapes lives in the DAG (routing, multi-parent nodes); predicate and +fusion labels may retain composition order (L6). === The checker as a pure function diff --git a/verification/proofs/agda/theorem-b/TB/Grade.agda b/verification/proofs/agda/theorem-b/TB/Grade.agda index e659297..2c3f85f 100644 --- a/verification/proofs/agda/theorem-b/TB/Grade.agda +++ b/verification/proofs/agda/theorem-b/TB/Grade.agda @@ -13,6 +13,9 @@ -- (verification/proofs/lean4/grade-boundary/L4Monotonicity.lean, FateA). -- The original Lean frozen interface (GradeBoundary.lean) describes the -- PRE-RATIFICATION carrier and is retained upstream under a provenance note. +-- Predicate and fusion labels are erased in this carrier: predicated and fused +-- are nullary. The monoid laws and grade-comm concern erased loss-shapes; +-- they assert no equality of predicate labels or nested provenance pairs. -- -- F1 Grade is a product Monoid (componentwise) — gmonoid-{assoc,unitL,unitR} -- F2′ the product is COMMUTATIVE on the ratified carrier — grade-comm diff --git a/verification/proofs/idris2/Trope/Coords.idr b/verification/proofs/idris2/Trope/Coords.idr index a13a576..8f4e0d7 100644 --- a/verification/proofs/idris2/Trope/Coords.idr +++ b/verification/proofs/idris2/Trope/Coords.idr @@ -8,9 +8,10 @@ ||| Misbound for bond, Conflated for merge): the BOTTOM of its order (worst ||| retention) and absorbing under ▷ — TWO-SIDEDLY on fate since R-2026-07-07 (A1) ||| — so a deceptive grade fails every honest floor and never composes away -||| (calculus §3.3, HC-2). Provenance tags on Fused are erased here -||| (they are metadata; they do not affect the lattice laws) — the executable -||| checker (src/checker) carries them. +||| (calculus §3.3, HC-2). Predicate labels and provenance tags on Fused are +||| erased here: Predicated and Fused are nullary. The laws concern erased +||| loss-shapes and assert no equality of predicate labels or nested provenance +||| pairs (calculus L1/L6). module Trope.Coords import Data.Nat diff --git a/verification/proofs/lean4/grade-boundary/GradeRatified.lean b/verification/proofs/lean4/grade-boundary/GradeRatified.lean index 39cc0d1..19eb3f8 100644 --- a/verification/proofs/lean4/grade-boundary/GradeRatified.lean +++ b/verification/proofs/lean4/grade-boundary/GradeRatified.lean @@ -14,6 +14,10 @@ fate coordinate — which is exactly `Trope.FateA` of `L4Monotonicity.lean` `Dropped ⊑ Predicated`, ratified in ADR 0004 as R-2026-07-07-01 and -02) — with the `Bond` and `Merge` coordinates unchanged from `GradeBoundary.lean`. +Predicate and fusion labels are erased: `Fate.predicated` and `Merge.fused` +are nullary. `instCommMonoid` proves the laws for these erased loss-shapes; +it asserts no equality of predicate labels or nested provenance pairs. + ## What is proved (sorry-free; `#print axioms` at the foot) * **`CommMonoid GradeR`** (`instCommMonoid`) — the ratified grade algebra is a diff --git a/verification/proofs/lean4/grade-boundary/L4Monotonicity.lean b/verification/proofs/lean4/grade-boundary/L4Monotonicity.lean index 3217015..2264b96 100644 --- a/verification/proofs/lean4/grade-boundary/L4Monotonicity.lean +++ b/verification/proofs/lean4/grade-boundary/L4Monotonicity.lean @@ -158,7 +158,9 @@ theorem le_total : ∀ a b : Fate, le a b ∨ le b a := by cases a <;> cases b <;> simp [le] <;> exact _root_.le_total _ _ /-- **Commutativity.** With (A1), amended composition is commutative: the sole -non-commuting pair of the shipped carrier was `(Dropped, Falsified)`. -/ +non-commuting pair of the shipped carrier was `(Dropped, Falsified)`. +`Fate.predicated` erases its predicate label; this theorem asserts no equality +of labelled predicates. -/ theorem comp_comm : ∀ a b : Fate, comp a b = comp b a := by intro a b cases a <;> cases b <;> simp [comp] From 35745d87dedc1715383cd4eda733e2d713fd344e Mon Sep 17 00:00:00 2001 From: "coderabbitai[bot]" <136622811+coderabbitai[bot]@users.noreply.github.com> Date: Tue, 27 Oct 2026 14:48:53 +0000 Subject: [PATCH 14/15] fix(ci): run conformance checks in E2E tests and clarify Lean axiom audit comments --- tests/e2e.sh | 141 +----------------- .../lean4/grade-boundary/EffectAtoms.lean | 2 +- .../lean4/grade-boundary/GradeBoundary.lean | 4 +- .../lean4/grade-boundary/GradeRatified.lean | 4 +- .../lean4/grade-boundary/L4Monotonicity.lean | 2 +- .../lean4/grade-boundary/TierTwoComplete.lean | 2 +- .../GradeFactorisation.lean | 4 +- .../GradeFactorisationR.lean | 2 +- 8 files changed, 17 insertions(+), 144 deletions(-) diff --git a/tests/e2e.sh b/tests/e2e.sh index 8cf64b0..73870d2 100755 --- a/tests/e2e.sh +++ b/tests/e2e.sh @@ -2,141 +2,14 @@ # SPDX-License-Identifier: MPL-2.0 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) # -# RSR Standard E2E Test Template +# Run the checker end to end against the shared conformance corpus: IR verdicts, +# witness edges and coordinates, and rejection of schema-invalid input. +# Build the reference checker with `just trope-build` first, or select an +# alternative compiled checker with TROPECHECK_BIN (as `just trope-rust` does). +# The conformance runner checks jq and the binary and propagates failures. # -# End-to-end tests validate the full pipeline: build → run → verify output. -# Customise this file for your project. Delete the examples that don't apply. -# -# Usage: -# bash tests/e2e.sh -# just e2e -# -# Merge requirements (STANDING): All 6 test categories must pass before merge: -# P2P, E2E (this file), aspect, execution, lifecycle, benchmarks - +# Usage: bash tests/e2e.sh set -euo pipefail SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)" -PROJECT_DIR="$(cd "$SCRIPT_DIR/.." && pwd)" - -PASS=0 -FAIL=0 -SKIP=0 - -# ─── Colour helpers ────────────────────────────────────────────────── -green() { printf '\033[32m%s\033[0m\n' "$*"; } -red() { printf '\033[31m%s\033[0m\n' "$*"; } -yellow(){ printf '\033[33m%s\033[0m\n' "$*"; } -bold() { printf '\033[1m%s\033[0m\n' "$*"; } - -# ─── Assertion helpers ─────────────────────────────────────────────── - -# check