hyperpolymath · Nov 9, 2026 · Nov 9, 2026
@@ -7,6 +7,19 @@ Changelog].
 
 === [Unreleased]
 
+==== Added (2026-11-09)
+
+* _squeakwell / VeriSimDB recovery ladder._ `+EchoPartialSection.agda+`
+(partial sections of a modality bundle; information order; resolve-parametric
+merge with the pointwise R1–R3 twins of verisimdb `+Octad.v+`; guarded fill as
+left-biased merge, inflationary and provably not monotone; restriction to an
+observed mask and its Echo fibre) and `+EchoFibreIntersection.agda+` (binary
+narrowing as the fibre of a pairing, witness-preserving `+Fin n+` steps,
+`+narrow-shrinks+` on `+FiberSize-fin+`). `+EchoTruncation.agda+`, until now
+compiled only through its corollaries, is wired into `+All.agda+` and pinned.
+Rocq recheck: verisimdb `+formal/Recovery.v+`; Lean side: tropical-types
+`+Resource/HubCeiling.lean+`.
+
 ==== Changed (2026-11-06)
 
 * Recorded the owner's prospective licence policy: CC-BY-SA-4.0 for new

@@ -227,6 +227,25 @@ path; citation-level — echo-types proves the general aggregation
 principle (and its macro instance), oikos’s alib will _consume_ it. The
 alib library itself is not yet built (design-note stage; Route A vs B
 pending owner decision).
+|squeakwell / VeriSimDB recovery ladder
+|`+proofs/agda/EchoPartialSection.agda+`, `+EchoFibreIntersection.agda+`,
+`+EchoTruncation.agda+` (wired 2026-11-09)
+|verisimdb `+formal/Recovery.v+` (Rocq recheck of R2/R3/R4/R9/R10 over
+`+Octad.v+`), tropical-types `+Resource/HubCeiling.lean+` (reach grades,
+hub ceilings, weighted residue measure), squeakwell `+docs/ROUTE-PLAN.adoc+`
+|*Theory landed, pointwise.* Partial sections with the resolve-parametric
+merge (the join-semilattice-of-partial-sections abstraction verisimdb’s
+CROSS-REPO-MAP flagged), guarded fill (inflationary, not monotone), the
+restriction fibre (fragment observation fidelity), binary and `+Fin n+`
+narrowing with `+narrow-shrinks+` on the honest count. Checked here with
+Agda 2.7.0.1 and the pinned stdlib / absolute-zero; Recovery.v with Coq
+8.18.0; HubCeiling with Lean 4.35.0.
+|Correspondence is a refinement, not same-statement: Agda proves the merge
+laws pointwise, Rocq as function equalities under
+`+functional_extensionality_dep+`. Termination (nine rounds) is Rocq-only
+(needs the finite octad). The Creusot export/queue postconditions (R11–R13
+engineering half) and the Idris2 wire contracts (R1, R15, R16) are not
+started; see squeakwell `+PROOF-STATUS.adoc+`.
 |===
 
 === Immediate next actions
@@ -347,6 +366,16 @@ to paper over this in the relational model.
 
 === Revision history
 
+* 2026-11-09: *squeakwell / VeriSimDB recovery ladder.* Added
+`+EchoPartialSection.agda+` (partial sections, information order,
+resolve-parametric merge = pointwise R1–R3 twins of verisimdb `+Octad.v+`,
+guarded fill inflationary-not-monotone, restriction fibre) and
+`+EchoFibreIntersection.agda+` (binary / `+Fin n+` narrowing,
+`+narrow-shrinks+`); wired the orphan `+EchoTruncation.agda+` into
+`+All.agda+`. New Tracks row. Rocq recheck lands as verisimdb
+`+formal/Recovery.v+`; Lean side as tropical-types
+`+Resource/HubCeiling.lean+`. `+--safe --without-K --cubical-compatible+`,
+zero postulates, funext-free.
 * 2026-06-18: *EchoAggregation general/macro split.* Generalised
 `+EchoAggregation.agda+` from the macro-economics-specific module into
 the general monoid-aggregation form requested by issue #175 (`+Monoid+`

@@ -512,6 +512,46 @@ Connect echo types with MAA's reversibility proofs
 
 * Docs: `roadmap.adoc` §"Deferred research track", `docs/bridges/EchoJanusBridge.adoc`.
 
+=== Database recovery — squeakwell / VeriSimDB bridge `[REAL]`
+
+The Agda source of truth for the repaired recovery invariants of
+https://github.com/hyperpolymath/squeakwell[squeakwell] (database
+recovery through cross-modal constraint propagation on VeriSimDB; route
+plan rungs R3, R8, R9, R12, R13). Landed 2026-11-09, `--safe --without-K
+--cubical-compatible`, zero postulates, pointwise (funext-free):
+
+* *Partial sections* — `EchoPartialSection.agda`: a VeriSimDB octad is a
+  partial section `(m : M) → Maybe (V m)` of a modality bundle. Information
+  order; `merge resolve` inherits exactly the algebra of `resolve`
+  (`merge-comm` / `merge-assoc` / `merge-idem`, the pointwise twins of
+  verisimdb `Octad.v` R1–R3 — implications, not CRDT laws); guarded fill
+  is the left-biased merge against an oracle proposal, never overwrites
+  (`fill-guarded`), is inflationary (`fill-inflationary`) and is NOT
+  monotone (`fill-not-monotone`, two-modality counter-model); restriction
+  to an observed mask and its Echo fibre (`restrict-fibre-agree`,
+  `restrict-blind`) — the fragment-granularity observation-fidelity shape.
+* *Multi-witness narrowing* — `EchoFibreIntersection.agda`: the fibre of a
+  pairing is the intersection of fibres over one witness
+  (`fibre-intersection-iso`); forgetting or adding a constraint keeps the
+  witness; `narrow-shrinks`: the `EchoFiberCount` count never grows when
+  an observation is added.
+* *Truncation wired* — `EchoTruncation.agda` is now in `All.agda` and
+  pinned (`echo-not-prop`); with `FiberSize-fin≡0⇒no-echo` /
+  `no-echo⇒FiberSize-fin≡0` it is the review-queue completeness kernel.
+
+Not claimed: inhabitation of the narrowed fibre; covering masks ⇒
+subsingleton (needs extensionality over opaque identifiers; dropped);
+termination of the recovery round (finite index set and a conflict test —
+proved in Rocq as `iter_9_fixpoint` in verisimdb `formal/Recovery.v`, not
+restated over an arbitrary `M`). Lean side (reach grades, hub ceilings,
+weighted residue measure): tropical-types `Resource/HubCeiling.lean`.
+Ledger of grades per rung: squeakwell `PROOF-STATUS.adoc`.
+
+* Proofs: `proofs/agda/EchoPartialSection.agda`,
+  `proofs/agda/EchoFibreIntersection.agda`, `proofs/agda/EchoTruncation.agda`.
+* Cross-repo: verisimdb `formal/Recovery.v` + `formal/CROSS-REPO-MAP.adoc`;
+  tropical-types `Resource/HubCeiling.lean`; squeakwell `docs/ROUTE-PLAN.adoc`.
+
 === Shannon / information theory `[REAL*]`
 Partial. The *discrete non-distinguishing* form lands as
 `EchoEntropy.agda` — the fibre-count shadow (uniform-prior Shannon

@@ -226,6 +226,18 @@ kernel** — the boundary is real and lives outside this core.
   flat `Echo*.agda` glob that Check B lints; recorded here for
   discoverability. Not kernel (the kernel remains exactly `Echo`).
 
+| *Derived — recovery ladder (2026-11-09)*
+| `EchoPartialSection` (Tier 1), `EchoFibreIntersection` (Tier 2)
+| squeakwell / VeriSimDB recovery bridge. `EchoPartialSection` imports only
+  `Echo` and stdlib: partial sections of a modality bundle, the information
+  order, the resolve-parametric merge (pointwise R1–R3 twins of verisimdb
+  `Octad.v`), guarded fill as left-biased merge (inflationary, not
+  monotone) and the restriction fibre. `EchoFibreIntersection` imports
+  `Echo` and `EchoFiberCount`: binary narrowing as the fibre of a pairing,
+  witness-preserving constraint steps, and `narrow-shrinks` on the honest
+  count. Both funext-free; Rocq recheck in verisimdb `formal/Recovery.v`.
+  `EchoTruncation` (Tier 1, already classified) is now wired into `All.agda`.
+
 | *Derived — Tier 1 additions (2026-11-06)*
 | `EchoSourcePreserving`, `EchoDependentPushforward`
 | Each imports only `Echo` and stdlib. The former proves the source-preserving

@@ -50,6 +50,12 @@ open import EchoSearchInstance
 open import EchoSearchExample
 open import EchoAccess
 open import EchoFiberCount
+-- squeakwell recovery ladder (2026-11-09): wires the once-orphan truncation
+-- lemma, multi-witness narrowing (R8) and partial sections / guarded fill /
+-- restriction fibre (R3, R9, R12). Rocq recheck: verisimdb formal/Recovery.v.
+open import EchoTruncation
+open import EchoFibreIntersection
+open import EchoPartialSection
 open import EchoEpistemicResidue
 open import EchoRelational
 open import EchoCategorical

@@ -0,0 +1,230 @@
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+
+-- EchoFibreIntersection: multi-witness narrowing (squeakwell rung R8).
+--
+-- A recovery engine that has observed several modalities of one entity
+-- asks for the witnesses satisfying ALL the observations at once. In
+-- Echo terms that is the intersection of fibres over one shared
+-- witness: `Σ A (λ x → f x ≡ y × g x ≡ z)`. This module pins the three
+-- facts hyperpolymath/squeakwell's proof ladder (docs/ROUTE-PLAN.adoc,
+-- rung R8) needs about that intersection:
+--
+--   * Binary narrowing is a fibre.  Intersecting the fibres of `f` at
+--     `y` and of `g` at `z` IS the fibre of the pairing `< f , g >` at
+--     `(y , z)`: `fibre-intersection-iso`, a K-free `_↔_` with `refl`
+--     round-trips (no funext — the equations are on pairs, not on
+--     functions).
+--   * Narrowing never changes the witness.  Forgetting either
+--     constraint is witness-preserving (`forget-left-witness`,
+--     `forget-right-witness`), and adding one more constraint to a
+--     family of `n` constraints is again witness-preserving in both
+--     directions (`narrow-fin-step-to`, `narrow-fin-step-from`). The
+--     `Fin n` family form is stated with pointwise equations, so it
+--     needs no funext; it is NOT packaged as a `_↔_` because the
+--     round-trip on the function side would.
+--   * Narrowing shrinks the candidate fibre.  On a finite domain with
+--     decidable equality, the honest count of `EchoFiberCount` can
+--     only go down when a constraint is added: `narrow-shrinks`
+--     (`FiberSize-fin < f , g > (y , z) ≤ FiberSize-fin f y`). This is
+--     the quantitative statement behind squeakwell's review queue:
+--     every extra observed modality narrows the candidates.
+--
+-- Honest scope. The survey's proposed "covering masks ⇒ subsingleton
+-- fibre" is NOT here: over an opaque value type two full sections that
+-- agree on every modality need not be equal without extensionality, and
+-- squeakwell's identifiers are opaque. The route plan dropped it; so
+-- does this module. Nothing here claims the intersection is inhabited:
+-- observations can be jointly unsatisfiable, and the count can be 0.
+--
+-- Headlines (pinned in Smoke.agda):
+--
+--   * fibre-intersection-iso   -- Echo < f , g > (y , z) ↔ Narrow f g y z
+--   * forget-left-witness      -- forgetting a constraint keeps the witness
+--   * forget-right-witness
+--   * narrow-fin-step-to       -- Fin (suc n) family = one more binary step
+--   * narrow-fin-step-from
+--   * narrow-shrinks           -- FiberSize-fin of the pairing ≤ FiberSize-fin of f
+
+module EchoFibreIntersection where
+
+open import Function.Base                         using (_∘_)
+open import Level                                 using (Level; _⊔_)
+open import Data.Empty                            using (⊥; ⊥-elim)
+import      Data.Nat.Base                         as ℕ
+open        ℕ                                     using (ℕ; _≤_; z≤n; s≤s)
+open import Data.Fin.Base                         using (Fin; zero; suc)
+open import Data.Product.Base                     using (Σ; _×_; _,_; proj₁; proj₂; <_,_>)
+open import Function.Bundles                      using (_↔_; mk↔ₛ′)
+open import Relation.Nullary.Decidable.Core       using (Dec; yes; no)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; cong₂)
+
+open import Echo                                  using (Echo)
+open import EchoFiberCount                        using (FiberSize-fin)
+
+private
+  variable
+    ℓa ℓb ℓc : Level
+    A : Set ℓa
+    B : Set ℓb
+    C : Set ℓc
+
+----------------------------------------------------------------------
+-- Binary narrowing: two constraints on one witness.
+----------------------------------------------------------------------
+
+-- The witnesses `x` with `f x ≡ y` AND `g x ≡ z`: the intersection of
+-- the two fibres over a shared witness.
+Narrow : (f : A → B) (g : A → C) → B → C → Set _
+Narrow {A = A} f g y z = Σ A (λ x → (f x ≡ y) × (g x ≡ z))
+
+pair-fibre→narrow :
+  {f : A → B} {g : A → C} {y : B} {z : C} →
+  Echo < f , g > (y , z) → Narrow f g y z
+pair-fibre→narrow (x , p) = x , cong proj₁ p , cong proj₂ p
+
+narrow→pair-fibre :
+  {f : A → B} {g : A → C} {y : B} {z : C} →
+  Narrow f g y z → Echo < f , g > (y , z)
+narrow→pair-fibre (x , p , q) = x , cong₂ _,_ p q
+
+-- Round trips. Both close by matching the equation on `refl`; the
+-- indices `y`, `z` are variables, so this is `--without-K`-safe.
+narrow-to-from :
+  {f : A → B} {g : A → C} {y : B} {z : C} →
+  (e : Echo < f , g > (y , z)) →
+  narrow→pair-fibre {f = f} {g = g} (pair-fibre→narrow e) ≡ e
+narrow-to-from (x , refl) = refl
+
+narrow-from-to :
+  {f : A → B} {g : A → C} {y : B} {z : C} →
+  (w : Narrow f g y z) →
+  pair-fibre→narrow {f = f} {g = g} (narrow→pair-fibre w) ≡ w
+narrow-from-to (x , refl , refl) = refl
+
+-- Headline 1: binary narrowing IS the fibre of the pairing.
+fibre-intersection-iso :
+  (f : A → B) (g : A → C) (y : B) (z : C) →
+  Echo < f , g > (y , z) ↔ Narrow f g y z
+fibre-intersection-iso f g y z =
+  mk↔ₛ′ pair-fibre→narrow narrow→pair-fibre
+        (narrow-from-to {f = f} {g = g}) (narrow-to-from {f = f} {g = g})
+
+----------------------------------------------------------------------
+-- Forgetting a constraint keeps the witness.
+----------------------------------------------------------------------
+
+forget-left :
+  {f : A → B} {g : A → C} {y : B} {z : C} → Narrow f g y z → Echo g z
+forget-left (x , _ , q) = x , q
+
+forget-right :
+  {f : A → B} {g : A → C} {y : B} {z : C} → Narrow f g y z → Echo f y
+forget-right (x , p , _) = x , p
+
+-- Headline 2: narrowing is a refinement of the SAME candidate, never a
+-- different one. Both are definitional.
+forget-left-witness :
+  {f : A → B} {g : A → C} {y : B} {z : C} (w : Narrow f g y z) →
+  proj₁ (forget-left {f = f} w) ≡ proj₁ w
+forget-left-witness _ = refl
+
+forget-right-witness :
+  {f : A → B} {g : A → C} {y : B} {z : C} (w : Narrow f g y z) →
+  proj₁ (forget-right {g = g} w) ≡ proj₁ w
+forget-right-witness _ = refl
+
+----------------------------------------------------------------------
+-- Families of constraints indexed by `Fin n`.
+----------------------------------------------------------------------
+
+-- `n` observations `fs i x ≡ ys i` on one witness `x`, stated pointwise
+-- (no function equality, hence no funext).
+NarrowFin : ∀ {n} (fs : Fin n → A → B) (ys : Fin n → B) → Set _
+NarrowFin {A = A} fs ys = Σ A (λ x → ∀ i → fs i x ≡ ys i)
+
+-- Headline 3: a family of `suc n` constraints is one binary narrowing
+-- step on top of a family of `n`, in both directions, and the witness
+-- is untouched (both maps are `refl` on `proj₁`).
+narrow-fin-step-to :
+  ∀ {n} (fs : Fin (ℕ.suc n) → A → B) (ys : Fin (ℕ.suc n) → B) →
+  NarrowFin fs ys →
+  Σ A (λ x → (fs zero x ≡ ys zero) × (∀ i → fs (suc i) x ≡ ys (suc i)))
+narrow-fin-step-to fs ys (x , h) = x , h zero , (λ i → h (suc i))
+
+narrow-fin-step-from :
+  ∀ {n} (fs : Fin (ℕ.suc n) → A → B) (ys : Fin (ℕ.suc n) → B) →
+  Σ A (λ x → (fs zero x ≡ ys zero) × (∀ i → fs (suc i) x ≡ ys (suc i))) →
+  NarrowFin fs ys
+narrow-fin-step-from fs ys (x , p , h) = x , step
+  where
+    step : ∀ i → fs i x ≡ ys i
+    step zero    = p
+    step (suc i) = h i
+
+narrow-fin-step-to-witness :
+  ∀ {n} (fs : Fin (ℕ.suc n) → A → B) (ys : Fin (ℕ.suc n) → B)
+  (w : NarrowFin fs ys) →
+  proj₁ (narrow-fin-step-to fs ys w) ≡ proj₁ w
+narrow-fin-step-to-witness _ _ _ = refl
+
+narrow-fin-step-from-witness :
+  ∀ {n} (fs : Fin (ℕ.suc n) → A → B) (ys : Fin (ℕ.suc n) → B)
+  (w : Σ A (λ x → (fs zero x ≡ ys zero) × (∀ i → fs (suc i) x ≡ ys (suc i)))) →
+  proj₁ (narrow-fin-step-from fs ys w) ≡ proj₁ w
+narrow-fin-step-from-witness _ _ _ = refl
+
+----------------------------------------------------------------------
+-- Narrowing shrinks the honest fibre count.
+----------------------------------------------------------------------
+
+-- Decidable equality on pairs from decidable equality on the components.
+dec-× :
+  ((b₁ b₂ : B) → Dec (b₁ ≡ b₂)) →
+  ((c₁ c₂ : C) → Dec (c₁ ≡ c₂)) →
+  (p q : B × C) → Dec (p ≡ q)
+dec-× _≟B_ _≟C_ (b , c) (b′ , c′) with b ≟B b′ | c ≟C c′
+... | yes refl | yes refl = yes refl
+... | yes _    | no ¬q    = no (λ e → ¬q (cong proj₂ e))
+... | no ¬p    | yes _    = no (λ e → ¬p (cong proj₁ e))
+... | no ¬p    | no _     = no (λ e → ¬p (cong proj₁ e))
+
+private
+  ≤-step : ∀ {m n} → m ≤ n → m ≤ ℕ.suc n
+  ≤-step z≤n     = z≤n
+  ≤-step (s≤s p) = s≤s (≤-step p)
+
+-- Headline 4: adding an observation never enlarges the enumerated
+-- candidate fibre. Walks the `FiberSize-fin` recursion on both sides in
+-- lock-step: a hit for the pair is a hit for `f`; a hit for `f` alone
+-- is a candidate the extra observation has ruled out.
+narrow-shrinks :
+  ∀ {n} (f : Fin n → B) (g : Fin n → C) (y : B) (z : C)
+  (_≟B_ : (b₁ b₂ : B) → Dec (b₁ ≡ b₂))
+  (_≟C_ : (c₁ c₂ : C) → Dec (c₁ ≡ c₂)) →
+  FiberSize-fin < f , g > (y , z) (dec-× _≟B_ _≟C_) ≤ FiberSize-fin f y _≟B_
+narrow-shrinks {n = ℕ.zero}  f g y z _≟B_ _≟C_ = z≤n
+narrow-shrinks {n = ℕ.suc m} f g y z _≟B_ _≟C_
+  with f zero ≟B y | dec-× _≟B_ _≟C_ (< f , g > zero) (y , z)
+... | yes _  | yes _ = s≤s (narrow-shrinks (f ∘ suc) (g ∘ suc) y z _≟B_ _≟C_)
+... | yes _  | no _  = ≤-step (narrow-shrinks (f ∘ suc) (g ∘ suc) y z _≟B_ _≟C_)
+... | no ¬p  | yes q = ⊥-elim (¬p (cong proj₁ q))
+... | no _   | no _  = narrow-shrinks (f ∘ suc) (g ∘ suc) y z _≟B_ _≟C_
+
+----------------------------------------------------------------------
+-- Companion remark.
+--
+-- What is deliberately NOT claimed:
+--
+--   * Inhabitation. `Narrow f g y z` may be empty; joint observations
+--     can be inconsistent. squeakwell reports that as an empty
+--     candidate fibre, routed to review (rung R13), not as a theorem.
+--   * Covering ⇒ subsingleton. The survey's "if the observed masks
+--     cover every modality the fibre is a subsingleton" needs equality
+--     of full sections from pointwise equality, i.e. extensionality, and
+--     opaque identifiers. Dropped in the route plan; not here.
+--   * A `_↔_` for the `Fin n` family step. The pointwise maps exist and
+--     preserve the witness; the function-side round trip would need
+--     funext and is left out rather than taken as a hypothesis.
+----------------------------------------------------------------------