Section 14.1: Transfer and its paired defects

This file was automatically generated by Claude.

Formalization of blueprint Section 14, "The two-side estimate" (sec:sides), subsection 1, "Transfer and its paired defects" (lines 2236-2273) of blueprint/formalization_blueprint.tex.

Transfer and its paired defects (blueprint lines 2239-2265)

theorem TrilinearHT.Auto.sum_filters_eq_bands {M : Type u_1} [AddCommGroup M] (v : ℕ → M) (hv : v 0 = 0) (P : ℕ) : ∑ p ∈ Finset.range P, v (p + 1) = ∑ i ∈ Finset.range (P + 1), (P - i) • (v (i + 1) - v i)

Abel summation for averaged filters: for Q_0 = 0, Σ_{p=1}^P Q_p = Σ_{i=1}^{P+1} (P + 1 - i) (Q_i - Q_{i-1}).

theorem TrilinearHT.Auto.transfer_identity {E : Type u_1} [AddCommGroup E] [Module ℂ E] (B : E →ₗ[ℂ] E →ₗ[ℂ] ℂ) (Qa Qc : ℕ → E →ₗ[ℂ] E) {P : ℕ} (hP : 0 < P) (ha0 : Qa 0 = 0) (hc0 : Qc 0 = 0) (haP : Qa (P + 1) = LinearMap.id) (hcP : Qc (P + 1) = LinearMap.id) (xa xc : E) : (B xa) ((↑P)⁻¹ • ∑ p ∈ Finset.range P, (Qc (p + 1)) xc) - (B ((↑P)⁻¹ • ∑ p ∈ Finset.range P, (Qa (p + 1)) xa)) xc = ∑ p ∈ Finset.range (P + 1), ∑ q ∈ Finset.range (P + 1), (↑p - ↑q) / ↑P * (B ((Qa (p + 1)) xa - (Qa p) xa)) ((Qc (q + 1)) xc - (Qc q) xc)

Blueprint eq:transfer (line 2252): for filters Q_{l,p} with Q_{l,0} = 0, Q_{l,P+1} = 1, bands A_p^l = Q_{l,p} - Q_{l,p-1} and averages QBar_l = P⁻¹ Σ_{p=1}^P Q_{l,p}, and any form H bilinear in the two transferred slots (the other slots fixed), H(x_a, QBar_c x_c) - H(QBar_a x_a, x_c) = Σ_{p,q=1}^{P+1} ((p - q)/P) H(A_p^a x_a, A_q^c x_c).

The parameters, masks, filters and tests of an attempt

def TrilinearHT.Auto.posExpand : List (ℕ × Bool) → List (ℤ × List ℕ)

The signed positive chains of a layer list given outermost first: each complement layer 1 - C contributes either nothing or -C.

Equations

• TrilinearHT.Auto.posExpand [] = [(1, [])]
• TrilinearHT.Auto.posExpand ((m, false) :: rest) = List.map (fun (t : ℤ × List ℕ) => (t.1, m :: t.2)) (TrilinearHT.Auto.posExpand rest)
• TrilinearHT.Auto.posExpand ((m, true) :: rest) = TrilinearHT.Auto.posExpand rest ++ List.map (fun (t : ℤ × List ℕ) => (-t.1, m :: t.2)) (TrilinearHT.Auto.posExpand rest)

theorem TrilinearHT.Auto.posExpand_length_le (ls : List (ℕ × Bool)) : (posExpand ls).length ≤ 2 ^ ls.length

The number of signed positive chains is at most 2^n.

Structural facts for the leaves of an attempt

The basic upper guard: expansion in vertex charts

def TrilinearHT.Auto.bilinTwo {E : Type u_1} [AddCommGroup E] [Module ℂ E] (Λ : MultilinearMap ℂ (fun (x : Fin 4) => E) ℂ) {a c : Fin 4} (hac : a ≠ c) (x : Fin 4 → E) : E →ₗ[ℂ] E →ₗ[ℂ] ℂ

A four-linear form as a bilinear form in two distinct slots, the other slots fixed.

Equations

• TrilinearHT.Auto.bilinTwo Λ hac x = LinearMap.mk₂ ℂ (fun (u v : E) => Λ (Function.update (Function.update x a u) c v)) ⋯ ⋯ ⋯ ⋯

theorem TrilinearHT.Auto.bilinTwo_apply {E : Type u_1} [AddCommGroup E] [Module ℂ E] (Λ : MultilinearMap ℂ (fun (x : Fin 4) => E) ℂ) {a c : Fin 4} (hac : a ≠ c) (x : Fin 4 → E) (u v : E) : ((bilinTwo Λ hac x) u) v = Λ (Function.update (Function.update x a u) c v)

theorem TrilinearHT.Auto.transfer_step {E : Type u_1} [AddCommGroup E] [Module ℂ E] (Λ : MultilinearMap ℂ (fun (x : Fin 4) => E) ℂ) {a c : Fin 4} (hac : a ≠ c) (x : Fin 4 → E) (Qa Qc : ℕ → E →ₗ[ℂ] E) {P : ℕ} (hP : 0 < P) (ha0 : Qa 0 = 0) (hc0 : Qc 0 = 0) (haP : Qa (P + 1) = LinearMap.id) (hcP : Qc (P + 1) = LinearMap.id) : Λ (Function.update x c ((↑P)⁻¹ • ∑ p ∈ Finset.range P, (Qc (p + 1)) (x c))) - Λ (Function.update x a ((↑P)⁻¹ • ∑ p ∈ Finset.range P, (Qa (p + 1)) (x a))) = ∑ p ∈ Finset.range (P + 1), ∑ q ∈ Finset.range (P + 1), (↑p - ↑q) / ↑P * Λ (Function.update (Function.update x a ((Qa (p + 1)) (x a) - (Qa p) (x a))) c ((Qc (q + 1)) (x c) - (Qc q) (x c)))

Blueprint eq:transfer (line 2252) for a four-linear form: transferring the averaged filter of the complement slot c to the helper average on the side slot a changes the form by the band sum Σ_{p,q} ((p - q)/P) H(A_p^a x_a, A_q^c x_c).

noncomputable def TrilinearHT.Auto.filterAvg {E : Type u_1} [AddCommGroup E] [Module ℂ E] (P : ℕ) (Q : ℕ → E →ₗ[ℂ] E) : E →ₗ[ℂ] E

The average P⁻¹ Σ_{p=1}^P Q_p of a filter family.

Equations

• TrilinearHT.Auto.filterAvg P Q = (↑P)⁻¹ • ∑ p ∈ Finset.range P, Q (p + 1)

theorem TrilinearHT.Auto.filterAvg_apply {E : Type u_1} [AddCommGroup E] [Module ℂ E] (P : ℕ) (Q : ℕ → E →ₗ[ℂ] E) (x : E) : (filterAvg P Q) x = (↑P)⁻¹ • ∑ p ∈ Finset.range P, (Q (p + 1)) x

@[reducible, inline]

abbrev TrilinearHT.Auto.TransferStep (E : Type u_2) [AddCommGroup E] [Module ℂ E] : Type u_2

One transfer step: the slot it acts on (true for c, false for d), the helper filters on the side slot and the filters of the complement slot.

Equations

• TrilinearHT.Auto.TransferStep E = (Bool × (ℕ → E →ₗ[ℂ] E) × (ℕ → E →ₗ[ℂ] E))

noncomputable def TrilinearHT.Auto.chainVal {E : Type u_1} [AddCommGroup E] [Module ℂ E] (P : ℕ) (v : Bool) : List (TransferStep E) → E → E

The complement value of slot c (v = true) or d (v = false): the averaged filters of its steps, outermost first, applied to the base.

Equations

• TrilinearHT.Auto.chainVal P v [] x✝ = x✝
• TrilinearHT.Auto.chainVal P v (st :: rest) x✝ = if st.1 = v then (TrilinearHT.Auto.filterAvg P st.2.2) (TrilinearHT.Auto.chainVal P v rest x✝) else TrilinearHT.Auto.chainVal P v rest x✝

noncomputable def TrilinearHT.Auto.chainSide {E : Type u_1} [AddCommGroup E] [Module ℂ E] (P : ℕ) : List (TransferStep E) → E → E

The side value after all transfers: the helper averages applied in step order.

Equations

• TrilinearHT.Auto.chainSide P [] x✝ = x✝
• TrilinearHT.Auto.chainSide P (st :: rest) x✝ = TrilinearHT.Auto.chainSide P rest ((TrilinearHT.Auto.filterAvg P st.2.1) x✝)

noncomputable def TrilinearHT.Auto.chainDefect {E : Type u_1} [AddCommGroup E] [Module ℂ E] (Λ : MultilinearMap ℂ (fun (x : Fin 4) => E) ℂ) (P : ℕ) (a c d : Fin 4) (x : Fin 4 → E) (yc yd : E) : List (TransferStep E) → E → ℂ

The band defects of all transfer steps.

Equations

• One or more equations did not get rendered due to their size.
• TrilinearHT.Auto.chainDefect Λ P a c d x yc yd [] x✝ = 0

theorem TrilinearHT.Auto.transfer_chain {E : Type u_1} [AddCommGroup E] [Module ℂ E] (Λ : MultilinearMap ℂ (fun (x : Fin 4) => E) ℂ) {P : ℕ} (hP : 0 < P) {a c d : Fin 4} (hac : a ≠ c) (had : a ≠ d) (hcd : c ≠ d) (x : Fin 4 → E) (yc yd : E) (steps : List (TransferStep E)) : (∀ st ∈ steps, st.2.1 0 = 0 ∧ st.2.2 0 = 0 ∧ st.2.1 (P + 1) = LinearMap.id ∧ st.2.2 (P + 1) = LinearMap.id) → ∀ (xa : E), Λ (Function.update (Function.update (Function.update x c (chainVal P true steps yc)) d (chainVal P false steps yd)) a xa) = Λ (Function.update (Function.update (Function.update x c yc) d yd) a (chainSide P steps xa)) + chainDefect Λ P a c d x yc yd steps xa

Blueprint lines 2241-2268 ("after all transfers the main term is H(D_{a,s} S_a, S_b, B_c, B_d)"): transferring the averaged filters of the two complement slots one at a time, each to a helper average on the side slot, the form of the side and the two complement chains is the form of the transferred side and the two bases plus the band defects of the steps.

theorem TrilinearHT.Auto.comp_list_sum {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) (L : List (E →L[ℂ] E)) : A ∘SL L.sum = (List.map (fun (T : E →L[ℂ] E) => A ∘SL T) L).sum

theorem TrilinearHT.Auto.neg_list_sum {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (L : List (E →L[ℂ] E)) : -L.sum = (List.map (fun (T : E →L[ℂ] E) => -T) L).sum

theorem TrilinearHT.Auto.layerOp_eq_posExpand {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (Cum : ℕ → E →L[ℂ] E) (ls : List (ℕ × Bool)) : layerOp Cum ls = (List.map (fun (t : ℤ × List ℕ) => ↑t.1 • chainOp Cum t.2) (posExpand ls.reverse)).sum

Blueprint line 2241 ("expand complements in the latter two histories as identity minus a positive average; there are only 2^{O(log L)} products"): a layered history is the signed sum of its positive chains.

theorem TrilinearHT.Auto.multilinear_update_list_sum {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (Λ : MultilinearMap ℂ (fun (x : Fin 4) => E) ℂ) (x : Fin 4 → E) (c : Fin 4) (L : List E) : Λ (Function.update x c L.sum) = (List.map (fun (v : E) => Λ (Function.update x c v)) L).sum

A multilinear form is additive over a list sum in one slot.

theorem TrilinearHT.Auto.list_sum_smul_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {ι : Type u_2} (L : List ι) (w : ι → ℂ) (T : ι → E →L[ℂ] E) (y : E) : (List.map (fun (t : ι) => w t • T t) L).sum y = (List.map (fun (t : ι) => w t • (T t) y) L).sum

The value of a list sum of scaled operators.

theorem TrilinearHT.Auto.apply_layerOp_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (B : E →L[ℂ] E) (C : ℕ → E →L[ℂ] E) (ls : List (ℕ × Bool)) (y : E) : B ((layerOp C ls) y) = (List.map (fun (t : ℤ × List ℕ) => ↑t.1 • B ((chainOp C t.2) y)) (posExpand ls.reverse)).sum

A layered output is the signed sum of its positive-chain outputs.

theorem TrilinearHT.Auto.multilinear_update_two_sums {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (Λ : MultilinearMap ℂ (fun (x : Fin 4) => E) ℂ) {c d : Fin 4} (hcd : c ≠ d) (x : Fin 4 → E) {α : Type u_2} {β : Type u_3} (Lc : List α) (Ld : List β) (f : α → E) (g : β → E) : Λ (Function.update (Function.update x c (List.map f Lc).sum) d (List.map g Ld).sum) = (List.map (fun (t' : β) => (List.map (fun (t : α) => Λ (Function.update (Function.update x c (f t)) d (g t'))) Lc).sum) Ld).sum

A multilinear form is biadditive over list sums in two distinct slots.

theorem TrilinearHT.Auto.form_layer_chains {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (Λ : MultilinearMap ℂ (fun (x : Fin 4) => E) ℂ) {c d : Fin 4} (hcd : c ≠ d) (x : Fin 4 → E) (Bc Bd : E →L[ℂ] E) (Cc Cd : ℕ → E →L[ℂ] E) (lc ld : List (ℕ × Bool)) (yc yd : E) : Λ (Function.update (Function.update x c (Bc ((layerOp Cc lc) yc))) d (Bd ((layerOp Cd ld) yd))) = (List.map (fun (t' : ℤ × List ℕ) => (List.map (fun (t : ℤ × List ℕ) => ↑t.1 * ↑t'.1 * Λ (Function.update (Function.update x c (Bc ((chainOp Cc t.2) yc))) d (Bd ((chainOp Cd t'.2) yd)))) (posExpand lc.reverse)).sum) (posExpand ld.reverse)).sum

Blueprint line 2241 ("expand complements in the latter two histories as identity minus a positive average; there are only 2^{O(log L)} products"): the form with whole layered outputs B_c(ℬ_c y_c), B_d(ℬ_d y_d) in two slots is the signed sum, over the pairs of positive chains of the two histories, of the forms with the chain outputs.

theorem TrilinearHT.Auto.searchLeaves_layers_distinct (fuel ℓ h : ℕ) (up : Fin 4) (low : Option (Fin 4)) (ls : Fin 4 → List (ℕ × Bool)) : (∀ (l : Fin 4), ∀ x ∈ ls l, x.1 ∉ Finset.Ico ℓ h) → (∀ (l l' : Fin 4), l ≠ l' → ∀ x ∈ ls l, ∀ y ∈ ls l', x.1 ≠ y.1) → ∀ L ∈ searchLeaves fuel ℓ h up low ls, ∀ (l l' : Fin 4), l ≠ l' → ∀ x ∈ L.layers l, ∀ y ∈ L.layers l', x.1 ≠ y.1

Blueprint line 2241 ("the ranks are distinct: a cumulative rank was inserted in just one slot at its binary split"): along the guarded search, if the layers so far avoid the open color range [ℓ, h) and have distinct indices in distinct slots, every leaf has distinct layer indices in distinct slots.

theorem TrilinearHT.Auto.leafAt_layers_distinct (fuel Lc : ℕ) (up₀ : Fin 4) (s : ℕ) (l l' : Fin 4) : l ≠ l' → ∀ x ∈ (leafAt fuel Lc up₀ s).layers l, ∀ y ∈ (leafAt fuel Lc up₀ s).layers l', x.1 ≠ y.1

The leaves of the attempt search have distinct cumulative indices in distinct slots.

noncomputable def TrilinearHT.Auto.padFam {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {P : ℕ} (Q : Fin P → E →L[ℂ] E) (p : ℕ) : E →ₗ[ℂ] E

Blueprint lines 2243-2247: the pad family Q_0 = 0, Q_p the pad-p projection for 1 ≤ p ≤ P, and Q_p = 1 beyond (Q_{P+1} = 1).

Equations

• TrilinearHT.Auto.padFam Q p = if p = 0 then 0 else if h : p - 1 < P then ↑(Q ⟨p - 1, h⟩) else LinearMap.id

theorem TrilinearHT.Auto.padFam_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {P : ℕ} (Q : Fin P → E →L[ℂ] E) : padFam Q 0 = 0

theorem TrilinearHT.Auto.padFam_top {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {P : ℕ} (Q : Fin P → E →L[ℂ] E) : padFam Q (P + 1) = LinearMap.id

theorem TrilinearHT.Auto.padFam_succ {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {P : ℕ} (Q : Fin P → E →L[ℂ] E) {p : ℕ} (hp : p < P) : padFam Q (p + 1) = ↑(Q ⟨p, hp⟩)

theorem TrilinearHT.Auto.filterAvg_padFam {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {P : ℕ} (Q : Fin P → E →L[ℂ] E) (x : E) : (filterAvg P (padFam Q)) x = (opAvg Q) x

The average of the pad family is the operator average of the pad projections: QBar = P⁻¹ Σ_{p=1}^P Q_p.

theorem TrilinearHT.Auto.pad_transfer_chain {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (Λ : MultilinearMap ℂ (fun (x : Fin 4) => E) ℂ) {P : ℕ} (hP : 0 < P) {a c d : Fin 4} (hac : a ≠ c) (had : a ≠ d) (hcd : c ≠ d) (x : Fin 4 → E) (yc yd : E) (steps : List (Bool × (Fin P → E →L[ℂ] E) × (Fin P → E →L[ℂ] E))) (xa : E) : Λ (Function.update (Function.update (Function.update x c (chainVal P true (List.map (fun (st : Bool × (Fin P → E →L[ℂ] E) × (Fin P → E →L[ℂ] E)) => (st.1, padFam st.2.1, padFam st.2.2)) steps) yc)) d (chainVal P false (List.map (fun (st : Bool × (Fin P → E →L[ℂ] E) × (Fin P → E →L[ℂ] E)) => (st.1, padFam st.2.1, padFam st.2.2)) steps) yd)) a xa) = Λ (Function.update (Function.update (Function.update x c yc) d yd) a (chainSide P (List.map (fun (st : Bool × (Fin P → E →L[ℂ] E) × (Fin P → E →L[ℂ] E)) => (st.1, padFam st.2.1, padFam st.2.2)) steps) xa)) + chainDefect Λ P a c d x yc yd (List.map (fun (st : Bool × (Fin P → E →L[ℂ] E) × (Fin P → E →L[ℂ] E)) => (st.1, padFam st.2.1, padFam st.2.2)) steps) xa

Blueprint lines 2243-2252 with transfer_chain on a four-linear form: for a list of transfer steps given by pad projections of complement filters (slot c or d) and helper projections on the identical masks (side slot a), the form of the side and the two averaged complement chains equals the form of the transferred side and the two bases plus the band defects.

theorem TrilinearHT.Auto.restore_two {E : Type u_1} [AddCommGroup E] [Module ℂ E] (Λ : MultilinearMap ℂ (fun (x : Fin 4) => E) ℂ) {c d : Fin 4} (hcd : c ≠ d) (x : Fin 4 → E) (Bc Bd Uc Ud : E) : Λ (Function.update (Function.update x c Bc) d Bd) = Λ (Function.update (Function.update x c (Bc + Uc)) d (Bd + Ud)) - (Λ (Function.update (Function.update x c Uc) d Bd) + Λ (Function.update (Function.update x c Bc) d Ud) + Λ (Function.update (Function.update x c Uc) d Ud))

Blueprint lines 2261-2262 ("restoring B_c, B_d to Y_c, Y_d gives the pair-small main term; each correction has an additional basic side U"): with Y = B + U in two slots, the transferred main term is the form of the full pair minus the three corrections containing a basic side.

Rank-ordered transfer steps (blueprint lines 2240-2252)

@[irreducible]

def TrilinearHT.Auto.rankMerge {α : Type u_1} (key : α → ℕ) : List α → List α → List (Bool × α)

Blueprint line 2241 ("in each product remove the larger rank among the two current outermost positive filters"): the merge of the filter lists of the two complement slots (outermost first), taking at each step the outermost filter of larger rank (true for slot c, false for d).

Equations

• One or more equations did not get rendered due to their size.
• TrilinearHT.Auto.rankMerge key [] x✝ = List.map (fun (y : α) => (false, y)) x✝
• TrilinearHT.Auto.rankMerge key (x_2 :: xs) [] = List.map (fun (x : α) => (true, x)) (x_2 :: xs)

theorem TrilinearHT.Auto.rankMerge_filter_true {α : Type u_1} (key : α → ℕ) (xs ys : List α) : List.map Prod.snd (List.filter (fun (e : Bool × α) => e.1) (rankMerge key xs ys)) = xs

The true entries of a merge are the first list.

theorem TrilinearHT.Auto.rankMerge_filter_false {α : Type u_1} (key : α → ℕ) (xs ys : List α) : List.map Prod.snd (List.filter (fun (e : Bool × α) => !e.1) (rankMerge key xs ys)) = ys

The false entries of a merge are the second list.

def TrilinearHT.Auto.applyAll {E : Type u_1} [AddCommGroup E] [Module ℂ E] : List (E →ₗ[ℂ] E) → E → E

The composition of a list of operators, outermost first.

Equations

• TrilinearHT.Auto.applyAll [] x✝ = x✝
• TrilinearHT.Auto.applyAll (T :: Ts) x✝ = T (TrilinearHT.Auto.applyAll Ts x✝)

theorem TrilinearHT.Auto.chainVal_eq_applyAll {E : Type u_1} [AddCommGroup E] [Module ℂ E] (P : ℕ) (v : Bool) (steps : List (TransferStep E)) (y : E) : chainVal P v steps y = applyAll (List.map (fun (st : TransferStep E) => filterAvg P st.2.2) (List.filter (fun (st : TransferStep E) => decide (st.1 = v)) steps)) y

The complement value of a slot depends only on the steps of that slot.

theorem TrilinearHT.Auto.rankMerge_filter_c {α : Type u_1} (key : α → ℕ) (xs ys : List α) : List.filter (fun (e : Bool × α) => decide (e.1 = true)) (rankMerge key xs ys) = List.map (fun (x : α) => (true, x)) xs

The c entries of a merge, as steps.

theorem TrilinearHT.Auto.rankMerge_filter_d {α : Type u_1} (key : α → ℕ) (xs ys : List α) : List.filter (fun (e : Bool × α) => decide (e.1 = false)) (rankMerge key xs ys) = List.map (fun (y : α) => (false, y)) ys

The d entries of a merge, as steps.

Sources of the other complement (blueprint lines 2254-2255)

Near and far tags of the far-band sources (blueprint lines 1805, 2254-2256)

Steps of a rank merge (blueprint line 2241)

theorem TrilinearHT.Auto.rankMerge_decomp {α : Type u_1} (key : α → ℕ) (xs ys : List α) (pre : List (Bool × α)) (e : Bool × α) (rest : List (Bool × α)) : rankMerge key xs ys = pre ++ e :: rest → ∃ (xs' : List α) (ys' : List α), rest = rankMerge key xs' ys' ∧ ((e.1 = true ∧ e.2 :: xs' <:+ xs ∧ ys' <:+ ys ∧ ∀ y ∈ ys'.head?, key y < key e.2) ∨ e.1 = false ∧ xs' <:+ xs ∧ e.2 :: ys' <:+ ys ∧ ∀ x ∈ xs'.head?, key x ≤ key e.2)

Blueprint line 2241 ("remove the larger rank among the two current outermost positive filters ... the other complementary argument always has a strictly lower-rank outer primal source"): every step of a rank merge takes the head of a suffix of one list, the remaining steps are the merge of the remaining suffixes, and the head of the other remaining suffix has smaller (for a c step: strictly smaller) rank.

Values along the transfer steps (blueprint lines 2241-2252)

The helper test family of an attempt (blueprint lines 1812-1817, 2236-2238)

noncomputable def TrilinearHT.Auto.padStep {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {P : ℕ} (st : Bool × (Fin P → E →L[ℂ] E) × (Fin P → E →L[ℂ] E)) : TransferStep E

The pad step of a raw step.

Equations

• TrilinearHT.Auto.padStep st = (st.1, TrilinearHT.Auto.padFam st.2.1, TrilinearHT.Auto.padFam st.2.2)

The helper rank on the side states (blueprint lines 2236-2237)

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.sideState_restrict_base {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) {n : ℕ} (Ms : ModeSystem A.G n) (l : Fin 4) (s : List (CatCol bf.Vtx)) (mb : bf.MainBudget s) (G : bf.Grp) (j : ℕ) (ls : List (ℕ × Bool)) (S : ModeSchedule) (hA : 6 ≤ S.A0) (SP : SideParams) (c : ℤ × ℤ → Ms.Md → ℂ) (b h : ℤ) (nf : ℕ) (I : ℤ × ℤ) : MainFresh fp.Mc nf ((columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯) (fp.sideState Ms l s mb G j ls S hA SP c b h)) ∧ ∀ᵐ (y : ℝ), y ∉ dyadicGridCell A.G I.1 I.2 → ↑↑((columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯) (fp.sideState Ms l s mb G j ls S hA SP c b h)) y = 0

The side state restricted to an active cell is an admissible helper base: its template coordinates vanish ("their extra private directions are distinct from the fresh helper directions") and it is supported on the cell.

Passing residuals and the far-band form bounds (blueprint lines 2252-2256)

theorem TrilinearHT.Auto.ResidPass.form_le {Tg : Type u_1} {G : RealDyadicGrid} {V : Type u_2} [Fintype V] {I : ℤ × ℤ} {c₀ : ℕ} {H : ℝ} {tagOf : Tg → ChartTag} {wI : ℝ × ℝ → ℂ} {t : Fin 4} {M : Tg → Prop} {R : ↥(ColumnL2 V)} {β : ℝ} (hpass : ResidPass G I c₀ H tagOf wI t M R β) {κ : LocalKernelClass} (hwI : IsAdmissibleLocalKernel κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) wI) {x : Tg} (hx : M x) {u a b : Fin 4} (hut : u ≠ t) (hua : u ≠ a) (hub : u ≠ b) (hta : t ≠ a) (htb : t ≠ b) (hab : a ≠ b) (A : QuadraticChartData (tagOf x).dim) (hA : QuadraticChartComplexity c₀ H A) (hAθ : A.horizontal = (tagOf x).θ) (hAM : A.matrix = ↑(slotCoeff u) • (tagOf x).C) (hAq : A.quadratic = ↑(slotCoeff u) * (tagOf x).lam) (X : Fin 4 → ↥(ColumnL2 V)) (hXu : ∀ᵐ (y : ℝ), y ∈ dyadicGridCell G I.1 I.2 → augPhys (X u) y = quadraticChartAtom A y) (hXt : X t = R) {Sa Sb : ℝ} (hSa : 0 < Sa) (hSb : 0 < Sb) (hXa : MeasureTheory.eLpNorm (augPhys (X a)) 2 (normalizedIntervalMeasure (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1)) ≤ ENNReal.ofReal Sa) (hXb : MeasureTheory.eLpNorm (augPhys (X b)) 2 (normalizedIntervalMeasure (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1)) ≤ ENNReal.ofReal Sb) : ‖(cellForm ⋯ hwI V) X‖ ≤ β * Sa * Sb

A passing residual bounds the cell form with a pure source of a tag in the mask in slot u, the residual in slot t, and two spectators of normalized sizes S_a, S_b.

theorem TrilinearHT.Auto.cellForm_pairs_le {G : RealDyadicGrid} {I : ℤ × ℤ} {κ : LocalKernelClass} {wI : ℝ × ℝ → ℂ} (hwI : IsAdmissibleLocalKernel κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) wI) {V : Type} [Fintype V] {u t a b : Fin 4} (hut : u ≠ t) (hua : u ≠ a) (hub : u ≠ b) (hta : t ≠ a) (htb : t ≠ b) (hab : a ≠ b) {ι : Type u_1} {ι' : Type u_2} (F : Finset ι) (c : ι → ℂ) (src : ι → ↥(ColumnL2 V)) (Ys : ι → ℝ → ℂ) (hsrc : ∀ m ∈ F, ∀ᵐ (y : ℝ), y ∈ dyadicGridCell G I.1 I.2 → augPhys (src m) y = Ys m y) (F' : Finset ι') (c' : ι' → ℂ) (col : ι' → ↥(ColumnL2 V)) (Y : ι' → ℝ → ℂ) (hcol : ∀ m ∈ F', ∀ᵐ (y : ℝ), y ∈ dyadicGridCell G I.1 I.2 → augPhys (col m) y = Y m y) {τ₂ : ℝ} (hsep : ∀ m ∈ F, ∀ m' ∈ F', PairSmall (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) wI u t (Ys m) (Y m') τ₂) (X : Fin 4 → ↥(ColumnL2 V)) (hXu : X u = ∑ m ∈ F, c m • src m) (hXt : X t = ∑ m ∈ F', c' m • col m) {Sa Sb : ℝ} (hSa : 0 < Sa) (hSb : 0 < Sb) (hXa : MeasureTheory.eLpNorm (augPhys (X a)) 2 (normalizedIntervalMeasure (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1)) ≤ ENNReal.ofReal Sa) (hXb : MeasureTheory.eLpNorm (augPhys (X b)) 2 (normalizedIntervalMeasure (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1)) ≤ ENNReal.ofReal Sb) : ‖(cellForm ⋯ hwI V) X‖ ≤ (τ₂ * Sa * Sb * ∑ m ∈ F, ‖c m‖) * ∑ m ∈ F', ‖c' m‖

Blueprint lines 2255-2256 ("for a far source, expand the helper primal and use the different-tag pair estimate"): combinations of pure columns in two slots, every pair separated in the sense of PairSmall, with two spectators, have form at most τ₂ S_a S_b (Σ |c_m|) (Σ |c'_{m'}|).

theorem TrilinearHT.Auto.ResidPass.cellPass {Tg : Type u_1} {G : RealDyadicGrid} {V : Type} [Fintype V] {I : ℤ × ℤ} {κ : LocalKernelClass} {wI : ℝ × ℝ → ℂ} (hwI : IsAdmissibleLocalKernel κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) wI) {c₀ : ℕ} {H : ℝ} {tagOf : Tg → ChartTag} {t : Fin 4} {M : Tg → Prop} {R : ↥(ColumnL2 V)} {β : ℝ} (h : ResidPass G I c₀ H tagOf wI t M R β) : CellPass hwI c₀ H tagOf t M R β

A passing residual passes at the cell-form level.

theorem TrilinearHT.Auto.CellPass.zero {Tg : Type u_1} {G : RealDyadicGrid} {V : Type} [Fintype V] {I : ℤ × ℤ} {κ : LocalKernelClass} {wI : ℝ × ℝ → ℂ} (hwI : IsAdmissibleLocalKernel κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) wI) (c₀ : ℕ) (H : ℝ) (tagOf : Tg → ChartTag) (t : Fin 4) (M : Tg → Prop) : CellPass hwI c₀ H tagOf t M 0 0

The zero residual passes at level zero.

theorem TrilinearHT.Auto.CellPass.form_band_le {Tg : Type u_1} {G : RealDyadicGrid} {V : Type} [Fintype V] {I : ℤ × ℤ} {κ : LocalKernelClass} {wI : ℝ × ℝ → ℂ} (hwI : IsAdmissibleLocalKernel κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) wI) {c₀ : ℕ} {H : ℝ} {tagOf : Tg → ChartTag} {t : Fin 4} {M₀ M₁ : Tg → Prop} {R₀ R₁ : ↥(ColumnL2 V)} {β₀ β₁ : ℝ} (h₀ : CellPass hwI c₀ H tagOf t M₀ R₀ β₀) (h₁ : CellPass hwI c₀ H tagOf t M₁ R₁ β₁) {u a b : Fin 4} (hut : u ≠ t) (hua : u ≠ a) (hub : u ≠ b) (hta : t ≠ a) (htb : t ≠ b) (hab : a ≠ b) {κs : Type u_2} (F : Finset κs) (c : κs → ℂ) (src : κs → ↥(ColumnL2 V)) (tag : κs → Tg) (htag : ∀ m ∈ F, M₀ (tag m) ∧ M₁ (tag m)) (hsrc : ∀ m ∈ F, ∃ (A : QuadraticChartData (tagOf (tag m)).dim), QuadraticChartComplexity c₀ H A ∧ A.horizontal = (tagOf (tag m)).θ ∧ A.matrix = ↑(slotCoeff u) • (tagOf (tag m)).C ∧ A.quadratic = ↑(slotCoeff u) * (tagOf (tag m)).lam ∧ ∀ᵐ (y : ℝ), y ∈ dyadicGridCell G I.1 I.2 → augPhys (src m) y = quadraticChartAtom A y) (X : Fin 4 → ↥(ColumnL2 V)) (hXu : X u = ∑ m ∈ F, c m • src m) (hXt : X t = R₀ - R₁) {Sa Sb : ℝ} (hSa : 0 < Sa) (hSb : 0 < Sb) (hXa : MeasureTheory.eLpNorm (augPhys (X a)) 2 (normalizedIntervalMeasure (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1)) ≤ ENNReal.ofReal Sa) (hXb : MeasureTheory.eLpNorm (augPhys (X b)) 2 (normalizedIntervalMeasure (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1)) ≤ ENNReal.ofReal Sb) : ‖(cellForm ⋯ hwI V) X‖ ≤ (∑ m ∈ F, ‖c m‖) * ((β₀ + β₁) * Sa * Sb)

A combination of pure sources in slot u (each tag in both masks) against the difference of two passing residuals in slot t, with two spectators, has form at most (Σ |c_m|) (β₀ + β₁) S_a S_b (the cell-form version of ResidPass.form_band_le).

Bounded sources, contractions and monotone levels (blueprint lines 1798, 2254-2256)

theorem TrilinearHT.Auto.CellPass.mono {Tg : Type u_1} {G : RealDyadicGrid} {V : Type} [Fintype V] {I : ℤ × ℤ} {κ : LocalKernelClass} {wI : ℝ × ℝ → ℂ} {hwI : IsAdmissibleLocalKernel κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) wI} {c₀ : ℕ} {H : ℝ} {tagOf : Tg → ChartTag} {t : Fin 4} {M : Tg → Prop} {R : ↥(ColumnL2 V)} {β β' : ℝ} (h : CellPass hwI c₀ H tagOf t M R β) (hβ : β ≤ β') : CellPass hwI c₀ H tagOf t M R β'

A residual passing at level β passes at every larger level.

Far bands on the main columns (blueprint lines 2252-2258)

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.padBand_mainRange {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (l : Fin 4) (s : List (CatCol bf.Vtx)) (I : ℤ × ℤ) (r : ℕ) (M : Fin fp.P → bf.Vtx → Prop) (hMm : ∀ (i j : Fin fp.P), i ≤ j → ∀ (x : bf.Vtx), M i x → M j x) {q : ℕ} (hq : q < fp.P) (v : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) : (padFam (fun (k : Fin fp.P) => mainProj A.G fp.Mc (bf.origCols l) s I r (M k)) (q + 1)) v - (padFam (fun (k : Fin fp.P) => mainProj A.G fp.Mc (bf.origCols l) s I r (M k)) q) v ∈ mainRange A.G fp.Mc (bf.origCols l) s I r (M ⟨q, hq⟩) ∧ ‖(padFam (fun (k : Fin fp.P) => mainProj A.G fp.Mc (bf.origCols l) s I r (M k)) (q + 1)) v - (padFam (fun (k : Fin fp.P) => mainProj A.G fp.Mc (bf.origCols l) s I r (M k)) q) v‖ ≤ 2 * ‖v‖

A band of a pad family of main projections with pad-monotone masks lies in the main range of its pad mask and has norm at most twice the input.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.far_helper_main {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) {I : ℤ × ℤ} (hI : I ∈ A.cells) {a u o b : Fin 4} (hua : u ≠ a) (huo : u ≠ o) (hub : u ≠ b) (hao : a ≠ o) (hab : a ≠ b) (hob : o ≠ b) (catu : List (CatCol bf.Vtx)) (hT : ∀ e ∈ catu, ∃ R ∈ residueBox (bf.vtag e.tag).dim 9, ∃ (γ : ℝ), e = templateCol (bf.vtag e.tag) u R γ e.birth e.rank e.tag) (htag : ∀ e ∈ catu, bf.occAvail (↑e.tag.2) e.tag.1) (r : ℕ) (M : Fin fp.P → bf.Vtx → Prop) (hMm : ∀ (i j : Fin fp.P), i ≤ j → ∀ (x : bf.Vtx), M i x → M j x) (cata : List (CatCol bf.Vtx)) (rH : ℕ) (xa v : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) {β : ℝ} (hpass : ∀ (k : Fin fp.P), CellPass ⋯ A.csrc A.Hsrc bf.vtag a (M k) (xa - (mainProj A.G fp.Mc (bf.origCols a) cata I rH (M k)) xa) β) (hβ : 0 ≤ β) {p q : ℕ} (hpq : q + 2 < p) (hpP : p ≤ fp.P) (X : Fin 4 → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (hXa : X a = (padFam (fun (k : Fin fp.P) => mainProj A.G fp.Mc (bf.origCols a) cata I rH (M k)) (p + 1)) xa - (padFam (fun (k : Fin fp.P) => mainProj A.G fp.Mc (bf.origCols a) cata I rH (M k)) p) xa) (hXu : X u = (padFam (fun (k : Fin fp.P) => mainProj A.G fp.Mc (bf.origCols u) catu I r (M k)) (q + 1)) v - (padFam (fun (k : Fin fp.P) => mainProj A.G fp.Mc (bf.origCols u) catu I r (M k)) q) v) {So Sb : ℝ} (hSo : 0 < So) (hSb : 0 < Sb) (hXo : MeasureTheory.eLpNorm (augPhys (X o)) 2 (normalizedIntervalMeasure (dyadicGridLeft A.G I.1 I.2) (dyadicGridLength A.G I.1)) ≤ ENNReal.ofReal So) (hXb : MeasureTheory.eLpNorm (augPhys (X b)) 2 (normalizedIntervalMeasure (dyadicGridLeft A.G I.1 I.2) (dyadicGridLength A.G I.1)) ≤ ENNReal.ofReal Sb) (d : bf.Vtx) : ‖(fp.Λc I) X‖ ≤ A.colBudget * √↑(mainLabelsM A.G fp.Mc (bf.origCols u) catu I r (M ⟨q, ⋯⟩) d).card * (2 * ‖v‖) / √(dyadicGridLength A.G I.1) * ((β + β) * So * Sb)

Blueprint lines 2253-2254 on the main columns (a far band pair with the helper band higher: "expand the lower c band into its main pure sources; their tags lie in both masks writing the higher helper band as a difference of residuals, and their ranks are lower than the helper rank. The helper test applies with arbitrary L² spectators"): at an active cell, the cell form with the helper band Q_{a,p+1} - Q_{a,p} of a side value in slot a, a lower main band Q_{u,q+1} - Q_{u,q} (q + 2 < p) in slot u and two spectators is at most (D √N (2 ‖v‖) / √|I|) (2 β) S_o S_b, where β is the level of the helper residuals, D the column budget and N the number of main labels of the lower band's mask.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.padBand_resid_lt_main {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (l : Fin 4) (s : List (CatCol bf.Vtx)) (I : ℤ × ℤ) (r : ℕ) (M : Fin fp.P → bf.Vtx → Prop) {q : ℕ} (hq1 : 1 ≤ q) (hq : q < fp.P) (v : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) : (padFam (fun (k : Fin fp.P) => mainProj A.G fp.Mc (bf.origCols l) s I r (M k)) (q + 1)) v - (padFam (fun (k : Fin fp.P) => mainProj A.G fp.Mc (bf.origCols l) s I r (M k)) q) v = v - (mainProj A.G fp.Mc (bf.origCols l) s I r (M ⟨q - 1, ⋯⟩)) v - (v - (mainProj A.G fp.Mc (bf.origCols l) s I r (M ⟨q, hq⟩)) v)

A band strictly inside a pad family of main projections is a difference of two residuals.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.padBand_resid_top_main {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (l : Fin 4) (s : List (CatCol bf.Vtx)) (I : ℤ × ℤ) (r : ℕ) (M : Fin fp.P → bf.Vtx → Prop) (v : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) : (padFam (fun (k : Fin fp.P) => mainProj A.G fp.Mc (bf.origCols l) s I r (M k)) (fp.P + 1)) v - (padFam (fun (k : Fin fp.P) => mainProj A.G fp.Mc (bf.origCols l) s I r (M k)) fp.P) v = v - (mainProj A.G fp.Mc (bf.origCols l) s I r (M ⟨fp.P - 1, ⋯⟩)) v - 0

The top band of a pad family of main projections is a single residual.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.padBand_size_main {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (l : Fin 4) (s : List (CatCol bf.Vtx)) (I : ℤ × ℤ) (r : ℕ) (M : Fin fp.P → bf.Vtx → Prop) (hMm : ∀ (i j : Fin fp.P), i ≤ j → ∀ (x : bf.Vtx), M i x → M j x) {q : ℕ} (hq : q ≤ fp.P) (v : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) {S : ℝ} (hS : 2 * ‖v‖ / √(dyadicGridLength A.G I.1) ≤ S) : MeasureTheory.eLpNorm (augPhys ((padFam (fun (k : Fin fp.P) => mainProj A.G fp.Mc (bf.origCols l) s I r (M k)) (q + 1)) v - (padFam (fun (k : Fin fp.P) => mainProj A.G fp.Mc (bf.origCols l) s I r (M k)) q) v)) 2 (normalizedIntervalMeasure (dyadicGridLeft A.G I.1 I.2) (dyadicGridLength A.G I.1)) ≤ ENNReal.ofReal S

The normalized size of a band of a pad family of main projections.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.far_pair_main {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) {I : ℤ × ℤ} (hI : I ∈ A.cells) {o a : Fin 4} (hoa : o ≠ a) {x y : bf.Vtx} (hfar : ¬(bf.tagDist fp.Hed).d (bf.admT.depth (bf.admAt I)) x y ≤ 1) (Ax : QuadraticChartData (bf.vtag x).dim) (hAx : QuadraticChartComplexity A.csrc A.Hsrc Ax) (hAxb : IsBoundedQuadraticChart Ax) (hθ : Ax.horizontal = (bf.vtag x).θ) (hM : Ax.matrix = ↑(slotCoeff o) • (bf.vtag x).C) (hq : Ax.quadratic = ↑(slotCoeff o) * (bf.vtag x).lam) (Ay : QuadraticChartData (bf.vtag y).dim) (hAy : QuadraticChartComplexity A.csrc A.Hsrc Ay) (hAyb : IsBoundedQuadraticChart Ay) (hθ' : Ay.horizontal = (bf.vtag y).θ) (hM' : Ay.matrix = ↑(slotCoeff a) • (bf.vtag y).C) (hq' : Ay.quadratic = ↑(slotCoeff a) * (bf.vtag y).lam) {τ₂ : ℝ} (hτ₂ : 0 < τ₂) (hτ₂1 : τ₂ ≤ 1) (hHed : Real.exp (↑A.Dg * (1 + Real.log A.Hsrc + Real.log τ₂⁻¹) ^ A.Dg) ≤ fp.Hed) : PairSmall (dyadicGridLeft A.G I.1 I.2) (dyadicGridLength A.G I.1) (A.w I) o a (quadraticChartAtom Ax) (quadraticChartAtom Ay) τ₂

Blueprint lines 2255-2256 ("for a far source, expand the helper primal and use the different-tag pair estimate") on the main columns: pure charts, in two different slots, of two vertices at graph distance greater than one at an active cell are pair-separated (PairSmall with τ₂).

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.far_main_main {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) {I : ℤ × ℤ} (hI : I ∈ A.cells) {a u o b : Fin 4} (hua : u ≠ a) (huo : u ≠ o) (hub : u ≠ b) (hao : a ≠ o) (hab : a ≠ b) (hob : o ≠ b) (catu : List (CatCol bf.Vtx)) (r : ℕ) (M : Fin fp.P → bf.Vtx → Prop) (hMm : ∀ (i j : Fin fp.P), i ≤ j → ∀ (x : bf.Vtx), M i x → M j x) (v : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) {βm : ℝ} (hmain : ∀ (k : Fin fp.P), CellPass ⋯ A.csrc A.Hsrc bf.vtag u (M k) (v - (mainProj A.G fp.Mc (bf.origCols u) catu I r (M k)) v) βm) (hβm : 0 ≤ βm) (cata : List (CatCol bf.Vtx)) (rH : ℕ) (xa : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) {ι : Type u_1} (Fo : Finset ι) (co : ι → ℂ) (src : ι → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (tago : ι → bf.Vtx) (Ys : ι → ℝ → ℂ) (hsrc : ∀ m ∈ Fo, ∃ (A' : QuadraticChartData (bf.vtag (tago m)).dim), QuadraticChartComplexity A.csrc A.Hsrc A' ∧ A'.horizontal = (bf.vtag (tago m)).θ ∧ A'.matrix = ↑(slotCoeff o) • (bf.vtag (tago m)).C ∧ A'.quadratic = ↑(slotCoeff o) * (bf.vtag (tago m)).lam ∧ ∀ᵐ (y : ℝ), y ∈ dyadicGridCell A.G I.1 I.2 → augPhys (src m) y = quadraticChartAtom A' y) (hYs : ∀ m ∈ Fo, ∀ᵐ (y : ℝ), y ∈ dyadicGridCell A.G I.1 I.2 → augPhys (src m) y = Ys m y) {p q : ℕ} (hpq : p + 2 < q) (hqP : q ≤ fp.P) (near : ι → Prop) (hnear : ∀ m ∈ Fo, near m → ∀ (k : Fin fp.P), q - 1 ≤ ↑k → M k (tago m)) (d : bf.Vtx) (Yh : bf.Lab ⊕ Fin fp.Mc → ℝ → ℂ) (hYh : ∀ n ∈ mainLabelsM A.G fp.Mc (bf.origCols a) cata I rH (M ⟨p, ⋯⟩) d, ∀ᵐ (y : ℝ), y ∈ dyadicGridCell A.G I.1 I.2 → augPhys (mainCol A.G fp.Mc (bf.origCols a) cata I n) y = Yh n y) {τ₂ : ℝ} (hτ₂ : 0 ≤ τ₂) (hfar : ∀ m ∈ Fo, ¬near m → ∀ n ∈ mainLabelsM A.G fp.Mc (bf.origCols a) cata I rH (M ⟨p, ⋯⟩) d, PairSmall (dyadicGridLeft A.G I.1 I.2) (dyadicGridLength A.G I.1) (A.w I) o a (Ys m) (Yh n) τ₂) (X : Fin 4 → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (hXa : X a = (padFam (fun (k : Fin fp.P) => mainProj A.G fp.Mc (bf.origCols a) cata I rH (M k)) (p + 1)) xa - (padFam (fun (k : Fin fp.P) => mainProj A.G fp.Mc (bf.origCols a) cata I rH (M k)) p) xa) (hXu : X u = (padFam (fun (k : Fin fp.P) => mainProj A.G fp.Mc (bf.origCols u) catu I r (M k)) (q + 1)) v - (padFam (fun (k : Fin fp.P) => mainProj A.G fp.Mc (bf.origCols u) catu I r (M k)) q) v) (hXo : X o = ∑ m ∈ Fo, co m • src m) {Sa Sv Sb : ℝ} (hSa : 0 < Sa) (hSv : 0 < Sv) (hSb : 0 < Sb) (hSa' : 2 * ‖xa‖ / √(dyadicGridLength A.G I.1) ≤ Sa) (hSv' : 2 * ‖v‖ / √(dyadicGridLength A.G I.1) ≤ Sv) (hXb : MeasureTheory.eLpNorm (augPhys (X b)) 2 (normalizedIntervalMeasure (dyadicGridLeft A.G I.1 I.2) (dyadicGridLength A.G I.1)) ≤ ENNReal.ofReal Sb) : ‖(fp.Λc I) X‖ ≤ (∑ m ∈ Fo, ‖co m‖) * ((βm + βm) * Sa * Sb) + (τ₂ * Sv * Sb * ∑ m ∈ Fo, ‖co m‖) * (A.colBudget * √↑(mainLabelsM A.G fp.Mc (bf.origCols a) cata I rH (M ⟨p, ⋯⟩) d).card * Sa)

Blueprint lines 2254-2256 on the main columns (a far band pair with the complement band higher: "expand instead the lower-rank primal source in position d ... Neighbor closure puts a near source into pad p + 1 and hence into both masks of the higher c residual band. The main test applies, keeping the entire lower helper band as an L² spectator. For a far source, expand the helper primal and use the different-tag pair estimate"): at an active cell, with the band Q_{u,q+1} - Q_{u,q} of a complement value v in slot u (p + 2 < q), the helper band of a side value in slot a, a combination of pure sources in slot o and a spectator in slot b, the form is at most the near part (Σ|c|) (2 β) S_a S_b plus the far part τ₂ S_v S_b (Σ|c|) D √N_a S_a (N_a the labels of the helper band's mask).

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.far_term_main {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) {I : ℤ × ℤ} (hI : I ∈ A.cells) {a u o b : Fin 4} (hua : u ≠ a) (huo : u ≠ o) (hub : u ≠ b) (hao : a ≠ o) (hab : a ≠ b) (hob : o ≠ b) (catu : List (CatCol bf.Vtx)) (hTu : ∀ e ∈ catu, ∃ R ∈ residueBox (bf.vtag e.tag).dim 9, ∃ (γ : ℝ), e = templateCol (bf.vtag e.tag) u R γ e.birth e.rank e.tag) (htagu : ∀ e ∈ catu, bf.occAvail (↑e.tag.2) e.tag.1) (cata : List (CatCol bf.Vtx)) (hTa : ∀ e ∈ cata, ∃ R ∈ residueBox (bf.vtag e.tag).dim 9, ∃ (γ : ℝ), e = templateCol (bf.vtag e.tag) a R γ e.birth e.rank e.tag) (htaga : ∀ e ∈ cata, bf.occAvail (↑e.tag.2) e.tag.1) (r rH : ℕ) (M : Fin fp.P → bf.Vtx → Prop) (hMm : ∀ (i j : Fin fp.P), i ≤ j → ∀ (x : bf.Vtx), M i x → M j x) (hMn : ∀ (k : Fin fp.P) (hk : ↑k + 1 < fp.P) (w y : bf.Vtx), M k w → y ∈ bf.admT.X (bf.admAt I) → (bf.tagDist fp.Hed).d (bf.admT.depth (bf.admAt I)) w y ≤ 1 → M ⟨↑k + 1, hk⟩ y) (v xa : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) {βm βH : ℝ} (hβm : 0 ≤ βm) (hβH : 0 ≤ βH) (hmain : ∀ (k : Fin fp.P), CellPass ⋯ A.csrc A.Hsrc bf.vtag u (M k) (v - (mainProj A.G fp.Mc (bf.origCols u) catu I r (M k)) v) βm) (hhelp : ∀ (k : Fin fp.P), CellPass ⋯ A.csrc A.Hsrc bf.vtag a (M k) (xa - (mainProj A.G fp.Mc (bf.origCols a) cata I rH (M k)) xa) βH) {ι : Type u_1} (Fo : Finset ι) (co : ι → ℂ) (src : ι → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (tago : ι → bf.Vtx) (hpres : ∀ m ∈ Fo, tago m ∈ bf.admT.X (bf.admAt I)) (hsrc : ∀ m ∈ Fo, ∃ (Ay : QuadraticChartData (bf.vtag (tago m)).dim), QuadraticChartComplexity A.csrc A.Hsrc Ay ∧ IsBoundedQuadraticChart Ay ∧ Ay.horizontal = (bf.vtag (tago m)).θ ∧ Ay.matrix = ↑(slotCoeff o) • (bf.vtag (tago m)).C ∧ Ay.quadratic = ↑(slotCoeff o) * (bf.vtag (tago m)).lam ∧ ∀ᵐ (y : ℝ), y ∈ dyadicGridCell A.G I.1 I.2 → augPhys (src m) y = quadraticChartAtom Ay y) {Co : ℝ} (hCo : ∑ m ∈ Fo, ‖co m‖ ≤ Co) {τ₂ : ℝ} (hτ₂ : 0 < τ₂) (hτ₂1 : τ₂ ≤ 1) (hHed : Real.exp (↑A.Dg * (1 + Real.log A.Hsrc + Real.log τ₂⁻¹) ^ A.Dg) ≤ fp.Hed) (d : bf.Vtx) {Nu NH : ℝ} (hNu : ∀ (k : Fin fp.P), ↑(mainLabelsM A.G fp.Mc (bf.origCols u) catu I r (M k) d).card ≤ Nu) (hNH : ∀ (k : Fin fp.P), ↑(mainLabelsM A.G fp.Mc (bf.origCols a) cata I rH (M k) d).card ≤ NH) {p q : ℕ} (hp : p ≤ fp.P) (hq : q ≤ fp.P) (hfar : q + 2 < p ∨ p + 2 < q) (X : Fin 4 → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (hXa : X a = (padFam (fun (k : Fin fp.P) => mainProj A.G fp.Mc (bf.origCols a) cata I rH (M k)) (p + 1)) xa - (padFam (fun (k : Fin fp.P) => mainProj A.G fp.Mc (bf.origCols a) cata I rH (M k)) p) xa) (hXu : X u = (padFam (fun (k : Fin fp.P) => mainProj A.G fp.Mc (bf.origCols u) catu I r (M k)) (q + 1)) v - (padFam (fun (k : Fin fp.P) => mainProj A.G fp.Mc (bf.origCols u) catu I r (M k)) q) v) (hXo : X o = ∑ m ∈ Fo, co m • src m) {So Sa Sv Sb : ℝ} (hSo : 0 < So) (hSa : 0 < Sa) (hSv : 0 < Sv) (hSb : 0 < Sb) (hSa' : 2 * ‖xa‖ / √(dyadicGridLength A.G I.1) ≤ Sa) (hSv' : 2 * ‖v‖ / √(dyadicGridLength A.G I.1) ≤ Sv) (hXo' : MeasureTheory.eLpNorm (augPhys (X o)) 2 (normalizedIntervalMeasure (dyadicGridLeft A.G I.1 I.2) (dyadicGridLength A.G I.1)) ≤ ENNReal.ofReal So) (hXb : MeasureTheory.eLpNorm (augPhys (X b)) 2 (normalizedIntervalMeasure (dyadicGridLeft A.G I.1 I.2) (dyadicGridLength A.G I.1)) ≤ ENNReal.ofReal Sb) : ‖(fp.Λc I) X‖ ≤ A.colBudget * √Nu * Sv * ((βH + βH) * So * Sb) + (Co * ((βm + βm) * Sa * Sb) + τ₂ * Sv * Sb * Co * (A.colBudget * √NH * Sa))

Blueprint lines 2252-2258 for one transfer step on the main columns: the step moves a filter with pad masks M (monotone in the pad, consisting of present vertices, with neighbor closure) of rank r from the complement slot u to helper projections of rank r_H on the identical masks in the side slot a; the remaining other complement in slot o is a combination of pure sources of present vertices with coefficient sum at most C_o. Then every far band pair |p - q| > 2 of the step has form at most D √N_u S_v (2 β_H) S_o S_b + C_o (2 β_m) S_a S_b + τ₂ S_v S_b C_o D √N_H S_a, where β_m, β_H are the levels of the main and helper residuals and N_u, N_H bound the labels of the masks.

Generic band defect bounds (blueprint lines 2252-2258)

theorem TrilinearHT.Auto.opAvg_const {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {P : ℕ} (hP : 0 < P) (T : E →L[ℂ] E) : (opAvg fun (x : Fin P) => T) = T

The average of a constant family of operators is the operator.

Near and far parts of the transfer defects (blueprint lines 2252-2258)

noncomputable def TrilinearHT.Auto.chainDefectSel {E : Type u_1} [AddCommGroup E] [Module ℂ E] (Λ : MultilinearMap ℂ (fun (x : Fin 4) => E) ℂ) (P : ℕ) (a c d : Fin 4) (x : Fin 4 → E) (yc yd : E) (sel : ℕ → ℕ → Prop) [DecidableRel sel] : List (TransferStep E) → E → ℂ

The band defects of the transfer steps restricted to the band pairs (p, q) selected by sel (the near pairs |p - q| ≤ 2 or the far pairs).

Equations

• One or more equations did not get rendered due to their size.
• TrilinearHT.Auto.chainDefectSel Λ P a c d x yc yd sel [] x✝ = 0

theorem TrilinearHT.Auto.chainDefectSel_le {E : Type u_1} [AddCommGroup E] [Module ℂ E] (Λ : MultilinearMap ℂ (fun (x : Fin 4) => E) ℂ) {P : ℕ} (hP : 0 < P) (a c d : Fin 4) (x : Fin 4 → E) (yc yd : E) (sel : ℕ → ℕ → Prop) [DecidableRel sel] {B : ℝ} (hB0 : 0 ≤ B) (steps : List (TransferStep E)) (xa : E) : (∀ (pre : List (TransferStep E)) (st : TransferStep E) (rest : List (TransferStep E)), steps = pre ++ st :: rest → ∀ p ≤ P, ∀ q ≤ P, sel p q → ‖Λ (Function.update (Function.update (Function.update (Function.update x c (chainVal P true rest yc)) d (chainVal P false rest yd)) a ((st.2.1 (p + 1)) (chainSide P pre xa) - (st.2.1 p) (chainSide P pre xa))) (if st.1 = true then c else d) ((st.2.2 (q + 1)) (chainVal P st.1 rest (if st.1 = true then yc else yd)) - (st.2.2 q) (chainVal P st.1 rest (if st.1 = true then yc else yd))))‖ ≤ B) → ‖chainDefectSel Λ P a c d x yc yd sel steps xa‖ ≤ ↑steps.length * ((↑P + 1) ^ 2 * B)

If every selected band term of every step (with the side value of the earlier steps) is at most B, the selected defects are at most #steps (P + 1)² B (the transfer coefficients (p - q) / P have modulus at most one).

Transfer steps of rank-merged main filters (blueprint lines 2240-2252)

theorem TrilinearHT.Auto.operatorComplementProduct_succ_shift {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (B : ℕ → H →L[ℂ] H) (n : ℕ) (x : H) : (operatorComplementProduct B (fun (x : ℕ) => false) (n + 1)) x = (operatorComplementProduct (fun (l : ℕ) => B (l + 1)) (fun (x : ℕ) => false) n) ((B 0) x)

A positive product of n + 1 factors is the product of the shifted factors after the first factor.

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.filtAvgM {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (l : Fin 4) (s : List (CatCol bf.Vtx)) (I : ℤ × ℤ) (f : ℕ × (Fin fp.P → bf.Vtx → Prop)) : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc)) →ₗ[ℂ] ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))

The averaged main filter of a rank and pad masks on the catalog s of the slot l.

Equations

• fp.filtAvgM l s I f = TrilinearHT.Auto.filterAvg fp.P (TrilinearHT.Auto.padFam fun (p : Fin fp.P) => TrilinearHT.Auto.mainProj A.G fp.Mc (bf.origCols l) s I f.1 (f.2 p))

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.filtAvgM_apply {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (l : Fin 4) (s : List (CatCol bf.Vtx)) (I : ℤ × ℤ) (f : ℕ × (Fin fp.P → bf.Vtx → Prop)) (y : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) : (fp.filtAvgM l s I f) y = (opAvg fun (p : Fin fp.P) => mainProj A.G fp.Mc (bf.origCols l) s I f.1 (f.2 p)) y

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.norm_applyAll_filtAvgM_le {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (l : Fin 4) (s : List (CatCol bf.Vtx)) (I : ℤ × ℤ) (L : List (ℕ × (Fin fp.P → bf.Vtx → Prop))) (y : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) : ‖applyAll (List.map (fp.filtAvgM l s I) L) y‖ ≤ ‖y‖

The averaged main filters along a list are contractions.

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.toStepM {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (cat : Fin 4 → List (CatCol bf.Vtx)) (a c d : Fin 4) (rH : ℕ) (I : ℤ × ℤ) (e : Bool × ℕ × (Fin fp.P → bf.Vtx → Prop)) : Bool × (Fin fp.P → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc)) →L[ℂ] ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) × (Fin fp.P → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc)) →L[ℂ] ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc)))

The transfer step of a merged filter on the main columns: helper pads of rank r_H on the catalog of the side slot a, and main pads of the filter rank on the catalog of its complement slot (c for true, d for false).

Equations

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

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.mergeStepsM {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (cat : Fin 4 → List (CatCol bf.Vtx)) (a c d : Fin 4) (rH : ℕ) (I : ℤ × ℤ) (xs ys : List (ℕ × (Fin fp.P → bf.Vtx → Prop))) : List (TransferStep ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc)))

The transfer steps of two filter lists merged by rank, on the main columns.

Equations

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

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.chainVal_mergeStepsM_c {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (cat : Fin 4 → List (CatCol bf.Vtx)) (a c d : Fin 4) (rH : ℕ) (I : ℤ × ℤ) (xs ys : List (ℕ × (Fin fp.P → bf.Vtx → Prop))) (y : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) : chainVal fp.P true (fp.mergeStepsM cat a c d rH I xs ys) y = applyAll (List.map (fp.filtAvgM c (cat c) I) xs) y

The slot c value of merged steps is the composition of the c filters.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.chainVal_mergeStepsM_d {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (cat : Fin 4 → List (CatCol bf.Vtx)) (a c d : Fin 4) (rH : ℕ) (I : ℤ × ℤ) (xs ys : List (ℕ × (Fin fp.P → bf.Vtx → Prop))) (y : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) : chainVal fp.P false (fp.mergeStepsM cat a c d rH I xs ys) y = applyAll (List.map (fp.filtAvgM d (cat d) I) ys) y

The slot d value of merged steps is the composition of the d filters.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.chainSide_mergeStepsM {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (cat : Fin 4 → List (CatCol bf.Vtx)) (a c d : Fin 4) (rH : ℕ) (I : ℤ × ℤ) (pre : List (Bool × ℕ × (Fin fp.P → bf.Vtx → Prop))) (x : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) : chainSide fp.P (List.map (fun (st : Bool × (Fin fp.P → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc)) →L[ℂ] ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) × (Fin fp.P → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc)) →L[ℂ] ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc)))) => (st.1, padFam st.2.1, padFam st.2.2)) (List.map (fp.toStepM cat a c d rH I) pre)) x = (operatorComplementProduct (fun (l : ℕ) => opAvg fun (p : Fin fp.P) => mainProj A.G fp.Mc (bf.origCols a) (cat a) I rH ((pre.getD l (true, 0, fun (x : Fin fp.P) (x_1 : bf.Vtx) => False)).2.2 p)) (fun (x : ℕ) => false) pre.length) x

The side value after merged steps is the product of the averaged helper filters of the steps, innermost first.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.norm_chainSide_mergeStepsM_le {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (cat : Fin 4 → List (CatCol bf.Vtx)) (a c d : Fin 4) (rH : ℕ) (I : ℤ × ℤ) (pre : List (Bool × ℕ × (Fin fp.P → bf.Vtx → Prop))) (x : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) : ‖chainSide fp.P (List.map (fun (st : Bool × (Fin fp.P → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc)) →L[ℂ] ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) × (Fin fp.P → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc)) →L[ℂ] ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc)))) => (st.1, padFam st.2.1, padFam st.2.2)) (List.map (fp.toStepM cat a c d rH I) pre)) x‖ ≤ ‖x‖

The side value after merged steps is a contraction of the side state.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.mergeStepsM_decomp {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (cat : Fin 4 → List (CatCol bf.Vtx)) (a c d : Fin 4) (rH : ℕ) (I : ℤ × ℤ) (xs ys : List (ℕ × (Fin fp.P → bf.Vtx → Prop))) (pre : List (TransferStep ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc)))) (st : TransferStep ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (rest : List (TransferStep ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc)))) (h : fp.mergeStepsM cat a c d rH I xs ys = pre ++ st :: rest) : ∃ (preM : List (Bool × ℕ × (Fin fp.P → bf.Vtx → Prop))) (e : Bool × ℕ × (Fin fp.P → bf.Vtx → Prop)) (xs' : List (ℕ × (Fin fp.P → bf.Vtx → Prop))) (ys' : List (ℕ × (Fin fp.P → bf.Vtx → Prop))), pre = List.map (fun (st : Bool × (Fin fp.P → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc)) →L[ℂ] ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) × (Fin fp.P → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc)) →L[ℂ] ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc)))) => (st.1, padFam st.2.1, padFam st.2.2)) (List.map (fp.toStepM cat a c d rH I) preM) ∧ st = ((fp.toStepM cat a c d rH I e).1, padFam (fp.toStepM cat a c d rH I e).2.1, padFam (fp.toStepM cat a c d rH I e).2.2) ∧ rest = fp.mergeStepsM cat a c d rH I xs' ys' ∧ rankMerge Prod.fst xs ys = preM ++ e :: rankMerge Prod.fst xs' ys' ∧ ((e.1 = true ∧ e.2 :: xs' <:+ xs ∧ ys' <:+ ys ∧ ∀ y ∈ ys'.head?, y.1 < e.2.1) ∨ e.1 = false ∧ xs' <:+ xs ∧ e.2 :: ys' <:+ ys ∧ ∀ x ∈ xs'.head?, x.1 ≤ e.2.1)

A step of merged transfer steps comes from a merge element: the earlier steps are those of the merge prefix and the later steps are the merge of the remaining suffixes.

The far band defects of rank-merged main filters (blueprint lines 2252-2258)

def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SrcDataM {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (o : Fin 4) (I : ℤ × ℤ) (w : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (Co : ℝ) : Prop

The source data of a slot value used by the far band estimate on the main columns: a combination of bounded pure sources of present vertices in the slot o with coefficient sum at most C_o.

Equations

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

def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.FiltOK {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (I : ℤ × ℤ) (f : ℕ × (Fin fp.P → bf.Vtx → Prop)) : Prop

The mask conditions of a removed filter (blueprint lines 2254-2256): its pad masks grow with the pad and have neighbor closure among present vertices.

Equations

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

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.far_stepM {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (cat : Fin 4 → List (CatCol bf.Vtx)) (hT : ∀ (l : Fin 4), ∀ e ∈ cat l, ∃ R ∈ residueBox (bf.vtag e.tag).dim 9, ∃ (γ : ℝ), e = templateCol (bf.vtag e.tag) l R γ e.birth e.rank e.tag) (htag : ∀ (l : Fin 4), ∀ e ∈ cat l, bf.occAvail (↑e.tag.2) e.tag.1) {I : ℤ × ℤ} (hI : I ∈ A.cells) {a u o b : Fin 4} (hua : u ≠ a) (huo : u ≠ o) (hub : u ≠ b) (hao : a ≠ o) (hab : a ≠ b) (hob : o ≠ b) (rH : ℕ) (f : ℕ × (Fin fp.P → bf.Vtx → Prop)) (hf : fp.FiltOK I f) (yu yo : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (xs' ys' : List (ℕ × (Fin fp.P → bf.Vtx → Prop))) {βm : ℝ} (hβm : 0 ≤ βm) (hmain : ∀ (k : Fin fp.P), CellPass ⋯ A.csrc A.Hsrc bf.vtag u (f.2 k) (applyAll (List.map (fp.filtAvgM u (cat u) I) xs') yu - (mainProj A.G fp.Mc (bf.origCols u) (cat u) I f.1 (f.2 k)) (applyAll (List.map (fp.filtAvgM u (cat u) I) xs') yu)) βm) {Co Sz : ℝ} (hSz : 0 < Sz) (hsrc : fp.SrcDataM o I (applyAll (List.map (fp.filtAvgM o (cat o) I) ys') yo) Co) (hyu : ‖yu‖ / √(dyadicGridLength A.G I.1) ≤ Sz) (hyo : ‖yo‖ / √(dyadicGridLength A.G I.1) ≤ Sz) (xa : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) {βH : ℝ} (hβH : 0 ≤ βH) (hhelp : ∀ (k : Fin fp.P), CellPass ⋯ A.csrc A.Hsrc bf.vtag a (f.2 k) (xa - (mainProj A.G fp.Mc (bf.origCols a) (cat a) I rH (f.2 k)) xa) βH) (d₀ : bf.Vtx) {Nm NH : ℝ} (hNm : ∀ (k : Fin fp.P), ↑(mainLabelsM A.G fp.Mc (bf.origCols u) (cat u) I f.1 (f.2 k) d₀).card ≤ Nm) (hNH : ∀ (k : Fin fp.P), ↑(mainLabelsM A.G fp.Mc (bf.origCols a) (cat a) I rH (f.2 k) d₀).card ≤ NH) {τ₂ : ℝ} (hτ₂ : 0 < τ₂) (hτ₂1 : τ₂ ≤ 1) (hHed : Real.exp (↑A.Dg * (1 + Real.log A.Hsrc + Real.log τ₂⁻¹) ^ A.Dg) ≤ fp.Hed) (X : Fin 4 → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) {p q : ℕ} (hp : p ≤ fp.P) (hq : q ≤ fp.P) (hfar : q + 2 < p ∨ p + 2 < q) (hXa : X a = (padFam (fun (k : Fin fp.P) => mainProj A.G fp.Mc (bf.origCols a) (cat a) I rH (f.2 k)) (p + 1)) xa - (padFam (fun (k : Fin fp.P) => mainProj A.G fp.Mc (bf.origCols a) (cat a) I rH (f.2 k)) p) xa) (hXu : X u = (padFam (fun (k : Fin fp.P) => mainProj A.G fp.Mc (bf.origCols u) (cat u) I f.1 (f.2 k)) (q + 1)) (applyAll (List.map (fp.filtAvgM u (cat u) I) xs') yu) - (padFam (fun (k : Fin fp.P) => mainProj A.G fp.Mc (bf.origCols u) (cat u) I f.1 (f.2 k)) q) (applyAll (List.map (fp.filtAvgM u (cat u) I) xs') yu)) (hXo : X o = applyAll (List.map (fp.filtAvgM o (cat o) I) ys') yo) {Sa Sb : ℝ} (hSa : 0 < Sa) (hSa' : 2 * ‖xa‖ / √(dyadicGridLength A.G I.1) ≤ Sa) (hSb : 0 < Sb) (hXb : MeasureTheory.eLpNorm (augPhys (X b)) 2 (normalizedIntervalMeasure (dyadicGridLeft A.G I.1 I.2) (dyadicGridLength A.G I.1)) ≤ ENNReal.ofReal Sb) : ‖(fp.Λc I) X‖ ≤ A.colBudget * √Nm * (2 * Sz) * ((βH + βH) * Sz * Sb) + (Co * ((βm + βm) * Sa * Sb) + τ₂ * (2 * Sz) * Sb * Co * (A.colBudget * √NH * Sa))

Blueprint lines 2252-2258 for one step of a merged transfer on the main columns: the step removes the filter f from the slot u, whose inner value (the inner filters xs' applied to the argument y_u) passes the main tests of the pads at level β_m; the side value x_a passes the helper tests at level β_H; the other complement (the filters ys' applied to y_o) has source data with coefficient sum C_o. Then every far band pair of the step has form at most D √N_m (2 S_z) (2 β_H) S_z S_b + C_o (2 β_m) S_a S_b + τ₂ (2 S_z) S_b C_o D √N_H S_a.

def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.headRank {α : Type u_1} (l : List (ℕ × α)) : ℕ

The rank of the outermost filter of a filter list (zero for the unfiltered argument).

Equations

• TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.headRank l = (Option.map Prod.fst l.head?).getD 0

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.chainPair_farM {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (cat : Fin 4 → List (CatCol bf.Vtx)) (hT : ∀ (l : Fin 4), ∀ e ∈ cat l, ∃ R ∈ residueBox (bf.vtag e.tag).dim 9, ∃ (γ : ℝ), e = templateCol (bf.vtag e.tag) l R γ e.birth e.rank e.tag) (htag : ∀ (l : Fin 4), ∀ e ∈ cat l, bf.occAvail (↑e.tag.2) e.tag.1) {I : ℤ × ℤ} (hI : I ∈ A.cells) {a b c d : Fin 4} (hca : c ≠ a) (hcd : c ≠ d) (hcb : c ≠ b) (hda : d ≠ a) (hdb : d ≠ b) (hab : a ≠ b) (rH : ℕ) (xs ys : List (ℕ × (Fin fp.P → bf.Vtx → Prop))) (yc yd : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (βm : ℕ → ℝ) (hβm : ∀ (r : ℕ), 0 ≤ βm r) (hxs : ∀ (f : ℕ × (Fin fp.P → bf.Vtx → Prop)) (xs' : List (ℕ × (Fin fp.P → bf.Vtx → Prop))), f :: xs' <:+ xs → fp.FiltOK I f ∧ ∀ (k : Fin fp.P), CellPass ⋯ A.csrc A.Hsrc bf.vtag c (f.2 k) (applyAll (List.map (fp.filtAvgM c (cat c) I) xs') yc - (mainProj A.G fp.Mc (bf.origCols c) (cat c) I f.1 (f.2 k)) (applyAll (List.map (fp.filtAvgM c (cat c) I) xs') yc)) (βm f.1)) (hys : ∀ (f : ℕ × (Fin fp.P → bf.Vtx → Prop)) (ys' : List (ℕ × (Fin fp.P → bf.Vtx → Prop))), f :: ys' <:+ ys → fp.FiltOK I f ∧ ∀ (k : Fin fp.P), CellPass ⋯ A.csrc A.Hsrc bf.vtag d (f.2 k) (applyAll (List.map (fp.filtAvgM d (cat d) I) ys') yd - (mainProj A.G fp.Mc (bf.origCols d) (cat d) I f.1 (f.2 k)) (applyAll (List.map (fp.filtAvgM d (cat d) I) ys') yd)) (βm f.1)) (hdist : ∀ f ∈ xs, ∀ g ∈ ys, f.1 ≠ g.1) (hposc : ∀ f ∈ xs, 0 < f.1) (hposd : ∀ g ∈ ys, 0 < g.1) (Co : ℕ → ℝ) {Sz : ℝ} (hSz : 0 < Sz) (hsc : ∀ (xs' : List (ℕ × (Fin fp.P → bf.Vtx → Prop))), xs' <:+ xs → fp.SrcDataM c I (applyAll (List.map (fp.filtAvgM c (cat c) I) xs') yc) (Co (headRank xs'))) (hsd : ∀ (ys' : List (ℕ × (Fin fp.P → bf.Vtx → Prop))), ys' <:+ ys → fp.SrcDataM d I (applyAll (List.map (fp.filtAvgM d (cat d) I) ys') yd) (Co (headRank ys'))) (hyc : ‖yc‖ / √(dyadicGridLength A.G I.1) ≤ Sz) (hyd : ‖yd‖ / √(dyadicGridLength A.G I.1) ≤ Sz) (x : Fin 4 → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) {βH : ℝ} (hβH : 0 ≤ βH) (hhelp : ∀ (preM : List (Bool × ℕ × (Fin fp.P → bf.Vtx → Prop))) (e : Bool × ℕ × (Fin fp.P → bf.Vtx → Prop)) (restM : List (Bool × ℕ × (Fin fp.P → bf.Vtx → Prop))), rankMerge Prod.fst xs ys = preM ++ e :: restM → ∀ (k : Fin fp.P), CellPass ⋯ A.csrc A.Hsrc bf.vtag a (e.2.2 k) ((operatorComplementProduct (fun (l : ℕ) => opAvg fun (p : Fin fp.P) => mainProj A.G fp.Mc (bf.origCols a) (cat a) I rH ((preM.getD l (true, 0, fun (x : Fin fp.P) (x_1 : bf.Vtx) => False)).2.2 p)) (fun (x : ℕ) => false) preM.length) (x a) - (mainProj A.G fp.Mc (bf.origCols a) (cat a) I rH (e.2.2 k)) ((operatorComplementProduct (fun (l : ℕ) => opAvg fun (p : Fin fp.P) => mainProj A.G fp.Mc (bf.origCols a) (cat a) I rH ((preM.getD l (true, 0, fun (x : Fin fp.P) (x_1 : bf.Vtx) => False)).2.2 p)) (fun (x : ℕ) => false) preM.length) (x a))) βH) (d₀ : bf.Vtx) {Nm NH : ℝ} (hNmc : ∀ f ∈ xs, ∀ (M : bf.Vtx → Prop), ↑(mainLabelsM A.G fp.Mc (bf.origCols c) (cat c) I f.1 M d₀).card ≤ Nm) (hNmd : ∀ g ∈ ys, ∀ (M : bf.Vtx → Prop), ↑(mainLabelsM A.G fp.Mc (bf.origCols d) (cat d) I g.1 M d₀).card ≤ Nm) (hNH : ∀ (M : bf.Vtx → Prop), ↑(mainLabelsM A.G fp.Mc (bf.origCols a) (cat a) I rH M d₀).card ≤ NH) {τ₂ : ℝ} (hτ₂ : 0 < τ₂) (hτ₂1 : τ₂ ≤ 1) (hHed : Real.exp (↑A.Dg * (1 + Real.log A.Hsrc + Real.log τ₂⁻¹) ^ A.Dg) ≤ fp.Hed) {Sa Sb : ℝ} (hSa : 0 < Sa) (hSa' : 2 * ‖x a‖ / √(dyadicGridLength A.G I.1) ≤ Sa) (hSb : 0 < Sb) (hXb : MeasureTheory.eLpNorm (augPhys (x b)) 2 (normalizedIntervalMeasure (dyadicGridLeft A.G I.1 I.2) (dyadicGridLength A.G I.1)) ≤ ENNReal.ofReal Sb) {B : ℝ} (hB0 : 0 ≤ B) (hB : ∀ (Rf : ℕ), ((∃ f ∈ xs, f.1 = Rf) ∨ ∃ g ∈ ys, g.1 = Rf) → ∀ Ro < Rf, A.colBudget * √Nm * (2 * Sz) * ((βH + βH) * Sz * Sb) + (Co Ro * ((βm Rf + βm Rf) * Sa * Sb) + τ₂ * (2 * Sz) * Sb * Co Ro * (A.colBudget * √NH * Sa)) ≤ B) : ‖chainDefectSel (fp.Λc I) fp.P a c d x yc yd (fun (p q : ℕ) => q + 2 < p ∨ p + 2 < q) (fp.mergeStepsM cat a c d rH I xs ys) (x a)‖ ≤ ↑(fp.mergeStepsM cat a c d rH I xs ys).length * ((↑fp.P + 1) ^ 2 * B)

Blueprint lines 2252-2258 ("the far terms cost at most ... per cell and group") for two lists of filters of the complement slots c, d with distinct positive ranks, merged by rank: if every removed filter has the mask conditions and its inner value passes the main tests of its pads at the level β_m of its rank, every remaining complement has source data with the coefficient sum C_o of its outer rank (rank zero when unfiltered), and the side value of every step passes the helper tests at level β_H, then the far band defects of the merged transfer steps are at most #steps (P + 1)² B, whenever B bounds the step bound of far_stepM for every removed rank and every strictly lower outer rank of the other complement ("the other complementary argument always has a strictly lower-rank outer primal source").

The filters of a leaf and their passes on the main columns (blueprint lines 2240-2256)

def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.slotFiltM {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (G : bf.Grp) (j : ℕ) (I : ℤ × ℤ) (t : List ℕ) : List (ℕ × (Fin fp.P → bf.Vtx → Prop))

The positive filters of a slot for the group G at the ball level j on the cell I along the positive chain t (outermost first): the ball filter, then the cumulative layers of the chain, each as its rank and its pad masks.

Equations

• fp.slotFiltM G j I t = (fp.brank j, fun (p : Fin fp.P) => fp.bmask I G j (↑p + 1)) :: List.map (fun (m : ℕ) => (fp.crank m, fun (p : Fin fp.P) => fp.cmask I m (↑p + 1))) t

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.applyAll_cumM {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (l : Fin 4) (s : List (CatCol bf.Vtx)) (I : ℤ × ℤ) (t : List ℕ) (y : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) : applyAll (List.map (fp.filtAvgM l s I) (List.map (fun (m : ℕ) => (fp.crank m, fun (p : Fin fp.P) => fp.cmask I m (↑p + 1))) t)) y = (chainOp (fun (m : ℕ) => fp.cumFilt l s I m) t) y

The cumulative layers of a positive chain are the averages of their pad families.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.applyAll_slotFiltM {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (l : Fin 4) (s : List (CatCol bf.Vtx)) (G : bf.Grp) (j : ℕ) (I : ℤ × ℤ) (t : List ℕ) (y : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) : applyAll (List.map (fp.filtAvgM l s I) (fp.slotFiltM G j I t)) y = (fp.ballFilt l s I G j) ((chainOp (fun (m : ℕ) => fp.cumFilt l s I m) t) y)

The filters of a slot along a positive chain compose to the ball filter of the chain output.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.slotFiltM_suffix_cons {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (G : bf.Grp) (j : ℕ) (I : ℤ × ℤ) (t : List ℕ) {f : ℕ × (Fin fp.P → bf.Vtx → Prop)} {xs' : List (ℕ × (Fin fp.P → bf.Vtx → Prop))} (h : f :: xs' <:+ fp.slotFiltM G j I t) : f = (fp.brank j, fun (p : Fin fp.P) => fp.bmask I G j (↑p + 1)) ∧ xs' = List.map (fun (m : ℕ) => (fp.crank m, fun (p : Fin fp.P) => fp.cmask I m (↑p + 1))) t ∨ ∃ k < t.length, f = (fp.crank (t.getD k 0), fun (p : Fin fp.P) => fp.cmask I (t.getD k 0) (↑p + 1)) ∧ xs' = List.map (fun (m : ℕ) => (fp.crank m, fun (p : Fin fp.P) => fp.cmask I m (↑p + 1))) (List.drop (k + 1) t)

A suffix of the filters of a slot along a chain, headed by a filter, is the whole list (the ball filter first) or a cumulative layer of the chain followed by the inner layers.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.filtOK_cum {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (I : ℤ × ℤ) (m : ℕ) : fp.FiltOK I (fp.crank m, fun (p : Fin fp.P) => fp.cmask I m (↑p + 1))

Blueprint line 2256 ("cumulative masks have neighbor closure by the triangle inequality"): the filters of cumulative layers have the mask conditions.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.filtOK_ball {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (I : ℤ × ℤ) {v₀ : bf.Vtx} (hv₀ : v₀ ∈ bf.admT.X (bf.admAt I)) (hs₀ : fp.K.Success (fp.K.colorData (bf.admT.st (bf.admAt I)) v₀)) {j : ℕ} (hj : j ≤ 4) : fp.FiltOK I (fp.brank j, fun (p : Fin fp.P) => fp.bmask I (fp.K.grp bf.admT A.famVtxBound (bf.admAt I) v₀) j (↑p + 1))

Blueprint line 2256 ("ball masks have it at actual uses by Lemma masks"): the ball filter of the group of a successful present vertex has the mask conditions.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.cmask_present {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) {I : ℤ × ℤ} {m p : ℕ} {x : bf.Vtx} (hx : fp.cmask I m p x) : x ∈ bf.admT.X (bf.admAt I)

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.bmask_present {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) {I : ℤ × ℤ} {G : bf.Grp} {j p : ℕ} {x : bf.Vtx} (hx : fp.bmask I G j p x) : x ∈ bf.admT.X (bf.admAt I)

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.srcDataM_filt {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (o : Fin 4) (s : List (CatCol bf.Vtx)) (hT : ∀ e ∈ s, ∃ R ∈ residueBox (bf.vtag e.tag).dim 9, ∃ (γ : ℝ), e = templateCol (bf.vtag e.tag) o R γ e.birth e.rank e.tag) (htag : ∀ e ∈ s, bf.occAvail (↑e.tag.2) e.tag.1) (I : ℤ × ℤ) (g : ℕ × (Fin fp.P → bf.Vtx → Prop)) (hg : ∀ (k : Fin fp.P) (x : bf.Vtx), g.2 k x → x ∈ bf.admT.X (bf.admAt I)) (d₀ : bf.Vtx) (z : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) {S N Co : ℝ} (hz : ‖z‖ / √(dyadicGridLength A.G I.1) ≤ S) (hN : ↑(mainLabelsM A.G fp.Mc (bf.origCols o) s I g.1 (fun (y : bf.Vtx) => ∃ (p : Fin fp.P), g.2 p y) d₀).card ≤ N) (hCo : A.colBudget * √N * S ≤ Co) : fp.SrcDataM o I ((fp.filtAvgM o s I g) z) Co

Blueprint line 2254 ("expand instead the lower-rank primal source"): an averaged main filter of a slot with masks of present vertices, applied to a value of size at most S √|I|, is a combination of bounded pure sources of present vertices with coefficient sum at most D √N S when the masked main labels number at most N.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.srcDataM_basic {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (o : Fin 4) (s : List (CatCol bf.Vtx)) (hT : ∀ e ∈ s, ∃ R ∈ residueBox (bf.vtag e.tag).dim 9, ∃ (γ : ℝ), e = templateCol (bf.vtag e.tag) o R γ e.birth e.rank e.tag) (htag : ∀ e ∈ s, bf.occAvail (↑e.tag.2) e.tag.1) {I : ℤ × ℤ} (hI : I ∈ A.cells) (d₀ : bf.Vtx) {S Co : ℝ} (hz : ‖bf.basicIn fp.Mc o I‖ / √(dyadicGridLength A.G I.1) ≤ S) (hCo : A.colBudget * √(2 * A.colBudget) * S ≤ Co) : fp.SrcDataM o I (bf.basicIn fp.Mc o I) Co

Blueprint line 2254 ("using its basic columns when it is unfiltered"): the basic input of a slot at an active cell is a combination of bounded pure sources of present vertices (its available original columns) with coefficient sum at most D √(2D) S.

def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.MainRk {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) {I : ℤ × ℤ} {Bn : Type} (w : fp.TestName I Bn) : Prop

A test name of main rank: target rank and history ranks at most L + 4 (blueprint lines 1815 and 1828: the main ranks are 1, …, L + 4, the rank L + 5 is reserved for the helper tests).

Equations

• fp.MainRk w = (↑w.1 + 1 ≤ fp.Lc + 4 ∧ ∀ (i : Fin ↑w.2.2.1.fst), ↑(w.2.2.1.snd i).1 ≤ fp.Lc + 4)

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.mainRk_layerName {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (I : ℤ × ℤ) (r : Fin (fp.Lc + 5)) (Mt : fp.MaskName I) (ls : List (ℕ × Bool)) (hls : ∀ e ∈ ls, e.1 ≤ fp.Lc) (hlen : ls.length ≤ fp.mH) (c : Fin ls.length → Fin fp.P) (hr : ↑r + 1 ≤ fp.Lc + 4) : fp.MainRk (fp.layerName I r Mt ls hls hlen c)

The layer test names of a target rank at most L + 4 have main rank (their history ranks are cumulative ranks L - m + 1 ≤ L + 1).

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.chain_passM {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (l : Fin 4) (s : List (CatCol bf.Vtx)) {I : ℤ × ℤ} (hI : I ∈ A.cells) (z : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) {τ : ℕ → ℝ} (hpass : ∀ (w : fp.TestName I Unit), fp.MainRk w → (fp.testOf l I (fun (x : Unit) => z) w).Pass A.G (bf.origCols l) I A.csrc A.Hsrc bf.vtag (A.w I) (τ (fp.testOf l I (fun (x : Unit) => z) w).r) fp.mH s) (ch : List ℕ) (hch : ∀ m ∈ ch, m ≤ fp.Lc) (hlen : ch.length ≤ fp.mH) (r : Fin (fp.Lc + 5)) (hr : ↑r + 1 ≤ fp.Lc + 4) (Mt : fp.MaskName I) : CellPass ⋯ A.csrc A.Hsrc bf.vtag l (fp.maskOf I Mt) ((chainOp (fun (m : ℕ) => fp.cumFilt l s I m) ch) z - (mainProj A.G fp.Mc (bf.origCols l) s I (↑r + 1) (fp.maskOf I Mt)) ((chainOp (fun (m : ℕ) => fp.cumFilt l s I m) ch) z)) (τ (↑r + 1) * cellNorm A.G I z)

Blueprint lines 1807-1811 and 2254 on a positive chain (the main test of a transfer step): if the named main tests of the slot pass, the residual of a single named target projection of rank r + 1 on the chain value of the basic argument passes at level τ_{r+1} ‖z‖_{2,I}.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.helper_stepPass {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (l : Fin 4) (s : List (CatCol bf.Vtx)) {I : ℤ × ℤ} (hI : I ∈ A.cells) {Bh : Type} (base : Bh → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (b₀ : Bh) {τH : ℝ} (hpass : ∀ (w : fp.HelperName I Bh), (fp.helperOf l I base w).Pass A.G (bf.origCols l) I A.csrc A.Hsrc bf.vtag (A.w I) τH fp.mH s) (k : ℕ) (hk : k ≤ fp.mH) (Mst : ℕ → Fin fp.P → bf.Vtx → Prop) (hMst : ∀ i < k, ∀ (p : Fin fp.P), ∃ (M : fp.MaskName I), fp.maskOf I M = Mst i p) (Mt : fp.MaskName I) : CellPass ⋯ A.csrc A.Hsrc bf.vtag l (fp.maskOf I Mt) ((operatorComplementProduct (fun (i : ℕ) => opAvg fun (p : Fin fp.P) => mainProj A.G fp.Mc (bf.origCols l) s I (fp.Lc + 5) (Mst i p)) (fun (x : ℕ) => false) k) (base b₀) - (mainProj A.G fp.Mc (bf.origCols l) s I (fp.Lc + 5) (fp.maskOf I Mt)) ((operatorComplementProduct (fun (i : ℕ) => opAvg fun (p : Fin fp.P) => mainProj A.G fp.Mc (bf.origCols l) s I (fp.Lc + 5) (Mst i p)) (fun (x : ℕ) => false) k) (base b₀))) (τH * cellNorm A.G I (base b₀))

Blueprint lines 2253 and 1810-1811 (the helper test of a transfer step): if the named helper tests of the slot pass on the base base b₀ at threshold τ_H, the residual of a single named helper target projection on the side value after k averaged helper factors with named pad masks passes at level τ_H ‖base b₀‖_{2,I}.

theorem TrilinearHT.Auto.rankMerge_mem {α : Type u_1} (key : α → ℕ) (xs ys : List α) {e : Bool × α} (he : e ∈ rankMerge key xs ys) : e.2 ∈ xs ∨ e.2 ∈ ys

The entries of a merge come from the two lists.

theorem TrilinearHT.Auto.rankMerge_length {α : Type u_1} (key : α → ℕ) (xs ys : List α) : (rankMerge key xs ys).length = xs.length + ys.length

A merge has the total length of the two lists.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.chain_passR {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (l : Fin 4) (s : List (CatCol bf.Vtx)) {I : ℤ × ℤ} (hI : I ∈ A.cells) (z : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) {τ : ℕ → ℝ} (hpass : ∀ (w : fp.TestName I Unit), fp.MainRk w → (fp.testOf l I (fun (x : Unit) => z) w).Pass A.G (bf.origCols l) I A.csrc A.Hsrc bf.vtag (A.w I) (τ (fp.testOf l I (fun (x : Unit) => z) w).r) fp.mH s) (ch : List ℕ) (hch : ∀ m ∈ ch, m ≤ fp.Lc) (hlen : ch.length ≤ fp.mH) {R : ℕ} (hR1 : 1 ≤ R) (hR : R ≤ fp.Lc + 4) (Mt : fp.MaskName I) : CellPass ⋯ A.csrc A.Hsrc bf.vtag l (fp.maskOf I Mt) ((chainOp (fun (m : ℕ) => fp.cumFilt l s I m) ch) z - (mainProj A.G fp.Mc (bf.origCols l) s I R (fp.maskOf I Mt)) ((chainOp (fun (m : ℕ) => fp.cumFilt l s I m) ch) z)) (τ R * cellNorm A.G I z)

chain_passM with the target rank R, 1 ≤ R ≤ L + 4.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.far_numeric {X1 X2 X3 Sz Sa Sb τH τf τ₂ τ₃ : ℝ} (hSa : 0 ≤ Sa) (hSb : 0 ≤ Sb) (h1 : τH * X1 ≤ τ₃) (h2 : τf * X2 ≤ τ₃) (h3 : τ₂ * (X2 * X3) ≤ τ₃) : X1 * (2 * Sz) * ((τH * Sa + τH * Sa) * Sz * Sb) + (X2 * Sz * ((τf * Sz + τf * Sz) * Sa * Sb) + τ₂ * (2 * Sz) * Sb * (X2 * Sz) * (X3 * Sa)) ≤ 8 * τ₃ * Sz ^ 2 * Sa * Sb

The far step bound with canceled thresholds: if the helper threshold cancels the main expansion of the removed filter, the main threshold of the removed rank cancels the expansion of the strictly lower-rank other complement, and τ₂ absorbs the pair-mismatch budgets, the step bound is at most 8 τ₃ S_z² S_a S_b.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.leaf_farM {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (cat : Fin 4 → List (CatCol bf.Vtx)) (hT : ∀ (l : Fin 4), ∀ e ∈ cat l, ∃ R ∈ residueBox (bf.vtag e.tag).dim 9, ∃ (γ : ℝ), e = templateCol (bf.vtag e.tag) l R γ e.birth e.rank e.tag) (htag : ∀ (l : Fin 4), ∀ e ∈ cat l, bf.occAvail (↑e.tag.2) e.tag.1) {I : ℤ × ℤ} (hI : I ∈ A.cells) {a b c d : Fin 4} (hca : c ≠ a) (hcd : c ≠ d) (hcb : c ≠ b) (hda : d ≠ a) (hdb : d ≠ b) (hab : a ≠ b) {τ : ℕ → ℝ} (hpass : ∀ (l : Fin 4), l = c ∨ l = d → ∀ (w : fp.TestName I Unit), fp.MainRk w → (fp.testOf l I (fun (x : Unit) => bf.basicIn fp.Mc l I) w).Pass A.G (bf.origCols l) I A.csrc A.Hsrc bf.vtag (A.w I) (τ (fp.testOf l I (fun (x : Unit) => bf.basicIn fp.Mc l I) w).r) fp.mH (cat l)) {Bh : Type} (base : Bh → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (b₀ : Bh) {τH : ℝ} (hτH : 0 ≤ τH) (hhpass : ∀ (w : fp.HelperName I Bh), (fp.helperOf a I base w).Pass A.G (bf.origCols a) I A.csrc A.Hsrc bf.vtag (A.w I) τH fp.mH (cat a)) (x : Fin 4 → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (hxa : x a = base b₀) {v₀ : bf.Vtx} (hv₀ : v₀ ∈ bf.admT.X (bf.admAt I)) (hs₀ : fp.K.Success (fp.K.colorData (bf.admT.st (bf.admAt I)) v₀)) {jc jd : ℕ} (hjc : 1 ≤ jc) (hjc4 : jc ≤ 4) (hjd : 1 ≤ jd) (hjd4 : jd ≤ 4) (hjcd : jc ≠ jd) (t t' : List ℕ) (ht : ∀ m ∈ t, 1 ≤ m ∧ m ≤ fp.Lc) (ht' : ∀ m ∈ t', 1 ≤ m ∧ m ≤ fp.Lc) (htt' : ∀ m ∈ t, m ∉ t') (hlen : t.length + t'.length + 2 ≤ fp.mH) {τ₃ Sz : ℝ} (hτ0 : ∀ (R : ℕ), 0 ≤ τ R) (n : ℕ → ℝ) (hn : Monotone n) (hn0 : 2 * A.colBudget ≤ n 0) (hτ : ∀ (R : ℕ), 1 ≤ R → R ≤ fp.Lc + 4 → τ R * (A.colBudget * √(n (R - 1))) ≤ τ₃) (hτH' : τH * (A.colBudget * √(n (fp.Lc + 4))) ≤ τ₃) (hSz : 0 < Sz) (hSzl : ∀ (l : Fin 4), ‖bf.basicIn fp.Mc l I‖ / √(dyadicGridLength A.G I.1) ≤ Sz) (d₀ : bf.Vtx) {NH : ℝ} (hNl : ∀ (l : Fin 4), ∀ r ≤ fp.Lc + 4, ∀ (M : bf.Vtx → Prop), ↑(mainLabelsM A.G fp.Mc (bf.origCols l) (cat l) I r M d₀).card ≤ n r) (hNH : ∀ (M : bf.Vtx → Prop), ↑(mainLabelsM A.G fp.Mc (bf.origCols a) (cat a) I (fp.Lc + 5) M d₀).card ≤ NH) {τ₂ : ℝ} (hτ₂ : 0 < τ₂) (hτ₂1 : τ₂ ≤ 1) (hτ₂' : τ₂ * (A.colBudget * √(n (fp.Lc + 4)) * (A.colBudget * √NH)) ≤ τ₃) (hHed : Real.exp (↑A.Dg * (1 + Real.log A.Hsrc + Real.log τ₂⁻¹) ^ A.Dg) ≤ fp.Hed) {Sa Sb : ℝ} (hSa : 0 < Sa) (hSa' : 2 * ‖x a‖ / √(dyadicGridLength A.G I.1) ≤ Sa) (hSb : 0 < Sb) (hXb : MeasureTheory.eLpNorm (augPhys (x b)) 2 (normalizedIntervalMeasure (dyadicGridLeft A.G I.1 I.2) (dyadicGridLength A.G I.1)) ≤ ENNReal.ofReal Sb) : ‖chainDefectSel (fp.Λc I) fp.P a c d x (bf.basicIn fp.Mc c I) (bf.basicIn fp.Mc d I) (fun (p q : ℕ) => q + 2 < p ∨ p + 2 < q) (fp.mergeStepsM cat a c d (fp.Lc + 5) I (fp.slotFiltM (fp.K.grp bf.admT A.famVtxBound (bf.admAt I) v₀) jc I t) (fp.slotFiltM (fp.K.grp bf.admT A.famVtxBound (bf.admAt I) v₀) jd I t')) (x a)‖ ≤ ↑(fp.mergeStepsM cat a c d (fp.Lc + 5) I (fp.slotFiltM (fp.K.grp bf.admT A.famVtxBound (bf.admAt I) v₀) jc I t) (fp.slotFiltM (fp.K.grp bf.admT A.famVtxBound (bf.admAt I) v₀) jd I t')).length * ((↑fp.P + 1) ^ 2 * (8 * τ₃ * Sz ^ 2 * Sa * Sb))

Blueprint lines 2252-2258 ("the main source coefficient factor is canceled by the denominator in eq:catalog-test ... their fixed powers of the main and helper budgets were included before choosing τ₂. The O(P²) band pairs and the polynomial number of transfer steps are also included. Thus the far terms cost at most D^{-C₃} ‖S_a‖_{2,I} ‖S_b‖_{2,I} per cell and group") at one leaf output pair on the main columns: with the sides in the slots a, b, the whole outputs of the complement slots c, d expanded into the positive chains t, t' (distinct splits in [1, L], distinct ball levels j_c, j_d of the group of a successful present vertex), the main tests of the slots passing on the basic arguments at thresholds τ_r with τ_r D √n_{r-1} ≤ τ₃ (n bounding the main labels of rank r), the helper tests of rank L + 5 passing on the side state of the slot a at a threshold τ_H with τ_H D √n_{L+4} ≤ τ₃, and τ₂ D² √n_{L+4} √N_H ≤ τ₃, the far band defects of the rank-ordered transfer steps are at most #steps (P + 1)² 8 τ₃ S_z² S_a S_b.

The transfer at a leaf on the main columns and its far defects (blueprint lines 2240-2258)

theorem TrilinearHT.Auto.chainDefect_split {E : Type u_1} [AddCommGroup E] [Module ℂ E] (Λ : MultilinearMap ℂ (fun (x : Fin 4) => E) ℂ) (P : ℕ) (a c d : Fin 4) (x : Fin 4 → E) (yc yd : E) (sel : ℕ → ℕ → Prop) [DecidableRel sel] (steps : List (TransferStep E)) (xa : E) : chainDefect Λ P a c d x yc yd steps xa = chainDefectSel Λ P a c d x yc yd sel steps xa + chainDefectSel Λ P a c d x yc yd (fun (p q : ℕ) => ¬sel p q) steps xa

Blueprint line 2252 ("only |p - q| ≤ 2 must be retained"): the band defects split into the band pairs selected by sel and the remaining ones.

theorem TrilinearHT.Auto.posExpand_mem_length (ls : List (ℕ × Bool)) (t : ℤ × List ℕ) : t ∈ posExpand ls → t.2.length ≤ ls.length

The signed positive chains are no longer than the layer list.

theorem TrilinearHT.Auto.posExpand_mem_sub (ls : List (ℕ × Bool)) (t : ℤ × List ℕ) : t ∈ posExpand ls → ∀ m ∈ t.2, ∃ (b : Bool), (m, b) ∈ ls

The splits of a signed positive chain are splits of the layer list.

theorem TrilinearHT.Auto.searchLeaves_layers_ge (B fuel ℓ h : ℕ) (up : Fin 4) (low : Option (Fin 4)) (ls : Fin 4 → List (ℕ × Bool)) : B ≤ ℓ → (∀ (l : Fin 4), ∀ e ∈ ls l, B ≤ e.1) → ∀ L ∈ searchLeaves fuel ℓ h up low ls, ∀ (l : Fin 4), ∀ e ∈ L.layers l, B ≤ e.1

The layers of the guarded search only split at colors at least the initial lower end.

theorem TrilinearHT.Auto.leafAt_layers_ge {fuel Lc : ℕ} {up₀ : Fin 4} (s : ℕ) (l : Fin 4) (e : ℕ × Bool) : e ∈ (leafAt fuel Lc up₀ s).layers l → 1 ≤ e.1

The cumulative splits of the leaves are colors at least one.

theorem TrilinearHT.Auto.role_ne_aux (up : Fin 4) (low : Option (Fin 4)) (l l' : Fin 4) : l ≠ l' → (if l = thirdSlot up low then 1 else if l = up then 2 else if l = (otherTwo up (thirdSlot up low)).1 then 3 else 4) ≠ if l' = thirdSlot up low then 1 else if l' = up then 2 else if l' = (otherTwo up (thirdSlot up low)).1 then 3 else 4

theorem TrilinearHT.Auto.SearchLeaf.role_injective (L : SearchLeaf) {l l' : Fin 4} (h : l ≠ l') : L.role l ≠ L.role l'

Blueprint line 2241 ("the four ball ranks are distinct"): distinct slots of a leaf have distinct ball levels.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.leaf_transferM {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (cat : Fin 4 → List (CatCol bf.Vtx)) (Lf : SearchLeaf) {a c d : Fin 4} (hac : a ≠ c) (had : a ≠ d) (hcd : c ≠ d) (G : bf.Grp) (I : ℤ × ℤ) (x : Fin 4 → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) : (fp.Λc I) (Function.update (Function.update x c ((fp.ballFilt c (cat c) I G (Lf.role c)) ((layerOp (fun (m : ℕ) => fp.cumFilt c (cat c) I m) (Lf.layers c)) (bf.basicIn fp.Mc c I)))) d ((fp.ballFilt d (cat d) I G (Lf.role d)) ((layerOp (fun (m : ℕ) => fp.cumFilt d (cat d) I m) (Lf.layers d)) (bf.basicIn fp.Mc d I)))) = (List.map (fun (t' : ℤ × List ℕ) => (List.map (fun (t : ℤ × List ℕ) => ↑t.1 * ↑t'.1 * ((fp.Λc I) (Function.update (Function.update (Function.update x c (bf.basicIn fp.Mc c I)) d (bf.basicIn fp.Mc d I)) a (chainSide fp.P (fp.mergeStepsM cat a c d (fp.Lc + 5) I (fp.slotFiltM G (Lf.role c) I t.2) (fp.slotFiltM G (Lf.role d) I t'.2)) (x a))) + chainDefect (fp.Λc I) fp.P a c d x (bf.basicIn fp.Mc c I) (bf.basicIn fp.Mc d I) (fp.mergeStepsM cat a c d (fp.Lc + 5) I (fp.slotFiltM G (Lf.role c) I t.2) (fp.slotFiltM G (Lf.role d) I t'.2)) (x a))) (posExpand (Lf.layers c).reverse)).sum) (posExpand (Lf.layers d).reverse)).sum

Blueprint lines 2240-2252 (transfer and its paired defects) at a leaf, a cell and a group on the main columns: with sides in the slots a, b and whole leaf outputs (the ball filter of the role level after the layered cumulative history of the basic input) in the slots c, d, the form is the signed sum over the pairs of positive chains of the two complement histories of the transferred main term (helper averages of rank L + 5 on the side a, the basic inputs in c, d) plus the band defects of the rank-ordered steps.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.leaf_far_search {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (cat : Fin 4 → List (CatCol bf.Vtx)) (hT : ∀ (l : Fin 4), ∀ e ∈ cat l, ∃ R ∈ residueBox (bf.vtag e.tag).dim 9, ∃ (γ : ℝ), e = templateCol (bf.vtag e.tag) l R γ e.birth e.rank e.tag) (htag : ∀ (l : Fin 4), ∀ e ∈ cat l, bf.occAvail (↑e.tag.2) e.tag.1) {I : ℤ × ℤ} (hI : I ∈ A.cells) {a b c d : Fin 4} (hca : c ≠ a) (hcd : c ≠ d) (hcb : c ≠ b) (hda : d ≠ a) (hdb : d ≠ b) (hab : a ≠ b) {τ : ℕ → ℝ} (hpass : ∀ (l : Fin 4), l = c ∨ l = d → ∀ (w : fp.TestName I Unit), fp.MainRk w → (fp.testOf l I (fun (x : Unit) => bf.basicIn fp.Mc l I) w).Pass A.G (bf.origCols l) I A.csrc A.Hsrc bf.vtag (A.w I) (τ (fp.testOf l I (fun (x : Unit) => bf.basicIn fp.Mc l I) w).r) fp.mH (cat l)) {Bh : Type} (base : Bh → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (b₀ : Bh) {τH : ℝ} (hτH : 0 ≤ τH) (hhpass : ∀ (w : fp.HelperName I Bh), (fp.helperOf a I base w).Pass A.G (bf.origCols a) I A.csrc A.Hsrc bf.vtag (A.w I) τH fp.mH (cat a)) (x : Fin 4 → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (hxa : x a = base b₀) {v₀ : bf.Vtx} (hv₀ : v₀ ∈ bf.admT.X (bf.admAt I)) (hs₀ : fp.K.Success (fp.K.colorData (bf.admT.st (bf.admAt I)) v₀)) {fuel : ℕ} {up₀ : Fin 4} (s : ℕ) (hmH : 2 * fuel + 2 ≤ fp.mH) {t t' : ℤ × List ℕ} (ht : t ∈ posExpand ((leafAt fuel fp.Lc up₀ s).layers c).reverse) (ht' : t' ∈ posExpand ((leafAt fuel fp.Lc up₀ s).layers d).reverse) {τ₃ Sz : ℝ} (hτ0 : ∀ (R : ℕ), 0 ≤ τ R) (n : ℕ → ℝ) (hn : Monotone n) (hn0 : 2 * A.colBudget ≤ n 0) (hτ : ∀ (R : ℕ), 1 ≤ R → R ≤ fp.Lc + 4 → τ R * (A.colBudget * √(n (R - 1))) ≤ τ₃) (hτH' : τH * (A.colBudget * √(n (fp.Lc + 4))) ≤ τ₃) (hSz : 0 < Sz) (hSzl : ∀ (l : Fin 4), ‖bf.basicIn fp.Mc l I‖ / √(dyadicGridLength A.G I.1) ≤ Sz) (d₀ : bf.Vtx) {NH : ℝ} (hNl : ∀ (l : Fin 4), ∀ r ≤ fp.Lc + 4, ∀ (M : bf.Vtx → Prop), ↑(mainLabelsM A.G fp.Mc (bf.origCols l) (cat l) I r M d₀).card ≤ n r) (hNH : ∀ (M : bf.Vtx → Prop), ↑(mainLabelsM A.G fp.Mc (bf.origCols a) (cat a) I (fp.Lc + 5) M d₀).card ≤ NH) {τ₂ : ℝ} (hτ₂ : 0 < τ₂) (hτ₂1 : τ₂ ≤ 1) (hτ₂' : τ₂ * (A.colBudget * √(n (fp.Lc + 4)) * (A.colBudget * √NH)) ≤ τ₃) (hHed : Real.exp (↑A.Dg * (1 + Real.log A.Hsrc + Real.log τ₂⁻¹) ^ A.Dg) ≤ fp.Hed) {Sa Sb : ℝ} (hSa : 0 < Sa) (hSa' : 2 * ‖x a‖ / √(dyadicGridLength A.G I.1) ≤ Sa) (hSb : 0 < Sb) (hXb : MeasureTheory.eLpNorm (augPhys (x b)) 2 (normalizedIntervalMeasure (dyadicGridLeft A.G I.1 I.2) (dyadicGridLength A.G I.1)) ≤ ENNReal.ofReal Sb) : ‖chainDefectSel (fp.Λc I) fp.P a c d x (bf.basicIn fp.Mc c I) (bf.basicIn fp.Mc d I) (fun (p q : ℕ) => q + 2 < p ∨ p + 2 < q) (fp.mergeStepsM cat a c d (fp.Lc + 5) I (fp.slotFiltM (fp.K.grp bf.admT A.famVtxBound (bf.admAt I) v₀) ((leafAt fuel fp.Lc up₀ s).role c) I t.2) (fp.slotFiltM (fp.K.grp bf.admT A.famVtxBound (bf.admAt I) v₀) ((leafAt fuel fp.Lc up₀ s).role d) I t'.2)) (x a)‖ ≤ ↑(fp.mergeStepsM cat a c d (fp.Lc + 5) I (fp.slotFiltM (fp.K.grp bf.admT A.famVtxBound (bf.admAt I) v₀) ((leafAt fuel fp.Lc up₀ s).role c) I t.2) (fp.slotFiltM (fp.K.grp bf.admT A.famVtxBound (bf.admAt I) v₀) ((leafAt fuel fp.Lc up₀ s).role d) I t'.2)).length * ((↑fp.P + 1) ^ 2 * (8 * τ₃ * Sz ^ 2 * Sa * Sb))

Blueprint lines 2252-2258 at a leaf of the guarded search on the main columns: for every pair of signed positive chains of the complement histories of the slots c, d (in the transfer identity leaf_transferM) and every group of a successful present vertex, the far band defects of the rank-ordered transfer steps are at most #steps (P + 1)² 8 τ₃ S_z² S_a S_b (the chain conditions of leaf_farM hold at the leaves: splits in [1, L], distinct across slots, distinct ball levels, histories within the main budget).

The transferred main term and its restoration on the main columns (lines 2256-2263)

theorem TrilinearHT.Auto.augPhys_cellLp_gen {V : Type u_1} [Fintype V] {G : RealDyadicGrid} {I : ℤ × ℤ} {f : ℝ → ℂ} (hf : MeasureTheory.MemLp f 2 (normalizedIntervalMeasure (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1))) : ∀ᵐ (y : ℝ), y ∈ dyadicGridCell G I.1 I.2 → augPhys (physicalColumnInput (cellLp G I f)) y = f y

The physical part of the augmented cell input is the function on the cell, in any column space.

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.Ucol {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} (bf : A.BasicFamilies) (Mc : ℕ) (l : Fin 4) (I : ℤ × ℤ) : ↥(ColumnL2 (bf.Lab ⊕ Fin Mc))

The basic side U_l of the slot l on the cell I in the main columns (blueprint prop:base, Y_l = B_l + U_l with U_i = U_j = 0).

Equations

• bf.Ucol Mc l I = TrilinearHT.Auto.physicalColumnInput (TrilinearHT.Auto.cellLp A.G I (if l = A.a ∨ l = A.b then A.U l I else 0))

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.basicIn_add_Ucol {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} (bf : A.BasicFamilies) (Mc : ℕ) (l : Fin 4) {I : ℤ × ℤ} (hI : I ∈ A.cells) : ∀ᵐ (y : ℝ), y ∈ dyadicGridCell A.G I.1 I.2 → augPhys (bf.basicIn Mc l I + bf.Ucol Mc l I) y = A.Y I l y

On an active cell the basic input plus the basic side is the full argument Y_l of eq:Y (blueprint lines 1609-1623: "the whole complementary B arguments restore to the full pair by adding basic sides U").

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.mergeStepsM_length {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (cat : Fin 4 → List (CatCol bf.Vtx)) (a c d : Fin 4) (rH : ℕ) (I : ℤ × ℤ) (xs ys : List (ℕ × (Fin fp.P → bf.Vtx → Prop))) : (fp.mergeStepsM cat a c d rH I xs ys).length = xs.length + ys.length

The number of merged transfer steps is the total number of filters.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.leaf_transferred_mainM {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (cat : Fin 4 → List (CatCol bf.Vtx)) (Lf : SearchLeaf) {a c d : Fin 4} (hac : a ≠ c) (had : a ≠ d) (hcd : c ≠ d) (G : bf.Grp) (I : ℤ × ℤ) (x : Fin 4 → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) : (fp.Λc I) (Function.update (Function.update x c ((fp.ballFilt c (cat c) I G (Lf.role c)) ((layerOp (fun (m : ℕ) => fp.cumFilt c (cat c) I m) (Lf.layers c)) (bf.basicIn fp.Mc c I)))) d ((fp.ballFilt d (cat d) I G (Lf.role d)) ((layerOp (fun (m : ℕ) => fp.cumFilt d (cat d) I m) (Lf.layers d)) (bf.basicIn fp.Mc d I)))) = (List.map (fun (t' : ℤ × List ℕ) => (List.map (fun (t : ℤ × List ℕ) => ↑t.1 * ↑t'.1 * ((fp.Λc I) (Function.update (Function.update (Function.update x a (chainSide fp.P (fp.mergeStepsM cat a c d (fp.Lc + 5) I (fp.slotFiltM G (Lf.role c) I t.2) (fp.slotFiltM G (Lf.role d) I t'.2)) (x a))) c (bf.basicIn fp.Mc c I + bf.Ucol fp.Mc c I)) d (bf.basicIn fp.Mc d I + bf.Ucol fp.Mc d I)) - ((fp.Λc I) (Function.update (Function.update (Function.update x a (chainSide fp.P (fp.mergeStepsM cat a c d (fp.Lc + 5) I (fp.slotFiltM G (Lf.role c) I t.2) (fp.slotFiltM G (Lf.role d) I t'.2)) (x a))) c (bf.Ucol fp.Mc c I)) d (bf.basicIn fp.Mc d I)) + (fp.Λc I) (Function.update (Function.update (Function.update x a (chainSide fp.P (fp.mergeStepsM cat a c d (fp.Lc + 5) I (fp.slotFiltM G (Lf.role c) I t.2) (fp.slotFiltM G (Lf.role d) I t'.2)) (x a))) c (bf.basicIn fp.Mc c I)) d (bf.Ucol fp.Mc d I)) + (fp.Λc I) (Function.update (Function.update (Function.update x a (chainSide fp.P (fp.mergeStepsM cat a c d (fp.Lc + 5) I (fp.slotFiltM G (Lf.role c) I t.2) (fp.slotFiltM G (Lf.role d) I t'.2)) (x a))) c (bf.Ucol fp.Mc c I)) d (bf.Ucol fp.Mc d I))) + chainDefect (fp.Λc I) fp.P a c d x (bf.basicIn fp.Mc c I) (bf.basicIn fp.Mc d I) (fp.mergeStepsM cat a c d (fp.Lc + 5) I (fp.slotFiltM G (Lf.role c) I t.2) (fp.slotFiltM G (Lf.role d) I t'.2)) (x a))) (posExpand (Lf.layers c).reverse)).sum) (posExpand (Lf.layers d).reverse)).sum

Blueprint lines 2256-2263 (eq:transferred-main) at a leaf, a cell and a group on the main columns: forwarding the transferred main term and retaining its defects, the form of the sides x_a, x_b and the whole leaf outputs in the slots c, d is the signed sum over the pairs of positive chains of H_I(D_{a,s} x_a, x_b, Y_c, Y_d) minus the three restoration corrections, each with an additional basic side U (Ucol), plus the band defects. Here D_{a,s} is the product of the helper averages of the merged steps (chainSide_mergeStepsM_eq, at most 2 fuel + 2 factors by leaf_steps_le), and B_l + U_l is the full argument Y_l on the cell (basicIn_add_Ucol).