Section 13.3: Bessel rows and the linear-side energy

This file was automatically generated by Claude.

Formalization of blueprint Section 13, "Fixed modes, the linear side, and hereditary representatives" (sec:modes), subsection 3, "Bessel rows and the linear-side energy" (lines 2046-2122) of blueprint/formalization_blueprint.tex.

Separated mode rows (lem:mode-rows, blueprint lines 2049-2059)

theorem TrilinearHT.Auto.cell_cross_pair_le (α β γ : ℝ) {a r θ : ℝ} (hr : 0 < r) (hθ : 0 < θ) {x₀ : ℝ} (hx₀ : x₀ ∈ Set.Icc a (a + r)) (hlarge : θ ≤ |2 * α * x₀ + β|) (hvar : 2 * |α| * r ≤ θ / 2) : r⁻¹ * ‖∫ (x : ℝ) in Set.Icc a (a + r), fourierWave 1 (α * x ^ 2 + β * x + γ)‖ ≤ 8 / (θ * r)

Blueprint lines 2054-2055: a quadratic phase difference whose derivative 2αx + β exceeds θ at one point of a cell [a, a + r], with slope variation 2|α| r ≤ θ/2, has normalized oscillatory integral at most 8/(θ r) on the cell.

theorem TrilinearHT.Auto.sum_norm_le_sqrt_card_mul {ν : Type u_1} (N : Finset ν) (γ : ν → ℂ) : ∑ n ∈ N, ‖γ n‖ ≤ √↑N.card * √(∑ n ∈ N, ‖γ n‖ ^ 2)

Σ ‖γ_n‖ ≤ √|N| (Σ ‖γ_n‖²)^{1/2}.

theorem TrilinearHT.Auto.mode_combination_cross_le {μ : Type u_2} {μ' : Type u_3} (M : Finset μ) (M' : Finset μ') (β : μ → ℂ) (β' : μ' → ℂ) (x : μ → μ' → ℂ) {ε L : ℝ} (hεL : 0 ≤ ε * L) (hx : ∀ m ∈ M, ∀ m' ∈ M', ‖x m m'‖ ≤ ε * L) : ‖∑ m ∈ M, ∑ m' ∈ M', β m * β' m' * x m m'‖ ≤ ε * L * (√↑M.card * √(∑ m ∈ M, ‖β m‖ ^ 2)) * (√↑M'.card * √(∑ m' ∈ M', ‖β' m'‖ ^ 2))

Blueprint line 2058: two finite mode combinations with pairwise normalized inner products at most ε on an overlap of length L pair to at most ε L √|M| √|M'| b b'.

theorem TrilinearHT.Auto.almost_orthogonal_synthesis_error {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {κ : Type u_2} (s : Finset κ) (v : κ → H) (b ℓ : κ → ℝ) (w : κ → κ → ℝ) {D η : ℝ} (hη : 0 ≤ η) (hD : 0 ≤ D) (hw0 : ∀ (e e' : κ), 0 ≤ w e e') (hws : ∀ (e e' : κ), w e e' = w e' e) (hcross : ∀ e ∈ s, ∀ e' ∈ s, e ≠ e' → ‖inner ℂ (v e) (v e')‖ ≤ η * w e e' * b e * b e') (hmult : ∀ e ∈ s, ∑ e' ∈ s, w e e' ≤ D * ℓ e) (hdiag : ∀ e ∈ s, ℓ e * b e ^ 2 ≤ D ^ 2 * ‖v e‖ ^ 2) : |‖∑ e ∈ s, v e‖ ^ 2 - ∑ e ∈ s, ‖v e‖ ^ 2| ≤ η * D ^ 3 * ∑ e ∈ s, ‖v e‖ ^ 2

Symmetric overlap and diagonal bounds control the absolute synthesis energy error. The upper and lower almost-orthogonality estimates are its two order consequences.

theorem TrilinearHT.Auto.almost_orthogonal_synthesis {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {κ : Type u_2} (s : Finset κ) (v : κ → H) (b ℓ : κ → ℝ) (w : κ → κ → ℝ) {D η : ℝ} (hη : 0 ≤ η) (hD : 0 ≤ D) (hw0 : ∀ (e e' : κ), 0 ≤ w e e') (hws : ∀ (e e' : κ), w e e' = w e' e) (hcross : ∀ e ∈ s, ∀ e' ∈ s, e ≠ e' → ‖inner ℂ (v e) (v e')‖ ≤ η * w e e' * b e * b e') (hmult : ∀ e ∈ s, ∑ e' ∈ s, w e e' ≤ D * ℓ e) (hdiag : ∀ e ∈ s, ℓ e * b e ^ 2 ≤ D ^ 2 * ‖v e‖ ^ 2) : ‖∑ e ∈ s, v e‖ ^ 2 ≤ (1 + η * D ^ 3) * ∑ e ∈ s, ‖v e‖ ^ 2

Blueprint lines 2057-2058: almost-orthogonal synthesis. If |⟨f_e, f_f⟩| ≤ η w_{ef} b_e b_f for e ≠ f, with symmetric overlaps w of multiplicity Σ_f w_{ef} ≤ D ℓ_e and diagonal control ℓ_e b_e² ≤ D² ‖f_e‖², then ‖Σ f_e‖² ≤ (1 + η D³) Σ ‖f_e‖².

theorem TrilinearHT.Auto.rows_bessel_of_synthesis {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {κ : Type u_2} (s : Finset κ) (g : κ → H) (F : H) {C : ℝ} (hC : 0 ≤ C) (hproj : ∀ e ∈ s, RCLike.re (inner ℂ (g e) F) = ‖g e‖ ^ 2) (hsyn : ‖∑ e ∈ s, g e‖ ^ 2 ≤ C * ∑ e ∈ s, ‖g e‖ ^ 2) : ∑ e ∈ s, ‖g e‖ ^ 2 ≤ C * ‖F‖ ^ 2

Blueprint line 2057 ("by duality"): row outputs g_e = P_e F of orthogonal projections satisfy Re⟨g_e, F⟩ = ‖g_e‖², so a synthesis bound ‖Σ g_e‖² ≤ C Σ ‖g_e‖² gives Σ ‖g_e‖² ≤ C ‖F‖².

theorem TrilinearHT.Auto.separated_projection_rows {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {κ : Type u_2} (s : Finset κ) (g : κ → H) (F : H) (b ℓ : κ → ℝ) (w : κ → κ → ℝ) {D η : ℝ} (hη : 0 ≤ η) (hD : 0 ≤ D) (hproj : ∀ e ∈ s, RCLike.re (inner ℂ (g e) F) = ‖g e‖ ^ 2) (hw0 : ∀ (e e' : κ), 0 ≤ w e e') (hws : ∀ (e e' : κ), w e e' = w e' e) (hcross : ∀ e ∈ s, ∀ e' ∈ s, e ≠ e' → ‖inner ℂ (g e) (g e')‖ ≤ η * w e e' * b e * b e') (hmult : ∀ e ∈ s, ∑ e' ∈ s, w e e' ≤ D * ℓ e) (hdiag : ∀ e ∈ s, ℓ e * b e ^ 2 ≤ D ^ 2 * ‖g e‖ ^ 2) : ∑ e ∈ s, ‖g e‖ ^ 2 ≤ (1 + η * D ^ 3) * ‖F‖ ^ 2

Blueprint lem:mode-rows (lines 2049-2059), assembled: projection-row outputs g_e = P_e F on cells of lengths ℓ_e with coefficient norms b_e, with cross pairings at most η w_{ef} b_e b_f (η = D_*^{-199} from cell_cross_pair_le, fourier_sum_tail_le, mode_combination_cross_le), overlap multiplicity D_* and private-coordinate diagonal control, satisfy Σ ‖P_e F‖² ≤ (1 + η D_*³) ‖F‖².

Composition with the main histories (lem:lift-composition, blueprint lines 2062-2077)

The linear-side energy (prop:linear-side, blueprint lines 2080-2120)

theorem TrilinearHT.Auto.frac_le_harmonic_sub {a b : ℕ} (hab : a ≤ b) : ↑(b - a) / ↑b ≤ ↑(harmonic b) - ↑(harmonic a)

(b - a)/b ≤ H_b - H_a for harmonic numbers.

theorem TrilinearHT.Auto.sum_frac_le_harmonic {α : Type u_1} [DecidableEq α] (S : ℕ → Finset α) (hS : Monotone S) (hS0 : S 0 = ∅) (X : ℕ → Finset α) (hX : ∀ (j : ℕ), X j ⊆ S j) (n A : ℕ) (hA : ∀ (x : α), {j ∈ Finset.range n | x ∈ X (j + 1)}.card ≤ A) : ∑ j ∈ Finset.range n, ↑(X (j + 1)).card / ↑(S (j + 1)).card ≤ ↑A * ↑(harmonic (S n).card)

Blueprint lines 2093-2094 (elementary fact): if nonempty sets S_j increase from S_0 = ∅, X_j ⊆ S_j, and each label belongs to at most A of the X_j, then Σ_j |X_j|/|S_j| ≤ A H_{|S_n|}; enumerate labels by first entry.

theorem TrilinearHT.Auto.sum_frac_le_log {α : Type u_1} [DecidableEq α] (S : ℕ → Finset α) (hS : Monotone S) (hS0 : S 0 = ∅) (X : ℕ → Finset α) (hX : ∀ (j : ℕ), X j ⊆ S j) (n A M : ℕ) (hA : ∀ (x : α), {j ∈ Finset.range n | x ∈ X (j + 1)}.card ≤ A) (hM : (S n).card ≤ M) : ∑ j ∈ Finset.range n, ↑(X (j + 1)).card / ↑(S (j + 1)).card ≤ ↑A * (1 + Real.log ↑M)

Corollary: Σ_j |X_j|/|S_j| ≤ A (1 + log M) when |S_n| ≤ M.

theorem TrilinearHT.Auto.sum_log_shift_le {p : ℕ → ℝ} {M : ℝ} (hp1 : ∀ (h : ℕ), 1 ≤ p h) (hpM : ∀ (h : ℕ), p h ≤ M) (Δ n : ℕ) : ∑ h ∈ Finset.range n, (Real.log (p (h + Δ)) - Real.log (p h)) ≤ ↑Δ * Real.log M

Blueprint line 2091, first term: for 1 ≤ p_h ≤ M the shifted logarithmic increments Σ_{h<n} log(p_{h+Δ}/p_h) sum to at most Δ log M.

theorem TrilinearHT.Auto.sum_log_chain_le {a c : ℕ → ℝ} (ha : ∀ (i : ℕ), 0 < a i) (hac : ∀ (i : ℕ), a i ≤ c i) (hca : ∀ (i : ℕ), c i ≤ a (i + 1)) (N : ℕ) : ∑ i ∈ Finset.range N, (Real.log (c i) - Real.log (a i)) ≤ Real.log (a N) - Real.log (a 0)

Blueprint line 2091, second term: along a chain P_i ⊆ C_i ⊆ P_{i+1} of positive sizes, Σ_i log(|C_i|/|P_i|) ≤ log |P_N| - log |P_0|.

theorem TrilinearHT.Auto.LiftData.norm_op_le {Pr : Type u_1} {Md : Type u_2} [Fintype Pr] [Fintype Md] [DecidableEq Pr] (L : LiftData Pr Md) (F : ↥(ColumnL2 Pr)) : ‖L.op F‖ ≤ √5 * ‖F‖

theorem TrilinearHT.Auto.fourierWave_one_mul (x y : ℝ) : fourierWave 1 x * fourierWave 1 y = fourierWave 1 (x + y)

theorem TrilinearHT.Auto.expanded_pair_le {κ : Type u_1} (S : Finset κ) (c : κ → ℂ) (ν : κ → ℝ) (Z : ℝ → ℂ) {a r Θ τ : ℝ} (hr : 0 < r) (hΘ : 0 < Θ) (hZm : Measurable Z) (hZb : ∀ (y : ℝ), ‖Z y‖ ≤ 1) (hZ : ∀ y ∈ Set.Icc a (a + r), ‖Z y - ∑ k ∈ S, c k * fourierWave 1 (ν k * y)‖ ≤ τ) (α β γ : ℝ) (hlarge : ∀ k ∈ S, ∃ x₀ ∈ Set.Icc a (a + r), Θ ≤ |2 * α * x₀ + (β + ν k)|) (hvar : 2 * |α| * r ≤ Θ / 2) : r⁻¹ * ‖∫ (y : ℝ) in Set.Icc a (a + r), Z y * fourierWave 1 (α * y ^ 2 + β * y + γ)‖ ≤ (∑ k ∈ S, ‖c k‖) * (8 / (Θ * r)) + τ

Blueprint lines 2054-2056: a quadratic oscillation e(αy² + βy + γ) against an amplitude Z that is, on the cell [a, a + r], a finite Fourier sum Σ c_k e(ν_k y) up to τ: if every shifted derivative 2αx + β + ν_k exceeds Θ at some point of the cell and the slope varies by at most Θ/2, the normalized pairing is at most (Σ |c_k|) 8/(Θ r) + τ.

theorem TrilinearHT.Auto.modeWave_mul_conj (z : ChartTag) (δ : ℝ) (ρ : Fin z.dim → ℝ) (cl : ℤ) (lam a γ lam' a' γ' y : ℝ) : modeWave z δ ρ cl lam a γ y * (starRingEnd ℂ) (modeWave z δ ρ cl lam' a' γ' y) = (gaugeSq δ ρ fun (i : Fin z.dim) => z.θ i * y) * fourierWave 1 ((lam - lam') * y ^ 2 + (2 * lam' * a' - 2 * lam * a + γ - γ') * y + (lam * a ^ 2 - γ * a - lam' * a' ^ 2 + γ' * a'))

The pointwise pairing of two modes of one role and group: the common gauge cancels.

theorem TrilinearHT.Auto.modeWave_pair_le_full (z : ChartTag) {δ : ℝ} (hδ : 0 < δ) (ρ : Fin z.dim → ℝ) (cl : ℤ) (lam a γ lam' a' γ' : ℝ) {a₀ r Θ : ℝ} (hr : 0 < r) (hΘ : 0 < Θ) {Q0 : ℕ} (hQ0 : 0 < Q0) (Kf : ℕ) {E0 : ℝ} (hbox : ↑Q0 * 2 ^ (Kf + 1) ≤ E0) (hsep : ∀ (n : Fin z.dim → ℤ), (∀ (i : Fin z.dim), |↑(n i)| ≤ E0) → ∃ x ∈ Set.Icc a₀ (a₀ + r), Θ ≤ |2 * lam * (x - a) + γ - (2 * lam' * (x - a') + γ') + ∑ i : Fin z.dim, ↑(n i) * (z.θ i / ↑Q0)|) (hvar : 2 * |lam - lam'| * r ≤ Θ / 2) : r⁻¹ * ‖∫ (y : ℝ) in Set.Icc a₀ (a₀ + r), modeWave z δ ρ cl lam a γ y * (starRingEnd ℂ) (modeWave z δ ρ cl lam' a' γ' y)‖ ≤ gaugeSqNorm z.dim δ * (8 / (Θ * r)) + 2 * gaugeTail z.dim δ / 2 ^ Kf

Blueprint lines 2054-2056 with the full Fourier norm of the squared gauge ("expand (ζ^ρ)² with coefficient sum at most D_* and tail D_*^{-300}; the Fourier sum and tail give C D_*/Ξ + D_*^{-300}"): under the hypotheses of modeWave_pair_le, the normalized pairing is at most gaugeSqNorm · 8/(Θ r) + 2 B_ζ/2^K.

Separated mode rows from mode Gram bounds (lem:mode-rows, blueprint lines 2049-2059)

theorem TrilinearHT.Auto.mode_projection_rows {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {κ : Type u_2} {μ : Type u_3} (s : Finset κ) (M : κ → Finset μ) (Ψ : κ → μ → H) [∀ (e : κ), (Submodule.span ℂ (Ψ e '' ↑(M e))).HasOrthogonalProjection] (F : H) (ℓ : κ → ℝ) (w : κ → κ → ℝ) {η ε D : ℝ} (hη : 0 ≤ η) (hε : 0 < ε) (hD : 0 ≤ D) (hw0 : ∀ (e e' : κ), 0 ≤ w e e') (hws : ∀ (e e' : κ), w e e' = w e' e) (hcross : ∀ e ∈ s, ∀ e' ∈ s, e ≠ e' → ∀ m ∈ M e, ∀ m' ∈ M e', ‖inner ℂ (Ψ e m) (Ψ e' m')‖ ≤ η * w e e') (hpriv : ∀ e ∈ s, ∀ (β : μ → ℂ), ε * ℓ e * ∑ m ∈ M e, ‖β m‖ ^ 2 ≤ ‖∑ m ∈ M e, β m • Ψ e m‖ ^ 2) (hmult : ∀ e ∈ s, ∑ e' ∈ s, w e e' ≤ D * ℓ e) (hcard : ∀ e ∈ s, ↑(M e).card ≤ ε * D ^ 2) : ∑ e ∈ s, ‖(Submodule.span ℂ (Ψ e '' ↑(M e))).starProjection F‖ ^ 2 ≤ (1 + η * D ^ 3) * ‖F‖ ^ 2

Blueprint lem:mode-rows from mode-level data: rows e project onto the spans of their augmented modes Ψ e m, m ∈ M_e. If modes of distinct rows have pairings at most η w_{ef} (cross pairs on overlapping cells), the private coordinates give ε ℓ_e Σ|β_m|² ≤ ‖Σ β_m Ψ e m‖², the overlaps have multiplicity Σ_f w_{ef} ≤ D ℓ_e, and |M_e| ≤ ε D², then Σ_e ‖P_e F‖² ≤ (1 + η D³) ‖F‖².

theorem TrilinearHT.Auto.inner_augMode {V : Type u_1} [Fintype V] [DecidableEq V] (J J' : Set ℝ) (ψ ψ' : ℝ → ℂ) (ε ε' : ℝ) (m m' : V) (y : ℝ) : inner ℂ (augMode J ψ ε m y) (augMode J' ψ' ε' m' y) = (J ∩ J').indicator (fun (y : ℝ) => (starRingEnd ℂ) (ψ y) * ψ' y + if m = m' then ↑(√ε * √ε') else 0) y

Pointwise pairing of two augmented modes: physical product plus private overlap.

theorem TrilinearHT.Auto.augMode_sum_norm_sq_ge {V : Type u_1} [Fintype V] [DecidableEq V] (J : Set ℝ) (ψ : V → ℝ → ℂ) (εw : V → ℝ) (M : Finset V) (β : V → ℂ) (y : ℝ) {ε : ℝ} (hε : ∀ m ∈ M, ε ≤ εw m) (hε0 : 0 ≤ ε) : J.indicator (fun (x : ℝ) => ε * ∑ m ∈ M, ‖β m‖ ^ 2) y ≤ ‖∑ m ∈ M, β m • augMode J (ψ m) (εw m) m y‖ ^ 2

The private coordinates of a combination of augmented modes on one cell.

theorem TrilinearHT.Auto.aug_mode_rows {V : Type u_1} [Fintype V] [DecidableEq V] {κ : Type u_2} (s : Finset κ) (J : κ → Set ℝ) (hJ : ∀ (e : κ), MeasurableSet (J e)) (hJf : ∀ (e : κ), MeasureTheory.volume (J e) ≠ ⊤) (M : κ → Finset V) (ψ : V → ℝ → ℂ) (hψ : ∀ (m : V), Measurable (ψ m)) (hψb : ∀ (m : V) (y : ℝ), ‖ψ m y‖ ≤ 1) (εw : V → ℝ) {η ε D : ℝ} (hη : 0 ≤ η) (hε : 0 < ε) (hD : 0 ≤ D) (hεw : ∀ e ∈ s, ∀ m ∈ M e, ε ≤ εw m) (hdisj : ∀ e ∈ s, ∀ e' ∈ s, e ≠ e' → ∀ m ∈ M e, m ∈ M e' → MeasureTheory.volume (J e ∩ J e') = 0) (hpair : ∀ e ∈ s, ∀ e' ∈ s, e ≠ e' → ∀ m ∈ M e, ∀ m' ∈ M e', ‖∫ (y : ℝ) in J e ∩ J e', (starRingEnd ℂ) (ψ m y) * ψ m' y‖ ≤ η * MeasureTheory.volume.real (J e ∩ J e')) (hmult : ∀ e ∈ s, ∑ e' ∈ s, MeasureTheory.volume.real (J e ∩ J e') ≤ D * MeasureTheory.volume.real (J e)) (hcard : ∀ e ∈ s, ↑(M e).card ≤ ε * D ^ 2) [∀ (e : κ), (Submodule.span ℂ ((fun (m : V) => MeasureTheory.MemLp.toLp (augMode (J e) (ψ m) (εw m) m) ⋯) '' ↑(M e))).HasOrthogonalProjection] (F : ↥(ColumnL2 V)) : ∑ e ∈ s, ‖(Submodule.span ℂ ((fun (m : V) => MeasureTheory.MemLp.toLp (augMode (J e) (ψ m) (εw m) m) ⋯) '' ↑(M e))).starProjection F‖ ^ 2 ≤ (1 + η * D ^ 3) * ‖F‖ ^ 2

Blueprint lem:mode-rows for augmented modes 1_{J_e}(ψ_m e_phys + √ε_m e_m): rows e on cells J_e with mode sets M_e that share no mode on overlapping cells, physical cross pairings |∫_{J_e ∩ J_f} ψBar_m ψ_{m'}| ≤ η |J_e ∩ J_f|, overlap multiplicity D, private weights at least ε and |M_e| ≤ ε D² give Σ_e ‖P_e F‖² ≤ (1 + η D³) ‖F‖².

Bad incidences along a linked chain of side events (eq:bad-density, lines 2088-2102)

theorem TrilinearHT.Auto.one_le_ten_log_of_ratio {x y : ℝ} (hy : 0 < y) (h : 10 * y < 9 * x) : 1 ≤ 10 * (Real.log x - Real.log y)

theorem TrilinearHT.Auto.chain_bad_count {α : Type u_1} [DecidableEq α] (N J Δ M Ae Ah : ℕ) (P C Xe Xh : ℕ → ℕ → Finset α) (hPne : ∀ (i h : ℕ), (P i h).Nonempty) (hPC : ∀ (i h : ℕ), P i h ⊆ C i h) (hCP : ∀ (i h : ℕ), C i h ⊆ P (i + 1) h) (hPm : ∀ (i : ℕ), Monotone (P i)) (hCm : ∀ (i : ℕ), Monotone (C i)) (hM : ∀ (i h : ℕ), (C i h).card ≤ M) (hXe : ∀ (i h : ℕ), Xe i h ⊆ C i h) (hXh : ∀ (i h : ℕ), Xh i h ⊆ C i h) (hAe : ∀ (h : ℕ) (x : α), {i ∈ Finset.range N | x ∈ Xe i h}.card ≤ Ae) (hAh : ∀ (i : ℕ) (x : α), {h ∈ Finset.range (J + 1) | x ∈ Xh i h}.card ≤ Ah) (bad : ℕ → ℕ → Prop) [(i h : ℕ) → Decidable (bad i h)] (hbad : ∀ (i h : ℕ), bad i h → h < Δ ∨ 10 * (P i (h - Δ)).card < 9 * (C i h).card ∨ (C i h).card < 10 * ((Xe i h).card + (Xh i h).card)) : ↑{p ∈ Finset.range N ×ˢ Finset.range (J + 1) | bad p.1 p.2}.card ≤ ↑N * ↑Δ + 10 * (↑N * ↑Δ * Real.log ↑M + (↑J + 1) * Real.log ↑M) + 10 * (((↑J + 1) * ↑Ae + ↑N * ↑Ah) * (1 + Real.log ↑M))

Blueprint lines 2088-2099: along a linked chain of N events, with predecessor and component label sets P_{i,h} ⊆ C_{i,h} ⊆ P_{i+1,h} increasing in the height and of size at most M, and bad-primary sets X^e_{i,h} (exceptional; each label in at most A_e events at a height) and X^h_{i,h} (height-bad; each label at most A_h heights at an event), the number of bad incidences — h < Δ, a failed predecessor-density test 10|P_{i,h-Δ}| < 9|C_{i,h}|, or more than a tenth of bad primaries — is at most NΔ + 10(NΔ log M + (J+1) log M) + 10((J+1)A_e + N A_h)(1 + log M).

Longest-chain levels (blueprint line 2104)

def TrilinearHT.Auto.LinkedChain {κ : Type u_1} (s : Set κ) (R : κ → κ → Prop) (k : ℕ) (e : κ) : Prop

A linked chain with k links in s ending at e.

Equations

• TrilinearHT.Auto.LinkedChain s R k e = ∃ (c : Fin (k + 1) → κ), (∀ (j : Fin (k + 1)), c j ∈ s) ∧ (∀ (j : Fin k), R (c j.castSucc) (c j.succ)) ∧ c (Fin.last k) = e

noncomputable def TrilinearHT.Auto.chainLevel {κ : Type u_1} (s : Set κ) (R : κ → κ → Prop) (L : ℕ) (e : κ) : ℕ

The longest-chain level of an event, among chains with at most L links.

Equations

• TrilinearHT.Auto.chainLevel s R L e = Nat.findGreatest (fun (x : ℕ) => TrilinearHT.Auto.LinkedChain s R x e) L

theorem TrilinearHT.Auto.linkedChain_zero {κ : Type u_1} (s : Set κ) (R : κ → κ → Prop) {e : κ} (he : e ∈ s) : LinkedChain s R 0 e

theorem TrilinearHT.Auto.linkedChain_extend {κ : Type u_1} (s : Set κ) (R : κ → κ → Prop) {k : ℕ} {e e' : κ} (h : LinkedChain s R k e) (he' : e' ∈ s) (hR : R e e') : LinkedChain s R (k + 1) e'

theorem TrilinearHT.Auto.chainLevel_le {κ : Type u_1} (s : Set κ) (R : κ → κ → Prop) (L : ℕ) (e : κ) : chainLevel s R L e ≤ L

theorem TrilinearHT.Auto.linkedChain_chainLevel {κ : Type u_1} (s : Set κ) (R : κ → κ → Prop) {L : ℕ} {e : κ} (he : e ∈ s) : LinkedChain s R (chainLevel s R L e) e

theorem TrilinearHT.Auto.chainLevel_lt {κ : Type u_1} (s : Set κ) (R : κ → κ → Prop) {L : ℕ} (hL : ∀ (k : ℕ) (e : κ), LinkedChain s R k e → k ≤ L) {e e' : κ} (he : e ∈ s) (he' : e' ∈ s) (hR : R e e') : chainLevel s R L e < chainLevel s R L e'

Linked events have strictly increasing levels when all chains have at most L links; hence events of one level are never linked.

noncomputable def TrilinearHT.Auto.pairConst (d : ℕ) (δ Ξ : ℝ) (Kf : ℕ) : ℝ

The pairing constant η = ‖(ζ^ρ)²‖_A · 8/Ξ + 2 B_ζ/2^K of modeWave_pair_le_full at threshold Ξ / r on a cell of length r (blueprint line 2055: C D_*/Ξ + D_*^{-300}).

Equations

• TrilinearHT.Auto.pairConst d δ Ξ Kf = TrilinearHT.Auto.gaugeSqNorm d δ * (8 / Ξ) + 2 * TrilinearHT.Auto.gaugeTail d δ / 2 ^ Kf

theorem TrilinearHT.Auto.pairConst_nonneg (d : ℕ) {δ Ξ : ℝ} (hδ : 0 < δ) (hΞ : 0 < Ξ) (Kf : ℕ) : 0 ≤ pairConst d δ Ξ Kf

theorem TrilinearHT.Auto.modeWave_rows {V : Type u_1} {κ : Type u_2} [Fintype V] [DecidableEq V] (z : ChartTag) {δ : ℝ} (hδ : 0 < δ) (ρ : Fin z.dim → ℝ) (cl : ℤ) (lam a γ εw : V → ℝ) (s : Finset κ) (J : κ → Set ℝ) (hJ : ∀ (e : κ), MeasurableSet (J e)) (hJf : ∀ (e : κ), MeasureTheory.volume (J e) ≠ ⊤) (M : κ → Finset V) {Ξ ε D : ℝ} (hΞ : 0 < Ξ) (hε : 0 < ε) (hD : 0 ≤ D) {Q0 : ℕ} (hQ0 : 0 < Q0) (Kf : ℕ) {E0 : ℝ} (hbox : ↑Q0 * 2 ^ (Kf + 1) ≤ E0) (hεw : ∀ e ∈ s, ∀ m ∈ M e, ε ≤ εw m) (hdisj : ∀ e ∈ s, ∀ e' ∈ s, e ≠ e' → ∀ m ∈ M e, m ∈ M e' → MeasureTheory.volume (J e ∩ J e') = 0) (hgeom : ∀ e ∈ s, ∀ e' ∈ s, e ≠ e' → MeasureTheory.volume (J e ∩ J e') ≠ 0 → ∃ (a' : ℝ) (r' : ℝ), 0 < r' ∧ J e ∩ J e' = Set.Ico a' (a' + r') ∧ ∀ m ∈ M e, ∀ m' ∈ M e', (∀ (n : Fin z.dim → ℤ), (∀ (i : Fin z.dim), |↑(n i)| ≤ E0) → ∃ x ∈ Set.Icc a' (a' + r'), Ξ / r' ≤ |2 * lam m * (x - a m) + γ m - (2 * lam m' * (x - a m') + γ m') + ∑ i : Fin z.dim, ↑(n i) * (z.θ i / ↑Q0)|) ∧ 2 * |lam m - lam m'| * r' ≤ Ξ / r' / 2) (hmult : ∀ e ∈ s, ∑ e' ∈ s, MeasureTheory.volume.real (J e ∩ J e') ≤ D * MeasureTheory.volume.real (J e)) (hcard : ∀ e ∈ s, ↑(M e).card ≤ ε * D ^ 2) [∀ (e : κ), (Submodule.span ℂ ((fun (m : V) => MeasureTheory.MemLp.toLp (augMode (J e) (modeWave z δ ρ cl (lam m) (a m) (γ m)) (εw m) m) ⋯) '' ↑(M e))).HasOrthogonalProjection] (F : ↥(ColumnL2 V)) : ∑ e ∈ s, ‖(Submodule.span ℂ ((fun (m : V) => MeasureTheory.MemLp.toLp (augMode (J e) (modeWave z δ ρ cl (lam m) (a m) (γ m)) (εw m) m) ⋯) '' ↑(M e))).starProjection F‖ ^ 2 ≤ (1 + pairConst z.dim δ Ξ Kf * D ^ 3) * ‖F‖ ^ 2

Blueprint lem:mode-rows for the modes ψ_m of one role, group and offset (eq:modes): rows e on cells J_e with mode sets M_e sharing no mode on overlapping cells, such that on the common (smaller) cell [a', a' + r') every pair of their modes is non-adjacent at height zero with threshold Ξ/r' and has slope variation at most Ξ/(2r'), and with point multiplicity D (Σ_f |J_e ∩ J_f| ≤ D |J_e|), satisfy Σ_e ‖P_e F‖² ≤ (1 + η D³) ‖F‖² with η = pairConst.

Exact subtotals versus row projections (blueprint lines 2112-2116)

theorem TrilinearHT.Auto.proj_complement_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {μ : Type u_2} (E A : Finset μ) (Ψ : μ → H) [(Submodule.span ℂ (Ψ '' ↑E)).HasOrthogonalProjection] (β : μ → ℂ) {η L ε ℓ : ℝ} (hηL : 0 ≤ η * L) (hεℓ : 0 < ε * ℓ) (hpair : ∀ m ∈ E, ∀ m' ∈ A, ‖inner ℂ (Ψ m) (Ψ m')‖ ≤ η * L) (hpriv : ∀ (c : μ → ℂ), ε * ℓ * ∑ m ∈ E, ‖c m‖ ^ 2 ≤ ‖∑ m ∈ E, c m • Ψ m‖ ^ 2) : ‖(Submodule.span ℂ (Ψ '' ↑E)).starProjection (∑ m' ∈ A, β m' • Ψ m')‖ ≤ η * L * (√↑E.card * (√↑A.card * √(∑ m' ∈ A, ‖β m'‖ ^ 2))) / √(ε * ℓ)

Blueprint lines 2112-2113: the projection onto the span of the modes Ψ m, m ∈ E, of a combination of complementary modes w = Σ_{m' ∈ A} β_{m'} Ψ m' with pairings at most η L is at most η L √|E| √|A| ‖β‖ / √(ε ℓ), when the private coordinates give ε ℓ Σ|c|² ≤ ‖Σ c_m Ψ m‖² on E.

theorem TrilinearHT.Auto.subtotals_synthesis_bounds {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {μ : Type u_2} {ι : Type u_3} (s : Finset ι) (E : ι → Finset μ) (Ψ : μ → H) (β : μ → ℂ) {η L ε D : ℝ} (hη : 0 ≤ η) (hL : 0 ≤ L) (hε : 0 < ε) (hpair : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → ∀ m ∈ E i, ∀ m' ∈ E j, ‖inner ℂ (Ψ m) (Ψ m')‖ ≤ η * L) (hpriv : ∀ i ∈ s, ε * L * ∑ m ∈ E i, ‖β m‖ ^ 2 ≤ ‖∑ m ∈ E i, β m • Ψ m‖ ^ 2) (hcard : ∀ i ∈ s, ↑(E i).card ≤ ε * D ^ 2) : ∃ (b : ι → ℝ), (∀ i ∈ s, ∀ j ∈ s, i ≠ j → ‖inner ℂ (∑ m ∈ E i, β m • Ψ m) (∑ m ∈ E j, β m • Ψ m)‖ ≤ η * L * b i * b j) ∧ ∀ i ∈ s, L * b i ^ 2 ≤ D ^ 2 * ‖∑ m ∈ E i, β m • Ψ m‖ ^ 2

Shared coefficient sizes give cross-pairing and diagonal bounds for finite subtotals.

theorem TrilinearHT.Auto.subtotals_almost_orthogonal {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {μ : Type u_2} {ι : Type u_3} (s : Finset ι) (E : ι → Finset μ) (Ψ : μ → H) (β : μ → ℂ) {η L ε D : ℝ} (hη : 0 ≤ η) (hL : 0 ≤ L) (hε : 0 < ε) (hD : 0 ≤ D) (hpair : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → ∀ m ∈ E i, ∀ m' ∈ E j, ‖inner ℂ (Ψ m) (Ψ m')‖ ≤ η * L) (hpriv : ∀ i ∈ s, ε * L * ∑ m ∈ E i, ‖β m‖ ^ 2 ≤ ‖∑ m ∈ E i, β m • Ψ m‖ ^ 2) (hnum : ↑s.card ≤ D) (hcard : ∀ i ∈ s, ↑(E i).card ≤ ε * D ^ 2) : ‖∑ i ∈ s, ∑ m ∈ E i, β m • Ψ m‖ ^ 2 ≤ (1 + η * D ^ 3) * ∑ i ∈ s, ‖∑ m ∈ E i, β m • Ψ m‖ ^ 2

Blueprint line 2116: on one cell the subtotals T_j = Σ_{m ∈ E_j} β_m Ψ m over disjoint components with mutual pairings at most η L are almost orthogonal: ‖Σ_j T_j‖² ≤ (1 + η D³) Σ_j ‖T_j‖² when the number of components is at most D, the private coordinates give ε L Σ|β|² ≤ ‖T_j‖² and |E_j| ≤ ε D².

Locality of mode rows (blueprint lines 2068-2069)

theorem TrilinearHT.Auto.augMode_toLp_vanish {V : Type u_1} [Fintype V] [DecidableEq V] {J : Set ℝ} (hJ : MeasurableSet J) (hJf : MeasureTheory.volume J ≠ ⊤) {ψ : ℝ → ℂ} (hψ : Measurable ψ) (hψb : ∀ (y : ℝ), ‖ψ y‖ ≤ 1) (ε : ℝ) (m : V) : ∀ᵐ (y : ℝ), y ∉ J → ↑↑(MeasureTheory.MemLp.toLp (augMode J ψ ε m) ⋯) y = 0

theorem TrilinearHT.Auto.LiftData.op_restrict {Pr : Type u_1} {Md : Type u_2} [Fintype Pr] [Fintype Md] [DecidableEq Pr] (L : LiftData Pr Md) (s : Set ℝ) (hs : MeasurableSet s) (F : ↥(ColumnL2 Pr)) : L.op ((columnL2Restriction s hs) F) = (columnL2Restriction s hs) (L.op F)

The mode lift is pointwise, hence commutes with restrictions.

theorem TrilinearHT.Auto.ModeSchedule.current_sub_later_pre (S : ModeSchedule) (hA : 6 ≤ S.A0) {Mode : Type u_1} {Mode' : Type u_2} {P : Type u_3} {P' : Type u_4} [Fintype Mode] [DecidableEq Mode] [DecidableEq P] [Fintype Mode'] [DecidableEq Mode'] [DecidableEq P'] {dz : ℕ} (ω : Mode → ℝ → ℝ) (ω' : Mode' → ℝ → ℝ) (ϑ : Fin dz → ℝ) (π : Mode → P) (π' : Mode' → P') (f : Mode → Mode') {a rv rt a' rv' rt' : ℝ} (hrt : S.Ξ / rv ≤ S.Ξ / rt) (hrt' : S.Ξ / rv' ≤ S.Ξ / rt') (hω : ∀ (m : Mode), ∀ y ∈ Set.Icc a' (a' + rv'), ω' (f m) y = ω m y) (hsub : Set.Icc a' (a' + rv') ⊆ Set.Icc a (a + rv)) (hth : S.Ξ / rt ≤ S.Ξ / rv') (h : ℕ) {x x' : Mode} (hx : x' ∈ (S.preCurrent hA ω ϑ π a rv rt hrt).F h x) : f x' ∈ (S.preCurrent hA ω' ϑ π' a' rv' rt' hrt').E h (f x)

Blueprint lines 2084-2086: CURRENT components on an earlier pre-cell are contained in PRE components on a later pre-cell inside it, once the later PRE threshold Ξ/r_v' is at least the earlier CURRENT threshold Ξ/r_t (block starts at least 3K apart). Modes are transported by f (inclusion of the earlier frozen list into the later one) with unchanged slopes.

Subtotals of a synthesized output (blueprint lines 2112-2118)

theorem TrilinearHT.Auto.projection_subtotal_close {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {μ : Type u_2} [DecidableEq μ] (E A : Finset μ) (hEA : E ⊆ A) (Ψ : μ → H) [(Submodule.span ℂ (Ψ '' ↑E)).HasOrthogonalProjection] (c : μ → ℂ) {η L ε ℓ : ℝ} (hηL : 0 ≤ η * L) (hεℓ : 0 < ε * ℓ) (hpair : ∀ m ∈ E, ∀ m' ∈ A \ E, ‖inner ℂ (Ψ m) (Ψ m')‖ ≤ η * L) (hpriv : ∀ (c : μ → ℂ), ε * ℓ * ∑ m ∈ E, ‖c m‖ ^ 2 ≤ ‖∑ m ∈ E, c m • Ψ m‖ ^ 2) : ‖(Submodule.span ℂ (Ψ '' ↑E)).starProjection (∑ m ∈ A, c m • Ψ m) - ∑ m ∈ E, c m • Ψ m‖ ≤ η * L * (√↑E.card * (√↑(A \ E).card * √(∑ m' ∈ A \ E, ‖c m'‖ ^ 2))) / √(ε * ℓ)

Blueprint lines 2112-2113: the row projection of a synthesized output Σ_{m ∈ A} c_m Ψ m onto the modes E ⊆ A differs from the exact subtotal Σ_{m ∈ E} c_m Ψ m by at most the complementary pairing bound.

theorem TrilinearHT.Auto.inner_augMode_toLp {V : Type u_1} [Fintype V] [DecidableEq V] {J J' : Set ℝ} (hJ : MeasurableSet J) (hJf : MeasureTheory.volume J ≠ ⊤) (hJ' : MeasurableSet J') (hJf' : MeasureTheory.volume J' ≠ ⊤) {ψ ψ' : ℝ → ℂ} (hψ : Measurable ψ) (hψb : ∀ (y : ℝ), ‖ψ y‖ ≤ 1) (hψ' : Measurable ψ') (hψb' : ∀ (y : ℝ), ‖ψ' y‖ ≤ 1) (ε ε' : ℝ) (m m' : V) : inner ℂ (MeasureTheory.MemLp.toLp (augMode J ψ ε m) ⋯) (MeasureTheory.MemLp.toLp (augMode J' ψ' ε' m') ⋯) = ∫ (y : ℝ) in J ∩ J', (starRingEnd ℂ) (ψ y) * ψ' y + if m = m' then ↑(√ε * √ε') else 0

The L² pairing of two augmented modes.

theorem TrilinearHT.Auto.inner_augMode_toLp_ne {V : Type u_1} [Fintype V] [DecidableEq V] {J : Set ℝ} (hJ : MeasurableSet J) (hJf : MeasureTheory.volume J ≠ ⊤) {ψ ψ' : ℝ → ℂ} (hψ : Measurable ψ) (hψb : ∀ (y : ℝ), ‖ψ y‖ ≤ 1) (hψ' : Measurable ψ') (hψb' : ∀ (y : ℝ), ‖ψ' y‖ ≤ 1) (ε ε' : ℝ) {m m' : V} (hmm : m ≠ m') : inner ℂ (MeasureTheory.MemLp.toLp (augMode J ψ ε m) ⋯) (MeasureTheory.MemLp.toLp (augMode J ψ' ε' m') ⋯) = ∫ (y : ℝ) in J, (starRingEnd ℂ) (ψ y) * ψ' y

Distinct augmented modes on one cell pair through their physical parts only.

theorem TrilinearHT.Auto.augMode_toLp_sum_norm_sq_ge {V : Type u_1} [Fintype V] [DecidableEq V] {J : Set ℝ} (hJ : MeasurableSet J) (hJf : MeasureTheory.volume J ≠ ⊤) (ψ : V → ℝ → ℂ) (hψ : ∀ (m : V), Measurable (ψ m)) (hψb : ∀ (m : V) (y : ℝ), ‖ψ m y‖ ≤ 1) (εw : V → ℝ) (M : Finset V) (β : V → ℂ) {ε : ℝ} (hε : ∀ m ∈ M, ε ≤ εw m) (hε0 : 0 ≤ ε) : ε * MeasureTheory.volume.real J * ∑ m ∈ M, ‖β m‖ ^ 2 ≤ ‖∑ m ∈ M, β m • MeasureTheory.MemLp.toLp (augMode J (ψ m) (εw m) m) ⋯‖ ^ 2

The private coordinates of a combination of augmented modes on one cell.

theorem TrilinearHT.Auto.columnL2_vanish_sum {V : Type u_1} {ι : Type u_2} [Fintype V] (s : Finset ι) (c : ι → ℂ) (v : ι → ↥(ColumnL2 V)) (J : Set ℝ) (hv : ∀ (i : ι), ∀ᵐ (y : ℝ), y ∉ J → ↑↑(v i) y = 0) : ∀ᵐ (y : ℝ), y ∉ J → ↑↑(∑ i ∈ s, c i • v i) y = 0

Combinations of column functions vanishing off J vanish off J.

theorem TrilinearHT.Auto.block_subtotals_le {V : Type u_1} {κ : Type u_2} [Fintype V] [DecidableEq V] (cells : Finset κ) (J : κ → Set ℝ) (hJ : ∀ (k : κ), MeasurableSet (J k)) (hJf : ∀ (k : κ), MeasureTheory.volume (J k) ≠ ⊤) (hdisjJ : (↑cells).PairwiseDisjoint J) (comps : κ → Finset (Finset V)) (ψ : V → ℝ → ℂ) (hψ : ∀ (m : V), Measurable (ψ m)) (hψb : ∀ (m : V) (y : ℝ), ‖ψ m y‖ ≤ 1) (εw : V → ℝ) (c : κ → V → ℂ) {η ε D : ℝ} (hη : 0 ≤ η) (hε : 0 < ε) (hD : 0 ≤ D) (hdisjE : ∀ k ∈ cells, ∀ E ∈ comps k, ∀ E' ∈ comps k, E ≠ E' → Disjoint E E') (hpair : ∀ k ∈ cells, ∀ E ∈ comps k, ∀ E' ∈ comps k, E ≠ E' → ∀ m ∈ E, ∀ m' ∈ E', ‖∫ (y : ℝ) in J k, (starRingEnd ℂ) (ψ m y) * ψ m' y‖ ≤ η * MeasureTheory.volume.real (J k)) (hεw : ∀ (m : V), ε ≤ εw m) (hnum : ∀ k ∈ cells, ↑(comps k).card ≤ D) (hcard : ∀ k ∈ cells, ∀ E ∈ comps k, ↑E.card ≤ ε * D ^ 2) : ‖∑ k ∈ cells, ∑ E ∈ comps k, ∑ m ∈ E, c k m • MeasureTheory.MemLp.toLp (augMode (J k) (ψ m) (εw m) m) ⋯‖ ^ 2 ≤ (1 + η * D ^ 3) * ∑ k ∈ cells, ∑ E ∈ comps k, ‖∑ m ∈ E, c k m • MeasureTheory.MemLp.toLp (augMode (J k) (ψ m) (εw m) m) ⋯‖ ^ 2

Blueprint lines 2116-2118 for one block: the side subtotal V = Σ_J Σ_E T_{E,J} over disjoint retained pre-cells J and, on each, disjoint minimal PRE components E with mutual physical pairings at most η |J|, satisfies ‖V‖² ≤ (1 + η D³) Σ_{J,E} ‖T_{E,J}‖².

Joint Bessel bounds for rows with group-dependent targets (lines 2068-2072)

theorem TrilinearHT.Auto.joint_bessel_hetero {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ι : Type u_2} {κ : ι → Type u_3} [Fintype ι] (F : ι → Type u_4) [(G : ι) → NormedAddCommGroup (F G)] [(G : ι) → InnerProductSpace ℂ (F G)] [∀ (G : ι), CompleteSpace (F G)] (s : (G : ι) → Finset (κ G)) (R : (G : ι) → κ G → H →L[ℂ] F G) {c : ℝ} (hc : 0 ≤ c) (hgrp : ∀ (G : ι) (x : H), ∑ k ∈ s G, ‖(R G k) x‖ ^ 2 ≤ c * ‖x‖ ^ 2) {C : ℝ} (hC : 0 ≤ C) (h : H) (hwr : ‖∑ G : ι, ∑ k ∈ s G, (ContinuousLinearMap.adjoint (R G k)) ((R G k) h)‖ ^ 2 ≤ C * ∑ G : ι, ‖∑ k ∈ s G, (ContinuousLinearMap.adjoint (R G k)) ((R G k) h)‖ ^ 2) : ∑ G : ι, ∑ k ∈ s G, ‖(R G k) h‖ ^ 2 ≤ C * c * ‖h‖ ^ 2

Blueprint lines 2068-2072: rows R_{G,k} : H → F_G that are Bessel with constant c within each group G, and whose adjoint outputs S_G = Σ_k R_{G,k}^* R_{G,k} h satisfy the whole-range almost orthogonality ‖Σ_G S_G‖² ≤ C Σ_G ‖S_G‖², have joint squared sum at most C c ‖h‖².

Lift rows over all groups of one color (blueprint lines 2066-2072)

theorem TrilinearHT.Auto.opAvg_adjoint {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {P : ℕ} (Q : Fin P → H →L[ℂ] H) (hQ : ∀ (p : Fin P), ContinuousLinearMap.adjoint (Q p) = Q p) : ContinuousLinearMap.adjoint (opAvg Q) = opAvg Q

Catalog projections commute with the restriction to their cell

Physical transfer between column spaces and the basic histories (lines 2072-2075)

Side events, linking, and the rows of one level (blueprint lines 2082-2110)

theorem TrilinearHT.Auto.ModeSchedule.gapEdge_symm (S : ModeSchedule) {Mode : Type u_1} {dz : ℕ} (ω : Mode → ℝ → ℝ) (ϑ : Fin dz → ℝ) (a r θr : ℝ) {h : ℕ} {m m' : Mode} (he : S.gapEdge ω ϑ a r θr h m m') : S.gapEdge ω ϑ a r θr h m' m

theorem TrilinearHT.Auto.ModeSchedule.sep_of_not_gapEdge_zero (S : ModeSchedule) {Mode : Type u_1} {dz : ℕ} (ω : Mode → ℝ → ℝ) (ϑ : Fin dz → ℝ) (a r θr : ℝ) {m m' : Mode} (hne : ¬S.gapEdge ω ϑ a r θr 0 m m') (n : Fin dz → ℤ) : (∀ (i : Fin dz), |↑(n i)| ≤ S.Eh 0) → ∃ x ∈ Set.Icc a (a + r), θr ≤ |ω m x - ω m' x + ∑ i : Fin dz, ↑(n i) * ϑ i|

Non-adjacency at height zero gives the separation hypothesis of the mode rows.

def TrilinearHT.Auto.ModeSystem.pre0Edge {Gd : RealDyadicGrid} {Mc : ℕ} (Ms : ModeSystem Gd Mc) (S : ModeSchedule) (J : ℤ × ℤ) (m m' : Ms.Md) : Prop

The PRE edge at height zero on a cell J between two modes.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev TrilinearHT.Auto.ModeSystem.Event {Gd : RealDyadicGrid} {Mc : ℕ} (Ms : ModeSystem Gd Mc) : Type

A side event: block start, retained pre-cell and mode set.

Equations

• Ms.Event = (ℤ × (ℤ × ℤ) × Finset Ms.Md)

def TrilinearHT.Auto.ModeSystem.Linked {Gd : RealDyadicGrid} {Mc : ℕ} (Ms : ModeSystem Gd Mc) (S : ModeSchedule) (e e' : Ms.Event) : Prop

Blueprint line 2084: an earlier event is linked to a later one on a descendant pre-cell when some of their modes agree or are adjacent in the later PRE graph at height zero.

Equations

• One or more equations did not get rendered due to their size.

theorem TrilinearHT.Auto.dyadicGridLength_le_of_subset (Gd : RealDyadicGrid) {I J : ℤ × ℤ} (h : dyadicGridCell Gd J.1 J.2 ⊆ dyadicGridCell Gd I.1 I.2) : dyadicGridLength Gd J.1 ≤ dyadicGridLength Gd I.1

theorem TrilinearHT.Auto.dyadicGridCell_nested_of_meet (Gd : RealDyadicGrid) {I J : ℤ × ℤ} (hIJ : I.1 ≤ J.1) (h : (dyadicGridCell Gd I.1 I.2 ∩ dyadicGridCell Gd J.1 J.2).Nonempty) : dyadicGridCell Gd J.1 J.2 ⊆ dyadicGridCell Gd I.1 I.2

Two meeting dyadic cells are nested, the deeper one inside.

theorem TrilinearHT.Auto.card_le_of_pairwiseDisjoint_subset {α : Type u_1} {β : Type u_2} (s : Finset α) (E : α → Finset β) (T : Finset β) (hne : ∀ e ∈ s, (E e).Nonempty) (hT : ∀ e ∈ s, E e ⊆ T) (hd : (↑s).PairwiseDisjoint E) : s.card ≤ T.card

A pairwise disjoint family of nonempty subsets of a finset T has at most |T| members.

noncomputable def TrilinearHT.Auto.ModeSystem.ptSet {Gd : RealDyadicGrid} {Mc : ℕ} (Ms : ModeSystem Gd Mc) (y : ℝ) : Finset Ms.Md

The modes whose first-match cells contain the point y: the modes on the path through y (blueprint lines 2114-2116: "label sets disjoint along paths with total count at most D_*").

Equations

• Ms.ptSet y = {m : Ms.Md | y ∈ TrilinearHT.Auto.dyadicGridCell Gd (Ms.cellOf m).1 (Ms.cellOf m).2}

theorem TrilinearHT.Auto.ModeSystem.mem_ptSet {Gd : RealDyadicGrid} {Mc : ℕ} (Ms : ModeSystem Gd Mc) {y : ℝ} {m : Ms.Md} : m ∈ Ms.ptSet y ↔ y ∈ dyadicGridCell Gd (Ms.cellOf m).1 (Ms.cellOf m).2

noncomputable def TrilinearHT.Auto.ModeSystem.evCell {Gd : RealDyadicGrid} {Mc : ℕ} (Ms : ModeSystem Gd Mc) (e : Ms.Event) : Set ℝ

The cell of an event as a set.

Equations

• Ms.evCell e = TrilinearHT.Auto.dyadicGridCell Gd e.2.1.1 e.2.1.2

noncomputable def TrilinearHT.Auto.ModeSystem.evMode {Gd : RealDyadicGrid} {Mc : ℕ} (Ms : ModeSystem Gd Mc) (e : Ms.Event) (m : Ms.Md) : ↥(ColumnL2 Ms.Md)

The augmented mode of m on the cell of the event e.

Equations

• One or more equations did not get rendered due to their size.

theorem TrilinearHT.Auto.ModeSystem.level_pair {Gd : RealDyadicGrid} {Mc : ℕ} (Ms : ModeSystem Gd Mc) (S : ModeSchedule) {s : Finset Ms.Event} (hdepth : ∀ e ∈ s, e.2.1.1 = e.1 - 2 * ↑S.K) (h3 : ∀ e ∈ s, ∀ e' ∈ s, e ≠ e' → e.1 = e'.1 → e.2.1 = e'.2.1 → Disjoint e.2.2 e'.2.2 ∧ ∀ m ∈ e.2.2, ∀ m' ∈ e'.2.2, ¬Ms.pre0Edge S e.2.1 m m') (h4 : ∀ e ∈ s, ∀ e' ∈ s, ¬Ms.Linked S e e') {e e' : Ms.Event} (he : e ∈ s) (he' : e' ∈ s) (hne : e ≠ e') (hov : (Ms.evCell e ∩ Ms.evCell e').Nonempty) : ∃ (c : ℤ × ℤ), (c = e.2.1 ∨ c = e'.2.1) ∧ Ms.evCell e ∩ Ms.evCell e' = dyadicGridCell Gd c.1 c.2 ∧ Disjoint e.2.2 e'.2.2 ∧ ∀ m ∈ e.2.2, ∀ m' ∈ e'.2.2, ¬Ms.pre0Edge S c m m'

Overlapping events of one level are comparable: the deeper cell is inside the other, the mode sets are disjoint and the modes are not adjacent at height zero on the smaller cell.

theorem TrilinearHT.Auto.sum_measureReal_inter_le {α : Type u_1} (s : Finset α) (J : α → Set ℝ) (hJ : ∀ (e : α), MeasurableSet (J e)) (hJf : ∀ (e : α), MeasureTheory.volume (J e) ≠ ⊤) (e : α) {N : ℕ} (hN : ∀ y ∈ J e, {e' ∈ s | y ∈ J e'}.card ≤ N) : ∑ e' ∈ s, MeasureTheory.volume.real (J e ∩ J e') ≤ ↑N * MeasureTheory.volume.real (J e)

The overlap sum of a family of sets is at most the pointwise multiplicity bound times the measure of one of them.

theorem TrilinearHT.Auto.ModeSystem.level_rows {Gd : RealDyadicGrid} {Mc : ℕ} (Ms : ModeSystem Gd Mc) (S : ModeSchedule) {s : Finset Ms.Event} (hδ : 0 < Ms.δc) (h1 : ∀ e ∈ s, e.2.2.Nonempty) (h2 : ∀ e ∈ s, ∀ m ∈ e.2.2, Ms.evCell e ⊆ dyadicGridCell Gd (Ms.cellOf m).1 (Ms.cellOf m).2) (hdepth : ∀ e ∈ s, e.2.1.1 = e.1 - 2 * ↑S.K) (h3 : ∀ e ∈ s, ∀ e' ∈ s, e ≠ e' → e.1 = e'.1 → e.2.1 = e'.2.1 → Disjoint e.2.2 e'.2.2 ∧ ∀ m ∈ e.2.2, ∀ m' ∈ e'.2.2, ¬Ms.pre0Edge S e.2.1 m m') (h4 : ∀ e ∈ s, ∀ e' ∈ s, ¬Ms.Linked S e e') (hΛ : 8 * Ms.Λ ≤ S.Ξ) (hΞ : 0 < S.Ξ) (hQ0 : 0 < S.Q0) (Kf : ℕ) (hbox : ↑S.Q0 * 2 ^ (Kf + 1) ≤ S.Eh 0) {ε D : ℝ} (hε : 0 < ε) (hεw : ∀ (m : Ms.Md), ε ≤ Ms.L.εM m) (hD0 : 0 ≤ D) (hD1 : ∀ (y : ℝ), ↑(Ms.ptSet y).card ≤ D) (hD2 : ∀ (y : ℝ), ↑(Ms.ptSet y).card ≤ ε * D ^ 2) [inst : ∀ (e : Ms.Event), (Submodule.span ℂ (Ms.evMode e '' ↑e.2.2)).HasOrthogonalProjection] (F : ↥(ColumnL2 Ms.Md)) : ∑ e ∈ s, ‖(Submodule.span ℂ (Ms.evMode e '' ↑e.2.2)).starProjection F‖ ^ 2 ≤ (1 + pairConst Ms.zc.dim Ms.δc S.Ξ Kf * D ^ 3) * ‖F‖ ^ 2

Blueprint lines 2104-2108: the side events of one level (pairwise unlinked, distinct components on one pre-cell non-adjacent at height zero) give Bessel mode rows (lem:mode-rows), with overlap multiplicity at most the number of modes.

The length of linked chains of side events (eq:bad-density, lines 2088-2102)

theorem TrilinearHT.Auto.chain_side_bound {P : Type u_1} [DecidableEq P] (n : ℕ) (Mode : ℕ → Type u_2) [(i : ℕ) → DecidableEq (Mode i)] (C : (i : ℕ) → ModeComponents (Mode i) P) (x : (i : ℕ) → Mode i) (Δ Jst M Ae Ah : ℕ) (δ : ℝ) (goodP : ℕ → ℕ → P → Prop) (nonexc : ℕ → P → Prop) (hlink : ∀ (i : ℕ), i + 1 < n → ∀ (h : ℕ), (C i).labels ((C i).F h (x i)) ⊆ (C (i + 1)).labels ((C (i + 1)).E h (x (i + 1)))) (hM : ∀ (i h : ℕ), ((C i).labels ((C i).F h (x i))).card ≤ M) (hAe : ∀ (p : P), {i ∈ Finset.range n | ¬nonexc i p}.card ≤ Ae) (hAh : ∀ i < n, ∀ (p : P), nonexc i p → {h ∈ Finset.range (Jst + 1) | ¬goodP i h p}.card ≤ Ah) (hside : ∀ i < n, δ * (↑Jst + 1) < ↑((C i).badHeights Δ (goodP i) Jst (x i)).card) : δ * ↑n * (↑Jst + 1) ≤ ↑n * ↑Δ + 10 * (↑n * ↑Δ * Real.log ↑M + (↑Jst + 1) * Real.log ↑M) + 10 * (((↑Jst + 1) * ↑Ae + ↑n * ↑Ah) * (1 + Real.log ↑M))

Blueprint lines 2088-2099 on a linked chain of n side events with component structures C_i and representative modes x_i: if the CURRENT label sets feed into the next PRE label sets, every key is exceptional in at most A_e events and height-bad at most A_h times at each event, and every event has more than δ (J + 1) bad heights, then δ n (J+1) ≤ nΔ + 10(nΔ log M + (J+1) log M) + 10((J+1) A_e + n A_h)(1 + log M).

def TrilinearHT.Auto.ModeSystem.goodP {Gd : RealDyadicGrid} {Mc : ℕ} (Ms : ModeSystem Gd Mc) (S : ModeSchedule) (SP : SideParams) (b : ℤ) (h : ℕ) (p : Ms.Key) : Prop

The goodness of a key at height h in the block b (nonexceptional, stable spans).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def TrilinearHT.Auto.ModeSystem.sideModes {Gd : RealDyadicGrid} {Mc : ℕ} (Ms : ModeSystem Gd Mc) (S : ModeSchedule) (hA : 6 ≤ S.A0) (SP : SideParams) (b : ℤ) (J : ℤ × ℤ) : Finset ↥(Ms.alive (ancAt Gd J (b - 4 * ↑S.K)))

The side modes of the block b on the pre-cell J: those that are not core.

Equations

• Ms.sideModes S hA SP b J = {x : ↥(Ms.alive (TrilinearHT.Auto.ancAt Gd J (b - 4 * ↑S.K))) | ¬(Ms.blockComps S hA b J).Core SP.Δ (Ms.goodP S SP b) SP.Jst SP.δs x}

noncomputable def TrilinearHT.Auto.ModeSystem.sideEvents {Gd : RealDyadicGrid} {Mc : ℕ} (Ms : ModeSystem Gd Mc) (S : ModeSchedule) (hA : 6 ≤ S.A0) (SP : SideParams) (b : ℤ) (J : ℤ × ℤ) : Finset (Finset Ms.Md)

The side events of the block b on the pre-cell J: the minimal PRE components of its side modes.

Equations

• One or more equations did not get rendered due to their size.

theorem TrilinearHT.Auto.ModeSystem.preComps_transport {Gd : RealDyadicGrid} {Mc : ℕ} (Ms : ModeSystem Gd Mc) (S : ModeSchedule) (hA : 6 ≤ S.A0) {u u' t t' : ℤ} {J J' : ℤ × ℤ} (h1 : J.1 ≤ t) (h2 : J'.1 ≤ t') (hUU : dyadicGridCell Gd (ancAt Gd J' u').1 (ancAt Gd J' u').2 ⊆ dyadicGridCell Gd (ancAt Gd J u).1 (ancAt Gd J u).2) (hsub : dyadicGridCell Gd J'.1 J'.2 ⊆ dyadicGridCell Gd J.1 J.2) (hth : t ≤ J'.1) (h : ℕ) {y y' : ↥(Ms.alive (ancAt Gd J u))} (hy : y' ∈ (Ms.preComps S hA u t J h1).F h y) : Ms.aliveMap hUU y' ∈ (Ms.preComps S hA u' t' J' h2).E h (Ms.aliveMap hUU y)

CURRENT components of an earlier pre-cell transport into PRE components of a later one.

theorem TrilinearHT.Auto.ModeSystem.link_labels {Gd : RealDyadicGrid} {Mc : ℕ} (Ms : ModeSystem Gd Mc) (S : ModeSchedule) (hA : 6 ≤ S.A0) {b b' : ℤ} {J J' : ℤ × ℤ} (hJ : J.1 = b - 2 * ↑S.K) (hJ' : J'.1 = b' - 2 * ↑S.K) (hbb : b + 3 * ↑S.K ≤ b') (hsub : dyadicGridCell Gd J'.1 J'.2 ⊆ dyadicGridCell Gd J.1 J.2) (x : ↥(Ms.alive (ancAt Gd J (b - 4 * ↑S.K)))) (x' : ↥(Ms.alive (ancAt Gd J' (b' - 4 * ↑S.K)))) {m m' : Ms.Md} (hm : m ∈ Finset.map { toFun := Subtype.val, inj' := ⋯ } ((Ms.blockComps S hA b J).E 0 x)) (hm' : m' ∈ Finset.map { toFun := Subtype.val, inj' := ⋯ } ((Ms.blockComps S hA b' J').E 0 x')) (hlink : m = m' ∨ Ms.pre0Edge S J' m m') (h : ℕ) : (Ms.blockComps S hA b J).labels ((Ms.blockComps S hA b J).F h x) ⊆ (Ms.blockComps S hA b' J').labels ((Ms.blockComps S hA b' J').E h x')

Blueprint lines 2084-2088: along a link from an event of block b on J to an event of a block b' ≥ b + 3K on J' ⊆ J, the CURRENT labels of the earlier representative at any height are PRE labels of the later representative.

def TrilinearHT.Auto.ModeSystem.nonexcAt {Gd : RealDyadicGrid} {Mc : ℕ} (Ms : ModeSystem Gd Mc) (S : ModeSchedule) (SP : SideParams) (b : ℤ) (p : Ms.Key) : Prop

The gap condition (nonexceptionality) of a key at the block b.

Equations

• One or more equations did not get rendered due to their size.

theorem TrilinearHT.Auto.ModeSystem.chain_events_bound {Gd : RealDyadicGrid} {Mc : ℕ} (Ms : ModeSystem Gd Mc) (S : ModeSchedule) (hA : 6 ≤ S.A0) (SP : SideParams) (s : Finset Ms.Event) (hev : ∀ e ∈ s, e.2.2 ∈ Ms.sideEvents S hA SP e.1 e.2.1) (hdepth : ∀ e ∈ s, e.2.1.1 = e.1 - 2 * ↑S.K) (hsep : ∀ e ∈ s, ∀ e' ∈ s, e.1 < e'.1 → e.1 + 3 * ↑S.K ≤ e'.1) {M : ℕ} (hM : ∀ (U : ℤ × ℤ), (Finset.image Ms.keyOf (Ms.alive U)).card ≤ M) {Ae Ah : ℕ} (hAe : ∀ (p : Ms.Key) (T : Finset ℤ), (∀ b ∈ T, ∃ e ∈ s, e.1 = b) → (∀ b ∈ T, ∀ b' ∈ T, b < b' → b + 3 * ↑S.K ≤ b') → {b ∈ T | ¬Ms.nonexcAt S SP b p}.card ≤ Ae) (hAh : ∀ (b : ℤ) (p : Ms.Key), Ms.nonexcAt S SP b p → {h ∈ Finset.range (SP.Jst + 1) | ¬Ms.goodP S SP b h p}.card ≤ Ah) {k : ℕ} {e : Ms.Event} (hc : LinkedChain (↑s) (Ms.Linked S) k e) : SP.δs * ↑(k + 1) * (↑SP.Jst + 1) ≤ ↑(k + 1) * ↑SP.Δ + 10 * (↑(k + 1) * ↑SP.Δ * Real.log ↑M + (↑SP.Jst + 1) * Real.log ↑M) + 10 * (((↑SP.Jst + 1) * ↑Ae + ↑(k + 1) * ↑Ah) * (1 + Real.log ↑M))

Blueprint lines 2088-2102 for the side events of one class: a linked chain with k links of side events whose blocks are at least 3K apart has δ (k+1)(J+1) at most the bad-incidence bound, where the keys of the modes alive at any cell number at most M (the label sets of the chain are path-local), every key is exceptional in at most A_e of the blocks of the events, and every nonexceptional key is height-bad at most A_h times in one block.

theorem TrilinearHT.Auto.ModeSystem.sideEvents_pair {Gd : RealDyadicGrid} {Mc : ℕ} (Ms : ModeSystem Gd Mc) (S : ModeSchedule) (hA : 6 ≤ S.A0) (SP : SideParams) {b : ℤ} {J : ℤ × ℤ} (hJ : J.1 ≤ b + ↑S.K) {E E' : Finset Ms.Md} (hE : E ∈ Ms.sideEvents S hA SP b J) (hE' : E' ∈ Ms.sideEvents S hA SP b J) (hne : E ≠ E') : Disjoint E E' ∧ ∀ m ∈ E, ∀ m' ∈ E', ¬Ms.pre0Edge S J m m'

Distinct minimal PRE components on one pre-cell are disjoint and not adjacent at height zero (blueprint line 2104: "distinct components on the same cell have this separation").

theorem TrilinearHT.Auto.ModeSystem.sideEvents_nonempty {Gd : RealDyadicGrid} {Mc : ℕ} (Ms : ModeSystem Gd Mc) (S : ModeSchedule) (hA : 6 ≤ S.A0) (SP : SideParams) {b : ℤ} {J : ℤ × ℤ} {E : Finset Ms.Md} (hE : E ∈ Ms.sideEvents S hA SP b J) : E.Nonempty

theorem TrilinearHT.Auto.ModeSystem.sideEvents_alive {Gd : RealDyadicGrid} {Mc : ℕ} (Ms : ModeSystem Gd Mc) (S : ModeSchedule) (hA : 6 ≤ S.A0) (SP : SideParams) {b : ℤ} {J : ℤ × ℤ} (hJ : b - 4 * ↑S.K ≤ J.1) {E : Finset Ms.Md} (hE : E ∈ Ms.sideEvents S hA SP b J) {m : Ms.Md} (hm : m ∈ E) : dyadicGridCell Gd J.1 J.2 ⊆ dyadicGridCell Gd (Ms.cellOf m).1 (Ms.cellOf m).2

theorem TrilinearHT.Auto.ModeSystem.class_rows {Gd : RealDyadicGrid} {Mc : ℕ} (Ms : ModeSystem Gd Mc) (S : ModeSchedule) (hA : 6 ≤ S.A0) (SP : SideParams) (s : Finset Ms.Event) (hev : ∀ e ∈ s, e.2.2 ∈ Ms.sideEvents S hA SP e.1 e.2.1) (hdepth : ∀ e ∈ s, e.2.1.1 = e.1 - 2 * ↑S.K) {L : ℕ} (hL : ∀ (k : ℕ) (e : Ms.Event), LinkedChain (↑s) (Ms.Linked S) k e → k ≤ L) (hδ : 0 < Ms.δc) (hΛ : 8 * Ms.Λ ≤ S.Ξ) (hΞ : 0 < S.Ξ) (hQ0 : 0 < S.Q0) (Kf : ℕ) (hbox : ↑S.Q0 * 2 ^ (Kf + 1) ≤ S.Eh 0) {ε D : ℝ} (hε : 0 < ε) (hεw : ∀ (m : Ms.Md), ε ≤ Ms.L.εM m) (hD0 : 0 ≤ D) (hD1 : ∀ (y : ℝ), ↑(Ms.ptSet y).card ≤ D) (hD2 : ∀ (y : ℝ), ↑(Ms.ptSet y).card ≤ ε * D ^ 2) [inst : ∀ (e : Ms.Event), (Submodule.span ℂ (Ms.evMode e '' ↑e.2.2)).HasOrthogonalProjection] (F : ↥(ColumnL2 Ms.Md)) : ∑ e ∈ s, ‖(Submodule.span ℂ (Ms.evMode e '' ↑e.2.2)).starProjection F‖ ^ 2 ≤ (↑L + 1) * ((1 + pairConst Ms.zc.dim Ms.δc S.Ξ Kf * D ^ 3) * ‖F‖ ^ 2)

Blueprint lines 2104-2108 for one class of blocks: the side events of the class, split into longest-chain levels (at most L + 1 of them when chains have at most L links), give Bessel mode rows with constant (L + 1)(1 + η D³).

theorem TrilinearHT.Auto.ModeSystem.evMode_eq {Gd : RealDyadicGrid} {Mc : ℕ} (Ms : ModeSystem Gd Mc) (e : Ms.Event) : Ms.evMode e = Ms.cellMode e.2.1

theorem TrilinearHT.Auto.ModeSystem.cellMode_inner_le {Gd : RealDyadicGrid} {Mc : ℕ} (Ms : ModeSystem Gd Mc) (S : ModeSchedule) (hδ : 0 < Ms.δc) (hΛ : 8 * Ms.Λ ≤ S.Ξ) (hΞ : 0 < S.Ξ) (hQ0 : 0 < S.Q0) (Kf : ℕ) (hbox : ↑S.Q0 * 2 ^ (Kf + 1) ≤ S.Eh 0) {J : ℤ × ℤ} {m m' : Ms.Md} (hm : dyadicGridCell Gd J.1 J.2 ⊆ dyadicGridCell Gd (Ms.cellOf m).1 (Ms.cellOf m).2) (hm' : dyadicGridCell Gd J.1 J.2 ⊆ dyadicGridCell Gd (Ms.cellOf m').1 (Ms.cellOf m').2) (hne : m ≠ m') (hna : ¬Ms.pre0Edge S J m m') : ‖inner ℂ (Ms.cellMode J m) (Ms.cellMode J m')‖ ≤ pairConst Ms.zc.dim Ms.δc S.Ξ Kf * dyadicGridLength Gd J.1

Blueprint lines 2054-2056 on one pre-cell: two distinct modes alive on J that are not adjacent at height zero there have augmented pairing at most η |J|.

theorem TrilinearHT.Auto.ModeSystem.sideEvents_subset_alive {Gd : RealDyadicGrid} {Mc : ℕ} (Ms : ModeSystem Gd Mc) (S : ModeSchedule) (hA : 6 ≤ S.A0) (SP : SideParams) {b : ℤ} {J : ℤ × ℤ} {E : Finset Ms.Md} (hE : E ∈ Ms.sideEvents S hA SP b J) : E ⊆ Ms.alive (ancAt Gd J (b - 4 * ↑S.K))

theorem TrilinearHT.Auto.ModeSystem.sideEvent_not_adj {Gd : RealDyadicGrid} {Mc : ℕ} (Ms : ModeSystem Gd Mc) (S : ModeSchedule) (hA : 6 ≤ S.A0) (SP : SideParams) {b : ℤ} {J : ℤ × ℤ} (hJ : J.1 ≤ b + ↑S.K) {E : Finset Ms.Md} (hE : E ∈ Ms.sideEvents S hA SP b J) {m m' : Ms.Md} (hm : m ∈ E) (hm' : m' ∈ Ms.alive (ancAt Gd J (b - 4 * ↑S.K)) \ E) : ¬Ms.pre0Edge S J m m'

Modes of a side event are not adjacent at height zero to the other alive modes of the pre-cell.

theorem TrilinearHT.Auto.ModeSystem.event_subtotal_close {Gd : RealDyadicGrid} {Mc : ℕ} (Ms : ModeSystem Gd Mc) (S : ModeSchedule) (hA : 6 ≤ S.A0) (SP : SideParams) {b : ℤ} {J : ℤ × ℤ} (hJ : J.1 ≤ b + ↑S.K) (hJu : b - 4 * ↑S.K ≤ J.1) {E : Finset Ms.Md} (hE : E ∈ Ms.sideEvents S hA SP b J) (c : Ms.Md → ℂ) [(Submodule.span ℂ (Ms.cellMode J '' ↑E)).HasOrthogonalProjection] (hδ : 0 < Ms.δc) (hΛ : 8 * Ms.Λ ≤ S.Ξ) (hΞ : 0 < S.Ξ) (hQ0 : 0 < S.Q0) (Kf : ℕ) (hbox : ↑S.Q0 * 2 ^ (Kf + 1) ≤ S.Eh 0) {ε : ℝ} (hε : 0 < ε) (hεw : ∀ (m : Ms.Md), ε ≤ Ms.L.εM m) : ‖(Submodule.span ℂ (Ms.cellMode J '' ↑E)).starProjection (∑ m ∈ Ms.alive (ancAt Gd J (b - 4 * ↑S.K)), c m • Ms.cellMode J m) - ∑ m ∈ E, c m • Ms.cellMode J m‖ ≤ pairConst Ms.zc.dim Ms.δc S.Ξ Kf * dyadicGridLength Gd J.1 * (√↑E.card * (√↑(Ms.alive (ancAt Gd J (b - 4 * ↑S.K)) \ E).card * √(∑ m' ∈ Ms.alive (ancAt Gd J (b - 4 * ↑S.K)) \ E, ‖c m'‖ ^ 2))) / √(ε * dyadicGridLength Gd J.1)

Blueprint lines 2112-2113 for a side event: the row projection of the frozen evaluation Σ_{m alive} c_m Ψ_m on the event's modes differs from the exact side subtotal by at most the complementary pairing bound.

noncomputable def TrilinearHT.Auto.ModeSystem.blockSide {Gd : RealDyadicGrid} {Mc : ℕ} (Ms : ModeSystem Gd Mc) (S : ModeSchedule) (hA : 6 ≤ S.A0) (SP : SideParams) (b : ℤ) (cells : Finset (ℤ × ℤ)) (c : ℤ × ℤ → Ms.Md → ℂ) : ↥(ColumnL2 Ms.Md)

The exact side subtotal of the block b: the side events on the retained pre-cells, with coefficients c J m of the frozen evaluation (blueprint line 2081, V_{l,G,b}).

Equations

• Ms.blockSide S hA SP b cells c = ∑ J ∈ cells, ∑ E ∈ Ms.sideEvents S hA SP b J, ∑ m ∈ E, c J m • Ms.cellMode J m

theorem TrilinearHT.Auto.ModeSystem.blockSide_norm_sq_le {Gd : RealDyadicGrid} {Mc : ℕ} (Ms : ModeSystem Gd Mc) (S : ModeSchedule) (hA : 6 ≤ S.A0) (SP : SideParams) {b : ℤ} {cells : Finset (ℤ × ℤ)} (hdepth : ∀ J ∈ cells, J.1 = b - 2 * ↑S.K) (c : ℤ × ℤ → Ms.Md → ℂ) (hδ : 0 < Ms.δc) (hΛ : 8 * Ms.Λ ≤ S.Ξ) (hΞ : 0 < S.Ξ) (hQ0 : 0 < S.Q0) (Kf : ℕ) (hbox : ↑S.Q0 * 2 ^ (Kf + 1) ≤ S.Eh 0) {ε D : ℝ} (hε : 0 < ε) (hεw : ∀ (m : Ms.Md), ε ≤ Ms.L.εM m) (hD0 : 0 ≤ D) (hD1 : ∀ (y : ℝ), ↑(Ms.ptSet y).card ≤ D) (hD2 : ∀ (y : ℝ), ↑(Ms.ptSet y).card ≤ ε * D ^ 2) : ‖Ms.blockSide S hA SP b cells c‖ ^ 2 ≤ (1 + pairConst Ms.zc.dim Ms.δc S.Ξ Kf * D ^ 3) * ∑ J ∈ cells, ∑ E ∈ Ms.sideEvents S hA SP b J, ‖∑ m ∈ E, c J m • Ms.cellMode J m‖ ^ 2

Blueprint lines 2116-2118 for one block: the side subtotal over disjoint retained pre-cells is almost orthogonal over its events.

noncomputable def TrilinearHT.Auto.ModeSystem.frozenEval {Gd : RealDyadicGrid} {Mc : ℕ} (Ms : ModeSystem Gd Mc) (S : ModeSchedule) (b : ℤ) (J : ℤ × ℤ) (c : Ms.Md → ℂ) : ↥(ColumnL2 Ms.Md)

The frozen evaluation of the block b on the pre-cell J: the synthesis of the modes alive on its decision cell with coefficients c (blueprint line 1959, ZTilde_{l,G,b} on J).

Equations

• Ms.frozenEval S b J c = ∑ m ∈ Ms.alive (TrilinearHT.Auto.ancAt Gd J (b - 4 * ↑S.K)), c m • Ms.cellMode J m

noncomputable def TrilinearHT.Auto.ModeSystem.eventErr {Gd : RealDyadicGrid} {Mc : ℕ} (Ms : ModeSystem Gd Mc) (S : ModeSchedule) (Kf : ℕ) (ε : ℝ) (b : ℤ) (J : ℤ × ℤ) (E : Finset Ms.Md) (c : Ms.Md → ℂ) : ℝ

The complementary pairing error of a side event (event_subtotal_close).

Equations

• One or more equations did not get rendered due to their size.

theorem TrilinearHT.Auto.ModeSystem.group_side_energy {Gd : RealDyadicGrid} {Mc : ℕ} (Ms : ModeSystem Gd Mc) (S : ModeSchedule) (hA : 6 ≤ S.A0) (SP : SideParams) (Bs : Finset ℤ) (cells : ℤ → Finset (ℤ × ℤ)) (hdepth : ∀ b ∈ Bs, ∀ J ∈ cells b, J.1 = b - 2 * ↑S.K) (c : ℤ → ℤ × ℤ → Ms.Md → ℂ) [inst : ∀ (J : ℤ × ℤ) (E : Finset Ms.Md), (Submodule.span ℂ (Ms.cellMode J '' ↑E)).HasOrthogonalProjection] (hδ : 0 < Ms.δc) (hΛ : 8 * Ms.Λ ≤ S.Ξ) (hΞ : 0 < S.Ξ) (hQ0 : 0 < S.Q0) (Kf : ℕ) (hbox : ↑S.Q0 * 2 ^ (Kf + 1) ≤ S.Eh 0) {ε D : ℝ} (hε : 0 < ε) (hεw : ∀ (m : Ms.Md), ε ≤ Ms.L.εM m) (hD0 : 0 ≤ D) (hD1 : ∀ (y : ℝ), ↑(Ms.ptSet y).card ≤ D) (hD2 : ∀ (y : ℝ), ↑(Ms.ptSet y).card ≤ ε * D ^ 2) : ∑ b ∈ Bs, ‖Ms.blockSide S hA SP b (cells b) (c b)‖ ^ 2 ≤ 2 * (1 + pairConst Ms.zc.dim Ms.δc S.Ξ Kf * D ^ 3) * ∑ b ∈ Bs, ∑ J ∈ cells b, ∑ E ∈ Ms.sideEvents S hA SP b J, (‖(Submodule.span ℂ (Ms.cellMode J '' ↑E)).starProjection (Ms.frozenEval S b J (c b J))‖ ^ 2 + Ms.eventErr S Kf ε b J E (c b J) ^ 2)

Blueprint lines 2104-2118 for one group: the exact side subtotals of its blocks have squared norms bounded by twice the almost-orthogonality constant times the squared row outputs of their side events plus the squared complementary errors.

The global ball outputs and histories of an attempt (blueprint lines 1857-1890)

The event rows of all groups composed with the attempt histories (lines 2062-2108)

noncomputable def TrilinearHT.Auto.ModeSystem.events {Gd : RealDyadicGrid} {Mc : ℕ} (Ms : ModeSystem Gd Mc) (S : ModeSchedule) (hA : 6 ≤ S.A0) (SP : SideParams) (Bs : Finset ℤ) (cells : ℤ → Finset (ℤ × ℤ)) : Finset Ms.Event

The side events (b, J, E) of the blocks Bs on their retained pre-cells.

Equations

• Ms.events S hA SP Bs cells = Bs.biUnion fun (b : ℤ) => (cells b).biUnion fun (J : ℤ × ℤ) => Finset.image (fun (E : Finset Ms.Md) => (b, J, E)) (Ms.sideEvents S hA SP b J)

theorem TrilinearHT.Auto.ModeSystem.sum_events {Gd : RealDyadicGrid} {Mc : ℕ} (Ms : ModeSystem Gd Mc) (S : ModeSchedule) (hA : 6 ≤ S.A0) (SP : SideParams) (Bs : Finset ℤ) (cells : ℤ → Finset (ℤ × ℤ)) (f : Ms.Event → ℝ) : ∑ e ∈ Ms.events S hA SP Bs cells, f e = ∑ b ∈ Bs, ∑ J ∈ cells b, ∑ E ∈ Ms.sideEvents S hA SP b J, f (b, J, E)

theorem TrilinearHT.Auto.ModeSystem.mem_events {Gd : RealDyadicGrid} {Mc : ℕ} (Ms : ModeSystem Gd Mc) (S : ModeSchedule) (hA : 6 ≤ S.A0) (SP : SideParams) {Bs : Finset ℤ} {cells : ℤ → Finset (ℤ × ℤ)} {e : Ms.Event} (he : e ∈ Ms.events S hA SP Bs cells) : e.1 ∈ Bs ∧ e.2.1 ∈ cells e.1 ∧ e.2.2 ∈ Ms.sideEvents S hA SP e.1 e.2.1

theorem TrilinearHT.Auto.chain_length_of_bound {δ Δ l Ae Ah Y x : ℝ} (hδ : 0 < δ) (hY : 0 < Y) (hx : 0 ≤ x) (hJ : 2 * (Δ + 10 * Δ * l + 10 * Ah * (1 + l)) ≤ δ * Y) (h : δ * x * Y ≤ x * Δ + 10 * (x * Δ * l + Y * l) + 10 * ((Y * Ae + x * Ah) * (1 + l))) : x ≤ 20 * (l + Ae * (1 + l)) / δ

Blueprint eq:bad-density (line 2102), the absorption step: the chain inequality with δ (J+1) at least twice the per-link cost gives k + 1 ≤ 20 (log M + A_e (1 + log M)) / δ.

eq:bad-density at the chosen schedule (blueprint lines 2100-2112)

theorem TrilinearHT.Auto.ModeSystem.exceptionalAt_of_not_nonexcAt {Gd : RealDyadicGrid} {Mc : ℕ} (Ms : ModeSystem Gd Mc) (S : ModeSchedule) (δs : ℝ) (hH : 0 ≤ S.H) {b : ℤ} {p : Ms.Key} (h : ¬Ms.nonexcAt S (S.sideParams δs) b p) : ExceptionalAt (Fin.append (Ms.θvOf p) fun (l : Fin Ms.zc.dim) => Ms.zc.θ l / ↑S.Q0) S.H Gd.baseLength S.T S.K b

A key that is not nonexceptional at a block (with the side parameters of the schedule) is exceptional there in the sense of eq:gap (ExceptionalAt with r₀ the base length of the grid).

theorem TrilinearHT.Auto.ModeSystem.not_exceptionalAt_of_nonexcAt {Gd : RealDyadicGrid} {Mc : ℕ} (Ms : ModeSystem Gd Mc) (S : ModeSchedule) (δs : ℝ) {b : ℤ} {p : Ms.Key} (h : Ms.nonexcAt S (S.sideParams δs) b p) : ¬ExceptionalAt (Fin.append (Ms.θvOf p) fun (l : Fin Ms.zc.dim) => Ms.zc.θ l / ↑S.Q0) S.H Gd.baseLength S.T S.K b

A nonexceptional key is not exceptional in the sense of eq:gap.

theorem TrilinearHT.Auto.ModeSystem.chain_length_schedule {Gd : RealDyadicGrid} {Mc : ℕ} (Ms : ModeSystem Gd Mc) (S : ModeSchedule) {Cj CA CT CK : ℕ} {δs W : ℝ} (hV : S.Valid Cj CA CT CK δs W) (hCj : 340 ≤ Cj) (hCA : 1 ≤ CA) (hδ : 0 < δs) (hδ1 : δs ≤ 1) (hd2 : 2 ≤ S.dmax) (hD : 2 ≤ S.Dstar) (hB : 2 ≤ S.Bstar) (hQ : 1 ≤ S.Q0) (hDm : 2 ≤ S.Dm) (hW : 8 * (↑S.dmax + 1) ^ 3 * Real.log (2 * S.H) / Real.log 2 ≤ W) (hdim : ∀ (p : Ms.Key), Ms.dvOf p + Ms.zc.dim ≤ S.dmax) {M : ℕ} (hM1 : 1 ≤ M) (hMD : ↑M ≤ 2 * S.Dm) (hM : ∀ (U : ℤ × ℤ), (Finset.image Ms.keyOf (Ms.alive U)).card ≤ M) (R₀ : ℤ) (s : Finset Ms.Event) (hev : ∀ e ∈ s, e.2.2 ∈ Ms.sideEvents S ⋯ (S.sideParams δs) e.1 e.2.1) (hdepth : ∀ e ∈ s, e.2.1.1 = e.1 - 2 * ↑S.K) (hgrid : ∀ e ∈ s, ↑S.K ∣ e.1 - R₀) (hsep : ∀ e ∈ s, ∀ e' ∈ s, e.1 < e'.1 → e.1 + 3 * ↑S.K ≤ e'.1) {k : ℕ} {e : Ms.Event} (hc : LinkedChain (↑s) (Ms.Linked S) k e) : ↑(k + 1) ≤ 180 * ↑S.dmax * Real.log (2 * S.Dm) / δs

Blueprint eq:bad-density (lines 2100-2112) at the chosen schedule: a linked chain of side events of one class (blocks on the K-grid through R₀, at least 3K apart) has length at most 180 d_max log(2 D_m) / δ_*, free of the height parameter. The label sets are path-local (the keys of the modes alive at any cell number at most M ≤ 2 D_m); a nonexceptional key is height-bad at most 3 d_max R_*^{ht} times at one event (lem:stabilize), a key is exceptional in at most 4 d_max blocks of the class (line 1996), and the choice J_* ≥ C_J δ_*^{-2} d_max R_*^{ht} log(2 D_m) with C_J ≥ 340 absorbs the first term.

theorem TrilinearHT.Auto.norm_physEmbed_apply_le {V : Type u_1} {W : Type u_2} [Fintype V] [Fintype W] (x : ↥(ColumnL2 V)) : ‖(physEmbed V W) x‖ ≤ ‖x‖

theorem TrilinearHT.Auto.physEmbed_restrict {V : Type u_1} {W : Type u_2} [Fintype V] [Fintype W] (s : Set ℝ) (hs : MeasurableSet s) (x : ↥(ColumnL2 V)) : (physEmbed V W) ((columnL2Restriction s hs) x) = (columnL2Restriction s hs) ((physEmbed V W) x)

noncomputable def TrilinearHT.Auto.blockClass (R₀ : ℤ) (K : ℕ) (b : ℤ) : Fin 3

The class β mod 3 of a block start b = R₀ + K β (blueprint lines 2084-2086).

Equations

• TrilinearHT.Auto.blockClass R₀ K b = ⟨((b - R₀) / ↑K % 3).toNat, ⋯⟩

theorem TrilinearHT.Auto.blockClass_sep {R₀ : ℤ} {K : ℕ} (hK : 1 ≤ K) {b b' : ℤ} (hb : ↑K ∣ b - R₀) (hb' : ↑K ∣ b' - R₀) (hc : blockClass R₀ K b = blockClass R₀ K b') (hlt : b < b') : b + 3 * ↑K ≤ b'

Blueprint lines 2084-2086: block starts of one class are at least 3K apart.

theorem TrilinearHT.Auto.ModeSystem.eventErr_sq_le {Gd : RealDyadicGrid} {Mc : ℕ} (Ms : ModeSystem Gd Mc) (S : ModeSchedule) (Kf : ℕ) {ε : ℝ} (hε : 0 < ε) (b : ℤ) (J : ℤ × ℤ) (E : Finset Ms.Md) (hE : E ⊆ Ms.alive (ancAt Gd J (b - 4 * ↑S.K))) (c : Ms.Md → ℂ) {D B : ℝ} (hD : ↑(Ms.alive (ancAt Gd J (b - 4 * ↑S.K))).card ≤ D) (hB : ∑ m' ∈ Ms.alive (ancAt Gd J (b - 4 * ↑S.K)), ‖c m'‖ ^ 2 ≤ B) : Ms.eventErr S Kf ε b J E c ^ 2 ≤ pairConst Ms.zc.dim Ms.δc S.Ξ Kf ^ 2 * dyadicGridLength Gd J.1 * D ^ 2 * B / ε

Blueprint line 2118 ("cross pairings are at most D_*^{-200} ... these squared additive errors are negligible"): the squared complementary pairing error of a side event is pairConst² |J| |E| |alive \ E| Σ |c|² / ε, at most pairConst² |J| D² B / ε when the alive modes number at most D and the coefficients have square sum at most B.

theorem TrilinearHT.Auto.columnL2Restriction_norm_sq_le {V : Type u_1} [Fintype V] (s : Set ℝ) (hs : MeasurableSet s) (g : ↥(ColumnL2 V)) : ‖(columnL2Restriction s hs) g‖ ^ 2 ≤ ‖g‖ ^ 2

Restriction to a set does not increase the squared norm.

theorem TrilinearHT.Auto.norm_sq_restrict_physEmbed_add {V : Type u_1} {W : Type u_2} {U : Type u_3} [Fintype V] [Fintype W] [Fintype U] (s : Set ℝ) (hs : MeasurableSet s) (x : ↥(ColumnL2 V)) (y : ↥(ColumnL2 W)) : ‖(columnL2Restriction s hs) ((physEmbed V U) x + (physEmbed W U) y)‖ ^ 2 ≤ 2 * ‖(columnL2Restriction s hs) x‖ ^ 2 + 2 * ‖y‖ ^ 2

Restricting a sum of physical embeddings costs twice the restricted first energy and twice the full second energy. This separates the rolling and fixed parts of a side state.

Per-group clearing integers (blueprint line 1890)

def TrilinearHT.Auto.ModeSchedule.withQ0 (S : ModeSchedule) (q : ℕ) : ModeSchedule

The schedule with the clearing integer Q₀ replaced by q (blueprint line 1890: Q₀ is chosen for each group center; eq:mode-parameters only uses an upper bound for it).

Equations

• S.withQ0 q = { dmax := S.dmax, Dstar := S.Dstar, Bstar := S.Bstar, Dm := S.Dm, Q0 := q, Cstar := S.Cstar, Rht := S.Rht, Jstar := S.Jstar, A0 := S.A0, H := S.H, T := S.T, K := S.K }

theorem TrilinearHT.Auto.ModeSchedule.Valid.withQ0 {S : ModeSchedule} {Cj CA CT CK : ℕ} {δs W : ℝ} (hV : S.Valid Cj CA CT CK δs W) (hD : 0 ≤ S.Dstar) (hB : 0 ≤ S.Bstar) {q : ℕ} (hq : q ≤ S.Q0) : (S.withQ0 q).Valid Cj CA CT CK δs W

eq:mode-parameters persists when the clearing integer is replaced by a smaller one: Q₀ enters only as a factor of the lower bound for H.

@[simp]

theorem TrilinearHT.Auto.ModeSchedule.withQ0_Dstar (S : ModeSchedule) (q : ℕ) : (S.withQ0 q).Dstar = S.Dstar

@[simp]

theorem TrilinearHT.Auto.ModeSchedule.withQ0_K (S : ModeSchedule) (q : ℕ) : (S.withQ0 q).K = S.K

@[simp]

theorem TrilinearHT.Auto.ModeSchedule.withQ0_Eh (S : ModeSchedule) (q h : ℕ) : (S.withQ0 q).Eh h = S.Eh h

theorem TrilinearHT.Auto.ModeSchedule.withQ0_box {S : ModeSchedule} {q : ℕ} (hq : q ≤ S.Q0) {X Y : ℝ} (hX : 0 ≤ X) (h : ↑S.Q0 * X ≤ Y) : ↑(S.withQ0 q).Q0 * X ≤ Y

Per-group box condition: a clearing integer below Q₀ inherits the frequency-box bound.

Linear sides from bounded frozen event projections (blueprint lines 2112-2118, 2160)

Global filters of the transfer steps (blueprint lines 2386-2391)

Variation of the global positive chains (blueprint lines 2390-2391, lem:variation)

Lift composition on the main columns (blueprint lem:lift-composition, lines 2062-2077)

noncomputable def TrilinearHT.Auto.piLpSingle {ι : Type u_1} [Fintype ι] [DecidableEq ι] (F : ι → Type u_2) [(G : ι) → NormedAddCommGroup (F G)] [(G : ι) → InnerProductSpace ℂ (F G)] (G : ι) : F G →L[ℂ] PiLp 2 F

The isometric embedding of one summand into the ℓ² sum of a finite family of inner product spaces.

Equations

• TrilinearHT.Auto.piLpSingle F G = (↑(WithLp.linearEquiv 2 ℂ ((G : ι) → F G)).symm ∘ₗ LinearMap.single ℂ F G).mkContinuous 1 ⋯

theorem TrilinearHT.Auto.norm_piLpSingle {ι : Type u_1} [Fintype ι] [DecidableEq ι] (F : ι → Type u_2) [(G : ι) → NormedAddCommGroup (F G)] [(G : ι) → InnerProductSpace ℂ (F G)] (G : ι) (v : F G) : ‖(piLpSingle F G) v‖ = ‖v‖

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.cell_ballFamT {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (l : Fin 4) (s : List (CatCol bf.Vtx)) (mb : bf.MainBudget s) (G : bf.Grp) (j : ℕ) (p : Fin fp.P) {I : ℤ × ℤ} (hI : I ∈ A.cells) : columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯ ∘SL (fp.ballFamT l s mb G j p).proj I.1 = cellColumnProjection (bf.mainTree fp.Mc s mb) (fp.ballMaskT l s mb G j p) ⋯

At an active cell the cell restriction after the ball depth projection is the cell projection of the main tree.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.gBall_restrict_comm {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (l : Fin 4) (s : List (CatCol bf.Vtx)) (mb : bf.MainBudget s) (G : bf.Grp) (j : ℕ) {I : ℤ × ℤ} (hI : I ∈ A.cells) : fp.gBall l s mb G j I.1 ∘SL columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯ = columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯ ∘SL fp.gBall l s mb G j I.1

The outer ball filter at the depth of an active cell commutes with the restriction to the cell.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.gBall_adjoint {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (l : Fin 4) (s : List (CatCol bf.Vtx)) (mb : bf.MainBudget s) (G : bf.Grp) (j : ℕ) (h : ℤ) : ContinuousLinearMap.adjoint (fp.gBall l s mb G j h) = fp.gBall l s mb G j h

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.main_rows_group {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (l : Fin 4) (s : List (CatCol bf.Vtx)) (mb : bf.MainBudget s) (G : bf.Grp) (j : ℕ) {ρ : Type u_1} {F : Type u_2} [Fintype ρ] [NormedAddCommGroup F] [NormedSpace ℂ F] (Q : ρ → ↥(ColumnL2 (bf.RLab fp.Mc s)) →L[ℂ] F) {c : ℝ} (hc : 0 ≤ c) (hQ : ∀ (x : ↥(ColumnL2 (bf.RLab fp.Mc s))), ∑ e : ρ, ‖(Q e) x‖ ^ 2 ≤ c * ‖x‖ ^ 2) (u : ρ → ℤ × ℤ) (hu : ∀ (e : ρ), u e ∈ A.cells) (hloc : ∀ (e : ρ), Q e ∘SL columnL2Restriction (dyadicGridCell A.G (u e).1 (u e).2) ⋯ = Q e) (y : ↥(ColumnL2 (bf.RLab fp.Mc s))) : ∑ e : ρ, ‖(Q e) ((fp.gBall l s mb G j (u e).1) y)‖ ^ 2 ≤ c * compression1 (bf.mainTree fp.Mc s mb) ^ 2 * ‖y‖ ^ 2

Blueprint lines 2068-2069 (lem:compression with one factor) for one group: rows Q_e on the relevant main columns, Bessel with constant c and local to active decision cells u_e, stay Bessel with constant c C₁² after inserting the outer averaged ball projection of the group at the depth of each decision cell.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.gBall_row_adjoint_mem {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (l : Fin 4) (s : List (CatCol bf.Vtx)) (mb : bf.MainBudget s) (G : bf.Grp) (j : ℕ) {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F] (Q : ↥(ColumnL2 (bf.RLab fp.Mc s)) →L[ℂ] F) {u : ℤ × ℤ} (hu : u ∈ A.cells) (hloc : Q ∘SL columnL2Restriction (dyadicGridCell A.G u.1 u.2) ⋯ = Q) (w : F) : (colRelabel (bf.rv fp.Mc s)) ((ContinuousLinearMap.adjoint (Q ∘SL fp.gBall l s mb G j u.1)) w) ∈ mainRange A.G fp.Mc (bf.origCols l) s u (fp.brank j) (fp.bmask u G j fp.P)

Blueprint lines 2070-2071 ("every term of A_G^* has outer factor L_{l,G,u_e}, so its range is a sum of whole usable main endpoint ranges"): for a row Q local to an active cell u, the adjoint of Q L_{l,G,u} takes values, after relabeling, in the main ball range of u at the largest pad.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.main_rows_joint {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (l : Fin 4) (s : List (CatCol bf.Vtx)) (hT : ∀ e ∈ s, ∃ R ∈ residueBox (bf.vtag e.tag).dim 9, ∃ (γ : ℝ), e = templateCol (bf.vtag e.tag) l R γ e.birth e.rank e.tag) (htag : ∀ e ∈ s, bf.occAvail (↑e.tag.2) e.tag.1) (d : bf.Vtx) (mb : bf.MainBudget s) {ι : Type u_1} {ρ : Type u_2} [Fintype ι] [Fintype ρ] (grp : ι → bf.Grp) (hgrp : Function.Injective grp) (k j : ℕ) (hPH : fp.bbase j + fp.P ≤ fp.Hmax) (F : ι → Type u_3) [(G : ι) → NormedAddCommGroup (F G)] [(G : ι) → InnerProductSpace ℂ (F G)] [∀ (G : ι), CompleteSpace (F G)] (Q : (G : ι) → ρ → ↥(ColumnL2 (bf.RLab fp.Mc s)) →L[ℂ] F G) {c : ℝ} (hc : 0 ≤ c) (hQ : ∀ (G : ι) (x : ↥(ColumnL2 (bf.RLab fp.Mc s))), ∑ e : ρ, ‖(Q G e) x‖ ^ 2 ≤ c * ‖x‖ ^ 2) (u : ι → ρ → ℤ × ℤ) (hu : ∀ (G : ι) (e : ρ), u G e ∈ A.cells) (hloc : ∀ (G : ι) (e : ρ), Q G e ∘SL columnL2Restriction (dyadicGridCell A.G (u G e).1 (u G e).2) ⋯ = Q G e) (hcert : ∀ (G : ι) (e : ρ), fp.Cert k (grp G) (u G e)) {ra rb : ℝ} (hroot : ∀ I ∈ A.cells, dyadicGridCell A.G I.1 I.2 ⊆ Set.Icc ra rb) {τ : ℝ} (hτ : 0 < τ) (hτ1 : τ ≤ 1) (hHed : Real.exp (↑A.Dg * (1 + Real.log A.Hsrc + Real.log τ⁻¹) ^ A.Dg) ≤ fp.Hed) {N : ℕ} (hN : ∀ (y : ℝ), {q : ι × (bf.Lab ⊕ Fin fp.Mc) | ∃ I ∈ A.cells, (∃ (k' : ℕ), fp.Cert k' (grp q.1) I) ∧ ∃ (p : Fin fp.P), y ∈ dyadicGridCell A.G I.1 I.2 ∧ q.2 ∈ mainLabelsM A.G fp.Mc (bf.origCols l) s I (fp.brank j) (fp.bmask I (grp q.1) j (↑p + 1)) d}.card ≤ N) (x : ↥(ColumnL2 (bf.RLab fp.Mc s))) : ∑ G : ι, ∑ e : ρ, ‖(Q G e) ((fp.gBall l s mb (grp G) j (u G e).1) x)‖ ^ 2 ≤ (1 + τ * ↑N * A.colBudget ^ 2) * (c * compression1 (bf.mainTree fp.Mc s mb) ^ 2) * ‖x‖ ^ 2

Blueprint lem:lift-composition, lines 2066-2071, on the main columns: rows Q_{G,e} on the relevant main columns, Bessel with constant c within each group of one color k and local to active decision cells u_{G,e} with downstream use certificates of G, stay jointly Bessel over all groups after inserting the outer averaged ball projections L_{l,G,u_{G,e}} at their decision cells. Per group this is lem:compression with one factor (cost C₁², main_rows_group); across the groups the adjoint outputs are sums of whole main ball ranges at the decision cells (gBall_row_adjoint_mem), and eq:whole-ranges gives the factor 1 + τ N colBudget².

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.lift_rows_history {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (l : Fin 4) (s : List (CatCol bf.Vtx)) (mb : bf.MainBudget s) {ι : Type u_1} {ρ : Type u_2} [Fintype ι] [Fintype ρ] (grp : ι → bf.Grp) (j : ℕ) (ls : List (ℕ × Bool)) (jb : Fin 2) (F : ι → Type u_3) [(G : ι) → NormedAddCommGroup (F G)] [(G : ι) → InnerProductSpace ℂ (F G)] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℂ E] (emb : (G : ι) → F G →L[ℂ] E) (hemb : ∀ (G : ι) (v : F G), ‖(emb G) v‖ = ‖v‖) (Q : (G : ι) → ρ → ↥(ColumnL2 (bf.RLab fp.Mc s)) →L[ℂ] F G) (u : ι → ρ → ℤ × ℤ) (hu : ∀ (G : ι) (e : ρ), u G e ∈ A.cells) (hloc : ∀ (G : ι) (e : ρ), Q G e ∘SL columnL2Restriction (dyadicGridCell A.G (u G e).1 (u G e).2) ⋯ = Q G e) {B : ℝ} (hB : 0 ≤ B) (hjoint : ∀ (x : ↥(ColumnL2 (bf.RLab fp.Mc s))), ∑ G : ι, ∑ e : ρ, ‖(Q G e) ((fp.gBall l s mb (grp G) j (u G e).1) x)‖ ^ 2 ≤ B * ‖x‖ ^ 2) (Z : ↥(ColumnL2 (bf.P l jb).V)) : ∑ G : ι, ∑ e : ρ, ‖(Q G e) ((fp.gOut l s mb (grp G) j ls (u G e).1) ((bf.famEmbR fp.Mc s l jb) (((bf.P l jb).Ψ.proj (u G e).1) Z)))‖ ^ 2 ≤ B * compressionC (bf.mainTree fp.Mc s mb) ls.length ^ 2 * compression1 (bf.P l jb).Ψ.D ^ 2 * ‖Z‖ ^ 2

Blueprint lines 2072-2075 ("apply compression again, with decision cells u_e, to insert those histories and the constituent basic projections acting on F_l"): rows Q_{G,e} local to active decision cells that are jointly Bessel with constant B after the outer ball projections stay jointly Bessel after inserting the shared history and the basic depth projection of the family j_b, at the cost C_{|ls|}² C_{1,j_b}² of basic_compression.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.row_out_restrictR {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (hne : A.cells.Nonempty) (l : Fin 4) (s : List (CatCol bf.Vtx)) (mb : bf.MainBudget s) (G : bf.Grp) (j : ℕ) (ls : List (ℕ × Bool)) (jb : Fin 2) {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] (Q : ↥(ColumnL2 (bf.RLab fp.Mc s)) →L[ℂ] F) {u : ℤ × ℤ} (hu : u ∈ A.cells) (hloc : Q ∘SL columnL2Restriction (dyadicGridCell A.G u.1 u.2) ⋯ = Q) (Z : ↥(ColumnL2 (bf.P l jb).V)) : Q ((fp.gOut l s mb G j ls u.1) ((bf.famEmbR fp.Mc s l jb) (((bf.P l jb).Ψ.proj u.1) Z))) = Q ((fp.gOut l s mb G j ls u.1) ((bf.famEmbR fp.Mc s l jb) (((bf.P l jb).Ψ.proj u.1) ((columnL2Restriction (dyadicGridCell A.G A.R.1 A.R.2) ⋯) Z))))

Rows local to an active cell see the input of a basic family only through its restriction to the attempt root (blueprint line 2075: ‖F_l‖₂² ≤ |R|).

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.lift_rows_bessel {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (s : List (CatCol bf.Vtx)) {Md : Type} [Fintype Md] (L : LiftData (bf.Lab ⊕ Fin fp.Mc) Md) {ρ : Type u_1} {F : Type u_2} [Fintype ρ] [NormedAddCommGroup F] [NormedSpace ℂ F] (P : ρ → ↥(ColumnL2 Md) →L[ℂ] F) {c : ℝ} (hc : 0 ≤ c) (hP : ∀ (x : ↥(ColumnL2 Md)), ∑ e : ρ, ‖(P e) x‖ ^ 2 ≤ c * ‖x‖ ^ 2) (x : ↥(ColumnL2 (bf.RLab fp.Mc s))) : ∑ e : ρ, ‖(P e ∘SL L.op ∘SL colRelabel (bf.rv fp.Mc s)) x‖ ^ 2 ≤ 5 * c * ‖x‖ ^ 2

The mode rows after the lift: Q_{G,e} = P_{G,e} R_{l,G} on the relevant main columns are Bessel with constant 5c within each group (the lift has norm at most √5).

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.lift_rows_local {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (s : List (CatCol bf.Vtx)) {Md : Type} [Fintype Md] (L : LiftData (bf.Lab ⊕ Fin fp.Mc) Md) {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] (P : ↥(ColumnL2 Md) →L[ℂ] F) {t : Set ℝ} (ht : MeasurableSet t) (hloc : P ∘SL columnL2Restriction t ht = P) : (P ∘SL L.op ∘SL colRelabel (bf.rv fp.Mc s)) ∘SL columnL2Restriction t ht = P ∘SL L.op ∘SL colRelabel (bf.rv fp.Mc s)

The mode rows after the lift stay local to a cell when the mode rows are.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.lift_composition_global {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (l : Fin 4) (s : List (CatCol bf.Vtx)) (hT : ∀ e ∈ s, ∃ R ∈ residueBox (bf.vtag e.tag).dim 9, ∃ (γ : ℝ), e = templateCol (bf.vtag e.tag) l R γ e.birth e.rank e.tag) (htag : ∀ e ∈ s, bf.occAvail (↑e.tag.2) e.tag.1) (d : bf.Vtx) (mb : bf.MainBudget s) (hne : A.cells.Nonempty) {ι : Type u_1} {ρ : Type u_2} [Fintype ι] [Fintype ρ] (grp : ι → bf.Grp) (hgrp : Function.Injective grp) (k j : ℕ) (hPH : fp.bbase j + fp.P ≤ fp.Hmax) (ls : List (ℕ × Bool)) (Md : ι → Type) [(G : ι) → Fintype (Md G)] (L : (G : ι) → LiftData (bf.Lab ⊕ Fin fp.Mc) (Md G)) (F : ι → Type u_3) [(G : ι) → NormedAddCommGroup (F G)] [(G : ι) → InnerProductSpace ℂ (F G)] [∀ (G : ι), CompleteSpace (F G)] (P : (G : ι) → ρ → ↥(ColumnL2 (Md G)) →L[ℂ] F G) {c : ℝ} (hc : 0 ≤ c) (hP : ∀ (G : ι) (x : ↥(ColumnL2 (Md G))), ∑ e : ρ, ‖(P G e) x‖ ^ 2 ≤ c * ‖x‖ ^ 2) (u : ι → ρ → ℤ × ℤ) (hu : ∀ (G : ι) (e : ρ), u G e ∈ A.cells) (hloc : ∀ (G : ι) (e : ρ), P G e ∘SL columnL2Restriction (dyadicGridCell A.G (u G e).1 (u G e).2) ⋯ = P G e) (hcert : ∀ (G : ι) (e : ρ), fp.Cert k (grp G) (u G e)) {ra rb : ℝ} (hroot : ∀ I ∈ A.cells, dyadicGridCell A.G I.1 I.2 ⊆ Set.Icc ra rb) {τ : ℝ} (hτ : 0 < τ) (hτ1 : τ ≤ 1) (hHed : Real.exp (↑A.Dg * (1 + Real.log A.Hsrc + Real.log τ⁻¹) ^ A.Dg) ≤ fp.Hed) {N : ℕ} (hN : ∀ (y : ℝ), {q : ι × (bf.Lab ⊕ Fin fp.Mc) | ∃ I ∈ A.cells, (∃ (k' : ℕ), fp.Cert k' (grp q.1) I) ∧ ∃ (p : Fin fp.P), y ∈ dyadicGridCell A.G I.1 I.2 ∧ q.2 ∈ mainLabelsM A.G fp.Mc (bf.origCols l) s I (fp.brank j) (fp.bmask I (grp q.1) j (↑p + 1)) d}.card ≤ N) : ∑ G : ι, ∑ e : ρ, ‖(P G e) ((L G).op (fp.basicOut l s mb (grp G) j ls (u G e).1))‖ ^ 2 ≤ 2 * ((1 + τ * ↑N * A.colBudget ^ 2) * (5 * c * compression1 (bf.mainTree fp.Mc s mb) ^ 2) * compressionC (bf.mainTree fp.Mc s mb) ls.length ^ 2 * (compression1 (bf.P l 0).Ψ.D ^ 2 + compression1 (bf.P l 1).Ψ.D ^ 2)) * dyadicGridLength A.G A.R.1

Blueprint lem:lift-composition (lines 2062-2077) on the main columns of a basic slot l, for the groups of one color k (with the ball level j and the shared history ls of a leaf of the color search), with the global coarse outputs: let L_G be the mode lift R_{l,G} of the group G, and let the mode projection rows P_{G,e} be Bessel with constant c within each group and local to active decision cells u_{G,e} with downstream use certificates. Then the outputs P_{G,e} R_{l,G} Z_{l,G,u_{G,e}} of the global coarse outputs at the depths of their decision cells have joint squared sum at most 2 (1 + τ N colBudget²) 5c C₁² C_{|ls|}² (C_{1,0}² + C_{1,1}²) |R|.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.liftConst_le_G0 {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (l : Fin 4) (s : List (CatCol bf.Vtx)) (mb : bf.MainBudget s) (ls : List (ℕ × Bool)) {c : ℝ} (hc : 0 ≤ c) {τ : ℝ} (hτ : 0 < τ) {N : ℕ} (hτN : τ * ↑N * A.colBudget ^ 2 ≤ 1) (cc : ℕ) (hcc : 1 ≤ cc) {kk : ℝ} (hk : 1 ≤ kk) (hDm : Real.log (2 * mb.B) ≤ kk ^ cc) (hDb : Real.log (2 * A.colBudget) ≤ kk ^ cc) (hn : ↑ls.length ≤ ↑cc * (Real.log kk + 1)) : 2 * ((1 + τ * ↑N * A.colBudget ^ 2) * (5 * c * compression1 (bf.mainTree fp.Mc s mb) ^ 2) * compressionC (bf.mainTree fp.Mc s mb) ls.length ^ 2 * (compression1 (bf.P l 0).Ψ.D ^ 2 + compression1 (bf.P l 1).Ψ.D ^ 2)) ≤ c * Real.exp ((6144 * (↑cc + 1) * (1024 * (↑cc + 1) + ↑cc + 7) + 4) * (1 + Real.log (2 * kk)) ^ 2)

The constant of lift_composition_global is at most c G₀ with G₀ = exp(C_q (1 + log 2k)²), C_q = 6144 (c+1) (1024 (c+1) + c + 7) + 4, under log (2 D_m) ≤ k^c, log (2 colBudget) ≤ k^c, shared histories of O(log k) factors and the pair threshold τ N colBudget² ≤ 1 (blueprint lines 2072-2077: "the loss is G₀").

Level rows of the side events at the chosen schedule (blueprint lines 2114-2116)

theorem TrilinearHT.Auto.ModeSchedule.pairConst_mul_le (S : ModeSchedule) (hD : 2 ≤ S.Dstar) {d : ℕ} {δ : ℝ} {Kf : ℕ} (hDg : gaugeSqNorm d δ ≤ S.Dstar) (hKf : 2 * gaugeTail d δ / 2 ^ Kf * S.Dstar ^ 300 ≤ 1) : pairConst d δ S.Ξ Kf * S.Dstar ^ 200 ≤ 1

Blueprint line 2055 at the chosen schedule ("the Fourier sum and tail give C D_*/Ξ + D_*^{-300} ≤ D_*^{-200}"): when D_* covers the full Fourier norm of the squared gauge and the truncation leaves a tail at most D_*^{-300}, the pairing constant is at most D_*^{-200} (with Ξ = D_*^{1000}).

theorem TrilinearHT.Auto.ModeSystem.group_event_rows_schedule {Gd : RealDyadicGrid} {Mc : ℕ} (Ms : ModeSystem Gd Mc) (S : ModeSchedule) {Cj CA CT CK : ℕ} {δs W : ℝ} (hV : S.Valid Cj CA CT CK δs W) (hCj : 340 ≤ Cj) (hCA : 1 ≤ CA) (hδs : 0 < δs) (hδ1 : δs ≤ 1) (hd2 : 2 ≤ S.dmax) (hD : 2 ≤ S.Dstar) (hB : 2 ≤ S.Bstar) (hQ : 1 ≤ S.Q0) (hDm : 2 ≤ S.Dm) (hW : 8 * (↑S.dmax + 1) ^ 3 * Real.log (2 * S.H) / Real.log 2 ≤ W) (hdim : ∀ (p : Ms.Key), Ms.dvOf p + Ms.zc.dim ≤ S.dmax) {M : ℕ} (hM1 : 1 ≤ M) (hMD : ↑M ≤ 2 * S.Dm) (hM : ∀ (U : ℤ × ℤ), (Finset.image Ms.keyOf (Ms.alive U)).card ≤ M) (R₀ : ℤ) (Bs : Finset ℤ) (cells : ℤ → Finset (ℤ × ℤ)) (hdepth : ∀ b ∈ Bs, ∀ J ∈ cells b, J.1 = b - 2 * ↑S.K) (hgrid : ∀ b ∈ Bs, ↑S.K ∣ b - R₀) (hδ : 0 < Ms.δc) (hΛ : Ms.Λ ≤ S.Dstar) (Kf : ℕ) (hDg : gaugeSqNorm Ms.zc.dim Ms.δc ≤ S.Dstar) (hKf : 2 * gaugeTail Ms.zc.dim Ms.δc / 2 ^ Kf * S.Dstar ^ 300 ≤ 1) (hBox : ↑S.Q0 * 2 ^ (Kf + 1) ≤ S.Bstar) (hεw : ∀ (m : Ms.Md), S.Dstar⁻¹ ≤ Ms.L.εM m) (hpt : ∀ (y : ℝ), ↑(Ms.ptSet y).card ≤ S.Dstar) [inst : ∀ (J : ℤ × ℤ) (E : Finset Ms.Md), (Submodule.span ℂ (Ms.cellMode J '' ↑E)).HasOrthogonalProjection] (F : ↥(ColumnL2 Ms.Md)) : ∑ e ∈ Ms.events S ⋯ (S.sideParams δs) Bs cells, ‖(Submodule.span ℂ (Ms.cellMode e.2.1 '' ↑e.2.2)).starProjection F‖ ^ 2 ≤ 6 * (↑⌊180 * ↑S.dmax * Real.log (2 * S.Dm) / δs⌋₊ + 1) * ‖F‖ ^ 2

Blueprint lines 2114-2116 at the chosen schedule, for one group: give the side events their longest-chain level within each of the three classes of blocks; events of one level on overlapping cells have neither shared nor adjacent modes, and their mode sets are disjoint along paths with at most D_* modes through each point. Lemma mode-rows (cross pairings at most D_*^{-200} by ModeSchedule.pairConst_mul_le, inverse private weights at most D_*) gives Bessel rows for each level, and the chains have length at most 180 d_max log(2 D_m)/δ_* (eq:bad-density), so the side-event rows of the group are Bessel with constant 6 (⌊180 d_max log(2 D_m)/δ_*⌋ + 1).

Exact side subtotals and their errors (blueprint line 2118)

theorem TrilinearHT.Auto.sum_sum_measureReal_le_of_count {ι : Type u_1} {α : ι → Type u_2} (u : Finset ι) (s : (G : ι) → Finset (α G)) (J : (G : ι) → α G → Set ℝ) (hJ : ∀ (G : ι) (e : α G), MeasurableSet (J G e)) {R : Set ℝ} (hRf : MeasureTheory.volume R ≠ ⊤) (hJR : ∀ G ∈ u, ∀ e ∈ s G, J G e ⊆ R) {N : ℕ} (hN : ∀ y ∈ R, ∑ G ∈ u, {e ∈ s G | y ∈ J G e}.card ≤ N) : ∑ G ∈ u, ∑ e ∈ s G, MeasureTheory.volume.real (J G e) ≤ ↑N * MeasureTheory.volume.real R

Blueprint eq:path in counting form, for a family of families of sets: sets inside R, of which at most N pass through each point of R, have total length at most N |R|.

theorem TrilinearHT.Auto.ModeSystem.class_count {Gd : RealDyadicGrid} {Mc : ℕ} (Ms : ModeSystem Gd Mc) (S : ModeSchedule) (hA : 6 ≤ S.A0) (SP : SideParams) (s : Finset Ms.Event) (hev : ∀ e ∈ s, e.2.2 ∈ Ms.sideEvents S hA SP e.1 e.2.1) (hdepth : ∀ e ∈ s, e.2.1.1 = e.1 - 2 * ↑S.K) {L : ℕ} (hL : ∀ (k : ℕ) (e : Ms.Event), LinkedChain (↑s) (Ms.Linked S) k e → k ≤ L) (y : ℝ) : {e ∈ s | y ∈ Ms.evCell e}.card ≤ (L + 1) * (Ms.ptSet y).card

Blueprint line 2118 ("the number of events along a path in one level is at most D_*"): in one class whose chains have at most L links, the side events through a point y number at most (L + 1) |ptSet y|, since the events of one longest-chain level through y have pairwise disjoint sets of modes through y.

theorem TrilinearHT.Auto.ModeSystem.group_count {Gd : RealDyadicGrid} {Mc : ℕ} (Ms : ModeSystem Gd Mc) (S : ModeSchedule) {Cj CA CT CK : ℕ} {δs W : ℝ} (hV : S.Valid Cj CA CT CK δs W) (hCj : 340 ≤ Cj) (hCA : 1 ≤ CA) (hδs : 0 < δs) (hδ1 : δs ≤ 1) (hd2 : 2 ≤ S.dmax) (hD : 2 ≤ S.Dstar) (hB : 2 ≤ S.Bstar) (hQ : 1 ≤ S.Q0) (hDm : 2 ≤ S.Dm) (hW : 8 * (↑S.dmax + 1) ^ 3 * Real.log (2 * S.H) / Real.log 2 ≤ W) (hdim : ∀ (p : Ms.Key), Ms.dvOf p + Ms.zc.dim ≤ S.dmax) {M : ℕ} (hM1 : 1 ≤ M) (hMD : ↑M ≤ 2 * S.Dm) (hM : ∀ (U : ℤ × ℤ), (Finset.image Ms.keyOf (Ms.alive U)).card ≤ M) (R₀ : ℤ) (Bs : Finset ℤ) (cells : ℤ → Finset (ℤ × ℤ)) (hdepth : ∀ b ∈ Bs, ∀ J ∈ cells b, J.1 = b - 2 * ↑S.K) (hgrid : ∀ b ∈ Bs, ↑S.K ∣ b - R₀) (y : ℝ) : {e ∈ Ms.events S ⋯ (S.sideParams δs) Bs cells | y ∈ Ms.evCell e}.card ≤ 3 * (⌊180 * ↑S.dmax * Real.log (2 * S.Dm) / δs⌋₊ + 1) * (Ms.ptSet y).card

Blueprint line 2118 at the chosen schedule, for one group: the side events through a point y number at most 3 (⌊180 d_max log(2 D_m)/δ_*⌋ + 1) |ptSet y| (three classes, longest-chain levels bounded by eq:bad-density, disjoint mode sets through y on each level).

theorem TrilinearHT.Auto.ModeSystem.side_errors_negligible (S : ModeSchedule) {Cj CA CT CK : ℕ} {δs W : ℝ} (hV : S.Valid Cj CA CT CK δs W) (hCj : 340 ≤ Cj) (hCA : 1 ≤ CA) (hδs : 0 < δs) (hδ1 : δs ≤ 1) (hd2 : 2 ≤ S.dmax) (hD : 2 ≤ S.Dstar) (hB : 2 ≤ S.Bstar) (_hQ : 1 ≤ S.Q0) (hDm : 2 ≤ S.Dm) (hW : 8 * (↑S.dmax + 1) ^ 3 * Real.log (2 * S.H) / Real.log 2 ≤ W) {Gd : RealDyadicGrid} {Mc : ℕ} {ι : Type u_1} [Fintype ι] (Ms : ι → ModeSystem Gd Mc) (q : ι → ℕ) (hq : ∀ (G : ι), 1 ≤ q G ∧ q G ≤ S.Q0) (hdim : ∀ (G : ι) (p : (Ms G).Key), (Ms G).dvOf p + (Ms G).zc.dim ≤ S.dmax) {M : ℕ} (hM1 : 1 ≤ M) (hMD : ↑M ≤ 2 * S.Dm) (hM : ∀ (G : ι) (U : ℤ × ℤ), (Finset.image (Ms G).keyOf ((Ms G).alive U)).card ≤ M) (R₀ : ℤ) (Bs : ι → Finset ℤ) (cells : ι → ℤ → Finset (ℤ × ℤ)) (hdepth : ∀ (G : ι), ∀ b ∈ Bs G, ∀ J ∈ cells G b, J.1 = b - 2 * ↑S.K) (hgrid : ∀ (G : ι), ∀ b ∈ Bs G, ↑S.K ∣ b - R₀) {R : ℤ × ℤ} (hcR : ∀ (G : ι), ∀ b ∈ Bs G, ∀ J ∈ cells G b, dyadicGridCell Gd J.1 J.2 ⊆ dyadicGridCell Gd R.1 R.2) (hδc : ∀ (G : ι), 0 < (Ms G).δc) (Kf : ℕ) (hDg : ∀ (G : ι), gaugeSqNorm (Ms G).zc.dim (Ms G).δc ≤ S.Dstar) (hKf : ∀ (G : ι), 2 * gaugeTail (Ms G).zc.dim (Ms G).δc / 2 ^ Kf * S.Dstar ^ 300 ≤ 1) (halive : ∀ (G : ι) (U : ℤ × ℤ), ↑((Ms G).alive U).card ≤ S.Dstar) (hpath : ∀ (y : ℝ), ∑ G : ι, ↑((Ms G).ptSet y).card ≤ S.Dstar) (c : (G : ι) → ℤ → ℤ × ℤ → (Ms G).Md → ℂ) {Bc : ℝ} (hBc : 0 ≤ Bc) (hc : ∀ (G : ι), ∀ b ∈ Bs G, ∀ J ∈ cells G b, ∑ m ∈ (Ms G).alive (ancAt Gd J (b - 4 * ↑S.K)), ‖c G b J m‖ ^ 2 ≤ Bc) : (∀ (G : ι), ∀ b ∈ Bs G, ∀ J ∈ cells G b, ∀ E ∈ (Ms G).sideEvents (S.withQ0 (q G)) ⋯ (S.sideParams δs) b J, (Ms G).eventErr (S.withQ0 (q G)) Kf S.Dstar⁻¹ b J E (c G b J) ^ 2 * S.Dstar ^ 397 ≤ Bc * dyadicGridLength Gd J.1) ∧ (∑ G : ι, ∑ b ∈ Bs G, ∑ J ∈ cells G b, ∑ E ∈ (Ms G).sideEvents (S.withQ0 (q G)) ⋯ (S.sideParams δs) b J, (Ms G).eventErr (S.withQ0 (q G)) Kf S.Dstar⁻¹ b J E (c G b J) ^ 2) * S.Dstar ^ 396 ≤ 3 * (↑⌊180 * ↑S.dmax * Real.log (2 * S.Dm) / δs⌋₊ + 1) * Bc * dyadicGridLength Gd R.1

Blueprint line 2118 at the chosen schedule ("pair them against a unit vector of the augmented range ... hence ‖P_{E,J} ZTilde - T_{E,J}‖_{2,J} ≤ D_*^{-190}; the number of events along a path in one level is at most D_*, and all groups are included in the path budget; these squared additive errors are negligible"). For the groups G with their frozen coefficients c_{G,b,J} (squared coefficient sums at most B_c on every pre-cell), at most D_* modes alive at any cell, cross pairings at most D_*^{-200} and at most D_* modes through each point across the groups (the path budget), the error of each exact side subtotal (event_subtotal_close) satisfies err² ≤ B_c |J| / D_*^{397}, and the total over all groups, blocks, pre-cells inside the root and side events is at most 3 (⌊180 d_max log(2 D_m)/δ_*⌋ + 1) B_c |R| / D_*^{396}.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.lift_composition_finset {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (l : Fin 4) (s : List (CatCol bf.Vtx)) (hT : ∀ e ∈ s, ∃ R ∈ residueBox (bf.vtag e.tag).dim 9, ∃ (γ : ℝ), e = templateCol (bf.vtag e.tag) l R γ e.birth e.rank e.tag) (htag : ∀ e ∈ s, bf.occAvail (↑e.tag.2) e.tag.1) (d : bf.Vtx) (mb : bf.MainBudget s) (hne : A.cells.Nonempty) {ι : Type u_1} {ρ : Type u_2} [Fintype ι] (grp : ι → bf.Grp) (hgrp : Function.Injective grp) (k j : ℕ) (hPH : fp.bbase j + fp.P ≤ fp.Hmax) (ls : List (ℕ × Bool)) (Md : ι → Type) [(G : ι) → Fintype (Md G)] (L : (G : ι) → LiftData (bf.Lab ⊕ Fin fp.Mc) (Md G)) (F : ι → Type u_3) [(G : ι) → NormedAddCommGroup (F G)] [(G : ι) → InnerProductSpace ℂ (F G)] [∀ (G : ι), CompleteSpace (F G)] (T : ι → Finset ρ) (P : (G : ι) → ρ → ↥(ColumnL2 (Md G)) →L[ℂ] F G) {c : ℝ} (hc : 0 ≤ c) (hP : ∀ (G : ι) (x : ↥(ColumnL2 (Md G))), ∑ e ∈ T G, ‖(P G e) x‖ ^ 2 ≤ c * ‖x‖ ^ 2) (u : ι → ρ → ℤ × ℤ) (hu : ∀ (G : ι), ∀ e ∈ T G, u G e ∈ A.cells) (hloc : ∀ (G : ι), ∀ e ∈ T G, P G e ∘SL columnL2Restriction (dyadicGridCell A.G (u G e).1 (u G e).2) ⋯ = P G e) (hcert : ∀ (G : ι), ∀ e ∈ T G, fp.Cert k (grp G) (u G e)) {ra rb : ℝ} (hroot : ∀ I ∈ A.cells, dyadicGridCell A.G I.1 I.2 ⊆ Set.Icc ra rb) {τ : ℝ} (hτ : 0 < τ) (hτ1 : τ ≤ 1) (hHed : Real.exp (↑A.Dg * (1 + Real.log A.Hsrc + Real.log τ⁻¹) ^ A.Dg) ≤ fp.Hed) {N : ℕ} (hN : ∀ (y : ℝ), {q : ι × (bf.Lab ⊕ Fin fp.Mc) | ∃ I ∈ A.cells, (∃ (k' : ℕ), fp.Cert k' (grp q.1) I) ∧ ∃ (p : Fin fp.P), y ∈ dyadicGridCell A.G I.1 I.2 ∧ q.2 ∈ mainLabelsM A.G fp.Mc (bf.origCols l) s I (fp.brank j) (fp.bmask I (grp q.1) j (↑p + 1)) d}.card ≤ N) : ∑ G : ι, ∑ e ∈ T G, ‖(P G e) ((L G).op (fp.basicOut l s mb (grp G) j ls (u G e).1))‖ ^ 2 ≤ 2 * ((1 + τ * ↑N * A.colBudget ^ 2) * (5 * c * compression1 (bf.mainTree fp.Mc s mb) ^ 2) * compressionC (bf.mainTree fp.Mc s mb) ls.length ^ 2 * (compression1 (bf.P l 0).Ψ.D ^ 2 + compression1 (bf.P l 1).Ψ.D ^ 2)) * dyadicGridLength A.G A.R.1

Blueprint lem:lift-composition (lines 2062-2077) with the global coarse outputs, for rows indexed by finite sets T_G depending on the group (as the side events of prop:linear-side): mode projection rows P_{G,e}, e ∈ T_G, Bessel with constant c within each group and local to active decision cells u_{G,e} with downstream use certificates, give outputs P_{G,e} R_{l,G} Z_{l,G,u_{G,e}} with joint squared sum at most the constant of lift_composition_global times |R|. The rows are padded by zero rows to one finite index type, and groups without rows are dropped.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.lift_composition_dep {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (l : Fin 4) (s : List (CatCol bf.Vtx)) (hT : ∀ e ∈ s, ∃ R ∈ residueBox (bf.vtag e.tag).dim 9, ∃ (γ : ℝ), e = templateCol (bf.vtag e.tag) l R γ e.birth e.rank e.tag) (htag : ∀ e ∈ s, bf.occAvail (↑e.tag.2) e.tag.1) (d : bf.Vtx) (mb : bf.MainBudget s) (hne : A.cells.Nonempty) {ι : Type u_1} [Fintype ι] {ρ : ι → Type u_2} (grp : ι → bf.Grp) (hgrp : Function.Injective grp) (k j : ℕ) (hPH : fp.bbase j + fp.P ≤ fp.Hmax) (ls : List (ℕ × Bool)) (Md : ι → Type) [(G : ι) → Fintype (Md G)] (L : (G : ι) → LiftData (bf.Lab ⊕ Fin fp.Mc) (Md G)) (F : ι → Type u_3) [(G : ι) → NormedAddCommGroup (F G)] [(G : ι) → InnerProductSpace ℂ (F G)] [∀ (G : ι), CompleteSpace (F G)] (T : (G : ι) → Finset (ρ G)) (P : (G : ι) → ρ G → ↥(ColumnL2 (Md G)) →L[ℂ] F G) {c : ℝ} (hc : 0 ≤ c) (hP : ∀ (G : ι) (x : ↥(ColumnL2 (Md G))), ∑ e ∈ T G, ‖(P G e) x‖ ^ 2 ≤ c * ‖x‖ ^ 2) (u : (G : ι) → ρ G → ℤ × ℤ) (hu : ∀ (G : ι), ∀ e ∈ T G, u G e ∈ A.cells) (hloc : ∀ (G : ι), ∀ e ∈ T G, P G e ∘SL columnL2Restriction (dyadicGridCell A.G (u G e).1 (u G e).2) ⋯ = P G e) (hcert : ∀ (G : ι), ∀ e ∈ T G, fp.Cert k (grp G) (u G e)) {ra rb : ℝ} (hroot : ∀ I ∈ A.cells, dyadicGridCell A.G I.1 I.2 ⊆ Set.Icc ra rb) {τ : ℝ} (hτ : 0 < τ) (hτ1 : τ ≤ 1) (hHed : Real.exp (↑A.Dg * (1 + Real.log A.Hsrc + Real.log τ⁻¹) ^ A.Dg) ≤ fp.Hed) {N : ℕ} (hN : ∀ (y : ℝ), {q : ι × (bf.Lab ⊕ Fin fp.Mc) | ∃ I ∈ A.cells, (∃ (k' : ℕ), fp.Cert k' (grp q.1) I) ∧ ∃ (p : Fin fp.P), y ∈ dyadicGridCell A.G I.1 I.2 ∧ q.2 ∈ mainLabelsM A.G fp.Mc (bf.origCols l) s I (fp.brank j) (fp.bmask I (grp q.1) j (↑p + 1)) d}.card ≤ N) : ∑ G : ι, ∑ e ∈ T G, ‖(P G e) ((L G).op (fp.basicOut l s mb (grp G) j ls (u G e).1))‖ ^ 2 ≤ 2 * ((1 + τ * ↑N * A.colBudget ^ 2) * (5 * c * compression1 (bf.mainTree fp.Mc s mb) ^ 2) * compressionC (bf.mainTree fp.Mc s mb) ls.length ^ 2 * (compression1 (bf.P l 0).Ψ.D ^ 2 + compression1 (bf.P l 1).Ψ.D ^ 2)) * dyadicGridLength A.G A.R.1

lift_composition_finset for rows indexed by finite sets T_G of types ρ_G depending on the group (as the side events (b, J, E) of the mode system of G).

Assembly of eq:linear-energy on the main columns (blueprint lines 2080-2118)

theorem TrilinearHT.Auto.augmentedMode_eq_add {Md : Type u_1} {inst : DecidableEq Md} (ψphys : Md → ℂ) (εM : Md → ℝ) (m : Md) : augmentedMode ψphys εM m = ψphys m • EuclideanSpace.single none 1 + ↑√(εM m) • EuclideanSpace.single (some m) 1

The augmented mode as a sum of its physical and private parts.

theorem TrilinearHT.Auto.ModeSystem.cellMode_vanish {Gd : RealDyadicGrid} {Mc : ℕ} (Ms : ModeSystem Gd Mc) (J : ℤ × ℤ) (m : Ms.Md) : ∀ᵐ (y : ℝ), y ∉ dyadicGridCell Gd J.1 J.2 → ↑↑(Ms.cellMode J m) y = 0

A cell mode vanishes off its cell.

theorem TrilinearHT.Auto.ModeSystem.frozenEval_eq_restrict {Gd : RealDyadicGrid} {Mc : ℕ} (Ms : ModeSystem Gd Mc) (S : ModeSchedule) (b : ℤ) (J : ℤ × ℤ) (β : Ms.Md → ℂ) (X : ↥(ColumnL2 Ms.Md)) (hX : ∀ᵐ (y : ℝ), y ∈ dyadicGridCell Gd J.1 J.2 → ↑↑X y = ∑ m : Ms.Md, β m • augmentedMode (fun (m : Ms.Md) => Ms.wave m y) Ms.L.εM m) (hβ : ∀ (m : Ms.Md), β m ≠ 0 → m ∈ Ms.alive (ancAt Gd J (b - 4 * ↑S.K))) : Ms.frozenEval S b J β = (columnL2Restriction (dyadicGridCell Gd J.1 J.2) ⋯) X

Blueprint line 1967 on a retained pre-cell: a column function that agrees on the cell J with the augmented-mode combination Σ_m β_m ψ_m, with β supported on the modes alive at the decision cell u_b, restricts on J to the frozen evaluation Σ_{m alive} β_m Ψ_m.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.norm_basicCell_le {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} (bf : A.BasicFamilies) (l : Fin 4) (jb : Fin 2) {I : ℤ × ℤ} (hI : I ∈ A.cells) : ‖(cellColumnProjection (bf.P l jb).Ψ.D (bf.P l jb).Ψ.A ⋯) (bf.P l jb).Z‖ ≤ ‖(columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯) (bf.P l jb).Z‖

A basic cell projection of a family input is at most the input on the cell.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.norm_basicOut_cell_le {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (l : Fin 4) (s : List (CatCol bf.Vtx)) (mb : bf.MainBudget s) (G : bf.Grp) (j : ℕ) (ls : List (ℕ × Bool)) {U : ℤ × ℤ} (hU : U ∈ A.cells) : ‖(columnL2Restriction (dyadicGridCell A.G U.1 U.2) ⋯) (fp.basicOut l s mb G j ls U.1)‖ ≤ ‖(columnL2Restriction (dyadicGridCell A.G U.1 U.2) ⋯) (bf.P l 0).Z‖ + ‖(columnL2Restriction (dyadicGridCell A.G U.1 U.2) ⋯) (bf.P l 1).Z‖

Blueprint line 1934 ("normalized endpoint cell"): on an active cell U the coarse output of a basic slot at the depth of U is at most the sum of the two family inputs on U (the ball filter, the shared history and the basic cell projections are contractions).

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.retained_decision {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (hanc : A.AncClosed) {G : bf.Grp} {b : ℤ} {K : ℕ} {J : ℤ × ℤ} (hJ : J ∈ fp.retainedV G b K) (hbR : A.R.1 ≤ b - 4 * ↑K) : dyadicGridCell A.G J.1 J.2 ⊆ dyadicGridCell A.G (ancAt A.G J (b - 4 * ↑K)).1 (ancAt A.G J (b - 4 * ↑K)).2 ∧ ancAt A.G J (b - 4 * ↑K) ∈ A.cells ∧ fp.Cert G.1 G (ancAt A.G J (b - 4 * ↑K))

Blueprint line 2116 ("their decision cells are the containing u_b-cells"): for a retained v_b-cell J of the group G in a block starting after the attempt root, the u_b-ancestor of J contains J, is active when the active cells are closed under ancestors, and carries a downstream use certificate of G for its color.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.frozen_coeffs {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (l : Fin 4) (s : List (CatCol bf.Vtx)) (mb : bf.MainBudget s) (hanc : A.AncClosed) (G : bf.Grp) {j : ℕ} (hj : j ≤ 4) (ls : List (ℕ × Bool)) (d : bf.Vtx) (D dB : ℕ) {H δc N : ℝ} (k : ℝ) (hHed : 2 ≤ fp.Hed) (hH : 1 ≤ H) (hδc : 0 < δc) (hN0 : 0 ≤ N) (hN : ∀ I ∈ A.cells, ↑(mainLabels A.G fp.Mc (bf.origCols l) s I (fp.brank j)).card ≤ N) {n : ℕ} (Ms : ModeSystem A.G n) (L : LiftData (bf.Lab ⊕ Fin fp.Mc) Ms.Md) {g : ℤ} (hex : fp.MainLiftExports l s G j d D dB H g L Ms.wave Ms.cellOf) (hεM : ∀ (m : Ms.Md), L.εM m = Ms.L.εM m) (S : ModeSchedule) {Dst CF : ℝ} (hCF : 0 ≤ CF) (hstar : fp.modeStar D dB H δc N k ≤ Dst) (hnorm : ∀ (jb : Fin 2), ∀ U ∈ A.cells, ‖(columnL2Restriction (dyadicGridCell A.G U.1 U.2) ⋯) (bf.P l jb).Z‖ ^ 2 ≤ CF * dyadicGridLength A.G U.1) {b : ℤ} {J : ℤ × ℤ} (hJ : J ∈ fp.retainedV G b S.K) : ∃ (β : Ms.Md → ℂ), Ms.frozenEval S b J β = (columnL2Restriction (dyadicGridCell A.G J.1 J.2) ⋯) (L.op (fp.frozenZ l s mb G j ls (b - 4 * ↑S.K))) ∧ ∑ m ∈ Ms.alive (ancAt A.G J (b - 4 * ↑S.K)), ‖β m‖ ^ 2 ≤ 4 * Dst ^ 2 * CF

Blueprint line 1967 and line 2118 ("its coefficient norm ... the complementary coefficient norm is at most D_*"): on a retained v_b-cell J of the group, with the active cells closed under ancestors and fresh normalized attempt roots (‖1_U F_{l,j}‖² ≤ C_F |U| on active cells), the lifted frozen output R_{l,G} Z_{l,G,u_b} restricts on J to the frozen evaluation of coefficients β supported on the modes alive at the decision cell u_b, with square sum at most 4 D_*^2 C_F (D_* covering the coefficient budget modeStar). Before the attempt the frozen output is zero and β = 0.

theorem TrilinearHT.Auto.ModeSystem.eventProj_restrict {Gd : RealDyadicGrid} {Mc : ℕ} (Ms : ModeSystem Gd Mc) (J : ℤ × ℤ) (E : Finset Ms.Md) [(Submodule.span ℂ (Ms.cellMode J '' ↑E)).HasOrthogonalProjection] {t : Set ℝ} (ht : MeasurableSet t) (hJt : dyadicGridCell Gd J.1 J.2 ⊆ t) (w : ↥(ColumnL2 Ms.Md)) : (Submodule.span ℂ (Ms.cellMode J '' ↑E)).starProjection ((columnL2Restriction t ht) w) = (Submodule.span ℂ (Ms.cellMode J '' ↑E)).starProjection w

The projection onto the span of the cell modes of E on J is local to every cell containing J.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.linear_energy {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (l : Fin 4) (s : List (CatCol bf.Vtx)) (hT : ∀ e ∈ s, ∃ R ∈ residueBox (bf.vtag e.tag).dim 9, ∃ (γ : ℝ), e = templateCol (bf.vtag e.tag) l R γ e.birth e.rank e.tag) (htag : ∀ e ∈ s, bf.occAvail (↑e.tag.2) e.tag.1) (d : bf.Vtx) (mb : bf.MainBudget s) (hne : A.cells.Nonempty) (hanc : A.AncClosed) {ι : Type u_1} [Fintype ι] (grp : ι → bf.Grp) (hgrp : Function.Injective grp) (k : ℕ) (hcol : ∀ (G : ι), (grp G).1 = k) {j : ℕ} (hj : j ≤ 4) (hPH : fp.bbase j + fp.P ≤ fp.Hmax) (ls : List (ℕ × Bool)) (S : ModeSchedule) {Cj CA CT CK : ℕ} {δs W : ℝ} (hV : S.Valid Cj CA CT CK δs W) (hCj : 340 ≤ Cj) (hCA : 1 ≤ CA) (hδs : 0 < δs) (hδ1 : δs ≤ 1) (hd2 : 2 ≤ S.dmax) (hD : 2 ≤ S.Dstar) (hB : 2 ≤ S.Bstar) (hQ : 1 ≤ S.Q0) (hDm : 2 ≤ S.Dm) (hW : 8 * (↑S.dmax + 1) ^ 3 * Real.log (2 * S.H) / Real.log 2 ≤ W) (D dB : ℕ) {H δc N kk : ℝ} (hHed : 2 ≤ fp.Hed) (hH : 1 ≤ H) (hδc : 0 < δc) (hN0 : 0 ≤ N) (hNl : ∀ I ∈ A.cells, ↑(mainLabels A.G fp.Mc (bf.origCols l) s I (fp.brank j)).card ≤ N) {n : ℕ} (Ms : ι → ModeSystem A.G n) (q : ι → ℕ) (hq : ∀ (G : ι), 1 ≤ q G ∧ q G ≤ S.Q0) (L : (G : ι) → LiftData (bf.Lab ⊕ Fin fp.Mc) (Ms G).Md) (gs : ι → ℤ) (hex : ∀ (G : ι), fp.MainLiftExports l s (grp G) j d D dB H (gs G) (L G) (Ms G).wave (Ms G).cellOf) (hεM : ∀ (G : ι) (m : (Ms G).Md), (L G).εM m = (Ms G).L.εM m) (hdim : ∀ (G : ι) (p : (Ms G).Key), (Ms G).dvOf p + (Ms G).zc.dim ≤ S.dmax) {M : ℕ} (hM1 : 1 ≤ M) (hMD : ↑M ≤ 2 * S.Dm) (hM : ∀ (G : ι) (U : ℤ × ℤ), (Finset.image (Ms G).keyOf ((Ms G).alive U)).card ≤ M) (hδ : ∀ (G : ι), 0 < (Ms G).δc) (hΛ : ∀ (G : ι), (Ms G).Λ ≤ S.Dstar) (Kf : ℕ) (hDg : ∀ (G : ι), gaugeSqNorm (Ms G).zc.dim (Ms G).δc ≤ S.Dstar) (hKf : ∀ (G : ι), 2 * gaugeTail (Ms G).zc.dim (Ms G).δc / 2 ^ Kf * S.Dstar ^ 300 ≤ 1) (hBox : ↑S.Q0 * 2 ^ (Kf + 1) ≤ S.Bstar) (hεw : ∀ (G : ι) (m : (Ms G).Md), S.Dstar⁻¹ ≤ (Ms G).L.εM m) (halive : ∀ (G : ι) (U : ℤ × ℤ), ↑((Ms G).alive U).card ≤ S.Dstar) (hpath : ∀ (y : ℝ), ∑ G : ι, ↑((Ms G).ptSet y).card ≤ S.Dstar) (hstar : fp.modeStar D dB H δc N kk ≤ S.Dstar) {CF : ℝ} (hCF : 0 ≤ CF) (hnorm : ∀ (jb : Fin 2), ∀ U ∈ A.cells, ‖(columnL2Restriction (dyadicGridCell A.G U.1 U.2) ⋯) (bf.P l jb).Z‖ ^ 2 ≤ CF * dyadicGridLength A.G U.1) (R₀ : ℤ) (Bs : Finset ℤ) (hgrid : ∀ b ∈ Bs, ↑S.K ∣ b - R₀) {ra rb : ℝ} (hroot : ∀ I ∈ A.cells, dyadicGridCell A.G I.1 I.2 ⊆ Set.Icc ra rb) {τ : ℝ} (hτ : 0 < τ) (hτ1 : τ ≤ 1) (hHτ : Real.exp (↑A.Dg * (1 + Real.log A.Hsrc + Real.log τ⁻¹) ^ A.Dg) ≤ fp.Hed) {Nq : ℕ} (hNq : ∀ (y : ℝ), {q : ι × (bf.Lab ⊕ Fin fp.Mc) | ∃ I ∈ A.cells, (∃ (k' : ℕ), fp.Cert k' (grp q.1) I) ∧ ∃ (p : Fin fp.P), y ∈ dyadicGridCell A.G I.1 I.2 ∧ q.2 ∈ mainLabelsM A.G fp.Mc (bf.origCols l) s I (fp.brank j) (fp.bmask I (grp q.1) j (↑p + 1)) d}.card ≤ Nq) (hτN : τ * ↑Nq * A.colBudget ^ 2 ≤ 1) (cc : ℕ) (hcc : 1 ≤ cc) {kq : ℝ} (hkq : 1 ≤ kq) (hDmq : Real.log (2 * mb.B) ≤ kq ^ cc) (hDb : Real.log (2 * A.colBudget) ≤ kq ^ cc) (hn : ↑ls.length ≤ ↑cc * (Real.log kq + 1)) : ∃ (c : (G : ι) → ℤ → ℤ × ℤ → (Ms G).Md → ℂ), (∀ (G : ι), ∀ b ∈ Bs, ∀ J ∈ fp.retainedV (grp G) b S.K, (Ms G).frozenEval (S.withQ0 (q G)) b J (c G b J) = (columnL2Restriction (dyadicGridCell A.G J.1 J.2) ⋯) ((L G).op (fp.frozenZ l s mb (grp G) j ls (b - 4 * ↑S.K)))) ∧ (∀ (G : ι), ∀ b ∈ Bs, ∀ J ∈ fp.retainedV (grp G) b S.K, ∑ m ∈ (Ms G).alive (ancAt A.G J (b - 4 * ↑S.K)), ‖c G b J m‖ ^ 2 ≤ 4 * S.Dstar ^ 2 * CF) ∧ ∑ G : ι, ∑ b ∈ Bs, ‖(Ms G).blockSide (S.withQ0 (q G)) ⋯ (S.sideParams δs) b (fp.retainedV (grp G) b S.K) (c G b)‖ ^ 2 ≤ 24 * (↑⌊180 * ↑S.dmax * Real.log (2 * S.Dm) / δs⌋₊ + 1) * (Real.exp ((6144 * (↑cc + 1) * (1024 * (↑cc + 1) + ↑cc + 7) + 4) * (1 + Real.log (2 * kq)) ^ 2) + 2 * CF / S.Dstar ^ 394) * dyadicGridLength A.G A.R.1

Blueprint prop:linear-side (eq:linear-energy, lines 2080-2118) for one basic role l of a search leaf, one color k with ball level j ≤ 4 and shared history ls: let the mode systems Ms_G with lifts R_{l,G} = L_G carry the exports of mainAttemptLift (MainLiftExports), at a schedule S whose budgets D_*, D_m, d_max cover the mode data (dimensions, label counts, curvatures, full Fourier norms of the squared gauges and truncation tails, inverse private weights, alive modes, modes along a path across groups, and the coefficient budget modeStar), with active cells closed under ancestors (the decision cells u_b are active) and a fresh normalized attempt root (‖1_U F_{l,j}‖² ≤ C_F |U| on active cells). Then there are frozen coefficients c_{G,b,J} representing ZTilde_{l,G,b} = R_{l,G} Z_{l,G,u_b} on every retained v_b-cell J of every block b ∈ Bs (frozenEval), with square sums at most 4 D_*² C_F over the alive modes (frozen_coeffs), and the exact side subtotals V_{l,G,b} (blockSide) satisfy Σ_{G,b} ‖V_{l,G,b}‖² ≤ 24 (⌊180 d_max log(2 D_m)/δ_*⌋ + 1) (G₀ + 2 C_F D_*^{-394}) |R| with G₀ = exp(C_q (1 + log 2k)²) of lift_composition_G0.

Proof: group_side_energy splits each block into its side events (almost orthogonal, cross pairings ≤ D_*^{-200}), the event rows of each group are Bessel with constant 6 (⌊180 d_max log(2 D_m)/δ_*⌋ + 1) (group_event_rows_schedule), their decision cells are the containing u_b-cells, so lem:lift-composition (lift_composition_dep, liftConst_le_G0) bounds the row outputs, and the exact-subtotal errors are negligible (side_errors_negligible, with the coefficient bound of frozen_coeffs).