thermo: close the C+ identity-only gap (injective + Bishop-finite), pin O-THERMO-∞#58
Merged
hyperpolymath merged 2 commits intoMay 18, 2026
Conversation
…n O-THERMO-∞ The STABILITY_ANALYSIS §3.3 ~70%/C+ rating was driven by one concrete gap: the only proved zero-cost (Bennett) instance was the identity map at index zero (bennett-reversible-id-zero). The general ThermodynamicOptimality predicate was otherwise unproved off that point. Closed cases (proved, --safe --without-K, zero postulates, zero escape pragmas; All.agda + Smoke.agda re-verified exit 0): - EchoFiberCount.FiberSize-fin-injective: any injective f : Fin n → B that hits y has fiber size exactly 1 (generalises FiberSize-fin-id-zero off the identity and off index zero). - EchoThermodynamics.bennett-reversible-injective: zero erasure bound for every injective map at every value it hits; id-zero is now a corollary. - EchoThermodynamicsFinite (new module): the exact blocker to generalising past Fin n is that fiber-erasure-bound is routed through FiberSize-fin, whose totality is structural recursion on the Fin index bound. Removed for any Bishop-finite carrier via transport along an explicit bijection (record FiniteDomain): bennett-reversible-finite, landauer-collapse-finite, fiber-erasure-bound-fin. Stated falsifiable obligation: - O-THERMO-∞ (docs/ECHO-CNO-BRIDGE.adoc §"Thermodynamic Bridge"): the infinite-carrier case (ProgramState = ℕ → ℕ) admits no --safe-total cost functional agreeing with fiber-erasure-bound on finite restrictions. Stated with an explicit kill condition (exhibit such a cost, or mechanise the impossibility), not softened to "future work". Honours retraction R-2026-05-18: orthogonal to the retracted graded-comonad / two-models / conservativity / universal-property / funext claims; no retracted claim reinstated; no Agda module weakened. Docs: ECHO-CNO-BRIDGE.adoc §"Thermodynamic Bridge" (proved generalisations + O-THERMO-∞ + Theorem 4 + AZ mapping row); STABILITY_ANALYSIS.md §3.3 + coverage matrix (C+ 70% -> B- 85%, with the single residual named). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> (cherry picked from commit 315af4213ea4add9498e5e41c34e9acceabbd43f)
Per MAP.adoc governance rule "update the relevant Directions entry *and* its status tag in the same PR". Thermodynamic entry stays [REAL*] (real, still partial) but the description now records: Bennett zero-cost generalised to every injective map on any Bishop-finite carrier; identity-at-zero is a corollary; sole residual = falsifiable obligation O-THERMO-∞; re-rated B-/~85% (was C+/~70%). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
hyperpolymath
added a commit
that referenced
this pull request
May 18, 2026
Route (a): mechanise the impossibility. EchoThermoCollapseImpossible
proves the doc's own kill condition, second horn — (i)∧(ii) ⊢ ⊥ —
verbatim, for the obligation's named witness.
- nat-into-collapse-fiber{-injective}: ℕ ↪ Echo (const y₀) y₀ — the
collapse fiber is infinite (the structural reason no finite count
exists), recorded positively.
- collapse-cost-impossible: any total --safe cost on (ℕ → B) agreeing
with fiber-erasure-bound on every finite restriction of the constant
map is impossible — clause (ii) at n=1,2 (T=1, via FiberSize-fin-
const, PR #58's honest count) forces its single value to be both 0
and 1. Impossibility CONFIRMED.
The quantitative-collapse functional provably does not extend to an
infinite carrier as a total --safe function: a settled NEGATIVE
boundary, not an open gap, not a defect. Orthogonal to the Bennett
zero direction (closed for all carriers, this PR's earlier commit).
Governance docs flipped O-THERMO-∞ [OPEN] → [CLOSED-NEG] and the
Thermodynamic Direction [REAL*] → [REAL] (no open obligation remains);
STABILITY §3.3 re-rated B- → B / ~95% (standing B- freeze lifts —
discharged negatively counts as discharged; not higher since a
confirmed-negative is an honest limit, and the separate
Information-Theory Direction stays unbuilt).
All --safe --without-K, zero postulates, zero escape pragmas (the lone
'postulate' string is the comment false-positive class, EchoKernel
precedent). Smoke.agda + All.agda exit 0; new headlines pinned.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
hyperpolymath
deleted the
thermo/bennett-injective-finite-stack-2026-05-18
branch
hyperpolymath
added a commit
that referenced
this pull request
May 18, 2026
…nite) Steps 1-3 of the thermodynamic-bridge continuation, stacked on PR #58. 1. EchoThermodynamicsArbitrary: FiberSubsingleton (K-free, --without-K safe surrogate for fibre isProp) + injective⇒fiber-subsingleton for an arbitrary carrier A : Set a (no Fin, no FiniteDomain). 2. reversible-erasure-cost (occupancy-keyed) + bennett-reversible- arbitrary: Bennett zero-cost for every injective map on any carrier, no finiteness. Anti-vacuity: occupancy≡FiberSize-fin and bennett-arbitrary-refines-finite certify the structural cost coincides with PR #58's established count and strictly subsumes it. 3. cno-identity over the genuine infinite absolute-zero Program carrier; bennett-reversible-cno-identity makes 'a CNO dissipates zero Landauer energy' a real theorem, not the historically vacuous claim. EchoFiberCount: added FiberSize-fin-subsingleton (Headline 2c), the finite-domain anti-vacuity hook (FiberSize-fin-injective is its corollary; kept as-is upstream for pin stability). O-THERMO-∞ unchanged and NOT discharged: re-narrowed in docs to be specifically the quantitative-collapse functional on an infinite carrier (orthogonal to the now-closed Bennett zero direction). All --safe --without-K, zero postulates, zero escape pragmas. Smoke.agda + All.agda exit 0. Docs (ECHO-CNO-BRIDGE §Thermodynamic Bridge, STABILITY_ANALYSIS §3.3 ~90%/B-, MAP.adoc status tag) updated in the same PR per the MAP governance rule. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
hyperpolymath
added a commit
that referenced
this pull request
May 18, 2026
Route (a): mechanise the impossibility. EchoThermoCollapseImpossible
proves the doc's own kill condition, second horn — (i)∧(ii) ⊢ ⊥ —
verbatim, for the obligation's named witness.
- nat-into-collapse-fiber{-injective}: ℕ ↪ Echo (const y₀) y₀ — the
collapse fiber is infinite (the structural reason no finite count
exists), recorded positively.
- collapse-cost-impossible: any total --safe cost on (ℕ → B) agreeing
with fiber-erasure-bound on every finite restriction of the constant
map is impossible — clause (ii) at n=1,2 (T=1, via FiberSize-fin-
const, PR #58's honest count) forces its single value to be both 0
and 1. Impossibility CONFIRMED.
The quantitative-collapse functional provably does not extend to an
infinite carrier as a total --safe function: a settled NEGATIVE
boundary, not an open gap, not a defect. Orthogonal to the Bennett
zero direction (closed for all carriers, this PR's earlier commit).
Governance docs flipped O-THERMO-∞ [OPEN] → [CLOSED-NEG] and the
Thermodynamic Direction [REAL*] → [REAL] (no open obligation remains);
STABILITY §3.3 re-rated B- → B / ~95% (standing B- freeze lifts —
discharged negatively counts as discharged; not higher since a
confirmed-negative is an honest limit, and the separate
Information-Theory Direction stays unbuilt).
All --safe --without-K, zero postulates, zero escape pragmas (the lone
'postulate' string is the comment false-positive class, EchoKernel
precedent). Smoke.agda + All.agda exit 0; new headlines pinned.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
hyperpolymath
added a commit
that referenced
this pull request
May 18, 2026
…ive (#60) Thermodynamic-bridge continuation. **Stacked on PR #58** (base = `thermo/bennett-injective-finite-stack-2026-05-18`, itself on PR #54 `docs/echo-types-master-map`). Depends on #58's `bennett-reversible-injective` / `FiberSize-fin-injective` / `FiberSize-fin-const` and on MAP.adoc (only on the #54 branch). **Re-target chain:** #54→main, then #58→main, then **this PR→main**. (Automated poll armed; merges out-of-band.) This PR closes the thermodynamic pillar: **no open obligation remains** for the Thermodynamic Direction (`[REAL*]` → `[REAL]`, B- → B / ~95%). ## Part 1 — Bennett zero-cost on an arbitrary carrier (Steps 1–3) The finiteness in PR #58 / `EchoThermodynamicsFinite` was an artefact of routing cost through `FiberSize-fin` (an enumeration); Bennett's physical content (no fan-in) needs no finiteness. 1. **`FiberSubsingleton` + `injective⇒fiber-subsingleton`** — K-free `--without-K`-safe "no fan-in" predicate, for an **arbitrary** carrier `A : Set a`. (Full fibre `isProp` would need `B` an h-set/UIP, unavailable under `--without-K`; the first-projection form is what the count needs.) 2. **`bennett-reversible-arbitrary`** — Bennett zero-cost for every injective map on **any** carrier, no `Fin`/`FiniteDomain`, via an occupancy-keyed `reversible-erasure-cost`. **Anti-vacuity:** `occupancy≡FiberSize-fin` + `bennett-arbitrary-refines-finite` prove it coincides with and strictly subsumes #58's established count. 3. **`bennett-reversible-cno-identity`** — instantiated at `cno-identity : Program → Program` over the genuine **infinite** absolute-zero `Program` carrier: "a CNO dissipates zero Landauer energy" is now a real theorem, not the historically vacuous claim. `EchoFiberCount` gains `FiberSize-fin-subsingleton` (`FiberSize-fin-injective` is its corollary; kept as-is upstream for pin stability). ## Part 2 — O-THERMO-∞ discharged negatively → `[CLOSED-NEG]` Route (a): mechanise the impossibility. `EchoThermoCollapseImpossible` proves the obligation's **own kill condition, second horn — (i)∧(ii) ⊢ ⊥ — verbatim**, for its named witness: - `nat-into-collapse-fiber{-injective}`: `ℕ ↪ Echo (const y₀) y₀` — the collapse fiber is infinite (the structural reason no finite count exists). - `collapse-cost-impossible`: any total `--safe` `cost` agreeing with `fiber-erasure-bound` on every finite restriction of the constant map is impossible — clause (ii) at `n = 1, 2` (`T = 1`, via `FiberSize-fin-const`) forces its single value to be both `0` and `1`. The quantitative-collapse functional provably does **not** extend to an infinite carrier as a total `--safe` function: a settled negative boundary, **not** a softened "future work" item and **not** a defect. Orthogonal to the Bennett zero direction (closed for all carriers, Part 1). ## Verification - All `--safe --without-K`, **zero postulates, zero escape pragmas** (the lone `postulate` string is the comment false-positive class — EchoKernel precedent). - `Smoke.agda` + `All.agda` typecheck (exit 0); all new headlines pinned in `Smoke.agda`. - Governance docs updated same PR per the MAP rule: `ECHO-CNO-BRIDGE.adoc` §"Thermodynamic Bridge" (O-THERMO-∞ → `[CLOSED-NEG]`), `STABILITY_ANALYSIS.md` §3.3 (B / ~95%, with explicit rationale for the freeze-lift), `docs/echo-types/MAP.adoc` (`[REAL*]` → `[REAL]`, proofs list). Honours retraction R-2026-05-18 — orthogonal; nothing retracted is reinstated. The separate Information-Theory bridge (Theorem 5) remains unbuilt by design — a different Direction. 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
hyperpolymath
added a commit
that referenced
this pull request
May 18, 2026
#57 reduced to its sole content not already in main: the new module proofs/agda/Ordinal/Buchholz/OrderExtendedDirect.agda (225 lines) + Smoke pins + All.agda registration. F1/F4/F2 spikes and the doc reframes from the original branch were superseded by #54/#55/#56/#58/#60 (present in main, byte-identical) and the Nix-flake commit dropped (Guix-primary policy). Typechecks --safe --without-K, zero postulates; full All.agda + Smoke + characteristic + examples suites green. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What
Advances the Thermodynamic — Landauer/Bennett direction from its
~70% / C+ rating by closing the one concrete gap that drove that rating
and converting the residual into a single falsifiable obligation.
The C+ gap was specific: the only proved zero-cost (Bennett) instance
was
bennett-reversible-id-zero— the identity map, at index zero.ThermodynamicOptimality(p) := fiber-erasure-bound p σ _≟_ T ≡ 0wasotherwise unproved off that single point.
Closed cases (proved)
All
--safe --without-K, zero postulates, zero escape pragmas;proofs/agda/All.agda+proofs/agda/Smoke.agdare-verify exit 0.EchoFiberCount.FiberSize-fin-injective— any injectivef : Fin n → Bthat hitsyhas fiber size exactly1(generalises
FiberSize-fin-id-zerooff the identity and offindex zero).
EchoThermodynamics.bennett-reversible-injective— zero erasurebound for every injective map at every value it hits;
bennett-reversible-id-zerois now a corollary.EchoThermodynamicsFinite(new) — names the exact blocker togeneralising past
Fin n(fiber-erasure-boundis routed throughFiberSize-fin, whose totality is structural recursion on theFinindex bound) and removes it for any Bishop-finite carrier via
transport along an explicit bijection (record
FiniteDomain):bennett-reversible-finite,landauer-collapse-finite.Stated falsifiable obligation
docs/ECHO-CNO-BRIDGE.adoc§"ThermodynamicBridge"): no
--safe-total cost functional on an infinite carrier(
ProgramState = ℕ → ℕ) can agree withfiber-erasure-boundon thefinite restrictions. Stated with an explicit kill condition
(exhibit such a
cost, or mechanise the impossibility) — notsoftened to "future work".
Honours retraction R-2026-05-18
Orthogonal to the retracted graded-comonad / two-models /
conservativity / universal-property / funext claims. No retracted
claim reinstated; no Agda module weakened or edited.
Docs (same PR)
docs/ECHO-CNO-BRIDGE.adoc§"Thermodynamic Bridge" — provedgeneralisations, O-THERMO-∞, Theorem 4, AZ mapping row.
docs/STABILITY_ANALYSIS.md§3.3 + coverage matrix — C+ 70% → B-85%, single residual named.
docs/echo-types/MAP.adoc— Thermodynamic Directions entry + statustag (governance rule). Stays
[REAL*](real, still partial) untilO-THERMO-∞ is discharged or refuted.
Base
Stacked on
docs/echo-types-master-map(PR #54) becauseMAP.adocdoes not exist on
mainyet and the governance rule requires thestatus-tag update in the same PR. Re-target to
mainonce #54 lands.🤖 Generated with Claude Code