fix(agda): restore main typecheck — carry the fiber invariant in FiberBundle

.github/workflows/actions.lock

@@ -8,14 +8,14 @@ workflows:
         - 'actions/checkout@v7.0.1'
     '.github/workflows/codeql.yml':
         - 'actions/checkout@v7.0.1'
-        - 'github/codeql-action@v4.38.0'
+        - 'github/codeql-action@v4.38.1'
     '.github/workflows/governance.yml': []
     '.github/workflows/hypatia-scan.yml':
         - 'actions/checkout@v7.0.1'
         - 'actions/github-script@v9.0.0'
         - 'actions/upload-artifact@v7.0.1'
         - 'erlef/setup-beam@v1.24.1'
-        - 'github/codeql-action@v4.38.0'
+        - 'github/codeql-action@v4.38.1'
     '.github/workflows/label-triage.yml': []
     '.github/workflows/labels.yml': []
     '.github/workflows/mirror.yml': []
@@ -70,9 +70,9 @@ dependencies:
         commit: 'sha1-54075bcc5e249e4758d363f27d099f55d843f124'
         owner_id: 47606891
         repo_id: 331103973
-    'github/codeql-action@v4.38.0':
-        ref: 'v4.38.0'
-        commit: 'sha1-b96794f015dfd88f77b49b1c93e0fa7110f94c63'
+    'github/codeql-action@v4.38.1':
+        ref: 'v4.38.1'
+        commit: 'sha1-1c5b675653bb5c22dbe9b12b556ec555138e09fd'
         owner_id: 9919
         repo_id: 259445878
     'hyperpolymath/smtp-notify-action@v0.3.0':

docs/echo-types/echo-kernel-note.adoc

@@ -96,7 +96,8 @@ kernel** — the boundary is real and lives outside this core.
   `EchoOFSUnivF5`, `EchoOFSUnivF5Diag`, `EchoOFSUnivF5Iso`,
   `EchoCanonicalIdentitySuite`, `EchoDifferential`, `EchoEntropy`,
   `EchoLLEncoding`, `EchoProbabilisticSupport`, `EchoProvenance`,
-  `EchoSecurity`
+  `EchoSecurity`, `EchoHaplotypeCollapsing`,
+  `EchoBitNarrowingNumeric`, `EchoExampleBitNarrowing`
 | Multi-hop. `EchoThermodynamics` reaches the kernel via
   `EchoFiberCount` (no direct `Echo` import);
   `EchoThermodynamicsFinite` is its Bishop-finite transport layer.

proofs/agda/EchoHaplotypeCollapsing.agda

@@ -44,7 +44,7 @@ open import EchoNoSectionGeneric using (no-section-of-collapsing-map)
 open import Data.Bool.Base using (Bool; true; false)
 open import Data.Nat.Base using (ℕ)
 open import Data.Product.Base using (Σ; _,_; _×_; proj₁; proj₂)
-open import Data.List.Base using (List; []; _∷_; _++_; map; length)
+open import Data.List.Base using (List; []; _∷_; _++_)
 open import Data.Unit.Base using (⊤)
 open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl; cong)
 open import Relation.Nullary using (¬_)
@@ -174,21 +174,32 @@ data PipelineRole : Set where
 record FiberBundle : Set where
   field
     haplotype      : Haplotype
-    representative : Clone
-    fiber          : List Clone
+    representative : HaploFiber haplotype
+    fiber          : List (HaploFiber haplotype)
 
 example-bundle : FiberBundle
 example-bundle = record
   { haplotype = 0
-  ; representative = clone₁
-  ; fiber = example-clones
+  ; representative = echo-clone₁
+  ; fiber = echo-clone₁ ∷ echo-clone₂ ∷ []
   }
 
 bundle-projection : FiberBundle → Haplotype
 bundle-projection = FiberBundle.haplotype
 
+-- Every element of the sidecar IS an echo at the bundle's haplotype, by
+-- construction: the field type *is* the fiber, so no separate soundness
+-- proof is needed.  This mirrors the Nickel contract in
+-- docs/echo-types/applications/haplotype-collapsing.adoc §"Nickel
+-- contracts enforce" — "every `clones[i].haplotype_id == haplotype_id`".
+--
+-- Previously `fiber : List Clone`, which carried no link to `haplotype`;
+-- the claim below was then unprovable (`refl` is not available for an
+-- arbitrary element).  The invariant belongs in the record, not in a
+-- side-condition at the use site — the same layering lesson as the
+-- `region_shrink` falsity in ephapax.
 bundle-fiber-echoes : (b : FiberBundle) → List (HaploFiber (FiberBundle.haplotype b))
-bundle-fiber-echoes b = map (λ c → c , refl) (FiberBundle.fiber b)
+bundle-fiber-echoes b = FiberBundle.fiber b
 
 ------------------------------------------------------------------------
 -- 7. Separation from O(n²) distance matrix