Skip to content

Commit 758f914

Browse files
hyperpolymathhyperpolymath
authored
Merge branch 'main' into claude/complete-echo-types-pr42-RJGlK
2 parents ffcc3ed + b7f47d2 commit 758f914

5 files changed

Lines changed: 1276 additions & 0 deletions

File tree

‎docs/gate-3-transport-handoff.adoc‎

Lines changed: 134 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,134 @@
1+
= Gate 3 Example: Transport-Echo — Handoff Notes
2+
:toc: macro
3+
:sectnums:
4+
:icons: font
5+
6+
[.lead]
7+
Worked Gate 3 example: structured loss under transport (explicit-Euler
8+
diffusion) and coarse-graining (block averaging) on rational-valued
9+
fields over a periodic grid. Subject file:
10+
`proofs/agda/examples/Transport.agda`.
11+
12+
*Status:* Gate 3 example, complete; both former gaps now *closed*.
13+
5(a) (the `∀ n` generalisation) via the extracted `VecRotation`
14+
module; 5(b) (the rank-1 characterisation at n = 4) via the ℚ ring
15+
solver. Compiles `--safe --without-K`, no postulates.
16+
17+
toc::[]
18+
19+
== What this example demonstrates
20+
21+
The example exhibits structured loss from two distinguishable sources
22+
on `Field n = Vec ℚ n` over a periodic grid. (i) The explicit-Euler
23+
diffusion step `step` at `λ = ¼` is *singular at the Nyquist mode* on
24+
even grids: the alternating vector is annihilated. (ii) Block
25+
averaging `avg` is non-injective (rung 2). (iii) Their composition
26+
`avg ∘ step` has a kernel that *strictly enlarges* beyond either
27+
source taken alone. It is a worked instance of `EchoGraded`'s
28+
base-Echo structure — rung 4's `echoStep-is-Echo` shows the
29+
transport-echo family is definitionally `Echo (avg …)` — and it
30+
introduces no new bridge axis.
31+
32+
== Load-bearing theorems
33+
34+
* `step-kernel-nontrivial` — explicit-Euler diffusion at `λ = ¼` on a
35+
periodic n-cycle is singular at the Nyquist mode for even `n`:
36+
an explicit nonzero field `f` with `step f ≡ 0` at `n = 2`.
37+
* `step-kernel-contains-nyquist-multiples` — every scalar multiple of
38+
the Nyquist mode is annihilated:
39+
`∀ c → step (map (c *_) (nyquist 2)) ≡ replicate 4 0ℚ`
40+
(containment, at the fixed even size).
41+
* `nyquist-in-step-kernel` — the `∀ n` form:
42+
`∀ n → step (nyquist n) ≡ replicate (2·n) 0ℚ` (closes former gap
43+
(a), via the extracted `VecRotation` module).
44+
* `step-kernel-at-4-is-nyquist-line` — the rank-1 converse at n = 4:
45+
`step f ≡ 0 → Σ[ c ] f ≡ map (c *_) (nyquist 2)` (closes former
46+
gap (b), 4×4 ℚ solve via the ring solver).
47+
* `compose-kernel-strictly-larger` — the kernel of `avg ∘ step`
48+
strictly contains both the step-then-`avg` loss and `ker step`
49+
alone. Witness `g6 = [1, -1, -1, 1]` at `n = 4`, block size 2
50+
(`step-then-avg = avg {1} {2} ∘ step`): `g6` lies in
51+
`ker (avg ∘ step)`, is not a scalar multiple of `nyquist 2`, and
52+
has `step g6 ≠ 0`.
53+
54+
== Infrastructure
55+
56+
The `step`-specific algebra below stays local to this file. The one
57+
genuinely reusable Vec-rotation fact has been *extracted* to the
58+
top-level `VecRotation` module (polymorphic over any carrier with an
59+
involutive negation): `rotL-alternating` / `rotR-alternating`, plus
60+
the `map-alternating` corollary. That module is what closes gap (a).
61+
62+
* `step-homog` — `step (map (c *_) v) ≡ map (c *_) (step v)`
63+
(ℚ-scalar homogeneity of `step`).
64+
* `step-additive` — `step (v + w) ≡ step v + step w` (additivity).
65+
Together with `step-homog` this is the ℚ-linearity of `step`.
66+
* `StepKernelSubspace` — record bundling `closed-+` and `closed-*ₗ`;
67+
with the `StepKernel` predicate and witness `step-kernel-subspace`,
68+
it packages the kernel as a ℚ-subspace.
69+
70+
Eight Vec-over-ℚ lemmas, reusable for future Vec-valued-field work:
71+
72+
[cols="1,3", options="header"]
73+
|===
74+
| Lemma | One-line statement
75+
76+
| `zip-interchange` | `(A+B)+(C+D) ≡ (A+C)+(B+D)` pointwise on vectors
77+
| `zip-sub-exchange` | `(A+C)-(B+D) ≡ (A-B)+(C-D)` pointwise on vectors
78+
| `++∷ʳ` | `zipWith _+_` distributes over snoc `_∷ʳ_`
79+
| `reverse-zipWith` | `reverse` distributes over `zipWith _+_`
80+
| `add-rotL` | left rotation distributes over `zipWith _+_`
81+
| `add-rotR` | right rotation distributes over `zipWith _+_`
82+
| `scale-+` | `map (c *_)` distributes over `zipWith _+_`
83+
| `scale-zero` | `map (c *_)` annihilates the zero vector
84+
|===
85+
86+
== Former gaps (both closed)
87+
88+
=== (a) `∀ n` generalisation of `nyquist-in-step-kernel` — CLOSED
89+
90+
The general `nyquist-in-step-kernel : ∀ n → step (nyquist n) ≡
91+
replicate (2·n) 0ℚ` now lands (no postulate, no size restriction).
92+
The Vec-rotation fact stdlib does not provide —
93+
`rotL (nyquist n) ≡ map -_ (nyquist n)`, and the `rotR` twin —
94+
was extracted to the `VecRotation` module as the polymorphic
95+
`rotL-alternating` / `rotR-alternating` (each requiring an
96+
involution hypothesis, discharged for ℚ by the ring solver). The
97+
in-file wiring (Rung 5a (closed)) bridges `step`'s local rotations
98+
to the module, lifts the per-entry Nyquist eigenvalue-0 identity
99+
pointwise, and transports across the `vcast ∘ concat ∘ replicate`
100+
builder. `nyquist-in-step-kernel-1` / `-2` are retained as fast
101+
`refl` sanity checks at the smallest sizes.
102+
103+
=== (b) `step-kernel-at-4-is-nyquist-line` (rank-1 characterisation) — CLOSED
104+
105+
`step-kernel-at-4-is-nyquist-line : ∀ (f : Field 4) → step f ≡
106+
replicate 4 0ℚ → Σ[ c ∈ ℚ ] f ≡ map (c *_) (nyquist 2)` now lands.
107+
The subspace closures (`step-additive`, `step-homog`,
108+
`StepKernelSubspace`) establish that `ker step` is a ℚ-subspace; this
109+
pins *which* subspace — the Nyquist line. The rank-1 fact is the 4×4
110+
ℚ system `step [a,b,c,d] ≡ 0`, whose only solution is
111+
`[a,−a,a,−a] = a·(nyquist 2)`. It is discharged with the stdlib ℚ
112+
ring solver (`Data.Rational.Solver`): constant folding does the
113+
linear algebra (4·¼ = 1, ½·2 = 1), so no cancellation lemma, nonzero
114+
side condition, or matrix module is needed. The containment result
115+
`step-kernel-contains-nyquist-multiples` remains as the easy
116+
direction.
117+
118+
== Why this stays in Gate 3
119+
120+
The example is a concrete worked instance demonstrating existing echo
121+
machinery on a real domain (rational fields over a periodic grid). It
122+
introduces no new bridge axis; it does not claim transport and
123+
coarse-graining are independent decorations producing substantive
124+
cross-axis content (the EI-2 investigation settled that question
125+
negatively); and it does not reach toward Gate 2's
126+
characteristic-theorem-family criteria. The strictly-larger kernel of
127+
`avg ∘ step` is *structured loss* — two distinguishable annihilation
128+
sources composing — not bridge-axis interaction.
129+
130+
== Build and verification
131+
132+
`proofs/agda/examples/Transport.agda` compiles under Agda 2.8.0 with
133+
agda-stdlib v2.3, `--safe --without-K`, no postulates, no
134+
`{-# TERMINATING #-}` pragmas, no `--rewriting`.

‎proofs/agda/All.agda‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -29,6 +29,7 @@ open import Dyadic
2929
open import DyadicEchoBridge
3030
open import EchoThermodynamics
3131
open import EchoStabilityTests
32+
open import VecRotation
3233

3334
open import Ordinal.Base
3435
open import Ordinal.Closure

‎proofs/agda/Smoke.agda‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -35,6 +35,7 @@ open import Echo using
3535
open import EchoCharacteristic using (collapse; echo-true; echo-false; echo-true≢echo-false)
3636
open import EchoResidue using (EchoR; collapse-to-residue; strict-weakening-collapse; no-section-collapse-to-residue)
3737
open import EchoExamples using (square9; visible; quot; collapse-residue-identifies)
38+
open import VecRotation using (rotL-alternating; rotR-alternating; map-alternating)
3839

3940
open import EchoApprox using
4041
( Tolerance

‎proofs/agda/VecRotation.agda‎

Lines changed: 136 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,136 @@
1+
{-# OPTIONS --safe --without-K #-}
2+
3+
------------------------------------------------------------------------
4+
-- Vec-rotation infrastructure.
5+
--
6+
-- One cyclic-rotation fact about the alternating (sign-flipping)
7+
-- vector, factored out of `examples/Transport.agda` where it blocked
8+
-- the `∀ n` generalisation of `nyquist-in-step-kernel`. Polymorphic
9+
-- over any carrier with an involutive "negation"; the ℚ Nyquist mode
10+
-- is the intended instance (`-_` is involutive via
11+
-- `Data.Rational.Properties.neg-involutive`).
12+
--
13+
-- `rotL`/`rotR` are reproduced verbatim from `examples/Transport.agda`
14+
-- (stdlib carries no cyclic rotation), so the lemma is drop-in for the
15+
-- consumer. Scope is deliberately one lemma plus its `map` corollary;
16+
-- this is not a general rotation theory.
17+
--
18+
-- Note on the statement. The minimally honest signature carries an
19+
-- explicit involution hypothesis `neg (neg x) ≡ x`: rotating an
20+
-- *even*-length alternating vector by one equals its pointwise
21+
-- negation, and the equality genuinely needs `neg² = id` (it fails
22+
-- pointwise otherwise). The `2 * n` length is what makes the
23+
-- alternation parity-stable; the builder mirrors Transport's
24+
-- `concat ∘ replicate` 2-block construction exactly.
25+
------------------------------------------------------------------------
26+
27+
module VecRotation where
28+
29+
open import Data.Nat.Base using (ℕ; zero; suc; _*_)
30+
open import Data.Vec.Base
31+
using (Vec; []; _∷_; _++_; map; concat; replicate; _∷ʳ_; reverse)
32+
open import Data.Vec.Properties
33+
using (reverse-∷; reverse-involutive)
34+
open import Relation.Binary.PropositionalEquality
35+
using (_≡_; refl; sym; trans; cong)
36+
37+
private
38+
variable
39+
A : Set
40+
41+
-- Cyclic rotations (verbatim from examples/Transport.agda).
42+
rotL : ∀ {n} → Vec A n → Vec A n
43+
rotL [] = []
44+
rotL (x ∷ xs) = xs ∷ʳ x
45+
46+
rotR : ∀ {n} → Vec A n → Vec A n
47+
rotR xs = reverse (rotL (reverse xs))
48+
49+
-- The alternating vector [a, neg a, a, neg a, …] of length 2·n,
50+
-- built from n copies of the 2-block (the shape of Transport's
51+
-- `nyquist`, modulo its outer `*-comm` `vcast`).
52+
alternating : (A → A) → (n : ℕ) → A → Vec A (n * 2)
53+
alternating neg n a = concat (replicate n (a ∷ neg a ∷ []))
54+
55+
-- One-step unfolding. Definitional: the 2-block keeps `a` fixed, so
56+
-- there is no parity flip to track here.
57+
alt-cons : ∀ (neg : A → A) n a →
58+
alternating neg (suc n) a ≡ a ∷ neg a ∷ alternating neg n a
59+
alt-cons neg n a = refl
60+
61+
-- `map neg` walks the alternation forward by one block. No involution
62+
-- needed; the consumer's homogeneity step uses this corollary.
63+
map-alternating : ∀ (neg : A → A) n a →
64+
map neg (alternating neg n a) ≡ alternating neg n (neg a)
65+
map-alternating neg zero a = refl
66+
map-alternating neg (suc n) a =
67+
cong (λ z → neg a ∷ neg (neg a) ∷ z) (map-alternating neg n a)
68+
69+
-- Snoc/cons reshuffle: appending `a` at the tail of an alternating
70+
-- vector equals consing `a` onto its pointwise negation. This is the
71+
-- single inductive step the rotation lemma turns on; the involution
72+
-- enters here (and only here).
73+
alt-snoc : ∀ (neg : A → A) (inv : ∀ x → neg (neg x) ≡ x) n a →
74+
alternating neg n a ∷ʳ a ≡ a ∷ map neg (alternating neg n a)
75+
alt-snoc neg inv zero a = refl
76+
alt-snoc neg inv (suc n) a =
77+
cong (λ z → a ∷ neg a ∷ z)
78+
(trans (alt-snoc neg inv n a)
79+
(cong (_∷ map neg (alternating neg n a)) (sym (inv a))))
80+
81+
-- Headline: left-rotating the (even-length) alternating vector equals
82+
-- negating it. This is exactly the Vec-rotation fact stdlib does not
83+
-- provide and that `examples/Transport.agda` documents as the blocker
84+
-- for `∀ n → step (nyquist n) ≡ 0`.
85+
rotL-alternating : ∀ (neg : A → A) (inv : ∀ x → neg (neg x) ≡ x) n a →
86+
rotL (alternating neg n a) ≡ map neg (alternating neg n a)
87+
rotL-alternating neg inv zero a = refl
88+
rotL-alternating neg inv (suc n) a =
89+
cong (neg a ∷_)
90+
(trans (alt-snoc neg inv n a)
91+
(cong (_∷ map neg (alternating neg n a)) (sym (inv a))))
92+
93+
------------------------------------------------------------------------
94+
-- rotR variant.
95+
--
96+
-- `rotR` is `step`'s other rotation, so the consumer needs it too.
97+
-- Rather than re-run the inductive argument through `reverse`'s
98+
-- double-snoc (which has no clean stdlib support), `rotR` is recovered
99+
-- as the inverse of `rotL`: `rotR ∘ rotL ≡ id` reduces, via the
100+
-- one derived helper `reverse-∷ʳ` (dual of stdlib `reverse-∷`), to
101+
-- `reverse-involutive`. `rotR-alternating` then reuses the landed
102+
-- `rotL-alternating` with no new induction over the alternation.
103+
104+
-- Dual of stdlib `reverse-∷`: snoc-then-reverse is reverse-then-cons.
105+
reverse-∷ʳ : ∀ x {n} (xs : Vec A n) → reverse (xs ∷ʳ x) ≡ x ∷ reverse xs
106+
reverse-∷ʳ x xs =
107+
trans (cong reverse
108+
(sym (trans (reverse-∷ x (reverse xs))
109+
(cong (_∷ʳ x) (reverse-involutive xs)))))
110+
(reverse-involutive (x ∷ reverse xs))
111+
112+
-- `rotR` undoes `rotL`.
113+
rotR-rotL : ∀ {n} (v : Vec A n) → rotR (rotL v) ≡ v
114+
rotR-rotL [] = refl
115+
rotR-rotL (x ∷ xs) =
116+
trans (cong (λ z → reverse (rotL z)) (reverse-∷ʳ x xs))
117+
(trans (reverse-∷ʳ x (reverse xs))
118+
(cong (x ∷_) (reverse-involutive xs)))
119+
120+
-- One step of the rotation, the right-handed way: `rotR` of the
121+
-- block-shifted alternation recovers the original.
122+
rotR-alternating-shift : ∀ (neg : A → A) (inv : ∀ x → neg (neg x) ≡ x)
123+
n a → rotR (alternating neg n (neg a)) ≡ alternating neg n a
124+
rotR-alternating-shift neg inv n a =
125+
trans (cong rotR
126+
(sym (trans (rotL-alternating neg inv n a)
127+
(map-alternating neg n a))))
128+
(rotR-rotL (alternating neg n a))
129+
130+
-- Headline (rotR twin of `rotL-alternating`).
131+
rotR-alternating : ∀ (neg : A → A) (inv : ∀ x → neg (neg x) ≡ x) n a →
132+
rotR (alternating neg n a) ≡ map neg (alternating neg n a)
133+
rotR-alternating neg inv n a =
134+
trans (cong rotR (cong (alternating neg n) (sym (inv a))))
135+
(trans (rotR-alternating-shift neg inv n (neg a))
136+
(sym (map-alternating neg n a)))

0 commit comments

Comments
 (0)