Section 15.4: Verification of the counting hypotheses

This file was automatically generated by Claude.

Formalization of blueprint Section 15, "Common heights and concentration of the core terms" (sec:core), subsection 4, "Verification of the counting hypotheses" (lines 2708-2745) of blueprint/formalization_blueprint.tex.

theorem TrilinearHT.Auto.pair_difference_eq_zero {u v s₁ s₂ e₁ e₂ w ε Sep : ℝ} {a b c d : ℤ} (h₁ : ↑a * u + ↑b * v = s₁ + e₁) (h₂ : ↑c * u + ↑d * v = s₂ + e₂) (hD : a * d - b * c ≠ 0) (hw : ↑d * s₁ - ↑b * s₂ = ↑(a * d - b * c) * w) (he₁ : |e₁| ≤ ε) (he₂ : |e₂| ≤ ε) (hsep : u ≠ 0 → Sep < |u - w|) (hS : (|↑d| + |↑b|) * ε ≤ Sep) : u = 0

Blueprint lines 2711-2712, conclusion: separation |u - w| > Σ for nonzero differences against every reserved shift, with (|d| + |b|) ε ≤ Σ, forces the difference to vanish.

theorem TrilinearHT.Auto.total_count_le {T : Type u_1} {P : Type u_2} {σ : Type u_3} [DecidableEq P] (S : Finset σ) (E : σ → Finset T) (proj : T → P) (Pairs : Finset P) (hproj : ∀ s ∈ S, ∀ t ∈ E s, proj t ∈ Pairs) (L : ℕ) (hmult : ∀ p ∈ Pairs, ∑ s ∈ S, {t ∈ E s | proj t = p}.card ≤ L) : ∑ s ∈ S, (E s).card ≤ L * Pairs.card

Blueprint eq:total-count (line 2729), first bound: if every pair of labels in roles i, j determines tuples with at most L scale occurrences in total, then Σ_s N_s ≤ L M_i M_j (here M_i M_j is the number of label pairs).

theorem TrilinearHT.Auto.scale_count_le {T : Type u_1} {P : Type u_2} (E : Finset T) (proj : T → P) (Pairs : Finset P) (hproj : ∀ t ∈ E, proj t ∈ Pairs) (hinj : Set.InjOn proj ↑E) : E.card ≤ Pairs.card

Blueprint eq:total-count, second bound: at one scale, pair determination makes the pair projection injective, so N_s ≤ M_i M_j ≤ (M')².

Verification of the counting hypotheses on tested tuples (blueprint lines 2709-2744)

theorem TrilinearHT.Auto.fin4_complement (i j : Fin 4) : i ≠ j → ∃ (k : Fin 4) (l : Fin 4), k ≠ l ∧ k ≠ i ∧ k ≠ j ∧ l ≠ i ∧ l ≠ j ∧ ∀ (r : Fin 4), r = i ∨ r = j ∨ r = k ∨ r = l

Every pair of distinct roles has two complementary roles.

theorem TrilinearHT.Auto.fin4_sum_eq {i j k l : Fin 4} (hkl : k ≠ l) (hki : k ≠ i) (hkj : k ≠ j) (hli : l ≠ i) (hlj : l ≠ j) (hij : i ≠ j) (f : Fin 4 → ℝ) : ∑ r : Fin 4, f r = f i + f j + f k + f l

theorem TrilinearHT.Auto.pair_role_of_diff {d : ℕ} (ζ : Fin d → ℝ) {x x' : Fin 4 → ℝ} {i j k l : Fin 4} (hkl : k ≠ l) (hki : k ≠ i) (hkj : k ≠ j) (hli : l ≠ i) (hlj : l ≠ j) (hij : i ≠ j) (hxi : x i = x' i) (hxj : x j = x' j) {n m n' m' : Fin d → ℤ} {B Q Sep ε : ℝ} (hn : ∀ (r : Fin d), |↑(n r)| ≤ B) (hm : ∀ (r : Fin d), |↑(m r)| ≤ B) (hn' : ∀ (r : Fin d), |↑(n' r)| ≤ B) (hm' : ∀ (r : Fin d), |↑(m' r)| ≤ B) (hq : |∑ r : Fin 4, x r + 36 * ∑ p : Fin d, ↑(n p) * ζ p - (∑ r : Fin 4, x' r + 36 * ∑ p : Fin d, ↑(n' p) * ζ p)| ≤ ε) (ht : |∑ r : Fin 4, ↑↑r * x r + 36 * ∑ p : Fin d, ↑(m p) * ζ p - (∑ r : Fin 4, ↑↑r * x' r + 36 * ∑ p : Fin d, ↑(m' p) * ζ p)| ≤ ε) (hsep : x k ≠ x' k → ∀ (N : Fin d → ℤ), (∀ (p : Fin d), |↑(N p)| ≤ Q) → Sep < |x k - x' k + ∑ p : Fin d, ↑(N p) * ζ p|) (hQ : 288 * B ≤ Q) (hSep : 4 * ε ≤ Sep) : x k = x' k

Blueprint lines 2716-2717 (pair determination): two tuples x, x' agreeing in roles i, j, whose sums q = Σ x_r + 36 n·ζ and t = Σ r x_r + 36 m·ζ (box shifts |n|, |m| ≤ B) differ by at most ε from those of x', agree in each other role k: the remaining two differences solve a two-by-two system of determinant at most 3 in absolute value, dividing 36 into the shift, and separation Sep with reserve 288 B ≤ Q, 4ε ≤ Sep forces them to vanish.

theorem TrilinearHT.Auto.four_core_pair_role {d : ℕ} (ζ : Fin d → ℝ) {x x' : Fin 4 → ℝ} {i j k l : Fin 4} (hkl : k ≠ l) (hki : k ≠ i) (hkj : k ≠ j) (hli : l ≠ i) (hlj : l ≠ j) (hij : i ≠ j) (hxi : x i = x' i) (hxj : x j = x' j) {n m n' m' : Fin d → ℤ} {B Q Sg ν R R' : ℝ} (hn : ∀ (r : Fin d), |↑(n r)| ≤ B) (hm : ∀ (r : Fin d), |↑(m r)| ≤ B) (hn' : ∀ (r : Fin d), |↑(n' r)| ≤ B) (hm' : ∀ (r : Fin d), |↑(m' r)| ≤ B) (hq : |∑ r : Fin 4, x r + 36 * ∑ p : Fin d, ↑(n p) * ζ p| ≤ ν * R) (ht : |∑ r : Fin 4, ↑↑r * x r + 36 * ∑ p : Fin d, ↑(m p) * ζ p| ≤ ν * R) (hq' : |∑ r : Fin 4, x' r + 36 * ∑ p : Fin d, ↑(n' p) * ζ p| ≤ ν * R') (ht' : |∑ r : Fin 4, ↑↑r * x' r + 36 * ∑ p : Fin d, ↑(m' p) * ζ p| ≤ ν * R') (hsep : x k ≠ x' k → ∀ (N : Fin d → ℤ), (∀ (p : Fin d), |↑(N p)| ≤ Q) → Sg * max R R' < |x k - x' k + ∑ p : Fin d, ↑(N p) * ζ p|) (hQ : 288 * B ≤ Q) (hSg : 8 * ν ≤ Sg) (hν : 0 ≤ ν) (hR : 0 ≤ R) : x k = x' k

Blueprint lines 2716-2717 (pair determination, four cores): two tested tuples x, x' at scales s, s' whose reference equations Σ x_r + 36 n·ζ = q, Σ r x_r + 36 m·ζ = t hold with |q|, |t| ≤ ν R_s and which agree in roles i, j, agree in each other role k, given separation with reserve 288 B ≤ Q, 8ν ≤ Σ.

theorem TrilinearHT.Auto.four_core_pair {d : ℕ} (ζ : Fin d → ℝ) {x x' : Fin 4 → ℝ} {i j : Fin 4} (hij : i ≠ j) (hxi : x i = x' i) (hxj : x j = x' j) {B Q Sg μ ν R R' : ℝ} (hx : FourRef ζ B μ ν R x) (hx' : FourRef ζ B μ ν R' x') (hsep : ∀ (r : Fin 4), x r ≠ x' r → ∀ (N : Fin d → ℤ), (∀ (p : Fin d), |↑(N p)| ≤ Q) → Sg * max R R' < |x r - x' r + ∑ p : Fin d, ↑(N p) * ζ p|) (hQ : 288 * B ≤ Q) (hSg : 8 * ν ≤ Sg) (hν : 0 ≤ ν) (hR : 0 ≤ R) : x = x'

Blueprint lines 2716-2717: two four-core tested tuples sharing labels in two distinct roles are equal (across all scales).

theorem TrilinearHT.Auto.four_core_ann {d : ℕ} (ζ : Fin d → ℝ) {x : Fin 4 → ℝ} {B μ ν R : ℝ} (hx : FourRef ζ B μ ν R x) {T : Finset (Fin 4)} (hT : T.card = 3) {l : Fin 4} (hl : l ∉ T) : ∃ (n : Fin d → ℤ), (∀ (k : Fin d), |↑(n k)| ≤ 4 * B) ∧ μ * R ≤ |∑ i ∈ T, ↑(roleCoeff i l) * x i + 36 * ∑ k : Fin d, ↑(n k) * ζ k| ∧ |∑ i ∈ T, ↑(roleCoeff i l) * x i + 36 * ∑ k : Fin d, ↑(n k) * ζ k| ≤ 4 * ν * R

Blueprint eq:triple-test for four cores (line 2722): the triple omitting the anchor l' has Σ_{i ≠ l'} (i - l') x_i + 36 (m - l' n)·ζ = t' - l' q', between μ R and 4 ν R, with a witness of size at most 4 B.

theorem TrilinearHT.Auto.sum_erase_roleCoeff {i j k l : Fin 4} (hkl : k ≠ l) (hki : k ≠ i) (hkj : k ≠ j) (hli : l ≠ i) (hlj : l ≠ j) (hij : i ≠ j) (f : Fin 4 → ℝ) (hi : f i = 0) (hj : f j = 0) : ∑ r ∈ Finset.univ.erase l, ↑(roleCoeff r l) * f r = ↑(roleCoeff k l) * f k

theorem TrilinearHT.Auto.three_core_pair {d : ℕ} (ζ : Fin d → ℝ) {l : Fin 4} {x x' : Fin 4 → ℝ} (hxl : x l = 0) (hxl' : x' l = 0) {i j : Fin 4} (hij : i ≠ j) (hil : i ≠ l) (hjl : j ≠ l) (hxi : x i = x' i) (hxj : x j = x' j) {B Q Sg μ ν R R' : ℝ} (hx : ThreeRef ζ l B μ ν R x) (hx' : ThreeRef ζ l B μ ν R' x') (hsep : ∀ (r : Fin 4), x r ≠ x' r → ∀ (N : Fin d → ℤ), (∀ (p : Fin d), |↑(N p)| ≤ Q) → Sg * max R R' < |x r - x' r + ∑ p : Fin d, ↑(N p) * ζ p|) (hQ : 72 * B ≤ Q) (hSg : 2 * ν ≤ Sg) (hν : 0 ≤ ν) (hR : 0 ≤ R) : x = x'

Blueprint line 2717 ("for three cores the single T_l equation determines the remaining label in the same way"): two three-core tested tuples sharing labels in two distinct core roles are equal, given separation with reserve 72 B ≤ Q, 2ν ≤ Σ.

theorem TrilinearHT.Auto.sum_erase_roleCoeff_eq (l : Fin 4) (x : Fin 4 → ℝ) : ∑ i ∈ Finset.univ.erase l, ↑(roleCoeff i l) * x i = ∑ r : Fin 4, ↑↑r * x r - ↑↑l * ∑ r : Fin 4, x r

theorem TrilinearHT.Auto.side_window_pair {d : ℕ} (ζ : Fin d → ℝ) {l i : Fin 4} (hil : i ≠ l) {x x' : Fin 4 → ℝ} (hxl : x l = 0) (hxl' : x' l = 0) (hxi : x i = x' i) {B Q Sg μ ν Λ R : ℝ} (hx : ThreeRef ζ l B μ ν R x) (hx' : ThreeRef ζ l B μ ν R x') {n n' : Fin d → ℤ} (hn : ∀ (p : Fin d), |↑(n p)| ≤ B) (hn' : ∀ (p : Fin d), |↑(n' p)| ≤ B) (hwin : |∑ r : Fin 4, x r + 36 * ∑ p : Fin d, ↑(n p) * ζ p - (∑ r : Fin 4, x' r + 36 * ∑ p : Fin d, ↑(n' p) * ζ p)| ≤ 4 * Λ * R) (hsep : ∀ (r : Fin 4), x r ≠ x' r → ∀ (N : Fin d → ℤ), (∀ (p : Fin d), |↑(N p)| ≤ Q) → Sg * R < |x r - x' r + ∑ p : Fin d, ↑(N p) * ζ p|) (hQ : 1152 * B ≤ Q) (hSg : 8 * ν + 48 * Λ ≤ Sg) (hR : 0 ≤ R) : x = x'

Blueprint lines 2724-2725 (core/side pair, windows): two three-core tested tuples at one scale R, sharing the label of a core role i, whose side windows meet (their Q values Σ x_r + 36 n·ζ differ by at most 4ΛR for box shifts n, n') are equal: with the two T_l equations the two other labels solve a two-by-two system of divisor at most 3, and separation with 8ν + 48Λ ≤ Σ, 1152 B ≤ Q forces equality.

theorem TrilinearHT.Auto.mem_sideWindow {d : ℕ} {ζ : Fin d → ℝ} {r Λ B : ℝ} {x : Fin 4 → ℝ} {k : ℤ} : k ∈ sideWindow ζ r Λ B x ↔ ∃ (n : Fin d → ℤ), (∀ (p : Fin d), |↑(n p)| ≤ B) ∧ |↑k - r * (∑ i : Fin 4, x i + 36 * ∑ p : Fin d, ↑(n p) * ζ p)| ≤ 2 * Λ

theorem TrilinearHT.Auto.sideWindow_disjoint {d : ℕ} (ζ : Fin d → ℝ) {l i : Fin 4} (hil : i ≠ l) {x x' : Fin 4 → ℝ} (hxl : x l = 0) (hxl' : x' l = 0) (hxi : x i = x' i) (hne : x ≠ x') {B Q Sg μ ν Λ r : ℝ} (hr : 0 < r) (hx : ThreeRef ζ l B μ ν r⁻¹ x) (hx' : ThreeRef ζ l B μ ν r⁻¹ x') (hsep : ∀ (j : Fin 4), x j ≠ x' j → ∀ (N : Fin d → ℤ), (∀ (p : Fin d), |↑(N p)| ≤ Q) → Sg * r⁻¹ < |x j - x' j + ∑ p : Fin d, ↑(N p) * ζ p|) (hQ : 1152 * B ≤ Q) (hSg : 8 * ν + 48 * Λ ≤ Sg) : Disjoint (sideWindow ζ r Λ B x) (sideWindow ζ r Λ B x')

Blueprint lines 2724-2726: at one scale R = r⁻¹, the side windows of distinct three-core tested tuples sharing a core label are disjoint (side_window_pair).

theorem TrilinearHT.Auto.side_incidence_le {Ω : Type u_1} [MeasurableSpace Ω] (P : MeasureTheory.Measure Ω) {τ : Type u_2} (Tr : Finset τ) (W : τ → Finset ℤ) (hdis : ∀ t ∈ Tr, ∀ t' ∈ Tr, t ≠ t' → Disjoint (W t) (W t')) (F : Ω → ℤ → ℝ) (hFi : ∀ (k : ℤ), MeasureTheory.Integrable (fun (ρ : Ω) => F ρ k) P) (G : Ω → ℝ) (hG : MeasureTheory.Integrable G P) (hpars : ∀ (ρ : Ω) (U : Finset ℤ), ∑ k ∈ U, F ρ k ≤ G ρ) {σ : ℝ} (hσ : ∀ t ∈ Tr, σ ^ 2 ≤ ∫ (ρ : Ω), ∑ k ∈ W t, F ρ k ∂P) : ↑Tr.card * σ ^ 2 ≤ ∫ (ρ : Ω), G ρ ∂P

Blueprint lines 2726-2728 (side incidence): if the tested triples Tr incident to one core label at one scale have pairwise disjoint side windows, and each has averaged window energy E_ρ Σ_{k ∈ W_t} F_ρ(k) ≥ σ², where for every offset ρ the window sums are bounded by the normalized energy G_ρ (Parseval), then |Tr| σ² ≤ E_ρ G_ρ; this is w_s σ².

theorem TrilinearHT.Auto.tested_scale_mult {d : ℕ} (ζ : Fin d → ℝ) (x : Fin 4 → ℝ) (T : Finset (Fin 4)) (l : Fin 4) {B μ ν R₀ : ℝ} (hB : 1 ≤ B) (hμ : 0 < μ) (hμν : μ ≤ ν) (hR₀ : 0 < R₀) (S : Finset ℤ) : ↑{s ∈ S | ∃ (n : Fin d → ℤ), (∀ (p : Fin d), |↑(n p)| ≤ B) ∧ μ * (R₀ * 2 ^ s) ≤ |∑ i ∈ T, ↑(roleCoeff i l) * x i + 36 * ∑ p : Fin d, ↑(n p) * ζ p| ∧ |∑ i ∈ T, ↑(roleCoeff i l) * x i + 36 * ∑ p : Fin d, ↑(n p) * ζ p| ≤ ν * (R₀ * 2 ^ s)}.card ≤ 32 * (↑(4 + d) + 1) ^ 4 * (Real.log (2 * (36 * B)) + Real.log (2 * ν / μ))

Blueprint lines 2723-2724 (multiplicity via lem:height): for a fixed tuple x, triple T and anchor l, the scales s at which some box shift |n| ≤ B gives the triple test μ R_s ≤ |Σ_{i ∈ T} (i - l) x_i + 36 n·ζ| ≤ ν R_s number at most 32 (d + 5)⁴ (log(72 B) + log(2ν/μ)): these are bounded-height rational evaluations of the vector (x, ζ).

theorem TrilinearHT.Auto.sep_of_scaled {d : ℕ} (θ : Fin d → ℝ) (c : ℕ) {E Q Sg a a' : ℝ} (hcQ : ↑c * Q ≤ E) (hsep : ∀ (n : Fin d → ℤ), (∀ (k : Fin d), |↑(n k)| ≤ E) → Sg < |a - a' + ∑ k : Fin d, ↑(n k) * θ k|) (N : Fin d → ℤ) : (∀ (k : Fin d), |↑(N k)| ≤ Q) → Sg < |a - a' + ∑ k : Fin d, ↑(N k) * (↑c * θ k)|

Blueprint lines 2733-2736 (separation reserve): separation against the shifts n·θ with |n| ≤ E (eq:representative-separation, θ = ϑ/L_h) gives separation against N·(cθ) with |N| ≤ Q whenever c Q ≤ E (ζ = 6^{Δ-2} ϑ/L_h, Q = ⌊E_h/6^{Δ-2}⌋).

Counting hypotheses on the attempt (blueprint lines 2707-2742)

theorem TrilinearHT.Auto.tested_mult_le {d : ℕ} {B μ ν : ℝ} (hB : 1 ≤ B) (hμ : 0 < μ) (hμν : μ ≤ ν) : 32 * (↑(4 + d) + 1) ^ 4 * (Real.log (2 * (36 * B)) + Real.log (2 * ν / μ)) ≤ 32 * (↑(4 + d) + 1) ^ 4 * (Real.log (72 * B) + Real.log 2 + 1) * (1 + Real.log (ν / μ))

Blueprint lines 2722-2724 (L₀ ≤ P^C (1 + log(ν/μ))^C): the multiplicity bound of tested_scale_mult, 32 (d + 5)^4 (log(72 B) + log(2ν/μ)), is at most 32 (d + 5)^4 (log(72 B) + log 2 + 1) (1 + log(ν/μ)).

noncomputable def TrilinearHT.Auto.fourMult (d : ℕ) (B μ ν : ℝ) : ℝ

The tested-tuple multiplicity L₀ of tested_scale_mult for four cores (L₀ ≤ P^C (1 + log(ν/μ))^C, blueprint line 2723).

Equations

• TrilinearHT.Auto.fourMult d B μ ν = 32 * (↑(4 + d) + 1) ^ 4 * (Real.log (2 * (36 * (4 * B))) + Real.log (2 * (4 * ν) / μ))

theorem TrilinearHT.Auto.one_le_fourMult (d : ℕ) {B μ ν : ℝ} (hB : 1 ≤ B) (hμ : 0 < μ) (hμν : μ ≤ ν) : 1 ≤ fourMult d B μ ν

theorem TrilinearHT.Auto.total_count_real (S : Finset ℤ) (E : ℤ → Finset (Fin 4 → ℝ)) (A : Fin 4 → Finset ℝ) {i j : Fin 4} (hA : ∀ s ∈ S, ∀ x ∈ E s, x i ∈ A i ∧ x j ∈ A j) (hpair : ∀ s ∈ S, ∀ s' ∈ S, ∀ x ∈ E s, ∀ x' ∈ E s', x i = x' i → x j = x' j → x = x') {L : ℝ} (hmult : ∀ (x : Fin 4 → ℝ), ↑{s ∈ S | x ∈ E s}.card ≤ L) : ∑ s ∈ S, ↑(E s).card ≤ L * ↑(A i).card * ↑(A j).card

Pair determination across all scales gives the total count: if two labels in roles i ≠ j determine the tuple across the scales and each tuple occurs at most L times, then Σ_s N_s ≤ L M_i M_j (blueprint eq:total-count, first bound).

noncomputable def TrilinearHT.Auto.threeMult (d : ℕ) (B μ ν : ℝ) : ℝ

The tested-tuple multiplicity L₀ of tested_scale_mult for three cores.

Equations

• TrilinearHT.Auto.threeMult d B μ ν = 32 * (↑(4 + d) + 1) ^ 4 * (Real.log (2 * (36 * B)) + Real.log (2 * ν / μ))

theorem TrilinearHT.Auto.one_le_threeMult (d : ℕ) {B μ ν : ℝ} (hB : 1 ≤ B) (hμ : 0 < μ) (hμν : μ ≤ ν) : 1 ≤ threeMult d B μ ν

theorem TrilinearHT.Auto.prod_ite_one_erase {l : Fin 4} (f : Fin 4 → ℝ) : (∏ j : Fin 4, if j = l then 1 else f j) = ∏ j ∈ Finset.univ.erase l, f j

Counting setup on the side states (blueprint lines 2709-2717)

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

A final class F at height h of the node (b, J): the CURRENT component of a mode good at h (a successful component, blueprint line 2172).

Equations

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

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

The modes good at h whose CURRENT component is the final class F.

Equations

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

theorem TrilinearHT.Auto.ModeSystem.goodModesOf_nonempty {Gd : RealDyadicGrid} {Mc : ℕ} (Ms : ModeSystem Gd Mc) (S : ModeSchedule) (hA : 6 ≤ S.A0) (SP : SideParams) {b : ℤ} {J : ℤ × ℤ} {h : ℕ} {F : Finset Ms.Md} (hF : Ms.HasGoodRep S hA SP b J h F) : (Ms.goodModesOf S hA SP b J h F).Nonempty

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

The good mode chosen in a successful final class: the good mode of least index whose CURRENT component is the class (a function of the node, the height and the class only; it is the mode of the successful component, succModes).

Equations

• Ms.goodRep S hA SP hF = ⋯.choose

theorem TrilinearHT.Auto.ModeSystem.goodRep_spec {Gd : RealDyadicGrid} {Mc : ℕ} (Ms : ModeSystem Gd Mc) (S : ModeSchedule) (hA : 6 ≤ S.A0) (SP : SideParams) {b : ℤ} {J : ℤ × ℤ} {h : ℕ} {F : Finset Ms.Md} (hF : Ms.HasGoodRep S hA SP b J h F) : (Ms.blockComps S hA b J).Good SP.Δ (Ms.goodP S SP b) h (Ms.goodRep S hA SP hF) ∧ Finset.map { toFun := Subtype.val, inj' := ⋯ } ((Ms.blockComps S hA b J).F h (Ms.goodRep S hA SP hF)) = F

theorem TrilinearHT.Auto.ModeSystem.goodRep_min {Gd : RealDyadicGrid} {Mc : ℕ} (Ms : ModeSystem Gd Mc) (S : ModeSchedule) (hA : 6 ≤ S.A0) (SP : SideParams) {b : ℤ} {J : ℤ × ℤ} {h : ℕ} {F : Finset Ms.Md} (hF : Ms.HasGoodRep S hA SP b J h F) (m : ↥(Ms.alive (ancAt Gd J (b - 4 * ↑S.K)))) (hm : (Ms.blockComps S hA b J).Good SP.Δ (Ms.goodP S SP b) h m) (hmF : Finset.map { toFun := Subtype.val, inj' := ⋯ } ((Ms.blockComps S hA b J).F h m) = F) : Ms.modeIdx ↑(Ms.goodRep S hA SP hF) ≤ Ms.modeIdx ↑m

The chosen good mode has the least index among the good modes of its class.

theorem TrilinearHT.Auto.ModeSystem.goodRep_val_eq {Gd : RealDyadicGrid} {Mc : ℕ} (Ms : ModeSystem Gd Mc) (S : ModeSchedule) (hA : 6 ≤ S.A0) (SP : SideParams) {b b' : ℤ} {J J' : ℤ × ℤ} {h : ℕ} {F : Finset Ms.Md} (hb : b = b') (hJ : J = J') (hF : Ms.HasGoodRep S hA SP b J h F) (hF' : Ms.HasGoodRep S hA SP b' J' h F) : ↑(Ms.goodRep S hA SP hF) = ↑(Ms.goodRep S hA SP hF')

theorem TrilinearHT.Auto.ModeSystem.goodRep_node_dist {Gd : RealDyadicGrid} {Mc : ℕ} (Ms : ModeSystem Gd Mc) (S : ModeSchedule) (hA : 6 ≤ S.A0) (SP : SideParams) {b b' : ℤ} {J J' : ℤ × ℤ} {h : ℕ} {F F' : Finset Ms.Md} (hb : b = b') (hJ : J = J') (hF : Ms.HasGoodRep S hA SP b J h F) (hF' : Ms.HasGoodRep S hA SP b' J' h F') (hm : ↑(Ms.goodRep S hA SP hF') ∈ Ms.alive (ancAt Gd J (b - 4 * ↑S.K))) (hmem : ⟨↑(Ms.goodRep S hA SP hF'), hm⟩ ∈ (Ms.blockComps S hA b J).F h (Ms.goodRep S hA SP hF)) : F = F'

Distinct successful classes of one node have good modes in different CURRENT components.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.hasGoodRep_of_mem_goodCls {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) {G : bf.Grp} {I : ℤ × ℤ} {j : Fin 4} {h : ℕ} {F : Finset (D.Ms j G).Md} (hF : F ∈ D.goodCls G I j h) : (D.Ms j G).HasGoodRep D.S ⋯ D.SP (A.blkStart D.S.K I.1) (D.preAt I) h F

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.classNode {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (G : bf.Grp) (I : ℤ × ℤ) (j : Fin 4) (h : ℕ) {F : Finset (D.Ms j G).Md} (hF : F ∈ D.goodCls G I j h) : ℤ × (ℤ × ℤ) × (D.Ms j G).Md

The mode node (b, J, m) of a successful final class F at the cell I (b the block, J the pre-cell, m its chosen good mode).

Equations

• D.classNode G I j h hF = (A.blkStart D.S.K I.1, D.preAt I, ↑((D.Ms j G).goodRep D.S ⋯ D.SP ⋯))

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.classNodes {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (G : bf.Grp) (j : Fin 4) (h : ℕ) (Cs : Finset (ℤ × ℤ)) : Finset (ℤ × (ℤ × ℤ) × (D.Ms j G).Md)

The mode nodes of the successful final classes at height h of the role j on the cells Cs.

Equations

• D.classNodes G j h Cs = Cs.biUnion fun (I : ℤ × ℤ) => Finset.image (fun (F : ↥(D.goodCls G I j h)) => D.classNode G I j h ⋯) (D.goodCls G I j h).attach

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.mem_classNodes {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) {G : bf.Grp} {j : Fin 4} {h : ℕ} {Cs : Finset (ℤ × ℤ)} {c : ℤ × (ℤ × ℤ) × (D.Ms j G).Md} : c ∈ D.classNodes G j h Cs ↔ ∃ I ∈ Cs, ∃ (F : Finset (D.Ms j G).Md) (hF : F ∈ D.goodCls G I j h), c = D.classNode G I j h hF

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.classNode_alive {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) {G : bf.Grp} {I : ℤ × ℤ} {j : Fin 4} {h : ℕ} {F : Finset (D.Ms j G).Md} (hF : F ∈ D.goodCls G I j h) : (D.classNode G I j h hF).2.2 ∈ (D.Ms j G).alive (ancAt A.G (D.classNode G I j h hF).2.1 ((D.classNode G I j h hF).1 - 4 * ↑D.S.K))

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.classNodes_props {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (G : bf.Grp) (j : Fin 4) (h : ℕ) (Cs : Finset (ℤ × ℤ)) : (∀ c ∈ D.classNodes G j h Cs, c.2.1.1 = c.1 - 2 * ↑D.S.K) ∧ (∀ c ∈ D.classNodes G j h Cs, c.2.2 ∈ (D.Ms j G).alive (ancAt A.G c.2.1 (c.1 - 4 * ↑D.S.K))) ∧ (∀ c ∈ D.classNodes G j h Cs, ∃ (hm : c.2.2 ∈ (D.Ms j G).alive (ancAt A.G c.2.1 (c.1 - 4 * ↑D.S.K))), ((D.Ms j G).blockComps D.S ⋯ c.1 c.2.1).Good D.SP.Δ ((D.Ms j G).goodP D.S D.SP c.1) h ⟨c.2.2, hm⟩) ∧ ∀ c ∈ D.classNodes G j h Cs, ∀ c' ∈ D.classNodes G j h Cs, c.1 = c'.1 → c.2.1 = c'.2.1 → ∀ (hm : c.2.2 ∈ (D.Ms j G).alive (ancAt A.G c.2.1 (c.1 - 4 * ↑D.S.K))) (hm' : c'.2.2 ∈ (D.Ms j G).alive (ancAt A.G c.2.1 (c.1 - 4 * ↑D.S.K))), c ≠ c' → ⟨c'.2.2, hm'⟩ ∉ ((D.Ms j G).blockComps D.S ⋯ c.1 c.2.1).F h ⟨c.2.2, hm⟩

The mode nodes of the successful classes satisfy the node hypotheses of the hereditary representatives (attempt_representatives3): pre-cells two block lengths up, alive good modes, and distinct nodes on one pre-cell in different CURRENT components.

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.repAnchor {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (G : bf.Grp) (I : ℤ × ℤ) (j : Fin 4) (h : ℕ) (rep : ℕ → ℕ → ℤ × (ℤ × ℤ) × (D.Ms j G).Md → (D.Ms j G).Md) (hrep : ∀ (k₁ k₂ : ℕ) (c : ℤ × (ℤ × ℤ) × (D.Ms j G).Md), rep k₁ k₂ c ∈ (D.Ms j G).predOfMode D.S ⋯ 10 h c) {F : Finset (D.Ms j G).Md} (hF : F ∈ D.goodCls G I j h) : ↥((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K)))

The anchor of a successful final class at the cell I given by representatives rep of the type classes of the class nodes (blueprint line 2467: "let a_j be its representative").

Equations

• D.repAnchor G I j h rep hrep hF = ⟨rep ((D.Ms j G).nodeType1 D.S ⋯ 10 h (D.classNode G I j h hF)) ((D.Ms j G).nodeType2 D.S ⋯ 10 h (D.classNode G I j h hF)) (D.classNode G I j h hF), ⋯⟩

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.repAnc {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (G : bf.Grp) (I : ℤ × ℤ) (j : Fin 4) (rep : ℕ → ℕ → ℕ → ℤ × (ℤ × ℤ) × (D.Ms j G).Md → (D.Ms j G).Md) (hrep : ∀ h ∈ ModeComponents.upperHeights D.SP.Jst D.SP.δs, ∀ (k₁ k₂ : ℕ) (c : ℤ × (ℤ × ℤ) × (D.Ms j G).Md), rep h k₁ k₂ c ∈ (D.Ms j G).predOfMode D.S ⋯ 10 h c) (d₀ : ↥((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K)))) (h : ℕ) (F : Finset (D.Ms j G).Md) : ↥((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K)))

The anchors at a cell from per-height representatives (a default alive mode d₀ for the classes that are not successful).

Equations

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

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.repAnc_ok {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (hstab : D.Stab) (hΔ : D.SP.Δ = 10) (G : bf.Grp) (I : ℤ × ℤ) (j : Fin 4) (rep : ℕ → ℕ → ℕ → ℤ × (ℤ × ℤ) × (D.Ms j G).Md → (D.Ms j G).Md) (hrep : ∀ h ∈ ModeComponents.upperHeights D.SP.Jst D.SP.δs, ∀ (k₁ k₂ : ℕ) (c : ℤ × (ℤ × ℤ) × (D.Ms j G).Md), rep h k₁ k₂ c ∈ (D.Ms j G).predOfMode D.S ⋯ 10 h c) (d₀ : ↥((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K)))) : D.AnchorOKAt G I j (D.repAnc G I j rep hrep d₀)

Blueprint line 2467 for the representatives: the anchors repAnc of the final classes satisfy AnchorOKAt; every mode of a core component good at h lies in the PRE predecessor of the representative of its class (the predecessor of the chosen good mode, selected_in_pred_of_rep).

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.typedNodes {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (G : bf.Grp) (j : Fin 4) (h : ℕ) (Cs : Finset (ℤ × ℤ)) (k₁ k₂ : ℕ) : Finset (ℤ × (ℤ × ℤ) × (D.Ms j G).Md)

The class nodes of one type class (k₁, k₂).

Equations

• D.typedNodes G j h Cs k₁ k₂ = {c ∈ D.classNodes G j h Cs | (D.Ms j G).nodeType1 D.S ⋯ 10 h c = k₁ ∧ (D.Ms j G).nodeType2 D.S ⋯ 10 h c = k₂}

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.rep_slope_sep {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (G : bf.Grp) (j : Fin 4) (h : ℕ) (Cs : Finset (ℤ × ℤ)) (k₁ k₂ : ℕ) (rep : ℤ × (ℤ × ℤ) × (D.Ms j G).Md → (D.Ms j G).Md) (hrep : ∀ (c : ℤ × (ℤ × ℤ) × (D.Ms j G).Md), rep c ∈ (D.Ms j G).predOfMode D.S ⋯ 10 h c) (hsepF : ∀ (c c' : ℤ × (ℤ × ℤ) × (D.Ms j G).Md), (D.Ms j G).nodeLt3 (D.typedNodes G j h Cs k₁ k₂) c c' → rep c ≠ rep c' → ∀ (z z' : ↥((D.Ms j G).alive (ancAt A.G c'.2.1 (c'.1 - 4 * ↑D.S.K)))), ↑z ∈ (D.Ms j G).predOfMode D.S ⋯ 10 h c → ↑z' ∈ (D.Ms j G).predOfMode D.S ⋯ 10 h c' → z ∉ ((D.Ms j G).blockComps D.S ⋯ c'.1 c'.2.1).F h z') (hΛ : 8 * (D.Ms j G).Λ ≤ D.S.Ξ) {xs : ℝ} {c c' : ℤ × (ℤ × ℤ) × (D.Ms j G).Md} (hc : c ∈ D.typedNodes G j h Cs k₁ k₂) (hc' : c' ∈ D.typedNodes G j h Cs k₁ k₂) (hxc : xs ∈ dyadicGridCell A.G c.2.1.1 c.2.1.2) (hxc' : xs ∈ dyadicGridCell A.G c'.2.1.1 c'.2.1.2) (hne : rep c ≠ rep c') {rI rI' : ℝ} (hrI : dyadicGridLength A.G (max c.1 c'.1 + ↑D.S.K) ≤ rI) (hrI' : dyadicGridLength A.G (max c.1 c'.1 + ↑D.S.K) ≤ rI') (cq : ℕ) {Q : ℝ} (hcQ : ↑cq * Q ≤ D.S.Eh h) (N : Fin (D.Ms j G).zc.dim → ℤ) (hN : ∀ (k : Fin (D.Ms j G).zc.dim), |↑(N k)| ≤ Q) : D.S.Ξ / 2 * max rI⁻¹ rI'⁻¹ < |(D.Ms j G).slope (rep c) xs - (D.Ms j G).slope (rep c') xs + ∑ k : Fin (D.Ms j G).zc.dim, ↑(N k) * (↑cq * ((D.Ms j G).zc.θ k / ↑D.S.Q0 / ModeSchedule.Lh h))|

Blueprint lines 2711-2712 and eq:representative-separation on the side states: two different representatives of one type class on class nodes whose pre-cells contain the path point x* have slopes at x* separated by (Ξ/2) max(r⁻¹, r'⁻¹) against all shifts N·ζ, ζ = c_q θ/(Q₀ L_h), |N| ≤ Q, c_q Q ≤ E_h (role_label_separation3, sep_of_scaled).

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.classTypeOf {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (G : bf.Grp) (I : ℤ × ℤ) (j : Fin 4) (h : ℕ) (F : Finset (D.Ms j G).Md) : ℕ × ℕ

The type (⌊log₂ |π(E)|⌋, ⌊log₂ |E|⌋) of the predecessor E of a successful final class at a cell (blueprint line 2172), (0, 0) for other classes.

Equations

• D.classTypeOf G I j h F = if hF : F ∈ D.goodCls G I j h then ((D.Ms j G).nodeType1 D.S ⋯ 10 h (D.classNode G I j h hF), (D.Ms j G).nodeType2 D.S ⋯ 10 h (D.classNode G I j h hF)) else (0, 0)

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.classNode_mem_typedNodes {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) {G : bf.Grp} {I : ℤ × ℤ} {j : Fin 4} {h : ℕ} {Cs : Finset (ℤ × ℤ)} (hI : I ∈ Cs) {F : Finset (D.Ms j G).Md} (hF : F ∈ D.goodCls G I j h) : D.classNode G I j h hF ∈ D.typedNodes G j h Cs (D.classTypeOf G I j h F).1 (D.classTypeOf G I j h F).2

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.path_label_sep {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (G : bf.Grp) (j : Fin 4) (h : ℕ) (Cs : Finset (ℤ × ℤ)) (rep : ℕ → ℕ → ℤ × (ℤ × ℤ) × (D.Ms j G).Md → (D.Ms j G).Md) (hrep : ∀ (k₁ k₂ : ℕ) (c : ℤ × (ℤ × ℤ) × (D.Ms j G).Md), rep k₁ k₂ c ∈ (D.Ms j G).predOfMode D.S ⋯ 10 h c) (hsepF : ∀ (k₁ k₂ : ℕ) (c c' : ℤ × (ℤ × ℤ) × (D.Ms j G).Md), (D.Ms j G).nodeLt3 (D.typedNodes G j h Cs k₁ k₂) c c' → rep k₁ k₂ c ≠ rep k₁ k₂ c' → ∀ (z z' : ↥((D.Ms j G).alive (ancAt A.G c'.2.1 (c'.1 - 4 * ↑D.S.K)))), ↑z ∈ (D.Ms j G).predOfMode D.S ⋯ 10 h c → ↑z' ∈ (D.Ms j G).predOfMode D.S ⋯ 10 h c' → z ∉ ((D.Ms j G).blockComps D.S ⋯ c'.1 c'.2.1).F h z') (hΛ : 8 * (D.Ms j G).Λ ≤ D.S.Ξ) {I I' : ℤ × ℤ} (hI : I ∈ Cs) (hI' : I' ∈ Cs) {xs : ℝ} (hxI : xs ∈ dyadicGridCell A.G I.1 I.2) (hxI' : xs ∈ dyadicGridCell A.G I'.1 I'.2) {F F' : Finset (D.Ms j G).Md} (hF : F ∈ D.goodCls G I j h) (hF' : F' ∈ D.goodCls G I' j h) (hκ : D.classTypeOf G I j h F = D.classTypeOf G I' j h F') (hne : (D.Ms j G).slope (↑(D.repAnchor G I j h rep hrep hF)) xs ≠ (D.Ms j G).slope (↑(D.repAnchor G I' j h rep hrep hF')) xs) (cq : ℕ) {Q : ℝ} (hcQ : ↑cq * Q ≤ D.S.Eh h) (N : Fin (D.Ms j G).zc.dim → ℤ) (hN : ∀ (k : Fin (D.Ms j G).zc.dim), |↑(N k)| ≤ Q) : D.S.Ξ / 2 * max (dyadicGridLength A.G I.1)⁻¹ (dyadicGridLength A.G I'.1)⁻¹ < |(D.Ms j G).slope (↑(D.repAnchor G I j h rep hrep hF)) xs - (D.Ms j G).slope (↑(D.repAnchor G I' j h rep hrep hF')) xs + ∑ k : Fin (D.Ms j G).zc.dim, ↑(N k) * (↑cq * ((D.Ms j G).zc.θ k / ↑D.S.Q0 / ModeSchedule.Lh h))|

Blueprint lines 2711-2712 on the side states (labels of representatives along a path): the anchors repAnchor of successful classes of one type at two cells containing the path point x* have different slopes at x* only if they are separated by (Ξ/2) max(|I|⁻¹, |I'|⁻¹) against all shifts N·ζ, ζ = c_q θ/(Q₀ L_h), |N| ≤ Q, c_q Q ≤ E_h (the larger reciprocal scale permits comparison across different cells).

noncomputable def TrilinearHT.Auto.zetaVec (z : ChartTag) (Q0 h : ℕ) : Fin z.dim → ℝ

The separation vector ζ = 6^{Δ-2} ϑ/L_h of the counting lemma in the chart z (blueprint line 2733, Δ = 10), so that 36 ζ = ξ = ϑ/L_{h-Δ}.

Equations

• TrilinearHT.Auto.zetaVec z Q0 h k = ↑(6 ^ 8) * (z.θ k / ↑Q0 / TrilinearHT.Auto.ModeSchedule.Lh h)

theorem TrilinearHT.Auto.ModeSystem.torusξ_eq_zeta {Gd : RealDyadicGrid} {Mc : ℕ} (Ms : ModeSystem Gd Mc) (S : ModeSchedule) {h : ℕ} (hh : 10 ≤ h) (i : Fin Ms.zc.dim) : Ms.torusξ S (h - 10) i = 36 * zetaVec Ms.zc S.Q0 h i

theorem TrilinearHT.Auto.ModeSchedule.Valid.shift_reserve {S : ModeSchedule} {Cj CA CT CK : ℕ} {δs W : ℝ} (hV : S.Valid Cj CA CT CK δs W) (hCA : 1 ≤ CA) (hd2 : 2 ≤ S.dmax) (hD : 2 ≤ S.Dstar) (hB : 2 ≤ S.Bstar) {h : ℕ} (hh : 10 ≤ h) : 288 * 6 ^ 8 * S.Dstar ^ 5 * S.Eh (h - 10) ≤ S.Eh h

The shift reserve of the counting arguments (blueprint lines 2716 and 2735): A₀ ≥ 6^{30} D_*, so 288 · 6^8 D_*^5 E_{h-Δ} ≤ E_h for h ≥ Δ = 10.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.fourRef_of_passes {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (hD : 0 ≤ D.S.Dstar) (hU : 1 ≤ D.U0) (hΔ : D.SP.Δ = 10) {G : bf.Grp} {I : ℤ × ℤ} {xs : ℝ} {h : ℕ} (hh : 10 ≤ h) (z : ChartTag) (hz : (D.Ms 0 G).zc = z) {a : (j : Fin 4) → ↥((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K)))} (hp : D.fourPasses G I xs (h - D.SP.Δ) a) : FourRef (zetaVec z D.S.Q0 h) (D.S.Dstar ^ 5 * D.S.Eh (h - D.SP.Δ)) (D.fourMuBand G I xs (h - D.SP.Δ) a) (2 * D.fourNuBand G I xs (h - D.SP.Δ) a) (dyadicGridLength A.G I.1)⁻¹ fun (j : Fin 4) => (D.Ms j G).slope (↑(a j)) xs

Blueprint lines 2713-2714 (the reference equations of eq:four-tests for the label tuple): the labels x_j = ω_{a_j}(x*) of a four-core tuple passing the test have the reference data FourRef with ζ = ξ/36, shifts in the full box B'_{h-Δ} = D_*^5 E_{h-Δ}, μ and 2ν the dyadic bands, and R = |I|⁻¹.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.threeRef_of_passes {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (hD : 0 ≤ D.S.Dstar) (hU : 1 ≤ D.U0) (hΔ : D.SP.Δ = 10) {G : bf.Grp} {I : ℤ × ℤ} {xs : ℝ} {h : ℕ} (hh : 10 ≤ h) (z : ChartTag) (hz : (D.Ms 0 G).zc = z) {l : Fin 4} {a : Fin 4 → ℝ} (hp : D.threePasses G I xs (h - D.SP.Δ) l a) : ThreeRef (zetaVec z D.S.Q0 h) l (D.S.Dstar ^ 5 * D.S.Eh (h - D.SP.Δ)) (D.threeMuBand G I xs (h - D.SP.Δ) l a) (2 * D.threeNuBand G I xs (h - D.SP.Δ) l a) (dyadicGridLength A.G I.1)⁻¹ a

Blueprint lines 2713-2715 (the T_l reference equation of a passing three-core tuple): the slopes x_j (side entry 0) have the reference data ThreeRef with ζ = ξ/36, the full box, μ and 2ν the dyadic bands, and R = |I|⁻¹.

def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.RepOK {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (G : bf.Grp) (j : Fin 4) (h : ℕ) (Cs : Finset (ℤ × ℤ)) (rep : ℕ → ℕ → ℤ × (ℤ × ℤ) × (D.Ms j G).Md → (D.Ms j G).Md) : Prop

The typed hereditary properties used for the counting: representatives in the predecessors of the nodes, and different representatives on comparable nodes of one type class in different later CURRENT components.

Equations

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

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.path_label_sep' {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (G : bf.Grp) (j : Fin 4) (h : ℕ) (Cs : Finset (ℤ × ℤ)) (rep : ℕ → ℕ → ℤ × (ℤ × ℤ) × (D.Ms j G).Md → (D.Ms j G).Md) (hrep : D.RepOK G j h Cs rep) (hΛ : 8 * (D.Ms j G).Λ ≤ D.S.Ξ) (z : ChartTag) (hz : (D.Ms j G).zc = z) {I I' : ℤ × ℤ} (hI : I ∈ Cs) (hI' : I' ∈ Cs) {xs : ℝ} (hxI : xs ∈ dyadicGridCell A.G I.1 I.2) (hxI' : xs ∈ dyadicGridCell A.G I'.1 I'.2) {F F' : Finset (D.Ms j G).Md} (hF : F ∈ D.goodCls G I j h) (hF' : F' ∈ D.goodCls G I' j h) (hκ : D.classTypeOf G I j h F = D.classTypeOf G I' j h F') (hne : (D.Ms j G).slope (↑(D.repAnchor G I j h rep ⋯ hF)) xs ≠ (D.Ms j G).slope (↑(D.repAnchor G I' j h rep ⋯ hF')) xs) {Q : ℝ} (hcQ : ↑(6 ^ 8) * Q ≤ D.S.Eh h) (N : Fin z.dim → ℤ) (hN : ∀ (k : Fin z.dim), |↑(N k)| ≤ Q) : D.S.Ξ / 2 * max (dyadicGridLength A.G I.1)⁻¹ (dyadicGridLength A.G I'.1)⁻¹ < |(D.Ms j G).slope (↑(D.repAnchor G I j h rep ⋯ hF)) xs - (D.Ms j G).slope (↑(D.repAnchor G I' j h rep ⋯ hF')) xs + ∑ k : Fin z.dim, ↑(N k) * zetaVec z D.S.Q0 h k|

path_label_sep in a common chart z with the separation vector ζ = 6^{Δ-2} ϑ/L_h and the shift bound Q with 6^{Δ-2} Q ≤ E_h (blueprint lines 2716 and 2733).

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.repAnchor_mem {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (G : bf.Grp) (I : ℤ × ℤ) (j : Fin 4) (h : ℕ) (rep : ℕ → ℕ → ℤ × (ℤ × ℤ) × (D.Ms j G).Md → (D.Ms j G).Md) (hrep : ∀ (k₁ k₂ : ℕ) (c : ℤ × (ℤ × ℤ) × (D.Ms j G).Md), rep k₁ k₂ c ∈ (D.Ms j G).predOfMode D.S ⋯ 10 h c) {F : Finset (D.Ms j G).Md} (hF : F ∈ D.goodCls G I j h) : ↑(D.repAnchor G I j h rep hrep hF) ∈ F

The representative of a successful final class lies in the class.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.goodCls_eq_of_mem {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) {G : bf.Grp} {I : ℤ × ℤ} {j : Fin 4} {h : ℕ} {F F' : Finset (D.Ms j G).Md} (hF : F ∈ D.goodCls G I j h) (hF' : F' ∈ D.goodCls G I j h) {y : (D.Ms j G).Md} (hy : y ∈ F) (hy' : y ∈ F') : F = F'

Two successful final classes of one cell sharing a mode are equal (they are CURRENT components).

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.repAnchor_slope_inj {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (G : bf.Grp) (j : Fin 4) (h : ℕ) (Cs : Finset (ℤ × ℤ)) (rep : ℕ → ℕ → ℤ × (ℤ × ℤ) × (D.Ms j G).Md → (D.Ms j G).Md) (hrep : D.RepOK G j h Cs rep) (hΛ : 8 * (D.Ms j G).Λ ≤ D.S.Ξ) (hD : 0 < D.S.Dstar) {I : ℤ × ℤ} (hI : I ∈ Cs) {xs : ℝ} (hxI : xs ∈ dyadicGridCell A.G I.1 I.2) {F F' : Finset (D.Ms j G).Md} (hF : F ∈ D.goodCls G I j h) (hF' : F' ∈ D.goodCls G I j h) (hκ : D.classTypeOf G I j h F = D.classTypeOf G I j h F') (heq : (D.Ms j G).slope (↑(D.repAnchor G I j h rep ⋯ hF)) xs = (D.Ms j G).slope (↑(D.repAnchor G I j h rep ⋯ hF')) xs) : F = F'

Blueprint line 2711 ("distinct labels in a fixed role and type have distinct values by eq:representative-separation at zero shift"): on a cell containing the path point, the representatives of distinct successful classes of one type have distinct slopes at x*.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.winB_le_sideSize {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (G : bf.Grp) (I : ℤ × ℤ) (xs : ℝ) (h' : ℕ) (l : Fin 4) (a : Fin 4 → ℝ) (X : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (i : ℕ) : D.winB G I xs h' l a X i ≤ √((dyadicGridLength A.G I.1)⁻¹ * ∫ (y : ℝ) in dyadicGridLeft A.G I.1 I.2..dyadicGridLeft A.G I.1 I.2 + dyadicGridLength A.G I.1, ‖augPhys X y‖ ^ 2)

Blueprint line 2711 ("in a side role a nonzero use has b_Λ ≥ σ_l, so Parseval also gives M_l^G ≥ 1"): the window size of a side is at most its normalized size ‖S‖_{2,I}, so a side bin σ_l ≤ b_Λ gives σ_l² ≤ r⁻¹ ∫_I |S|² (each nonzero use contributes at least 1 to M_l^G).

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.U0_reserve {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (hD : 2 ≤ D.S.Dstar) : 16 * D.U0 ≤ D.S.Ξ / 2

The band reserve of the pair determination (blueprint line 2716, ν ≤ C U₀ ≪ Ξ): 16 U₀ ≤ Ξ / 2 for D_* ≥ 2 (U₀ = D_*^{250}, Ξ = D_*^{1000}).

The triple tests and the scale multiplicity on the side states (eq:triple-test)

theorem TrilinearHT.Auto.ModeSchedule.Valid.fullBox_le_H {S : ModeSchedule} {Cj CA CT CK : ℕ} {δs W : ℝ} (hV : S.Valid Cj CA CT CK δs W) (hd2 : 2 ≤ S.dmax) (hD : 2 ≤ S.Dstar) (hB : 2 ≤ S.Bstar) (hQ : 1 ≤ S.Q0) {h' : ℕ} (hh : h' ≤ S.Jstar) : S.Dstar ^ 5 * S.Eh h' ≤ S.Dstar ^ 5 * S.H

The full box B'_{h-Δ} = D_*^5 E_{h-Δ} of a height h ≤ J_* is at most D_*^5 H (the height H dominates E_{J_*}, Valid.H_ge).

def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.AncNe {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (G : bf.Grp) (I : ℤ × ℤ) : Prop

The alive sets of the four roles of the group at the decision cell of the cell I are nonempty: anchors of the classes of the cell exist.

Equations

• D.AncNe G I = ∀ (j : Fin 4), ((D.Ms j G).alive (TrilinearHT.Auto.ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K))).Nonempty

def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.AncNe3 {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (G : bf.Grp) (I : ℤ × ℤ) (l : Fin 4) : Prop

The alive sets of the core roles j ≠ l of the group at the decision cell of the cell I are nonempty: anchors of the core classes of the cell exist.

Equations

• D.AncNe3 G I l = ∀ (j : Fin 4), j ≠ l → ((D.Ms j G).alive (TrilinearHT.Auto.ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K))).Nonempty

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.fourPathE {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (G : bf.Grp) (h : ℕ) (xs : ℝ) (cellOf : ℤ → ℤ × ℤ) (ancOf : (s : ℤ) → D.AncNe G (cellOf s) → ℕ → (j : Fin 4) → Finset (D.Ms j G).Md → ↥((D.Ms j G).alive (ancAt A.G (D.preAt (cellOf s)) (A.blkStart D.S.K (cellOf s).1 - 4 * ↑D.S.K)))) (c : ℝ × ℝ × (Fin 4 → ℝ)) (κ : Fin 4 → ℕ × ℕ) (s : ℤ) : Finset (Fin 4 → ℝ)

The tested four-core label tuples at the scale s of a path (blueprint line 2709, "fix the path point x*, final height, all role types, and the frequency and amplitude bins"): the slopes at x* of the anchors of the tested tuples of final classes at the cell cellOf s in the bin c with the role types κ.

Equations

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

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.mem_fourPathE {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) {G : bf.Grp} {h : ℕ} {xs : ℝ} {cellOf : ℤ → ℤ × ℤ} {ancOf : (s : ℤ) → D.AncNe G (cellOf s) → ℕ → (j : Fin 4) → Finset (D.Ms j G).Md → ↥((D.Ms j G).alive (ancAt A.G (D.preAt (cellOf s)) (A.blkStart D.S.K (cellOf s).1 - 4 * ↑D.S.K)))} {c : ℝ × ℝ × (Fin 4 → ℝ)} {κ : Fin 4 → ℕ × ℕ} {s : ℤ} {x : Fin 4 → ℝ} : x ∈ D.fourPathE G h xs cellOf ancOf c κ s ↔ ∃ (hs : D.AncNe G (cellOf s)) (p : (j : Fin 4) → Finset (D.Ms j G).Md), (∀ (j : Fin 4), p j ∈ D.goodCls G (cellOf s) j h) ∧ (D.fourPasses G (cellOf s) xs (h - D.SP.Δ) fun (j : Fin 4) => ancOf s hs h j (p j)) ∧ (∀ (j : Fin 4), 0 < D.clsSize G (cellOf s) j (p j)) ∧ D.fourBinOf G (cellOf s) xs (ancOf s hs) h p = c ∧ (∀ (j : Fin 4), D.classTypeOf G (cellOf s) j h (p j) = κ j) ∧ x = fun (j : Fin 4) => (D.Ms j G).slope (↑(ancOf s hs h j (p j))) xs

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.fourPathE_ref {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (hD : 2 ≤ D.S.Dstar) (hΔ : D.SP.Δ = 10) {G : bf.Grp} (z : ChartTag) (hz : (D.Ms 0 G).zc = z) {h : ℕ} (hh : 10 ≤ h) {xs : ℝ} {cellOf : ℤ → ℤ × ℤ} {ancOf : (s : ℤ) → D.AncNe G (cellOf s) → ℕ → (j : Fin 4) → Finset (D.Ms j G).Md → ↥((D.Ms j G).alive (ancAt A.G (D.preAt (cellOf s)) (A.blkStart D.S.K (cellOf s).1 - 4 * ↑D.S.K)))} {c : ℝ × ℝ × (Fin 4 → ℝ)} {κ : Fin 4 → ℕ × ℕ} {s : ℤ} {x : Fin 4 → ℝ} (hx : x ∈ D.fourPathE G h xs cellOf ancOf c κ s) : FourRef (zetaVec z D.S.Q0 h) (D.S.Dstar ^ 5 * D.S.Eh (h - D.SP.Δ)) c.1 (2 * c.2.1) (dyadicGridLength A.G (cellOf s).1)⁻¹ x

Blueprint lines 2713-2714 and eq:triple-test: the label tuples tested at the scale s of a path in the bin c = (μ, ν, σ) have the reference data FourRef with the full box, the bands μ, 2ν and R_s = |I_s|⁻¹.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.fourMult_le_sched {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) {Cj CA CT CK : ℕ} {δs W : ℝ} (hV : D.S.Valid Cj CA CT CK δs W) (hd2 : 2 ≤ D.S.dmax) (hD : 2 ≤ D.S.Dstar) (hB : 2 ≤ D.S.Bstar) (hQ : 1 ≤ D.S.Q0) (hSP : D.SP = D.S.sideParams δs) {h : ℕ} (hh : h ≤ D.SP.Jst) {d : ℕ} (hd : d ≤ D.S.dmax) {μ ν : ℝ} (hμ : 0 < μ) (hμν : μ ≤ 8 * ν) : 32 * (↑(4 + d) + 1) ^ 4 * (Real.log (2 * (36 * (4 * (D.S.Dstar ^ 5 * D.S.Eh (h - D.SP.Δ))))) + Real.log (2 * (4 * (2 * ν)) / μ)) ≤ 32 * (↑D.S.dmax + 5) ^ 4 * (Real.log (288 * (D.S.Dstar ^ 5 * D.S.H)) + Real.log 2 + 1) * (1 + Real.log (8 * ν / μ))

Blueprint lines 2723-2724 (L₀ ≤ P^C (1 + log(ν/μ))^C, L₀ ≥ 1): at the chosen schedule the multiplicity of fourPathE_mult is at most 32 (d_max + 5)⁴ (log(288 D_*^5 H) + log 2 + 1) (1 + log(8ν/μ)). The factor before 1 + log(8ν/μ) is polynomial in d_max, log D_* and log H, the rational heights and dimensions of the frequency vector.

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.threePathE {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (G : bf.Grp) (h : ℕ) (xs : ℝ) (l : Fin 4) (cellOf : ℤ → ℤ × ℤ) (ancOf : (s : ℤ) → D.AncNe3 G (cellOf s) l → ℕ → (j : Fin 4) → j ≠ l → Finset (D.Ms j G).Md → ↥((D.Ms j G).alive (ancAt A.G (D.preAt (cellOf s)) (A.blkStart D.S.K (cellOf s).1 - 4 * ↑D.S.K)))) (Iw : ℕ) (c : ℝ × ℝ × ℕ × ℝ × (Fin 4 → ℝ)) (κ : Fin 4 → ℕ × ℕ) (s : ℤ) : Finset (Fin 4 → ℝ)

The tested three-core label tuples at the scale s of a path (side role l): the slope tuples (0 in the side role) of the tested tuples and shells at the cell cellOf s in the bin c with the core role types κ.

Equations

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

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.mem_threePathE {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) {G : bf.Grp} {h : ℕ} {xs : ℝ} {l : Fin 4} {cellOf : ℤ → ℤ × ℤ} {ancOf : (s : ℤ) → D.AncNe3 G (cellOf s) l → ℕ → (j : Fin 4) → j ≠ l → Finset (D.Ms j G).Md → ↥((D.Ms j G).alive (ancAt A.G (D.preAt (cellOf s)) (A.blkStart D.S.K (cellOf s).1 - 4 * ↑D.S.K)))} {Iw : ℕ} {c : ℝ × ℝ × ℕ × ℝ × (Fin 4 → ℝ)} {κ : Fin 4 → ℕ × ℕ} {s : ℤ} {x : Fin 4 → ℝ} : x ∈ D.threePathE G h xs l cellOf ancOf Iw c κ s ↔ ∃ (hs : D.AncNe3 G (cellOf s) l), ∃ q ∈ D.threeTested G (cellOf s) xs l (ancOf s hs) (D.toLeaf.sv l G (cellOf s)) Iw h, D.threeBinOf G (cellOf s) xs l (ancOf s hs) (D.toLeaf.sv l G (cellOf s)) h q = c ∧ (∀ (j : Fin 4), j ≠ l → D.classTypeOf G (cellOf s) j h (q.1 j) = κ j) ∧ x = D.slopes3 G (cellOf s) xs l (ancOf s hs) h q.1

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.threePathE_ref {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (hD : 2 ≤ D.S.Dstar) (hΔ : D.SP.Δ = 10) {G : bf.Grp} (z : ChartTag) (hz : (D.Ms 0 G).zc = z) {h : ℕ} (hh : 10 ≤ h) {xs : ℝ} {l : Fin 4} {cellOf : ℤ → ℤ × ℤ} {ancOf : (s : ℤ) → D.AncNe3 G (cellOf s) l → ℕ → (j : Fin 4) → j ≠ l → Finset (D.Ms j G).Md → ↥((D.Ms j G).alive (ancAt A.G (D.preAt (cellOf s)) (A.blkStart D.S.K (cellOf s).1 - 4 * ↑D.S.K)))} {Iw : ℕ} {c : ℝ × ℝ × ℕ × ℝ × (Fin 4 → ℝ)} {κ : Fin 4 → ℕ × ℕ} {s : ℤ} {x : Fin 4 → ℝ} (hx : x ∈ D.threePathE G h xs l cellOf ancOf Iw c κ s) : ThreeRef (zetaVec z D.S.Q0 h) l (D.S.Dstar ^ 5 * D.S.Eh (h - D.SP.Δ)) c.1 (2 * c.2.1) (dyadicGridLength A.G (cellOf s).1)⁻¹ x

Blueprint eq:triple-test for three cores (lines 2718-2722, "for three it is the nonzero T_l test"): the label tuples tested at the scale s of a path in the bin c = (μ, ν, Λ, b, σ) have the reference data ThreeRef (μ R_s ≤ |T_l + n·ξ| ≤ 2ν R_s, |n| ≤ B'_{h-Δ}).

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.mult_le_sched {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) {Cj CA CT CK : ℕ} {δs W : ℝ} (hV : D.S.Valid Cj CA CT CK δs W) (hd2 : 2 ≤ D.S.dmax) (hD : 2 ≤ D.S.Dstar) (hB : 2 ≤ D.S.Bstar) (hQ : 1 ≤ D.S.Q0) (hSP : D.SP = D.S.sideParams δs) {h : ℕ} (hh : h ≤ D.SP.Jst) {d : ℕ} (hd : d ≤ D.S.dmax) {B μ ν : ℝ} (hB1 : 1 ≤ B) (hBE : B ≤ 4 * (D.S.Dstar ^ 5 * D.S.Eh (h - D.SP.Δ))) (hμ : 0 < μ) (hμν : μ ≤ ν) : 32 * (↑(4 + d) + 1) ^ 4 * (Real.log (2 * (36 * B)) + Real.log (2 * ν / μ)) ≤ 32 * (↑D.S.dmax + 5) ^ 4 * (Real.log (288 * (D.S.Dstar ^ 5 * D.S.H)) + Real.log 2 + 1) * (1 + Real.log (ν / μ))

The multiplicity bound of lem:height at the chosen schedule (blueprint lines 2723-2724, L₀ ≤ P^C (1 + log(ν/μ))^C): for box sizes 1 ≤ B ≤ 4 D_*^5 E_{h-Δ}, 32 (d + 5)⁴ (log(72 B) + log(2ν/μ)) is at most 32 (d_max + 5)⁴ (log(288 D_*^5 H) + log 2 + 1)(1 + log(ν/μ)); the first factor is polynomial in the dimension and the logarithmic heights log D_*, log H.

The total counts on the side states (eq:total-count)

theorem TrilinearHT.Auto.four_core_total_abstract {d : ℕ} (ζ : Fin d → ℝ) (S : Finset ℤ) (E : ℤ → Finset (Fin 4 → ℝ)) (Al : Fin 4 → Finset ℝ) (hAl : ∀ s ∈ S, ∀ x ∈ E s, ∀ (j : Fin 4), x j ∈ Al j) {B μ ν R₀ Q Sg : ℝ} (hB : 1 ≤ B) (hμ : 0 < μ) (hμν : μ ≤ ν) (hR₀ : 0 < R₀) (href : ∀ s ∈ S, ∀ x ∈ E s, FourRef ζ B μ ν (R₀ * 2 ^ s) x) (hsep : ∀ (r : Fin 4), ∀ s ∈ S, ∀ s' ∈ S, ∀ x ∈ E s, ∀ x' ∈ E s', x r ≠ x' r → ∀ (N : Fin d → ℤ), (∀ (p : Fin d), |↑(N p)| ≤ Q) → Sg * max (R₀ * 2 ^ s) (R₀ * 2 ^ s') < |x r - x' r + ∑ p : Fin d, ↑(N p) * ζ p|) (hQ : 288 * B ≤ Q) (hSg : 8 * ν ≤ Sg) : (∀ (i j : Fin 4), i ≠ j → ∑ s ∈ S, ↑(E s).card ≤ fourMult d B μ ν * ↑(Al i).card * ↑(Al j).card) ∧ ∀ (i j : Fin 4), i ≠ j → ∀ s ∈ S, ↑(E s).card ≤ ↑(Al i).card * ↑(Al j).card

Blueprint eq:total-count for four cores, abstract form: label tuples E_s with reference data at the scales R₀ 2^s, labels in the sets A_j, and same-role labels separated against the reserved shifts. Then two labels determine the tuple across all scales (four_core_pair), each tuple occurs at at most L₀ = fourMult scales (tested_scale_mult), so Σ_s N_s ≤ L₀ |A_i| |A_j| and N_s ≤ |A_i| |A_j| for distinct roles i, j.

theorem TrilinearHT.Auto.three_core_total_abstract {d : ℕ} (ζ : Fin d → ℝ) (l : Fin 4) (S : Finset ℤ) (E : ℤ → Finset (Fin 4 → ℝ)) (Al : Fin 4 → Finset ℝ) (hAl : ∀ s ∈ S, ∀ x ∈ E s, ∀ (j : Fin 4), j ≠ l → x j ∈ Al j) (hxl : ∀ s ∈ S, ∀ x ∈ E s, x l = 0) {B μ ν R₀ Q Sg : ℝ} (hB : 1 ≤ B) (hμ : 0 < μ) (hμν : μ ≤ ν) (hR₀ : 0 < R₀) (href : ∀ s ∈ S, ∀ x ∈ E s, ThreeRef ζ l B μ ν (R₀ * 2 ^ s) x) (hsep : ∀ (r : Fin 4), ∀ s ∈ S, ∀ s' ∈ S, ∀ x ∈ E s, ∀ x' ∈ E s', x r ≠ x' r → ∀ (N : Fin d → ℤ), (∀ (p : Fin d), |↑(N p)| ≤ Q) → Sg * max (R₀ * 2 ^ s) (R₀ * 2 ^ s') < |x r - x' r + ∑ p : Fin d, ↑(N p) * ζ p|) (hQ : 72 * B ≤ Q) (hSg : 2 * ν ≤ Sg) (w : ℤ → ℝ) (hinc : ∀ s ∈ S, ∀ (i : Fin 4), i ≠ l → ∀ (a : ℝ), ↑{x ∈ E s | x i = a}.card ≤ w s) : (∀ (i j : Fin 4), i ≠ j → i ≠ l → j ≠ l → ∑ s ∈ S, ↑(E s).card ≤ threeMult d B μ ν * ↑(Al i).card * ↑(Al j).card) ∧ (∀ (i : Fin 4), i ≠ l → ∑ s ∈ S, ↑(E s).card ≤ ↑(Al i).card * ∑ s ∈ S, w s) ∧ ∀ (i j : Fin 4), i ≠ j → i ≠ l → j ≠ l → ∀ s ∈ S, ↑(E s).card ≤ ↑(Al i).card * ↑(Al j).card

Blueprint eq:total-count for three cores (side role l), abstract form: label tuples with side entry 0 and the T_l reference data at the scales R₀ 2^s, core labels in the sets A_j, same-role labels separated against the reserved shifts, and for every core label a at most w_s tuples at the scale s incident to it (side incidence). Then Σ_s N_s ≤ L₀ |A_i| |A_j| for core roles, Σ_s N_s ≤ |A_i| Σ_s w_s for a core/side pair, and N_s ≤ |A_i| |A_j|.

theorem TrilinearHT.Auto.ThreeRef.mono {d : ℕ} {ζ : Fin d → ℝ} {l : Fin 4} {B B' μ ν R : ℝ} {x : Fin 4 → ℝ} (hx : ThreeRef ζ l B μ ν R x) (hB : B ≤ B') : ThreeRef ζ l B' μ ν R x

def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.FourPathAnc {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (G : bf.Grp) (h : ℕ) (Cs : Finset (ℤ × ℤ)) (rep : (j : Fin 4) → ℕ → ℕ → ℤ × (ℤ × ℤ) × (D.Ms j G).Md → (D.Ms j G).Md) (hrep : ∀ (j : Fin 4), D.RepOK G j h Cs (rep j)) (cellOf : ℤ → ℤ × ℤ) (ancOf : (s : ℤ) → D.AncNe G (cellOf s) → ℕ → (j : Fin 4) → Finset (D.Ms j G).Md → ↥((D.Ms j G).alive (ancAt A.G (D.preAt (cellOf s)) (A.blkStart D.S.K (cellOf s).1 - 4 * ↑D.S.K)))) (S : Finset ℤ) : Prop

The anchors along a path are the representatives of the successful classes (four cores).

Equations

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

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.four_path_sep {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (G : bf.Grp) (h : ℕ) (Cs : Finset (ℤ × ℤ)) (rep : (j : Fin 4) → ℕ → ℕ → ℤ × (ℤ × ℤ) × (D.Ms j G).Md → (D.Ms j G).Md) (hrep : ∀ (j : Fin 4), D.RepOK G j h Cs (rep j)) (hΛ : ∀ (j : Fin 4), 8 * (D.Ms j G).Λ ≤ D.S.Ξ) (z : ChartTag) (hz : ∀ (j : Fin 4), (D.Ms j G).zc = z) {Q : ℝ} (hcQ : ↑(6 ^ 8) * Q ≤ D.S.Eh h) {S : Finset ℤ} {cellOf : ℤ → ℤ × ℤ} {xs : ℝ} (hpath : ∀ s ∈ S, cellOf s ∈ Cs ∧ xs ∈ dyadicGridCell A.G (cellOf s).1 (cellOf s).2) (hcell : ∀ (s : ℤ), (cellOf s).1 = s) {ancOf : (s : ℤ) → D.AncNe G (cellOf s) → ℕ → (j : Fin 4) → Finset (D.Ms j G).Md → ↥((D.Ms j G).alive (ancAt A.G (D.preAt (cellOf s)) (A.blkStart D.S.K (cellOf s).1 - 4 * ↑D.S.K)))} (hanc : D.FourPathAnc G h Cs rep hrep cellOf ancOf S) (c : ℝ × ℝ × (Fin 4 → ℝ)) (κ : Fin 4 → ℕ × ℕ) (r : Fin 4) (s : ℤ) : s ∈ S → ∀ s' ∈ S, ∀ x ∈ D.fourPathE G h xs cellOf ancOf c κ s, ∀ x' ∈ D.fourPathE G h xs cellOf ancOf c κ s', x r ≠ x' r → ∀ (N : Fin z.dim → ℤ), (∀ (p : Fin z.dim), |↑(N p)| ≤ Q) → D.S.Ξ / 2 * max (A.G.baseLength⁻¹ * 2 ^ s) (A.G.baseLength⁻¹ * 2 ^ s') < |x r - x' r + ∑ p : Fin z.dim, ↑(N p) * zetaVec z D.S.Q0 h p|

Blueprint lines 2711-2716 along a path (four cores): distinct same-role labels of tuples tested at the scales s, s' are separated by (Ξ/2) max(R_s, R_{s'}) against all reserved shifts.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.four_core_total_side {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) {Cj CA CT CK : ℕ} {δs W : ℝ} (hV : D.S.Valid Cj CA CT CK δs W) (hCA : 1 ≤ CA) (hd2 : 2 ≤ D.S.dmax) (hD : 2 ≤ D.S.Dstar) (hB : 2 ≤ D.S.Bstar) (hΔ : D.SP.Δ = 10) (G : bf.Grp) (h : ℕ) (hh : 10 ≤ h) (Cs : Finset (ℤ × ℤ)) (rep : (j : Fin 4) → ℕ → ℕ → ℤ × (ℤ × ℤ) × (D.Ms j G).Md → (D.Ms j G).Md) (hrep : ∀ (j : Fin 4), D.RepOK G j h Cs (rep j)) (hΛ : ∀ (j : Fin 4), 8 * (D.Ms j G).Λ ≤ D.S.Ξ) (z : ChartTag) (hz : ∀ (j : Fin 4), (D.Ms j G).zc = z) {S : Finset ℤ} {cellOf : ℤ → ℤ × ℤ} {xs : ℝ} (hpath : ∀ s ∈ S, cellOf s ∈ Cs ∧ xs ∈ dyadicGridCell A.G (cellOf s).1 (cellOf s).2) (hcell : ∀ (s : ℤ), (cellOf s).1 = s) {ancOf : (s : ℤ) → D.AncNe G (cellOf s) → ℕ → (j : Fin 4) → Finset (D.Ms j G).Md → ↥((D.Ms j G).alive (ancAt A.G (D.preAt (cellOf s)) (A.blkStart D.S.K (cellOf s).1 - 4 * ↑D.S.K)))} (hanc : D.FourPathAnc G h Cs rep hrep cellOf ancOf S) (c : ℝ × ℝ × (Fin 4 → ℝ)) (κ : Fin 4 → ℕ × ℕ) : (∀ (i j : Fin 4), i ≠ j → ∑ s ∈ S, ↑(D.fourPathE G h xs cellOf ancOf c κ s).card ≤ fourMult z.dim (D.S.Dstar ^ 5 * D.S.Eh (h - D.SP.Δ)) c.1 (2 * c.2.1) * ↑(S.biUnion fun (s : ℤ) => Finset.image (fun (x : Fin 4 → ℝ) => x i) (D.fourPathE G h xs cellOf ancOf c κ s)).card * ↑(S.biUnion fun (s : ℤ) => Finset.image (fun (x : Fin 4 → ℝ) => x j) (D.fourPathE G h xs cellOf ancOf c κ s)).card) ∧ ∀ (i j : Fin 4), i ≠ j → ∀ s ∈ S, ↑(D.fourPathE G h xs cellOf ancOf c κ s).card ≤ ↑(S.biUnion fun (s : ℤ) => Finset.image (fun (x : Fin 4 → ℝ) => x i) (D.fourPathE G h xs cellOf ancOf c κ s)).card * ↑(S.biUnion fun (s : ℤ) => Finset.image (fun (x : Fin 4 → ℝ) => x j) (D.fourPathE G h xs cellOf ancOf c κ s)).card

Blueprint eq:total-count for four cores on the side states (lines 2726-2729): along a path, with the anchors given by the representatives, fixed height, types and bin, the tested label sets E_s satisfy Σ_s N_s ≤ L₀ |A_i| |A_j| (L₀ = fourMult) and N_s ≤ |A_i| |A_j| for distinct roles i, j, where A_j is the set of labels of role j along the path.

theorem TrilinearHT.Auto.ModeSchedule.Valid.window_reserve {S : ModeSchedule} {Cj CA CT CK : ℕ} {δs W : ℝ} (hV : S.Valid Cj CA CT CK δs W) (hCA : 1 ≤ CA) (hd2 : 2 ≤ S.dmax) (hD : 2 ≤ S.Dstar) (hB : 2 ≤ S.Bstar) {h : ℕ} (hh : 10 ≤ h) : 18432 * 6 ^ 8 * S.Dstar ^ 5 * S.Eh (h - 10) ≤ S.Eh h

The window shift reserve of the side incidence (blueprint lines 2726-2727, windows with the box 16 B'_{h-Δ}): 1152 · 16 · 6^8 D_*^5 E_{h-Δ} ≤ E_h for h ≥ Δ = 10 (A₀ ≥ 6^{30} D_*).

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.U0_window_reserve {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (hD : 2 ≤ D.S.Dstar) : 128 * D.U0 ≤ D.S.Ξ / 2

The band reserve of the side incidence (blueprint line 2727, ν, Λ ≤ C U₀ ≪ Ξ): 128 U₀ ≤ Ξ / 2 for D_* ≥ 2 (U₀ = D_*^{250}, Ξ = D_*^{1000}).

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.threeWin_eq_sideWindow {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (hD : 0 ≤ D.S.Dstar) (hΔ : D.SP.Δ = 10) {G : bf.Grp} (z : ChartTag) (hz : (D.Ms 0 G).zc = z) {h : ℕ} (hh : 10 ≤ h) (I : ℤ × ℤ) (xs : ℝ) {l : Fin 4} {a : Fin 4 → ℝ} (hal : a l = 0) (Λ : ℝ) : D.threeWin G I xs (h - D.SP.Δ) l a Λ = sideWindow (zetaVec z D.S.Q0 h) (dyadicGridLength A.G I.1) Λ (16 * (D.S.Dstar ^ 5 * D.S.Eh (h - D.SP.Δ))) a

The three-core side windows are the abstract side windows sideWindow (blueprint lines 2556-2560 and 2726): for a tuple with side entry 0, Q = Σ_{j ≠ l} a_j = Σ_j a_j and n·ξ = 36 n·ζ (ξ = ϑ/L_{h-Δ}, ζ = 6^{Δ-2} ϑ/L_h), with the box 16 B'_{h-Δ}.

def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.ThreePathAnc {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (G : bf.Grp) (h : ℕ) (l : Fin 4) (Cs : Finset (ℤ × ℤ)) (rep : (j : Fin 4) → ℕ → ℕ → ℤ × (ℤ × ℤ) × (D.Ms j G).Md → (D.Ms j G).Md) (hrep : ∀ (j : Fin 4), D.RepOK G j h Cs (rep j)) (cellOf : ℤ → ℤ × ℤ) (ancOf : (s : ℤ) → D.AncNe3 G (cellOf s) l → ℕ → (j : Fin 4) → j ≠ l → Finset (D.Ms j G).Md → ↥((D.Ms j G).alive (ancAt A.G (D.preAt (cellOf s)) (A.blkStart D.S.K (cellOf s).1 - 4 * ↑D.S.K)))) (S : Finset ℤ) : Prop

The anchors along a path are the representatives of the successful classes (three cores with side role l).

Equations

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

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.three_path_sep {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (G : bf.Grp) (h : ℕ) (l : Fin 4) (Cs : Finset (ℤ × ℤ)) (rep : (j : Fin 4) → ℕ → ℕ → ℤ × (ℤ × ℤ) × (D.Ms j G).Md → (D.Ms j G).Md) (hrep : ∀ (j : Fin 4), D.RepOK G j h Cs (rep j)) (hΛ : ∀ (j : Fin 4), 8 * (D.Ms j G).Λ ≤ D.S.Ξ) (z : ChartTag) (hz : ∀ (j : Fin 4), (D.Ms j G).zc = z) {Q : ℝ} (hcQ : ↑(6 ^ 8) * Q ≤ D.S.Eh h) {S : Finset ℤ} {cellOf : ℤ → ℤ × ℤ} {xs : ℝ} (hpath : ∀ s ∈ S, cellOf s ∈ Cs ∧ xs ∈ dyadicGridCell A.G (cellOf s).1 (cellOf s).2) {ancOf : (s : ℤ) → D.AncNe3 G (cellOf s) l → ℕ → (j : Fin 4) → j ≠ l → Finset (D.Ms j G).Md → ↥((D.Ms j G).alive (ancAt A.G (D.preAt (cellOf s)) (A.blkStart D.S.K (cellOf s).1 - 4 * ↑D.S.K)))} (hanc : D.ThreePathAnc G h l Cs rep hrep cellOf ancOf S) (Iw : ℕ) (c : ℝ × ℝ × ℕ × ℝ × (Fin 4 → ℝ)) (κ : Fin 4 → ℕ × ℕ) (r : Fin 4) (s : ℤ) : s ∈ S → ∀ s' ∈ S, ∀ x ∈ D.threePathE G h xs l cellOf ancOf Iw c κ s, ∀ x' ∈ D.threePathE G h xs l cellOf ancOf Iw c κ s', x r ≠ x' r → ∀ (N : Fin z.dim → ℤ), (∀ (p : Fin z.dim), |↑(N p)| ≤ Q) → D.S.Ξ / 2 * max (dyadicGridLength A.G (cellOf s).1)⁻¹ (dyadicGridLength A.G (cellOf s').1)⁻¹ < |x r - x' r + ∑ p : Fin z.dim, ↑(N p) * zetaVec z D.S.Q0 h p|

Blueprint lines 2711-2716 along a path (three cores, side role l): distinct same-role labels of tuples tested at the cells of the scales s, s' are separated by (Ξ/2) max(R_s, R_{s'}) against all reserved shifts (the side entries are 0).

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.sideWeight {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (G : bf.Grp) (l : Fin 4) (cellOf : ℤ → ℤ × ℤ) (σl : ℝ) (s : ℤ) : ℝ

The side incidence weight w_s = σ_l^{-2} ‖S_{l,G,s}‖²_{2,I_s} of the scale s of a path (blueprint line 2728), with ‖S‖²_{2,I} = r⁻¹ ∫_I |S_phys|².

Equations

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

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.sideWeight_nonneg {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (G : bf.Grp) (l : Fin 4) (cellOf : ℤ → ℤ × ℤ) (σl : ℝ) (s : ℤ) : 0 ≤ D.sideWeight G l cellOf σl s

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.three_side_incidence {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) {Cj CA CT CK : ℕ} {δs W : ℝ} (hV : D.S.Valid Cj CA CT CK δs W) (hCA : 1 ≤ CA) (hd2 : 2 ≤ D.S.dmax) (hD : 2 ≤ D.S.Dstar) (hB : 2 ≤ D.S.Bstar) (hΔ : D.SP.Δ = 10) (G : bf.Grp) (h : ℕ) (hh : 10 ≤ h) (l : Fin 4) (Cs : Finset (ℤ × ℤ)) (rep : (j : Fin 4) → ℕ → ℕ → ℤ × (ℤ × ℤ) × (D.Ms j G).Md → (D.Ms j G).Md) (hrep : ∀ (j : Fin 4), D.RepOK G j h Cs (rep j)) (hΛ : ∀ (j : Fin 4), 8 * (D.Ms j G).Λ ≤ D.S.Ξ) (z : ChartTag) (hz : ∀ (j : Fin 4), (D.Ms j G).zc = z) {S : Finset ℤ} {cellOf : ℤ → ℤ × ℤ} {xs : ℝ} (hpath : ∀ s ∈ S, cellOf s ∈ Cs ∧ xs ∈ dyadicGridCell A.G (cellOf s).1 (cellOf s).2) {ancOf : (s : ℤ) → D.AncNe3 G (cellOf s) l → ℕ → (j : Fin 4) → j ≠ l → Finset (D.Ms j G).Md → ↥((D.Ms j G).alive (ancAt A.G (D.preAt (cellOf s)) (A.blkStart D.S.K (cellOf s).1 - 4 * ↑D.S.K)))} (hanc : D.ThreePathAnc G h l Cs rep hrep cellOf ancOf S) {Iw : ℕ} (hIw : 2 ^ Iw ≤ 2 * D.U0) (c : ℝ × ℝ × ℕ × ℝ × (Fin 4 → ℝ)) (κ : Fin 4 → ℕ × ℕ) {s : ℤ} (hs : s ∈ S) {i : Fin 4} (hil : i ≠ l) (a : ℝ) : ↑{x ∈ D.threePathE G h xs l cellOf ancOf Iw c κ s | x i = a}.card ≤ D.sideWeight G l cellOf c.2.2.2.1 s

Blueprint lines 2726-2728 (side incidence on the side states): at one scale s of a path, the tested three-core tuples of the bin c = (μ, ν, i, σ_l, σ) incident to a fixed core label a in the role i ≠ l have pairwise disjoint side windows (sideWindow_disjoint: window box 16 B'_{h-Δ}, Λ = 2^i ≤ 2^{I_w} ≤ 2 U₀), each of window energy at least (r σ_l)²; Bessel for each offset and the expectation bound their number by w_s = σ_l^{-2} ‖S_{l,G,s}‖²_{2,I_s}.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.three_core_total_side {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) {Cj CA CT CK : ℕ} {δs W : ℝ} (hV : D.S.Valid Cj CA CT CK δs W) (hCA : 1 ≤ CA) (hd2 : 2 ≤ D.S.dmax) (hD : 2 ≤ D.S.Dstar) (hB : 2 ≤ D.S.Bstar) (hΔ : D.SP.Δ = 10) (G : bf.Grp) (h : ℕ) (hh : 10 ≤ h) (l : Fin 4) (Cs : Finset (ℤ × ℤ)) (rep : (j : Fin 4) → ℕ → ℕ → ℤ × (ℤ × ℤ) × (D.Ms j G).Md → (D.Ms j G).Md) (hrep : ∀ (j : Fin 4), D.RepOK G j h Cs (rep j)) (hΛ : ∀ (j : Fin 4), 8 * (D.Ms j G).Λ ≤ D.S.Ξ) (z : ChartTag) (hz : ∀ (j : Fin 4), (D.Ms j G).zc = z) {S : Finset ℤ} {cellOf : ℤ → ℤ × ℤ} {xs : ℝ} (hpath : ∀ s ∈ S, cellOf s ∈ Cs ∧ xs ∈ dyadicGridCell A.G (cellOf s).1 (cellOf s).2) (hcell : ∀ (s : ℤ), (cellOf s).1 = s) {ancOf : (s : ℤ) → D.AncNe3 G (cellOf s) l → ℕ → (j : Fin 4) → j ≠ l → Finset (D.Ms j G).Md → ↥((D.Ms j G).alive (ancAt A.G (D.preAt (cellOf s)) (A.blkStart D.S.K (cellOf s).1 - 4 * ↑D.S.K)))} (hanc : D.ThreePathAnc G h l Cs rep hrep cellOf ancOf S) {Iw : ℕ} (hIw : 2 ^ Iw ≤ 2 * D.U0) (c : ℝ × ℝ × ℕ × ℝ × (Fin 4 → ℝ)) (κ : Fin 4 → ℕ × ℕ) : (∀ (i j : Fin 4), i ≠ j → i ≠ l → j ≠ l → ∑ s ∈ S, ↑(D.threePathE G h xs l cellOf ancOf Iw c κ s).card ≤ threeMult z.dim (D.S.Dstar ^ 5 * D.S.Eh (h - D.SP.Δ)) c.1 (2 * c.2.1) * ↑(S.biUnion fun (s : ℤ) => Finset.image (fun (x : Fin 4 → ℝ) => x i) (D.threePathE G h xs l cellOf ancOf Iw c κ s)).card * ↑(S.biUnion fun (s : ℤ) => Finset.image (fun (x : Fin 4 → ℝ) => x j) (D.threePathE G h xs l cellOf ancOf Iw c κ s)).card) ∧ (∀ (i : Fin 4), i ≠ l → ∑ s ∈ S, ↑(D.threePathE G h xs l cellOf ancOf Iw c κ s).card ≤ ↑(S.biUnion fun (s : ℤ) => Finset.image (fun (x : Fin 4 → ℝ) => x i) (D.threePathE G h xs l cellOf ancOf Iw c κ s)).card * ∑ s ∈ S, D.sideWeight G l cellOf c.2.2.2.1 s) ∧ ∀ (i j : Fin 4), i ≠ j → i ≠ l → j ≠ l → ∀ s ∈ S, ↑(D.threePathE G h xs l cellOf ancOf Iw c κ s).card ≤ ↑(S.biUnion fun (s : ℤ) => Finset.image (fun (x : Fin 4 → ℝ) => x i) (D.threePathE G h xs l cellOf ancOf Iw c κ s)).card * ↑(S.biUnion fun (s : ℤ) => Finset.image (fun (x : Fin 4 → ℝ) => x j) (D.threePathE G h xs l cellOf ancOf Iw c κ s)).card

Blueprint eq:total-count for three cores on the side states (lines 2726-2729, side role l): along a path, with the anchors given by the representatives, fixed height, core types and bin c = (μ, ν, i, σ_l, σ), the tested label sets E_s (tuples tested with the shell Λ = 2^i of the bin) satisfy Σ_s N_s ≤ L₀ |A_i| |A_j| (L₀ = threeMult) and N_s ≤ |A_i| |A_j| for distinct core roles i, j, and Σ_s N_s ≤ |A_i| Σ_s w_s for a core role i and the side (w_s = σ_l^{-2} ‖S_{l,G,s}‖²_{2,I_s}, Σ_s w_s = M_l^G); here A_j is the set of labels of role j along the path.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.fourPathE_card {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (G : bf.Grp) (h : ℕ) (Cs : Finset (ℤ × ℤ)) (rep : (j : Fin 4) → ℕ → ℕ → ℤ × (ℤ × ℤ) × (D.Ms j G).Md → (D.Ms j G).Md) (hrep : ∀ (j : Fin 4), D.RepOK G j h Cs (rep j)) (hΛ : ∀ (j : Fin 4), 8 * (D.Ms j G).Λ ≤ D.S.Ξ) (hD : 0 < D.S.Dstar) {S : Finset ℤ} {cellOf : ℤ → ℤ × ℤ} {xs : ℝ} (hpath : ∀ s ∈ S, cellOf s ∈ Cs ∧ xs ∈ dyadicGridCell A.G (cellOf s).1 (cellOf s).2) {ancOf : (s : ℤ) → D.AncNe G (cellOf s) → ℕ → (j : Fin 4) → Finset (D.Ms j G).Md → ↥((D.Ms j G).alive (ancAt A.G (D.preAt (cellOf s)) (A.blkStart D.S.K (cellOf s).1 - 4 * ↑D.S.K)))} (hanc : D.FourPathAnc G h Cs rep hrep cellOf ancOf S) (c : ℝ × ℝ × (Fin 4 → ℝ)) (κ : Fin 4 → ℕ × ℕ) {s : ℤ} (hs : s ∈ S) (hA : D.AncNe G (cellOf s)) : (D.fourPathE G h xs cellOf ancOf c κ s).card = {p ∈ D.fourTested G (cellOf s) xs (ancOf s hA) h | D.fourBinOf G (cellOf s) xs (ancOf s hA) h p = c ∧ ∀ (j : Fin 4), D.classTypeOf G (cellOf s) j h (p j) = κ j}.card

Blueprint line 2711 ("identify a representative with its fixed real value"), four cores: along a path with the representatives as anchors, distinct tested tuples of one type in one bin have distinct label tuples, so N_s = |E_s| is the number of tested tuples in the bin.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.threePathE_card {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (G : bf.Grp) (h : ℕ) (l : Fin 4) (Cs : Finset (ℤ × ℤ)) (rep : (j : Fin 4) → ℕ → ℕ → ℤ × (ℤ × ℤ) × (D.Ms j G).Md → (D.Ms j G).Md) (hrep : ∀ (j : Fin 4), D.RepOK G j h Cs (rep j)) (hΛ : ∀ (j : Fin 4), 8 * (D.Ms j G).Λ ≤ D.S.Ξ) (hD : 0 < D.S.Dstar) {S : Finset ℤ} {cellOf : ℤ → ℤ × ℤ} {xs : ℝ} (hpath : ∀ s ∈ S, cellOf s ∈ Cs ∧ xs ∈ dyadicGridCell A.G (cellOf s).1 (cellOf s).2) {ancOf : (s : ℤ) → D.AncNe3 G (cellOf s) l → ℕ → (j : Fin 4) → j ≠ l → Finset (D.Ms j G).Md → ↥((D.Ms j G).alive (ancAt A.G (D.preAt (cellOf s)) (A.blkStart D.S.K (cellOf s).1 - 4 * ↑D.S.K)))} (hanc : D.ThreePathAnc G h l Cs rep hrep cellOf ancOf S) (Iw : ℕ) (c : ℝ × ℝ × ℕ × ℝ × (Fin 4 → ℝ)) (κ : Fin 4 → ℕ × ℕ) {s : ℤ} (hs : s ∈ S) (hA : D.AncNe3 G (cellOf s) l) : (D.threePathE G h xs l cellOf ancOf Iw c κ s).card = {q ∈ D.threeTested G (cellOf s) xs l (ancOf s hA) (D.toLeaf.sv l G (cellOf s)) Iw h | D.threeBinOf G (cellOf s) xs l (ancOf s hA) (D.toLeaf.sv l G (cellOf s)) h q = c ∧ ∀ (j : Fin 4), j ≠ l → D.classTypeOf G (cellOf s) j h (q.1 j) = κ j}.card

Blueprint line 2711 for three cores (side role l): along a path with the representatives as anchors, distinct tested tuples and shells of one type in one bin have distinct label tuples, so N_s = |E_s| is the number of tested tuples and shells in the bin.

The applied sparse count on the side states (eq:applied-sparse)

theorem TrilinearHT.Auto.four_core_sparse_explicit (d : ℕ) (ζ : Fin d → ℝ) (A : Fin 4 → Finset ℝ) (M L : ℝ) : 1 ≤ M → 1 ≤ L → (∀ (i : Fin 4), ↑(A i).card ≤ M) → ∀ (B Sg Q μ ν R₀ : ℝ), 1 ≤ B → 0 < μ → μ ≤ 1 → 1 ≤ ν → 0 < R₀ → ∀ (S : Finset ℤ) (E : ℤ → Finset (Fin 4 → ℝ)), (∀ s ∈ S, ∀ x ∈ E s, ∀ (i : Fin 4), x i ∈ A i) → (∀ (x : Fin 4 → ℝ), ↑{s ∈ S | x ∈ E s}.card ≤ L) → (∀ s ∈ S, ∀ x ∈ E s, FourRef ζ B μ ν (R₀ * 2 ^ s) x) → (∀ (i : Fin 4), ∀ s ∈ S, ∀ s' ∈ S, ∀ x ∈ E s, ∀ x' ∈ E s', x i ≠ x' i → ∀ (n : Fin d → ℤ), (∀ (k : Fin d), |↑(n k)| ≤ Q) → Sg * max (R₀ * 2 ^ s) (R₀ * 2 ^ s') < |x i - x' i + ∑ k : Fin d, ↑(n k) * ζ k|) → (∀ s ∈ S, (E s).Nonempty → ∀ (n : Fin d → ℤ), (∀ (k : Fin d), |↑(n k)| ≤ Q) → |∑ k : Fin d, ↑(n k) * ζ k| ∉ Set.Icc (μ * (R₀ * 2 ^ s) / 1000) (1000 * (4 * ν) * (R₀ * 2 ^ s))) → 7200000 * (↑d + 1) ^ 2 * (4 * B) ≤ Q → 288 * B ≤ Q → 7200000 * (↑d + 1) ^ 2 * (4 * ν) ≤ Sg → 8 * ν ≤ Sg → ∀ (δ : ℝ), 0 < δ → δ ≤ 1 → ∑ s ∈ S with ↑(E s).card ≤ δ * M ^ 2, ↑(E s).card ≤ 3 * 10 ^ 11 * (1 + Real.logb 2 (2 + (↑d + 1) ^ 2 * (4 * ν) / μ)) * L ^ 12 * δ ^ (1 / 300) * M ^ 2

four_core_sparse_count with the explicit constants C = 3 · 10^{11}, C_res = 7200000 of sparse_count_explicit (blueprint eq:applied-sparse, lines 2731-2741).

theorem TrilinearHT.Auto.three_core_sparse_explicit (d : ℕ) (ζ : Fin d → ℝ) (l : Fin 4) (A : Fin 4 → Finset ℝ) (M L : ℝ) : 1 ≤ M → 1 ≤ L → (∀ (i : Fin 4), i ≠ l → ↑(A i).card ≤ M) → ∀ (B Sg Q μ ν R₀ : ℝ), 1 ≤ B → 0 < μ → μ ≤ 1 → 1 ≤ ν → 0 < R₀ → ∀ (S : Finset ℤ) (E : ℤ → Finset (Fin 4 → ℝ)), (∀ s ∈ S, ∀ x ∈ E s, (∀ (i : Fin 4), i ≠ l → x i ∈ A i) ∧ x l = 0) → (∀ (x : Fin 4 → ℝ), ↑{s ∈ S | x ∈ E s}.card ≤ L) → (∃ (w : ℤ → ℝ), (∀ (s : ℤ), 0 ≤ w s) ∧ ∑ s ∈ S, w s ≤ M ∧ ∀ s ∈ S, ∀ (i : Fin 4), i ≠ l → ∀ (a : ℝ), ↑{x ∈ E s | x i = a}.card ≤ w s) → (∀ s ∈ S, ∀ x ∈ E s, ThreeRef ζ l B μ ν (R₀ * 2 ^ s) x) → (∀ (i : Fin 4), ∀ s ∈ S, ∀ s' ∈ S, ∀ x ∈ E s, ∀ x' ∈ E s', x i ≠ x' i → ∀ (n : Fin d → ℤ), (∀ (k : Fin d), |↑(n k)| ≤ Q) → Sg * max (R₀ * 2 ^ s) (R₀ * 2 ^ s') < |x i - x' i + ∑ k : Fin d, ↑(n k) * ζ k|) → (∀ s ∈ S, (E s).Nonempty → ∀ (n : Fin d → ℤ), (∀ (k : Fin d), |↑(n k)| ≤ Q) → |∑ k : Fin d, ↑(n k) * ζ k| ∉ Set.Icc (μ * (R₀ * 2 ^ s) / 1000) (1000 * ν * (R₀ * 2 ^ s))) → 7200000 * (↑d + 1) ^ 2 * B ≤ Q → 72 * B ≤ Q → 7200000 * (↑d + 1) ^ 2 * ν ≤ Sg → 2 * ν ≤ Sg → ∀ (δ : ℝ), 0 < δ → δ ≤ 1 → ∑ s ∈ S with ↑(E s).card ≤ δ * M ^ 2, ↑(E s).card ≤ 3 * 10 ^ 11 * (1 + Real.logb 2 (2 + (↑d + 1) ^ 2 * ν / μ)) * L ^ 12 * δ ^ (1 / 300) * M ^ 2

three_core_sparse_count with the explicit constants C = 3 · 10^{11}, C_res = 7200000 of sparse_count_explicit (blueprint eq:applied-sparse, lines 2731-2741).

theorem TrilinearHT.Auto.fourRef_mult {d : ℕ} (ζ : Fin d → ℝ) (S : Finset ℤ) (E : ℤ → Finset (Fin 4 → ℝ)) {B μ ν R₀ : ℝ} (hB : 1 ≤ B) (hμ : 0 < μ) (hμν : μ ≤ ν) (hR₀ : 0 < R₀) (href : ∀ s ∈ S, ∀ x ∈ E s, FourRef ζ B μ ν (R₀ * 2 ^ s) x) (x : Fin 4 → ℝ) : ↑{s ∈ S | x ∈ E s}.card ≤ fourMult d B μ ν

Blueprint lines 2722-2724: a four-core label tuple with the reference data FourRef at the scales R₀ 2^s occurs at at most L₀ = fourMult scales (tested_scale_mult).

theorem TrilinearHT.Auto.threeRef_mult {d : ℕ} (ζ : Fin d → ℝ) (l : Fin 4) (S : Finset ℤ) (E : ℤ → Finset (Fin 4 → ℝ)) {B μ ν R₀ : ℝ} (hB : 1 ≤ B) (hμ : 0 < μ) (hμν : μ ≤ ν) (hR₀ : 0 < R₀) (href : ∀ s ∈ S, ∀ x ∈ E s, ThreeRef ζ l B μ ν (R₀ * 2 ^ s) x) (x : Fin 4 → ℝ) : ↑{s ∈ S | x ∈ E s}.card ≤ threeMult d B μ ν

Blueprint lines 2722-2724: a three-core label tuple with the reference data ThreeRef at the scales R₀ 2^s occurs at at most L₀ = threeMult scales (tested_scale_mult).

theorem TrilinearHT.Auto.ModeSchedule.Valid.sparse_reserve {S : ModeSchedule} {Cj CA CT CK : ℕ} {δs W : ℝ} (hV : S.Valid Cj CA CT CK δs W) (hCA : 1 ≤ CA) (hd2 : 2 ≤ S.dmax) (hD : 2 ≤ S.Dstar) (hB : 2 ≤ S.Bstar) {h : ℕ} (hh : 10 ≤ h) : 7200000 * (↑S.dmax + 1) ^ 2 * 4 * 6 ^ 8 * S.Dstar ^ 5 * S.Eh (h - 10) ≤ S.Eh h

The shift reserve of eq:applied-sparse (blueprint lines 2733-2736, "the choice of A₀ and B'_h = D_*^5 E_{h-Δ} gives Q ≥ C_res (d+1)² C B'_h"): with C_res = 7200000 and the factor 4 of the four-core annuli, 7200000 (d_max+1)² · 4 · 6^8 D_*^5 E_{h-Δ} ≤ E_h for h ≥ Δ = 10 (A₀ ≥ 6^{30} C_* D_* and d_max ≤ C_*).

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.U0_sparse_reserve {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (hD : 2 ≤ D.S.Dstar) (hdD : ↑D.S.dmax ≤ D.S.Dstar) : 7200000 * (↑D.S.dmax + 1) ^ 2 * (8 * D.U0) ≤ D.S.Ξ / 2

The band reserve of eq:applied-sparse (blueprint line 2736, "Ξ = D_*^{1000} and ν ≤ C D_*^{250} give the required Σ reserve"): 7200000 (d_max+1)² · 8 U₀ ≤ Ξ/2 when the budget D_* ≥ 2 also covers the dimension, d_max ≤ D_*.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.side_pure_gap {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) {Cj CA CT CK : ℕ} {δs W : ℝ} (hV : D.S.Valid Cj CA CT CK δs W) (hCA : 1 ≤ CA) (hCT : 4 ≤ CT) (hd2 : 2 ≤ D.S.dmax) (hD : 2 ≤ D.S.Dstar) (hB : 2 ≤ D.S.Bstar) (hQ : 1 ≤ D.S.Q0) (hSP : D.SP = D.S.sideParams δs) (I : ℤ × ℤ) (G : bf.Grp) (j : Fin 4) (z : ChartTag) (hz : (D.Ms j G).zc = z) (hdim : z.dim ≤ D.S.dmax) {h : ℕ} (hh : 10 ≤ h) (hhJ : h ≤ D.SP.Jst) {m : ↥((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K)))} (hgood : ((D.Ms j G).blockComps D.S ⋯ (A.blkStart D.S.K I.1) (D.preAt I)).Good D.SP.Δ ((D.Ms j G).goodP D.S D.SP (A.blkStart D.S.K I.1)) h m) {μ ν : ℝ} (hμ : D.U0⁻¹ / 2 < μ) (hν : ν ≤ 8 * D.U0) (n : Fin z.dim → ℤ) (hn : ∀ (k : Fin z.dim), |↑(n k)| ≤ D.S.Eh h / ↑(6 ^ 8)) : |∑ k : Fin z.dim, ↑(n k) * zetaVec z D.S.Q0 h k| ∉ Set.Icc (μ * (dyadicGridLength A.G I.1)⁻¹ / 1000) (1000 * ν * (dyadicGridLength A.G I.1)⁻¹)

Blueprint lines 2736-2738 (the pure-shift gap on the side states): a mode good at the height h on the cell I lies in a successful component, which contains a nonexceptional primary; its gap eq:gap (thresholds T⁻¹/r_{v_b}, T/r_{t_b}), applied to the pure shifts n·ζ (ζ = 6^{Δ-2} ϑ/L_h, integer |n|_∞ ≤ E_h/6^8 < H), excludes the whole annulus [μ R/1000, 1000 ν R] (R = |I|⁻¹) for U₀⁻¹/2 < μ and ν ≤ 8 U₀.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.sparse_rhs_nonneg {d : ℕ} {μ ν L δ M : ℝ} (hμ : 0 < μ) (hν : 0 ≤ ν) (hδ : 0 ≤ δ) : 0 ≤ 3 * 10 ^ 11 * (1 + Real.logb 2 (2 + (↑d + 1) ^ 2 * ν / μ)) * L ^ 12 * δ ^ (1 / 300) * M ^ 2

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.four_core_applied_side {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) {Cj CA CT CK : ℕ} {δs W : ℝ} (hV : D.S.Valid Cj CA CT CK δs W) (hCA : 1 ≤ CA) (hCT : 4 ≤ CT) (hd2 : 2 ≤ D.S.dmax) (hD : 2 ≤ D.S.Dstar) (hB : 2 ≤ D.S.Bstar) (hQ0 : 1 ≤ D.S.Q0) (hSP : D.SP = D.S.sideParams δs) (hdD : ↑D.S.dmax ≤ D.S.Dstar) (G : bf.Grp) (h : ℕ) (hh : 10 ≤ h) (hhJ : h ≤ D.SP.Jst) (Cs : Finset (ℤ × ℤ)) (rep : (j : Fin 4) → ℕ → ℕ → ℤ × (ℤ × ℤ) × (D.Ms j G).Md → (D.Ms j G).Md) (hrep : ∀ (j : Fin 4), D.RepOK G j h Cs (rep j)) (hΛ : ∀ (j : Fin 4), 8 * (D.Ms j G).Λ ≤ D.S.Ξ) (z : ChartTag) (hz : ∀ (j : Fin 4), (D.Ms j G).zc = z) (hdim : z.dim ≤ D.S.dmax) {S : Finset ℤ} {cellOf : ℤ → ℤ × ℤ} {xs : ℝ} (hpath : ∀ s ∈ S, cellOf s ∈ Cs ∧ xs ∈ dyadicGridCell A.G (cellOf s).1 (cellOf s).2) (hcell : ∀ (s : ℤ), (cellOf s).1 = s) {ancOf : (s : ℤ) → D.AncNe G (cellOf s) → ℕ → (j : Fin 4) → Finset (D.Ms j G).Md → ↥((D.Ms j G).alive (ancAt A.G (D.preAt (cellOf s)) (A.blkStart D.S.K (cellOf s).1 - 4 * ↑D.S.K)))} (hanc : D.FourPathAnc G h Cs rep hrep cellOf ancOf S) (c : ℝ × ℝ × (Fin 4 → ℝ)) (hc : 0 < c.1 ∧ 0 ≤ c.2.1) (κ : Fin 4 → ℕ × ℕ) {M : ℝ} (hM : ∀ (i : Fin 4), ↑(S.biUnion fun (s : ℤ) => Finset.image (fun (x : Fin 4 → ℝ) => x i) (D.fourPathE G h xs cellOf ancOf c κ s)).card ≤ M) {δ : ℝ} (hδ0 : 0 < δ) (hδ1 : δ ≤ 1) : ∑ s ∈ S with ↑(D.fourPathE G h xs cellOf ancOf c κ s).card ≤ δ * M ^ 2, ↑(D.fourPathE G h xs cellOf ancOf c κ s).card ≤ 3 * 10 ^ 11 * (1 + Real.logb 2 (2 + (↑z.dim + 1) ^ 2 * (4 * (2 * c.2.1)) / c.1)) * fourMult z.dim (D.S.Dstar ^ 5 * D.S.Eh (h - D.SP.Δ)) c.1 (2 * c.2.1) ^ 12 * δ ^ (1 / 300) * M ^ 2

Blueprint eq:applied-sparse for four cores on the side states (lines 2731-2742): along a path with the representatives as anchors, at a fixed height h ≤ J_*, types and bin c = (μ, ν, σ), lem:sparse-count applies with ζ = 6^{Δ-2} ϑ/L_h, Q = E_h/6^8, Σ = Ξ/2, B = B'_{h-Δ}, the bands μ, 4 · 2ν (absorbing the constants of eq:triple-test), L = L₀ and any M ≥ M_i^G = |A_i|: pair determination and multiplicity (eq:total-count), separation, the reserves (Valid.shift_reserve, Valid.sparse_reserve, U0_sparse_reserve with d_max ≤ D_*) and the pure-shift gap of the nonexceptional primary (side_pure_gap) hold, so Σ_{N_s ≤ δ M²} N_s ≤ C ℓ L₀^{12} δ^{1/300} M² with ℓ = 1 + log₂(2 + (d+1)² 8ν/μ).

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.three_core_applied_side {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) {Cj CA CT CK : ℕ} {δs W : ℝ} (hV : D.S.Valid Cj CA CT CK δs W) (hCA : 1 ≤ CA) (hCT : 4 ≤ CT) (hd2 : 2 ≤ D.S.dmax) (hD : 2 ≤ D.S.Dstar) (hB : 2 ≤ D.S.Bstar) (hQ0 : 1 ≤ D.S.Q0) (hSP : D.SP = D.S.sideParams δs) (hdD : ↑D.S.dmax ≤ D.S.Dstar) (G : bf.Grp) (h : ℕ) (hh : 10 ≤ h) (hhJ : h ≤ D.SP.Jst) (l : Fin 4) (Cs : Finset (ℤ × ℤ)) (rep : (j : Fin 4) → ℕ → ℕ → ℤ × (ℤ × ℤ) × (D.Ms j G).Md → (D.Ms j G).Md) (hrep : ∀ (j : Fin 4), D.RepOK G j h Cs (rep j)) (hΛ : ∀ (j : Fin 4), 8 * (D.Ms j G).Λ ≤ D.S.Ξ) (z : ChartTag) (hz : ∀ (j : Fin 4), (D.Ms j G).zc = z) (hdim : z.dim ≤ D.S.dmax) {S : Finset ℤ} {cellOf : ℤ → ℤ × ℤ} {xs : ℝ} (hpath : ∀ s ∈ S, cellOf s ∈ Cs ∧ xs ∈ dyadicGridCell A.G (cellOf s).1 (cellOf s).2) (hcell : ∀ (s : ℤ), (cellOf s).1 = s) {ancOf : (s : ℤ) → D.AncNe3 G (cellOf s) l → ℕ → (j : Fin 4) → j ≠ l → Finset (D.Ms j G).Md → ↥((D.Ms j G).alive (ancAt A.G (D.preAt (cellOf s)) (A.blkStart D.S.K (cellOf s).1 - 4 * ↑D.S.K)))} (hanc : D.ThreePathAnc G h l Cs rep hrep cellOf ancOf S) {Iw : ℕ} (hIw : 2 ^ Iw ≤ 2 * D.U0) (c : ℝ × ℝ × ℕ × ℝ × (Fin 4 → ℝ)) (hc : 0 < c.1 ∧ 0 ≤ c.2.1) (κ : Fin 4 → ℕ × ℕ) {M : ℝ} (hM : ∀ (i : Fin 4), i ≠ l → ↑(S.biUnion fun (s : ℤ) => Finset.image (fun (x : Fin 4 → ℝ) => x i) (D.threePathE G h xs l cellOf ancOf Iw c κ s)).card ≤ M) (hMl : ∑ s ∈ S, D.sideWeight G l cellOf c.2.2.2.1 s ≤ M) {δ : ℝ} (hδ0 : 0 < δ) (hδ1 : δ ≤ 1) : ∑ s ∈ S with ↑(D.threePathE G h xs l cellOf ancOf Iw c κ s).card ≤ δ * M ^ 2, ↑(D.threePathE G h xs l cellOf ancOf Iw c κ s).card ≤ 3 * 10 ^ 11 * (1 + Real.logb 2 (2 + (↑z.dim + 1) ^ 2 * (2 * c.2.1) / c.1)) * threeMult z.dim (D.S.Dstar ^ 5 * D.S.Eh (h - D.SP.Δ)) c.1 (2 * c.2.1) ^ 12 * δ ^ (1 / 300) * M ^ 2

Blueprint eq:applied-sparse for three cores on the side states (side role l, lines 2731-2742): as four_core_applied_side, with the T_l reference, the bands μ, 2ν, L = L₀ = threeMult, any M with M ≥ |A_i| for the core roles and M ≥ M_l^G = Σ_s w_s (side incidence, three_side_incidence; shells 2^{I_w} ≤ 2 U₀), giving Σ_{N_s ≤ δ M²} N_s ≤ C ℓ L₀^{12} δ^{1/300} M² with ℓ = 1 + log₂(2 + (d+1)² 2ν/μ).