From 834e8ad7ee0399b088da0d607abd22fd72b0ed26 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 13:22:06 +0000 Subject: [PATCH 1/2] docs(proofs): correct claims that say more than the Agda states MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit A statement-level review (2026-11-09) compared the ledger, Smoke.agda comments and module headers with the statements they describe. This commit changes comments, ledger text and labels only; no proof term changes, and every theorem name and Smoke pin is kept. Vacuous or hypothesis-restating results, now labelled as such: - EchoThermodynamicsArbitrary.bennett-reversible-arbitrary: the injectivity hypothesis is unused; the cost is 0 for every f. - EchoDeniability.partial-deniable-restricted: restates its hypothesis. - NotResourceInstance.measure-not-injective: conditional, not "every measure is lossy". Overclaims corrected: - PROOF-STATUS "Pillars A–D COMPLETE" restated the claims R-2026-05-18 withdrew (graded-comonad laws, terminal-cone UP, model-independence, conservativity metatheorem). - EchoAbstractionBarrier (no enforced barrier; Echo is a transparent Σ), EchoEntropy (blind by construction), EchoLLEncoding (propositional carriers only), F5 (existence of the comparison iso, not uniqueness), EchoVariance/F1 Smoke comments (no graded monad, no adjunction; F1 is a lossless writer that does not mention Echo), EchoProvenance (the Echo-vs-Σ clearance does not hold), ImageFactorizationProp (conditional on a TruncInterface the --safe build does not supply). - Stale names and notes: const-fibre-↔-domain, aggregate-non-injective, F5-3 "final open slice", All.agda "scaffold" labels, σ–π "set equality", MAP.adoc CNO module list. PROOF-STATUS gains a "Design audit (2026-11-09)" table and records that every theorem is `ungraded` under PROOF-POLICY §8 (no PWG-3 receipt in repo; no Rocq/Lean leg). Checked: All, Smoke and AuditSmoke compile under `--safe --without-K --cubical-compatible` with the pinned toolchain (Agda 2.7.0.1, stdlib 8326c74, absolute-zero f486c29, via scripts/setup-agda.sh); kernel-guard, check-agda-invocations, check-no-unsafe and tools/check-guardrails.sh pass. Local, not a CI receipt. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01MF5GeeBBDF6sUzr6pZTjWV --- PROOF-STATUS.adoc | 83 ++++++++++++++-- docs/echo-types/MAP.adoc | 4 +- proofs/agda/All.agda | 12 +-- .../Echo/Separation/NotResourceInstance.agda | 12 ++- proofs/agda/EchoAbstractionBarrier.agda | 14 +-- proofs/agda/EchoDeniability.agda | 4 +- proofs/agda/EchoLossTaxonomy.agda | 10 +- proofs/agda/EchoProvenance.agda | 7 +- proofs/agda/EchoThermodynamicsArbitrary.agda | 15 +-- proofs/agda/Smoke.agda | 99 ++++++++++--------- 10 files changed, 171 insertions(+), 89 deletions(-) diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc index 33af9e8c..e93f8b2b 100644 --- a/PROOF-STATUS.adoc +++ b/PROOF-STATUS.adoc @@ -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 diff --git a/docs/echo-types/MAP.adoc b/docs/echo-types/MAP.adoc index 639cf61e..e6b825d4 100644 --- a/docs/echo-types/MAP.adoc +++ b/docs/echo-types/MAP.adoc @@ -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`. diff --git a/proofs/agda/All.agda b/proofs/agda/All.agda index afc06452..79ffb393 100644 --- a/proofs/agda/All.agda +++ b/proofs/agda/All.agda @@ -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 diff --git a/proofs/agda/Echo/Separation/NotResourceInstance.agda b/proofs/agda/Echo/Separation/NotResourceInstance.agda index 1f056df3..f8e74127 100644 --- a/proofs/agda/Echo/Separation/NotResourceInstance.agda +++ b/proofs/agda/Echo/Separation/NotResourceInstance.agda @@ -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 : diff --git a/proofs/agda/EchoAbstractionBarrier.agda b/proofs/agda/EchoAbstractionBarrier.agda index 038c673f..038b5fcb 100644 --- a/proofs/agda/EchoAbstractionBarrier.agda +++ b/proofs/agda/EchoAbstractionBarrier.agda @@ -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 diff --git a/proofs/agda/EchoDeniability.agda b/proofs/agda/EchoDeniability.agda index 55f27d96..3342774e 100644 --- a/proofs/agda/EchoDeniability.agda +++ b/proofs/agda/EchoDeniability.agda @@ -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 : diff --git a/proofs/agda/EchoLossTaxonomy.agda b/proofs/agda/EchoLossTaxonomy.agda index bc117ef6..89963d56 100644 --- a/proofs/agda/EchoLossTaxonomy.agda +++ b/proofs/agda/EchoLossTaxonomy.agda @@ -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: -- diff --git a/proofs/agda/EchoProvenance.agda b/proofs/agda/EchoProvenance.agda index 510e8887..0adacdbc 100644 --- a/proofs/agda/EchoProvenance.agda +++ b/proofs/agda/EchoProvenance.agda @@ -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 diff --git a/proofs/agda/EchoThermodynamicsArbitrary.agda b/proofs/agda/EchoThermodynamicsArbitrary.agda index 26dafa11..1926b1cd 100644 --- a/proofs/agda/EchoThermodynamicsArbitrary.agda +++ b/proofs/agda/EchoThermodynamicsArbitrary.agda @@ -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) diff --git a/proofs/agda/Smoke.agda b/proofs/agda/Smoke.agda index 05786096..c2cf3591 100644 --- a/proofs/agda/Smoke.agda +++ b/proofs/agda/Smoke.agda @@ -159,8 +159,8 @@ open import EchoReversibilityBridge using -- operational once-only reversal discipline. `takeForReverse` replays a -- `holding` cell / fails on `spent`; `consume` transitions Holding→Spent; -- `once-only` is the headline — after `consume`, a further `takeForReverse` --- is always `nothing` (the state-machine form of the Idris `(1 e)` linear --- consumption). `holding-reverses` / `spent-does-not-reverse` mirror the +-- is always `nothing`. It holds definitionally and mirrors the Idris +-- discipline; it does not enforce linear consumption (audit 2026-11-09). `holding-reverses` / `spent-does-not-reverse` mirror the -- Idris `holdingReverses` / `spentDoesNotReverse`. open import EchoResidueCell using ( ResidueCell @@ -244,8 +244,10 @@ open import EchoImageFactorization using -- EchoImageFactorizationProp — (epi, mono) image factorisation -- module-parameterised in a propositional-truncation interface --- (`TruncInterface`). Closes the (epi, mono) earn-back gate the --- base module flagged: takes ∥_∥ as an explicit module parameter +-- (`TruncInterface`). Conditional: nothing in the --safe build supplies +-- a `TruncInterface` (only the quarantined postulated shadow or the +-- cubical island does), so the (epi, mono) gate stays OPEN in +-- PROOF-STATUS. Takes ∥_∥ as an explicit module parameter -- (mirroring the funext-as-module-parameter discipline of -- `EchoOFSUnivF5`), then ships the (-1)-truncated image + its -- monic right leg + its mere-surjective left leg. Zero postulates @@ -259,9 +261,10 @@ open import EchoImageFactorizationProp using -- EchoLossTaxonomy — function-side classification of `f : A → B` -- by echo shape. Four cases: EQUIV (centre + projection unique), -- INJ (projection unique, re-export), SURJ (every fibre inhabited, --- re-export), CONST (fibre at y₀ ↔ A). The EQUIV/CONST cases ship --- new content (`HasInverse` record, `const-fibre-↔-domain` packaged --- as `↔`); INJ/SURJ are taxonomy-side renames of the +-- re-export), CONST (a section A → fibre at y₀; the full ↔ needs UIP +-- and is not proved). The EQUIV/CONST cases ship new content +-- (`HasInverse` record and the CONST section); INJ/SURJ are +-- taxonomy-side renames of the -- `EchoImageFactorization` headlines. Honest scope: the full -- "contractible fibre" and "propositional fibre" upgrades need UIP / -- truncation and are documented as the next earn-back. Companion to @@ -366,7 +369,7 @@ open import EchoFiberTriangulation using ( echo-is-stdlib-witness -- T1 calibration ; all-echo→stdlib-strictly-surjective ; stdlib-strictly-surjective→all-echo - ; echo↔coecho -- T2 genuine content + ; echo↔coecho -- T2 (an involution by sym) ; all-echo→stdlib-surjection -- T3 surjection tie ) @@ -618,13 +621,12 @@ open import EchoThermodynamics using ; landauer-collapse ) --- EchoEntropy — discrete Shannon-entropy non-distinguishing theorem. --- Companion to EchoAbstractionBarrier: the entropic shadow (fibre --- count = 2 bit on collapse@tt) agrees on echo-true vs echo-false, --- so any consumer factoring through it cannot distinguish them. +-- EchoEntropy — a discrete entropy shadow (fibre count 2 on a Fin 2 +-- encoding of collapse@tt). The shadow is a constant function, so the +-- "blind" results hold by construction (refl); they record that a +-- count-valued consumer cannot see the witness, not a Shannon-entropy +-- theorem. Real-valued Shannon entropy remains OPEN (audit 2026-11-09). -- Matched-negative via `sigma-distinguishes` (witness side does). --- Closes the "Shannon-entropy formalisations not yet present" item --- flagged in EchoThermodynamics + EchoStabilityTests. open import EchoEntropy using ( collapse-as-fin ; collapse-fibre-count @@ -646,6 +648,9 @@ open import EchoThermodynamicsFinite using ; landauer-collapse-finite ) +-- Audit 2026-11-09: `bennett-reversible-arbitrary` does not use its +-- injectivity hypothesis; the structural cost is 0 for every f +-- (occupancy is 0 or 1 and ⌊log₂⌋ of either is 0). Vacuous as stated. open import EchoThermodynamicsArbitrary using ( FiberSubsingleton ; injective⇒fiber-subsingleton @@ -722,13 +727,12 @@ open import EchoAbstractionBarrier using ; sigma-distinguishes ) --- EchoLLEncoding — linear-logic shallow-encoding gap. Companion to --- EchoAbstractionBarrier: no standard LL `!A`-style shadow encoding --- preserves Echo's `no-section-weaken` property, because the --- distinguishing data lives in the witness LL discards. The trivial --- ⊤-shadow is the canonical LL `!A := 1` model and admits a section --- of the encoded weakening; the source side does not. Closes the --- LL-encoding-gap follow-up to the abstraction-barrier audit. +-- EchoLLEncoding — linear-logic shallow-encoding gap. Every encoding +-- whose linear carrier is a proposition (`ForgetsWitness`) admits a +-- section of the encoded weakening, so `no-section-weaken` does not +-- survive it; the ⊤-shadow (`!A := 1`) is one such encoding. This is +-- not a claim about all LL encodings: the identity encoding X = LEcho +-- keeps no-section, and `enc-commutes` is not used (audit 2026-11-09). open import EchoLLEncoding using ( LLShallowEncoding ; trivial-encoding @@ -854,15 +858,19 @@ open import EchoOFSUnivF5 using -- `lift x = h (e⁻¹ x)` where `e⁻¹` is the inverse from `HasInverse e`. -- Both triangles (lift ∘ e ≡ h, proj₁ ∘ lift ≡ k) commute pointwise -- K-free; strict forms lifted via funext. Uniqueness K-free pointwise; --- strict via funext. F5-2 partial-pass; F5-3 (factorisation uniqueness --- up to iso) remains the final open slice for full F5 pass. +-- strict via funext. (F5-3 landed later; see below.) The lift uses only +-- that `e` is an equivalence, not anything about proj₁ or Echo. open import EchoOFSUnivF5Diag using ( module Pointwise ; module Strict ) --- Pillar F, Gate F5 third slice — F5 FULL PASS. --- Factorisation uniqueness up to iso. Given any second (eq, proj) +-- Pillar F, Gate F5 third slice. Audit 2026-11-09: this proves that a +-- comparison iso EXISTS for any second factorisation; it does not prove +-- the iso unique, and the F5-2 lifting holds against any map, so the +-- "full OFS" here is not the (equivalence, projection) system in the +-- usual sense. Read "F5 full pass" below as "three slices landed". +-- Given any second (eq, proj) -- factorisation `f = p ∘ g` with `g : A → X` an equivalence (via -- `HasInverse`), construct the canonical iso `φ : X ↔ Σ B (Echo f)` -- with `φ.to ∘ g ≡ encode f` and `proj₁ ∘ φ.to ≡ p` (both strict @@ -929,8 +937,9 @@ open import EchoTransaction using ) -- EchoSelectiveProjection — relational-algebra σ–π commutativity (issue --- #176). Column-safe selection commutes with projection (set-equality of --- the result relations); a projected-away-column predicate admits no +-- #176). Column-safe selection commutes with projection (logical +-- equivalence ⇔ of membership in the result relations); a +-- projected-away-column predicate admits no -- column-restricted lift (the non-commuting counterexample). open import EchoSelectiveProjection using ( SelectiveProjection @@ -996,9 +1005,10 @@ open import EchoDifferential using -- (2026-06-13). Two production functions at opposite ends of the -- deniability spectrum: produce-perfect (constant → fully deniable, -- no section) and produce-partial (injective → not deniable for --- arbitrary openers, has section). IsConstantOpener is the exact --- cut-point at which deniability is restored for the partial case; --- it is the type-level analogue of the `affine` mode in +-- arbitrary openers, has section). For a constant opener the partial +-- case is deniable, but `partial-deniable-restricted` is its hypothesis +-- restated (no exactness or minimality is proved); IsConstantOpener +-- is the type-level analogue of the `affine` mode in -- EchoObservationalEquivalence. no-section-produce-perfect / partial- -- has-section make the duality a checked theorem pair. open import EchoDeniability using @@ -1051,11 +1061,11 @@ open import EchoStepNDModelF2 using ; nd-fibre-not-prop -- the fibre is not a proposition ) --- Pillar F, Gate F1 — the MAKE-OR-BREAK gate (docs/echo-types/ --- earn-back-plan.adoc §F1). A genuine graded comonad on the --- iterated-residue carrier `D r A = r nested R-layers`, with grade --- monoid (ℕ, +, 0), Echo as the grade-unit object (D 0 (Echo f y) is --- the bare echo), NESTED comultiplication δ : D (m+n) ⇒ D m ∘ D n, +-- Pillar F, Gate F1 (docs/echo-types/earn-back-plan.adoc §F1). A graded +-- comonad on the iterated-product carrier `D r A = A × Bool^r`, with +-- grade monoid (ℕ, +, 0). It does not mention Echo, and it is lossless: +-- δ is `coe` along a type equality and is inverted by μ-writer (see +-- EchoVariance). Comultiplication δ : D (m+n) ⇒ D m ∘ D n, -- all three graded-comonad laws proved, and a separating witness -- showing D 2 is not collapsing to ⊤. --safe --without-K, zero -- postulates, no funext. Scope: this earns back the graded-comonad @@ -1096,20 +1106,19 @@ open import EchoGradedComonadInstance2 using -- Variance verdict (docs/echo-types/variance-resolution.adoc): the -- monad / comonad / adjunction status of loss accumulation, resolved in --- --safe Agda rather than asserted. Accumulation is the graded-MONAD --- multiplication (total + canonical); recoverability is exact on the --- grade-0 fibre (the section/retraction adjunction); the graded-COMONAD --- direction fails for genuine loss (no bare-residue recovery); the --- "graded comonad" reading (F1) is the LOSSLESS complement-storing writer --- (δ invertible). Pinned so a slide back to an unqualified "graded --- comonad of loss" claim fails CI fast. +-- --safe Agda. Audit 2026-11-09: these maps do NOT supply a graded monad, +-- and the fibre round trips are not an adjunction (EchoVariance's own +-- header says so; EchoDependentPushforward supplies an adjunction). +-- `no-bare-recovery` forbids a left inverse of one Boolean collapse; it +-- does not rule out graded comonads (EchoErasingGradedComonad is one). +-- The F1 reading is the lossless writer (δ invertible). open import EchoVariance using - ( accumulate -- μ : D_r (D_s A) → D_{r+s} A — accumulation is monadic + ( accumulate -- μ : D_r (D_s A) → D_{r+s} A (map shape only) ; split-with-factoring -- δ given the factoring (its inverse) ; accumulate-split-id -- exact on the fibre (round-trip refl) ; split-accumulate-id -- exact on the fibre (round-trip refl) - ; recoverable-fibre -- A ↔ Σ B (Echo f): the grade-0 section/retraction adjunction - ; no-bare-recovery -- the comonad obstruction: collapse has no section + ; recoverable-fibre -- A ↔ Σ B (Echo f): total completion (not an adjunction) + ; no-bare-recovery -- collapse has no left inverse ; fibre-retains-lost-bit -- the lost bit lives on the fibre, not as a complement ; μ-writer -- F1 writer's accumulation (inverse of δ) ; writer-μ-section -- writer δ is invertible ⇒ LOSSLESS (complement-storing) From 51cfb9ca57601d4e6611904e16119ea509499d57 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 15:19:30 +0000 Subject: [PATCH 2/2] proofs(thermo): faithful Bennett statement on an enumerated fibre MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit bennett-reversible-arbitrary keyed its cost on fibre occupancy (0 or 1), so the cost was 0 for every map and the injectivity hypothesis was unused (2026-11-09 audit). It is kept, marked deprecated. New, in EchoThermodynamicsArbitrary: - FiberEnum f y: a list of preimages of y that contains every echo's domain point and has no repeats; enumerated-erasure-cost = Landauer bound on its length. No finiteness of the domain is assumed. - bennett-enumerated: injective ⇒ cost 0 (inj is what proves it) - landauer-fan-in: two distinct preimages ⇒ cost ≥ k·T - collapse-enum / collapse-erasure-cost: Bool → ⊤ costs exactly T - bennett-enumerated-cno-identity at the identity on Program Pinned in Smoke.agda; PROOF-STATUS and STABILITY_ANALYSIS updated, and the latter no longer calls the identity-map instance a CNO result. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01MF5GeeBBDF6sUzr6pZTjWV --- PROOF-STATUS.adoc | 6 +- docs/STABILITY_ANALYSIS.adoc | 12 +- proofs/agda/EchoThermodynamicsArbitrary.agda | 149 ++++++++++++++++++- proofs/agda/Smoke.agda | 12 +- 4 files changed, 164 insertions(+), 15 deletions(-) diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc index e93f8b2b..7954516c 100644 --- a/PROOF-STATUS.adoc +++ b/PROOF-STATUS.adoc @@ -181,7 +181,11 @@ and labels were corrected in the same change; no proof term changed. | `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`. +for every `f`. Kept, deprecated. *Resolved 2026-11-09:* `bennett-enumerated` +computes the cost from an enumeration of the fibre (preimages, complete, no +repeats) and needs `inj`; `landauer-fan-in` proves the converse (two distinct +preimages cost at least k·T), and `collapse-erasure-cost` shows `Bool → ⊤` +costs exactly T. | `EchoDeniability.partial-deniable-restricted` | Restates its hypothesis (`IsConstantOpener d` is the goal). No exactness or diff --git a/docs/STABILITY_ANALYSIS.adoc b/docs/STABILITY_ANALYSIS.adoc index 56e1e07f..4e546a2d 100644 --- a/docs/STABILITY_ANALYSIS.adoc +++ b/docs/STABILITY_ANALYSIS.adoc @@ -95,12 +95,12 @@ for *every injective map* (`+bennett-reversible-injective+`), not just an explicit bijection (`+FiniteDomain+`, `+bennett-reversible-finite+`, `+landauer-collapse-finite+`) — `+--safe --without-K+`, zero postulates - Bennett zero-cost lifted further to an *arbitrary carrier — no -finiteness at all* (`+bennett-reversible-arbitrary+`, occupancy-keyed; -K-free subsingleton route), certified faithful vs. the established count -(`+occupancy≡FiberSize-fin+`, `+bennett-arbitrary-refines-finite+`), and -instantiated on the genuine *infinite* absolute-zero `+Program+` CNO -(`+bennett-reversible-cno-identity+`) — the historically vacuous "`CNO -dissipates zero energy`" is now a real theorem - Landauer worst-case +finiteness at all* (`+bennett-enumerated+`, keyed on an enumeration of +the fibre, with the converse `+landauer-fan-in+`; the earlier +`+bennett-reversible-arbitrary+`, occupancy-keyed, is vacuous and deprecated), +and instantiated on the identity map over the *infinite* absolute-zero +`+Program+` type (`+bennett-enumerated-cno-identity+`). That is the identity +function, not an executed CNO - Landauer worst-case collapse (`+landauer-collapse[-finite]+`) - *O-THERMO-∞ settled `+[CLOSED-NEG]+`*: the quantitative-collapse functional provably does _not_ extend to an infinite carrier as a total `+--safe+` function — diff --git a/proofs/agda/EchoThermodynamicsArbitrary.agda b/proofs/agda/EchoThermodynamicsArbitrary.agda index 1926b1cd..cfa1941a 100644 --- a/proofs/agda/EchoThermodynamicsArbitrary.agda +++ b/proofs/agda/EchoThermodynamicsArbitrary.agda @@ -54,7 +54,12 @@ -- * FiberSubsingleton -- K-free "no fan-in" -- * injective⇒fiber-subsingleton -- arbitrary carrier -- * reversible-erasure-cost -- structural Bennett cost --- * bennett-reversible-arbitrary -- cost 0 (inj UNUSED; see below) +-- * bennett-reversible-arbitrary -- DEPRECATED: cost 0 for every f +-- * FiberEnum, enumerated-erasure-cost -- faithful, enumerated fibre +-- * bennett-enumerated -- injective ⇒ cost 0 (uses inj) +-- * landauer-fan-in -- 2 preimages ⇒ cost ≥ k·T +-- * collapse-erasure-cost -- non-vacuity: Bool → ⊤ costs T +-- * bennett-enumerated-cno-identity -- faithful form at the CNO identity -- * occupancy≡FiberSize-fin -- faithfulness vs. #58 count -- * bennett-arbitrary-refines-finite -- subsumes #58 finite result -- * bennett-reversible-cno-identity -- cost 0 at the CNO identity @@ -64,12 +69,24 @@ module EchoThermodynamicsArbitrary where open import Level using (Level; _⊔_) import Data.Nat.Base as ℕ open ℕ using (ℕ; _*_) -open import Data.Nat.Properties using (*-zeroʳ) -open import Data.Nat.Logarithm using (⌊log₂_⌋) +open import Data.Nat.Base using (_≤_; z≤n; s≤s) +open import Data.Nat.Properties using + (*-zeroʳ; *-identityʳ; *-identityˡ; *-monoʳ-≤; m≤n⇒m≤1+n) +open import Data.Nat.Logarithm using (⌊log₂_⌋; ⌊log₂⌋-mono-≤) +open import Data.Bool.Base using (Bool; true; false) +open import Data.Unit.Base using (⊤; tt) +open import Data.Empty using (⊥-elim) +open import Relation.Nullary.Negation.Core using (¬_) +open import Data.List.Base using (List; []; _∷_; length) +open import Data.List.Relation.Unary.All using (All; []; _∷_) +open import Data.List.Relation.Unary.Any using (here; there) +open import Data.List.Membership.Propositional using (_∈_) +open import Data.List.Relation.Unary.Unique.Propositional using (Unique) +open import Data.List.Relation.Unary.AllPairs using ([]; _∷_) open import Data.Fin.Base using (Fin) open import Data.Product.Base using (Σ; _,_; _×_; proj₁) open import Relation.Nullary.Decidable.Core using (Dec; yes; no) -open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans) +open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong; subst) open import Echo using (Echo) open import CNO using (Program) @@ -147,9 +164,10 @@ occupancy-cost-zero f y (no _) T -- 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. +-- non-injective Boolean collapse gets cost 0 too. DEPRECATED: the +-- faithful statement is `bennett-enumerated` (Step 2b), whose cost can +-- be non-zero (`landauer-fan-in`, `collapse-erasure-cost`). The type is +-- kept for API compatibility. bennett-reversible-arbitrary : ∀ {a b} {A : Set a} {B : Set b} (f : A → B) (y : B) @@ -197,6 +215,115 @@ bennett-arbitrary-refines-finite f y _≟_ inj d i₀ hit T = bennett-reversible-arbitrary f y inj d T , bennett-reversible-injective f y _≟_ inj i₀ hit T +---------------------------------------------------------------------- +-- Step 2b — the enumerated-fibre cost (faithful; added 2026-11-09). +-- +-- The occupancy cost above is 0 for every `f`, so it cannot tell a +-- reversible map from an erasing one. Here the cost is computed from +-- a supplied enumeration of the fibre: a list of preimages of `y` that +-- contains every echo's domain point and has no repeats. No finiteness +-- of `A` is assumed; only the fibre over `y` must be enumerated. +-- Both directions are proved: +-- +-- * `bennett-enumerated` — injective ⇒ cost 0 (uses `inj`); +-- * `landauer-fan-in` — two distinct preimages ⇒ cost ≥ k·T; +-- +-- and `collapse-erasure-cost` exhibits a map with cost exactly T. +---------------------------------------------------------------------- + +record FiberEnum {a b} {A : Set a} {B : Set b} (f : A → B) (y : B) + : Set (a ⊔ b) where + field + elems : List A + sound : All (λ x → f x ≡ y) elems + complete : (e : Echo f y) → proj₁ e ∈ elems + distinct : Unique elems + +open FiberEnum public + +fiber-card : + ∀ {a b} {A : Set a} {B : Set b} {f : A → B} {y : B} → + FiberEnum f y → ℕ +fiber-card E = length (elems E) + +enumerated-erasure-cost : + ∀ {a b} {A : Set a} {B : Set b} {f : A → B} {y : B} → + FiberEnum f y → Temperature → Energy +enumerated-erasure-cost E T = landauer-bound T (fiber-card E) + +private + log₂≤1 : ∀ {n} → n ≤ 1 → ⌊log₂ n ⌋ ≡ 0 + log₂≤1 z≤n = refl + log₂≤1 (s≤s z≤n) = refl + + -- With no repeats and every element a preimage, injectivity leaves + -- room for at most one element. + injective-≤1 : + ∀ {a b} {A : Set a} {B : Set b} (f : A → B) {y : B} → + (∀ {x x′ : A} → f x ≡ f x′ → x ≡ x′) → + (xs : List A) → All (λ x → f x ≡ y) xs → Unique xs → length xs ≤ 1 + injective-≤1 f inj [] _ _ = z≤n + injective-≤1 f inj (x ∷ []) _ _ = s≤s z≤n + injective-≤1 f inj (x ∷ x′ ∷ xs) (px ∷ px′ ∷ _) ((x≢x′ ∷ _) ∷ _) = + ⊥-elim (x≢x′ (inj (trans px (sym px′)))) + + ∈⇒1≤length : ∀ {a} {A : Set a} {x : A} {xs : List A} → x ∈ xs → 1 ≤ length xs + ∈⇒1≤length {xs = _ ∷ _} _ = s≤s z≤n + + -- Two distinct members force at least two elements. + two-members : + ∀ {a} {A : Set a} {x₁ x₂ : A} {xs : List A} → + x₁ ∈ xs → x₂ ∈ xs → ¬ (x₁ ≡ x₂) → 2 ≤ length xs + two-members (here p₁) (here p₂) ne = ⊥-elim (ne (trans p₁ (sym p₂))) + two-members (here _) (there m₂) ne = s≤s (∈⇒1≤length m₂) + two-members (there m₁) (here _) ne = s≤s (∈⇒1≤length m₁) + two-members (there m₁) (there m₂) ne = m≤n⇒m≤1+n (two-members m₁ m₂ ne) + +-- HEADLINE (Bennett). An injective map has an enumerated fibre of at +-- most one element, so its erasure cost is 0. Unlike the occupancy +-- version, the hypothesis `inj` is what makes this true. +bennett-enumerated : + ∀ {a b} {A : Set a} {B : Set b} + (f : A → B) (y : B) + (inj : ∀ {x x′ : A} → f x ≡ f x′ → x ≡ x′) + (E : FiberEnum f y) (T : Temperature) → + enumerated-erasure-cost E T ≡ 0 +bennett-enumerated f y inj E T = + trans (cong (k * T *_) + (log₂≤1 (injective-≤1 f inj (elems E) (sound E) (distinct E)))) + (*-zeroʳ (k * T)) + +-- HEADLINE (Landauer, converse direction). Two distinct preimages of +-- `y` put at least two elements in any enumeration of the fibre, so the +-- erasure cost is at least k·T. +landauer-fan-in : + ∀ {a b} {A : Set a} {B : Set b} + (f : A → B) (y : B) (x₁ x₂ : A) → + ¬ (x₁ ≡ x₂) → f x₁ ≡ y → f x₂ ≡ y → + (E : FiberEnum f y) (T : Temperature) → + k * T ≤ enumerated-erasure-cost E T +landauer-fan-in f y x₁ x₂ ne h₁ h₂ E T = + subst (_≤ k * T * ⌊log₂ fiber-card E ⌋) (*-identityʳ (k * T)) + (*-monoʳ-≤ (k * T) + (⌊log₂⌋-mono-≤ {2} {fiber-card E} + (two-members (complete E (x₁ , h₁)) (complete E (x₂ , h₂)) ne))) + +-- Non-vacuity: the Boolean collapse has an enumerated fibre of two +-- elements and costs exactly k·T = T. +collapse : Bool → ⊤ +collapse _ = tt + +collapse-enum : FiberEnum collapse tt +collapse-enum = record + { elems = true ∷ false ∷ [] + ; sound = refl ∷ refl ∷ [] + ; complete = λ { (true , _) → here refl ; (false , _) → there (here refl) } + ; distinct = ((λ ()) ∷ []) ∷ ([] ∷ []) + } + +collapse-erasure-cost : ∀ T → enumerated-erasure-cost collapse-enum T ≡ T +collapse-erasure-cost T = trans (*-identityʳ (1 * T)) (*-identityˡ T) + ---------------------------------------------------------------------- -- Step 3 — the real CNO theorem, on the infinite carrier. -- @@ -223,3 +350,11 @@ bennett-reversible-cno-identity : reversible-erasure-cost cno-identity σ d T ≡ 0 bennett-reversible-cno-identity σ d T = bennett-reversible-arbitrary cno-identity σ cno-identity-injective d T + +-- The faithful form at the CNO identity, for any enumeration of its +-- fibre. +bennett-enumerated-cno-identity : + (σ : Program) (E : FiberEnum cno-identity σ) (T : Temperature) → + enumerated-erasure-cost E T ≡ 0 +bennett-enumerated-cno-identity σ E T = + bennett-enumerated cno-identity σ cno-identity-injective E T diff --git a/proofs/agda/Smoke.agda b/proofs/agda/Smoke.agda index c2cf3591..fe6ac1e4 100644 --- a/proofs/agda/Smoke.agda +++ b/proofs/agda/Smoke.agda @@ -650,9 +650,19 @@ open import EchoThermodynamicsFinite using -- Audit 2026-11-09: `bennett-reversible-arbitrary` does not use its -- injectivity hypothesis; the structural cost is 0 for every f --- (occupancy is 0 or 1 and ⌊log₂⌋ of either is 0). Vacuous as stated. +-- (occupancy is 0 or 1 and ⌊log₂⌋ of either is 0). Vacuous as stated, +-- kept deprecated. The faithful statement is `bennett-enumerated`, with +-- the converse `landauer-fan-in` and the witness `collapse-erasure-cost`. open import EchoThermodynamicsArbitrary using ( FiberSubsingleton + ; FiberEnum + ; fiber-card + ; enumerated-erasure-cost + ; bennett-enumerated + ; landauer-fan-in + ; collapse-enum + ; collapse-erasure-cost + ; bennett-enumerated-cno-identity ; injective⇒fiber-subsingleton ; reversible-erasure-cost ; bennett-reversible-arbitrary