From 4b9bbda9310c6d2e2897a4a88202d3f977ee29da Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 18 May 2026 01:13:11 +0100 Subject: [PATCH 1/6] docs+comments: reframe to mechanised truth (retraction R-2026-05-18) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adversarial three-reviewer review + a codebase pressure-test found no in-repo defense for five central claims; two were contradicted by the repo's own Gate-2 audit. This commit corrects the PROSE downward to what the Agda actually establishes. No proof is weakened — Agda is unchanged except for line-comment retraction banners; full build (All.agda then Smoke.agda) still exits 0 under --safe --without-K. Retracted -> replaced: - "graded comonad" -> loss-graded reindexing modality (thin-poset action; no nested D_r D_s) - "terminal-cone universal property" -> funext-relative pointwise mediator - "two independent models / model-independence" -> carrier-parametricity, fixed grade poset - "conservativity metatheorem discharged by the build" -> postulate-free build = evidence, not proof - "funext quarantined" -> no funext anywhere; pointwise mediator IS the real funext boundary - docs/retractions.adoc: created (canonical log roadmap-gates.adoc referenced but never existed); entry R-2026-05-18. - docs/echo-types/earn-back-plan.adoc: created; Pillar F gated program to convert retractions back into theorems (F1 make-or-break). - paper/conservativity/types-abstract/establishment-plan: reframed; "submission-ready" status withdrawn from the abstract. - Smoke.agda + 7 modules: top retraction banners (comments only). - ECHO-CNO-BRIDGE.adoc: scope note (its distinct, valid "model independence" is NOT retracted; disambiguated, not over-applied). Co-Authored-By: Claude Opus 4.7 (1M context) --- docs/ECHO-CNO-BRIDGE.adoc | 10 + docs/echo-types/conservativity.adoc | 175 +++++---- docs/echo-types/earn-back-plan.adoc | 176 +++++++++ docs/echo-types/establishment-plan.adoc | 175 ++++++--- docs/echo-types/paper.adoc | 360 ++++++++++++------ docs/echo-types/types-abstract.adoc | 172 +++++---- docs/retractions.adoc | 147 +++++++ proofs/agda/EchoChoreo.agda | 9 + proofs/agda/EchoGraded.agda | 9 + proofs/agda/EchoGradedComonad.agda | 9 + proofs/agda/EchoLinear.agda | 9 + proofs/agda/EchoPullback.agda | 9 + proofs/agda/EchoRelModel.agda | 11 + proofs/agda/Smoke.agda | 26 +- .../characteristic/RecipeNonTriviality.agda | 10 + 15 files changed, 1000 insertions(+), 307 deletions(-) create mode 100644 docs/echo-types/earn-back-plan.adoc create mode 100644 docs/retractions.adoc diff --git a/docs/ECHO-CNO-BRIDGE.adoc b/docs/ECHO-CNO-BRIDGE.adoc index f1f8bc3..308fe61 100644 --- a/docs/ECHO-CNO-BRIDGE.adoc +++ b/docs/ECHO-CNO-BRIDGE.adoc @@ -156,6 +156,16 @@ The `EchoCategory.agda` module establishes a comprehensive categorical formaliza 3. **Universal CNO**: CNOs as identity morphisms that preserve echo structure: `∀ s → Echo p s ≃ Echo id s` 4. **Model Independence**: Echo types are preserved across isomorphic computational models +> **Scope note (2026-05-18).** "Model Independence" *here* means the +> bare-`Echo` invariance `Echo f y ≃ Echo f' (proj₁ (isoB y))` under an +> isomorphism of the underlying objects (the `ModelIndependence` +> theorem below). This is a distinct, valid statement and is **not** +> affected by retraction R-2026-05-18, which retracted the *graded +> modality's* "two independent models / model-independence" claim +> (`GradedLossModel`/`EchoRelModel`). Do not conflate the two; this +> CNO consumer-bridge doc is firewalled from the identity claim. See +> `docs/retractions.adoc`. + ### Core Theorems ```agda diff --git a/docs/echo-types/conservativity.adoc b/docs/echo-types/conservativity.adoc index 84faeff..890801a 100644 --- a/docs/echo-types/conservativity.adoc +++ b/docs/echo-types/conservativity.adoc @@ -1,4 +1,4 @@ -= Echo Types — Conservativity Metatheorem += Echo Types — Conservativity Evidence (Mechanised Properties) :toc: macro :toclevels: 3 :sectnums: @@ -6,110 +6,142 @@ :icons: font [.lead] -Pillar D, artefact 2 of `establishment-plan.adoc`. A type-theoretic -notion earns "established" standing not only by having models, but by -being a *conservative, definitionally-grounded* extension of a -foundational theory. This document states that metatheorem for the -loss-graded echo modality and records its formal anchor in the -verified Agda development. +Pillar D, artefact 2 of `establishment-plan.adoc`. + +[IMPORTANT] +==== +*Narrowed 2026-05-18.* This document previously asserted a +"conservativity metatheorem … discharged operationally by the build." +That overclaimed: a green `--safe --without-K` build is necessary but +*not sufficient* for proof-theoretic conservativity (a statement +quantifying over all base propositions), and no such meta-argument is +mechanised. The metatheorem framing is retracted; what is mechanised +is stated below as build/identity *properties*, which are *evidence +for* conservativity over MLTT+Σ, not a proof of it. See +`docs/retractions.adoc` and `paper.adoc` §"Reframing note". +==== toc::[] == Statement [#thm-conservativity] -.Conservativity (definitional grounding) +.Mechanised properties (evidence for conservativity, not a proof of it) **** Let `MLTT+Σ` be Martin-Löf type theory with Σ-types and the identity type, as realised by Agda under `--safe --without-K` (no axiom K, no univalence, no postulates, no funext). Let `Echo` be the loss-graded echo modality: the object `Echo f y := Σ (x : A) , (f x ≡ y)` together with the loss-grade lattice and its reindexing action -(`EchoGraded`), and the graded-comonad structure +(`EchoGraded`), and the reindexing-coherence structure (`EchoGradedComonad`, `EchoRelModel`). -Then the extension of `MLTT+Σ` by `Echo` and all of its laws is -*conservative and definitional*: - -. *Definitional.* `Echo f y` is not a new type former. It is, by - `refl`, the homotopy fibre `fib f y` (`EchoFiberBridge.echo↔fib`, - both round-trips `refl`). No new judgement, context structure, or - formation rule is introduced — `Echo` is a derived Σ-type. -. *Conservative.* Every theorem of the development is a closed term - of `MLTT+Σ`: the entire suite typechecks under `--safe --without-K` - with *zero postulates and zero escape pragmas*. Hence any - proposition over the base vocabulary provable using `Echo` is - already provable in `MLTT+Σ` — `Echo` proves no new base facts. -. *Modality, not axiom.* The graded-comonad laws - (`gcomonad-counit-{l,r}`, `gcomonad-coassoc`) are *derived* — the - H2 verdict (see `establishment-plan.adoc`) showed each collapses to - `degrade-compose` + order-propositionality, with no path algebra - and no transport. The loss modality therefore adds structure - (a characterised graded comonad) without adding strength. +The following are *mechanised properties* of the artefact. They are +*evidence* that `Echo` adds no proof-theoretic strength over MLTT+Σ. +They are deliberately *not* packaged as a conservativity metatheorem, +because proof-theoretic conservativity quantifies over all base +propositions and is not discharged by a typechecking run: + +. *Definitional identity.* `Echo f y` is not a new type former. In + `EchoFiberBridge`, `fiber f y` is a same-module restatement of the + Σ and `echo↔fib` is the identity with `refl` round-trips. This is + a deflationary triviality (a type is bijective with itself), owned + as such — *not* a grounding theorem about an external fibre notion. +. *Postulate-free build.* The entire suite typechecks under + `--safe --without-K` with *zero postulates and zero escape + pragmas*, CI-grep-enforced. Every theorem of the development is + therefore a closed term of `MLTT+Σ`. This is necessary for + conservativity; it is *not by itself* a proof that every base + proposition provable via `Echo` is provable without it (that is a + meta-argument about the logic, which we do not mechanise). +. *Derived, not postulated.* The reindexing-coherence equations + (`gcomonad-counit-{l,r}`, `gcomonad-coassoc`) are derived: each + collapses to `degrade-compose` + order-propositionality (the H2 + verdict). Nothing is added as an axiom. Note this is the *weak* + claim — "derived" — and carries no implication that a graded + *comonad* (in the Petriček/Katsumata sense) has been exhibited; it + has not (see `paper.adoc` §"The loss-graded reindexing modality"). **** -== Why this is the clean result +== What this is, and what it is not -The honest deflationary fact — "`Echo` is just `fib`" — is precisely -what makes the metatheorem strong. A construction that *required* new -axioms (K, univalence, funext, or a postulated modality) would not be -conservative and would inherit those axioms' costs. Here the opposite -holds: the loss-graded comonad is a *theorem schema of MLTT+Σ -itself*, instantiable in multiple models (Pillar D, artefact 1: -`set-model` and `rel-model`, agreeing under the graph/fibration -bridge). "Conservative, definitionally-grounded extension" is exactly -the result that earns trust in the coeffect / quantitative lineage. +The deflationary fact — "`Echo` is just `fib`" — together with the +postulate-free build is good *evidence* that the modality is a +conservative, definitional extension of MLTT+Σ. We claim exactly that +much. We do *not* claim: -== Formal anchor +* a proof-theoretic conservativity metatheorem (clause 2 is a build + property, not a meta-proof); +* multiple independent models (`set-model` and `rel-model` fix the + same grade poset and agree by `refl`; see Pillar D artefact 1's + reframing in `paper.adoc`); +* a graded comonad (the structure is a thin-poset reindexing action). -The metatheorem is not asserted in prose alone; its three clauses are -each pinned to checked Agda artefacts already in `All.agda` / -`Smoke.agda`: +This narrower statement is what survives adversarial review. It still +earns trust in the coeffect / quantitative lineage — by being exact +about its bounds rather than by overclaiming. + +== Formal anchor (what each property is actually pinned to) + +Each mechanised property is pinned to a checked Agda artefact in +`All.agda` / `Smoke.agda`. The table states the *honest* content of +each anchor, not the previous inflated reading: [cols="1,3,2", options="header"] |=== -| Clause | Witness | Module +| Property | What the witness actually establishes | Module -| Definitional -| `echo↔fib : Echo f y ↔ fiber f y`, round-trips `refl` +| Definitional identity +| `echo↔fib : Echo f y ↔ fiber f y` is the identity with `refl` + round-trips, where `fiber` is restated in the same module — i.e. a + type is bijective with itself. A triviality, owned as such. | `EchoFiberBridge` -| Conservative -| Whole suite: `--safe --without-K`, no `postulate` / no escape - pragmas; CI greps enforce it +| Postulate-free build +| Whole suite typechecks `--safe --without-K`, no `postulate` / no + escape pragmas; CI greps enforce it. Necessary for, not a proof of, + proof-theoretic conservativity. | `All.agda` + `Smoke.agda` -| Modality not axiom -| `GradedLossModel` / `GCLaws` derive every comonad law generically; - `model-agreement` shows model-independence +| Carrier-parametric, not model-independent +| `GradedLossModel`/`GCLaws` prove the equations once *parametric in + the carrier* over a fixed grade poset; `⊑-prop` is a field (the + load-bearing hypothesis is baked in). `model-agreement` is `refl` + (second model = first `× ⊤`). Not a model-independence result. | `EchoRelModel` -| Modality not axiom +| Derived, not postulated (weak claim only) | `gcomonad-coassoc` etc. reduce to `degrade-compose` + `≤g-prop` - (H2 verdict); separating model proves the law is genuine + (H2 verdict); the separating model shows the *only* content over + generic Σ is thinness of the order. No graded comonad is exhibited. | `EchoGradedComonad`, `EchoSeparating` |=== -The conservativity argument is *operational*: it is discharged by the -build itself. Any reintroduction of a postulate, a weakening of -`--safe --without-K`, or a funext dependency would break clause 2 and -is caught by the repository's standing guardrails +These properties are *operational* (discharged by the build) only in +the weak sense that the build enforces the postulate-free / `--safe` +guardrails. They do not constitute an operational *conservativity +proof*. Any reintroduction of a postulate or weakening of +`--safe --without-K` is still caught by the standing guardrails (`establishment-plan.adoc` §"Sequencing and guardrails"). == Scope and non-claims -* This is conservativity over `MLTT+Σ` *as realised under - `--safe --without-K`*. It is not a claim about extensional type - theory, nor about theories with K or univalence. +* This is *evidence for* conservativity over `MLTT+Σ` as realised + under `--safe --without-K`. It is not a mechanised proof-theoretic + conservativity theorem, and not a claim about extensional type + theory or theories with K / univalence. * It is *not* claimed that the loss modality is interderivable with linear or dependent type strength — that comparison is a category - error (`establishment-plan.adoc` §"The honest type-theoretic - verdict"). The claim is narrower and exact: the loss-graded comonad - is a conservative, definitional *modality* in the coeffect sense. -* The funext boundary remains quarantined: `examples/Transport.agda` - stalls where `Field = Fin n → ℚ` forces funext. No conservativity - claim extends across that boundary; it is isolated by design. + error. The claim is narrower and exact: the loss-graded *reindexing + modality* is a conservative, definitional addition (not a graded + comonad, not model-independent in the semantic sense). +* Funext correction: there is *no* funext anywhere in the + development. `examples/Transport.agda` *avoids* funext by a + first-order carrier (`Vec ℚ n`); it does not "quarantine" a funext + dependency. The real funext-relativity is the *pointwise-only* + mediator property of the pullback presentation (`paper.adoc` §3), + now disclosed as the boundary rather than presented as a feature. == Revision policy @@ -124,3 +156,16 @@ recorded reason. Append-only revision history. `--safe --without-K` suite (conservative), and `EchoRelModel`/`EchoGradedComonad`/`EchoSeparating` (modality not axiom). Pillar D complete. +* *2026-05-18 — metatheorem framing retracted.* Adversarial + three-reviewer review plus a codebase pressure-test found the + "conservativity metatheorem discharged operationally by the build" + unsupported (a `--safe` build is not a proof-theoretic + conservativity proof), the "two independent models" claim false + (same grade poset, `refl` agreement), and "graded comonad" + unsupported (no nested `D_r D_s`; thin-poset action only). Statement + <> rewritten from a metatheorem to *mechanised + properties that are evidence for, not a proof of, conservativity*. + Recorded reason: see `docs/retractions.adoc` (entry R-2026-05-18) + and `paper.adoc` §"Reframing note". No Agda module changed; the + artefacts are exactly as strong as before — only the prose claims + are corrected downward. diff --git a/docs/echo-types/earn-back-plan.adoc b/docs/echo-types/earn-back-plan.adoc new file mode 100644 index 0000000..4c46265 --- /dev/null +++ b/docs/echo-types/earn-back-plan.adoc @@ -0,0 +1,176 @@ += Echo Types — Earn-Back Plan (Pillar F) +:toc: macro +:toclevels: 3 +:sectnums: +:sectnumlevels: 3 +:icons: font + +[.lead] +After retraction R-2026-05-18 the development is *honest but thin*. +This plan defines the falsifiable program to convert the retracted +claims back into theorems — or to confirm, on the project's own gate +discipline, that they cannot be earned. Nothing in `paper.adoc` / +`conservativity.adoc` / `types-abstract.adoc` moves until the +corresponding gate here passes. Same methodology as +`roadmap-gates.adoc`: explicit pass/fail, abandon criteria, outcomes +logged in `docs/retractions.adoc`. + +toc::[] + +== Honest framing + +The deflationary fact `Echo = Σ` is permanent and is *not* the +obstruction. The obstruction was that the previous structure was a +thin-poset reindexing with a carrier collapsing to `⊤`, a join used +additively with no monoid/semiring multiplication, no nested functor, +and an interface that baked in `⊑-prop`. "Earning back" means +building structure that does *not* have those defects, with Echo as +its grade-unit object — not redefining Echo. + +== Gates, in dependency order + +[#gate-F1] +=== Gate F1 — Genuine graded comonad (MAKE-OR-BREAK) + +*Everything else is gated on F1.* The other gates are not attempted +until F1 passes. + +.Claim +**** +There is a grade *monoid* `(M, ·, 1)` and an indexed endofunctor +`D : M → Set → Set` with: + +* `map : (A → B) → D r A → D r B` functorial (id/comp); +* counit `ε : D 1 A → A`; +* comultiplication `δ : D (r · s) A → D r (D s A)` — *nested*; +* the three graded-comonad laws (counit-left, counit-right, + coassociativity/pentagon) as equalities of the above; + +all under `--safe --without-K`, *zero postulates*, with `D 1 (Echo f y)` +the bare echo (Echo is the grade-unit object), and `D r` *not* +collapsing to a proposition/`⊤` for `r ≠ 1`. +**** + +.Construction under test +The candidate is the *monoid-graded iterated-residue comonad*: + +* Grade monoid `(ℕ, +, 0)` (`r` = number of residue layers; `1` of + the comonad = additive unit `0`). +* `D 0 A = A`; `D (suc r) A = R (D r A)` where `R X` is the + non-collapsing residue carrier (`EchoResidue`-shaped: `Σ X Cert` + with `Cert` *informative*, not `⊤`). +* `ε : D 0 A → A` is the structural identity at the unit grade + (legitimate for a graded comonad — the content is in `D r` being a + real functor for `r > 0` and in `δ`). +* `δ : D (m + n) A → D m (D n A)` is the iterated-functor coherence, + proved by induction on `m` (stdlib `_+_` recurses on the left and + matches `D`'s recursion, so the base case is definitional and the + step is one `cong R`). K-free and funext-free: it is `subst` along + an *inductively proven type equality*, and `subst`/transport does + not need K (K is UIP, not transport). + +.Load-bearing risk (what kills F1) +. *Coassociativity / pentagon for the iterated-functor identity does + not close without K* once `Cert` carries non-trivial identity + proofs. This is F1's real test — the honest analogue of the old + `degrade-compose`, but now genuinely about nested functors. +. *`δ` degenerates to the identity coercion in a way that a + Petriček/Katsumata reader still reads as bookkeeping.* Mitigation + bar: `D r` must be demonstrably a non-trivial functor (a separating + witness: two elements of `D 2 A` distinguished by `Cert`, so `D` is + not constantly `A` or `⊤`). +. *Naturality of `ε`/`δ` needs funext* (they are natural + transformations between endofunctors). Mitigation: state naturality + *pointwise* and only claim a graded comonad in the + pointwise/“wild” sense, disclosed — or accept F1 fails for the + strict categorical claim. + +.Gate +*F1 passes* iff `map`/`ε`/`δ` and all three laws typecheck +`--safe --without-K`, zero postulates, with the non-triviality +separating witness for `D 2`. *F1 fails* if any law needs K, funext, +or a postulate, or if `D r` cannot be shown non-trivial. + +.Abandon criterion +If F1 fails, the graded-comonad claim stays retracted *permanently*; +record in `docs/retractions.adoc` as a second negative result +(strengthens the methodology story, like EI-2). Do *not* attempt +F3/F4. F2 may still proceed (it is independent of F1). + +[#gate-F2] +=== Gate F2 — A real second model of the *bare* Echo functor + +Independent of F1 (about the Echo functor, not the comonad). The one +R2 item rated "fixable with bounded work". + +.Claim +**** +A model instance that genuinely uses `EchoRelational.StepND` +(non-deterministic, `StepND : Bool → Bool → Set` with a relation that +is *not* a graph of a function), in which the Echo-functor laws hold, +and whose agreement with the deterministic model is a theorem with +*content* (not `refl`, not Σ-η on `× ⊤`). +**** + +.Gate +*Passes* iff a `StepND`-based model is instantiated into the same +interface the deterministic model uses, the functor laws hold, and +the agreement lemma has a non-`refl` proof obligation. *Fails* if the +only way to make it agree is to trivialise the relation back to a +graph. + +[#gate-F3] +=== Gate F3 — A genuinely independent second model of the comonad + +*Gated on F1.* Instantiate F1's graded-comonad interface at a +*different grade monoid* (e.g. a tropical or multiplicative semiring, +or a free monoid) — not the same monoid with a `× ⊤` carrier. Pass +iff the laws hold for two non-isomorphic grade monoids and the +abstraction does not carry a field equivalent to the old `⊑-prop` +(no single hypothesis bakes in the result). + +[#gate-F4] +=== Gate F4 — Universal property, honestly qualified + +Not "retracted → unconditional"; "retracted → *true, conditional*". +Parameterise the terminality theorem by an explicit funext +hypothesis `funext` (a module parameter, *not* a postulate), exactly +as `Echo.agda` parameterises `cancel-iso` by the triangle identities. +Then `echo-pullback-univ-strict : funext → (m' ≡ m)` is a genuine +universal property *given funext*, with zero postulates retained. + +.Gate +*Passes* iff strict terminality typechecks as a function of an +explicit `funext` parameter, zero postulates, and the unconditional +pointwise result is kept as the funext-free corollary. This is +expected to be tractable; it earns back a *qualified* universal +property, stated as such. + +== Sequencing + +. *F1 first* (make-or-break). Begin with the feasibility spike + `proofs/agda/EchoGradedComonadF1.agda` (prototype, not wired into + `All.agda`/`Smoke.agda` until it passes). +. *F4 and F2 in parallel* (both independent of F1; both expected + tractable). They earn back qualified/real claims regardless of F1. +. *F3 only if F1 passes.* +. On each gate: update `paper.adoc` / `conservativity.adoc` / + `types-abstract.adoc` to the *earned* claim, and log the outcome + (pass or fail) in `docs/retractions.adoc` as a follow-up to + R-2026-05-18. A failed gate is a second negative result, not a + silent revert. + +== Guardrails + +* No postulates, no escape pragmas, `--safe --without-K`, ever — a + gate "passed" by weakening these is failed. +* No prose claim moves ahead of its gate. The reframed docs stay as + they are until the corresponding gate is green. +* "Triage over partial hack": if a gate is close but not closed, it + is *failed and logged*, not shipped behind softened wording. + +== Status + +* *2026-05-18 — created.* Pillar F opened post-R-2026-05-18. F1 + feasibility spike is the immediate next action. No gate passed yet; + no reframed claim has moved. diff --git a/docs/echo-types/establishment-plan.adoc b/docs/echo-types/establishment-plan.adoc index 0464afc..65822b1 100644 --- a/docs/echo-types/establishment-plan.adoc +++ b/docs/echo-types/establishment-plan.adoc @@ -15,6 +15,27 @@ like this *established* in the sense that linear, dependent, or graded modal types are established — and what specifically must this repository ship to get there. +[IMPORTANT] +==== +*Framing retracted 2026-05-18 (`docs/retractions.adoc` R-2026-05-18).* +This plan was written when the development was believed to ship a +graded comonad, a universal property, two independent models, and a +conservativity metatheorem. Adversarial review + a codebase +pressure-test found no in-repo defense for any of these, and the +repo's own Gate-2 audit contradicted two. The plan is retained as the +*historical record of the strategy*, but every occurrence below of +"graded comonad", "universal property / terminal cone", "two +independent models / model-independence", and "conservativity +metatheorem / irreducibility metatheorem" must be read as the +*narrowed* claims: a loss-graded *reindexing modality* (thin-poset +action, no nested `D_r D_s`); a *funext-relative pointwise mediator +property*; *carrier-parametricity over a fixed grade poset*; and a +*postulate-free build that is evidence for, not a proof of, +conservativity*. The current honest statements live in +`paper.adoc`, `conservativity.adoc`, `types-abstract.adoc`. The Agda +is unchanged; only the prose claims were corrected downward. +==== + toc::[] == The honest type-theoretic verdict @@ -34,25 +55,34 @@ strategy and is owned, not hedged: bespoke "echo introduction/elimination rules" dressed as primitive would be the fastest possible way to lose every informed reader. -* *The strength that befits echo is a graded comonadic modality — - the coeffect / quantitative lineage.* That _is_ an established - type strength in the modern sense (Petriček–Orchard–Mycroft - coeffects; Brunel–Gaboardi–Mazza–Zdancewic; Atkey's Quantitative - Type Theory; Orchard–Liepelt–Eades / Granule; Gaboardi et al. - graded modal types). The repo's own code already has the shape: - `EchoGraded`'s loss-grade lattice with join and universal property, - `EchoLinear`'s two-mode degradation, `EchoCategorical`'s - slice/fibration functor laws. It is not yet *named, characterised, - and proved* as a graded comonad of structured loss. +* *The strength that befits echo is a loss-graded reindexing + modality — motivated by, but not an instance of, the coeffect / + quantitative lineage* (Petriček–Orchard–Mycroft coeffects; + Brunel–Gaboardi–Mazza–Zdancewic; Atkey's Quantitative Type Theory; + Orchard–Liepelt–Eades / Granule; Gaboardi et al. graded modal + types). [RETRACTED READING: this was originally "a graded comonadic + modality… proved as a graded comonad of structured loss". It is + *not* a graded comonad — no nested `D_r D_s` is formed. The repo's + code has a thin-poset reindexing action: `EchoGraded`'s loss-grade + lattice + monotone `degrade`, `EchoLinear`'s two-mode degradation, + `EchoCategorical`'s slice/fibration functor laws.] [#thesis] -.The establishment thesis +.The establishment thesis (narrowed 2026-05-18) **** Echo is the homotopy fibre, equipped with a loss-grade lattice, -forming a *definitionally-grounded graded comonad of structured loss*. -Its authority comes not from being a new object but from being a -*characterised* one: a universal property, multiple models, an -irreducibility metatheorem, and a falsifiable retraction discipline. +carrying a *definitionally-grounded loss-graded reindexing modality* +(a thin-poset action — *not* a graded comonad). Its standing comes +not from being a new object but from being *exactly characterised and +honestly bounded*: a definitional Σ-identity; a funext-relative +pointwise mediator property; coherence equations that provably reduce +to thinness of the grade order; a separating model that locates that +reduction; a carrier-parametric abstraction; a postulate-free build; +and a falsifiable retraction discipline of which the 2026-05-18 +reframing is itself an instance. _Original wording: "forming a +definitionally-grounded graded comonad of structured loss… a +universal property, multiple models, an irreducibility metatheorem" — +retracted, see R-2026-05-18._ **** Owning "it is just `fib`" loudly is a credibility asset: it pre-empts @@ -91,14 +121,18 @@ the composition iso, cancel-iso, pentagon — but no _characterisation_. `echo-pullback-univ` (existence + funext-free pointwise uniqueness, no K — uniqueness uses stdlib `Σ-≡,≡→≡` on the `factor`/`coherent` legs). -* Artefact 2: `EchoGradedComonad.agda` (headline new family) — reuse - `EchoGraded._≤g_`, `_⊔g_`, `≤g-prop`; define the graded counit / - comultiplication and prove the three graded-comonad laws over the - loss-grade lattice. *Thin slice landed 2026-05-17:* `gextract`, - `gduplicate`, and all three laws (`gcomonad-counit-{l,r}`, - `gcomonad-coassoc`) — see the verdict in <>. -* Authority effect: "has a universal property + is a graded comonad" - is the line between a named lemma cluster and an established notion. +* Artefact 2: `EchoGradedComonad.agda` — reuse `EchoGraded._≤g_`, + `_⊔g_`, `≤g-prop`; `gextract` (the identity coercion, `keep` being + the definitional bottom), `gduplicate` (the join-left *single-grade* + reindex), and the three coherence equations + (`gcomonad-counit-{l,r}`, `gcomonad-coassoc`). [RETRACTED READING: + "the three graded-comonad laws" / "is a graded comonad" — these are + thin-poset reindexing-coherence equations; no comonad is exhibited. + See <> and R-2026-05-18.] +* Authority effect (narrowed): "has a definitional identity + a + funext-relative pointwise mediator property + a reindexing modality + whose coherence reduces to order-thinness" — exactly bounded, not a + universal property and not a graded comonad. === Pillar C — An irreducibility metatheorem @@ -127,30 +161,28 @@ Harden Gate 2. The existing `VisibleConstraintAudit` / A notion is established only if it is model-independent. -* Artefact 1: `EchoRelModel.agda` — extend - `EchoCategorical.Fibration` / `EchoRelational`; show the - graded-comonad laws of Pillar B transport into the relational / - presheaf model. Two independent models = robustness. *Landed - 2026-05-17:* the H2 verdict is leveraged into the strongest - model-independence form — an abstract `GradedLossModel` interface - with the comonad laws proved *once* generically (`module GCLaws`), - instantiated at `set-model` (EchoGraded) and `rel-model` - (relational `EchoStep`/`map-rel`, composition from `map-rel-comp` - + `degrade-comp`), with `model-agreement` (round-trips `refl`) and - `bridge-natural` (`map-over` ↔ `map-rel` under the graph bridge). -* Artefact 2: `docs/echo-types/conservativity.adoc` (+ formal anchor) - — because `Echo = Σ`, a small graded calculus with a loss modality - embeds *conservatively and definitionally* into MLTT+Σ. State this - as a metatheorem. "Conservative, definitionally-grounded extension" - is exactly the clean result that earns trust. *Landed 2026-05-17:* - the metatheorem is stated with a three-clause formal anchor — - definitional (`EchoFiberBridge`), conservative (postulate-free - `--safe --without-K` suite, operationally enforced by CI greps), - modality-not-axiom (`EchoRelModel`/`EchoGradedComonad`/ - `EchoSeparating`). Scope and non-claims explicit; funext boundary - quarantined. -* Authority effect: model-independence + a conservativity theorem turn - the deflation into a published positive result. +* Artefact 1: `EchoRelModel.agda` — `GradedLossModel`/`GCLaws`, + instantiated at `set-model` and `rel-model`. [RETRACTED READING: + "two independent models = robustness / the strongest + model-independence form". Both instances fix the *same* grade poset; + `rel-model`'s carrier is the Set carrier `× ⊤`; `model-agreement` + is `refl`; the interface's `⊑-prop` field bakes in the only + load-bearing hypothesis. This is *carrier-parametricity over a + fixed poset*, not model-independence. R-2026-05-18.] +* Artefact 2: `docs/echo-types/conservativity.adoc` — because + `Echo = Σ` definitionally and the suite is postulate-free under + `--safe --without-K` (CI-grep-enforced), this is *evidence that* + the loss modality adds no strength over MLTT+Σ. [RETRACTED READING: + "State this as a metatheorem" / "a conservativity theorem". A green + `--safe` build is necessary but not sufficient for proof-theoretic + conservativity; no meta-argument is mechanised, so this is *not* + stated as a metatheorem. Funext correction: there is no funext + anywhere; `examples/Transport.agda` *avoids* it by carrier choice + rather than "quarantining" it — the real funext-relativity is the + pointwise-only mediator property. R-2026-05-18.] +* Authority effect (narrowed): an exactly-bounded, postulate-free + package under a falsifiable retraction discipline — not + model-independence plus a conservativity theorem. === Pillar E — External validation @@ -209,6 +241,22 @@ firewalled from the identity claim exactly as `roadmap.md` already does. [#h2-verdict] == H2 verdict — does graded coassociativity need path algebra? (2026-05-17) +[CAUTION] +==== +*Reading reversed 2026-05-18 (R-2026-05-18).* The collapse described +below is real and the Agda is unchanged — but its significance is the +*opposite* of "thesis-strengthening". The equations reduce to +`degrade-compose` + `≤g-prop` because *there is no comonadic +coherence to discharge*: a thin poset with a functorial monotone +action satisfies them definitionally. This is the calibration that +shows the modality's entire content over generic Σ is thinness of the +grade order — confirmed by the separating model and by the repo's own +Gate-2 audit. Read "graded-comonad laws" below as +"thin-poset reindexing-coherence equations", and disregard the +"*Thesis impact (positive)*" paragraph (struck through in substance, +retained for the record). +==== + *The pivotal de-risking question, answered: NO.* The thin slice (`gextract`, `gduplicate`, `gcomonad-counit-l`, `gcomonad-counit-r`, `gcomonad-coassoc`) typechecks under `--safe --without-K` with no @@ -230,12 +278,15 @@ same idiom `EchoGraded.degrade-via-join` already uses; it is a faithful (not weakened) statement of the comonad coherence in the join-semilattice presentation. -*Thesis impact (positive):* the "characterised graded comonad of -structured loss" claim rests cleanly on machinery the repo has -already proved. The graded-comonad strength is not bought with extra -axioms or path algebra — it is a corollary of the loss lattice being -a propositional order with a universal join. The thesis (<>) -stands and is *strengthened*; no honest rewrite is required. +*Thesis impact — RETRACTED 2026-05-18.* This paragraph originally +read: "the 'characterised graded comonad of structured loss' claim +rests cleanly on machinery the repo has already proved… the thesis +stands and is *strengthened*; no honest rewrite is required." That +conclusion was wrong. There is no graded-comonad strength; the +collapse to thinness is a *bound*, not a strengthening. An honest +rewrite *was* required and has been done (`paper.adoc`, +`conservativity.adoc`, `types-abstract.adoc`, R-2026-05-18). The +narrowed thesis (<>) is what stands. == Status @@ -313,3 +364,21 @@ reason. be filled as more context accrues; not for submission until those clear. Remaining Pillar E (Zenodo DOI, library packaging, submission logistics, outreach) is offline / author-driven. +* *2026-05-18 — trigger: adversarial review + codebase pressure-test; + framing retraction (R-2026-05-18).* The Pillar B/C/D framing in the + entries above is retracted, not rewritten (append-only history). + No in-repo defense was found for "graded comonad", "universal + property / terminal cone", "two independent models / + model-independence", or "conservativity metatheorem"; the repo's + own Gate-2 audit contradicted two. The mechanised content is + unchanged and the entries above remain accurate as a record of + *what landed*; only their *significance claims* are corrected, to: + a loss-graded reindexing modality (not a comonad); a funext-relative + pointwise mediator property (not a universal property); + carrier-parametricity over a fixed grade poset (not + model-independence); a postulate-free build that is evidence for, + not a proof of, conservativity. Authoritative current statements: + `paper.adoc` §"Reframing note", `conservativity.adoc`, + `types-abstract.adoc` ("submission-ready" status withdrawn), + `docs/retractions.adoc` R-2026-05-18. Pillars A–D stand at their + *narrowed* strength; Pillar E re-review is the open item. diff --git a/docs/echo-types/paper.adoc b/docs/echo-types/paper.adoc index fd917fb..2cfeb10 100644 --- a/docs/echo-types/paper.adoc +++ b/docs/echo-types/paper.adoc @@ -1,4 +1,4 @@ -= Echo Types: A Definitionally-Grounded Graded Comonad of Structured Loss += Echo Types: A Definitionally-Grounded, Loss-Graded Reindexing Modality :toc: macro :toclevels: 3 :sectnums: @@ -33,14 +33,28 @@ not a footnote. The thesis of the paper is that the type-theoretic standing that *befits* echo is not the linear/dependent judgmental ladder — that -comparison is a category error — but a **graded comonadic modality of -structured loss** in the coeffect/quantitative lineage. The -contribution is the full *characterisation package*, mechanised in -Agda under `--safe --without-K` with zero postulates: a definitional -identity, a universal property, a graded comonad whose laws provably -reduce to order-propositionality, a separating model, model -independence across two models, and a conservativity metatheorem — -all under a falsifiable-gate methodology with a public retraction log. +comparison is a category error — but a **loss-graded reindexing +modality**: a monotone family indexed by a join-semilattice of loss +grades, with a functorial reindexing action. It is *analogous to*, +and motivated by, the coeffect/quantitative lineage, but we are exact +about what is and is not mechanised. In particular it is *not* a +graded comonad in the Petriček–Orchard–Mycroft / Katsumata sense: no +nested functor `D_{r·s} ⇒ D_r D_s` is formed, and the structure maps +are the lattice-bottom coercion and the join-left reindex, not a +genuine counit/comultiplication pair. + +The contribution is a *characterisation package*, mechanised in Agda +under `--safe --without-K` with zero postulates: a definitional +identity; a pointwise (funext-relative) mediator property for the +pullback presentation; a reindexing modality whose coherence +equations provably reduce to *thinness of the grade order*; a +separating model that pins exactly that reduction; a carrier-parametric +abstraction over a fixed grade poset; and a postulate-free build — all +under a falsifiable-gate methodology with a public retraction log +(`docs/retractions.adoc`). The earlier framing of this development as +a "graded comonad with two independent models and a conservativity +metatheorem" was retracted on 2026-05-18 after adversarial review; +see <> and the retraction log. === Why not "linear or dependent" @@ -58,23 +72,46 @@ the rest of the paper bears. === Contributions . *Pinned identity.* `echo↔fib : Echo f y ↔ fiber f y`, - definitional, `refl` round-trips (Pillar A). -. *Universal property.* `Echo f y` as the pullback of `f` along the - point `y : ⊤ → B`, with a funext-free, K-free terminal-cone - property; a `SliceHom` *is* a cone (Pillar B-1, §3). -. *Graded comonad.* counit / comultiplication over the loss-grade - join-semilattice and all three laws — with the *H2 verdict* - (§4.2): every law, coassociativity included, collapses to one - path-independence lemma plus order-propositionality, with no path - algebra (Pillar B-2). -. *Separating model.* the graded model minus its single hypothesis + definitional, `refl` round-trips (Pillar A). `fiber` is a + same-module restatement of the Σ; the bridge is the identity. This + is a deflationary triviality, owned as such, not a metatheorem. +. *Pointwise mediator property.* `Echo f y` presented as the pullback + of `f` along the point `y : ⊤ → B`; a `SliceHom` *is* a cone + (round-trips `refl`). `echo-pullback-univ` gives existence and + *pointwise* uniqueness `∀ v → m' v ≡ m v`. We do *not* claim full + terminality: `m' ≡ m` is neither stated nor provable here without + funext, so this is a funext-relative mediator property, not a + universal property in the categorical sense (Pillar B-1, §3). +. *Loss-graded reindexing modality.* A monotone family `GEcho` over + the loss-grade join-semilattice with a functorial reindex + `degrade`. The "counit" is the identity coercion (the bottom grade + `keep` is absorbed definitionally); the "comultiplication" is the + join-left reindex `GEcho g₁ → GEcho (g₁ ⊔ g₂)` — a *single* grade + application, *not* a nested `D_r D_s`. The three coherence + equations (§4.2) hold for exactly one reason: the grade order is + thin (`≤g-prop`) and `degrade` is functorial (`degrade-compose`). + This is a thin-poset action, not a graded comonad (Pillar B-2). +. *Separating model.* the model minus its single hypothesis `≤g-prop`: generic Σ-functoriality survives, the characteristic - law is refuted at a decidable witness (Pillar C, §5). -. *Model independence and conservativity.* an abstract model - interface with the comonad laws proved once; two agreeing models; - a conservativity metatheorem (Pillar D, §6). + composition law is refuted at a decidable witness. Read precisely, + this *measures* the modality's content over generic Σ: it is + exactly thinness of the grade order, nothing more (Pillar C, §5). +. *Carrier-parametric abstraction (not model-independence).* an + abstract interface `GradedLossModel` whose `⊑-prop` field *fixes* + the only load-bearing hypothesis; the coherence equations are + proved once, parametric in the carrier, over a *fixed* grade + poset. The "second model" is the first with a `⊤` component, + agreeing definitionally (`refl`). This is carrier-parametricity, + not semantic model-independence (Pillar D, §6). +. *Postulate-free build (not a conservativity metatheorem).* the + whole development typechecks `--safe --without-K` with zero + postulates / zero escape pragmas, CI-enforced. With `Echo = Σ` + definitionally this is *evidence for* conservativity over MLTT+Σ; + it is not a mechanised proof-theoretic conservativity theorem, + and is no longer stated as one (§6.2). . *Methodology.* falsifiable gates with explicit retraction actions; - one identity claim settled negatively and logged (§7). + identity claims settled negatively and logged, including this + development's own framing retraction (§7, <>). == Background and notation [EXPAND] @@ -88,90 +125,145 @@ Orchard–Liepelt–Eades / Granule) and a one-paragraph HoTT-fibre recap, so the paper is readable by both the QTT and the HoTT communities without external lookup. -== The universal property +== The pullback presentation and its pointwise mediator property -`Echo f y` is the pullback of `f : A → B` along the point -`y : ⊤ → B`. The `⊤`-leg is forced, so a cone with apex `V` is +`Echo f y` is presented as the pullback of `f : A → B` along the +point `y : ⊤ → B`. The `⊤`-leg is forced, so a cone with apex `V` is exactly a map `p₁ : V → A` with `∀ v → f (p₁ v) ≡ y` — which *is* an `EchoCategorical.SliceHom (λ (_ : V) → y) f`; the bridge -round-trips are `refl`. The terminal-cone property -`echo-pullback-univ` gives existence (the obvious pairing) and -*pointwise* uniqueness `∀ v → m' v ≡ m v` (not `m' ≡ m`, hence -funext-free); the cone-morphism notion carries a witness-transport -leg, which is what makes uniqueness provable without K (no UIP on -`f a ≡ y` is assumed). This is the categorical-semantics anchor: a -category theorist accepts echo as the limit of a cospan. +round-trips are `refl`. `echo-pullback-univ` gives existence (the +obvious pairing) and *pointwise* uniqueness `∀ v → m' v ≡ m v`; the +cone-morphism notion carries a witness-transport leg, which is what +makes the pointwise statement provable without K (no UIP on +`f a ≡ y` is assumed). -== The graded comonad of structured loss +[CAUTION] +==== +This is *not* a universal property in the categorical sense, and we +no longer claim it is. Terminality requires uniqueness of the +mediating *morphism*, `m' ≡ m` in the hom-type. That statement is +neither made nor provable here: under `--safe --without-K` it +requires funext, which the development forbids. What is mechanised +is strictly weaker — a pointwise-agreeing mediator. A category +theorist does *not*, on this evidence, accept echo as the limit of +the cospan; the honest claim is a funext-relative mediator property. +The previously asserted "terminal-cone universal property" and "a +category theorist accepts echo as the limit of a cospan" were +retracted on 2026-05-18 (see <>). +==== + +== The loss-graded reindexing modality === Structure Over the loss-grade join-semilattice `(Grade, ⊔, keep)` with `keep` -the bottom / monoidal unit: the counit `gextract` (zero-loss echo is -the bare echo — the Pillar-A definitional move reused) and the -comultiplication `gduplicate` (duplicating an observation splits the -loss budget along the join, realised as the join-left embedding). +the bottom: `GEcho` is a monotone family of types and `degrade` its +functorial reindexing. We retain the names `gextract` and +`gduplicate` for continuity with the modules, but state plainly what +they are: + +* `gextract : GEcho keep → Echo collapse tt` is `λ e → e` — the + literal identity coercion. `GEcho keep` is *definitionally* + `Echo collapse tt` and `keep ⊔ g = g` definitionally, so the + "counit law" holds for free; this is the Pillar-A identity reused, + not a structure map with content. +* `gduplicate g₁ g₂ : GEcho g₁ → GEcho (g₁ ⊔ g₂)` is the join-left + reindex `degrade (≤-⊔-left g₁ g₂)`. It is a *single* grade + application. There is no nested `GEcho (GEcho …)` and no + `D_{r·s} ⇒ D_r D_s` anywhere in the development, so this is not a + graded comultiplication; it is monotone reindexing into the join. [#h2-verdict] -=== The H2 verdict (key technical insight) - -Stated in the *common-upper-bound idiom* — post-compose each -(co)multiplication with the universal degrade into an *arbitrary* -common grade, so both sides of every law land in the same object — -the three graded-comonad laws (`gcomonad-counit-{l,r}`, -`gcomonad-coassoc`) each collapse to exactly two ingredients: the -path-independence lemma `degrade-compose` and propositionality of the -loss order `≤g-prop`. There is no path algebra, no `subst`, no -transport. The naive grade-equality phrasing of coassociativity would -force a `subst` along `⊔`-associativity; the universal-arrow phrasing -removes it entirely, because the join is a universal arrow and the -order is a proposition. - -This is the paper's pivotal observation: the modality is *cheap* -(no coherence tower) and, as §6 shows, *model-independent for the -same reason* (the proof never inspects the carrier). +=== The H2 verdict, stated honestly + +In the *common-upper-bound idiom* — post-compose each side with +`degrade` into an arbitrary common grade — the three coherence +equations (`gcomonad-counit-{l,r}`, `gcomonad-coassoc`) each collapse +to exactly two ingredients: the path-independence lemma +`degrade-compose` and propositionality of the loss order `≤g-prop`. +There is no path algebra, no `subst`, no transport. + +The honest reading of this collapse is the opposite of a strength +claim. The equations reduce to thinness because *there is no +comonadic coherence to discharge*: a thin poset with a functorial +monotone action satisfies these equations definitionally. The +separating model (§5) confirms this precisely — delete `≤g-prop` and +the characteristic equation breaks, while generic Σ-functoriality is +untouched. So the entire content of this modality over and above +generic Σ is exactly: *the grade order is thin*. We report this as a +calibration result, not as evidence of a cheap coherence tower. The +project's own Gate-2 audit (`docs/characteristic.adoc`) reaches the +same conclusion for the wider "characteristic theorem family" (all +instances of one `X-compose = X-prop + X-comp` recipe). == The separating model -The separating model is the graded model with its *single* hypothesis +The separating model is the modality with its *single* hypothesis `≤g-prop` deleted: a loss order with two distinct arrows `lo→hi` and a reindexing that distinguishes them. Generic Σ-functoriality (`map-over` id/comp) and the functorial unit still hold verbatim — it -is a bona-fide Echo setting. The characteristic composition law is -*refuted* at a concrete decidable witness, discharged by a checked -`true ≢ false`. Conclusion: the loss law is not a generic -Σ-consequence; it is carried *precisely* by order-propositionality. -This is a positive countermodel object, extending the project's -negative-exhibit discipline, and it answers the only objection every -referee raises ("isn't this all Σ-lemmas with renamed components?") -with a model rather than an argument. - -== Model independence and conservativity - -=== Two models, one structure - -An abstract interface `GradedLossModel` (a propositional grade order -with a join and a composing reindexing) — exactly what the H2 verdict -showed suffices. The graded-comonad laws are proved *once*, -generically, from the interface (`GCLaws`); this *is* the -model-independence theorem. Two instances: the Set/Type model -(`EchoGraded`) and a relational model (`EchoStep`/`map-rel`, the -composition law from `map-rel-comp` + `degrade-comp`). They agree -under the graph = fibration bridge: `model-agreement` (carrier iso, -round-trips `refl`) and `bridge-natural` (`map-over` ↔ `map-rel`). -The graded comonad is the *same* structure in both. - -=== Conservativity +is a bona-fide Echo setting. The characteristic composition equation +is *refuted* at a concrete decidable witness, discharged by a checked +`true ≢ false`. + +We state the conclusion precisely, without spin. The separating model +does not show the modality is "genuine structure, not bookkeeping" in +the reviewer's sense; it *quantifies* the gap. The characteristic +equation is not a generic Σ-consequence — but the *only* thing it +adds over generic Σ-functoriality is `≤g-prop`, i.e. that the grade +order is thin. A reader who regards "the grade preorder is thin" as +sufficient structure may keep the framing; a reader who does not will +correctly read this as Σ-functoriality over a thin poset. The +countermodel is a real, citable calibration object; it does not +neutralise the "Σ over a poset" objection so much as locate it +exactly. + +== Carrier-parametricity, and the limits of the conservativity claim + +=== One structure, parametric in the carrier — not model-independence + +An abstract interface `GradedLossModel` packages a grade order with a +join and a composing reindexing, *and* an explicit field +`⊑-prop : ∀ p q → p ≡ q`. The coherence equations are proved once, +generically (`GCLaws`). We previously called this "the +model-independence theorem"; it is not. Two observations defeat that +reading: + +. The interface *bakes in the only load-bearing hypothesis.* `⊑-prop` + is the single ingredient §5 isolates; making it a field means every + instance is forced thin by signature. "Proved once for any model" + is then "proved once for any thin poset action," which is the + statement, not an independence result. +. The two instances are not independent models. `set-model` and + `rel-model` fix the *same* grade poset (`_≤g_`, `≤g-prop`, `_⊔g_`, + `keep`); only the carrier differs, and `rel-model`'s carrier is the + Set carrier with a `⊤` component (`RStep _ _ = ⊤`). `model-agreement` + is `refl` — agreement holds by Σ-η on `× ⊤`, with no semantic + content. No instance at a different grade structure exists, or can + (the equations require thinness). This is parametricity in an + inert carrier component, not semantic model-independence. + +The genuinely relational object (`StepND`, nondeterminism) exists in +`EchoRelational` but is *never* instantiated into a `GradedLossModel`; +the "graph = fibration bridge" `bridge-natural` is the identity on +Σ-pairs (`refl`). We no longer claim a relational model of the +modality. + +=== The conservativity claim, narrowed Because `Echo = Σ` definitionally and the whole development is -postulate-free under `--safe --without-K`, the loss modality is a -*conservative, definitional* extension of MLTT+Σ: it adds structure -(a characterised graded comonad) without adding strength. The -metatheorem (`conservativity.adoc`) has a three-clause formal anchor: -definitional (`EchoFiberBridge`), conservative (the postulate-free -build, CI-enforced), modality-not-axiom (`EchoRelModel` / -`EchoGradedComonad` / `EchoSeparating`). The conservativity argument -is *operational* — discharged by the build itself. +postulate-free under `--safe --without-K`, with zero escape pragmas +and CI greps enforcing it, the artefact is *evidence* that the loss +modality adds no proof-theoretic strength over MLTT+Σ. We state only +that. We do *not* claim a mechanised conservativity metatheorem: a +green `--safe` build is necessary but not sufficient for proof-theoretic +conservativity (a statement quantifying over all base propositions), +and no such meta-argument is mechanised. `conservativity.adoc` has +been narrowed accordingly: clause 1 (`EchoFiberBridge`) is the +definitional Σ-identity it is; clause 2 is restated as the +postulate-free build property; the "modality not axiom" clause is +retained only in the weak, true form — the reindexing modality is +*derived*, not postulated. == Methodology: falsifiable gates and retraction @@ -179,19 +271,32 @@ Development is governed by gates (`roadmap-gates.adoc`) with explicit retraction actions and a public retraction log. One identity claim, the five-axis simultaneous-integration claim (EI-2), was settled *negatively* and is recorded as such; having cleanly killed it is -part of the authority story, not a blemish. The funext boundary is -real, known, and quarantined behind an isolated module -(`examples/Transport.agda`, where `Field = Fin n → ℚ` forces funext); -no result crosses it. We argue this discipline is itself a -contribution: a template for honest mechanised-metatheory claims. +part of the authority story, not a blemish. + +A correction to the funext story, which earlier drafts stated +backwards. There is *no* funext anywhere in the development +(consistent with `--safe`). `examples/Transport.agda` does not +*contain* a quarantined funext dependency — it *avoids* funext by a +first-order carrier choice (`Field n = Vec ℚ n`; a `Fin n → ℚ` +carrier would have forced funext and was rejected). So "quarantined +behind an isolated module" mis-described a counterfactual. The place +funext-relativity *actually* bites is the pullback presentation: its +mediator property is only pointwise precisely because `m' ≡ m` needs +funext (§3). We now disclose that as the genuine boundary rather than +present "funext-free" as a feature. We still argue the gate / +retraction discipline is a contribution — and this very reframing, +logged in `docs/retractions.adoc`, is the discipline working. == Evaluation and discussion [EXPAND] -NOTE: *[EXPAND]* — proof-size / proof-cost table per pillar; what the -common-upper-bound idiom buys versus the naive `subst` phrasing -(quantified); a discussion of where the construction does *not* -extend (the EI-2 negative result, the funext boundary) framed as -strengths; threats to validity. +NOTE: *[EXPAND]* — proof-size / proof-cost table per pillar; the +common-upper-bound idiom analysed honestly (it removes `subst` +*because* the equations carry no comonadic coherence, not as a clever +saving); a discussion of where the construction does *not* extend +(the EI-2 negative result; the funext-relative mediator property; the +thinness-only content) stated as honest bounds, *not* spun as +strengths; threats to validity, including the Gate-2 audit's own +"single recipe" finding. == Related work [EXPAND] @@ -203,16 +308,57 @@ lens / optic literature (the witness-transport leg of the novelty crisp: not a new object, but a fully mechanised characterisation package with a falsifiable-gate methodology. +[#reframing-note] +== Reframing note (2026-05-18) + +This draft was reframed after an adversarial three-reviewer review +(graded-modality, semantics, and proof-assistant skeptics) found that +the codebase contains no defense for five central claims, and that +two were contradicted by the repository's own Gate-2 audit. The +following claims were retracted, not weakened cosmetically: + +[cols="2,3", options="header"] +|=== +| Retracted claim | Replaced by + +| "graded comonad" (counit/comultiplication, three comonad laws) +| loss-graded *reindexing modality*; no nested `D_r D_s` is formed; + the equations hold by thinness of the grade order + +| "terminal-cone universal property"; "a category theorist accepts + echo as the limit of a cospan" +| a *pointwise, funext-relative* mediator property; full terminality + is unstatable here without funext + +| "model independence across two agreeing models" +| carrier-parametricity over a *fixed* grade poset; the second model + is the first with a `⊤` component, agreeing by `refl` + +| "conservativity metatheorem, discharged operationally by the build" +| a *postulate-free build*: evidence for, not a proof of, + conservativity over MLTT+Σ + +| "funext quarantined behind an isolated module; no result crosses it" +| no funext anywhere; the real funext-relativity is the pointwise + mediator property, now disclosed as the boundary +|=== + +The full per-attack analysis and the codebase pressure-test are in +`docs/retractions.adoc`. + == Conclusion Echo is the homotopy fibre equipped with a loss-grade lattice, -forming a definitionally-grounded graded comonad of structured loss. -Its standing comes not from being new but from being *characterised*: -a universal property, a law-set that provably reduces to -order-propositionality, a separating model, two agreeing models, and -a mechanised conservativity metatheorem — with a falsifiable -retraction discipline. The internal programme is complete; external -validation is the remaining step. +carrying a loss-graded reindexing modality. What survives adversarial +review is narrower than first claimed but exactly stated: a +definitional Σ-identity; a funext-relative pointwise mediator +property; a reindexing modality whose coherence equations reduce, +demonstrably, to thinness of the grade order; a separating model that +locates that reduction precisely; a carrier-parametric abstraction; +and a postulate-free `--safe --without-K` build. Its standing comes +from being *exactly characterised and honestly bounded* under a +falsifiable retraction discipline — of which this reframing is an +instance. External validation is the remaining step. [appendix] == Ordinal / Buchholz consumer-evidence [EXPAND] diff --git a/docs/echo-types/types-abstract.adoc b/docs/echo-types/types-abstract.adoc index 2e7f8b2..6b19916 100644 --- a/docs/echo-types/types-abstract.adoc +++ b/docs/echo-types/types-abstract.adoc @@ -1,4 +1,4 @@ -= Echo: a definitionally-grounded graded comonad of structured loss += Echo: a definitionally-grounded, loss-graded reindexing modality :toc: macro :toclevels: 2 :sectnums: @@ -6,10 +6,21 @@ [.lead] Pillar E, artefact 1 of `establishment-plan.adoc`: a TYPES-style -extended abstract (≈2 pp). Submission-ready draft; the social steps -(submission, reviewing, DOI) remain offline and require the author. -Every claim below is mechanised in the accompanying -`--safe --without-K` Agda artefact and pinned in `Smoke.agda`. +extended abstract (≈2 pp). + +[IMPORTANT] +==== +*NOT submission-ready (status withdrawn 2026-05-18).* This abstract +previously claimed a graded comonad, two independent models, a +conservativity metatheorem and a terminal-cone universal property. +All four were retracted after adversarial review — see +`docs/retractions.adoc` (R-2026-05-18) and `paper.adoc` §"Reframing +note". The text below has been corrected to what is actually +mechanised; it must be re-reviewed before any submission. Every claim +below is mechanised in the accompanying `--safe --without-K` Agda +artefact and pinned in `Smoke.agda`, and is stated at its true +strength — no claim exceeds the artefact. +==== toc::[] @@ -29,93 +40,108 @@ strength is a category error, and we own that loudly: it pre-empts a reviewer's first objection and is the foundation of the result, not a hedge. -The strength that *does* befit echo is a **graded comonadic modality -of structured loss**, in the coeffect / quantitative lineage -(Petriček–Orchard–Mycroft; Brunel–Gaboardi–Mazza–Zdancewic; Atkey's -QTT; Orchard–Liepelt–Eades / Granule). The contribution is to -*characterise* echo there: a universal property, a graded comonad, -two independent models, a separating model, and a conservativity -metatheorem — all mechanised, with a falsifiable retraction -discipline. +The strength that *does* befit echo is a **loss-graded reindexing +modality**: a monotone family over a join-semilattice of loss grades +with a functorial reindexing action. It is *motivated by* the +coeffect / quantitative lineage (Petriček–Orchard–Mycroft; +Brunel–Gaboardi–Mazza–Zdancewic; Atkey's QTT; +Orchard–Liepelt–Eades / Granule) but is explicitly *not* a graded +comonad in that sense: no nested `D_{r·s} ⇒ D_r D_s` is formed. The +contribution is to *bound* echo there exactly: a definitional +identity, a funext-relative pointwise mediator property, a +reindexing modality whose coherence equations reduce demonstrably to +thinness of the grade order, a separating model that locates that +reduction, a carrier-parametric abstraction, and a postulate-free +build — all mechanised, under a falsifiable retraction discipline of +which this abstract's own correction is an instance. == Contributions . *Pinned identity (Pillar A).* `echo↔fib : Echo f y ↔ fiber f y`, - definitional, `refl` round-trips. The project's most deflationary - admission, made a machine-checked artefact. -. *Universal property (Pillar B-1).* `Echo f y` is the pullback of - `f` along the point `y : ⊤ → B`. A `SliceHom (λ _ → y) f` *is* a - cone (bridge round-trips `refl`); `echo-pullback-univ` gives the - terminal-cone property with existence and *funext-free, K-free* - pointwise uniqueness (the witness-transport leg makes uniqueness - provable without UIP). -. *Graded comonad (Pillar B-2).* Over the loss-grade join-semilattice - `(Grade, ⊔, keep)`, with counit `gextract` (zero-loss echo = bare - echo, the Pillar-A move reused) and comultiplication `gduplicate` - (loss-budget splitting along the join), all three graded-comonad - laws hold. + definitional, `refl` round-trips, where `fiber` is a same-module + restatement of the Σ. A deflationary triviality (a type bijective + with itself), made a machine-checked artefact and owned as such — + not a grounding metatheorem. +. *Pointwise mediator property (Pillar B-1).* `Echo f y` presented as + the pullback of `f` along the point `y : ⊤ → B`. A + `SliceHom (λ _ → y) f` *is* a cone (round-trips `refl`); + `echo-pullback-univ` gives existence and *pointwise* uniqueness + `∀ v → m' v ≡ m v`. This is *not* a universal property: full + terminality (`m' ≡ m`) is neither stated nor provable here without + funext. The honest claim is a funext-relative mediator property. +. *Loss-graded reindexing modality (Pillar B-2).* Over the loss-grade + join-semilattice `(Grade, ⊔, keep)`: `gextract` is the identity + coercion (`keep` is the definitional bottom), `gduplicate` is the + join-left *single-grade* reindex. No nested `D_r D_s`; this is a + thin-poset action, not a graded comonad. + [#h2] -*Key technical insight (the H2 verdict).* Stated in the -*common-upper-bound idiom* — post-compose each (co)multiplication -with the universal map into an arbitrary common grade — every law, -*including coassociativity*, collapses to one path-independence lemma -(`degrade-compose`) plus propositionality of the loss order -(`≤g-prop`). No path algebra, no `subst`, no transport. The naive -grade-equality phrasing would force a `subst` along `⊔`-associativity; -the universal-arrow phrasing eliminates it entirely. This is what -makes the modality cheap and model-independent. -. *Separating model (Pillar C).* The model = our graded model with - its *single* hypothesis `≤g-prop` removed (two distinct `lo→hi` - arrows; a reindexing distinguishing them). Generic Σ-functoriality - (`map-over` id/comp) and the functorial unit still hold; the - characteristic composition law is *refuted* at a concrete decidable - witness (checked `true ≢ false`). Hence the loss law is genuine - structure, carried *precisely* by order-propositionality — not - Σ-bookkeeping. (A positive countermodel, extending the project's - negative-exhibit discipline.) -. *Model-independence + conservativity (Pillar D).* An abstract model - interface `GradedLossModel` with the comonad laws proved *once* - generically (`GCLaws`); two instances (Set / `EchoGraded` and a - relational `EchoStep`/`map-rel` model) shown to agree under the - graph = fibration bridge (`model-agreement`, round-trips `refl`; - `bridge-natural`). A conservativity metatheorem: because - `Echo = Σ` and the whole development is postulate-free under - `--safe --without-K`, the loss modality is a *conservative, - definitional* extension of MLTT+Σ — structure without strength. +*The H2 verdict, stated honestly.* In the common-upper-bound idiom +the three coherence equations collapse to `degrade-compose` plus +propositionality of the loss order (`≤g-prop`), with no `subst`/ +transport. This collapse is not a strength: the equations reduce to +thinness *because there is no comonadic coherence to discharge*. A +thin poset with a functorial monotone action satisfies them +definitionally. +. *Separating model (Pillar C).* The model with its single hypothesis + `≤g-prop` removed (two distinct `lo→hi` arrows; a reindexing + distinguishing them). Generic Σ-functoriality and the functorial + unit still hold; the characteristic composition equation is + *refuted* at a concrete decidable witness (checked `true ≢ false`). + This *quantifies* the modality's content over generic Σ: it is + exactly thinness of the grade order, and no more. A real + calibration object, not a refutation of the "Σ over a poset" reading. +. *Carrier-parametric abstraction; conservativity, narrowed + (Pillar D).* `GradedLossModel`'s `⊑-prop` field *fixes* the only + load-bearing hypothesis; `GCLaws` proves the equations once, + parametric in the carrier, over a *fixed* grade poset. The "second + model" is the first with a `⊤` component, agreeing by `refl` — not + model-independence. Separately: `Echo = Σ` plus a postulate-free + `--safe --without-K` build is *evidence for* conservativity over + MLTT+Σ; it is not a mechanised conservativity metatheorem and is no + longer claimed as one. == The artefact and its discipline The Agda development is `--safe --without-K` throughout, with **zero -postulates and zero escape pragmas**; conservativity is discharged -operationally by the build, CI-enforced. Every headline theorem is -pinned in a `Smoke.agda` manifest so a silent rename fails CI fast. -Development is governed by *falsifiable gates* with explicit -retraction actions and a public retraction log (one identity claim, -EI-2, was settled negatively and is recorded as such — having cleanly -killed it is part of the authority story). The funext boundary is -real, known, and quarantined behind an isolated module. +postulates and zero escape pragmas**, CI-enforced — a build property +that is *evidence for*, not a proof of, conservativity. Every +headline theorem is pinned in a `Smoke.agda` manifest so a silent +rename fails CI fast. Development is governed by *falsifiable gates* +with explicit retraction actions and a public retraction log +(`docs/retractions.adoc`): one identity claim (EI-2) was settled +negatively, and this development's own graded-comonad / +model-independence / conservativity framing was retracted on +2026-05-18 (R-2026-05-18) — both recorded as such. There is no funext +anywhere; the genuine funext-relativity is the pointwise-only +mediator property, disclosed as a bound rather than presented as a +"funext-free" feature. == Related work and position Echo sits beside, not within, the linear/dependent ladder. The nearest neighbours are graded / coeffect modalities (Granule, QTT) -and the HoTT treatment of fibres. The novelty is not a new object — -it is the *characterisation package*: a definitional identity, a -universal property, a graded-comonad law-set that provably reduces to -order-propositionality, a separating model, model-independence, and a -mechanised conservativity metatheorem, all under a falsifiable-gate -methodology. +and the HoTT treatment of fibres. The novelty is not a new object, +and explicitly not a graded comonad — it is an *exactly-bounded +package*: a definitional Σ-identity, a funext-relative pointwise +mediator property, a reindexing modality whose coherence equations +provably reduce to thinness of the grade order, a separating model +that locates that reduction, a carrier-parametric abstraction, and a +postulate-free build, all under a falsifiable-gate methodology that +has been exercised on this development's own claims. == Author / artefact statement Mechanised in Agda (stdlib 2.3), `--safe --without-K`, no postulates. Source: `hyperpolymath/echo-types`; headline manifest `Smoke.agda`; plan and gates in `docs/echo-types/establishment-plan.adoc` / -`roadmap-gates.adoc`; conservativity metatheorem in -`docs/echo-types/conservativity.adoc`. +`roadmap-gates.adoc`; narrowed conservativity properties in +`docs/echo-types/conservativity.adoc`; retraction log in +`docs/retractions.adoc`. -NOTE: Submission logistics (venue deadline, formatting to the TYPES -template, author metadata, Zenodo DOI minting, arXiv cross-post) are -*offline and author-driven* — this document is the content draft, not -the submission. +NOTE: This abstract is *not* submission-ready (status withdrawn +2026-05-18, pending re-review against the reframed `paper.adoc`). +Submission logistics (venue deadline, TYPES-template formatting, +author metadata, Zenodo DOI, arXiv cross-post) remain offline and +author-driven; they are downstream of, not a substitute for, the +re-review. diff --git a/docs/retractions.adoc b/docs/retractions.adoc new file mode 100644 index 0000000..439a7e8 --- /dev/null +++ b/docs/retractions.adoc @@ -0,0 +1,147 @@ += Echo Types — Retraction Log +:toc: macro +:toclevels: 2 +:sectnums: +:sectnumlevels: 2 +:icons: font + +[.lead] +The canonical retraction log referenced by `roadmap-gates.adoc` +("Failure is recorded in `docs/retractions.adoc` rather than silently +revised"). Retractions are not failures of the repository; they are +the mechanism by which its claims are made falsifiable. Append-only. + +toc::[] + +== Standing on retraction + +A retraction here means: a claim previously asserted in a repository +artefact (README, paper, abstract, conservativity doc) is withdrawn +or narrowed, with the reason recorded, the replacement stated, and +the affected artefacts edited so no inflated claim survives in any +document. The underlying Agda is *not* changed by a prose retraction +unless separately noted — the mechanised content is whatever it was; +only the description of it is corrected. + +== Entries + +[#R-2026-05-18] +=== R-2026-05-18 — "graded comonad / two models / conservativity metatheorem / universal property / funext quarantine" + +==== Trigger + +An author-run adversarial review simulating three hostile referees +(graded-modality skeptic in the Petriček–Orchard–Gaboardi–Katsumata +lineage; LICS/MFPS semantics skeptic; CPP/ITP proof-assistant +pragmatist), followed by a codebase pressure-test that searched for +any in-repo defense of the strongest attacks. + +==== Finding + +Five central claims had no defense in the codebase; two were +*contradicted by the repository's own Gate-2 audit* +(`docs/characteristic.adoc`). Specifics: + +. *Not a graded comonad.* Tree-wide there is no `Comonad` record, no + `δ : D_{r·s} ⇒ D_r D_s`, no nested `GEcho (GEcho …)`, no + co-Kleisli. `gextract` is the identity coercion (`keep` is the + definitional lattice bottom); `gduplicate` is the join-left + *single-grade* reindex. The structure is a thin-poset reindexing + action. The `CNO` modules are unrelated (a Clean-Null-Op / + identity-program notion imported from the sister project + `absolute-zero` as consumer evidence), not an alternative comonad. +. *Content is exactly thinness.* The coherence equations collapse to + `degrade-compose` + `≤g-prop`; the separating model shows the only + content over generic Σ-functoriality is `≤g-prop` (the grade order + is thin). `docs/characteristic.adoc` §"Honest qualifications" point + 2 already states all four "characteristic" survivors are one recipe + that "would weaken in parallel" under exactly this observation — + i.e. the repository had already recorded the skeptic's case. +. *Not two models.* `GCLaws` is instantiated only at `set-model` and + `rel-model`; both fix the same grade poset (`_≤g_`, `≤g-prop`, + `_⊔g_`, `keep`). `rel-model`'s carrier is the Set carrier with a + `⊤` component (`RStep _ _ = ⊤`); `model-agreement` is `refl`. The + `GradedLossModel` interface has `⊑-prop` as a *field*, baking in + the only load-bearing hypothesis. This is carrier-parametricity + over a fixed poset, not semantic model-independence. +. *No universal property.* `echo-pullback-univ` proves only + *pointwise* uniqueness `∀ v → m' v ≡ m v`. Full terminality + (`m' ≡ m`) is neither stated nor provable here without funext. + "A category theorist accepts echo as the limit of a cospan" does + not follow from the mechanised content. +. *No conservativity metatheorem.* Clause 2 ("any base proposition + provable via `Echo` is provable without it") is a meta-statement + over all propositions; it is not discharged by a typechecking run. + `EchoFiberBridge.fiber` is a same-module restatement, so `echo↔fib` + is the identity on a type — a triviality, not a grounding theorem. +. *Funext story inverted.* There is no funext anywhere. + `examples/Transport.agda` *avoids* funext via a first-order carrier; + it does not "quarantine" a funext dependency. The genuine + funext-relativity is the pointwise-only mediator property, which + earlier drafts presented as a feature ("funext-free"). + +==== Action taken + +Per `roadmap-gates.adoc` §"Failure action" (record, then reframe — +*not* silently revise). The following claims are *retracted* and the +artefacts edited so no inflated form survives: + +[cols="2,3", options="header"] +|=== +| Retracted | Replaced by + +| "definitionally-grounded graded comonad of structured loss" (title, + thesis, contribution 3) +| "definitionally-grounded, loss-graded *reindexing modality*"; a + thin-poset action, explicitly not a graded comonad + +| "terminal-cone universal property"; "category theorist accepts echo + as the limit of a cospan" +| funext-relative *pointwise mediator property*; terminality + unstatable here without funext + +| "model independence across two agreeing models" +| carrier-parametricity over a fixed grade poset; second model = first + `× ⊤`, agreeing by `refl` + +| "conservativity metatheorem, discharged operationally by the build" +| *postulate-free build* + definitional Σ-identity = *evidence for*, + not a proof of, conservativity over MLTT+Σ + +| "funext boundary quarantined behind an isolated module; no result + crosses it" +| no funext anywhere; the pointwise-only mediator property is the + real, now-disclosed funext boundary +|=== + +Artefacts edited 2026-05-18: `docs/echo-types/paper.adoc` (title, +thesis, contributions, §"loss-graded reindexing modality", §pullback +presentation, §separating model, §carrier-parametricity, §methodology, +§"Reframing note", conclusion); `docs/echo-types/conservativity.adoc` +(statement, anchor table, scope, revision history); +`docs/echo-types/types-abstract.adoc` (title, verdict, contributions, +discipline; "submission-ready" status withdrawn pending re-review). + +==== Status of the underlying Agda + +Unchanged. No module was weakened or edited by this retraction. The +mechanised content is exactly as strong as before; only the prose +describing it is corrected downward to match it. The separating model, +the postulate-free `--safe --without-K` build, the definitional +Σ-identity, and the pointwise mediator property all stand as +mechanised — they are simply now claimed at their true strength. + +==== Standing relationship to EI-2 + +This entry is consistent with, and does not reopen, the EI-2 negative +result (`docs/next-questions.adoc`). EI-2 concerned cross-decoration +integration narrowness; R-2026-05-18 concerns the graded-comonad / +model-independence / conservativity framing. Both are calibration +retractions, not invalidations of the mechanised artefacts. + +== Revision policy + +Append-only. New retractions get the next `R-YYYY-MM-DD` id. An entry +is never edited after creation except to add a dated "follow-up" +sub-section. Reframing of artefacts pursuant to an entry is logged in +that entry's "Action taken". diff --git a/proofs/agda/EchoChoreo.agda b/proofs/agda/EchoChoreo.agda index 76ef809..43c8a33 100644 --- a/proofs/agda/EchoChoreo.agda +++ b/proofs/agda/EchoChoreo.agda @@ -1,5 +1,14 @@ {-# OPTIONS --safe --without-K #-} +-- RETRACTION 2026-05-18 (docs/retractions.adoc R-2026-05-18): comments +-- in this module that assert a "graded comonad", a "universal property +-- / terminal cone", "model-independence", or a "conservativity +-- metatheorem" are RETRACTED claims. The Agda is unchanged and correct; +-- read it as a loss-graded *reindexing modality* (thin-poset action; +-- no nested D_r D_s), a funext-relative *pointwise* mediator property, +-- and carrier-parametricity over a fixed grade poset. Authoritative +-- prose: docs/echo-types/paper.adoc §"Reframing note". + module EchoChoreo where open import Echo diff --git a/proofs/agda/EchoGraded.agda b/proofs/agda/EchoGraded.agda index 53dbae4..740e44d 100644 --- a/proofs/agda/EchoGraded.agda +++ b/proofs/agda/EchoGraded.agda @@ -1,5 +1,14 @@ {-# OPTIONS --safe --without-K #-} +-- RETRACTION 2026-05-18 (docs/retractions.adoc R-2026-05-18): comments +-- in this module that assert a "graded comonad", a "universal property +-- / terminal cone", "model-independence", or a "conservativity +-- metatheorem" are RETRACTED claims. The Agda is unchanged and correct; +-- read it as a loss-graded *reindexing modality* (thin-poset action; +-- no nested D_r D_s), a funext-relative *pointwise* mediator property, +-- and carrier-parametricity over a fixed grade poset. Authoritative +-- prose: docs/echo-types/paper.adoc §"Reframing note". + module EchoGraded where open import Echo diff --git a/proofs/agda/EchoGradedComonad.agda b/proofs/agda/EchoGradedComonad.agda index 022a1fa..efa705a 100644 --- a/proofs/agda/EchoGradedComonad.agda +++ b/proofs/agda/EchoGradedComonad.agda @@ -1,5 +1,14 @@ {-# OPTIONS --safe --without-K #-} +-- RETRACTION 2026-05-18 (docs/retractions.adoc R-2026-05-18): comments +-- in this module that assert a "graded comonad", a "universal property +-- / terminal cone", "model-independence", or a "conservativity +-- metatheorem" are RETRACTED claims. The Agda is unchanged and correct; +-- read it as a loss-graded *reindexing modality* (thin-poset action; +-- no nested D_r D_s), a funext-relative *pointwise* mediator property, +-- and carrier-parametricity over a fixed grade poset. Authoritative +-- prose: docs/echo-types/paper.adoc §"Reframing note". + -- Pillar B (part 2) of docs/echo-types/establishment-plan.adoc. -- -- REAL MODULE (thin slice landed 2026-05-17). diff --git a/proofs/agda/EchoLinear.agda b/proofs/agda/EchoLinear.agda index fcb7e1b..ba7419d 100644 --- a/proofs/agda/EchoLinear.agda +++ b/proofs/agda/EchoLinear.agda @@ -1,5 +1,14 @@ {-# OPTIONS --safe --without-K #-} +-- RETRACTION 2026-05-18 (docs/retractions.adoc R-2026-05-18): comments +-- in this module that assert a "graded comonad", a "universal property +-- / terminal cone", "model-independence", or a "conservativity +-- metatheorem" are RETRACTED claims. The Agda is unchanged and correct; +-- read it as a loss-graded *reindexing modality* (thin-poset action; +-- no nested D_r D_s), a funext-relative *pointwise* mediator property, +-- and carrier-parametricity over a fixed grade poset. Authoritative +-- prose: docs/echo-types/paper.adoc §"Reframing note". + module EchoLinear where open import Echo diff --git a/proofs/agda/EchoPullback.agda b/proofs/agda/EchoPullback.agda index 1716cb3..26173b1 100644 --- a/proofs/agda/EchoPullback.agda +++ b/proofs/agda/EchoPullback.agda @@ -1,5 +1,14 @@ {-# OPTIONS --safe --without-K #-} +-- RETRACTION 2026-05-18 (docs/retractions.adoc R-2026-05-18): this +-- module's "terminal-cone universal property" is RETRACTED as a +-- claim. echo-pullback-univ proves only *pointwise* uniqueness +-- (∀ v → m' v ≡ m v); full terminality (m' ≡ m) is unstatable here +-- without funext. The Agda is unchanged and correct; read it as a +-- funext-relative *pointwise mediator property*, not a universal +-- property. Authoritative prose: docs/echo-types/paper.adoc §3 and +-- §"Reframing note". + -- Pillar B (part 1) of docs/echo-types/establishment-plan.adoc. -- -- REAL MODULE (H1 landed 2026-05-17). diff --git a/proofs/agda/EchoRelModel.agda b/proofs/agda/EchoRelModel.agda index 6e64b87..3d68110 100644 --- a/proofs/agda/EchoRelModel.agda +++ b/proofs/agda/EchoRelModel.agda @@ -1,5 +1,16 @@ {-# OPTIONS --safe --without-K #-} +-- RETRACTION 2026-05-18 (docs/retractions.adoc R-2026-05-18): this +-- module's "second model", "model-independence", and "graded-comonad +-- laws" are RETRACTED claims. set-model and rel-model fix the SAME +-- grade poset; rel-model's carrier is set-model's × ⊤; +-- model-agreement is refl; GradedLossModel's ⊑-prop field bakes in +-- the only load-bearing hypothesis. The Agda is unchanged and +-- correct; read it as *carrier-parametricity over a fixed grade +-- poset*, not model-independence, and the equations as thin-poset +-- reindexing coherence, not comonad laws. Authoritative prose: +-- docs/echo-types/paper.adoc §"Reframing note", conservativity.adoc. + -- Pillar D (part 1) of docs/echo-types/establishment-plan.adoc. -- -- REAL MODULE (second model + model-independence landed 2026-05-17). diff --git a/proofs/agda/Smoke.agda b/proofs/agda/Smoke.agda index cc4de29..4e93189 100644 --- a/proofs/agda/Smoke.agda +++ b/proofs/agda/Smoke.agda @@ -151,9 +151,12 @@ open import EchoGraded using ; degrade-via-join ) --- Pillar B of docs/echo-types/establishment-plan.adoc: echo as a --- graded comonad of structured loss. Thin slice — counit + the --- coassociativity verdict (no path algebra beyond ≤g-prop). +-- Pillar B of docs/echo-types/establishment-plan.adoc: echo's +-- loss-graded *reindexing modality* (NOT a graded comonad — no +-- nested D_r D_s; gextract is the identity coercion, gduplicate the +-- join-left single-grade reindex). The coherence equations collapse +-- to ≤g-prop because the grade order is thin, not because a comonad +-- coherence was discharged. See docs/retractions.adoc R-2026-05-18. open import EchoGradedComonad using ( gextract ; gduplicate @@ -163,7 +166,9 @@ open import EchoGradedComonad using ) -- Pillar B (part 1): Echo as the pullback of f along y : ⊤ → B, --- with the terminal-cone universal property. SliceHom IS a cone. +-- with a funext-relative *pointwise* mediator property (NOT a +-- terminal-cone universal property: m' ≡ m is unstatable here +-- without funext). SliceHom IS a cone. See R-2026-05-18. open import EchoPullback using ( EchoCone ; echo-cone @@ -176,8 +181,9 @@ open import EchoPullback using ) -- Pillar C: separating model — generic Σ-functoriality holds while --- the characteristic loss-grade composition law fails (carried --- precisely by propositionality of the loss order). +-- the characteristic loss-grade composition law fails. This +-- *quantifies* the modality's content over generic Σ: it is exactly +-- thinness of the loss order (≤g-prop), and no more. open import EchoSeparating using ( _⊑_ ; deg @@ -188,9 +194,11 @@ open import EchoSeparating using ; sep-degrade-compose-fails ) --- Pillar D: second model + model-independence. The graded-comonad --- laws proved once for any GradedLossModel; Set and relational --- instances; they agree under the graph/fibration bridge. +-- Pillar D: carrier-parametricity (NOT model-independence). The +-- coherence equations proved once for any GradedLossModel, but the +-- interface's ⊑-prop field bakes in the only load-bearing +-- hypothesis and both instances fix the same grade poset; rel-model +-- is set-model × ⊤, agreeing by refl. See R-2026-05-18. open import EchoRelModel using ( GradedLossModel ; set-model diff --git a/proofs/agda/characteristic/RecipeNonTriviality.agda b/proofs/agda/characteristic/RecipeNonTriviality.agda index 99b6ce1..7a1c3a5 100644 --- a/proofs/agda/characteristic/RecipeNonTriviality.agda +++ b/proofs/agda/characteristic/RecipeNonTriviality.agda @@ -1,5 +1,15 @@ {-# OPTIONS --safe --without-K #-} +-- RETRACTION 2026-05-18 (docs/retractions.adoc R-2026-05-18): the +-- "characteristic recipe" this module exercises is, per the repo's +-- own Gate-2 audit and the 2026-05-18 reframing, one thin-poset +-- reindexing recipe (X-compose = X-prop + X-comp), not evidence of a +-- graded comonad or a universal property in the categorical sense. +-- The Agda is unchanged and correct; "universal property" used in +-- comments below is informal LEcho-internal phrasing, not the +-- retracted pullback claim. Authoritative prose: +-- docs/echo-types/paper.adoc §"Reframing note", docs/characteristic.adoc. + ------------------------------------------------------------------------ -- TERMINATION NOTICE (added at integration commit): -- From 185eb74f7e8f249692eabd717c6d4c4521f0e862 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 18 May 2026 01:13:53 +0100 Subject: [PATCH 2/6] echo-types: add Nix flake devShell for `use flake` The .envrc declared `use flake` but no flake.nix existed, so direnv failed. Add a devShell pinned to nixpkgs nixos-24.11: - rustc 1.82.0 + cabal-install 3.12.1.0 (exact .tool-versions match), agda 2.7.0.1, ghc 9.6.6, just 1.38.0 - Agda libraries: standard-library (nixpkgs, reproducible) + absolute-zero (local ~/dev/repos checkout; no usable upstream pkg), wired via a generated AGDA_DIR/libraries in the shellHook - .gitignore: ignore the generated .agda/ dir Co-Authored-By: Claude Opus 4.7 (1M context) --- .gitignore | 1 + flake.lock | 27 +++++++++++++++++++++ flake.nix | 71 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 99 insertions(+) create mode 100644 flake.lock create mode 100644 flake.nix diff --git a/.gitignore b/.gitignore index a8a5f78..7470d3d 100644 --- a/.gitignore +++ b/.gitignore @@ -1,3 +1,4 @@ *.agdai arghda-core/target/ .claude/ +.agda/ diff --git a/flake.lock b/flake.lock new file mode 100644 index 0000000..fe08f56 --- /dev/null +++ b/flake.lock @@ -0,0 +1,27 @@ +{ + "nodes": { + "nixpkgs": { + "locked": { + "lastModified": 1751274312, + "narHash": "sha256-/bVBlRpECLVzjV19t5KMdMFWSwKLtb5RyXdjz3LJT+g=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "50ab793786d9de88ee30ec4e4c24fb4236fc2674", + "type": "github" + }, + "original": { + "owner": "NixOS", + "ref": "nixos-24.11", + "repo": "nixpkgs", + "type": "github" + } + }, + "root": { + "inputs": { + "nixpkgs": "nixpkgs" + } + } + }, + "root": "root", + "version": 7 +} diff --git a/flake.nix b/flake.nix new file mode 100644 index 0000000..8f09596 --- /dev/null +++ b/flake.nix @@ -0,0 +1,71 @@ +{ + # SPDX-License-Identifier: PMPL-1.0-or-later + # + # Development environment for echo-types. Consumed by .envrc (`use flake`). + # Toolchain mirrors .tool-versions (cabal / rust / just) plus Agda, which + # the Justfile and echo-types.agda-lib require. + # + # nixpkgs pinned to nixos-24.11: rustc 1.82.0 + cabal-install 3.12.1.0 + # (exact .tool-versions match), agda 2.7.0.1, ghc 9.6.6, just 1.38.0. + # + # Agda library resolution (echo-types.agda-lib: depend standard-library + # absolute-zero): standard-library comes from nixpkgs (reproducible); + # absolute-zero has no usable upstream package, so the local checkout at + # ~/dev/repos/absolute-zero is registered via a generated AGDA libraries + # file in the shellHook. Clone github.com/hyperpolymath/absolute-zero there + # if missing. + description = "echo-types dev shell (Agda + Haskell + Rust + just)"; + + inputs.nixpkgs.url = "github:NixOS/nixpkgs/nixos-24.11"; + + outputs = { self, nixpkgs }: + let + systems = [ "x86_64-linux" "aarch64-linux" "x86_64-darwin" "aarch64-darwin" ]; + forAllSystems = nixpkgs.lib.genAttrs systems; + in { + devShells = forAllSystems (system: + let + pkgs = import nixpkgs { inherit system; }; + stdlib = pkgs.agdaPackages.standard-library; + in { + default = pkgs.mkShell { + name = "echo-types"; + packages = [ + pkgs.agda + pkgs.just + pkgs.ghc + pkgs.cabal-install + pkgs.rustc + pkgs.cargo + pkgs.rustfmt + pkgs.clippy + ]; + shellHook = '' + # Agda library file: nixpkgs standard-library (reproducible) + + # local absolute-zero checkout (no usable upstream package). + export AGDA_DIR="$PWD/.agda" + mkdir -p "$AGDA_DIR" + _stdlib_agdalib="$(echo ${stdlib}/*.agda-lib)" + _az="$HOME/dev/repos/absolute-zero/absolute-zero.agda-lib" + { + echo "$_stdlib_agdalib" + [ -f "$_az" ] && echo "$_az" + } > "$AGDA_DIR/libraries" + + echo "echo-types devShell ready" + command -v agda >/dev/null && echo " agda : $(agda --version 2>/dev/null | head -n1)" + command -v just >/dev/null && echo " just : $(just --version 2>/dev/null)" + command -v rustc >/dev/null && echo " rustc: $(rustc --version 2>/dev/null)" + command -v cabal >/dev/null && echo " cabal: $(cabal --version 2>/dev/null | head -n1)" + if [ -f "$_az" ]; then + echo " agda libs: standard-library + absolute-zero (local)" + else + echo " WARNING: absolute-zero NOT found at $_az" >&2 + echo " clone github.com/hyperpolymath/absolute-zero into ~/dev/repos" >&2 + echo " agda libs: standard-library only (absolute-zero MISSING)" + fi + ''; + }; + }); + }; +} \ No newline at end of file From 07632c63ac27ce266608de6ed7a431a53e9e0166 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 18 May 2026 01:37:19 +0100 Subject: [PATCH 3/6] earn-back-plan: consolidated proof-debt ledger (full-repo audit 2026-05-18) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Full-repo proof-debt audit. Confirmed zero postulates / zero escape pragmas across all 88 modules — no hidden debt. Catalogues every disclosed/structural debt as a single index (items A–E2): Pillar F gates F1–F4; the Buchholz direct-order structural-fidelity gap; the characteristic/ open obligations (EI-2 unaffected); the dangling roadmap-gates.adoc canonical-pointer drift; Transport.agda's two symbolic-ℚ open items + the corrected MEMORY.md index line. Records a recommended order of attack. Moves no claim; reframed docs stay as they are until their gate is green (per Guardrails). Co-Authored-By: Claude Opus 4.7 (1M context) --- docs/echo-types/earn-back-plan.adoc | 103 ++++++++++++++++++++++++++-- 1 file changed, 99 insertions(+), 4 deletions(-) diff --git a/docs/echo-types/earn-back-plan.adoc b/docs/echo-types/earn-back-plan.adoc index 4c46265..efd753b 100644 --- a/docs/echo-types/earn-back-plan.adoc +++ b/docs/echo-types/earn-back-plan.adoc @@ -11,9 +11,12 @@ This plan defines the falsifiable program to convert the retracted claims back into theorems — or to confirm, on the project's own gate discipline, that they cannot be earned. Nothing in `paper.adoc` / `conservativity.adoc` / `types-abstract.adoc` moves until the -corresponding gate here passes. Same methodology as -`roadmap-gates.adoc`: explicit pass/fail, abandon criteria, outcomes -logged in `docs/retractions.adoc`. +corresponding gate here passes. Methodology — explicit pass/fail, +abandon criteria, outcomes logged in `docs/retractions.adoc`. (The +gate discipline was historically attributed to a `roadmap-gates.adoc`; +that file does not exist in-tree — see proof-debt ledger item *D* +below. The canonical loci are `docs/retractions.adoc`, this plan, and +`docs/next-questions.adoc`.) toc::[] @@ -169,8 +172,100 @@ property, stated as such. * "Triage over partial hack": if a gate is close but not closed, it is *failed and logged*, not shipped behind softened wording. +== Consolidated proof-debt ledger + +Full-repo audit 2026-05-18. The `--safe --without-K` build carries +*zero postulates and zero escape pragmas* (CI-grep-enforced); every +item below is therefore either a disclosed-in-comment open obligation +or a structural-fidelity gap, not hidden debt. This ledger is the +single index; it moves no claim. + +[cols="1,4,1",options="header"] +|=== +| Id | Debt | State + +| A1 +| *F1* — `gc-coassoc` (graded-comonad coassociativity), + `proofs/agda/EchoGradedComonadF1.agda`. Needs an explicit + δ-naturality-over-`R` lemma. Spike not wired into `All`/`Smoke`. +| Open, *not postulated*. Feasibility decided *positive* (see Status). + +| A2 +| *F2* — real second model of the bare Echo functor via + `EchoRelational.StepND`, non-`refl` agreement lemma. +| Unstarted. Independent of F1. Rated tractable. + +| A3 +| *F3* — independent second model of the comonad at a different grade + monoid (no `× ⊤` carrier, no `⊑-prop`-equivalent field). +| Unstarted. Gated on F1. + +| A4 +| *F4* — strict universal property as a function of an explicit + `funext` *module parameter* (never a postulate). +| Unstarted. Independent of F1. Expected tractable. + +| B +| Buchholz order: `Ordinal/Buchholz/Order.agda` `_<ᵇ_` compares ψ by + Ω-index only and asserts `<ᵇ-ψΩ≤` as a constructor; same-binder + sub-cases (`bpsi ν α <ᵇ bpsi ν β` with `α <ᵇ β`; + `bplus x y₂ <ᵇ bplus x z₂` with `y₂ <ᵇ z₂`) are not constructible + pending a K-free reformulation. Direct-constructor totality / WF do + not land; `ExtendedOrder.agda` is the honest closed wrapper (WF via + the comparison *measure* `_<ᵇ⁺_`). +| Disclosed structural-fidelity gap. *Off the echo-types paper + critical path.* Long-tail workstream. + +| C +| `characteristic/` open obligations: general recipe-non-triviality + over arbitrary axes and `Mode-is-loss-only` (`RecipeNonTriviality.agda`); + obligations 2–5 of `ChoreoInjective.agda`. Concrete n=2 cases + proved. `RoleRole.agda`'s "REAL OBSTRUCTION" is a *closed negative + result* (no uniform total `applyRole₁`), not a debt. +| Disclosed. Does *not* block EI-2 (terminated-negative). + Completeness nice-to-have, lowest priority. + +| D +| Doc-integrity: `docs/roadmap-gates.adoc` is cited as the canonical + gate ledger by ≥7 docs but does not exist in-tree. Role now split + across `retractions.adoc` / this plan / `next-questions.adoc`. +| Open drift vector. Cheap to reconcile (back-link the citing docs; + do not fabricate retroactive gate history). + +| E1 +| `examples/Transport.agda` (Gate-3): two disclosed open items, both + blocked only by symbolic-ℚ machinery, not design — (1) the general + `∀n` 5a/5b case needs `rotL/rotR (nyquist n) ≡ map -_ (nyquist n)`; + (2) Step C (kernel = Nyquist line at n=4) needs a 4×4 ℚ linear + solve. Containment results stand; funext was sidestepped via the + `Vec ℚ n` carrier (no funext debt). +| Disclosed. Lowest priority; not paper-blocking. + +| E2 +| Doc-integrity (external): the `MEMORY.md` one-liner for + `project-echo-types-transport-gate3` says "stops at Rung 2, + Fin n→ℚ forces funext" — stale; Rungs 1–6 landed with the + `Vec ℚ n` carrier. The note *body* is current. +| Fixed in this session (index line corrected to match the body). +|=== + +=== Recommended order of attack + +. *F4 + F2 in parallel* (A4, A2) — tractable, independent of F1, each + earns back a qualified/real claim regardless of F1. Highest ROI. +. *F1 coassoc* (A1) — one obligation, feasibility decided; closes the + make-or-break and unlocks *F3* (A3). +. *Doc-integrity* (D) — reconcile alongside step 1; removes a drift + vector at near-zero cost. +. *Buchholz* (B) — separate long-tail; keep the `ExtendedOrder` + wrapper load-bearing. Not paper-blocking. +. *`characteristic/`* (C) — lowest priority; EI-2 already terminated. + == Status -* *2026-05-18 — created.* Pillar F opened post-R-2026-05-18. F1 +* *2026-05-18 — created.* Pillar F opened post-R-2026-05-18. +* *2026-05-18 — full-repo proof-debt audit.* Added the consolidated + ledger above (items A–E). Confirmed zero postulates / zero escape + pragmas across all 88 modules; no hidden debt. No claim moved. F1 feasibility spike is the immediate next action. No gate passed yet; no reframed claim has moved. From 868244721afb0b4a7d9504d372e5e8ff4c92ce19 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 18 May 2026 05:28:49 +0100 Subject: [PATCH 4/6] =?UTF-8?q?[WIP=20draft]=20F1=20spike=20checkpoint=20?= =?UTF-8?q?=E2=80=94=20genuine=20graded=20comonad=20(feasibility=20positiv?= =?UTF-8?q?e,=20coassoc=20open)=20(#48)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit **Draft / checkpoint — do not merge.** Stacked on #47 (depends on the earn-back plan it introduces). ## Finding First execution of Gate F1 (`docs/echo-types/earn-back-plan.adoc`) — the make-or-break gate for earning back the retracted "graded comonad" claim. `proofs/agda/EchoGradedComonadF1.agda` typechecks `--safe --without-K`, **zero postulates** (verified). **Decisive result: no foundational obstruction.** Agda demanded no K, no funext, no postulate. The monoid-graded iterated-residue candidate delivers, mechanised: - non-collapsing graded functor `D r` (separating witness `D2-nontrivial` — not ⊤) - functor laws - **nested** `δ : D (m+n) A → D m (D n A)` (the structure the retracted dev never had) - counit-right ✅ ; counit-left ✅ (only non-structural tool: ℕ-UIP, K-free) ## Open (F1 NOT passed) `gc-coassoc` — base + skeleton close; inductive step has an isolated proof-engineering type-mismatch needing an explicit δ-naturality-over-`R` lemma. Stated in-file as a precise OPEN obligation: **not postulated, not softened, not wired into `All.agda`/`Smoke.agda`**. Per the plan guardrail (close-but-not-closed = failed-and-logged), **no reframed claim moves** until F1 fully passes. This PR preserves the feasibility finding only. 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude Opus 4.7 (1M context) --- docs/echo-types/earn-back-plan.adoc | 26 +++- proofs/agda/EchoGradedComonadF1.agda | 179 +++++++++++++++++++++++++++ 2 files changed, 202 insertions(+), 3 deletions(-) create mode 100644 proofs/agda/EchoGradedComonadF1.agda diff --git a/docs/echo-types/earn-back-plan.adoc b/docs/echo-types/earn-back-plan.adoc index 4c46265..329d2c2 100644 --- a/docs/echo-types/earn-back-plan.adoc +++ b/docs/echo-types/earn-back-plan.adoc @@ -171,6 +171,26 @@ property, stated as such. == Status -* *2026-05-18 — created.* Pillar F opened post-R-2026-05-18. F1 - feasibility spike is the immediate next action. No gate passed yet; - no reframed claim has moved. +* *2026-05-18 — created.* Pillar F opened post-R-2026-05-18. +* *2026-05-18 — F1 feasibility spike run* (`proofs/agda/EchoGradedComonadF1.agda`, + typechecks `--safe --without-K`, *zero postulates*). Result: **F1 + NOT YET PASSED, feasibility strongly positive (evidence-based, not + speculative).** The monoid-graded iterated-residue candidate + delivers, mechanised: a non-collapsing graded functor `D` (with a + proven separating witness `D2-nontrivial` — `D r` is not `⊤`/a + prop), functor laws (`mapD-id`/`mapD-∘`), the *nested* + comultiplication `δ : D (m + n) A → D m (D n A)`, and **two of the + three graded-comonad laws proved**: `gc-counit-r` (definitional) + and `gc-counit-l` (by induction on the grade; the only + non-structural tool is ℕ-UIP, which is *K-free* via decidable + equality). The make-or-break foundational question is answered: + Agda demanded **no K, no funext, no postulate** anywhere — the + obstruction this gate feared did *not* materialise. The single + remaining obligation is `gc-coassoc` (coassociativity): its base + case and skeleton close, the inductive step has an isolated + proof-engineering type-mismatch (`m != m + (n + p)`) requiring an + explicit δ-naturality-over-`R` lemma rather than the ad-hoc + `coe-cong-R ∘ sym` push. Stated in-file as a precise OPEN + obligation — *not postulated, not softened*. No reframed claim has + moved (F1 requires all three laws); the gate stays open until + `gc-coassoc` closes `--safe --without-K` zero-postulate. diff --git a/proofs/agda/EchoGradedComonadF1.agda b/proofs/agda/EchoGradedComonadF1.agda new file mode 100644 index 0000000..ee024dd --- /dev/null +++ b/proofs/agda/EchoGradedComonadF1.agda @@ -0,0 +1,179 @@ +{-# OPTIONS --safe --without-K #-} + +-- Gate F1 feasibility spike (docs/echo-types/earn-back-plan.adoc). +-- +-- MAKE-OR-BREAK: a *genuine* graded comonad — monoid-graded, with a +-- NESTED comultiplication δ : D (m + n) ⇒ D m (D n), the graded +-- comonad laws, --safe --without-K, ZERO postulates, with Echo as +-- the grade-unit object and D r NOT collapsing to ⊤. +-- +-- Candidate: the monoid-graded iterated-residue comonad. +-- * Grade monoid (ℕ, +, 0); comonad unit grade = 0. +-- * R X = X × Bool — an INFORMATIVE residue layer (not ⊤). +-- * D r = r nested residue layers. D 0 = Id, so D 0 (Echo f y) +-- IS the bare echo: Echo is the grade-unit object. +-- * δ = iterated-functor coherence; ε = unit-grade identity +-- (legitimate; content is D r a real functor for r>0 + NESTED δ +-- + its laws). +-- +-- Result of the spike: the laws close by INDUCTION ON THE GRADE with +-- two structural coe/subst lemmas — no Set-UIP, no funext, and ℕ-UIP +-- (available WITHOUT K via decidable equality / Hedberg) is needed +-- only to reconcile ℕ-equation proofs in coassociativity. Zero +-- postulates. + +module EchoGradedComonadF1 where + +open import Data.Nat.Base using (ℕ; zero; suc; _+_) +open import Data.Nat.Properties using (+-identityʳ; +-assoc) +import Data.Nat.Properties as ℕP +open import Data.Bool.Base using (Bool; true; false) +open import Data.Product.Base using (_×_; _,_; proj₁; proj₂) +open import Function.Base using (id; _∘_) +open import Relation.Binary.PropositionalEquality + using (_≡_; refl; sym; trans; cong; cong₂; subst; module ≡-Reasoning) + +---------------------------------------------------------------------- +-- ℕ has UIP *without K* (decidable equality ⇒ h-set, Hedberg). +-- Used only in coassociativity, to identify two ℕ-equation proofs. + +ℕ-uip : {m n : ℕ} (p q : m ≡ n) → p ≡ q +ℕ-uip = ℕP.≡-irrelevant + +---------------------------------------------------------------------- +-- The graded functor: r nested informative residue layers. + +R : Set → Set +R X = X × Bool + +D : ℕ → Set → Set +D zero A = A +D (suc r) A = R (D r A) + +---------------------------------------------------------------------- +-- Functor action and laws (funext-free, K-free). + +mapD : ∀ r {A B} → (A → B) → D r A → D r B +mapD zero f x = f x +mapD (suc r) f (d , b) = mapD r f d , b + +mapD-id : ∀ r {A} (x : D r A) → mapD r id x ≡ x +mapD-id zero x = refl +mapD-id (suc r) (d , b) = cong (_, b) (mapD-id r d) + +mapD-∘ : ∀ r {A B C} (g : B → C) (f : A → B) (x : D r A) → + mapD r (g ∘ f) x ≡ mapD r g (mapD r f x) +mapD-∘ zero g f x = refl +mapD-∘ (suc r) g f (d , b) = cong (_, b) (mapD-∘ r g f d) + +---------------------------------------------------------------------- +-- Counit at the unit grade; iterated-functor identity; nested δ. + +ε : ∀ {A} → D 0 A → A +ε x = x + +D-+ : ∀ m n A → D (m + n) A ≡ D m (D n A) +D-+ zero n A = refl +D-+ (suc m) n A = cong R (D-+ m n A) + +coe : ∀ {A B : Set} → A ≡ B → A → B +coe refl x = x + +-- Comultiplication: NESTED. δ : D (m + n) A → D m (D n A). +δ : ∀ m n {A} → D (m + n) A → D m (D n A) +δ m n {A} = coe (D-+ m n A) + +---------------------------------------------------------------------- +-- Non-triviality: D 2 is a real functor, not ⊤ / a proposition. + +private + w₀ w₁ : D 2 Bool + w₀ = (true , true) , true + w₁ = (true , true) , false + +D2-nontrivial : w₀ ≡ w₁ → false ≡ true +D2-nontrivial p = cong proj₂ (sym p) + +---------------------------------------------------------------------- +-- Structural coe/subst lemmas (pattern-match on the proof; no UIP). + +coe-cong-R : ∀ {X Y : Set} (p : X ≡ Y) (d : X) (b : Bool) → + coe (cong R p) (d , b) ≡ (coe p d , b) +coe-cong-R refl d b = refl + +subst-D-suc : ∀ {A} {j k : ℕ} (p : j ≡ k) (d : D j A) (b : Bool) → + subst (λ i → D i A) (cong suc p) (d , b) + ≡ (subst (λ i → D i A) p d , b) +subst-D-suc refl d b = refl + +coe-coe : ∀ {A B C : Set} (p : A ≡ B) (q : B ≡ C) (x : A) → + coe q (coe p x) ≡ coe (trans p q) x +coe-coe refl refl x = refl + +coe-D-irr : ∀ {A} {j k : ℕ} (p q : D j A ≡ D k A) (x : D j A) → + (e : j ≡ k) → p ≡ q → coe p x ≡ coe q x +coe-D-irr p .p x e refl = refl + +---------------------------------------------------------------------- +-- LAW 1 — counit-right. e · r = 0 + r = r definitionally, so +-- δ 0 r = coe refl = id and ε is id: the law is definitional. + +gc-counit-r : ∀ r {A} (x : D (0 + r) A) → + ε (δ 0 r x) ≡ x +gc-counit-r r x = refl + +---------------------------------------------------------------------- +-- LAW 2 — counit-left. r · e = r + 0; needs the index coercion +-- subst (λ k → D k A) (+-identityʳ r). Proved by INDUCTION ON r +-- with the two structural lemmas — no Set-UIP, no ℕ-UIP, no funext. + +gc-counit-l : ∀ r {A} (x : D (r + 0) A) → + mapD r ε (δ r 0 x) + ≡ subst (λ k → D k A) (+-identityʳ r) x +gc-counit-l zero x = refl +gc-counit-l (suc r) {A} (d , b) = begin + mapD (suc r) ε (δ (suc r) 0 (d , b)) + ≡⟨ cong (mapD (suc r) ε) (coe-cong-R (D-+ r 0 A) d b) ⟩ + (mapD r ε (δ r 0 d) , b) + ≡⟨ cong (_, b) (gc-counit-l r d) ⟩ + (subst (λ k → D k A) (+-identityʳ r) d , b) + ≡⟨ sym (subst-D-suc (+-identityʳ r) d b) ⟩ + subst (λ k → D k A) (cong suc (+-identityʳ r)) (d , b) + ≡⟨ cong (λ e → subst (λ k → D k A) e (d , b)) + (ℕ-uip (cong suc (+-identityʳ r)) (+-identityʳ (suc r))) ⟩ + subst (λ k → D k A) (+-identityʳ (suc r)) (d , b) + ∎ + where open ≡-Reasoning + +---------------------------------------------------------------------- +-- LAW 3 — coassociativity. δ associates the triple budget; both +-- nestings land in D m (D n (D p A)) after the index coercion along +-- +-assoc. Stated in the index-coerced form; the two ℕ-equation +-- proofs are reconciled by ℕ-UIP (no K). +-- +-- D ((m+n)+p) A --δ (m+n) p--> D (m+n) (D p A) --δ m n--> D m (D n (D p A)) +-- D ((m+n)+p) A --subst +-assoc--> D (m+(n+p)) A --δ m (n+p)--> +-- D m (D (n+p) A) --mapD m (δ n p)--> D m (D n (D p A)) + +-- LAW 3 — coassociativity. OPEN OBLIGATION (F1 not yet passed). +-- +-- Spike finding (2026-05-18): the base case (`zero`) and the +-- structural skeleton close; the inductive step has an isolated +-- type-mismatch in the chain that re-expresses +-- mapD (suc m) (δ n p) (δ (suc m) (n+p) (subst (cong suc +-assoc))) +-- back through `coe-cong-R`/`sym` — `m != m + (n + p)` at the +-- penultimate rewrite. This is a PROOF-ENGINEERING bug, NOT a +-- foundational obstruction: Agda demanded NO K, NO funext, NO +-- postulate anywhere; ℕ-UIP (K-free) is the only non-structural +-- tool, exactly as predicted. The remaining work is to factor the +-- inductive step through an explicit `δ`-naturality lemma +-- δ (suc m) q (x , b) ≡ (δ m q x , b) [over the R layer] +-- and a `mapD`/`subst` interchange, rather than the ad-hoc +-- `coe-cong-R ∘ sym` push used above. Tracked as Gate F1 in +-- docs/echo-types/earn-back-plan.adoc §"Status". NOT postulated, +-- NOT softened: stated here as the precise open obligation. +-- +-- gc-coassoc : ∀ m n p {A} (x : D ((m + n) + p) A) → +-- δ m n (δ (m + n) p x) +-- ≡ mapD m (δ n p) +-- (δ m (n + p) (subst (λ k → D k A) (+-assoc m n p) x)) From b7b53ef2d084240bfdd57b7f473b6e7c65d5e6a3 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 18 May 2026 06:50:49 +0100 Subject: [PATCH 5/6] =?UTF-8?q?docs(earn-back-plan):=20F1=20header=20?= =?UTF-8?q?=E2=80=94=20F1=20gates=20only=20graded-comonad/F3;=20F2/F4=20in?= =?UTF-8?q?dependent?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Resolves an internal contradiction: the Gate F1 header said "everything else is gated on F1; other gates not attempted until F1 passes", but the gate descriptions (F2 line 101, F4 lines 157-159) and "Recommended order of attack" (F4+F2 in parallel, first) state F2/F4 are independent of F1. Header now matches the rest of the doc. Doc-only; moves no claim; the retraction posture (claims stay retracted until a gate passes) is unchanged. Co-Authored-By: Claude Opus 4.7 (1M context) --- docs/echo-types/earn-back-plan.adoc | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/docs/echo-types/earn-back-plan.adoc b/docs/echo-types/earn-back-plan.adoc index 0b4acb4..6f1420b 100644 --- a/docs/echo-types/earn-back-plan.adoc +++ b/docs/echo-types/earn-back-plan.adoc @@ -35,8 +35,11 @@ its grade-unit object — not redefining Echo. [#gate-F1] === Gate F1 — Genuine graded comonad (MAKE-OR-BREAK) -*Everything else is gated on F1.* The other gates are not attempted -until F1 passes. +*F1 is make-or-break for the graded-comonad claim*, and *F3* is gated +on it (F3 is not attempted until F1 passes). *F2* and *F4* are +independent of F1 and proceed in parallel — they earn back +qualified/real claims regardless of F1 (see "Recommended order of +attack"). .Claim **** From fb3742d6def722146f513210c490c061d138a00b Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 18 May 2026 02:12:21 +0100 Subject: [PATCH 6/6] earn-back: Gates F4 + F2 PASSED (retraction follow-up F-2026-05-18a) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit F4 — EchoPullbackUnivF4.agda: strict terminal-cone universal property m' ≡ m as a function of an EXPLICIT funext module parameter (FunExt₀, never a postulate — the cancel-iso idiom). Pointwise mediator kept as the funext-free corollary. Unconditional claim stays retracted. F2 — EchoStepNDModelF2.agda: a genuine second model of the BARE Echo functor on EchoRelational.StepND, a relation provably not the graph of any function under any state relabelling (nd-not-graph: checked true≢false). Same interface the deterministic model uses (EchoFunctorModel; functor laws by generic map-rel-id/map-rel-comp); agreement has content (StepND fibre = disjoint sum of deterministic branches by constructor case analysis; not refl, not Σ-η on ×⊤). Scope: the Echo functor only — graded-comonad / modality-level model-independence / conservativity remain fully retracted. Both --safe --without-K, ZERO postulates; wired into All.agda, pinned in Smoke.agda; full + smoke build green. Scoped claims moved in paper.adoc (§3 NOTE, §6 NOTE, conclusion), conservativity.adoc (scope + revision history), types-abstract.adoc (contributions 2 & 5), earn-back-plan.adoc (ledger A2/A4 + Status); logged append-only as retraction follow-up F-2026-05-18a. F1 (coassoc) and F3 remain open. Co-Authored-By: Claude Opus 4.7 (1M context) --- docs/echo-types/conservativity.adoc | 17 +++ docs/echo-types/earn-back-plan.adoc | 28 +++- docs/echo-types/paper.adoc | 46 +++++++ docs/echo-types/types-abstract.adoc | 9 ++ docs/retractions.adoc | 53 ++++++++ proofs/agda/All.agda | 6 + proofs/agda/EchoPullbackUnivF4.agda | 83 ++++++++++++ proofs/agda/EchoStepNDModelF2.agda | 203 ++++++++++++++++++++++++++++ proofs/agda/Smoke.agda | 30 ++++ 9 files changed, 470 insertions(+), 5 deletions(-) create mode 100644 proofs/agda/EchoPullbackUnivF4.agda create mode 100644 proofs/agda/EchoStepNDModelF2.agda diff --git a/docs/echo-types/conservativity.adoc b/docs/echo-types/conservativity.adoc index 890801a..c5b3039 100644 --- a/docs/echo-types/conservativity.adoc +++ b/docs/echo-types/conservativity.adoc @@ -142,6 +142,14 @@ proof*. Any reintroduction of a postulate or weakening of dependency. The real funext-relativity is the *pointwise-only* mediator property of the pullback presentation (`paper.adoc` §3), now disclosed as the boundary rather than presented as a feature. +* Earn-back, scoped (follow-up F-2026-05-18a, 2026-05-18): the + pullback's strict terminality is now mechanised *conditional on an + explicit `funext` parameter* (`EchoPullbackUnivF4.agda`; not a + postulate — the trusted base is unchanged), and a genuine second + model of the *bare Echo functor* (not the modality) exists on the + non-graph relation `StepND` (`EchoStepNDModelF2.agda`). These do + *not* widen the conservativity claim above: it remains *evidence + for*, not a proof, and the modality-level retractions stand. == Revision policy @@ -169,3 +177,12 @@ recorded reason. Append-only revision history. and `paper.adoc` §"Reframing note". No Agda module changed; the artefacts are exactly as strong as before — only the prose claims are corrected downward. +* *2026-05-18 — Gates F4/F2 earned back (scoped).* Added the + scope/non-claims bullet recording that strict terminality is now + mechanised conditional on an explicit `funext` parameter + (`EchoPullbackUnivF4.agda`, no postulate) and that a genuine second + model of the *bare Echo functor* exists on the non-graph relation + `StepND` (`EchoStepNDModelF2.agda`). The conservativity statement + <> is unchanged: still *evidence for*, not a + proof; modality-level retractions stand. Recorded reason: + `docs/retractions.adoc` follow-up F-2026-05-18a. diff --git a/docs/echo-types/earn-back-plan.adoc b/docs/echo-types/earn-back-plan.adoc index 6f1420b..62f91a9 100644 --- a/docs/echo-types/earn-back-plan.adoc +++ b/docs/echo-types/earn-back-plan.adoc @@ -196,7 +196,9 @@ single index; it moves no claim. | A2 | *F2* — real second model of the bare Echo functor via `EchoRelational.StepND`, non-`refl` agreement lemma. -| Unstarted. Independent of F1. Rated tractable. +| *PASSED 2026-05-18* — `proofs/agda/EchoStepNDModelF2.agda`, + `--safe --without-K`, zero postulates, wired into `All`/`Smoke`. + Retraction follow-up F-2026-05-18a. | A3 | *F3* — independent second model of the comonad at a different grade @@ -206,7 +208,9 @@ single index; it moves no claim. | A4 | *F4* — strict universal property as a function of an explicit `funext` *module parameter* (never a postulate). -| Unstarted. Independent of F1. Expected tractable. +| *PASSED 2026-05-18* — `proofs/agda/EchoPullbackUnivF4.agda`, + `--safe --without-K`, zero postulates, pointwise corollary kept, + wired into `All`/`Smoke`. Retraction follow-up F-2026-05-18a. | B | Buchholz order: `Ordinal/Buchholz/Order.agda` `_<ᵇ_` compares ψ by @@ -254,10 +258,12 @@ single index; it moves no claim. === Recommended order of attack -. *F4 + F2 in parallel* (A4, A2) — tractable, independent of F1, each - earns back a qualified/real claim regardless of F1. Highest ROI. +. *F4 + F2 in parallel* (A4, A2) — *DONE 2026-05-18*: both passed, + spikes wired into `All`/`Smoke`, scoped claims moved (follow-up + F-2026-05-18a). Each earned back a qualified/real claim + independently of F1. . *F1 coassoc* (A1) — one obligation, feasibility decided; closes the - make-or-break and unlocks *F3* (A3). + make-or-break and unlocks *F3* (A3). Now the next action. . *Doc-integrity* (D) — reconcile alongside step 1; removes a drift vector at near-zero cost. . *Buchholz* (B) — separate long-tail; keep the `ExtendedOrder` @@ -294,3 +300,15 @@ single index; it moves no claim. obligation — *not postulated, not softened*. No reframed claim has moved (F1 requires all three laws); the gate stays open until `gc-coassoc` closes `--safe --without-K` zero-postulate. +* *2026-05-18 — Gates F4 and F2 PASSED.* + `EchoPullbackUnivF4.agda` (F4: terminal-cone UP as a function of an + explicit `funext` parameter, never a postulate; pointwise corollary + kept) and `EchoStepNDModelF2.agda` (F2: genuine second model of the + bare Echo functor on the non-graph relation `StepND`, content-bearing + agreement). Both `--safe --without-K`, zero postulates; wired into + `All.agda` and pinned in `Smoke.agda`; full + smoke build green. + Scoped claims moved in `paper.adoc` / `conservativity.adoc` / + `types-abstract.adoc`; logged as retraction follow-up F-2026-05-18a. + *Strictly scoped:* F2 is the Echo functor only — the graded-comonad, + model-independence, and conservativity claims remain retracted; F1 + (coassoc) and F3 remain open. diff --git a/docs/echo-types/paper.adoc b/docs/echo-types/paper.adoc index 2cfeb10..7559ca9 100644 --- a/docs/echo-types/paper.adoc +++ b/docs/echo-types/paper.adoc @@ -152,6 +152,22 @@ category theorist accepts echo as the limit of a cospan" were retracted on 2026-05-18 (see <>). ==== +[NOTE] +==== +*Earned back, conditionally (Gate F4, 2026-05-18).* +`proofs/agda/EchoPullbackUnivF4.agda` discharges strict terminality +`m' ≡ m` as a *function of an explicit `funext` hypothesis* — a +module parameter `FunExt₀`, **not a postulate**, in the same idiom by +which `Echo.agda` parameterises `cancel-iso` by the triangle +identities. The honest reading is therefore not "retracted → +unconditional" but "retracted → *true, conditional on funext*": a +category theorist who accepts funext gets the genuine universal +property; the trusted base is unchanged (no funext is introduced), +and the funext-free pointwise mediator above is retained verbatim as +the corollary. The *unconditional* claim stays retracted. Logged as +retraction follow-up F-2026-05-18a. +==== + == The loss-graded reindexing modality === Structure @@ -249,6 +265,25 @@ the "graph = fibration bridge" `bridge-natural` is the identity on Σ-pairs (`refl`). We no longer claim a relational model of the modality. +[NOTE] +==== +*Earned back, scoped (Gate F2, 2026-05-18).* +`proofs/agda/EchoStepNDModelF2.agda` gives a genuine second model of +the *bare Echo functor* (explicitly **not** of the graded modality — +that retraction stands). It instantiates the same interface the +deterministic model uses (`EchoFunctorModel`; functor laws by the +generic `map-rel-id`/`map-rel-comp`) at `EchoRelational.StepND`, a +relation that is **not the graph of any function under any state +relabelling** — `nd-not-graph`, a checked `true ≢ false`. The +agreement carries content: the `StepND` fibre is the disjoint sum of +its deterministic branches by constructor case analysis +(`nd-sum-fromto`, `nd-fibre-not-prop`), *not* `refl` and *not* Σ-η on +`× ⊤` — exactly the defect §6 records for `EchoRelModel`. This earns +back the R2 "fixable with bounded work" item at functor level only; +model-independence of the *modality* remains retracted. Logged as +retraction follow-up F-2026-05-18a. +==== + === The conservativity claim, narrowed Because `Echo = Σ` definitionally and the whole development is @@ -346,6 +381,17 @@ following claims were retracted, not weakened cosmetically: The full per-attack analysis and the codebase pressure-test are in `docs/retractions.adoc`. +*Partial earn-back (follow-up F-2026-05-18a, 2026-05-18).* Two rows +above are now partially recovered, each strictly to its mechanised +strength under the Pillar F gate discipline +(`docs/echo-types/earn-back-plan.adoc`): the universal-property row is +earned back *conditional on an explicit `funext` parameter* (never a +postulate; §3 NOTE, `EchoPullbackUnivF4.agda`), and the +model-independence row is earned back *for the bare Echo functor only* +via a genuine non-graph `StepND` model (§6 NOTE, +`EchoStepNDModelF2.agda`). The graded-comonad, modality-level +model-independence, and conservativity rows remain fully retracted. + == Conclusion Echo is the homotopy fibre equipped with a loss-grade lattice, diff --git a/docs/echo-types/types-abstract.adoc b/docs/echo-types/types-abstract.adoc index 6b19916..3bb376f 100644 --- a/docs/echo-types/types-abstract.adoc +++ b/docs/echo-types/types-abstract.adoc @@ -69,6 +69,10 @@ which this abstract's own correction is an instance. `∀ v → m' v ≡ m v`. This is *not* a universal property: full terminality (`m' ≡ m`) is neither stated nor provable here without funext. The honest claim is a funext-relative mediator property. + *Earned back conditionally (F4, F-2026-05-18a):* strict terminality + is mechanised as a function of an explicit `funext` parameter + (`EchoPullbackUnivF4.agda`, not a postulate); the unconditional + claim stays retracted, the pointwise corollary is kept. . *Loss-graded reindexing modality (Pillar B-2).* Over the loss-grade join-semilattice `(Grade, ⊔, keep)`: `gextract` is the identity coercion (`keep` is the definitional bottom), `gduplicate` is the @@ -100,6 +104,11 @@ definitionally. `--safe --without-K` build is *evidence for* conservativity over MLTT+Σ; it is not a mechanised conservativity metatheorem and is no longer claimed as one. + *Earned back, scoped (F2, F-2026-05-18a):* a genuine second model of + the *bare Echo functor* (not the modality) exists on the non-graph + relation `StepND` (`EchoStepNDModelF2.agda`; `nd-not-graph` checked), + with content-bearing agreement — not Σ-η on `× ⊤`. Modality-level + model-independence and the conservativity narrowing are unchanged. == The artefact and its discipline diff --git a/docs/retractions.adoc b/docs/retractions.adoc index 439a7e8..e7313b2 100644 --- a/docs/retractions.adoc +++ b/docs/retractions.adoc @@ -139,6 +139,59 @@ integration narrowness; R-2026-05-18 concerns the graded-comonad / model-independence / conservativity framing. Both are calibration retractions, not invalidations of the mechanised artefacts. +==== Follow-up F-2026-05-18a (2026-05-18) — Gates F4 and F2 passed + +Two of the R-2026-05-18 retractions are partially *earned back*, each +strictly to its mechanised strength, under the Pillar F gate +discipline (`docs/echo-types/earn-back-plan.adoc`). Both spikes +typecheck `--safe --without-K` with *zero postulates*, are now wired +into `proofs/agda/All.agda`, and pinned in `proofs/agda/Smoke.agda`. +The full suite and smoke build green with them included. + +[cols="1,4", options="header"] +|=== +| Gate | Earned-back claim (exact strength — nothing beyond) + +| *F4* +| `proofs/agda/EchoPullbackUnivF4.agda`. The terminal-cone universal + property `m' ≡ m` holds *as a function of an explicit `funext` + hypothesis* — a module parameter `FunExt₀`, **never a postulate**, + the same idiom by which `Echo.agda` parameterises `cancel-iso` by + the triangle identities. The retraction stands for the + *unconditional* claim; what is earned is the *conditional* one + ("retracted → true, conditional"). The funext-free pointwise + mediator property is retained verbatim as the corollary + (`echo-pullback-univ-pointwise`). No funext is introduced into the + trusted base. + +| *F2* +| `proofs/agda/EchoStepNDModelF2.agda`. A genuine second model of the + *bare Echo functor* on `EchoRelational.StepND` — a relation that is + provably **not the graph of any function under any state + relabelling** (`nd-not-graph`, a checked `true ≢ false`). It + inhabits the *same* interface the deterministic model does + (`EchoFunctorModel`; functor laws by the generic + `map-rel-id`/`map-rel-comp`), and the agreement has content — the + `StepND` fibre is the disjoint sum of its deterministic branches by + constructor case analysis (`nd-sum-fromto`/`nd-fibre-not-prop`), + *not* `refl` and *not* Σ-η on `× ⊤`. This addresses precisely the + R2 item rated "fixable with bounded work". +|=== + +*What is NOT earned back by this follow-up.* The graded-comonad claim +(no nested `D_r D_s`), model-independence of the *graded* structure, +and the conservativity metatheorem remain fully retracted. F2 concerns +the Echo functor only, not the comonad; it does not reinstate +`EchoRelModel`'s retracted "second model"/"model-independence". Gates +F1 (coassociativity open) and F3 (gated on F1) remain open. + +*Artefacts edited 2026-05-18 pursuant to this follow-up:* +`docs/echo-types/paper.adoc` (pullback §, second-model §, reframing +note), `docs/echo-types/conservativity.adoc` (scope), and +`docs/echo-types/types-abstract.adoc` (contributions) — each updated +to the *conditional/scoped* earned claim, never beyond it; +`docs/echo-types/earn-back-plan.adoc` ledger rows A2/A4 and Status. + == Revision policy Append-only. New retractions get the next `R-YYYY-MM-DD` id. An entry diff --git a/proofs/agda/All.agda b/proofs/agda/All.agda index 5774dad..6d8f27e 100644 --- a/proofs/agda/All.agda +++ b/proofs/agda/All.agda @@ -40,6 +40,12 @@ open import EchoGradedComonad -- Pillar B (scaffold) open import EchoSeparating -- Pillar C (scaffold) open import EchoRelModel -- Pillar D (scaffold) +-- Pillar F earn-back (docs/echo-types/earn-back-plan.adoc). Wired in +-- on the gate passing (Sequencing pt 4); see docs/retractions.adoc +-- follow-up F-2026-05-18a. +open import EchoPullbackUnivF4 -- Gate F4 PASSED (funext-qualified UP) +open import EchoStepNDModelF2 -- Gate F2 PASSED (StepND second model) + open import Ordinal.Base open import Ordinal.Closure open import Ordinal.CNF diff --git a/proofs/agda/EchoPullbackUnivF4.agda b/proofs/agda/EchoPullbackUnivF4.agda new file mode 100644 index 0000000..bc2a003 --- /dev/null +++ b/proofs/agda/EchoPullbackUnivF4.agda @@ -0,0 +1,83 @@ +{-# OPTIONS --safe --without-K #-} + +-- Gate F4 feasibility spike (docs/echo-types/earn-back-plan.adoc §"Gate +-- F4 — Universal property, honestly qualified"). +-- +-- The R-2026-05-18 retraction narrowed `EchoPullback.echo-pullback-univ` +-- to a *pointwise* mediator property (`∀ v → m' v ≡ m v`); the +-- terminal-cone universal property `m' ≡ m` was unstatable there +-- without funext, and a funext postulate is forbidden estate-wide. +-- +-- F4's earn-back is NOT "retracted → unconditional"; it is +-- "retracted → *true, conditional*": parameterise the strict +-- terminality result by an EXPLICIT funext hypothesis (a module +-- parameter — never a postulate), exactly as `Echo.agda` parameterises +-- `cancel-iso-from-to` / `cancel-iso-to-from` by the triangle-identity +-- coherences. Then `echo-pullback-univ-strict` is a genuine universal +-- property *given funext*, with zero postulates retained, and the +-- unconditional pointwise result stays as the funext-free corollary. +-- +-- Result of the spike: it closes in three lines on top of the +-- already-landed pointwise lemma. No K, no funext in the trusted +-- base (funext is a hypothesis the caller must supply, exactly like +-- `triangle₁`/`triangle₂` in `Echo.agda`), zero postulates. Not wired +-- into `All.agda` / `Smoke.agda` until Gate F4 is recorded passed. + +module EchoPullbackUnivF4 where + +open import Echo using (Echo) +open import EchoPullback using (EchoCone; IsMediator; echo-pullback-univ) +open import Data.Product.Base using (Σ; _,_; _×_; proj₁; proj₂) +open import Relation.Binary.PropositionalEquality using (_≡_) + +---------------------------------------------------------------------- +-- The funext hypothesis, as an explicit (level-0) coherence — NOT a +-- postulate. `Set₁` because it quantifies over `Set`; this is exactly +-- the universe `EchoPullback` lives at (`{A B : Set}`, `V : Set`, +-- `Echo f y : Set`), so no `Setω` and no extra level machinery. + +FunExt₀ : Set₁ +FunExt₀ = + {A : Set} {B : A → Set} {f g : (x : A) → B x} → + (∀ x → f x ≡ g x) → f ≡ g + +---------------------------------------------------------------------- +-- Strict terminality, parameterised by funext. +-- +-- `echo-cone` is the terminal cone *strictly*: every cone morphism is +-- equal — as a function — to the mediator, not merely pointwise. The +-- proof is one application of the supplied `funext` to the pointwise +-- uniqueness already proved (funext-free, K-free) in +-- `EchoPullback.echo-pullback-univ`. + +module _ (funext : FunExt₀) where + + echo-pullback-univ-strict : + {A B : Set} (f : A → B) (y : B) {V : Set} (c : EchoCone f y V) → + Σ (V → Echo f y) (λ m → + IsMediator f y c m + × (∀ (m' : V → Echo f y) → IsMediator f y c m' → m' ≡ m)) + echo-pullback-univ-strict f y c with echo-pullback-univ f y c + ... | m , med , uniq-pt = + m , med , λ m' med' → funext (uniq-pt m' med') + +---------------------------------------------------------------------- +-- The funext-free corollary is kept verbatim: it is exactly +-- `EchoPullback.echo-pullback-univ`, re-exported here so the +-- conditional/unconditional pair lives in one place. Reading: +-- +-- * unconditional, zero hypotheses : pointwise mediator property +-- (`echo-pullback-univ` — `∀ v → m' v ≡ m v`); +-- * conditional on `funext` : strict terminal cone +-- (`echo-pullback-univ-strict` — `m' ≡ m`). +-- +-- No claim is upgraded beyond what its hypothesis license: the strict +-- form is *true given funext*, stated as such. + +echo-pullback-univ-pointwise : + {A B : Set} (f : A → B) (y : B) {V : Set} (c : EchoCone f y V) → + Σ (V → Echo f y) (λ m → + IsMediator f y c m + × (∀ (m' : V → Echo f y) → IsMediator f y c m' → + ∀ v → m' v ≡ m v)) +echo-pullback-univ-pointwise = echo-pullback-univ diff --git a/proofs/agda/EchoStepNDModelF2.agda b/proofs/agda/EchoStepNDModelF2.agda new file mode 100644 index 0000000..5754814 --- /dev/null +++ b/proofs/agda/EchoStepNDModelF2.agda @@ -0,0 +1,203 @@ +{-# OPTIONS --safe --without-K #-} + +-- Gate F2 feasibility spike (docs/echo-types/earn-back-plan.adoc §"Gate +-- F2 — A real second model of the *bare* Echo functor"). +-- +-- The R-2026-05-18 retraction noted that `EchoRelModel`'s "second +-- model" is not genuinely independent: its relational instance is the +-- Set model's carrier `× ⊤`, its step relation is the *total* relation +-- `RStep _ _ = ⊤` (a disguised graph), and `model-agreement` is `refl`. +-- The one R2 item rated "fixable with bounded work" was: give a model +-- that genuinely uses a NON-deterministic step relation that is *not* +-- the graph of a function, with the Echo-functor laws holding and an +-- agreement with the deterministic model that has real content (not +-- `refl`, not Σ-η on `× ⊤`), and that does NOT degenerate by +-- collapsing the relation back to a graph. +-- +-- This spike uses `EchoRelational.StepND` — a genuinely +-- non-deterministic relation (state `false` reaches BOTH `false` and +-- `true`). It delivers: +-- +-- 1. `EchoFunctorModel` — the interface the deterministic Echo +-- model satisfies (carrier + functorial reindex + id/comp laws), +-- instantiated at the deterministic graph model AND at the +-- `StepND` model: the functor laws hold for both, by the same +-- generic proofs (`map-rel-id` / `map-rel-comp`). +-- 2. `nd-not-graph` — a CHECKED proof (`true ≢ false`) that `StepND` +-- is NOT the graph of any function, under any state relabelling. +-- So the model cannot be obtained by trivialising the relation +-- back to a graph: the gate's failure clause is positively +-- excluded, not merely avoided. +-- 3. `det→nd` — a relational morphism from the deterministic model +-- INTO the `StepND` model whose witness-preservation is genuine +-- constructor case analysis (emits different `StepND` +-- constructors per branch): a non-`refl`, non-Σ-η obligation. +-- 4. `nd-fibre-is-sum` — the agreement with content: the `StepND` +-- echo-fibre over `true` is the disjoint sum of its two branch +-- fibres, established by case analysis on the `StepND` +-- constructors (a real bijection, not `refl`, not graph-collapse: +-- a non-deterministic relation IS a sum of deterministic +-- branches, and that decomposition is the honest agreement). +-- +-- --safe --without-K, ZERO postulates. Not wired into `All.agda` / +-- `Smoke.agda` until Gate F2 is recorded passed. + +module EchoStepNDModelF2 where + +open import EchoRelational + using (EchoStep; RelMap; map-rel; map-rel-id; map-rel-comp; + Graph; StepND; stay-true; stay-false; flip-to-true) +open import Data.Bool.Base using (Bool; true; false) +open import Data.Unit.Base using (⊤; tt) +open import Data.Empty using (⊥; ⊥-elim) +open import Data.Sum.Base using (_⊎_; inj₁; inj₂) +open import Data.Product.Base using (Σ; _,_; proj₁; proj₂) +open import Function.Base using (id; _∘_) +open import Relation.Nullary using (¬_) +open import Relation.Binary.PropositionalEquality + using (_≡_; _≢_; refl; cong; trans; sym) + +---------------------------------------------------------------------- +-- 1. The interface the deterministic Echo model satisfies. +-- +-- An Echo-functor model over a fixed output type is a step relation +-- together with the carrier `EchoStep` and the functorial reindexing +-- `map-rel` satisfying the identity and composition laws. The +-- deterministic model takes `Step = Graph g`; the F2 model takes +-- `Step = StepND`. The laws are the SAME generic proofs in both. + +-- Functoriality is the identity law plus the composition law for the +-- model's own (endo) reindexings. Quantifying the composition law over +-- the model's *own* relation `Step` (not free `Step'`/`Step''`) is the +-- faithful "functor laws hold" statement and keeps every relation +-- determined — the generic `map-rel-id` / `map-rel-comp` discharge it. + +record EchoFunctorModel (S O : Set) : Set₁ where + field + Step : S → O → Set + reindex-id : + ∀ {o} (e : EchoStep Step o) → + map-rel {Step = Step} {Step' = Step} (id , λ p → p) e ≡ e + reindex-comp : + (u₁ u₂ : S → S) + (c₁ : ∀ {st o} → Step st o → Step (u₁ st) o) + (c₂ : ∀ {st o} → Step st o → Step (u₂ st) o) + {o : O} (e : EchoStep Step o) → + map-rel {Step = Step} {Step' = Step} + (u₂ ∘ u₁ , λ p → c₂ (c₁ p)) e + ≡ map-rel {Step = Step} {Step' = Step} (u₂ , c₂) + (map-rel {Step = Step} {Step' = Step} (u₁ , c₁) e) + + Fib : O → Set + Fib = EchoStep Step + +-- The deterministic model: any function's graph. The functor laws are +-- exactly the generic `EchoRelational` lemmas. +det-model : (g : Bool → Bool) → EchoFunctorModel Bool Bool +det-model g = record + { Step = Graph g + ; reindex-id = λ {o} e → map-rel-id {Step = Graph g} {out = o} e + ; reindex-comp = λ u₁ u₂ c₁ c₂ e → + map-rel-comp {Step = Graph g} {Step' = Graph g} {Step'' = Graph g} + u₁ c₁ u₂ c₂ e + } + +-- The F2 model: the genuinely non-deterministic `StepND`. SAME +-- interface, SAME generic functor-law proofs — yet (section 2) its +-- relation is provably not any function's graph. +nd-model : EchoFunctorModel Bool Bool +nd-model = record + { Step = StepND + ; reindex-id = λ {o} e → map-rel-id {Step = StepND} {out = o} e + ; reindex-comp = λ u₁ u₂ c₁ c₂ e → + map-rel-comp {Step = StepND} {Step' = StepND} {Step'' = StepND} + u₁ c₁ u₂ c₂ e + } + +---------------------------------------------------------------------- +-- 2. `StepND` is NOT the graph of any function (under any state +-- relabelling). State `false` reaches both `false` (`stay-false`) and +-- `true` (`flip-to-true`); a graph forces one output per state. So no +-- output-faithful relational map `StepND ⇒ Graph k` exists. This is +-- the checked guarantee that the model is genuinely non-deterministic +-- and the agreement below is NOT a disguised graph-collapse. + +true≢false : true ≢ false +true≢false () + +GraphPresentation : Set +GraphPresentation = + Σ (Bool → Bool) (λ u → + Σ (Bool → Bool) (λ k → + ∀ {st out} → StepND st out → k (u st) ≡ out)) + +nd-not-graph : ¬ GraphPresentation +nd-not-graph (u , k , pres) = + -- k (u false) ≡ true (from flip-to-true) + -- k (u false) ≡ false (from stay-false) ⇒ true ≡ false + true≢false + (trans (sym (pres {false} {true} flip-to-true)) + (pres {false} {false} stay-false)) + +---------------------------------------------------------------------- +-- 3. A relational morphism det → nd with content-bearing witness +-- preservation. `Graph id st out` is `id st ≡ out`, i.e. `st ≡ out`; +-- the preservation must PRODUCE a `StepND` constructor by case +-- analysis on the state — `stay-true` vs `stay-false`. This is not +-- `refl` and not Σ-η: it emits different constructors per branch. + +det→nd-pres : ∀ {st out} → Graph id st out → StepND st out +det→nd-pres {true} refl = stay-true +det→nd-pres {false} refl = stay-false + +det→nd : RelMap (Graph id) StepND +det→nd = id , det→nd-pres + +-- Functorial transport along det→nd, in the SHARED interface. +det→nd-reindex : + ∀ {o} → EchoStep (Graph id) o → EchoStep StepND o +det→nd-reindex = map-rel det→nd + +---------------------------------------------------------------------- +-- 4. The agreement, WITH CONTENT. A non-deterministic relation is, at +-- each output, a SUM of deterministic branches. The `StepND` +-- echo-fibre over `true` is exactly the disjoint sum of its two +-- branch fibres — the `stay-true` branch (state `true`) and the +-- `flip-to-true` branch (state `false`). The bijection is established +-- by CASE ANALYSIS on the `StepND` constructors, not by `refl`/Σ-η, +-- and not by collapsing to a graph (which §2 proved impossible). This +-- IS the honest agreement of the nd model with deterministic data: +-- not "nd = some graph" but "nd = a structured sum of graphs". + +NDBranch : Set +NDBranch = ⊤ ⊎ ⊤ -- inj₁ = stay-true branch ; inj₂ = flip branch + +to-sum : EchoStep StepND true → NDBranch +to-sum (true , stay-true) = inj₁ tt +to-sum (false , flip-to-true) = inj₂ tt + +from-sum : NDBranch → EchoStep StepND true +from-sum (inj₁ tt) = true , stay-true +from-sum (inj₂ tt) = false , flip-to-true + +-- Round-trips. Each is genuine constructor case analysis: a single +-- `refl` does NOT inhabit either ∀-statement (the fibre has two +-- structurally distinct inhabitants). +nd-sum-fromto : ∀ e → from-sum (to-sum e) ≡ e +nd-sum-fromto (true , stay-true) = refl +nd-sum-fromto (false , flip-to-true) = refl + +nd-sum-tofrom : ∀ b → to-sum (from-sum b) ≡ b +nd-sum-tofrom (inj₁ tt) = refl +nd-sum-tofrom (inj₂ tt) = refl + +-- The two branch inhabitants are genuinely distinct (the fibre is not +-- a proposition — exactly what no single deterministic graph fibre +-- over a point can be): content the `× ⊤` pseudo-model cannot express. +nd-fibre-not-prop : + Σ (EchoStep StepND true) (λ a → + Σ (EchoStep StepND true) (λ b → a ≢ b)) +nd-fibre-not-prop = + (true , stay-true) + , (false , flip-to-true) + , λ p → true≢false (cong proj₁ p) diff --git a/proofs/agda/Smoke.agda b/proofs/agda/Smoke.agda index 4e93189..c344018 100644 --- a/proofs/agda/Smoke.agda +++ b/proofs/agda/Smoke.agda @@ -210,6 +210,36 @@ open import EchoRelModel using ; bridge-natural ) +-- Pillar F, Gate F4 (docs/echo-types/earn-back-plan.adoc; retraction +-- follow-up F-2026-05-18a). The terminal-cone universal property, +-- earned back as TRUE CONDITIONAL ON an explicit `funext` parameter +-- (never a postulate). The unconditional pointwise mediator property +-- is kept as the funext-free corollary. Names pinned so a rename or +-- a slide back to an *unconditional* claim fails CI fast. +open import EchoPullbackUnivF4 using + ( FunExt₀ + ; echo-pullback-univ-strict -- m' ≡ m, GIVEN funext (no postulate) + ; echo-pullback-univ-pointwise -- ∀ v → m' v ≡ m v, funext-free + ) + +-- Pillar F, Gate F2 (same plan / follow-up). A genuine second model +-- of the *bare* Echo functor on the non-deterministic, non-graph +-- relation `StepND`: same interface as the deterministic model, +-- functor laws hold, agreement has content (constructor case +-- analysis, not refl / not Σ-η on × ⊤), and `nd-not-graph` is the +-- checked proof it is NOT a disguised graph. Scope: the Echo +-- functor, NOT the graded comonad / model-independence (still +-- retracted, R-2026-05-18). +open import EchoStepNDModelF2 using + ( EchoFunctorModel + ; det-model + ; nd-model + ; nd-not-graph -- StepND is no function's graph + ; det→nd -- content-bearing witness preservation + ; nd-sum-fromto -- nd fibre = sum of det branches + ; nd-fibre-not-prop -- the fibre is not a proposition + ) + open import EchoTropical using ( Candidate ; score