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