examples/Transport: add transport-echo Gate 3 example + handoff (prior session)

Pre-existing worked Gate 3 example (structured loss under transport +
coarse-graining on ℚ fields over a periodic grid) and its handoff
notes. Complete locally but never committed; recorded here as the
as-found baseline before the gap-closure work in the following commit.
Compiles --safe --without-K, no postulates; two gaps documented in §5.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

docs/gate-3-transport-handoff.adoc

@@ -0,0 +1,116 @@
+= Gate 3 Example: Transport-Echo — Handoff Notes
+:toc: macro
+:sectnums:
+:icons: font
+
+[.lead]
+Worked Gate 3 example: structured loss under transport (explicit-Euler
+diffusion) and coarse-graining (block averaging) on rational-valued
+fields over a periodic grid. Subject file:
+`proofs/agda/examples/Transport.agda`.
+
+*Status:* Gate 3 example, complete with two documented gaps
+(section 5). Compiles `--safe --without-K`, no postulates.
+
+toc::[]
+
+== What this example demonstrates
+
+The example exhibits structured loss from two distinguishable sources
+on `Field n = Vec ℚ n` over a periodic grid. (i) The explicit-Euler
+diffusion step `step` at `λ = ¼` is *singular at the Nyquist mode* on
+even grids: the alternating vector is annihilated. (ii) Block
+averaging `avg` is non-injective (rung 2). (iii) Their composition
+`avg ∘ step` has a kernel that *strictly enlarges* beyond either
+source taken alone. It is a worked instance of `EchoGraded`'s
+base-Echo structure — rung 4's `echoStep-is-Echo` shows the
+transport-echo family is definitionally `Echo (avg …)` — and it
+introduces no new bridge axis.
+
+== Load-bearing theorems
+
+* `step-kernel-nontrivial` — explicit-Euler diffusion at `λ = ¼` on a
+  periodic n-cycle is singular at the Nyquist mode for even `n`:
+  an explicit nonzero field `f` with `step f ≡ 0` at `n = 2`.
+* `step-kernel-contains-nyquist-multiples` — every scalar multiple of
+  the Nyquist mode is annihilated:
+  `∀ c → step (map (c *_) (nyquist 2)) ≡ replicate 4 0ℚ`
+  (containment, at the fixed even size).
+* `compose-kernel-strictly-larger` — the kernel of `avg ∘ step`
+  strictly contains both the step-then-`avg` loss and `ker step`
+  alone. Witness `g6 = [1, -1, -1, 1]` at `n = 4`, block size 2
+  (`step-then-avg = avg {1} {2} ∘ step`): `g6` lies in
+  `ker (avg ∘ step)`, is not a scalar multiple of `nyquist 2`, and
+  has `step g6 ≠ 0`.
+
+== Infrastructure
+
+Factored locally and scoped to this file by design (not promoted to a
+utilities module). Future Vec-valued-field examples may want to
+extract them.
+
+* `step-homog` — `step (map (c *_) v) ≡ map (c *_) (step v)`
+  (ℚ-scalar homogeneity of `step`).
+* `step-additive` — `step (v + w) ≡ step v + step w` (additivity).
+  Together with `step-homog` this is the ℚ-linearity of `step`.
+* `StepKernelSubspace` — record bundling `closed-+` and `closed-*ₗ`;
+  with the `StepKernel` predicate and witness `step-kernel-subspace`,
+  it packages the kernel as a ℚ-subspace.
+
+Eight Vec-over-ℚ lemmas, reusable for future Vec-valued-field work:
+
+[cols="1,3", options="header"]
+|===
+| Lemma | One-line statement
+
+| `zip-interchange`  | `(A+B)+(C+D) ≡ (A+C)+(B+D)` pointwise on vectors
+| `zip-sub-exchange` | `(A+C)-(B+D) ≡ (A-B)+(C-D)` pointwise on vectors
+| `++∷ʳ`             | `zipWith _+_` distributes over snoc `_∷ʳ_`
+| `reverse-zipWith`  | `reverse` distributes over `zipWith _+_`
+| `add-rotL`         | left rotation distributes over `zipWith _+_`
+| `add-rotR`         | right rotation distributes over `zipWith _+_`
+| `scale-+`          | `map (c *_)` distributes over `zipWith _+_`
+| `scale-zero`       | `map (c *_)` annihilates the zero vector
+|===
+
+== Documented gaps
+
+=== (a) `∀ n` generalisation of `nyquist-in-step-kernel`
+
+`nyquist-in-step-kernel-1` and `-2` stand (computed by `refl` at
+`n = 1` and `n = 2`). The general
+`∀ n → step (nyquist n) ≡ replicate (2·n) 0ℚ` is blocked on a
+Vec-rotation fact stdlib does not provide: that
+`rotL (nyquist n) ≡ map -_ (nyquist n)` (and the same for `rotR`) —
+rotation of the alternating vector equals its negation. With that
+lemma the general case closes via `step-homog`. The lane forbade
+postulating it, so the general statement is documented in-file
+rather than asserted.
+
+=== (b) `step-kernel-at-4-is-nyquist-line` (rank-1 characterisation)
+
+Not attempted past the ~150-line threshold. The subspace closures
+(`step-additive`, `step-homog`, `StepKernelSubspace`) establish that
+`ker step` is a ℚ-subspace, but not *which* subspace. Pinning it to
+the Nyquist line at `n = 4` is the rank-1 fact, requiring either a
+symbolic 4×4 ℚ linear solve or a ℚ-linear-algebra module carrying a
+rank-1 characterisation — neither in scope. The containment result
+`step-kernel-contains-nyquist-multiples` stands in its place.
+
+== Why this stays in Gate 3
+
+The example is a concrete worked instance demonstrating existing echo
+machinery on a real domain (rational fields over a periodic grid). It
+introduces no new bridge axis; it does not claim transport and
+coarse-graining are independent decorations producing substantive
+cross-axis content (the EI-2 investigation settled that question
+negatively); and it does not reach toward Gate 2's
+characteristic-theorem-family criteria. The strictly-larger kernel of
+`avg ∘ step` is *structured loss* — two distinguishable annihilation
+sources composing — not bridge-axis interaction.
+
+== Build and verification
+
+`proofs/agda/examples/Transport.agda` compiles under Agda 2.8.0 with
+agda-stdlib v2.3, `--safe --without-K`, no postulates, no
+`{-# TERMINATING #-}` pragmas, no `--rewriting`.