echo-types: Bennett on an arbitrary carrier + O-THERMO-∞ closed-negative (#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>

Author: hyperpolymath

docs/ECHO-CNO-BRIDGE.adoc

@@ -75,19 +75,27 @@ bennett-reversible :
   fiber-erasure-bound f y _≟_ T ≡ 0
 ```
 
-**Status: PROVED**, and (2026-05-18) generalised twice: from the
-identity to *every injective map* (`bennett-reversible-injective`),
-and from `Fin n` to *any Bishop-finite carrier* via transport
-(`bennett-reversible-finite`, `EchoThermodynamicsFinite`).
-`bennett-reversible-id-zero` is now a corollary.
-
-**NOT proved**: the analogous claim over an infinite carrier
-(`ProgramState = ℕ → ℕ`). This is no longer a vague gap — it is the
-precise, falsifiable obligation **O-THERMO-∞**, stated with its kill
-condition in §"Thermodynamic Bridge" below. The earlier
-`cno-thermodynamic-optimality` formulation rested on a hardcoded
-`FiberSize ≡ 1` that made the claim vacuous; that hardcode is gone,
-and the honest finite/Bishop-finite case is proved instead.
+**Status: PROVED**, and (2026-05-18) generalised three times: from
+the identity to *every injective map* (`bennett-reversible-injective`),
+from `Fin n` to *any Bishop-finite carrier* via transport
+(`bennett-reversible-finite`, `EchoThermodynamicsFinite`), and from
+there to an *arbitrary carrier with no finiteness at all*
+(`bennett-reversible-arbitrary`, `EchoThermodynamicsArbitrary`),
+including the genuine infinite `Program` CNO
+(`bennett-reversible-cno-identity`). `bennett-reversible-id-zero` is a
+corollary. The Bennett zero direction is closed for *all* carriers.
+
+**The infinite-carrier _quantitative collapse_ functional is
+`[CLOSED-NEG]`**: not a vague gap and no longer open — the falsifiable
+obligation **O-THERMO-∞** is now discharged *negatively*, its
+impossibility mechanised (`collapse-cost-impossible`,
+`EchoThermoCollapseImpossible`; see §"Thermodynamic Bridge" below). A
+count-based collapse cost provably cannot exist on an infinite carrier
+as a total `--safe` function — a settled boundary, do not reopen. The
+earlier `cno-thermodynamic-optimality` formulation rested on a
+hardcoded `FiberSize ≡ 1` that made the claim vacuous; that hardcode
+is gone, the honest finite/Bishop-finite/arbitrary cases are proved,
+and the infinite count case is settled negative.
 
 ### Theorem 5: Information-preservation (NOT YET FORMALISED)
 
@@ -140,7 +148,7 @@ Absolute Zero defines CNOs with four properties:
 | `FinalState(p, σ) = σ` | `Echo p σ` contains `(σ, refl)` |
 | `NoSideEffects(p)` | `Echo p σ` is singleton (only `σ` maps to `σ`) |
 | `ThermodynamicallyReversible(p)` | `Echo p σ ≃ Echo id σ` |
-| `ThermodynamicOptimality(p)` | `fiber-erasure-bound p σ _≟_ T ≡ 0` _(proved for every injective `p` on any Bishop-finite carrier — Theorem 4; infinite-carrier case = falsifiable obligation O-THERMO-∞)_ |
+| `ThermodynamicOptimality(p)` | `reversible-erasure-cost p σ d T ≡ 0` _(proved for every injective `p` on **any** carrier — Bishop-finite via `fiber-erasure-bound`, arbitrary/infinite incl. the `Program` CNO via `reversible-erasure-cost` — Theorem 4; the quantitative-collapse functional on an infinite carrier is settled `[CLOSED-NEG]` — impossibility mechanised, `collapse-cost-impossible`)_ |
 | `InformationPreservation(p)` | _no formalised analogue — `echo-information-loss` was never defined; see Theorem 5_ |
 | `UniversalCNO(p)` | `∀ σ → Echo p σ ≃ Echo id σ` (NEW) |
 | `ModelIndependence(p)` | `Echo f y ≃ Echo f' y'` across isomorphic models (NEW) |
@@ -300,33 +308,84 @@ landauer-collapse-finite :
   fiber-erasure-bound-fin fd f y _≟_ T ≡ k * T * ⌊log₂ card fd ⌋
 ```
 
-### Open obligation O-THERMO-∞ (precise, falsifiable — not softened)
+**Proved — Bennett zero-cost on an _arbitrary_ carrier, past
+Bishop-finite (`EchoThermodynamicsArbitrary`).** The finiteness in the
+two results above is an artefact of routing cost through
+`FiberSize-fin` (an enumeration); the *physical content* of Bennett —
+a reversible map has no fan-in — needs no finiteness at all. An
+injective `f : A → B` has a subsingleton fiber for *any* `A : Set a`.
+Keying the Bennett cost on a decidable-inhabitation occupancy instead
+of an enumeration discharges this with no finiteness hypothesis,
+`--safe --without-K`, zero postulates:
 
-The infinite carrier (`ProgramState = ℕ → ℕ`, or any `A` with no
-`A ≃ Fin n`) does **not** generalise, and the reason is now stated
-sharply enough to be refuted:
+```agda
+FiberSubsingleton f y = (p q : Echo f y) → proj₁ p ≡ proj₁ q  -- K-free
+
+injective⇒fiber-subsingleton :                                -- any A
+  (inj : ∀ {x x′} → f x ≡ f x′ → x ≡ x′) → FiberSubsingleton f y
 
-> **O-THERMO-∞.** There is no function
+bennett-reversible-arbitrary :        -- A : Set a arbitrary; no Fin, no ≃
+  (inj : ∀ {x x′ : A} → f x ≡ f x′ → x ≡ x′)
+  (d : Dec (Echo f y)) (T : Temperature) →
+  reversible-erasure-cost f y d T ≡ 0
+```
+
+This is **not** a vacuous re-definition: `occupancy≡FiberSize-fin`
+proves the occupancy *coincides with* the established honest count
+`FiberSize-fin` on every finite restriction under the subsingleton
+hypothesis, and `bennett-arbitrary-refines-finite` shows it strictly
+subsumes the `Fin n` result of PR #58. The `--without-K` reason
+for the first-projection form (not full fiber `isProp`) is recorded in
+the module header: full `isProp` needs `B` an h-set / UIP, unavailable
+under `--without-K`; the projection form is K-free provable from
+injectivity and is exactly what the count needs.
+
+**The real CNO theorem, on the infinite carrier.** `cno-identity :
+Program → Program` (the absolute-zero `Program = List Instruction`
+carrier — *infinite*, the very `ProgramState`-flavoured type the
+original companion remarks disclaimed) is injective, so
+`bennett-reversible-cno-identity` gives erasure cost `≡ 0` at every
+fiber and temperature. "A CNO dissipates zero Landauer energy" is now
+a *real* theorem for the identity/injective CNO over the genuine
+infinite carrier — no longer the vacuous claim the deleted
+`ECHO-CNO-BRIDGE-SUMMARY.md` made.
+
+### O-THERMO-∞ — `[CLOSED-NEG]` (impossibility CONFIRMED)
+
+O-THERMO-∞ concerns *only* the **quantitative collapse** functional
+(`fiber-erasure-bound` / `landauer-collapse`, the count direction) on
+an infinite carrier — a strictly different functional from the
+occupancy-keyed Bennett cost, which is closed for all carriers
+(occupancy is capped at 1; the collapse cost grows as `⌊log₂ N⌋` with
+the fiber count). It is **discharged via the second horn of its own
+kill condition**: a mechanised proof that clauses (i)∧(ii) ⊢ ⊥.
+
+> **O-THERMO-∞ (as stated).** There is no function
 > `cost : (ℕ → B) → (y : B) → DecidableEquality B → Temperature → Energy`
 > that is (i) `--safe --without-K` total (no postulate, no escape
 > pragma), and (ii) agrees with `fiber-erasure-bound` on every finite
-> restriction `Fin n ↪ ℕ` (equivalently: agrees with
-> `fiber-erasure-bound-fin` for every `FiniteDomain`-witnessed
-> sub-carrier).
+> restriction `Fin n ↪ ℕ`.
+>
+> **Settled NEGATIVE.** `EchoThermoCollapseImpossible.collapse-cost-impossible`
+> mechanises (i)∧(ii) ⊢ ⊥ verbatim, for the doc's own named witness.
+> The constant map `c : ℕ → B`, `c _ = y₀` has an *infinite* fiber
+> (`nat-into-collapse-fiber{-injective}` exhibits `ℕ ↪ Echo c y₀` —
+> the structural reason no finite count exists). Its restriction along
+> any `Fin n ↪ ℕ` is the constant `Fin n → B`, whose
+> `fiber-erasure-bound` over `y₀` is `landauer-bound T n` (PR #58's
+> honest `FiberSize-fin-const`). Clause (ii) then forces the *single*
+> total value `cost c y₀ _≟_ T` to equal `landauer-bound T n` for
+> every `n`; at `T = 1` that is `⌊log₂ n⌋`, so it must be both `0`
+> (`n = 1`) and `1` (`n = 2`) — contradiction. Impossibility
+> **confirmed**: the quantitative-collapse functional provably does
+> *not* extend to an infinite carrier as a total `--safe` function.
 >
-> **Falsifier (how to kill this obligation).** Exhibit such a `cost`
-> and a mechanised proof of (i)+(ii); that refutes O-THERMO-∞ and
-> earns the claim back. **Witness that it bites:** the constant map
-> `c : ℕ → B`, `c _ = y₀` has `Echo c y₀ ≃ ℕ` — an infinite fiber.
-> Clause (ii) instantiated at the finite restrictions forces, by
-> `landauer-collapse`, `cost c y₀ _≟_ T = k · T · ⌊log₂ N⌋` with the
-> finite counts `N = 0,1,2,…` unboundedly — so any total `cost` must
-> assign `⌊log₂_⌋` of a quantity with no natural-number value. The
-> obligation is discharged in exactly one of two ways: a constructive
-> `cost` meeting (i)+(ii) (impossibility refuted), or a mechanised
-> proof that (i)∧(ii) ⊢ ⊥ (impossibility confirmed). Neither is in
-> the suite; until one lands, `ThermodynamicOptimality(p)` over an
-> infinite `ProgramState` is **`[OPEN]`**, not "future work".
+> This is a `[CLOSED-NEG]` boundary of the theory — a settled negative
+> result, **do not reopen**. It is *not* a softened "future work" item
+> and it is *not* a defect: the only way a count-based collapse cost
+> could exist on the infinite carrier is the (refuted) first horn, and
+> the negative is now mechanised. `--safe --without-K`, zero
+> postulates, zero escape pragmas; pinned in `Smoke.agda`.
 
 ### What is still NOT proved (unchanged)
 
@@ -342,11 +401,17 @@ sharply enough to be refuted:
    and `fiber-erasure-bound`; now at the full Bishop-finite-carrier
    level, not merely `Fin n`.
 2. **Thermodynamic Reversibility (shape)**: proved for *every*
-   injective map (`bennett-reversible-injective`) and lifted to any
-   Bishop-finite carrier (`bennett-reversible-finite`).
-   `bennett-reversible-id-zero` is now a corollary. The infinite
-   `ProgramState` case is the single, falsifiable obligation
-   O-THERMO-∞ above — `[OPEN]`, with a stated kill condition.
+   injective map (`bennett-reversible-injective`), lifted to any
+   Bishop-finite carrier (`bennett-reversible-finite`), and now to an
+   *arbitrary* carrier with no finiteness at all
+   (`bennett-reversible-arbitrary`), including the genuine infinite
+   `Program` CNO (`bennett-reversible-cno-identity`).
+   `bennett-reversible-id-zero` is a corollary. The Bennett zero
+   direction is closed for all carriers; the quantitative-collapse
+   functional on an infinite carrier (O-THERMO-∞) is now
+   **`[CLOSED-NEG]`** — its impossibility is mechanised
+   (`collapse-cost-impossible`), a settled boundary, no open
+   obligation remains for this Direction.
 3. **Information Theory**: not bridged. Open work — see
    `docs/echo-types/roadmap.md`.
 

docs/STABILITY_ANALYSIS.md

@@ -78,25 +78,46 @@ Echo {A = A} f y = Σ A (λ x → f x ≡ y)
 
 **Stability:** New but well-grounded in existing echo type theory
 
-#### 3.3 Thermodynamic Models: B- (was C+; advanced 2026-05-18)
-**Proofs:** `EchoThermodynamics.agda`, `EchoFiberCount.agda`, `EchoThermodynamicsFinite.agda`
+#### 3.3 Thermodynamic Models: B (was C+ → B-; advanced 2026-05-18)
+**Proofs:** `EchoThermodynamics.agda`, `EchoFiberCount.agda`, `EchoThermodynamicsFinite.agda`, `EchoThermodynamicsArbitrary.agda`, `EchoThermoCollapseImpossible.agda`
 - Landauer bound *shape* `k·T·⌊log₂ N⌋` (honest fiber count, no hardcode)
 - Bennett zero-cost for **every injective map** (`bennett-reversible-injective`),
   not just `id` at index zero — `bennett-reversible-id-zero` is now a corollary
 - Lifted off `Fin n` to **any Bishop-finite carrier** by transport along 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 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 — impossibility mechanised
+  (`collapse-cost-impossible`; `nat-into-collapse-fiber` exhibits the
+  collapse fiber as infinite). The doc's own kill condition,
+  discharged via its second horn
 
 **Stability:** The C+ ~70% rating was driven by one concrete gap — the only
-proved zero-cost instance was the identity at index zero. That gap is closed:
-optimality now holds for every injective map on every Bishop-finite carrier.
-The *single* remaining open item is the infinite-carrier case
-(`ProgramState = ℕ → ℕ`), now pinned as the **precise, falsifiable obligation
-O-THERMO-∞** with a stated kill condition (see
-`docs/ECHO-CNO-BRIDGE.adoc` §"Thermodynamic Bridge"). Not "needs more
-development" — one named obligation, refutable by exhibiting a total
-`--safe` cost functional or by mechanising its impossibility.
+proved zero-cost instance was the identity at index zero. That gap is fully
+closed: the Bennett zero-cost direction now holds for every injective map on
+**every carrier** — Bishop-finite *and* arbitrary/infinite, including the
+genuine infinite `Program` CNO. The previously-open item — the **quantitative
+collapse functional** (`fiber-erasure-bound` / `landauer-collapse`) on an
+infinite carrier, the obligation **O-THERMO-∞** — is now **discharged
+negatively**: `collapse-cost-impossible` mechanises its kill condition's
+second horn ((i)∧(ii) ⊢ ⊥) verbatim, for the doc's own named witness. It is
+therefore `[CLOSED-NEG]` — a settled boundary of the theory, do not reopen,
+not a defect. **No open obligation remains for this Direction.** The standing
+B- freeze (no re-rate until O-THERMO-∞ is discharged or refuted) is therefore
+lifted — discharged negatively counts as discharged — and the grade advances
+to **B**. (It is *not* higher: a confirmed-negative is an honest limit, not
+extra positive coverage; and the separate Information-Theory bridge — Theorem
+5, `echo-information-loss` never defined — remains unbuilt, but that is a
+different Direction.)
 
 ### 4. Proof Ecosystem Stability: B+
 
@@ -111,7 +132,7 @@ development" — one named obligation, refutable by exhibiting a total
 | Relational | 80% | B |
 | CNO Integration | 98% | A- |
 | JanusKey Bridge | 90% | B+ |
-| Thermodynamics | 85% | B- |
+| Thermodynamics | 95% | B |
 
 **Proof Quality Indicators:**
 - ✅ All core theorems have constructive proofs

docs/echo-types/MAP.adoc

@@ -58,19 +58,30 @@ remainder of information-losing computation: for `f : A → B`,
 
 == Directions
 
-=== Thermodynamic — Landauer/Bennett energy bounds `[REAL*]`
+=== Thermodynamic — Landauer/Bennett energy bounds `[REAL]`
 Landauer/Bennett bound *shape*; `ThermodynamicallyReversible(p)
 ≙ Echo p σ ≃ Echo id σ`. Zero-cost (Bennett) proved for *every
-injective map* on *any Bishop-finite carrier* (transport along an
-explicit bijection); the identity-at-zero instance is now a corollary.
-Sole residual is the infinite-carrier case, pinned as the falsifiable
-obligation **O-THERMO-∞** (kill condition stated). Re-rated B- / ~85%
-in STABILITY_ANALYSIS §3.3 (was C+ / ~70%, 2026-05-18). Stays `[REAL*]`
-— real, still partial — until O-THERMO-∞ is discharged or refuted.
+injective map* on *any Bishop-finite carrier*, and lifted to an
+*arbitrary carrier with no finiteness at all* (K-free subsingleton /
+occupancy route), certified faithful against the established count and
+instantiated on the genuine *infinite* absolute-zero `Program` CNO —
+"a CNO dissipates zero Landauer energy" is now a real theorem, not the
+historically vacuous claim. The one residual — the *quantitative
+collapse* functional on an infinite carrier, **O-THERMO-∞** — is now
+`[CLOSED-NEG]`: its impossibility is mechanised
+(`collapse-cost-impossible`, the doc's own kill condition discharged
+negatively). No open obligation remains for this Direction; tag
+advanced `[REAL*]` → `[REAL]`. Re-rated B / ~95% in
+STABILITY_ANALYSIS §3.3 (was C+ / ~70% then B- / ~90%, 2026-05-18);
+the standing B- freeze lifted because O-THERMO-∞ is now discharged
+(negatively). The Information-Theory bridge is a *separate* Direction
+(see Shannon entry), not part of this one.
 
 * Proofs: `proofs/agda/EchoThermodynamics.agda`,
   `proofs/agda/EchoFiberCount.agda`,
-  `proofs/agda/EchoThermodynamicsFinite.agda`.
+  `proofs/agda/EchoThermodynamicsFinite.agda`,
+  `proofs/agda/EchoThermodynamicsArbitrary.agda`,
+  `proofs/agda/EchoThermoCollapseImpossible.agda`.
 * Docs: `docs/ECHO-CNO-BRIDGE.adoc` §"Thermodynamic Bridge",
   `docs/STABILITY_ANALYSIS.md` §3.3, `docs/WORK_PLAN.md` §5,
   `docs/adjacency/hott-fibers.adoc`.

proofs/agda/All.agda

@@ -30,6 +30,8 @@ open import Dyadic
 open import DyadicEchoBridge
 open import EchoThermodynamics
 open import EchoThermodynamicsFinite
+open import EchoThermodynamicsArbitrary
+open import EchoThermoCollapseImpossible
 open import EchoStabilityTests
 open import VecRotation
 

proofs/agda/EchoFiberCount.agda

@@ -174,6 +174,42 @@ FiberSize-fin-injective {n = ℕ.suc m} f y _≟_ inj (suc i′) hit
 ... | no  _  = FiberSize-fin-injective (f ∘ suc) y _≟_
                  (λ eq → Fin-suc-inj (inj eq)) i′ hit
 
+----------------------------------------------------------------------
+-- Headline 2c — FiberSize-fin-subsingleton
+--
+-- The fiber-local hypothesis behind the arbitrary-carrier Bennett
+-- result. If the fiber over `y` is a *subsingleton* — any two hitting
+-- indices coincide — and *some* index `i₀` hits, then the count is
+-- exactly 1. This is strictly weaker as a hypothesis than global
+-- injectivity: it only constrains the indices over `y`. Indeed
+-- `FiberSize-fin-injective` is the corollary obtained by feeding
+-- `ss i j fi fj = inj (trans fi (sym fj))` (kept as-is upstream for
+-- pin stability; this lemma is the honest generalisation).
+--
+-- The proof walks the `FiberSize-fin` recursion in lock-step with the
+-- witness exactly as the injective version does, but discharges the
+-- "no other hit" obligation from subsingleton-ness rather than from
+-- injectivity.
+----------------------------------------------------------------------
+
+FiberSize-fin-subsingleton :
+  ∀ {b} {B : Set b} {n : ℕ}
+  (f : Fin n → B) (y : B) (_≟_ : (y₁ y₂ : B) → Dec (y₁ ≡ y₂))
+  (ss : (i j : Fin n) → f i ≡ y → f j ≡ y → i ≡ j)
+  (i₀ : Fin n) → f i₀ ≡ y →
+  FiberSize-fin f y _≟_ ≡ ℕ.suc ℕ.zero
+FiberSize-fin-subsingleton {n = ℕ.suc m} f y _≟_ ss zero hit
+  with f zero ≟ y
+... | yes _  = cong ℕ.suc
+                 (FiberSize-fin-no-hit (f ∘ suc) y _≟_
+                   (λ j fsj≡y → suc≢zero-Fin j (ss (suc j) zero fsj≡y hit)))
+... | no ¬p  = ⊥-elim (¬p hit)
+FiberSize-fin-subsingleton {n = ℕ.suc m} f y _≟_ ss (suc i′) hit
+  with f zero ≟ y
+... | yes p  = ⊥-elim (suc≢zero-Fin i′ (sym (ss zero (suc i′) p hit)))
+... | no  _  = FiberSize-fin-subsingleton (f ∘ suc) y _≟_
+                 (λ i j fi fj → Fin-suc-inj (ss (suc i) (suc j) fi fj)) i′ hit
+
 ----------------------------------------------------------------------
 -- Headline 3 — FiberSize-fin ≡ 0 ⟺ ¬ Echo (split into two halves).
 --