hyperpolymath · Nov 9, 2026
@@ -126,8 +126,10 @@ CI run or the separate named CI check requested in #321.
 == Build invariant (verified)
 
 * `--safe --without-K` throughout `proofs/agda/**`.
-* `agda proofs/agda/All.agda` (≈200 modules) and `agda proofs/agda/Smoke.agda`
-  exit 0. Last verified 2026-06-18.
+* `agda proofs/agda/All.agda` and `agda proofs/agda/Smoke.agda` exit 0. Last
+  verified 2026-11-09 (local, cold, Agda 2.7.0.1 + the pinned stdlib and
+  absolute-zero via `scripts/setup-agda.sh`; all eight CI entrypoints and the
+  four guard scripts passed; not a CI receipt).
 * Guardrails are CI-enforced (`tools/check-guardrails.sh`): every file under
   `proofs/agda/**` must declare `{-# OPTIONS --safe --without-K #-}`, and
   `believe_me`, `postulate`, `TERMINATING`, `REWRITE`, `NO_POSITIVITY_CHECK`,
@@ -141,13 +143,20 @@ CI run or the separate named CI check requested in #321.
   both triangle identities).
 * Pentagon coherence — `Echo-comp-pent-Σ-assoc` (full Σ-associativity iso).
 
-=== Establishment track — Pillars A–D COMPLETE
+=== Establishment track — Pillars A–D (narrowed by R-2026-05-18)
 * *A* `EchoFiberBridge.agda` — `echo↔fib` definitional bridge (Echo ≡ fibre).
-* *B* `EchoGradedComonad.agda` (graded-comonad laws) + `EchoPullback.agda`
-  (funext-free, K-free terminal-cone universal property).
+* *B* `EchoGradedComonad.agda` and `EchoPullback.agda` are real modules, but
+  R-2026-05-18 withdrew the "graded-comonad laws" and "terminal-cone universal
+  property" readings (`docs/retractions.adoc`). What stands: `EchoGraded` is a
+  thin-poset reindexing modality, and `EchoPullback` proves existence with
+  pointwise uniqueness; the strict universal property is the funext-qualified
+  F4 module.
 * *C* `EchoSeparating.agda` — separating model; characteristic law refuted.
-* *D* `EchoRelModel.agda` — model-independence theorem (`GCLaws` once for any
-  model) + `docs/echo-types/conservativity.adoc` metatheorem.
+* *D* `EchoRelModel.agda` — `GCLaws` instantiated at `set-model` and
+  `rel-model`, which share one grade poset: carrier-parametricity over a
+  fixed poset, not semantic model-independence. The conservativity
+  metatheorem was withdrawn and now lives in
+  `docs/retracted/conservativity.adoc`.
 
 === Canonical-identity spine (Tier 1/2/3)
 `EchoTotalCompletion` (`A ≃ Σ B (Echo f)`), `EchoOrthogonalFactorizationSystem`,
@@ -157,7 +166,65 @@ CI run or the separate named CI check requested in #321.
 (`EchoOFSUnivF5*`), the audience moves (`EchoProvenance`, `EchoSecurity`,
 `EchoProbabilisticSupport`, `EchoDifferential`), `EchoCanonicalIdentitySuite`,
 `EchoDeniability`, and `EchoAggregation` (micro→macro aggregation as an Echo
-map; `aggregate-non-injective` + `no-canonical-disaggregation`).
+map; `pairSum-non-injective` + `no-canonical-disaggregation`).
+
+=== Design audit (2026-11-09)
+
+A statement-level review against the claims in this file, `Smoke.agda`
+comments and module headers. Every term type-checks; these entries record
+where a statement says less than the surrounding text claimed. Comments
+and labels were corrected in the same change; no proof term changed.
+
+[cols="2,3",options="header"]
+|===
+| Result | What it actually states
+
+| `EchoThermodynamicsArbitrary.bennett-reversible-arbitrary`
+| *Vacuous as stated*: the injectivity hypothesis is unused and the cost is 0
+for every `f`. A faithful Bennett statement is `open`.
+
+| `EchoDeniability.partial-deniable-restricted`
+| Restates its hypothesis (`IsConstantOpener d` is the goal). No exactness or
+minimality of the constant-opener class is proved.
+
+| `Echo.Separation.NotResourceInstance.measure-not-injective`
+| Conditional: a measure that already agrees on two distinct echoes
+identifies them. It does not show every measure is lossy.
+
+| `EchoAbstractionBarrier`
+| Shows affine consumers are blind and `proj₁` is not. There is no enforced
+barrier: `Echo` is a transparent Σ.
+
+| `EchoEntropy`
+| The shadow is constant, so "blind" holds by construction. Not a Shannon
+entropy result; real-valued entropy stays `open`.
+
+| `EchoLLEncoding`
+| Holds for encodings whose linear carrier is a proposition. Not a statement
+about all LL encodings (the identity encoding keeps no-section).
+
+| F5 (`EchoOFSUnivF5*`)
+| Existence of a comparison iso, not its uniqueness; the lifting uses only
+that one leg is an equivalence. "F5 full pass" means the three slices
+landed, not a full orthogonal factorisation system in the usual sense.
+
+| `EchoVariance`, `EchoGradedComonadF1` (Smoke comments)
+| The maps do not supply a graded monad, the fibre round trips are not an
+adjunction, and F1 is a lossless writer that does not mention Echo.
+
+| `EchoProvenance`
+| Its Echo-vs-Σ clearance claim does not hold (Echo is definitionally Σ).
+
+| `EchoImageFactorizationProp`
+| Conditional on a `TruncInterface` that the `--safe` build does not supply;
+the (epi, mono) gate stays `open`.
+|===
+
+Under PROOF-POLICY §8 every theorem here is `ungraded`: no PWG-3 receipt
+(Agda version, standard-library pin, flags, import cone, commit) is recorded
+in-repo, and no Rocq or Lean leg exists. CNO-facing results also inherit the
+limits recorded in absolute-zero's 2026-11-09 design audit (its `IsCNO` is
+degenerate).
 
 === Ordinal / Buchholz track — moved
 The ordinal lane left echo-types on 2026-10-20 (echo-types#349, decision

@@ -429,8 +429,8 @@ The echo-invariant line: epistemic structure, choreographies, roles.
 Certified Null Operations = echo types where `f = id`. absolute-zero is
 both a *dependency* of the core and a *bridge* target.
 
-* Proofs: `proofs/agda/EchoCNOBridge.agda`, `MinimalCNO.agda`,
-  `WorkingCNO.agda`.
+* Proofs: `proofs/agda/EchoCNOBridge.agda` (in `All.agda`). `MinimalCNO.agda`
+  and `WorkingCNO.agda` are not reachable from `All.agda`.
 * Docs: `docs/ECHO-CNO-BRIDGE.adoc`,
   `docs/echo-types/cross-repo-bridge-status.md`.
 

@@ -68,13 +68,13 @@ open import EchoStabilityTests
 open import VecRotation
 
 -- Establishment-plan pillars (docs/echo-types/establishment-plan.adoc).
--- A is a real bridge; B–D are doc-only scaffolds (no declarations,
--- typecheck under --safe --without-K, tracked here per policy).
+-- All four are real modules now; R-2026-05-18 narrowed what B and D
+-- claim (see docs/retractions.adoc and PROOF-STATUS.adoc).
 open import EchoFiberBridge     -- Pillar A (landed)
-open import EchoPullback        -- Pillar B (scaffold)
-open import EchoGradedComonad   -- Pillar B (scaffold)
-open import EchoSeparating      -- Pillar C (scaffold)
-open import EchoRelModel        -- Pillar D (scaffold)
+open import EchoPullback        -- Pillar B
+open import EchoGradedComonad   -- Pillar B
+open import EchoSeparating      -- Pillar C
+open import EchoRelModel        -- Pillar D
 
 -- Pillar F earn-back (docs/echo-types/earn-back-plan.adoc). Wired in
 -- on the gate passing (Sequencing pt 4); see docs/retractions.adoc

@@ -14,9 +14,11 @@
 -- module establishes that invariant in two complementary, mechanised
 -- ways — it does NOT claim the impossible universal "no semiring can
 -- ever encode any echo-like quotient"; it claims the useful project
--- invariant that the proof-relevant Echo structure is not determined
--- by any semiring-valued grade/measure, so any such measure is a
--- lossy observation.
+-- invariant that the specific grade/measure examples below are lossy
+-- observations of the proof-relevant Echo structure. (Audit 2026-11-09:
+-- the general form below is conditional on the measure already agreeing
+-- on two distinct echoes; it does not show that every measure is lossy,
+-- and an injective measure, e.g. the identity, exists.)
 --
 -- Pillar 1 (structural — the index axis is real).
 --   The characteristic degradation law `degrade-compose` is carried
@@ -132,8 +134,8 @@ equal-measure-does-not-imply-equal-echo =
 -- (in particular any semiring-/resource-algebra-valued residue
 -- measure that factors through the trivial residue), if `m` agrees on
 -- the two distinct echoes then it identifies two distinct residues.
--- So a residue measure is always a lossy observation of Echo, never a
--- faithful encoding of it.
+-- This repackages the hypothesis; it is a conditional, not a proof that
+-- every residue measure is lossy.
 ----------------------------------------------------------------------
 
 measure-not-injective :

@@ -26,17 +26,17 @@
 --   `affine-consumer-cannot-distinguish` — POSITIVE: any
 --   `g : LEcho affine → X` assigns the same value to the weakened
 --   images of `echo-true` and `echo-false`. Direct corollary of
---   `affine-all-equal`. This is what the Echo interface GUARANTEES
---   that raw Σ does not.
+--   `affine-all-equal`: functions out of the contractible affine
+--   carrier are constant.
 --
 --   `sigma-distinguishes` — NEGATIVE: the raw Σ-projection `proj₁`
 --   IS a consumer that distinguishes `echo-true` from `echo-false`.
---   Exhibiting this concrete counter-program makes the abstraction
---   barrier a checked artefact, not a wish: the Echo interface
---   refuses to export `proj₁` *exactly because* `sigma-distinguishes`
---   shows what would happen if it did.
 --
--- Together they say: hiding `proj₁` is a guarantee, not a convention.
+-- Audit 2026-11-09: there is no enforced abstraction barrier. `Echo` is
+-- a transparent Σ (no `abstract` block), and `proj₁` is used on Echo
+-- throughout the repo. The pair of theorems shows what a barrier WOULD
+-- buy (affine consumers are blind, proj₁ is not); hiding `proj₁` is a
+-- convention, not a checked guarantee.
 --
 -- Honest framing notes:
 -- * "Theorem 1" (consumer factorisation) from the original sketch was

@@ -173,7 +173,9 @@ IsConstantOpener d = d Trace ≡ d Erased
 -- For any constant opener, the two histories remain indistinguishable
 -- even under injective production: d cannot exploit the residue
 -- difference if it never looks.  Goal reduces by computation to
--- d Trace ≡ d Erased, which is exactly `const`.
+-- d Trace ≡ d Erased, which is exactly `const`: the theorem restates
+-- its hypothesis (audit 2026-11-09). No exactness or minimality of
+-- this class is proved.
 ------------------------------------------------------------------------
 
 partial-deniable-restricted :

@@ -33,15 +33,15 @@
 --   * CONST — `f = λ _ → y₀`. Then `Echo f y₀` is canonically `A`
 --     itself (every domain element is a preimage of the unique
 --     image), and `Echo f y ≡ ⊥-shape` for `y ≢ y₀` (the fibre is
---     empty whenever `y` is distinct from `y₀`). The full-domain
---     fibre at `y₀` is packaged as `const-fibre-↔-domain`.
+--     empty whenever `y` is distinct from `y₀`). Only a section
+--     A → fibre at `y₀` is proved; the full ↔ needs UIP on B
+--     (no `const-fibre-↔-domain` exists; audit 2026-11-09).
 --
 -- Closes Tier 2 #2 per the synthesis-roadmap reorder (Image → Loss →
 -- Residue → Decoration → ObsEquiv). The headlines below are
 -- almost-all re-exports / restatements; the load-bearing NEW content
 -- is the EQUIV case's `HasInverse` record + the three small
--- theorems hanging off it, and the CONST case's `↔`-packaged
--- fibre-is-domain witness.
+-- theorems hanging off it, and the CONST case's section.
 --
 -- Headlines (pinned in Smoke.agda):
 --
@@ -266,7 +266,7 @@ const-fibre-section-projects-to-id _ _ = refl
 --   EQUIV                    │  centre + uniq up to UIP / contractibility
 --   INJ                      │  projection unique (K-free here)
 --   SURJ                     │  every fibre inhabited (refl iff)
---   CONST  (at y₀)           │  fibre IS the domain (↔ proved here)
+--   CONST  (at y₀)           │  section from the domain (↔ needs UIP)
 --
 -- Cases NOT covered by the four headlines, with reasons:
 --

@@ -64,9 +64,10 @@
 -- The falsifier per the Echo-vs-Σ Track A/B/C bar: if every
 -- headline below could be re-proved using only `Σ` + `_≡_` (no
 -- `Echo`), the module would fail to clear the bar. The headlines
--- below directly invoke `Echo`'s fibre-shape primitives; replacing
--- `Echo project p` by a generic Σ would lose the residue-collapse
--- alignment with `EchoResidue.collapse-residue-same`.
+-- below directly invoke `Echo`'s fibre-shape primitives.
+-- Audit 2026-11-09: `Echo` is definitionally a Σ, so by the falsifier
+-- above these headlines CAN be re-proved with Σ + `_≡_`; the clearance
+-- claim does not hold, and PROOF-STATUS's Echo-vs-Σ banner governs.
 
 module EchoProvenance where
 

@@ -54,10 +54,10 @@
 --   * FiberSubsingleton                     -- K-free "no fan-in"
 --   * injective⇒fiber-subsingleton          -- arbitrary carrier
 --   * reversible-erasure-cost               -- structural Bennett cost
---   * bennett-reversible-arbitrary          -- injective ⇒ cost 0, any A
+--   * bennett-reversible-arbitrary          -- cost 0 (inj UNUSED; see below)
 --   * occupancy≡FiberSize-fin               -- faithfulness vs. #58 count
 --   * bennett-arbitrary-refines-finite      -- subsumes #58 finite result
---   * bennett-reversible-cno-identity       -- the real CNO theorem
+--   * bennett-reversible-cno-identity       -- cost 0 at the CNO identity
 
 module EchoThermodynamicsArbitrary where
 
@@ -144,11 +144,12 @@ occupancy-cost-zero f y (yes _) T
 occupancy-cost-zero f y (no  _) T
   rewrite ⌊log₂0⌋≡0 = *-zeroʳ (k * T)
 
--- HEADLINE. Bennett zero-cost for *any* injective `f : A → B`, with
--- `A` an arbitrary `Set a` — no `Fin n`, no `FiniteDomain`. The
--- injectivity hypothesis carries the physical content (it is what
--- makes the cost model faithful, via the subsingleton); the equality
--- to 0 then holds at every temperature and every fibre.
+-- Audit 2026-11-09: VACUOUS AS STATED. The proof is
+-- `occupancy-cost-zero`, which holds for EVERY `f` (occupancy is 0 or 1
+-- and ⌊log₂⌋ of either is 0), so the `inj` argument is unused and the
+-- non-injective Boolean collapse gets cost 0 too. A faithful Bennett
+-- statement needs a cost that can be non-zero for non-injective maps
+-- (open). The type is kept for API compatibility.
 bennett-reversible-arbitrary :
   ∀ {a b} {A : Set a} {B : Set b}
   (f : A → B) (y : B)