From 25fb76074af3d85550a2ad6894593fb6187c6c11 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 26 May 2026 23:20:21 +0100 Subject: [PATCH] fix+feat: resolve paper.adoc merge conflict + clear related-work [EXPAND] + land Track C MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Three-in-one batch closing the remaining session items. 1. P0 — paper.adoc merge-conflict resolution - Remove three unresolved git conflict markers at lines 557, 1137, 1156 (from merge commit cab99f1 incorporating reframe/retraction- 2026-05-18). The HEAD chunk (579 lines of substantive proof-size / threats-to-validity / related-work analysis) and the incoming chunk (related-work [EXPAND] note + 2-cat ruleout note) both kept; conflict markers stripped, no content lost. - Delete duplicate Reframing note (37 lines at former 1207-1243); single canonical copy retained earlier in the file. - paper.adoc 1278 → 1238 lines. 2. Lane 1 close-out — paper.adoc [EXPAND] tag 2 (related-work pass) - Clear the two stale TODO notes (related-work expansion + 2-cat ruleout fold-in). Both notes' content was silently delivered in the substantive subsections above: §"HoTT homotopy fibres", §"Graded comonads, coeffects, and QTT", §"Lenses and optics (the witness-transport leg)" — the latter already containing the 2-categorical rule-out at lines 948-953. - Replaced with a single explanatory NOTE pointing at the delivered subsections + the comparators.adoc companion. - Lane 1 close-out: only the ordinal-appendix [EXPAND] (tag 4) remains, gated on the Bachmann-Howard milestone per design. 3. Lane 2 close-out item 2 — Track C - New proofs/agda/examples/EchoVsSigma.agda. Three lemmas pairing each headline example with the small raw-Σ counter-program the Echo interface refuses to export at affine mode: * parser-sigma-distinguishes (echo-parse-nested vs echo-parse- pair at parses≡true, via proj₁ + paren-nested≢paren-pair) * provenance-sigma-distinguishes (echo-prov-true vs echo-prov- false at project≡0, via prov∘proj₁ + true≢false) * absint-sigma-distinguishes (echo-pos-p1 vs echo-pos-p2 at α≡pos, via proj₁ + p1≢p2) - Mirrors EchoAbstractionBarrier.sigma-distinguishes at the per-example level. Together with EchoAbstractionBarrier.affine- consumer-cannot-distinguish, establishes the Gate 3 matched-positive + matched-negative pair discipline ("raw Σ would leak; Echo blocks it"). - Builds clean under --safe --without-K, zero postulates. - Wired into examples/All.agda; pinned in Smoke.agda under own using-block. 4. Roadmap Lane 2 update - Mark Track C item as LANDED 2026-05-26. Gate-2 nominee re-audit (item 3) remains the sole open requirement for full Lane 2 close-out. Build verification: agda proofs/agda/All.agda, proofs/agda/Smoke.agda, proofs/agda/examples/All.agda all exit 0 under --safe --without-K. Retraction discipline (R-2026-05-18) respected throughout: no new prose introduces graded-comonad, full-universal-property, model-independence, or general-parametricity claims. Co-Authored-By: Claude Opus 4.7 (1M context) --- docs/echo-types/paper.adoc | 74 ++++-------------- proofs/agda/Smoke.agda | 11 +++ proofs/agda/examples/All.agda | 1 + proofs/agda/examples/EchoVsSigma.agda | 104 ++++++++++++++++++++++++++ roadmap.adoc | 15 ++-- 5 files changed, 140 insertions(+), 65 deletions(-) create mode 100644 proofs/agda/examples/EchoVsSigma.agda diff --git a/docs/echo-types/paper.adoc b/docs/echo-types/paper.adoc index a1bbeb0..fd002f7 100644 --- a/docs/echo-types/paper.adoc +++ b/docs/echo-types/paper.adoc @@ -554,7 +554,6 @@ mechanised strength, neither less nor more. === Proof size per pillar -<<<<<<< HEAD The four pillars together occupy ~930 lines across six modules, with zero postulates and three `rewrite` sites (one in the foundational `degrade-compose`; one in its `rel-model` lift; one in @@ -1134,26 +1133,21 @@ Swamy et al. "Dependent types and multi-monadic effects in F\*" (POPL 2016); Vazou–Seidel–Jhala–Vytiniotis–Peyton Jones "Refinement types for Haskell" (ICFP 2014, Liquid Haskell). -======= -NOTE: *[EXPAND]* — detailed positioning against: Granule / QTT graded -modalities; comonadic notions of computation (Uustalu–Vene); -coeffects (Petriček–Orchard–Mycroft); HoTT fibrewise constructions; -lens / optic literature (the witness-transport leg of -`echo-pullback-univ` resembles the very-well-behaved *1-lens* laws — -no 2-cell-equipped optic, see below). Make the novelty crisp: not a -new object, but a fully mechanised characterisation package with a -falsifiable-gate methodology. - -NOTE: *[2-cat ruled out, see `decisions/no-2-cat.adoc`]* — when the -related-work pass expands the lens/optic comparison and the -graded-modality positioning, fold in the 2-categorical rule-out: a -"bicategorical echo" reading was considered and ruled out on the -landed evidence (every would-be 2-cell appears as `refl` or is -prop-forced trivial by `≤g-prop` / `⊑-prop`); the construction -resembles a very-well-behaved *1-lens*, not a 2-cell-equipped optic. -The closure note in `decisions/no-2-cat.adoc` is the load-bearing -artifact; this paragraph should cite it rather than re-argue. ->>>>>>> docs/rule-out-2cat-and-roadmap-correction + +NOTE: *Related-work `[EXPAND]` cleared 2026-05-26.* The original +`[EXPAND]` TODO requested detailed positioning against Granule / QTT +graded modalities, Uustalu–Vene comonads, Petriček–Orchard–Mycroft +coeffects, HoTT fibrewise constructions, and the lens / optic +literature with the 1-lens-vs-2-cell-optic clarification. That work +has been delivered above in §"HoTT homotopy fibres", §"Graded comonads, +coeffects, and QTT", and §"Lenses and optics (the witness-transport +leg)" — including the explicit 2-categorical rule-out at the end of +the lens/optic subsection (`docs/echo-types/decisions/no-2-cat.adoc` +is the load-bearing closure note). A companion single-page comparator +table at `docs/echo-types/comparators.adoc` (Echo vs Granule / QTT / +choreographic / Linear Haskell) ships the axis-by-axis summary form +for reviewers who want the at-a-glance positioning rather than the +prose narrative above. [#reframing-note] == Reframing note (2026-05-18) @@ -1204,44 +1198,6 @@ via a genuine non-graph `StepND` model (§6 NOTE, `EchoStepNDModelF2.agda`). The graded-comonad, modality-level model-independence, and conservativity rows remain fully retracted. -[#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, diff --git a/proofs/agda/Smoke.agda b/proofs/agda/Smoke.agda index 97780ae..1847ed8 100644 --- a/proofs/agda/Smoke.agda +++ b/proofs/agda/Smoke.agda @@ -378,6 +378,17 @@ open import EchoAbstractionBarrier using ; sigma-distinguishes ) +-- examples.EchoVsSigma — Track C of the Echo-vs-Σ identity claim. +-- Per-example raw-Σ counter-programs paired with each headline +-- example (parser, provenance, absint) — the matched-negative +-- companions for Gate 3. See `roadmap.adoc` §Lane 2 close-out +-- item 2. +open import examples.EchoVsSigma using + ( parser-sigma-distinguishes + ; provenance-sigma-distinguishes + ; absint-sigma-distinguishes + ) + open import EchoGraded using ( Grade ; degrade diff --git a/proofs/agda/examples/All.agda b/proofs/agda/examples/All.agda index 2bf668e..7af859b 100644 --- a/proofs/agda/examples/All.agda +++ b/proofs/agda/examples/All.agda @@ -15,3 +15,4 @@ import examples.TropicalArgmin import examples.EpistemicUpdate import examples.LinearErasure import examples.Transport +import examples.EchoVsSigma diff --git a/proofs/agda/examples/EchoVsSigma.agda b/proofs/agda/examples/EchoVsSigma.agda new file mode 100644 index 0000000..c637c01 --- /dev/null +++ b/proofs/agda/examples/EchoVsSigma.agda @@ -0,0 +1,104 @@ +{-# OPTIONS --safe --without-K #-} + +-- Track C of the Echo-vs-Σ identity claim consolidation +-- (`roadmap.adoc` §Lane 2 close-out item 2; companion to +-- `core/skepticisms/is-this-just-sigma-types.md` §5 and +-- `docs/echo-types/sigma-distinctness-map.adoc` §"Demand 5"). +-- +-- For each headline example (parser, provenance, absint), exhibit the +-- small raw-Σ counter-program that the Echo interface refuses to +-- export at affine mode. Each `*-sigma-distinguishes` is the +-- *negative companion* to the positive distinct-echoes-same-y theorem +-- already in the example module: it shows the concrete consumer that +-- would let the bug through if `proj₁` (or anything that factors +-- through it) were exposed. +-- +-- The pattern mirrors `EchoAbstractionBarrier.sigma-distinguishes` at +-- the per-example level. Together with the affine-side guarantee in +-- `EchoAbstractionBarrier.affine-consumer-cannot-distinguish`, these +-- per-example negatives establish the Gate 3 "matched-positive + +-- matched-negative pair" discipline ("raw Σ would leak; Echo blocks +-- it") for each headline example. +-- +-- Scope guardrail: each lemma is a *concrete instance* of the raw-Σ +-- distinguish pattern at the linear-side echo, exhibiting what an +-- unprotected Σ-projection would do with the example's distinct +-- preimages. The corresponding affine-side guarantee that nothing of +-- this shape can exist is the general `affine-consumer-cannot-distinguish`, +-- not re-proven here per-example. + +module examples.EchoVsSigma where + +open import Echo using (Echo) + +open import EchoExampleParser + using ( Token + ; parses + ; paren-pair; paren-nested + ; echo-parse-pair; echo-parse-nested + ; paren-nested≢paren-pair + ) +open import EchoExampleProvenance + using ( Row; project + ; echo-prov-true; echo-prov-false + ; true≢false + ) +open Row using (prov) +open import EchoExampleAbsInt + using ( Sign; Carrier; pos; α + ; p1; p2 + ; echo-pos-p1; echo-pos-p2 + ; p1≢p2 + ) + +open import Data.Bool.Base using (Bool; true) +open import Data.List.Base using (List) +open import Data.Product.Base using (Σ; _,_; proj₁) +open import Relation.Binary.PropositionalEquality + using (_≡_; _≢_) +open import Function.Base using (_∘_) + +---------------------------------------------------------------------- +-- Parser example (`EchoExampleParser`). +-- +-- `paren-nested` (`((` `)` `)`) and `paren-pair` (`(` `)` `(` `)`) +-- both have `parses ≡ true`. The Echo retains the distinction +-- (`echo-parse-nested≢echo-parse-pair`). The raw-Σ counter-program +-- below uses `proj₁` directly to recover the original `List Token`, +-- distinguishing the two echoes via the already-proven +-- `paren-nested≢paren-pair`. The Echo interface at affine mode would +-- refuse to export `proj₁`; this lemma exhibits exactly what would +-- leak if it didn't. + +parser-sigma-distinguishes : + Σ (Echo parses true → List Token) + (λ g → g echo-parse-nested ≢ g echo-parse-pair) +parser-sigma-distinguishes = proj₁ , paren-nested≢paren-pair + +---------------------------------------------------------------------- +-- Provenance example (`EchoExampleProvenance`). +-- +-- `row-with-prov-true` and `row-with-prov-false` project to the same +-- payload (`project ≡ 0`) but carry distinct provenance Booleans. The +-- Echo retains the provenance (`echo-prov-true≢echo-prov-false`). The +-- raw-Σ counter-program composes `prov` with `proj₁` to leak the +-- provenance Bool, distinguishing the two echoes via `true≢false`. + +provenance-sigma-distinguishes : + Σ (Echo project 0 → Bool) + (λ g → g echo-prov-true ≢ g echo-prov-false) +provenance-sigma-distinguishes = prov ∘ proj₁ , true≢false + +---------------------------------------------------------------------- +-- Abstract-interpretation example (`EchoExampleAbsInt`). +-- +-- `p1` and `p2` both abstract to `pos` under the 5-element sign +-- lattice (`α p1 ≡ α p2 ≡ pos`). The Echo retains the concrete +-- carrier (`echo-pos-p1≢echo-pos-p2`). The raw-Σ counter-program +-- uses `proj₁` to recover the concrete Carrier, distinguishing via +-- `p1≢p2`. + +absint-sigma-distinguishes : + Σ (Echo α pos → Carrier) + (λ g → g echo-pos-p1 ≢ g echo-pos-p2) +absint-sigma-distinguishes = proj₁ , p1≢p2 diff --git a/roadmap.adoc b/roadmap.adoc index c0689ea..3133cff 100644 --- a/roadmap.adoc +++ b/roadmap.adoc @@ -161,14 +161,17 @@ gate cross-links) landed in-session. Tracks B + C remain. *Close-out criterion (falsifiable).* All three hold: -. Track B (consumer-side abstraction barrier) — same artefact named in - Lane 1's close-out. (Lane 1 and Lane 2 share this artefact; that is - intentional, not duplication.) -. Track C (per-example raw-Σ counter-programs) lands as - `proofs/agda/examples/EchoVsSigma.agda`, pairing each headline - example with the small Σ-misuse it blocks. Pinned in Smoke. +. *LANDED 2026-05-26.* Track B (consumer-side abstraction barrier) — + same artefact named in Lane 1's close-out. (Lane 1 and Lane 2 share + this artefact; that is intentional, not duplication.) +. *LANDED 2026-05-26.* Track C (per-example raw-Σ counter-programs) + shipped as `proofs/agda/examples/EchoVsSigma.agda`, pairing each + headline example (parser, provenance, abs-int) with the small + Σ-misuse it blocks. Builds clean under `--safe --without-K`; + pinned in `Smoke.agda` under own `using` block. . The Gate 2 nominee list is re-audited and crosses the *comfortable* threshold (≥ 3 of 4 surviving), not merely the honest minimum. + *(Remaining open item for Lane 2 close-out.)* *Artefacts (landed today).* `core/skepticisms/is-this-just-sigma-types.md` (canonical answer doc, 5-section structure mirroring the demands);