Trilinear Hilbert transform: C3v_budget

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideLeafM.C3v_budget {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (T : fp.SideLeafM) (S : Finset (ℤ × ℤ)) (hS : S ⊆ A.cells) (gs : ℤ × ℤ → Finset bf.Grp) (gset : Finset bf.Grp) (hgs : ∀ I ∈ S, gs I ⊆ gset) (G₀ : bf.Grp) (Sc : Finset (ℤ × ℤ)) (hSc : ∀ I ∈ S, ∀ J ∈ A.cells, dyadicGridCell A.G I.1 I.2 ⊆ dyadicGridCell A.G J.1 J.2 → A.blkStart T.K I.1 ≤ J.1 → J ∈ Sc) (ScG : bf.Grp → Finset (ℤ × ℤ)) (hScG : ∀ I ∈ S, ∀ G ∈ gs I, ∀ J ∈ A.cells, dyadicGridCell A.G I.1 I.2 ⊆ dyadicGridCell A.G J.1 J.2 → A.blkStart T.K I.1 ≤ J.1 → J ∈ ScG G) {Lp Jm : ℕ} (hLp : ∀ (l : Fin 4), (T.pe l).length ≤ Lp) (hJm : ∀ (c d : Fin 4) (i i' : ℕ), (T.desc c d (T.tOf c i) (T.tOf d i')).length ≤ Jm) {C₀ B₀ Cy : ℝ} (hC₀ : 0 < C₀) (hy : ∀ I ∈ S, ∀ (l : Fin 4), T.u ≠ some l → ‖bf.basicIn fp.Mc l I‖ / √(dyadicGridLength A.G I.1) ≤ Cy ∧ ‖bf.Ucol fp.Mc l I‖ / √(dyadicGridLength A.G I.1) ≤ Cy) {Bs BU Eb : ℝ} (hEb : 0 ≤ Eb) (hBs : ∑ I ∈ S, ∑ G ∈ gs I, ∑ l : Fin 4, ‖T.sv l G I‖ ^ 2 ≤ Bs) (hBU : ∑ I ∈ S, ∑ l : Fin 4, ‖bf.Ucol fp.Mc l I‖ ^ 2 ≤ BU) (hEi : ∀ (a c d : Fin 4) (i i' j : ℕ), j < (T.desc c d (T.tOf c i) (T.tOf d i')).length → ∑ J ∈ Sc, T.iYe a c d G₀ (T.tOf c i) (T.tOf d i') j J ≤ Eb) (hEp : ∀ (a c d : Fin 4) (i i' j : ℕ), j < (T.desc c d (T.tOf c i) (T.tOf d i')).length → T.cumY c d (T.tOf c i) (T.tOf d i') j → ∑ J ∈ Sc, T.pYe a c d G₀ (T.tOf c i) (T.tOf d i') j J ≤ ↑fp.P * Eb) (hEF : ∀ (a c d : Fin 4) (i i' j : ℕ), j < (T.desc c d (T.tOf c i) (T.tOf d i')).length → T.cumF c d (T.tOf c i) (T.tOf d i') j → ∑ J ∈ Sc, T.dFe a c d G₀ (T.tOf c i) (T.tOf d i') j J ≤ Eb) (hEpG : ∀ (a c d : Fin 4) (i i' j : ℕ), j < (T.desc c d (T.tOf c i) (T.tOf d i')).length → ¬T.cumY c d (T.tOf c i) (T.tOf d i') j → ∑ G ∈ gset, ∑ J ∈ ScG G, T.pYe a c d G (T.tOf c i) (T.tOf d i') j J ≤ ↑fp.P * Eb) (hEFG : ∀ (a c d : Fin 4) (i i' j : ℕ), j < (T.desc c d (T.tOf c i) (T.tOf d i')).length → ¬T.cumF c d (T.tOf c i) (T.tOf d i') j → ∑ G ∈ gset, ∑ J ∈ ScG G, T.dFe a c d G (T.tOf c i) (T.tOf d i') j J ≤ Eb) : ∑ I ∈ S, dyadicGridLength A.G I.1 * T.C3v C₀ B₀ G₀ gs I ^ 2 ≤ 2 * (36 * 256 * 256 * (↑Lp ^ 2 * (2 * (1 + 5 * ↑Jm)) * (↑Lp ^ 2 * (localFormUniformConstant κ' ^ 2 * (8 * Cy ^ 2 * BU)) + (2 / ↑fp.P * localFormUniformConstant κ') ^ 2 * 6 * (↑Lp * ↑Lp * (↑Jm * 5) * T.frzB C₀ Eb)))) + 2 * (36 * 256 * 256 * (2 * (localFormUniformConstant κ' * B₀) ^ 2 * Bs + ↑Lp ^ 2 * (2 * (1 + 5 * ↑Jm)) * ((2 / ↑fp.P * localFormUniformConstant κ') ^ 2 * 6 * (↑Lp * ↑Lp * (↑Jm * 5) * T.frzB C₀ Eb))))

Blueprint lines 2375-2394 (the third strong factors in integrated form, shared histories counted once): the length-weighted squares of the cell values C₃ of the third strong factors are bounded by the U energy B_U of the cells (counted once, not per group), the side masses B_s, and the freeze budgets frzB of the steps, which come from the freeze energies of the shared outputs (over the ancestors S_c of the uses) and the joint freeze energies of the group-indexed outputs (over the ancestors S_G of the uses of each group).

The 2+2 patterns of a leaf (blueprint lines 2446-2456)

theorem TrilinearHT.Auto.min_add_le_add_min {η a b : ℝ} (ha : 0 ≤ a) : min η (a + b) ≤ a + min η b

min(η, A + B) ≤ A + min(η, B) for A ≥ 0.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideLeafM.ns_mul_le_s2 {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (T : fp.SideLeafM) {a b : Fin 4} (hab : a ≠ b) (G : bf.Grp) (I : ℤ × ℤ) : T.ns a G I * T.ns b G I ≤ T.s2 G I

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideLeafM.absPart'_nonneg {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (T : fp.SideLeafM) (C₀ τ cF : ℝ) (hτ : 0 ≤ τ) (hcF : 0 ≤ cF) (a b c d : Fin 4) (G : bf.Grp) (I : ℤ × ℤ) : 0 ≤ T.absPart' C₀ τ cF a b c d G I

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideLeafM.two_two_leafM {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (T : fp.SideLeafM) (S : Finset (ℤ × ℤ)) (hS : S ⊆ A.cells) (hroot : ∀ I ∈ S, dyadicGridCell A.G I.1 I.2 ⊆ dyadicGridCell A.G A.R.1 A.R.2) (gs : ℤ × ℤ → Finset bf.Grp) {τ cF C₀ B₀ : ℝ} (hτ : 0 ≤ τ) (hcF : 0 ≤ cF) (hC₀ : 0 ≤ C₀) (hB₀ : 0 ≤ B₀) (hpair : ∀ I ∈ S, ∀ (c d : Fin 4), c ≠ d → T.u ≠ some c → T.u ≠ some d → PairSmall (dyadicGridLeft A.G I.1 I.2) (dyadicGridLength A.G I.1) (A.w I) c d (A.Y I c) (A.Y I d) τ) (hfar : ∀ I ∈ S, ∀ G ∈ gs I, ∀ (a b c d : Fin 4), T.Val a b c d → ¬T.Ucase c d → ∀ t ∈ T.pe c, ∀ t' ∈ T.pe d, ‖chainDefectSel (fp.Λc I) fp.P a c d (fun (l : Fin 4) => T.sv l G I) (bf.basicIn fp.Mc c I) (bf.basicIn fp.Mc d I) (fun (p q : ℕ) => q + 2 < p ∨ p + 2 < q) (fp.mergeStepsM T.cat a c d (fp.Lc + 5) I (fp.slotFiltM G (T.Lf.role c) I t.2) (fp.slotFiltM G (T.Lf.role d) I t'.2)) (T.sv a G I)‖ ≤ cF * T.ns a G I * T.ns b G I) (hsc : ∀ I ∈ S, ∀ (l : Fin 4), T.u ≠ some l → ‖bf.basicIn fp.Mc l I‖ ≤ C₀ * √(dyadicGridLength A.G I.1)) (hout : ∀ I ∈ S, ∀ G ∈ gs I, ∀ (l : Fin 4), ‖T.out l G I‖ ≤ B₀ * √(dyadicGridLength A.G I.1)) {Ts Cc : ℝ} (hTs : ∀ (x : ℝ), ∑ I ∈ S with x ∈ dyadicGridCell A.G I.1 I.2, ∑ G ∈ gs I, T.s2 G I ≤ Ts) (C3 : ℤ × ℤ → ℝ) (hC3 : ∀ I ∈ S, ∀ G ∈ gs I, 6 * ∑ a : Fin 4, ∑ b : Fin 4, ∑ c : Fin 4, ∑ d : Fin 4, T.third C₀ B₀ a b c d G I ≤ C3 I) (hCc : ∀ (x : ℝ), ∑ I ∈ S with x ∈ dyadicGridCell A.G I.1 I.2, C3 I ^ 2 ≤ Cc) {η p : ℝ} (hη : 0 ≤ η) (hp : 2 / 3 < p) (hp1 : p ≤ 1) : ∑ I ∈ S, dyadicGridLength A.G I.1 * min η ‖∑ σ : Fin 4 → Fin 3 with (∀ (l : Fin 4), σ l ≠ 2) ∧ {l : Fin 4 | σ l = 0}.card = 2 ∧ {l : Fin 4 | σ l = 1}.card = 2, ∑ G ∈ gs I, (fp.Λc I) fun (l : Fin 4) => if σ l = 0 then T.out l G I else T.sv l G I‖ ≤ ∑ I ∈ S, dyadicGridLength A.G I.1 * (6 * ∑ G ∈ gs I, ∑ a : Fin 4, ∑ b : Fin 4, ∑ c : Fin 4, ∑ d : Fin 4, T.absPart' C₀ τ cF a b c d G I) + η ^ (1 - p) * (Ts ^ (p / 2) * Ts ^ (p / 2) * Cc ^ (p / 2) * dyadicGridLength A.G A.R.1)

Blueprint lines 2375-2382 and 2446-2456 on one localization leaf, on the main columns: with the pair-small restored complements, the far bound, current complement bounds C₀, whole outputs bounded by B₀, the side path cap T_s, and a cell value C₃ of the third strong factors bounding the third factor of every group at the cell ("a third factor is shared or bounded by its group square sum") with path cap C_c, the weighted active minimum of the restored 2+2 patterns is at most the weighted absolute parts plus η^{1-p} T_s^p C_c^{p/2} |R|.

The two-side estimate of a leaf (blueprint lines 2425-2456)

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideLeafM.abs_sum_leM {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (T : fp.SideLeafM) (S : Finset (ℤ × ℤ)) (hroot : ∀ I ∈ S, dyadicGridCell A.G I.1 I.2 ⊆ dyadicGridCell A.G A.R.1 A.R.2) (gs : ℤ × ℤ → Finset bf.Grp) {C₀ τ cF Np Ts : ℝ} (hτ : 0 ≤ τ) (hcF : 0 ≤ cF) (hNp : ∀ (c d : Fin 4), ↑(T.pe d).length * ↑(T.pe c).length ≤ Np) (hTs : ∀ (x : ℝ), ∑ I ∈ S with x ∈ dyadicGridCell A.G I.1 I.2, ∑ G ∈ gs I, T.s2 G I ≤ Ts) : ∑ I ∈ S, dyadicGridLength A.G I.1 * (6 * ∑ G ∈ gs I, ∑ a : Fin 4, ∑ b : Fin 4, ∑ c : Fin 4, ∑ d : Fin 4, T.absPart' C₀ τ cF a b c d G I) ≤ 6 * 256 * Np * (τ + cF) * Ts * dyadicGridLength A.G A.R.1 + 6 * ∑ I ∈ S, dyadicGridLength A.G I.1 * ∑ G ∈ gs I, ∑ a : Fin 4, ∑ b : Fin 4, ∑ c : Fin 4, ∑ d : Fin 4, if T.Val a b c d ∧ ¬T.Ucase c d then T.nearAbs C₀ a b c d G I else 0

Blueprint line 2384 (pair-small main terms and far terms, absolute): the weighted absolute parts of a leaf are at most 6 · 256 N_p (τ + c_F) T_s |R| plus the weighted near parts, where N_p bounds the numbers of pairs of positive chains and T_s is the side path cap.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideLeafM.len_s2 {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (T : fp.SideLeafM) (G : bf.Grp) (I : ℤ × ℤ) : dyadicGridLength A.G I.1 * T.s2 G I = ∑ l : Fin 4, ‖T.sv l G I‖ ^ 2

The side mass of a cell and group, weighted by its length, is the sum of the squared sides.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideLeafM.leaf_two_two_boundM {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (T : fp.SideLeafM) {q : ℝ} (hq2 : 2 < q) (hq3 : q < 3) (hanc : A.AncClosed) {Nd N : ℕ} (hKNd : A.DepthWin Nd) (hKN : T.K ≤ 2 ^ N) (S : Finset (ℤ × ℤ)) (hS : S ⊆ A.cells) (hroot : ∀ I ∈ S, dyadicGridCell A.G I.1 I.2 ⊆ dyadicGridCell A.G A.R.1 A.R.2) (gs : ℤ × ℤ → Finset bf.Grp) (gset : Finset bf.Grp) (hgs : ∀ I ∈ S, gs I ⊆ gset) (Lp Jm Bn k : ℕ) (hBn : ∀ I ∈ S, T.bk I < Bn) (hLp : ∀ (l : Fin 4), (T.pe l).length ≤ Lp) (hJm : ∀ (c d : Fin 4) (i i' : ℕ), (T.desc c d (T.tOf c i) (T.tOf d i')).length ≤ Jm) (Act : Finset (ℤ × ℤ)) (hact : ∀ I ∈ S, I ∈ Act ∧ ∀ G ∈ gs I, G ∈ fp.groupsAt I k) {Mp : ℝ} (hMp : ∀ (y : ℝ), ↑{c ∈ Act | y ∈ dyadicGridCell A.G c.1 c.2}.card ≤ Mp) (okZ : Fin 4 → bf.Grp → ℤ × ℤ → Prop) (BZ EW : Fin 4 → ℝ) (hcap : ∀ (l : Fin 4), T.u ≠ some l → A.VarCap gset (T.Z l) (okZ l) (BZ l)) (hok : ∀ (l : Fin 4), T.u ≠ some l → ∀ I ∈ S, ∀ G ∈ gs I, ∀ J ∈ A.cells, dyadicGridCell A.G I.1 I.2 ⊆ dyadicGridCell A.G J.1 J.2 → okZ l G J) (hEW : ∀ (l : Fin 4), T.u ≠ some l → ∑ G ∈ gset, ∑ β ∈ Finset.range Bn, ‖(columnL2Restriction (⋃ J ∈ Finset.image (fun (I : ℤ × ℤ) => ancAt A.G I (A.R.1 + ↑(T.K * β))) ({I ∈ S | G ∈ gs I ∧ T.bk I = β}), dyadicGridCell A.G J.1 J.2) ⋯) (T.Wb l G (A.R.1 + ↑(T.K * β)))‖ ^ 2 ≤ EW l) {EU : ℝ} (hEU : ∀ (l : Fin 4), T.u = some l → ∑ I ∈ S, ∑ G ∈ gs I, ‖(columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯) (T.sv l G I)‖ ^ 2 ≤ EU) {τ cF C₀ B₀ : ℝ} (hτ : 0 ≤ τ) (hcF : 0 ≤ cF) (hC₀ : 0 ≤ C₀) (hB₀ : 0 ≤ B₀) (hpair : ∀ I ∈ S, ∀ (c d : Fin 4), c ≠ d → T.u ≠ some c → T.u ≠ some d → PairSmall (dyadicGridLeft A.G I.1 I.2) (dyadicGridLength A.G I.1) (A.w I) c d (A.Y I c) (A.Y I d) τ) (hfar : ∀ I ∈ S, ∀ G ∈ gs I, ∀ (a b c d : Fin 4), T.Val a b c d → ¬T.Ucase c d → ∀ t ∈ T.pe c, ∀ t' ∈ T.pe d, ‖chainDefectSel (fp.Λc I) fp.P a c d (fun (l : Fin 4) => T.sv l G I) (bf.basicIn fp.Mc c I) (bf.basicIn fp.Mc d I) (fun (p q : ℕ) => q + 2 < p ∨ p + 2 < q) (fp.mergeStepsM T.cat a c d (fp.Lc + 5) I (fp.slotFiltM G (T.Lf.role c) I t.2) (fp.slotFiltM G (T.Lf.role d) I t'.2)) (T.sv a G I)‖ ≤ cF * T.ns a G I * T.ns b G I) (hsc : ∀ I ∈ S, ∀ (l : Fin 4), T.u ≠ some l → ‖bf.basicIn fp.Mc l I‖ ≤ C₀ * √(dyadicGridLength A.G I.1)) (hout : ∀ I ∈ S, ∀ G ∈ gs I, ∀ (l : Fin 4), ‖T.out l G I‖ ≤ B₀ * √(dyadicGridLength A.G I.1)) {Np : ℝ} (hNp : ∀ (c d : Fin 4), ↑(T.pe d).length * ↑(T.pe c).length ≤ Np) {Bs B3 : ℝ} (hBs : ∑ I ∈ S, ∑ G ∈ gs I, ∑ l : Fin 4, ‖T.sv l G I‖ ^ 2 ≤ Bs) (C3 : ℤ × ℤ → ℝ) (hC3 : ∀ I ∈ S, ∀ G ∈ gs I, 6 * ∑ a : Fin 4, ∑ b : Fin 4, ∑ c : Fin 4, ∑ d : Fin 4, T.third C₀ B₀ a b c d G I ≤ C3 I) (hB3 : ∑ I ∈ S, dyadicGridLength A.G I.1 * C3 I ^ 2 ≤ B3) (hP : 1 ≤ fp.P) (Γa Γb : Fin 4 → ℝ) (ΓU : ℝ) (hΓa : ∀ (a : Fin 4), T.u ≠ some a → fp.stackEA (nOs Lp Jm) (T.cat a) (T.mbs a) T.Dpre N (BZ a) (EW a) ≤ (↑fp.P + 2) * Γa a * dyadicGridLength A.G A.R.1) (hΓb : ∀ (b : Fin 4), T.u ≠ some b → ↑(nOs Lp Jm).card * (↑N * BZ b + EW b) ≤ Γb b * dyadicGridLength A.G A.R.1) (hΓU : ↑(nOs Lp Jm).card * EU ≤ ΓU * dyadicGridLength A.G A.R.1) {η p ρ : ℝ} (hη : 0 ≤ η) (hp : 2 / 3 < p) (hp1 : p ≤ 1) (hρ : 0 < ρ) (hρ1 : ρ < 1) : ∃ C ⊆ A.cells, dyadicRootLength A.G (maximalDyadicCells A.G C) ≤ 2 * ρ * dyadicGridLength A.G A.R.1 ∧ ∑ I ∈ S with ¬∃ e ∈ C, dyadicGridCell A.G I.1 I.2 ⊆ dyadicGridCell A.G e.1 e.2, dyadicGridLength A.G I.1 * min η ‖∑ σ : Fin 4 → Fin 3 with (∀ (l : Fin 4), σ l ≠ 2) ∧ {l : Fin 4 | σ l = 0}.card = 2 ∧ {l : Fin 4 | σ l = 1}.card = 2, ∑ G ∈ gs I, (fp.Λc I) fun (l : Fin 4) => if σ l = 0 then T.out l G I else T.sv l G I‖ ≤ 6 * 256 * Np * (τ + cF) * ((Bs / dyadicGridLength A.G A.R.1 + B3 / dyadicGridLength A.G A.R.1) / ρ) * dyadicGridLength A.G A.R.1 + 6 * ∑ a : Fin 4, ∑ b : Fin 4, ∑ e : Fin 4, T.nearBnd hq2 hq3 Nd N Lp Jm Mp C₀ (ρ / 64) Γa Γb ΓU a b e + η ^ (1 - p) * (((Bs / dyadicGridLength A.G A.R.1 + B3 / dyadicGridLength A.G A.R.1) / ρ) ^ (p / 2) * ((Bs / dyadicGridLength A.G A.R.1 + B3 / dyadicGridLength A.G A.R.1) / ρ) ^ (p / 2) * ((Bs / dyadicGridLength A.G A.R.1 + B3 / dyadicGridLength A.G A.R.1) / ρ) ^ (p / 2) * dyadicGridLength A.G A.R.1) ∧ ∀ (x : ℝ), ∑ I ∈ {I ∈ S | ¬∃ e ∈ C, dyadicGridCell A.G I.1 I.2 ⊆ dyadicGridCell A.G e.1 e.2} with x ∈ dyadicGridCell A.G I.1 I.2, ∑ G ∈ gs I, T.s2 G I ≤ (Bs / dyadicGridLength A.G A.R.1 + B3 / dyadicGridLength A.G A.R.1) / ρ

Blueprint lines 2425-2456, the two-side estimate of one localization leaf on the main columns: one cut family of root fraction at most 2ρ such that on the retained cells the weighted active minimum of the restored 2+2 patterns is at most the pair-small and far absolute bound 6·256 N_p (τ + c_F) T_c |R|, six times the critical near-band bounds nearBnd of the slot triples (eq:near-band), and the power cost η^{1-p} T_c^{3p/2} |R| of the three strong factors, with the joint path cap T_c = (B_s + B_3)/(ρ |R|) of the side mass B_s and the integrated budget B_3 of a cell value C₃ bounding the third strong factors of all groups at the cell.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideLeafM.frz_shared {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (T : fp.SideLeafM) {Z : bf.Grp → ℤ → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))} (G₀ : bf.Grp) {B : ℝ} (hcap : A.VarCap {G₀} Z (fun (x : bf.Grp) (x_1 : ℤ × ℤ) => True) B) (Sc : Finset (ℤ × ℤ)) (hSc : Sc ⊆ A.cells) : ∑ J ∈ Sc, ‖(columnL2Restriction (dyadicGridCell A.G J.1 J.2) ⋯) (Z G₀ J.1 - Z G₀ (A.blkStart T.K J.1))‖ ^ 2 ≤ ↑T.K * B

The freeze energy of a shared output over certified ancestors from its variation capacity.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideLeafM.C3v_budget_cap {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (T : fp.SideLeafM) (S : Finset (ℤ × ℤ)) (hS : S ⊆ A.cells) (gs : ℤ × ℤ → Finset bf.Grp) (gset : Finset bf.Grp) (hgs : ∀ I ∈ S, gs I ⊆ gset) (G₀ : bf.Grp) (Sc : Finset (ℤ × ℤ)) (hScc : Sc ⊆ A.cells) (hSc : ∀ I ∈ S, ∀ J ∈ A.cells, dyadicGridCell A.G I.1 I.2 ⊆ dyadicGridCell A.G J.1 J.2 → A.blkStart T.K I.1 ≤ J.1 → J ∈ Sc) (ScG : bf.Grp → Finset (ℤ × ℤ)) (ok : bf.Grp → ℤ × ℤ → Prop) (hScGc : ∀ G ∈ gset, ∀ J ∈ ScG G, J ∈ A.cells ∧ ok G J) (hScG : ∀ I ∈ S, ∀ G ∈ gs I, ∀ J ∈ A.cells, dyadicGridCell A.G I.1 I.2 ⊆ dyadicGridCell A.G J.1 J.2 → A.blkStart T.K I.1 ≤ J.1 → J ∈ ScG G) {Lp Jm : ℕ} (hLp : ∀ (l : Fin 4), (T.pe l).length ≤ Lp) (hJm : ∀ (c d : Fin 4) (i i' : ℕ), (T.desc c d (T.tOf c i) (T.tOf d i')).length ≤ Jm) {C₀ B₀ Cy : ℝ} (hC₀ : 0 < C₀) (hy : ∀ I ∈ S, ∀ (l : Fin 4), T.u ≠ some l → ‖bf.basicIn fp.Mc l I‖ / √(dyadicGridLength A.G I.1) ≤ Cy ∧ ‖bf.Ucol fp.Mc l I‖ / √(dyadicGridLength A.G I.1) ≤ Cy) {Bs BU Bv : ℝ} (hBv : 0 ≤ Bv) (hBs : ∑ I ∈ S, ∑ G ∈ gs I, ∑ l : Fin 4, ‖T.sv l G I‖ ^ 2 ≤ Bs) (hBU : ∑ I ∈ S, ∑ l : Fin 4, ‖bf.Ucol fp.Mc l I‖ ^ 2 ≤ BU) (hVi : ∀ (a c d : Fin 4) (i i' j : ℕ), j < (T.desc c d (T.tOf c i) (T.tOf d i')).length → A.VarCap {G₀} (fun (G : bf.Grp) (h : ℤ) => T.Xo a c d G (T.tOf c i) (T.tOf d i') j (fp.P + 1) h) (fun (x : bf.Grp) (x_1 : ℤ × ℤ) => True) Bv) (hVp : ∀ (a c d : Fin 4) (i i' j n : ℕ), j < (T.desc c d (T.tOf c i) (T.tOf d i')).length → n < fp.P → T.cumY c d (T.tOf c i) (T.tOf d i') j → A.VarCap {G₀} (fun (G : bf.Grp) (h : ℤ) => T.Xo a c d G (T.tOf c i) (T.tOf d i') j (n + 1) h) (fun (x : bf.Grp) (x_1 : ℤ × ℤ) => True) Bv) (hVF : ∀ (a c d : Fin 4) (i i' j : ℕ), j < (T.desc c d (T.tOf c i) (T.tOf d i')).length → T.cumF c d (T.tOf c i) (T.tOf d i') j → A.VarCap {G₀} (fun (G : bf.Grp) (h : ℤ) => fp.FfrM T.cat T.mbs a c d (fp.Lc + 5) G (T.Lf.role c) (T.Lf.role d) (T.desc c d (T.tOf c i) (T.tOf d i')) j h) (fun (x : bf.Grp) (x_1 : ℤ × ℤ) => True) Bv) (hVpG : ∀ (a c d : Fin 4) (i i' j n : ℕ), j < (T.desc c d (T.tOf c i) (T.tOf d i')).length → n < fp.P → ¬T.cumY c d (T.tOf c i) (T.tOf d i') j → A.VarCap gset (fun (G : bf.Grp) (h : ℤ) => T.Xo a c d G (T.tOf c i) (T.tOf d i') j (n + 1) h) ok Bv) (hVFG : ∀ (a c d : Fin 4) (i i' j : ℕ), j < (T.desc c d (T.tOf c i) (T.tOf d i')).length → ¬T.cumF c d (T.tOf c i) (T.tOf d i') j → A.VarCap gset (fun (G : bf.Grp) (h : ℤ) => fp.FfrM T.cat T.mbs a c d (fp.Lc + 5) G (T.Lf.role c) (T.Lf.role d) (T.desc c d (T.tOf c i) (T.tOf d i')) j h) ok Bv) : ∑ I ∈ S, dyadicGridLength A.G I.1 * T.C3v C₀ B₀ G₀ gs I ^ 2 ≤ 2 * (36 * 256 * 256 * (↑Lp ^ 2 * (2 * (1 + 5 * ↑Jm)) * (↑Lp ^ 2 * (localFormUniformConstant κ' ^ 2 * (8 * Cy ^ 2 * BU)) + (2 / ↑fp.P * localFormUniformConstant κ') ^ 2 * 6 * (↑Lp * ↑Lp * (↑Jm * 5) * T.frzB C₀ (↑T.K * Bv))))) + 2 * (36 * 256 * 256 * (2 * (localFormUniformConstant κ' * B₀) ^ 2 * Bs + ↑Lp ^ 2 * (2 * (1 + 5 * ↑Jm)) * ((2 / ↑fp.P * localFormUniformConstant κ') ^ 2 * 6 * (↑Lp * ↑Lp * (↑Jm * 5) * T.frzB C₀ (↑T.K * Bv)))))

Blueprint lines 2386-2394 (third strong factors with shared histories counted once), from variation capacities: if the identity outputs, the pads of cumulative steps and the other complements with cumulative histories have variation capacity B_v as shared outputs, and the pads of ball steps and the other complements with a ball have joint variation capacity B_v over the groups (with the certificates ok on the ancestors of their uses), then the cell values C₃ of the third strong factors have the integrated bound of C3v_budget with E_b = K B_v.

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideLeafM.B3cap {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (T : fp.SideLeafM) (Lp Jm : ℕ) (C₀ B₀ Cy Bs BU Bv : ℝ) : ℝ

The integrated budget of the third strong factors of C3v_budget_cap.

Equations

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

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideLeafM.leaf_two_two_capM {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (T : fp.SideLeafM) {q : ℝ} (hq2 : 2 < q) (hq3 : q < 3) (hanc : A.AncClosed) {Nd N : ℕ} (hKNd : A.DepthWin Nd) (hKN : T.K ≤ 2 ^ N) (S : Finset (ℤ × ℤ)) (hS : S ⊆ A.cells) (hroot : ∀ I ∈ S, dyadicGridCell A.G I.1 I.2 ⊆ dyadicGridCell A.G A.R.1 A.R.2) (gs : ℤ × ℤ → Finset bf.Grp) (gset : Finset bf.Grp) (hgs : ∀ I ∈ S, gs I ⊆ gset) (Lp Jm Bn k : ℕ) (hBn : ∀ I ∈ S, T.bk I < Bn) (hLp : ∀ (l : Fin 4), (T.pe l).length ≤ Lp) (hJm : ∀ (c d : Fin 4) (i i' : ℕ), (T.desc c d (T.tOf c i) (T.tOf d i')).length ≤ Jm) (Act : Finset (ℤ × ℤ)) (hact : ∀ I ∈ S, I ∈ Act ∧ ∀ G ∈ gs I, G ∈ fp.groupsAt I k) {Mp : ℝ} (hMp : ∀ (y : ℝ), ↑{c ∈ Act | y ∈ dyadicGridCell A.G c.1 c.2}.card ≤ Mp) (okZ : Fin 4 → bf.Grp → ℤ × ℤ → Prop) (BZ EW : Fin 4 → ℝ) (hcap : ∀ (l : Fin 4), T.u ≠ some l → A.VarCap gset (T.Z l) (okZ l) (BZ l)) (hok : ∀ (l : Fin 4), T.u ≠ some l → ∀ I ∈ S, ∀ G ∈ gs I, ∀ J ∈ A.cells, dyadicGridCell A.G I.1 I.2 ⊆ dyadicGridCell A.G J.1 J.2 → okZ l G J) (hEW : ∀ (l : Fin 4), T.u ≠ some l → ∑ G ∈ gset, ∑ β ∈ Finset.range Bn, ‖(columnL2Restriction (⋃ J ∈ Finset.image (fun (I : ℤ × ℤ) => ancAt A.G I (A.R.1 + ↑(T.K * β))) ({I ∈ S | G ∈ gs I ∧ T.bk I = β}), dyadicGridCell A.G J.1 J.2) ⋯) (T.Wb l G (A.R.1 + ↑(T.K * β)))‖ ^ 2 ≤ EW l) {EU : ℝ} (hEU : ∀ (l : Fin 4), T.u = some l → ∑ I ∈ S, ∑ G ∈ gs I, ‖(columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯) (T.sv l G I)‖ ^ 2 ≤ EU) {τ cF C₀ B₀ : ℝ} (hτ : 0 ≤ τ) (hcF : 0 ≤ cF) (hC₀ : 0 < C₀) (hB₀ : 0 ≤ B₀) (hpair : ∀ I ∈ S, ∀ (c d : Fin 4), c ≠ d → T.u ≠ some c → T.u ≠ some d → PairSmall (dyadicGridLeft A.G I.1 I.2) (dyadicGridLength A.G I.1) (A.w I) c d (A.Y I c) (A.Y I d) τ) (hfar : ∀ I ∈ S, ∀ G ∈ gs I, ∀ (a b c d : Fin 4), T.Val a b c d → ¬T.Ucase c d → ∀ t ∈ T.pe c, ∀ t' ∈ T.pe d, ‖chainDefectSel (fp.Λc I) fp.P a c d (fun (l : Fin 4) => T.sv l G I) (bf.basicIn fp.Mc c I) (bf.basicIn fp.Mc d I) (fun (p q : ℕ) => q + 2 < p ∨ p + 2 < q) (fp.mergeStepsM T.cat a c d (fp.Lc + 5) I (fp.slotFiltM G (T.Lf.role c) I t.2) (fp.slotFiltM G (T.Lf.role d) I t'.2)) (T.sv a G I)‖ ≤ cF * T.ns a G I * T.ns b G I) (hbas : ∀ J ∈ A.cells, ∀ (l : Fin 4), T.u ≠ some l → ‖bf.basicIn fp.Mc l J‖ ≤ C₀ * √(dyadicGridLength A.G J.1)) (hout : ∀ I ∈ S, ∀ G ∈ gs I, ∀ (l : Fin 4), ‖T.out l G I‖ ≤ B₀ * √(dyadicGridLength A.G I.1)) {Np : ℝ} (hNp : ∀ (c d : Fin 4), ↑(T.pe d).length * ↑(T.pe c).length ≤ Np) {Bs : ℝ} (hBs : ∑ I ∈ S, ∑ G ∈ gs I, ∑ l : Fin 4, ‖T.sv l G I‖ ^ 2 ≤ Bs) (G₀ : bf.Grp) (Sc : Finset (ℤ × ℤ)) (hScc : Sc ⊆ A.cells) (hSc : ∀ I ∈ S, ∀ J ∈ A.cells, dyadicGridCell A.G I.1 I.2 ⊆ dyadicGridCell A.G J.1 J.2 → A.blkStart T.K I.1 ≤ J.1 → J ∈ Sc) (ScG : bf.Grp → Finset (ℤ × ℤ)) (ok : bf.Grp → ℤ × ℤ → Prop) (hScGc : ∀ G ∈ gset, ∀ J ∈ ScG G, J ∈ A.cells ∧ ok G J) (hScG : ∀ I ∈ S, ∀ G ∈ gs I, ∀ J ∈ A.cells, dyadicGridCell A.G I.1 I.2 ⊆ dyadicGridCell A.G J.1 J.2 → A.blkStart T.K I.1 ≤ J.1 → J ∈ ScG G) {Cy : ℝ} (hy : ∀ I ∈ S, ∀ (l : Fin 4), T.u ≠ some l → ‖bf.basicIn fp.Mc l I‖ / √(dyadicGridLength A.G I.1) ≤ Cy ∧ ‖bf.Ucol fp.Mc l I‖ / √(dyadicGridLength A.G I.1) ≤ Cy) {BU Bv : ℝ} (hBv : 0 ≤ Bv) (hBU : ∑ I ∈ S, ∑ l : Fin 4, ‖bf.Ucol fp.Mc l I‖ ^ 2 ≤ BU) (hVi : ∀ (a c d : Fin 4) (i i' j : ℕ), j < (T.desc c d (T.tOf c i) (T.tOf d i')).length → A.VarCap {G₀} (fun (G : bf.Grp) (h : ℤ) => T.Xo a c d G (T.tOf c i) (T.tOf d i') j (fp.P + 1) h) (fun (x : bf.Grp) (x_1 : ℤ × ℤ) => True) Bv) (hVp : ∀ (a c d : Fin 4) (i i' j n : ℕ), j < (T.desc c d (T.tOf c i) (T.tOf d i')).length → n < fp.P → T.cumY c d (T.tOf c i) (T.tOf d i') j → A.VarCap {G₀} (fun (G : bf.Grp) (h : ℤ) => T.Xo a c d G (T.tOf c i) (T.tOf d i') j (n + 1) h) (fun (x : bf.Grp) (x_1 : ℤ × ℤ) => True) Bv) (hVF : ∀ (a c d : Fin 4) (i i' j : ℕ), j < (T.desc c d (T.tOf c i) (T.tOf d i')).length → T.cumF c d (T.tOf c i) (T.tOf d i') j → A.VarCap {G₀} (fun (G : bf.Grp) (h : ℤ) => fp.FfrM T.cat T.mbs a c d (fp.Lc + 5) G (T.Lf.role c) (T.Lf.role d) (T.desc c d (T.tOf c i) (T.tOf d i')) j h) (fun (x : bf.Grp) (x_1 : ℤ × ℤ) => True) Bv) (hVpG : ∀ (a c d : Fin 4) (i i' j n : ℕ), j < (T.desc c d (T.tOf c i) (T.tOf d i')).length → n < fp.P → ¬T.cumY c d (T.tOf c i) (T.tOf d i') j → A.VarCap gset (fun (G : bf.Grp) (h : ℤ) => T.Xo a c d G (T.tOf c i) (T.tOf d i') j (n + 1) h) ok Bv) (hVFG : ∀ (a c d : Fin 4) (i i' j : ℕ), j < (T.desc c d (T.tOf c i) (T.tOf d i')).length → ¬T.cumF c d (T.tOf c i) (T.tOf d i') j → A.VarCap gset (fun (G : bf.Grp) (h : ℤ) => fp.FfrM T.cat T.mbs a c d (fp.Lc + 5) G (T.Lf.role c) (T.Lf.role d) (T.desc c d (T.tOf c i) (T.tOf d i')) j h) ok Bv) (hP : 1 ≤ fp.P) (Γa Γb : Fin 4 → ℝ) (ΓU : ℝ) (hΓa : ∀ (a : Fin 4), T.u ≠ some a → fp.stackEA (nOs Lp Jm) (T.cat a) (T.mbs a) T.Dpre N (BZ a) (EW a) ≤ (↑fp.P + 2) * Γa a * dyadicGridLength A.G A.R.1) (hΓb : ∀ (b : Fin 4), T.u ≠ some b → ↑(nOs Lp Jm).card * (↑N * BZ b + EW b) ≤ Γb b * dyadicGridLength A.G A.R.1) (hΓU : ↑(nOs Lp Jm).card * EU ≤ ΓU * dyadicGridLength A.G A.R.1) {η p ρ : ℝ} (hη : 0 ≤ η) (hp : 2 / 3 < p) (hp1 : p ≤ 1) (hρ : 0 < ρ) (hρ1 : ρ < 1) : ∃ C ⊆ A.cells, dyadicRootLength A.G (maximalDyadicCells A.G C) ≤ 2 * ρ * dyadicGridLength A.G A.R.1 ∧ ∑ I ∈ S with ¬∃ e ∈ C, dyadicGridCell A.G I.1 I.2 ⊆ dyadicGridCell A.G e.1 e.2, dyadicGridLength A.G I.1 * min η ‖∑ σ : Fin 4 → Fin 3 with (∀ (l : Fin 4), σ l ≠ 2) ∧ {l : Fin 4 | σ l = 0}.card = 2 ∧ {l : Fin 4 | σ l = 1}.card = 2, ∑ G ∈ gs I, (fp.Λc I) fun (l : Fin 4) => if σ l = 0 then T.out l G I else T.sv l G I‖ ≤ 6 * 256 * Np * (τ + cF) * ((Bs / dyadicGridLength A.G A.R.1 + T.B3cap Lp Jm C₀ B₀ Cy Bs BU Bv / dyadicGridLength A.G A.R.1) / ρ) * dyadicGridLength A.G A.R.1 + 6 * ∑ a : Fin 4, ∑ b : Fin 4, ∑ e : Fin 4, T.nearBnd hq2 hq3 Nd N Lp Jm Mp C₀ (ρ / 64) Γa Γb ΓU a b e + η ^ (1 - p) * (((Bs / dyadicGridLength A.G A.R.1 + T.B3cap Lp Jm C₀ B₀ Cy Bs BU Bv / dyadicGridLength A.G A.R.1) / ρ) ^ (p / 2) * ((Bs / dyadicGridLength A.G A.R.1 + T.B3cap Lp Jm C₀ B₀ Cy Bs BU Bv / dyadicGridLength A.G A.R.1) / ρ) ^ (p / 2) * ((Bs / dyadicGridLength A.G A.R.1 + T.B3cap Lp Jm C₀ B₀ Cy Bs BU Bv / dyadicGridLength A.G A.R.1) / ρ) ^ (p / 2) * dyadicGridLength A.G A.R.1) ∧ ∀ (x : ℝ), ∑ I ∈ {I ∈ S | ¬∃ e ∈ C, dyadicGridCell A.G I.1 I.2 ⊆ dyadicGridCell A.G e.1 e.2} with x ∈ dyadicGridCell A.G I.1 I.2, ∑ G ∈ gs I, T.s2 G I ≤ (Bs / dyadicGridLength A.G A.R.1 + T.B3cap Lp Jm C₀ B₀ Cy Bs BU Bv / dyadicGridLength A.G A.R.1) / ρ

Blueprint lines 2375-2456, the two-side estimate of one localization leaf on the main columns with the third strong factors in integrated form: one cut family of root fraction at most 2ρ such that on the retained cells the weighted active minimum of the restored 2+2 patterns is at most the pair-small and far absolute bound, six times the critical near-band bounds (eq:near-band), and the power cost of the three strong factors with the joint path cap T_c = (B_s + B_3)/(ρ |R|), where B_3 = B3cap collects the U energy (counted once per cell), the side masses and the freeze budgets of the shared and of the group-indexed frozen complements (blueprint line 2263: "a shared history will not be counted once for every group").

Global complement histories as main-base histories (blueprint lines 2263, 2386-2390)

theorem TrilinearHT.Auto.opAvg_conj {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [NormedAddCommGroup F] [InnerProductSpace ℂ F] {P : ℕ} (R : E →L[ℂ] F) (S : F →L[ℂ] E) (Q : Fin P → E →L[ℂ] E) : (opAvg fun (p : Fin P) => R ∘SL Q p ∘SL S) = R ∘SL opAvg Q ∘SL S

Averages commute with conjugation.

theorem TrilinearHT.Auto.layerOp_conj_left {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [NormedAddCommGroup F] [InnerProductSpace ℂ F] (R : E →L[ℂ] F) (S : F →L[ℂ] E) (hSR : ∀ (y : E), S (R y) = y) (Cum : ℕ → E →L[ℂ] E) (ls : List (ℕ × Bool)) (y : F) : S ((layerOp (fun (m : ℕ) => R ∘SL Cum m ∘SL S) ls) y) = (layerOp Cum ls) (S y)

A left inverse of the conjugation intertwines the layered histories of the conjugated layers with those of the layers.

theorem TrilinearHT.Auto.layerOp_conj {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [NormedAddCommGroup F] [InnerProductSpace ℂ F] (R : E →L[ℂ] F) (S : F →L[ℂ] E) (hSR : ∀ (y : E), S (R y) = y) (Cum : ℕ → E →L[ℂ] E) (ls : List (ℕ × Bool)) (hne : ls ≠ []) (hfalse : ∀ x ∈ ls, x.2 = false) (y : F) : (layerOp (fun (m : ℕ) => R ∘SL Cum m ∘SL S) ls) y = R ((layerOp Cum ls) (S y))

A nonempty layered history of conjugated averaged layers (without complements) is the conjugated layered history.

theorem TrilinearHT.Auto.layerOp_map {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (Cum : ℕ → E →L[ℂ] E) (f : ℕ → ℕ) (ls : List (ℕ × Bool)) : layerOp Cum (List.map (fun (x : ℕ × Bool) => (f x.1, x.2)) ls) = layerOp (fun (m : ℕ) => Cum (f m)) ls

Reindexing the layers of a layered history.

def TrilinearHT.Auto.restIdxM (v : Bool) : List (Bool × ℕ × Option ℕ) → ℕ → List (ℕ × Bool)

The layer indices (innermost first) of the descriptors of slot v of a list of descriptors starting at the position k.

Equations

• TrilinearHT.Auto.restIdxM v [] x✝ = []
• TrilinearHT.Auto.restIdxM v (e :: es) x✝ = TrilinearHT.Auto.restIdxM v es (x✝ + 1) ++ if e.1 = v then [(x✝, false)] else []

theorem TrilinearHT.Auto.restIdxM_false (v : Bool) (es : List (Bool × ℕ × Option ℕ)) (k : ℕ) (x : ℕ × Bool) : x ∈ restIdxM v es k → x.2 = false

theorem TrilinearHT.Auto.restIdxM_mem (v : Bool) (D es : List (Bool × ℕ × Option ℕ)) (k : ℕ) : (∀ (i : ℕ) (hi : i < es.length), es[i] = D.getD (k + i) (true, 0, none)) → ∀ x ∈ restIdxM v es k, D.getD x.1 (true, 0, none) ∈ es ∧ (D.getD x.1 (true, 0, none)).1 = v

The layer indices of slot v point to descriptors of slot v in the list.

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.cmpMaskM {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (cat : Fin 4 → List (CatCol bf.Vtx)) (mbs : (l : Fin 4) → bf.MainBudget (cat l)) (c d : Fin 4) (G : bf.Grp) (jc jd : ℕ) (v : Bool) (D : List (Bool × ℕ × Option ℕ)) (m : ℕ) (p : Fin fp.P) : InheritedColumnMask (bf.mainTree fp.Mc (cat (if v = true then c else d)) (mbs (if v = true then c else d)))

The inherited complement masks of the descriptors of slot v (true for c, false for d) on its main tree, indexed by the position of the descriptor.

Equations

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

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.chainVal_globM {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (cat : Fin 4 → List (CatCol bf.Vtx)) (mbs : (l : Fin 4) → bf.MainBudget (cat l)) (a c d : Fin 4) (rH : ℕ) (G : bf.Grp) (jc jd : ℕ) (v : Bool) (D : List (Bool × ℕ × Option ℕ)) (h : ℤ) (x : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (es : List (Bool × ℕ × Option ℕ)) (k : ℕ) : (∀ (i : ℕ) (hi : i < es.length), es[i] = D.getD (k + i) (true, 0, none)) → chainVal fp.P v (List.map padStep (List.map (fun (e : Bool × ℕ × Option ℕ) => fp.gStepM cat mbs a c d rH G jc jd e h) es)) x = (layerOp (fun (m : ℕ) => opAvg fun (p : Fin fp.P) => fp.gProjC (cat (if v = true then c else d)) (mbs (if v = true then c else d)) (cmpMaskM cat mbs c d G jc jd v D m p) h) (restIdxM v es k)) x

The complement value of slot v after global steps is the layered history of the conjugated global projections with the complement masks of its descriptors.

theorem TrilinearHT.Auto.chainVal_append {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (P : ℕ) (v : Bool) (L₁ L₂ : List (TransferStep E)) (y : E) : chainVal P v (L₁ ++ L₂) y = chainVal P v L₁ (chainVal P v L₂ y)

Complement values over concatenated step lists compose.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.mergeDescM_slot {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (jc jd : ℕ) (t t' : List ℕ) {e : Bool × ℕ × Option ℕ} (he : e ∈ fp.mergeDescM jc jd t t') : e.2 = (fp.brank (if e.1 = true then jc else jd), none) ∨ ∃ (m : ℕ), e.2 = (fp.crank m, some m)

The descriptors of the merge of the slot descriptors are the ball descriptor or cumulative descriptors of their slot.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.mergeDescM_later {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (jc jd : ℕ) (t t' : List ℕ) {i : ℕ} (hi : i < (fp.mergeDescM jc jd t t').length) {e : Bool × ℕ × Option ℕ} (he : e ∈ List.drop (i + 1) (fp.mergeDescM jc jd t t')) (hev : e.1 = ((fp.mergeDescM jc jd t t').getD i (true, 0, none)).1) : ∃ (m : ℕ), e.2 = (fp.crank m, some m)

Blueprint line 2263: a descriptor of a slot that comes after another descriptor of the same slot is cumulative.

def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.lsCum (D : List (Bool × ℕ × Option ℕ)) (ls : List (ℕ × Bool)) : List (ℕ × Bool)

The cumulative layer indices of a list of layer positions in the descriptors D.

Equations

• TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.lsCum D ls = List.map (fun (y : ℕ × Bool) => ((D.getD y.1 (true, 0, none)).2.2.getD 0, y.2)) ls

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.lsCum_length (D : List (Bool × ℕ × Option ℕ)) (ls : List (ℕ × Bool)) : (lsCum D ls).length = ls.length

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.cmpMaskM_cum {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (cat : Fin 4 → List (CatCol bf.Vtx)) (mbs : (l : Fin 4) → bf.MainBudget (cat l)) (c d : Fin 4) (G : bf.Grp) (jc jd : ℕ) (w : Bool) (D : List (Bool × ℕ × Option ℕ)) (k : ℕ) (p : Fin fp.P) {m : ℕ} (hm : (D.getD k (true, 0, none)).2 = (fp.crank m, some m)) : cmpMaskM cat mbs c d G jc jd w D k p = fp.cumMaskT (if w = true then c else d) (cat (if w = true then c else d)) (mbs (if w = true then c else d)) m p

The complement mask of a cumulative descriptor is the cumulative mask of its split.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.globHist_cmp_cum {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (cat : Fin 4 → List (CatCol bf.Vtx)) (mbs : (l : Fin 4) → bf.MainBudget (cat l)) (c d : Fin 4) (G : bf.Grp) (jc jd : ℕ) (w : Bool) (D es : List (Bool × ℕ × Option ℕ)) (k : ℕ) (hes : ∀ (i : ℕ) (hi : i < es.length), es[i] = D.getD (k + i) (true, 0, none)) (hcum : ∀ e ∈ es, e.1 = w → ∃ (m : ℕ), e.2 = (fp.crank m, some m)) (h : ℤ) : layerOp (fun (m : ℕ) => opAvg fun (p : Fin fp.P) => ((bf.mainBase fp.Mc (cat (if w = true then c else d)) (mbs (if w = true then c else d))).withMask (cmpMaskM cat mbs c d G jc jd w D m p)).proj h) (restIdxM w es k) = fp.gHist (if w = true then c else d) (cat (if w = true then c else d)) (mbs (if w = true then c else d)) (lsCum D (restIdxM w es k)) h

The layers of slot v with cumulative descriptors are the averaged cumulative projections of the main tree of its slot.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.cum_hist_left {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (cat : Fin 4 → List (CatCol bf.Vtx)) (mbs : (l : Fin 4) → bf.MainBudget (cat l)) (a c d : Fin 4) (rH : ℕ) (G : bf.Grp) (jc jd : ℕ) (w : Bool) (D es : List (Bool × ℕ × Option ℕ)) (k : ℕ) (hes : ∀ (i : ℕ) (hi : i < es.length), es[i] = D.getD (k + i) (true, 0, none)) (hcum : ∀ e ∈ es, e.1 = w → ∃ (m : ℕ), e.2 = (fp.crank m, some m)) (h : ℤ) (x : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) : (ContinuousLinearMap.adjoint (colRelabel (bf.rv fp.Mc (cat (if w = true then c else d))))) (chainVal fp.P w (List.map padStep (List.map (fun (e : Bool × ℕ × Option ℕ) => fp.gStepM cat mbs a c d rH G jc jd e h) es)) x) = (fp.gHist (if w = true then c else d) (cat (if w = true then c else d)) (mbs (if w = true then c else d)) (lsCum D (restIdxM w es k)) h) ((ContinuousLinearMap.adjoint (colRelabel (bf.rv fp.Mc (cat (if w = true then c else d))))) x)

Blueprint line 2263 ("its complementary band history is shared across groups"): the relabeling adjoint of a complement value of slot w after global steps whose descriptors of that slot are cumulative is the shared main-base history of the relabeled input.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.cum_hist_full {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (cat : Fin 4 → List (CatCol bf.Vtx)) (mbs : (l : Fin 4) → bf.MainBudget (cat l)) (a c d : Fin 4) (rH : ℕ) (G : bf.Grp) (jc jd : ℕ) (w : Bool) (D es : List (Bool × ℕ × Option ℕ)) (k : ℕ) (hes : ∀ (i : ℕ) (hi : i < es.length), es[i] = D.getD (k + i) (true, 0, none)) (hcum : ∀ e ∈ es, e.1 = w → ∃ (m : ℕ), e.2 = (fp.crank m, some m)) (hne : restIdxM w es k ≠ []) (h : ℤ) (x : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) : chainVal fp.P w (List.map padStep (List.map (fun (e : Bool × ℕ × Option ℕ) => fp.gStepM cat mbs a c d rH G jc jd e h) es)) x = (colRelabel (bf.rv fp.Mc (cat (if w = true then c else d)))) ((fp.gHist (if w = true then c else d) (cat (if w = true then c else d)) (mbs (if w = true then c else d)) (lsCum D (restIdxM w es k)) h) ((ContinuousLinearMap.adjoint (colRelabel (bf.rv fp.Mc (cat (if w = true then c else d))))) x))

A complement value of slot w after global steps whose descriptors of that slot are cumulative, at least one of them: the relabeled shared main-base history.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.cum_hist_empty {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (cat : Fin 4 → List (CatCol bf.Vtx)) (mbs : (l : Fin 4) → bf.MainBudget (cat l)) (a c d : Fin 4) (rH : ℕ) (G : bf.Grp) (jc jd : ℕ) (w : Bool) (D es : List (Bool × ℕ × Option ℕ)) (k : ℕ) (hes : ∀ (i : ℕ) (hi : i < es.length), es[i] = D.getD (k + i) (true, 0, none)) (hemp : restIdxM w es k = []) (h : ℤ) (x : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) : chainVal fp.P w (List.map padStep (List.map (fun (e : Bool × ℕ × Option ℕ) => fp.gStepM cat mbs a c d rH G jc jd e h) es)) x = x

A complement value of slot w after global steps without descriptors of that slot is the input.

theorem TrilinearHT.Auto.drop_getD_eq {α : Type u_1} (D : List α) (k : ℕ) (d : α) (i : ℕ) (hi : i < (List.drop k D).length) : (List.drop k D)[i] = D.getD (k + i) d

The entries of a dropped list are the entries of the list at the shifted positions.

theorem TrilinearHT.Auto.chainVal_skip {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (P : ℕ) (v : Bool) (L : List (TransferStep E)) (hL : ∀ st ∈ L, st.1 ≠ v) (y : E) : chainVal P v L y = y

Complement values skip steps of the other slot.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.gBasic_ite {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (v : Bool) (c d : Fin 4) (h : ℤ) : (if v = true then bf.gBasic fp.Mc c h else bf.gBasic fp.Mc d h) = bf.gBasic fp.Mc (if v = true then c else d) h

The basic input of the slot of a step.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.merge_after_cum {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (jc jd : ℕ) (t t' : List ℕ) (j : ℕ) (e : Bool × ℕ × Option ℕ) : e ∈ List.drop (j + 1) (fp.mergeDescM jc jd t t') → e.1 = ((fp.mergeDescM jc jd t t').getD j (true, 0, none)).1 → ∃ (m : ℕ), e.2 = (fp.crank m, some m)

The later descriptors of the slot of a step of merged descriptors are cumulative.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideLeafM.desc_after_cum {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (T : fp.SideLeafM) (c d : Fin 4) (t t' : List ℕ) (j : ℕ) (e : Bool × ℕ × Option ℕ) : e ∈ List.drop (j + 1) (T.desc c d t t') → e.1 = ((T.desc c d t t').getD j (true, 0, none)).1 → ∃ (m : ℕ), e.2 = (fp.crank m, some m)

The later descriptors of the slot of a step of a chain pair are cumulative.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideLeafM.Xo_pad {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (T : fp.SideLeafM) (a c d : Fin 4) (G : bf.Grp) (t t' : List ℕ) (j n : ℕ) (hn : n < fp.P) (h : ℤ) : T.Xo a c d G t t' j (n + 1) h = fp.basicOutM (if ((T.desc c d t t').getD j (true, 0, none)).1 = true then c else d) (T.cat (if ((T.desc c d t t').getD j (true, 0, none)).1 = true then c else d)) (T.mbs (if ((T.desc c d t t').getD j (true, 0, none)).1 = true then c else d)) (cmpMaskM T.cat T.mbs c d G (T.Lf.role c) (T.Lf.role d) ((T.desc c d t t').getD j (true, 0, none)).1 (T.desc c d t t') j ⟨n, hn⟩) (lsCum (T.desc c d t t') (restIdxM ((T.desc c d t t').getD j (true, 0, none)).1 (List.drop (j + 1) (T.desc c d t t')) (j + 1))) h

Blueprint lines 1871 and 2386 ("couple individual pad choices across times"): the pad output n + 1 of a step is the single-pad main output of its complement mask after the shared history of the later descriptors of its slot.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideLeafM.Xo_top {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (T : fp.SideLeafM) (a c d : Fin 4) (G : bf.Grp) (t t' : List ℕ) (j : ℕ) (h : ℤ) : T.Xo a c d G t t' j (fp.P + 1) h = if restIdxM ((T.desc c d t t').getD j (true, 0, none)).1 (List.drop (j + 1) (T.desc c d t t')) (j + 1) = [] then bf.gBasic fp.Mc (if ((T.desc c d t t').getD j (true, 0, none)).1 = true then c else d) h else fp.histOut (if ((T.desc c d t t').getD j (true, 0, none)).1 = true then c else d) (T.cat (if ((T.desc c d t t').getD j (true, 0, none)).1 = true then c else d)) (T.mbs (if ((T.desc c d t t').getD j (true, 0, none)).1 = true then c else d)) (lsCum (T.desc c d t t') (restIdxM ((T.desc c d t t').getD j (true, 0, none)).1 (List.drop (j + 1) (T.desc c d t t')) (j + 1))) h

The identity output of a step: the shared history of the later descriptors of its slot applied to the basic input, or the basic input itself without later descriptors of its slot.

theorem TrilinearHT.Auto.restIdxM_length_le (v : Bool) (es : List (Bool × ℕ × Option ℕ)) (k : ℕ) : (restIdxM v es k).length ≤ es.length

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.gBasic_ite_not {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (v : Bool) (c d : Fin 4) (h : ℤ) : (if v = true then bf.gBasic fp.Mc d h else bf.gBasic fp.Mc c h) = bf.gBasic fp.Mc (if (!v) = true then c else d) h

The basic input of the other slot of a step.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.cmpMaskM_ball {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (cat : Fin 4 → List (CatCol bf.Vtx)) (mbs : (l : Fin 4) → bf.MainBudget (cat l)) (c d : Fin 4) (G : bf.Grp) (jc jd : ℕ) (w : Bool) (D : List (Bool × ℕ × Option ℕ)) (k : ℕ) (p : Fin fp.P) (hm : (D.getD k (true, 0, none)).2 = (fp.brank (if w = true then jc else jd), none)) : cmpMaskM cat mbs c d G jc jd w D k p = fp.ballMaskT (if w = true then c else d) (cat (if w = true then c else d)) (mbs (if w = true then c else d)) G (if w = true then jc else jd) p

The complement mask of a ball descriptor is the ball mask of its slot.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideLeafM.F_cum {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (T : fp.SideLeafM) (a c d : Fin 4) (G : bf.Grp) (t t' : List ℕ) (j : ℕ) (hF : T.cumF c d t t' j) (h : ℤ) : fp.FfrM T.cat T.mbs a c d (fp.Lc + 5) G (T.Lf.role c) (T.Lf.role d) (T.desc c d t t') j h = if restIdxM (!((T.desc c d t t').getD j (true, 0, none)).1) (List.drop (j + 1) (T.desc c d t t')) (j + 1) = [] then bf.gBasic fp.Mc (if (!((T.desc c d t t').getD j (true, 0, none)).1) = true then c else d) h else fp.histOut (if (!((T.desc c d t t').getD j (true, 0, none)).1) = true then c else d) (T.cat (if (!((T.desc c d t t').getD j (true, 0, none)).1) = true then c else d)) (T.mbs (if (!((T.desc c d t t').getD j (true, 0, none)).1) = true then c else d)) (lsCum (T.desc c d t t') (restIdxM (!((T.desc c d t t').getD j (true, 0, none)).1) (List.drop (j + 1) (T.desc c d t t')) (j + 1))) h

Blueprint line 2263 ("the other complement ... is shared"): with a cumulative later history, the other complement of a step is the shared history of its slot applied to its basic input, or the basic input itself without later descriptors of its slot.

theorem TrilinearHT.Auto.opAvg_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {P : ℕ} (Q : Fin P → E →L[ℂ] E) (y : E) : (opAvg Q) y = (↑P)⁻¹ • ∑ p : Fin P, (Q p) y

The average of finitely many operators applied to a vector.

theorem TrilinearHT.Auto.chainVal_cons_pad {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (P : ℕ) (v : Bool) (st : Bool × (Fin P → E →L[ℂ] E) × (Fin P → E →L[ℂ] E)) (rest : List (TransferStep E)) (y : E) (h : st.1 = v) : chainVal P v (padStep st :: rest) y = (opAvg st.2.2) (chainVal P v rest y)

A padded step of the slot of a complement value applies its pad average.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.ball_avg_eq {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (cat : Fin 4 → List (CatCol bf.Vtx)) (mbs : (l : Fin 4) → bf.MainBudget (cat l)) (a c d : Fin 4) (rH : ℕ) (G : bf.Grp) (jc jd : ℕ) (w : Bool) (D pre post : List (Bool × ℕ × Option ℕ)) (k₀ : ℕ) (hpre : ∀ e ∈ pre, e.1 ≠ w) (hpost : ∀ (i : ℕ) (hi : i < post.length), post[i] = D.getD (k₀ + 1 + i) (true, 0, none)) (hcum : ∀ e ∈ post, e.1 = w → ∃ (m : ℕ), e.2 = (fp.crank m, some m)) (h : ℤ) (x : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) : chainVal fp.P w (List.map padStep (List.map (fun (e : Bool × ℕ × Option ℕ) => fp.gStepM cat mbs a c d rH G jc jd e h) (pre ++ (w, fp.brank (if w = true then jc else jd), none) :: post))) x = (↑fp.P)⁻¹ • ∑ p : Fin fp.P, (colRelabel (bf.rv fp.Mc (cat (if w = true then c else d)))) ((fp.gOutM (if w = true then c else d) (cat (if w = true then c else d)) (mbs (if w = true then c else d)) (fp.ballMaskT (if w = true then c else d) (cat (if w = true then c else d)) (mbs (if w = true then c else d)) G (if w = true then jc else jd) p) (lsCum D (restIdxM w post (k₀ + 1))) h) ((ContinuousLinearMap.adjoint (colRelabel (bf.rv fp.Mc (cat (if w = true then c else d))))) x))

Blueprint line 2263 ("the other complement ... has a positive ball outermost"): a complement value of slot w after global steps whose first descriptor of that slot is its ball descriptor and whose later descriptors of that slot are cumulative is the pad average of the relabeled single ball-pad outputs after the shared history.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideLeafM.F_ball {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (T : fp.SideLeafM) (a c d : Fin 4) (t t' : List ℕ) (j : ℕ) (hF : ¬T.cumF c d t t' j) : ∃ (ls : List (ℕ × Bool)), ls.length ≤ (T.desc c d t t').length ∧ ∀ (G : bf.Grp) (h : ℤ), fp.FfrM T.cat T.mbs a c d (fp.Lc + 5) G (T.Lf.role c) (T.Lf.role d) (T.desc c d t t') j h = (↑fp.P)⁻¹ • ∑ p : Fin fp.P, fp.basicOutM (if (!((T.desc c d t t').getD j (true, 0, none)).1) = true then c else d) (T.cat (if (!((T.desc c d t t').getD j (true, 0, none)).1) = true then c else d)) (T.mbs (if (!((T.desc c d t t').getD j (true, 0, none)).1) = true then c else d)) (fp.ballMaskT (if (!((T.desc c d t t').getD j (true, 0, none)).1) = true then c else d) (T.cat (if (!((T.desc c d t t').getD j (true, 0, none)).1) = true then c else d)) (T.mbs (if (!((T.desc c d t t').getD j (true, 0, none)).1) = true then c else d)) G (if (!((T.desc c d t t').getD j (true, 0, none)).1) = true then T.Lf.role c else T.Lf.role d) p) ls h

Blueprint line 2263 ("the other complement similarly ... has a positive ball outermost"): if the later history of the other complement of a step contains its ball descriptor, the other complement is the pad average of the single ball-pad main outputs of its slot after a shared history, for one list of layers serving all groups and depths.

Variation capacities of the frozen outputs (blueprint lines 1861-1877, 2386-2390)

theorem TrilinearHT.Auto.norm_avg_sq_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {P : ℕ} (hP : 0 < P) (v : Fin P → E) : ‖(↑P)⁻¹ • ∑ p : Fin P, v p‖ ^ 2 ≤ (↑P)⁻¹ * ∑ p : Fin P, ‖v p‖ ^ 2

The square of an average is at most the average of the squares.

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.capV {κ' : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ' c₀) (c : ℕ) (kk : ℝ) : ℝ

The common variation capacity G₀ · 4 |R| of the single outputs (basic_variationM_le).

Equations

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

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.four_le_capV {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} (c : ℕ) (kk : ℝ) (hk : 1 ≤ kk) : 4 * dyadicGridLength A.G A.R.1 ≤ capV A c kk

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.gBasic_variation {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (hne : A.cells.Nonempty) (l : Fin 4) {ι : Type u_1} [Fintype ι] (r t : ι → ℕ) (hrt : ∀ (i : ι), r i ≤ t i) (hdis : ∀ (i i' : ι), i ≠ i' → Disjoint (Finset.Ioc (r i) (t i)) (Finset.Ioc (r i') (t i'))) (Ec : ι → Finset (ℤ × ℤ)) (hEc : ∀ (i : ι), ∀ I ∈ Ec i, I ∈ A.cells) : ∑ i : ι, ‖(columnL2Restriction (⋃ I ∈ Ec i, dyadicGridCell A.G I.1 I.2) ⋯) (bf.gBasic fp.Mc l (A.R.1 + ↑(t i)) - bf.gBasic fp.Mc l (A.R.1 + ↑(r i)))‖ ^ 2 ≤ 4 * dyadicGridLength A.G A.R.1

Blueprint line 1877 for a basic input without later history: the restricted jumps of the global basic input over disjoint depth intervals have total square at most 4 |R|.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.histOut_variation_le {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (l : Fin 4) (s : List (CatCol bf.Vtx)) (mb : bf.MainBudget s) (hne : A.cells.Nonempty) {ι : Type u_1} [Fintype ι] (ls : List (ℕ × Bool)) (r t : ι → ℕ) (hrt : ∀ (i : ι), r i ≤ t i) (hdis : ∀ (i i' : ι), i ≠ i' → Disjoint (Finset.Ioc (r i) (t i)) (Finset.Ioc (r i') (t i'))) (htd : ∀ (i : ι), t i ≤ A.treeDepth) (Ec : ι → Finset (ℤ × ℤ)) (hEc : ∀ (i : ι), ∀ I ∈ Ec i, I ∈ A.cells) (c : ℕ) (hc : 1 ≤ c) {kk : ℝ} (hk : 1 ≤ kk) (hDm : Real.log (2 * mb.B) ≤ kk ^ c) (hDb : Real.log (2 * A.colBudget) ≤ kk ^ c) (hn : ↑ls.length ≤ ↑c * (Real.log kk + 1)) : ∑ i : ι, ‖(columnL2Restriction (⋃ I ∈ Ec i, dyadicGridCell A.G I.1 I.2) ⋯) (fp.histOut l s mb ls (A.R.1 + ↑(t i)) - fp.histOut l s mb ls (A.R.1 + ↑(r i)))‖ ^ 2 ≤ capV A c kk

Blueprint line 1868 ("the same assertion holds for a shared history, omitting G"): the shared history outputs have variation capacity G₀ · 4 |R|.

theorem TrilinearHT.Auto.ActiveSetup.varCap_congr {κ' : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ' c₀) {γ : Type u_1} {V : Type u_2} [Fintype V] {Gs : Finset γ} {Z Z' : γ → ℤ → ↥(ColumnL2 V)} {ok : γ → ℤ × ℤ → Prop} {B : ℝ} (hZ : ∀ g ∈ Gs, ∀ (h : ℤ), Z g h = Z' g h) (hcap : A.VarCap Gs Z ok B) : A.VarCap Gs Z' ok B

Variation capacities only depend on the outputs of the groups considered.

theorem TrilinearHT.Auto.ActiveSetup.varCap_avg {κ' : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ' c₀) {γ : Type u_1} {V : Type u_2} [Fintype V] {P : ℕ} (hP : 0 < P) {Gs : Finset γ} {Z : Fin P → γ → ℤ → ↥(ColumnL2 V)} {ok : γ → ℤ × ℤ → Prop} {B : ℝ} (hcap : ∀ (p : Fin P), A.VarCap Gs (Z p) ok B) : A.VarCap Gs (fun (g : γ) (h : ℤ) => (↑P)⁻¹ • ∑ p : Fin P, Z p g h) ok B

Blueprint lines 1883 and 2398 ("couple pad choices across times and restore their averages by Jensen"): pad averages of outputs with a common variation capacity have that capacity.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.varCap_ballP {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (l : Fin 4) (s : List (CatCol bf.Vtx)) (hT : ∀ e ∈ s, ∃ R ∈ residueBox (bf.vtag e.tag).dim 9, ∃ (γ : ℝ), e = templateCol (bf.vtag e.tag) l R γ e.birth e.rank e.tag) (htag : ∀ e ∈ s, bf.occAvail (↑e.tag.2) e.tag.1) (dv : bf.Vtx) (mb : bf.MainBudget s) (hanc : A.AncClosed) (hne : A.cells.Nonempty) (Gs : Finset bf.Grp) (k j : ℕ) (hPH : fp.bbase j + fp.P ≤ fp.Hmax) (ls : List (ℕ × Bool)) {ra rb : ℝ} (hroot : ∀ I ∈ A.cells, dyadicGridCell A.G I.1 I.2 ⊆ Set.Icc ra rb) {τ : ℝ} (hτ : 0 < τ) (hτ1 : τ ≤ 1) (hHed : Real.exp (↑A.Dg * (1 + Real.log A.Hsrc + Real.log τ⁻¹) ^ A.Dg) ≤ fp.Hed) {N : ℕ} (hN : ∀ (y : ℝ), {q : ↥Gs × (bf.Lab ⊕ Fin fp.Mc) | ∃ I ∈ A.cells, (∃ (k' : ℕ), fp.Cert k' (↑q.1) I) ∧ ∃ (p : Fin fp.P), y ∈ dyadicGridCell A.G I.1 I.2 ∧ q.2 ∈ mainLabelsM A.G fp.Mc (bf.origCols l) s I (fp.brank j) (fp.bmask I (↑q.1) j (↑p + 1)) dv}.card ≤ N) (hτN : τ * ↑N * A.colBudget ^ 2 ≤ 1) (cc : ℕ) (hc : 1 ≤ cc) {kk : ℝ} (hk : 1 ≤ kk) (hDm : Real.log (2 * mb.B) ≤ kk ^ cc) (hDb : Real.log (2 * A.colBudget) ≤ kk ^ cc) (hn : ↑ls.length ≤ ↑cc * (Real.log kk + 1)) (p : Fin fp.P) : A.VarCap Gs (fun (G : bf.Grp) (h : ℤ) => fp.basicOutM l s mb (fp.ballMaskT l s mb G j p) ls h) (fun (G : bf.Grp) (J : ℤ × ℤ) => fp.Cert k G J) (capV A cc kk)

Blueprint lines 1861-1877 and 2386 ("joint group budgets for positive ball ranges"): the single ball-pad outputs of the groups of G_s after a shared history have joint variation capacity G₀ · 4 |R| on cells certified for their groups.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.varCap_cumP {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (l : Fin 4) (s : List (CatCol bf.Vtx)) (mb : bf.MainBudget s) (hne : A.cells.Nonempty) (G₀ : bf.Grp) (m : ℕ) (p : Fin fp.P) (ls : List (ℕ × Bool)) (cc : ℕ) (hc : 1 ≤ cc) {kk : ℝ} (hk : 1 ≤ kk) (hDm : Real.log (2 * mb.B) ≤ kk ^ cc) (hDb : Real.log (2 * A.colBudget) ≤ kk ^ cc) (hn : ↑ls.length ≤ ↑cc * (Real.log kk + 1)) : A.VarCap {G₀} (fun (x : bf.Grp) (h : ℤ) => fp.basicOutM l s mb (fp.cumMaskT l s mb m p) ls h) (fun (x : bf.Grp) (x_1 : ℤ × ℤ) => True) (capV A cc kk)

Blueprint lines 1868 and 2386 ("shared budgets for group-independent histories"): a single cumulative-pad output after a shared history has variation capacity G₀ · 4 |R|, counted once.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.varCap_histOut {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (l : Fin 4) (s : List (CatCol bf.Vtx)) (mb : bf.MainBudget s) (hne : A.cells.Nonempty) (G₀ : bf.Grp) (ls : List (ℕ × Bool)) (cc : ℕ) (hc : 1 ≤ cc) {kk : ℝ} (hk : 1 ≤ kk) (hDm : Real.log (2 * mb.B) ≤ kk ^ cc) (hDb : Real.log (2 * A.colBudget) ≤ kk ^ cc) (hn : ↑ls.length ≤ ↑cc * (Real.log kk + 1)) : A.VarCap {G₀} (fun (x : bf.Grp) (h : ℤ) => fp.histOut l s mb ls h) (fun (x : bf.Grp) (x_1 : ℤ × ℤ) => True) (capV A cc kk)

The shared history outputs have variation capacity G₀ · 4 |R|, counted once.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.varCap_gBasic {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (l : Fin 4) (hne : A.cells.Nonempty) (G₀ : bf.Grp) (cc : ℕ) {kk : ℝ} (hk : 1 ≤ kk) : A.VarCap {G₀} (fun (x : bf.Grp) (h : ℤ) => bf.gBasic fp.Mc l h) (fun (x : bf.Grp) (x_1 : ℤ × ℤ) => True) (capV A cc kk)

The global basic inputs have variation capacity G₀ · 4 |R|, counted once.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideLeafM.role_ite {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (T : fp.SideLeafM) (c d : Fin 4) (v : Bool) : (if v = true then T.Lf.role c else T.Lf.role d) = T.Lf.role (if v = true then c else d)

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideLeafM.lsCum_drop_le {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (T : fp.SideLeafM) (c d : Fin 4) (t t' : List ℕ) (w : Bool) (j : ℕ) : (lsCum (T.desc c d t t') (restIdxM w (List.drop (j + 1) (T.desc c d t t')) (j + 1))).length ≤ (T.desc c d t t').length

The cumulative history layers of the later descriptors of a slot are at most the steps.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideLeafM.step_slot {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (T : fp.SideLeafM) (c d : Fin 4) (t t' : List ℕ) {j : ℕ} (hj : j < (T.desc c d t t').length) : ((T.desc c d t t').getD j (true, 0, none)).2 = (fp.brank (if ((T.desc c d t t').getD j (true, 0, none)).1 = true then T.Lf.role c else T.Lf.role d), none) ∨ ∃ (m : ℕ), ((T.desc c d t t').getD j (true, 0, none)).2 = (fp.crank m, some m)

The descriptor of a step is a slot descriptor.

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideLeafM.vS {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (T : fp.SideLeafM) (c d : Fin 4) (t t' : List ℕ) (j : ℕ) : Fin 4

The slot of the step j of a chain pair.

Equations

• T.vS c d t t' j = if ((T.desc c d t t').getD j (true, 0, none)).1 = true then c else d

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideLeafM.wS {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (T : fp.SideLeafM) (c d : Fin 4) (t t' : List ℕ) (j : ℕ) : Fin 4

The other slot of the step j of a chain pair.

Equations

• T.wS c d t t' j = if (!((T.desc c d t t').getD j (true, 0, none)).1) = true then c else d

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideLeafM.lsV {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (T : fp.SideLeafM) (c d : Fin 4) (t t' : List ℕ) (j : ℕ) : List (ℕ × Bool)

The shared history layers of the slot of the step j.

Equations

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

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideLeafM.lsW {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (T : fp.SideLeafM) (c d : Fin 4) (t t' : List ℕ) (j : ℕ) : List (ℕ × Bool)

The shared history layers of the other slot of the step j.

Equations

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

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideLeafM.varCap_top {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (T : fp.SideLeafM) (a c d : Fin 4) (t t' : List ℕ) (j : ℕ) (hne : A.cells.Nonempty) (G₀ : bf.Grp) (cc : ℕ) (hc : 1 ≤ cc) {kk : ℝ} (hk : 1 ≤ kk) (hDm : ∀ (l : Fin 4), Real.log (2 * (T.mbs l).B) ≤ kk ^ cc) (hDb : Real.log (2 * A.colBudget) ≤ kk ^ cc) (hlen : ↑(T.desc c d t t').length ≤ ↑cc * (Real.log kk + 1)) : A.VarCap {G₀} (fun (G : bf.Grp) (h : ℤ) => T.Xo a c d G t t' j (fp.P + 1) h) (fun (x : bf.Grp) (x_1 : ℤ × ℤ) => True) (capV A cc kk)

Blueprint line 2263 ("split its terminal complementary band into the shared identity"): the identity outputs of a step have variation capacity G₀ · 4 |R|, counted once.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideLeafM.varCap_pad_cum {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (T : fp.SideLeafM) (a c d : Fin 4) (t t' : List ℕ) {j : ℕ} (hj : j < (T.desc c d t t').length) (n : ℕ) (hn : n < fp.P) (hY : T.cumY c d t t' j) (hne : A.cells.Nonempty) (G₀ : bf.Grp) (cc : ℕ) (hc : 1 ≤ cc) {kk : ℝ} (hk : 1 ≤ kk) (hDm : ∀ (l : Fin 4), Real.log (2 * (T.mbs l).B) ≤ kk ^ cc) (hDb : Real.log (2 * A.colBudget) ≤ kk ^ cc) (hlen : ↑(T.desc c d t t').length ≤ ↑cc * (Real.log kk + 1)) : A.VarCap {G₀} (fun (G : bf.Grp) (h : ℤ) => T.Xo a c d G t t' j (n + 1) h) (fun (x : bf.Grp) (x_1 : ℤ × ℤ) => True) (capV A cc kk)

Blueprint line 2263 ("if the outgoing filter is cumulative ... its complementary band history is shared across groups"): the pad outputs of a cumulative step have variation capacity G₀ · 4 |R|, counted once.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideLeafM.varCap_F_cum {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (T : fp.SideLeafM) (a c d : Fin 4) (t t' : List ℕ) (j : ℕ) (hF : T.cumF c d t t' j) (hne : A.cells.Nonempty) (G₀ : bf.Grp) (cc : ℕ) (hc : 1 ≤ cc) {kk : ℝ} (hk : 1 ≤ kk) (hDm : ∀ (l : Fin 4), Real.log (2 * (T.mbs l).B) ≤ kk ^ cc) (hDb : Real.log (2 * A.colBudget) ≤ kk ^ cc) (hlen : ↑(T.desc c d t t').length ≤ ↑cc * (Real.log kk + 1)) : A.VarCap {G₀} (fun (G : bf.Grp) (h : ℤ) => fp.FfrM T.cat T.mbs a c d (fp.Lc + 5) G (T.Lf.role c) (T.Lf.role d) (T.desc c d t t') j h) (fun (x : bf.Grp) (x_1 : ℤ × ℤ) => True) (capV A cc kk)

Blueprint line 2263 ("the other complement ... is shared"): the other complements with a cumulative later history have variation capacity G₀ · 4 |R|, counted once.

structure TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideLeafM.BallData {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (T : fp.SideLeafM) (gset : Finset bf.Grp) : Type

The localization data of the slot catalogs used by the joint ball variation (the template catalogs, their tags, the ball levels and the overlap of the ball labels of the groups).

• hT (l : Fin 4) (e : CatCol bf.Vtx) : e ∈ T.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 : CatCol bf.Vtx) : e ∈ T.cat l → bf.occAvail (↑e.tag.2) e.tag.1
• dv : Fin 4 → bf.Vtx

  Chart tag used as the distinguished representative in each slot.

• hPH (l : Fin 4) : fp.bbase (T.Lf.role l) + fp.P ≤ fp.Hmax
• N : ℕ

  Uniform count bound for certified main labels visible at a point.

• hN (l : Fin 4) (y : ℝ) : {q : ↥gset × (bf.Lab ⊕ Fin fp.Mc) | ∃ I ∈ A.cells, (∃ (k' : ℕ), fp.Cert k' (↑q.1) I) ∧ ∃ (p : Fin fp.P), y ∈ dyadicGridCell A.G I.1 I.2 ∧ q.2 ∈ mainLabelsM A.G fp.Mc (bf.origCols l) (T.cat l) I (fp.brank (T.Lf.role l)) (fp.bmask I (↑q.1) (T.Lf.role l) (↑p + 1)) (self.dv l)}.card ≤ self.N

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideLeafM.varCap_pad_ball {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (T : fp.SideLeafM) (a c d : Fin 4) (t t' : List ℕ) {j : ℕ} (hj : j < (T.desc c d t t').length) (n : ℕ) (hn : n < fp.P) (hY : ¬T.cumY c d t t' j) {gset : Finset bf.Grp} (B : T.BallData gset) (hanc : A.AncClosed) (hne : A.cells.Nonempty) (k : ℕ) {ra rb : ℝ} (hroot : ∀ I ∈ A.cells, dyadicGridCell A.G I.1 I.2 ⊆ Set.Icc ra rb) {τ : ℝ} (hτ : 0 < τ) (hτ1 : τ ≤ 1) (hHed : Real.exp (↑A.Dg * (1 + Real.log A.Hsrc + Real.log τ⁻¹) ^ A.Dg) ≤ fp.Hed) (hτN : τ * ↑B.N * A.colBudget ^ 2 ≤ 1) (cc : ℕ) (hc : 1 ≤ cc) {kk : ℝ} (hk : 1 ≤ kk) (hDm : ∀ (l : Fin 4), Real.log (2 * (T.mbs l).B) ≤ kk ^ cc) (hDb : Real.log (2 * A.colBudget) ≤ kk ^ cc) (hlen : ↑(T.desc c d t t').length ≤ ↑cc * (Real.log kk + 1)) : A.VarCap gset (fun (G : bf.Grp) (h : ℤ) => T.Xo a c d G t t' j (n + 1) h) (fun (G : bf.Grp) (J : ℤ × ℤ) => fp.Cert k G J) (capV A cc kk)

Blueprint lines 2263 and 2386 ("joint group budgets for positive ball ranges"): the pad outputs of a ball step have joint variation capacity G₀ · 4 |R| over the groups, on cells certified for their groups.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideLeafM.varCap_F_ball {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (T : fp.SideLeafM) (a c d : Fin 4) (t t' : List ℕ) (j : ℕ) (hF : ¬T.cumF c d t t' j) {gset : Finset bf.Grp} (B : T.BallData gset) (hanc : A.AncClosed) (hne : A.cells.Nonempty) (k : ℕ) {ra rb : ℝ} (hroot : ∀ I ∈ A.cells, dyadicGridCell A.G I.1 I.2 ⊆ Set.Icc ra rb) {τ : ℝ} (hτ : 0 < τ) (hτ1 : τ ≤ 1) (hHed : Real.exp (↑A.Dg * (1 + Real.log A.Hsrc + Real.log τ⁻¹) ^ A.Dg) ≤ fp.Hed) (hτN : τ * ↑B.N * A.colBudget ^ 2 ≤ 1) (cc : ℕ) (hc : 1 ≤ cc) {kk : ℝ} (hk : 1 ≤ kk) (hDm : ∀ (l : Fin 4), Real.log (2 * (T.mbs l).B) ≤ kk ^ cc) (hDb : Real.log (2 * A.colBudget) ≤ kk ^ cc) (hlen : ↑(T.desc c d t t').length ≤ ↑cc * (Real.log kk + 1)) : A.VarCap gset (fun (G : bf.Grp) (h : ℤ) => fp.FfrM T.cat T.mbs a c d (fp.Lc + 5) G (T.Lf.role c) (T.Lf.role d) (T.desc c d t t') j h) (fun (G : bf.Grp) (J : ℤ × ℤ) => fp.Cert k G J) (capV A cc kk)

Blueprint lines 2263 and 2386 ("the other complement ... has a positive ball outermost"): the other complements with a ball in their later history have joint variation capacity G₀ · 4 |R| over the groups (pad averages of single ball-pad outputs, by Jensen).

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideLeafM.leaf_two_two_ballM {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (T : fp.SideLeafM) {q : ℝ} (hq2 : 2 < q) (hq3 : q < 3) (hanc : A.AncClosed) (hne : A.cells.Nonempty) {Nd N : ℕ} (hKNd : A.DepthWin Nd) (hKN : T.K ≤ 2 ^ N) (S : Finset (ℤ × ℤ)) (hS : S ⊆ A.cells) (hroot : ∀ I ∈ S, dyadicGridCell A.G I.1 I.2 ⊆ dyadicGridCell A.G A.R.1 A.R.2) (gs : ℤ × ℤ → Finset bf.Grp) (gset : Finset bf.Grp) (hgs : ∀ I ∈ S, gs I ⊆ gset) (Lp Jm Bn k : ℕ) (hBn : ∀ I ∈ S, T.bk I < Bn) (hLp : ∀ (l : Fin 4), (T.pe l).length ≤ Lp) (hJm : ∀ (c d : Fin 4) (i i' : ℕ), (T.desc c d (T.tOf c i) (T.tOf d i')).length ≤ Jm) (Act : Finset (ℤ × ℤ)) (hact : ∀ I ∈ S, I ∈ Act ∧ ∀ G ∈ gs I, G ∈ fp.groupsAt I k) {Mp : ℝ} (hMp : ∀ (y : ℝ), ↑{c ∈ Act | y ∈ dyadicGridCell A.G c.1 c.2}.card ≤ Mp) (hcertS : ∀ I ∈ S, ∀ G ∈ gs I, fp.Cert k G I) (okZ : Fin 4 → bf.Grp → ℤ × ℤ → Prop) (BZ EW : Fin 4 → ℝ) (hcap : ∀ (l : Fin 4), T.u ≠ some l → A.VarCap gset (T.Z l) (okZ l) (BZ l)) (hok : ∀ (l : Fin 4), T.u ≠ some l → ∀ I ∈ S, ∀ G ∈ gs I, ∀ J ∈ A.cells, dyadicGridCell A.G I.1 I.2 ⊆ dyadicGridCell A.G J.1 J.2 → okZ l G J) (hEW : ∀ (l : Fin 4), T.u ≠ some l → ∑ G ∈ gset, ∑ β ∈ Finset.range Bn, ‖(columnL2Restriction (⋃ J ∈ Finset.image (fun (I : ℤ × ℤ) => ancAt A.G I (A.R.1 + ↑(T.K * β))) ({I ∈ S | G ∈ gs I ∧ T.bk I = β}), dyadicGridCell A.G J.1 J.2) ⋯) (T.Wb l G (A.R.1 + ↑(T.K * β)))‖ ^ 2 ≤ EW l) {EU : ℝ} (hEU : ∀ (l : Fin 4), T.u = some l → ∑ I ∈ S, ∑ G ∈ gs I, ‖(columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯) (T.sv l G I)‖ ^ 2 ≤ EU) {τ cF C₀ B₀ : ℝ} (hτ : 0 ≤ τ) (hcF : 0 ≤ cF) (hC₀ : 0 < C₀) (hB₀ : 0 ≤ B₀) (hpair : ∀ I ∈ S, ∀ (c d : Fin 4), c ≠ d → T.u ≠ some c → T.u ≠ some d → PairSmall (dyadicGridLeft A.G I.1 I.2) (dyadicGridLength A.G I.1) (A.w I) c d (A.Y I c) (A.Y I d) τ) (hfar : ∀ I ∈ S, ∀ G ∈ gs I, ∀ (a b c d : Fin 4), T.Val a b c d → ¬T.Ucase c d → ∀ t ∈ T.pe c, ∀ t' ∈ T.pe d, ‖chainDefectSel (fp.Λc I) fp.P a c d (fun (l : Fin 4) => T.sv l G I) (bf.basicIn fp.Mc c I) (bf.basicIn fp.Mc d I) (fun (p q : ℕ) => q + 2 < p ∨ p + 2 < q) (fp.mergeStepsM T.cat a c d (fp.Lc + 5) I (fp.slotFiltM G (T.Lf.role c) I t.2) (fp.slotFiltM G (T.Lf.role d) I t'.2)) (T.sv a G I)‖ ≤ cF * T.ns a G I * T.ns b G I) (hbas : ∀ J ∈ A.cells, ∀ (l : Fin 4), T.u ≠ some l → ‖bf.basicIn fp.Mc l J‖ ≤ C₀ * √(dyadicGridLength A.G J.1)) (hout : ∀ I ∈ S, ∀ G ∈ gs I, ∀ (l : Fin 4), ‖T.out l G I‖ ≤ B₀ * √(dyadicGridLength A.G I.1)) {Np : ℝ} (hNp : ∀ (c d : Fin 4), ↑(T.pe d).length * ↑(T.pe c).length ≤ Np) {Bs : ℝ} (hBs : ∑ I ∈ S, ∑ G ∈ gs I, ∑ l : Fin 4, ‖T.sv l G I‖ ^ 2 ≤ Bs) (G₀ : bf.Grp) {Cy : ℝ} (hy : ∀ I ∈ S, ∀ (l : Fin 4), T.u ≠ some l → ‖bf.basicIn fp.Mc l I‖ / √(dyadicGridLength A.G I.1) ≤ Cy ∧ ‖bf.Ucol fp.Mc l I‖ / √(dyadicGridLength A.G I.1) ≤ Cy) {BU : ℝ} (hBU : ∑ I ∈ S, ∑ l : Fin 4, ‖bf.Ucol fp.Mc l I‖ ^ 2 ≤ BU) (B : T.BallData gset) {ra rb : ℝ} (hroot' : ∀ I ∈ A.cells, dyadicGridCell A.G I.1 I.2 ⊆ Set.Icc ra rb) {τ' : ℝ} (hτ' : 0 < τ') (hτ1 : τ' ≤ 1) (hHed : Real.exp (↑A.Dg * (1 + Real.log A.Hsrc + Real.log τ'⁻¹) ^ A.Dg) ≤ fp.Hed) (hτN : τ' * ↑B.N * A.colBudget ^ 2 ≤ 1) (cc : ℕ) (hc : 1 ≤ cc) {kk : ℝ} (hk : 1 ≤ kk) (hDm : ∀ (l : Fin 4), Real.log (2 * (T.mbs l).B) ≤ kk ^ cc) (hDb : Real.log (2 * A.colBudget) ≤ kk ^ cc) (hJc : ↑Jm ≤ ↑cc * (Real.log kk + 1)) (hP : 1 ≤ fp.P) (Γa Γb : Fin 4 → ℝ) (ΓU : ℝ) (hΓa : ∀ (a : Fin 4), T.u ≠ some a → fp.stackEA (nOs Lp Jm) (T.cat a) (T.mbs a) T.Dpre N (BZ a) (EW a) ≤ (↑fp.P + 2) * Γa a * dyadicGridLength A.G A.R.1) (hΓb : ∀ (b : Fin 4), T.u ≠ some b → ↑(nOs Lp Jm).card * (↑N * BZ b + EW b) ≤ Γb b * dyadicGridLength A.G A.R.1) (hΓU : ↑(nOs Lp Jm).card * EU ≤ ΓU * dyadicGridLength A.G A.R.1) {η p ρ : ℝ} (hη : 0 ≤ η) (hp : 2 / 3 < p) (hp1 : p ≤ 1) (hρ : 0 < ρ) (hρ1 : ρ < 1) : ∃ C ⊆ A.cells, dyadicRootLength A.G (maximalDyadicCells A.G C) ≤ 2 * ρ * dyadicGridLength A.G A.R.1 ∧ ∑ I ∈ S with ¬∃ e ∈ C, dyadicGridCell A.G I.1 I.2 ⊆ dyadicGridCell A.G e.1 e.2, dyadicGridLength A.G I.1 * min η ‖∑ σ : Fin 4 → Fin 3 with (∀ (l : Fin 4), σ l ≠ 2) ∧ {l : Fin 4 | σ l = 0}.card = 2 ∧ {l : Fin 4 | σ l = 1}.card = 2, ∑ G ∈ gs I, (fp.Λc I) fun (l : Fin 4) => if σ l = 0 then T.out l G I else T.sv l G I‖ ≤ 6 * 256 * Np * (τ + cF) * ((Bs / dyadicGridLength A.G A.R.1 + T.B3cap Lp Jm C₀ B₀ Cy Bs BU (capV A cc kk) / dyadicGridLength A.G A.R.1) / ρ) * dyadicGridLength A.G A.R.1 + 6 * ∑ a : Fin 4, ∑ b : Fin 4, ∑ e : Fin 4, T.nearBnd hq2 hq3 Nd N Lp Jm Mp C₀ (ρ / 64) Γa Γb ΓU a b e + η ^ (1 - p) * (((Bs / dyadicGridLength A.G A.R.1 + T.B3cap Lp Jm C₀ B₀ Cy Bs BU (capV A cc kk) / dyadicGridLength A.G A.R.1) / ρ) ^ (p / 2) * ((Bs / dyadicGridLength A.G A.R.1 + T.B3cap Lp Jm C₀ B₀ Cy Bs BU (capV A cc kk) / dyadicGridLength A.G A.R.1) / ρ) ^ (p / 2) * ((Bs / dyadicGridLength A.G A.R.1 + T.B3cap Lp Jm C₀ B₀ Cy Bs BU (capV A cc kk) / dyadicGridLength A.G A.R.1) / ρ) ^ (p / 2) * dyadicGridLength A.G A.R.1) ∧ ∀ (x : ℝ), ∑ I ∈ {I ∈ S | ¬∃ e ∈ C, dyadicGridCell A.G I.1 I.2 ⊆ dyadicGridCell A.G e.1 e.2} with x ∈ dyadicGridCell A.G I.1 I.2, ∑ G ∈ gs I, T.s2 G I ≤ (Bs / dyadicGridLength A.G A.R.1 + T.B3cap Lp Jm C₀ B₀ Cy Bs BU (capV A cc kk) / dyadicGridLength A.G A.R.1) / ρ

Blueprint lines 2375-2456, the two-side estimate of one localization leaf on the main columns, with the freeze budgets of the third strong factors derived from lem:variation: the frozen outputs (identity outputs, cumulative pads and shared other complements counted once; ball pads and other complements with a ball jointly over the groups, on certified cells) have variation capacity G₀ · 4 |R| (capV).

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideLeafM.s2_eq {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (T : fp.SideLeafM) (G : bf.Grp) (I : ℤ × ℤ) : T.s2 G I = ∑ l : Fin 4, ‖T.sv l G I‖ ^ 2 / dyadicGridLength A.G I.1

The squared normalized side sizes of a group at a cell.

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideLeafM.Tcap {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (T : fp.SideLeafM) (Lp Jm : ℕ) (C₀ B₀ Cy Bs BU Bv ρ : ℝ) : ℝ

The joint path cap T_c = (B_s + B_3)/(ρ |R|) of the side estimate.

Equations

• T.Tcap Lp Jm C₀ B₀ Cy Bs BU Bv ρ = (Bs / TrilinearHT.Auto.dyadicGridLength A.G A.R.1 + T.B3cap Lp Jm C₀ B₀ Cy Bs BU Bv / TrilinearHT.Auto.dyadicGridLength A.G A.R.1) / ρ

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideLeafM.leaf_side_estimateM {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (T : fp.SideLeafM) {q : ℝ} (hq2 : 2 < q) (hq3 : q < 3) (hanc : A.AncClosed) (hne : A.cells.Nonempty) {Nd N : ℕ} (hKNd : A.DepthWin Nd) (hKN : T.K ≤ 2 ^ N) (S : Finset (ℤ × ℤ)) (hS : S ⊆ A.cells) (hroot : ∀ I ∈ S, dyadicGridCell A.G I.1 I.2 ⊆ dyadicGridCell A.G A.R.1 A.R.2) (gs : ℤ × ℤ → Finset bf.Grp) (gset : Finset bf.Grp) (hgs : ∀ I ∈ S, gs I ⊆ gset) (Lp Jm Bn k : ℕ) (hBn : ∀ I ∈ S, T.bk I < Bn) (hLp : ∀ (l : Fin 4), (T.pe l).length ≤ Lp) (hJm : ∀ (c d : Fin 4) (i i' : ℕ), (T.desc c d (T.tOf c i) (T.tOf d i')).length ≤ Jm) (Act : Finset (ℤ × ℤ)) (hact : ∀ I ∈ S, I ∈ Act ∧ ∀ G ∈ gs I, G ∈ fp.groupsAt I k) {Mp : ℝ} (hMp : ∀ (y : ℝ), ↑{c ∈ Act | y ∈ dyadicGridCell A.G c.1 c.2}.card ≤ Mp) (hcertS : ∀ I ∈ S, ∀ G ∈ gs I, fp.Cert k G I) (okZ : Fin 4 → bf.Grp → ℤ × ℤ → Prop) (BZ EW : Fin 4 → ℝ) (hcap : ∀ (l : Fin 4), T.u ≠ some l → A.VarCap gset (T.Z l) (okZ l) (BZ l)) (hok : ∀ (l : Fin 4), T.u ≠ some l → ∀ I ∈ S, ∀ G ∈ gs I, ∀ J ∈ A.cells, dyadicGridCell A.G I.1 I.2 ⊆ dyadicGridCell A.G J.1 J.2 → okZ l G J) (hEW : ∀ (l : Fin 4), T.u ≠ some l → ∑ G ∈ gset, ∑ β ∈ Finset.range Bn, ‖(columnL2Restriction (⋃ J ∈ Finset.image (fun (I : ℤ × ℤ) => ancAt A.G I (A.R.1 + ↑(T.K * β))) ({I ∈ S | G ∈ gs I ∧ T.bk I = β}), dyadicGridCell A.G J.1 J.2) ⋯) (T.Wb l G (A.R.1 + ↑(T.K * β)))‖ ^ 2 ≤ EW l) {EU : ℝ} (hEU : ∀ (l : Fin 4), T.u = some l → ∑ I ∈ S, ∑ G ∈ gs I, ‖(columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯) (T.sv l G I)‖ ^ 2 ≤ EU) {τ cF C₀ B₀ : ℝ} (hτ : 0 ≤ τ) (hcF : 0 ≤ cF) (hC₀ : 0 < C₀) (hB₀ : 0 ≤ B₀) (hpair : ∀ I ∈ S, ∀ (c d : Fin 4), c ≠ d → T.u ≠ some c → T.u ≠ some d → PairSmall (dyadicGridLeft A.G I.1 I.2) (dyadicGridLength A.G I.1) (A.w I) c d (A.Y I c) (A.Y I d) τ) (hfar : ∀ I ∈ S, ∀ G ∈ gs I, ∀ (a b c d : Fin 4), T.Val a b c d → ¬T.Ucase c d → ∀ t ∈ T.pe c, ∀ t' ∈ T.pe d, ‖chainDefectSel (fp.Λc I) fp.P a c d (fun (l : Fin 4) => T.sv l G I) (bf.basicIn fp.Mc c I) (bf.basicIn fp.Mc d I) (fun (p q : ℕ) => q + 2 < p ∨ p + 2 < q) (fp.mergeStepsM T.cat a c d (fp.Lc + 5) I (fp.slotFiltM G (T.Lf.role c) I t.2) (fp.slotFiltM G (T.Lf.role d) I t'.2)) (T.sv a G I)‖ ≤ cF * T.ns a G I * T.ns b G I) (hbas : ∀ J ∈ A.cells, ∀ (l : Fin 4), T.u ≠ some l → ‖bf.basicIn fp.Mc l J‖ ≤ C₀ * √(dyadicGridLength A.G J.1)) (hout : ∀ I ∈ S, ∀ G ∈ gs I, ∀ (l : Fin 4), ‖T.out l G I‖ ≤ B₀ * √(dyadicGridLength A.G I.1)) {Np : ℝ} (hNp : ∀ (c d : Fin 4), ↑(T.pe d).length * ↑(T.pe c).length ≤ Np) {Bs : ℝ} (hBs : ∑ I ∈ S, ∑ G ∈ gs I, ∑ l : Fin 4, ‖T.sv l G I‖ ^ 2 ≤ Bs) (G₀ : bf.Grp) {Cy : ℝ} (hy : ∀ I ∈ S, ∀ (l : Fin 4), T.u ≠ some l → ‖bf.basicIn fp.Mc l I‖ / √(dyadicGridLength A.G I.1) ≤ Cy ∧ ‖bf.Ucol fp.Mc l I‖ / √(dyadicGridLength A.G I.1) ≤ Cy) {BU : ℝ} (hBU : ∑ I ∈ S, ∑ l : Fin 4, ‖bf.Ucol fp.Mc l I‖ ^ 2 ≤ BU) (B : T.BallData gset) {ra rb : ℝ} (hroot' : ∀ I ∈ A.cells, dyadicGridCell A.G I.1 I.2 ⊆ Set.Icc ra rb) {τ' : ℝ} (hτ' : 0 < τ') (hτ1 : τ' ≤ 1) (hHed : Real.exp (↑A.Dg * (1 + Real.log A.Hsrc + Real.log τ'⁻¹) ^ A.Dg) ≤ fp.Hed) (hτN : τ' * ↑B.N * A.colBudget ^ 2 ≤ 1) (cc : ℕ) (hc : 1 ≤ cc) {kk : ℝ} (hk : 1 ≤ kk) (hDm : ∀ (l : Fin 4), Real.log (2 * (T.mbs l).B) ≤ kk ^ cc) (hDb : Real.log (2 * A.colBudget) ≤ kk ^ cc) (hJc : ↑Jm ≤ ↑cc * (Real.log kk + 1)) (hP : 1 ≤ fp.P) (Γa Γb : Fin 4 → ℝ) (ΓU : ℝ) (hΓa : ∀ (a : Fin 4), T.u ≠ some a → fp.stackEA (nOs Lp Jm) (T.cat a) (T.mbs a) T.Dpre N (BZ a) (EW a) ≤ (↑fp.P + 2) * Γa a * dyadicGridLength A.G A.R.1) (hΓb : ∀ (b : Fin 4), T.u ≠ some b → ↑(nOs Lp Jm).card * (↑N * BZ b + EW b) ≤ Γb b * dyadicGridLength A.G A.R.1) (hΓU : ↑(nOs Lp Jm).card * EU ≤ ΓU * dyadicGridLength A.G A.R.1) {η p ρ : ℝ} (hη : 0 ≤ η) (hp : 2 / 3 < p) (hp1 : p ≤ 1) (hρ : 0 < ρ) (hρ1 : ρ < 1) : ∃ C ⊆ A.cells, dyadicRootLength A.G (maximalDyadicCells A.G C) ≤ 2 * ρ * dyadicGridLength A.G A.R.1 ∧ ∑ I ∈ S with ¬∃ e ∈ C, dyadicGridCell A.G I.1 I.2 ⊆ dyadicGridCell A.G e.1 e.2, dyadicGridLength A.G I.1 * min η ‖∑ σ : Fin 4 → Fin 3 with (∀ (l : Fin 4), σ l ≠ 2) ∧ {l : Fin 4 | σ l = 0}.card = 2 ∧ {l : Fin 4 | σ l = 1}.card = 2, ∑ G ∈ gs I, (fp.Λc I) fun (l : Fin 4) => if σ l = 0 then T.out l G I else T.sv l G I‖ ≤ 6 * 256 * Np * (τ + cF) * T.Tcap Lp Jm C₀ B₀ Cy Bs BU (capV A cc kk) ρ * dyadicGridLength A.G A.R.1 + 6 * ∑ a : Fin 4, ∑ b : Fin 4, ∑ e : Fin 4, T.nearBnd hq2 hq3 Nd N Lp Jm Mp C₀ (ρ / 64) Γa Γb ΓU a b e + η ^ (1 - p) * (T.Tcap Lp Jm C₀ B₀ Cy Bs BU (capV A cc kk) ρ ^ (p / 2) * T.Tcap Lp Jm C₀ B₀ Cy Bs BU (capV A cc kk) ρ ^ (p / 2) * T.Tcap Lp Jm C₀ B₀ Cy Bs BU (capV A cc kk) ρ ^ (p / 2) * dyadicGridLength A.G A.R.1) ∧ (∀ (core err : ℤ × ℤ → bf.Grp → Fin 4 → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))), ∀ S' ⊆ {I ∈ S | ¬∃ e ∈ C, dyadicGridCell A.G I.1 I.2 ⊆ dyadicGridCell A.G e.1 e.2}, ∀ {Bc : ℝ}, 0 ≤ Bc → (∀ I ∈ S', ∀ G ∈ gs I, ∀ (l : Fin 4), ‖core I G l‖ ≤ Bc * √(dyadicGridLength A.G I.1)) → ∑ I ∈ S', dyadicGridLength A.G I.1 * min η (∑ σ : Fin 4 → Fin 3 with (∀ (l : Fin 4), σ l ≠ 2) ∧ 3 ≤ patternCount σ 1, ‖∑ G ∈ gs I, (fp.Λc I) (patternPiece (core I G) (fun (l : Fin 4) => T.sv l G I) (err I G) σ)‖) ≤ η ^ (1 - p) * (81 * localFormUniformConstant κ' * max Bc √(T.Tcap Lp Jm C₀ B₀ Cy Bs BU (capV A cc kk) ρ)) ^ p * (T.Tcap Lp Jm C₀ B₀ Cy Bs BU (capV A cc kk) ρ ^ (p / 2) * T.Tcap Lp Jm C₀ B₀ Cy Bs BU (capV A cc kk) ρ ^ (p / 2) * T.Tcap Lp Jm C₀ B₀ Cy Bs BU (capV A cc kk) ρ ^ (p / 2) * dyadicGridLength A.G A.R.1)) ∧ ∀ (x : ℝ), ∑ I ∈ {I ∈ S | ¬∃ e ∈ C, dyadicGridCell A.G I.1 I.2 ⊆ dyadicGridCell A.G e.1 e.2} with x ∈ dyadicGridCell A.G I.1 I.2, ∑ G ∈ gs I, T.s2 G I ≤ T.Tcap Lp Jm C₀ B₀ Cy Bs BU (capV A cc kk) ρ

Blueprint lines 2446-2456, the side estimate of one localization leaf on the main columns (unconditional form on the leaf data): one cut family of root fraction at most 2ρ such that on the retained cells

• the weighted active minimum of the two-side terms (two sides, whole current outputs in the other positions) is at most the pair-small and far absolute bound, six times the critical near-band bounds (eq:near-band), and the power cost of the three strong factors, with shared frozen histories counted once (leaf_two_two_ballM);
• on every set of retained cells on which given cores have normalized size at most B_c, the weighted active minimum of the error-free core/side patterns with at least three sides is at most their power cost η^{1-p} (81 C_κ max(B_c, √T_c))^p T_c^{3p/2} |R| (eq:three-sides, eq:min-power): the sides have normalized size at most √T_c on retained cells;
• the side cap: the retained paths carry squared normalized side sizes at most T_c (eq:side-cap), with the joint path cap T_c = (B_s + B_3)/(ρ |R|).

The leaf data from the side states (blueprint lines 2123-2130, 2236-2237)

structure TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) : Type 1

The input of the side estimate on one localization leaf: the slot catalogs with their main budgets, the search leaf, the optional slot of the basic U argument (whose inputs are the basic sides U_{l,I} of prop:base), and the mode systems with the frozen coefficients of the linear sides (prop:linear-side) defining the side states S_{l,G,s} = Z_{l,G,s} - Z_{l,G,u_b} + V_{l,G,b} (blueprint eq:sides).

• cat : Fin 4 → List (CatCol bf.Vtx)

  Catalog columns in each slot of the mode-side input.

• mbs (l : Fin 4) : bf.MainBudget (self.cat l)

  Pathwise main-label budget for each slot catalog.

• Lf : SearchLeaf

  Search leaf determining the side filters.

• u : Option (Fin 4)

  Optional slot carrying the expanded outer input.

• S : ModeSchedule

  Height and block schedule of the mode-side input.

• hA : 6 ≤ self.S.A0
• SP : SideParams

  Coherence and side-event parameters of the mode-side input.

• hK : 1 ≤ self.S.K
• n : ℕ

  Number of primary column labels in each frozen mode system.

• Ms : Fin 4 → bf.Grp → ModeSystem A.G self.n

  Frozen mode system assigned to each slot and group.

• c (l : Fin 4) (G : bf.Grp) : ℤ → ℤ × ℤ → (self.Ms l G).Md → ℂ

  Frozen mode coefficients indexed by block start and pre-cell.

def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.withQ0 {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (q : ℕ) : fp.SideInput

The side input with the clearing integer of its schedule replaced by q (the side input of one group, blueprint line 1890); all other data are those of D.

Equations

• D.withQ0 q = { cat := D.cat, mbs := D.mbs, Lf := D.Lf, u := D.u, S := D.S.withQ0 q, hA := ⋯, SP := D.SP, hK := ⋯, n := D.n, Ms := D.Ms, c := D.c }

@[simp]

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.withQ0_S {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (q : ℕ) : (D.withQ0 q).S = D.S.withQ0 q

@[simp]

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.withQ0_SP {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (q : ℕ) : (D.withQ0 q).SP = D.SP

@[simp]

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.withQ0_u {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (q : ℕ) : (D.withQ0 q).u = D.u

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.Zr {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (l : Fin 4) (G : bf.Grp) (h : ℤ) : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))

The rolling outputs Z_{l,G,h} in physical coordinates.

Equations

• D.Zr l G h = (fp.physMain (bf.Lab ⊕ Fin fp.Mc)) (fp.basicOut l (D.cat l) (D.mbs l) G (D.Lf.role l) (D.Lf.layers l) h)

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.Wr {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (l : Fin 4) (G : bf.Grp) (b : ℤ) : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))

The block input W_b = Z_b - Z_{u_b} + V_b of the block starting at b.

Equations

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

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.gs' {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (l : Fin 4) (G : bf.Grp) (h : ℤ) : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))

The global side state at the depth h (blueprint eq:sides).

Equations

• D.gs' l G h = fp.sideState (D.Ms l G) l (D.cat l) (D.mbs l) G (D.Lf.role l) (D.Lf.layers l) D.S ⋯ D.SP (D.c l G (A.blkStart D.S.K h)) (A.blkStart D.S.K h) h

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.gs'_eq {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (l : Fin 4) (G : bf.Grp) (h : ℤ) : D.gs' l G h = D.Zr l G h - D.Zr l G (A.blkStart D.S.K h) + D.Wr l G (A.blkStart D.S.K h)

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.gs'_range {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (l : Fin 4) (G : bf.Grp) (h : ℤ) : D.gs' l G h ∈ (↑(colRelabel (bf.rv fp.Mc (D.cat l)))).range

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.toLeaf {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) : fp.SideLeafM

The leaf data of the side estimate: the basic slots carry the side states restricted to the cells, the U slot (if any) its whole output.

Equations

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

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.toLeafQ {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (qG : bf.Grp → ℕ) : fp.SideLeafM

The leaf data with per-group clearing integers qG (blueprint line 1890: Q₀ is chosen for each group center): the side states, block inputs and global sides of the group G are those of the side input with Q₀ = qG G.

Equations

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

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.toLeafQ_sv {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (qG : bf.Grp → ℕ) (l : Fin 4) (G : bf.Grp) (I : ℤ × ℤ) : (D.toLeafQ qG).sv l G I = (D.withQ0 (qG G)).toLeaf.sv l G I

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.toLeafQ_out {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (qG : bf.Grp → ℕ) (l : Fin 4) (G : bf.Grp) (I : ℤ × ℤ) : (D.toLeafQ qG).out l G I = (D.withQ0 (qG G)).toLeaf.out l G I

The energies of the side-state leaf data (blueprint lines 2159-2163)

theorem TrilinearHT.Auto.colRelabel_physicalColumnInput {V : Type u_1} {W : Type u_2} [Fintype V] [Fintype W] (f : V → W) (g : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : (colRelabel f) (physicalColumnInput g) = physicalColumnInput g

Relabeling keeps the physical input physical.

theorem TrilinearHT.Auto.physicalColumnInput_cellLp_vanish' {V : Type u_1} [Fintype V] (G : RealDyadicGrid) (I : ℤ × ℤ) (f : ℝ → ℂ) : ∀ᵐ (y : ℝ), y ∉ dyadicGridCell G I.1 I.2 → ↑↑(physicalColumnInput (cellLp G I f)) y = 0

The physical input of a cell function vanishes off the cell (without integrability).

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.Ucol_mem_range {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} (bf : A.BasicFamilies) (Mc : ℕ) (s : List (CatCol bf.Vtx)) (l : Fin 4) (I : ℤ × ℤ) : bf.Ucol Mc l I ∈ (↑(colRelabel (bf.rv Mc s))).range

The basic sides lie in the range of every relabeling of the main columns.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.restrict_Ucol {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} (bf : A.BasicFamilies) (Mc : ℕ) (l : Fin 4) (I : ℤ × ℤ) : (columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯) (bf.Ucol Mc l I) = bf.Ucol Mc l I

The basic side of a cell is supported on the cell.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.cell_out_eq {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (l : Fin 4) (s : List (CatCol bf.Vtx)) (mb : bf.MainBudget s) (G : bf.Grp) (j : ℕ) (ls : List (ℕ × Bool)) {I : ℤ × ℤ} (hI : I ∈ A.cells) (x : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (hx : x ∈ (↑(colRelabel (bf.rv fp.Mc s))).range) (hxI : (columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯) x = x) : (fp.ballFilt l s I G j) ((layerOp (fun (m : ℕ) => fp.cumFilt l s I m) ls) x) = (colRelabel (bf.rv fp.Mc s)) ((columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯) ((fp.gOut l s mb G j ls I.1) ((ContinuousLinearMap.adjoint (colRelabel (bf.rv fp.Mc s))) x)))

The cell outputs are the cell restrictions of the global outputs of any input of the range of the relabeling supported on the cell.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.cell_bessel {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (l : Fin 4) (s : List (CatCol bf.Vtx)) (hT : ∀ e ∈ s, ∃ R ∈ residueBox (bf.vtag e.tag).dim 9, ∃ (γ : ℝ), e = templateCol (bf.vtag e.tag) l R γ e.birth e.rank e.tag) (htag : ∀ e ∈ s, bf.occAvail (↑e.tag.2) e.tag.1) (d : bf.Vtx) (mb : bf.MainBudget s) (gset : Finset bf.Grp) (k j : ℕ) (hPH : fp.bbase j + fp.P ≤ fp.Hmax) (ls : List (ℕ × Bool)) {I : ℤ × ℤ} (hI : I ∈ A.cells) (g : Finset bf.Grp) (hg : g ⊆ gset) (hcert : ∀ G ∈ g, fp.Cert k G I) {ra rb : ℝ} (hroot : ∀ I ∈ A.cells, dyadicGridCell A.G I.1 I.2 ⊆ Set.Icc ra rb) {τ : ℝ} (hτ : 0 < τ) (hτ1 : τ ≤ 1) (hHed : Real.exp (↑A.Dg * (1 + Real.log A.Hsrc + Real.log τ⁻¹) ^ A.Dg) ≤ fp.Hed) {N : ℕ} (hN : ∀ (y : ℝ), {q : ↥gset × (bf.Lab ⊕ Fin fp.Mc) | ∃ I ∈ A.cells, (∃ (k' : ℕ), fp.Cert k' (↑q.1) I) ∧ ∃ (p : Fin fp.P), y ∈ dyadicGridCell A.G I.1 I.2 ∧ q.2 ∈ mainLabelsM A.G fp.Mc (bf.origCols l) s I (fp.brank j) (fp.bmask I (↑q.1) j (↑p + 1)) d}.card ≤ N) (x : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (hx : x ∈ (↑(colRelabel (bf.rv fp.Mc s))).range) (hxI : (columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯) x = x) : ∑ G ∈ g, ‖(fp.ballFilt l s I G j) ((layerOp (fun (m : ℕ) => fp.cumFilt l s I m) ls) x)‖ ^ 2 ≤ (1 + τ * ↑N * A.colBudget ^ 2) * ‖x‖ ^ 2

The current group Bessel inequality on one cell (blueprint line 2159, "a basic U side is bounded by current group Bessel"): for an input of the range of the relabeling supported on an active cell, the outputs of the groups certified at the cell have total square at most (1 + τ N C²) times its square.

theorem TrilinearHT.Auto.norm_sq_restrict_biUnion_empty {V : Type u_1} [Fintype V] (Gd : RealDyadicGrid) (T : Finset (ℤ × ℤ)) (hT : T = ∅) (x : ↥(ColumnL2 V)) : ‖(columnL2Restriction (⋃ J ∈ T, dyadicGridCell Gd J.1 J.2) ⋯) x‖ ^ 2 = 0

The restriction to an empty union of cells vanishes.

theorem TrilinearHT.Auto.toNat_ediv_eq {x : ℤ} (hx : 0 ≤ x) (K : ℕ) : (x / ↑K).toNat = x.toNat / K

For a nonnegative integer, the natural quotient of its natural value is the natural value of its quotient.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.blkStart_nat {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} (K t : ℕ) : A.blkStart K (A.R.1 + ↑t) = A.R.1 + ↑(K * (t / K))

The block start of a depth below the root.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.sum_sub_eq_ite {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {g gset : Finset bf.Grp} (hg : g ⊆ gset) (f : bf.Grp → ℝ) : ∑ G ∈ g, f G = ∑ G : ↥gset, if ↑G ∈ g then f ↑G else 0

A sum over a subset of the groups as a sum over the group set with indicators.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.gs'_nat {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (l : Fin 4) (G : bf.Grp) (t : ℕ) : D.gs' l G (A.R.1 + ↑t) = fp.sideState (D.Ms l G) l (D.cat l) (D.mbs l) G (D.Lf.role l) (D.Lf.layers l) D.S ⋯ D.SP (D.c l G (A.R.1 + ↑(D.S.K * (t / D.S.K)))) (A.R.1 + ↑(D.S.K * (t / D.S.K))) (A.R.1 + ↑t)

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.toLeaf_sv_basic {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) {l : Fin 4} (hl : D.u ≠ some l) (G : bf.Grp) (I : ℤ × ℤ) : D.toLeaf.sv l G I = (columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯) (D.gs' l G I.1)

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.toLeaf_sv_U {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) {l : Fin 4} (hl : D.u = some l) (G : bf.Grp) (I : ℤ × ℤ) : D.toLeaf.sv l G I = (fp.ballFilt l (D.cat l) I G (D.Lf.role l)) ((layerOp (fun (m : ℕ) => fp.cumFilt l (D.cat l) I m) (D.Lf.layers l)) (bf.Ucol fp.Mc l I))

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.sideB {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (cc : ℕ) (kk Vl : ℝ) : ℝ

The bound of the integrated side energies of a basic slot: the rolling part 2 K (20 G₀ + 32) |R| (eq:variation) and twice K times the linear-side energy V_l |R| (eq:linear-energy).

Equations

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

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.sideB0 {κ' : LocalKernelClass} {c₀ : ℕ} (A' : ActiveSetup κ' c₀) (cc : ℕ) (kk Vl : ℝ) : ℝ

The energy bound of the block inputs of a basic slot at the block starts (eq:stack-energy, lines 2393-2399 and 2415-2419): the rolling block inputs 2 (20 G₀ + 32) |R| (bounded overlap of the intervals [u_b, b], rolling_budget_blocks) and twice the linear-side energy V_l |R|, each V_{l,G,b} once; no factor K.

Equations

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

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.V_sum_le {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (qG : bf.Grp → ℕ) (l : Fin 4) (gset : Finset bf.Grp) (Bn : ℕ) (Sd : Finset ℕ) (hSd : ∀ t ∈ Sd, ∃ β < Bn, t = D.S.K * β) : ∑ b ∈ Sd, ∑ G : ↥gset, ‖(D.Ms l ↑G).blockSide (D.S.withQ0 (qG ↑G)) ⋯ D.SP (A.R.1 + ↑b) (fp.retainedV (↑G) (A.R.1 + ↑b) D.S.K) (D.c l (↑G) (A.R.1 + ↑b))‖ ^ 2 ≤ ∑ G ∈ gset, ∑ β ∈ Finset.range Bn, ‖(D.Ms l G).blockSide (D.S.withQ0 (qG G)) ⋯ D.SP (A.R.1 + ↑(D.S.K * β)) (fp.retainedV G (A.R.1 + ↑(D.S.K * β)) D.S.K) (D.c l G (A.R.1 + ↑(D.S.K * β)))‖ ^ 2

The linear-side energies of the block starts of a set of depths K β, β < B_n, are at most those of all block starts below B_n.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.basic_side_energy {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (qG : bf.Grp → ℕ) (hanc : A.AncClosed) (hne : A.cells.Nonempty) {l : Fin 4} (hl : D.u ≠ some l) (S : Finset (ℤ × ℤ)) (hS : S ⊆ A.cells) (gs : ℤ × ℤ → Finset bf.Grp) (gset : Finset bf.Grp) (hgs : ∀ I ∈ S, gs I ⊆ gset) (k Bn : ℕ) (hcertS : ∀ I ∈ S, ∀ G ∈ gs I, fp.Cert k G I) (hBn : ∀ I ∈ S, (D.toLeafQ qG).bk I < Bn) (B : (D.toLeafQ qG).BallData gset) {ra rb : ℝ} (hroot' : ∀ I ∈ A.cells, dyadicGridCell A.G I.1 I.2 ⊆ Set.Icc ra rb) {τ' : ℝ} (hτ' : 0 < τ') (hτ1 : τ' ≤ 1) (hHed : Real.exp (↑A.Dg * (1 + Real.log A.Hsrc + Real.log τ'⁻¹) ^ A.Dg) ≤ fp.Hed) (hτN : τ' * ↑B.N * A.colBudget ^ 2 ≤ 1) (cc : ℕ) (hc : 1 ≤ cc) {kk : ℝ} (hk : 1 ≤ kk) (hDm : ∀ (l : Fin 4), Real.log (2 * (D.mbs l).B) ≤ kk ^ cc) (hDb : Real.log (2 * A.colBudget) ≤ kk ^ cc) (hLs : ∀ (l : Fin 4), ↑(D.Lf.layers l).length ≤ ↑cc * (Real.log kk + 1)) {Vl : ℝ} (hlin : ∑ G ∈ gset, ∑ β ∈ Finset.range Bn, ‖(D.Ms l G).blockSide (D.S.withQ0 (qG G)) ⋯ D.SP (A.R.1 + ↑(D.S.K * β)) (fp.retainedV G (A.R.1 + ↑(D.S.K * β)) D.S.K) (D.c l G (A.R.1 + ↑(D.S.K * β)))‖ ^ 2 ≤ Vl * dyadicGridLength A.G A.R.1) : ∑ I ∈ S, ∑ G ∈ gs I, ‖(D.toLeafQ qG).sv l G I‖ ^ 2 ≤ D.sideB cc kk Vl

Blueprint line 2159 for a basic B slot of the leaf data: the sides on the cells of all groups have total square at most sideB (sideState_budget on the cells of each depth, which are disjoint, cell_budget_eq; the rolling sides by eq:variation and the fixed V_{l,G,b} by the linear-side bound eq:linear-energy).

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.block_energy {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (qG : bf.Grp → ℕ) (hanc : A.AncClosed) (hne : A.cells.Nonempty) {l : Fin 4} (S : Finset (ℤ × ℤ)) (hS : S ⊆ A.cells) (gs : ℤ × ℤ → Finset bf.Grp) (gset : Finset bf.Grp) (k Bn : ℕ) (hcertS : ∀ I ∈ S, ∀ G ∈ gs I, fp.Cert k G I) (hBn : ∀ I ∈ S, (D.toLeafQ qG).bk I < Bn) (B : (D.toLeafQ qG).BallData gset) {ra rb : ℝ} (hroot' : ∀ I ∈ A.cells, dyadicGridCell A.G I.1 I.2 ⊆ Set.Icc ra rb) {τ' : ℝ} (hτ' : 0 < τ') (hτ1 : τ' ≤ 1) (hHed : Real.exp (↑A.Dg * (1 + Real.log A.Hsrc + Real.log τ'⁻¹) ^ A.Dg) ≤ fp.Hed) (hτN : τ' * ↑B.N * A.colBudget ^ 2 ≤ 1) (cc : ℕ) (hc : 1 ≤ cc) {kk : ℝ} (hk : 1 ≤ kk) (hDm : ∀ (l : Fin 4), Real.log (2 * (D.mbs l).B) ≤ kk ^ cc) (hDb : Real.log (2 * A.colBudget) ≤ kk ^ cc) (hLs : ∀ (l : Fin 4), ↑(D.Lf.layers l).length ≤ ↑cc * (Real.log kk + 1)) {Vl : ℝ} (hlin : ∑ G ∈ gset, ∑ β ∈ Finset.range Bn, ‖(D.Ms l G).blockSide (D.S.withQ0 (qG G)) ⋯ D.SP (A.R.1 + ↑(D.S.K * β)) (fp.retainedV G (A.R.1 + ↑(D.S.K * β)) D.S.K) (D.c l G (A.R.1 + ↑(D.S.K * β)))‖ ^ 2 ≤ Vl * dyadicGridLength A.G A.R.1) : ∑ G ∈ gset, ∑ β ∈ Finset.range Bn, ‖(columnL2Restriction (⋃ J ∈ Finset.image (fun (I : ℤ × ℤ) => ancAt A.G I (A.R.1 + ↑((D.toLeafQ qG).K * β))) ({I ∈ S | G ∈ gs I ∧ (D.toLeafQ qG).bk I = β}), dyadicGridCell A.G J.1 J.2) ⋯) ((D.toLeafQ qG).Wb l G (A.R.1 + ↑((D.toLeafQ qG).K * β)))‖ ^ 2 ≤ sideB0 A cc kk Vl

Blueprint lines 2393-2399 and 2415-2419 (eq:stack-energy) for the block inputs W_b = Z_b - Z_{u_b} + V_b of a basic slot at the block starts b = R + K β, restricted to the ancestors at depth b of the cells of the block β of each group: total square at most sideB0 (sideState_budget_blocks at the depths K β, where the side state is the block input), with no factor K.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.U_side_energy {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (qG : bf.Grp → ℕ) {l : Fin 4} (hl : D.u = some l) (S : Finset (ℤ × ℤ)) (hS : S ⊆ A.cells) (gs : ℤ × ℤ → Finset bf.Grp) (gset : Finset bf.Grp) (hgs : ∀ I ∈ S, gs I ⊆ gset) (k : ℕ) (hcertS : ∀ I ∈ S, ∀ G ∈ gs I, fp.Cert k G I) (B : (D.toLeafQ qG).BallData gset) {ra rb : ℝ} (hroot' : ∀ I ∈ A.cells, dyadicGridCell A.G I.1 I.2 ⊆ Set.Icc ra rb) {τ' : ℝ} (hτ' : 0 < τ') (hτ1 : τ' ≤ 1) (hHed : Real.exp (↑A.Dg * (1 + Real.log A.Hsrc + Real.log τ'⁻¹) ^ A.Dg) ≤ fp.Hed) (hτN : τ' * ↑B.N * A.colBudget ^ 2 ≤ 1) : ∑ I ∈ S, ∑ G ∈ gs I, ‖(D.toLeafQ qG).sv l G I‖ ^ 2 ≤ 2 * ∑ I ∈ S, ‖bf.Ucol fp.Mc l I‖ ^ 2

Blueprint line 2159 for the basic U slot of the leaf data ("a basic U side is bounded by current group Bessel and eq:basic-side"): on each cell the outputs of the certified groups have total square at most twice the square of the basic side (cell_bessel).

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.toLeaf_cap {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (qG : bf.Grp → ℕ) (hanc : A.AncClosed) (hne : A.cells.Nonempty) (gset : Finset bf.Grp) (k : ℕ) (B : (D.toLeafQ qG).BallData gset) {ra rb : ℝ} (hroot' : ∀ I ∈ A.cells, dyadicGridCell A.G I.1 I.2 ⊆ Set.Icc ra rb) {τ' : ℝ} (hτ' : 0 < τ') (hτ1 : τ' ≤ 1) (hHed : Real.exp (↑A.Dg * (1 + Real.log A.Hsrc + Real.log τ'⁻¹) ^ A.Dg) ≤ fp.Hed) (hτN : τ' * ↑B.N * A.colBudget ^ 2 ≤ 1) (cc : ℕ) (hc : 1 ≤ cc) {kk : ℝ} (hk : 1 ≤ kk) (hDm : ∀ (l : Fin 4), Real.log (2 * (D.mbs l).B) ≤ kk ^ cc) (hDb : Real.log (2 * A.colBudget) ≤ kk ^ cc) (hLs : ∀ (l : Fin 4), ↑(D.Lf.layers l).length ≤ ↑cc * (Real.log kk + 1)) (l : Fin 4) : A.VarCap gset ((D.toLeafQ qG).Z l) (fun (G : bf.Grp) (J : ℤ × ℤ) => fp.Cert k G J) (capV A cc kk)

Blueprint lem:variation for the leaf data: the rolling outputs of every slot have variation capacity capV over the certified cells (varCap_basicOut).

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.sideBs {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (cc : ℕ) (kk : ℝ) (Vl : Fin 4 → ℝ) (BU : ℝ) : ℝ

The integrated side budget of the leaf data: 2 B_U for the basic U slot and sideB for the basic B slots.

Equations

• D.sideBs cc kk Vl BU = ∑ l : Fin 4, if D.u = some l then 2 * BU else D.sideB cc kk (Vl l)

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.side_estimate {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (qG : bf.Grp → ℕ) {q : ℝ} (hq2 : 2 < q) (hq3 : q < 3) (hanc : A.AncClosed) (hne : A.cells.Nonempty) {Nd N : ℕ} (hKNd : A.DepthWin Nd) (hKN : (D.toLeafQ qG).K ≤ 2 ^ N) (S : Finset (ℤ × ℤ)) (hS : S ⊆ A.cells) (hroot : ∀ I ∈ S, dyadicGridCell A.G I.1 I.2 ⊆ dyadicGridCell A.G A.R.1 A.R.2) (gs : ℤ × ℤ → Finset bf.Grp) (gset : Finset bf.Grp) (hgs : ∀ I ∈ S, gs I ⊆ gset) (Lp Jm Bn k : ℕ) (hBn : ∀ I ∈ S, (D.toLeafQ qG).bk I < Bn) (hLp : ∀ (l : Fin 4), ((D.toLeafQ qG).pe l).length ≤ Lp) (hJm : ∀ (c d : Fin 4) (i i' : ℕ), ((D.toLeafQ qG).desc c d ((D.toLeafQ qG).tOf c i) ((D.toLeafQ qG).tOf d i')).length ≤ Jm) (Act : Finset (ℤ × ℤ)) (hact : ∀ I ∈ S, I ∈ Act ∧ ∀ G ∈ gs I, G ∈ fp.groupsAt I k) {Mp : ℝ} (hMp : ∀ (y : ℝ), ↑{c ∈ Act | y ∈ dyadicGridCell A.G c.1 c.2}.card ≤ Mp) (hcertS : ∀ I ∈ S, ∀ G ∈ gs I, fp.Cert k G I) {τ cF C₀ B₀ : ℝ} (hτ : 0 ≤ τ) (hcF : 0 ≤ cF) (hC₀ : 0 < C₀) (hB₀ : 0 ≤ B₀) (hpair : ∀ I ∈ S, ∀ (c d : Fin 4), c ≠ d → (D.toLeafQ qG).u ≠ some c → (D.toLeafQ qG).u ≠ some d → PairSmall (dyadicGridLeft A.G I.1 I.2) (dyadicGridLength A.G I.1) (A.w I) c d (A.Y I c) (A.Y I d) τ) (hfar : ∀ I ∈ S, ∀ G ∈ gs I, ∀ (a b c d : Fin 4), (D.toLeafQ qG).Val a b c d → ¬(D.toLeafQ qG).Ucase c d → ∀ t ∈ (D.toLeafQ qG).pe c, ∀ t' ∈ (D.toLeafQ qG).pe d, ‖chainDefectSel (fp.Λc I) fp.P a c d (fun (l : Fin 4) => (D.toLeafQ qG).sv l G I) (bf.basicIn fp.Mc c I) (bf.basicIn fp.Mc d I) (fun (p q : ℕ) => q + 2 < p ∨ p + 2 < q) (fp.mergeStepsM (D.toLeafQ qG).cat a c d (fp.Lc + 5) I (fp.slotFiltM G ((D.toLeafQ qG).Lf.role c) I t.2) (fp.slotFiltM G ((D.toLeafQ qG).Lf.role d) I t'.2)) ((D.toLeafQ qG).sv a G I)‖ ≤ cF * (D.toLeafQ qG).ns a G I * (D.toLeafQ qG).ns b G I) (hbas : ∀ J ∈ A.cells, ∀ (l : Fin 4), (D.toLeafQ qG).u ≠ some l → ‖bf.basicIn fp.Mc l J‖ ≤ C₀ * √(dyadicGridLength A.G J.1)) (hout : ∀ I ∈ S, ∀ G ∈ gs I, ∀ (l : Fin 4), ‖(D.toLeafQ qG).out l G I‖ ≤ B₀ * √(dyadicGridLength A.G I.1)) {Np : ℝ} (hNp : ∀ (c d : Fin 4), ↑((D.toLeafQ qG).pe d).length * ↑((D.toLeafQ qG).pe c).length ≤ Np) (G₀ : bf.Grp) {Cy : ℝ} (hy : ∀ I ∈ S, ∀ (l : Fin 4), (D.toLeafQ qG).u ≠ some l → ‖bf.basicIn fp.Mc l I‖ / √(dyadicGridLength A.G I.1) ≤ Cy ∧ ‖bf.Ucol fp.Mc l I‖ / √(dyadicGridLength A.G I.1) ≤ Cy) {BU : ℝ} (hBU : ∑ I ∈ S, ∑ l : Fin 4, ‖bf.Ucol fp.Mc l I‖ ^ 2 ≤ BU) (B : (D.toLeafQ qG).BallData gset) {ra rb : ℝ} (hroot' : ∀ I ∈ A.cells, dyadicGridCell A.G I.1 I.2 ⊆ Set.Icc ra rb) {τ' : ℝ} (hτ' : 0 < τ') (hτ1 : τ' ≤ 1) (hHed : Real.exp (↑A.Dg * (1 + Real.log A.Hsrc + Real.log τ'⁻¹) ^ A.Dg) ≤ fp.Hed) (hτN : τ' * ↑B.N * A.colBudget ^ 2 ≤ 1) (cc : ℕ) (hc : 1 ≤ cc) {kk : ℝ} (hk : 1 ≤ kk) (hDm : ∀ (l : Fin 4), Real.log (2 * ((D.toLeafQ qG).mbs l).B) ≤ kk ^ cc) (hDb : Real.log (2 * A.colBudget) ≤ kk ^ cc) (hJc : ↑Jm ≤ ↑cc * (Real.log kk + 1)) (hLs : ∀ (l : Fin 4), ↑(D.Lf.layers l).length ≤ ↑cc * (Real.log kk + 1)) {Vl : Fin 4 → ℝ} (hlin : ∀ (l : Fin 4), D.u ≠ some l → ∑ G ∈ gset, ∑ β ∈ Finset.range Bn, ‖(D.Ms l G).blockSide (D.S.withQ0 (qG G)) ⋯ D.SP (A.R.1 + ↑(D.S.K * β)) (fp.retainedV G (A.R.1 + ↑(D.S.K * β)) D.S.K) (D.c l G (A.R.1 + ↑(D.S.K * β)))‖ ^ 2 ≤ Vl l * dyadicGridLength A.G A.R.1) (hP : 1 ≤ fp.P) (Γa Γb : Fin 4 → ℝ) (ΓU : ℝ) (hΓa : ∀ (a : Fin 4), (D.toLeafQ qG).u ≠ some a → fp.stackEA (SideLeafM.nOs Lp Jm) ((D.toLeafQ qG).cat a) ((D.toLeafQ qG).mbs a) (D.toLeafQ qG).Dpre N (capV A cc kk) (sideB0 A cc kk (Vl a)) ≤ (↑fp.P + 2) * Γa a * dyadicGridLength A.G A.R.1) (hΓb : ∀ (b : Fin 4), (D.toLeafQ qG).u ≠ some b → ↑(SideLeafM.nOs Lp Jm).card * (↑N * capV A cc kk + sideB0 A cc kk (Vl b)) ≤ Γb b * dyadicGridLength A.G A.R.1) (hΓU : ↑(SideLeafM.nOs Lp Jm).card * (2 * BU) ≤ ΓU * dyadicGridLength A.G A.R.1) {η p ρ : ℝ} (hη : 0 ≤ η) (hp : 2 / 3 < p) (hp1 : p ≤ 1) (hρ : 0 < ρ) (hρ1 : ρ < 1) : ∃ C ⊆ A.cells, dyadicRootLength A.G (maximalDyadicCells A.G C) ≤ 2 * ρ * dyadicGridLength A.G A.R.1 ∧ ∑ I ∈ S with ¬∃ e ∈ C, dyadicGridCell A.G I.1 I.2 ⊆ dyadicGridCell A.G e.1 e.2, dyadicGridLength A.G I.1 * min η ‖∑ σ : Fin 4 → Fin 3 with (∀ (l : Fin 4), σ l ≠ 2) ∧ {l : Fin 4 | σ l = 0}.card = 2 ∧ {l : Fin 4 | σ l = 1}.card = 2, ∑ G ∈ gs I, (fp.Λc I) fun (l : Fin 4) => if σ l = 0 then (D.toLeafQ qG).out l G I else (D.toLeafQ qG).sv l G I‖ ≤ 6 * 256 * Np * (τ + cF) * (D.toLeafQ qG).Tcap Lp Jm C₀ B₀ Cy (D.sideBs cc kk Vl BU) BU (capV A cc kk) ρ * dyadicGridLength A.G A.R.1 + 6 * ∑ a : Fin 4, ∑ b : Fin 4, ∑ e : Fin 4, (D.toLeafQ qG).nearBnd hq2 hq3 Nd N Lp Jm Mp C₀ (ρ / 64) Γa Γb ΓU a b e + η ^ (1 - p) * ((D.toLeafQ qG).Tcap Lp Jm C₀ B₀ Cy (D.sideBs cc kk Vl BU) BU (capV A cc kk) ρ ^ (p / 2) * (D.toLeafQ qG).Tcap Lp Jm C₀ B₀ Cy (D.sideBs cc kk Vl BU) BU (capV A cc kk) ρ ^ (p / 2) * (D.toLeafQ qG).Tcap Lp Jm C₀ B₀ Cy (D.sideBs cc kk Vl BU) BU (capV A cc kk) ρ ^ (p / 2) * dyadicGridLength A.G A.R.1) ∧ (∀ (core err : ℤ × ℤ → bf.Grp → Fin 4 → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))), ∀ S' ⊆ {I ∈ S | ¬∃ e ∈ C, dyadicGridCell A.G I.1 I.2 ⊆ dyadicGridCell A.G e.1 e.2}, ∀ {Bc : ℝ}, 0 ≤ Bc → (∀ I ∈ S', ∀ G ∈ gs I, ∀ (l : Fin 4), ‖core I G l‖ ≤ Bc * √(dyadicGridLength A.G I.1)) → ∑ I ∈ S', dyadicGridLength A.G I.1 * min η (∑ σ : Fin 4 → Fin 3 with (∀ (l : Fin 4), σ l ≠ 2) ∧ 3 ≤ patternCount σ 1, ‖∑ G ∈ gs I, (fp.Λc I) (patternPiece (core I G) (fun (l : Fin 4) => (D.toLeafQ qG).sv l G I) (err I G) σ)‖) ≤ η ^ (1 - p) * (81 * localFormUniformConstant κ' * max Bc √((D.toLeafQ qG).Tcap Lp Jm C₀ B₀ Cy (D.sideBs cc kk Vl BU) BU (capV A cc kk) ρ)) ^ p * ((D.toLeafQ qG).Tcap Lp Jm C₀ B₀ Cy (D.sideBs cc kk Vl BU) BU (capV A cc kk) ρ ^ (p / 2) * (D.toLeafQ qG).Tcap Lp Jm C₀ B₀ Cy (D.sideBs cc kk Vl BU) BU (capV A cc kk) ρ ^ (p / 2) * (D.toLeafQ qG).Tcap Lp Jm C₀ B₀ Cy (D.sideBs cc kk Vl BU) BU (capV A cc kk) ρ ^ (p / 2) * dyadicGridLength A.G A.R.1)) ∧ ∀ (x : ℝ), ∑ I ∈ {I ∈ S | ¬∃ e ∈ C, dyadicGridCell A.G I.1 I.2 ⊆ dyadicGridCell A.G e.1 e.2} with x ∈ dyadicGridCell A.G I.1 I.2, ∑ G ∈ gs I, (D.toLeafQ qG).s2 G I ≤ (D.toLeafQ qG).Tcap Lp Jm C₀ B₀ Cy (D.sideBs cc kk Vl BU) BU (capV A cc kk) ρ

Blueprint lines 2446-2456, the side estimate of one localization leaf on the side states (eq:sides): leaf_side_estimateM for the leaf data toLeaf of the side input, with the variation capacities of the rolling outputs (toLeaf_cap, lem:variation), the energies of the block inputs (block_energy) and of the sides (basic_side_energy, U_side_energy) derived from eq:variation, the linear-side bound eq:linear-energy (hlin), current group Bessel and the basic-side energy B_U (eq:basic-side); the joint side budget is sideBs. The outputs are the cut family, the two-side bound, the three-side power bound on retained cells with bounded cores, and the side cap on the retained paths.

The far bound of the side-state leaf data (blueprint lines 2252-2258)

theorem TrilinearHT.Auto.le_of_forall_pos_mul_le {X K a b : ℝ} (h : ∀ (ε : ℝ), 0 < ε → X ≤ K * ((2 * a + ε) * (b + ε))) : X ≤ K * (2 * a * b)

A bound valid with every positive enlargement of the two sizes holds for the sizes.

theorem TrilinearHT.Auto.eLpNorm_augPhys_le_ns {V : Type u_1} [Fintype V] (Gd : RealDyadicGrid) (I : ℤ × ℤ) (x : ↥(ColumnL2 V)) : MeasureTheory.eLpNorm (augPhys x) 2 (normalizedIntervalMeasure (dyadicGridLeft Gd I.1 I.2) (dyadicGridLength Gd I.1)) ≤ ENNReal.ofReal (‖x‖ / √(dyadicGridLength Gd I.1))

The normalized L² size of the physical part on a cell is at most the normalized size.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideLeafM.far_bound {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (T : fp.SideLeafM) {fuel : ℕ} {up₀ : Fin 4} {s : ℕ} (hLf : T.Lf = leafAt fuel fp.Lc up₀ s) (hmH : 2 * fuel + 2 ≤ fp.mH) (hT : ∀ (l : Fin 4), ∀ e ∈ T.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 ∈ T.cat l, bf.occAvail (↑e.tag.2) e.tag.1) (S : Finset (ℤ × ℤ)) (gs : ℤ × ℤ → Finset bf.Grp) (huse : ∀ I ∈ S, ∀ G ∈ gs I, fp.ActualUse G I) {τ : ℕ → ℝ} (hpass : ∀ I ∈ S, ∀ (l : Fin 4), T.u ≠ some l → ∀ (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 (T.cat l)) {τH : ℝ} (hτH : 0 ≤ τH) {Bh : Type} (gE : ℤ × ℤ → Bh → bf.Grp) (hgE : ∀ I ∈ S, ∀ G ∈ gs I, ∃ (i : Bh), gE I i = G) (hhpass : ∀ I ∈ S, ∀ (a : Fin 4) (w : fp.HelperName I Bh), (fp.helperOf a I (fun (i : Bh) => T.sv a (gE I i) I) w).Pass A.G (bf.origCols a) I A.csrc A.Hsrc bf.vtag (A.w I) τH fp.mH (T.cat a)) {τ₃ 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 : ∀ I ∈ S, ∀ (l : Fin 4), ‖bf.basicIn fp.Mc l I‖ / √(dyadicGridLength A.G I.1) ≤ Sz) (d₀ : bf.Vtx) {NH : ℝ} (hNl : ∀ I ∈ S, ∀ (l : Fin 4), ∀ r ≤ fp.Lc + 4, ∀ (M : bf.Vtx → Prop), ↑(mainLabelsM A.G fp.Mc (bf.origCols l) (T.cat l) I r M d₀).card ≤ n r) (hNH : ∀ I ∈ S, ∀ (a : Fin 4) (M : bf.Vtx → Prop), ↑(mainLabelsM A.G fp.Mc (bf.origCols a) (T.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) (I : ℤ × ℤ) : I ∈ S → ∀ G ∈ gs I, ∀ (a b c d : Fin 4), T.Val a b c d → ¬T.Ucase c d → ∀ t ∈ T.pe c, ∀ t' ∈ T.pe d, ‖chainDefectSel (fp.Λc I) fp.P a c d (fun (l : Fin 4) => T.sv l G I) (bf.basicIn fp.Mc c I) (bf.basicIn fp.Mc d I) (fun (p q : ℕ) => q + 2 < p ∨ p + 2 < q) (fp.mergeStepsM T.cat a c d (fp.Lc + 5) I (fp.slotFiltM G (T.Lf.role c) I t.2) (fp.slotFiltM G (T.Lf.role d) I t'.2)) (T.sv a G I)‖ ≤ (2 * ↑fuel + 2) * ((↑fp.P + 1) ^ 2 * (16 * τ₃ * Sz ^ 2)) * T.ns a G I * T.ns b G I

Blueprint lines 2252-2258 on leaf data at a leaf of the guarded search (leaf_far_search): when the catalogs pass all residual tests of the basic inputs and all helper tests whose bases are the cell sides (the instantiated helper catalog, lines 2167-2169), the far band defects of the transfer steps of every valid pattern of an actual use have absolute value at most c_F n_a n_b with c_F = (2 fuel + 2) (P + 1)² 16 τ₃ S_z² and the normalized side sizes n.

The sizes of the leaf inputs (blueprint prop:base, lines 1607-1616)

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.norm_basicIn_le {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} (bf : A.BasicFamilies) (Mc : ℕ) (l : Fin 4) {I : ℤ × ℤ} (hI : I ∈ A.cells) {CF : ℝ} (hCF : 0 ≤ CF) (hnorm : ∀ (jb : Fin 2), ‖(columnL2Restriction (dyadicGridCell A.G I.1 I.2) ⋯) (bf.P l jb).Z‖ ^ 2 ≤ CF * dyadicGridLength A.G I.1) : ‖bf.basicIn Mc l I‖ ≤ 2 * √CF * √(dyadicGridLength A.G I.1)

On a normalized root (‖1_U F_{l,j}‖² ≤ C_F |U| on the active cells) the basic inputs have normalized size at most 2 √C_F (blueprint prop:base, "their normalized L² sizes are bounded").

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.normF {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} (bf : A.BasicFamilies) (l : Fin 4) (jb : Fin 2) {U : ℤ × ℤ} (hU : U ∈ A.cells) : ‖(columnL2Restriction (dyadicGridCell A.G U.1 U.2) ⋯) (bf.P l jb).Z‖ ^ 2 ≤ 1 * dyadicGridLength A.G U.1

The basic family inputs are normalized on every cell of the setup (blueprint prop:base, "their normalized L² sizes are bounded"): ‖1_U F_{l,j}‖² ≤ |U| (the hnormF input with C_F = 1).

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.norm_sq_Ucol_le {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} (bf : A.BasicFamilies) (Mc : ℕ) (l : Fin 4) (I : ℤ × ℤ) : ‖bf.Ucol Mc l I‖ ^ 2 ≤ dyadicGridLength A.G I.1 * (MeasureTheory.eLpNorm (A.U l I) 2 (A.μ I)).toReal ^ 2

The squared norm of a basic side is its length times its normalized square size.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.norm_Ucol_le {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} (bf : A.BasicFamilies) (Mc : ℕ) (l : Fin 4) (I : ℤ × ℤ) : ‖bf.Ucol Mc l I‖ ≤ A.S * √(dyadicGridLength A.G I.1)

The basic sides have normalized size at most S.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.Ucol_energy {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} (bf : A.BasicFamilies) {η₀ E : ℝ} (h : A.SubRootProps η₀ E) (Mc : ℕ) (S : Finset (ℤ × ℤ)) (hS : S ⊆ A.cells) : ∑ I ∈ S, ∑ l : Fin 4, ‖bf.Ucol Mc l I‖ ^ 2 ≤ 4 * E * dyadicGridLength A.G A.R.1

Blueprint eq:basic-side for the basic sides of the four slots on a set of active cells: total square at most 4 E |R|.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideLeafM.norm_out_le {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (T : fp.SideLeafM) (l : Fin 4) (G : bf.Grp) (I : ℤ × ℤ) : ‖T.out l G I‖ ≤ ‖T.xin l I‖

The whole leaf outputs are at most the slot inputs (contractions).

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.farC {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (fuel : ℕ) (τ₃ Sz : ℝ) : ℝ

The far constant c_F = (2 fuel + 2) (P + 1)² 16 τ₃ S_z² of far_bound.

Equations

• fp.farC fuel τ₃ Sz = (2 * ↑fuel + 2) * ((↑fp.P + 1) ^ 2 * (16 * τ₃ * Sz ^ 2))

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.Tside {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (qG : bf.Grp → ℕ) (Lp Jm : ℕ) (CF E : ℝ) (cc : ℕ) (kk : ℝ) (Vl : Fin 4 → ℝ) (ρ : ℝ) : ℝ

The joint path cap of the side estimate on the side states: T_c of Tcap with the basic sizes 2 √C_F (normalized root), the output and side sizes max(2 √C_F, S) and the basic-side energy 4 E |R| (eq:basic-side).

Equations

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

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.side_estimate_leaf {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (qG : bf.Grp → ℕ) {q : ℝ} (hq2 : 2 < q) (hq3 : q < 3) (hanc : A.AncClosed) (hne : A.cells.Nonempty) {fuel : ℕ} {up₀ : Fin 4} {s : ℕ} (hLf : D.Lf = leafAt fuel fp.Lc up₀ s) (hmH : 2 * fuel + 2 ≤ fp.mH) {Nd N : ℕ} (hKNd : A.DepthWin Nd) (hKN : D.S.K ≤ 2 ^ N) (S : Finset (ℤ × ℤ)) (hS : S ⊆ A.cells) (hroot : ∀ I ∈ S, dyadicGridCell A.G I.1 I.2 ⊆ dyadicGridCell A.G A.R.1 A.R.2) (gs : ℤ × ℤ → Finset bf.Grp) (gset : Finset bf.Grp) (hgs : ∀ I ∈ S, gs I ⊆ gset) (Lp Jm Bn k : ℕ) (hBn : ∀ I ∈ S, (D.toLeafQ qG).bk I < Bn) (hLp : ∀ (l : Fin 4), ((D.toLeafQ qG).pe l).length ≤ Lp) (hJm : ∀ (c d : Fin 4) (i i' : ℕ), ((D.toLeafQ qG).desc c d ((D.toLeafQ qG).tOf c i) ((D.toLeafQ qG).tOf d i')).length ≤ Jm) (Act : Finset (ℤ × ℤ)) (hact : ∀ I ∈ S, I ∈ Act ∧ ∀ G ∈ gs I, G ∈ fp.groupsAt I k) {Mp : ℝ} (hMp : ∀ (y : ℝ), ↑{c ∈ Act | y ∈ dyadicGridCell A.G c.1 c.2}.card ≤ Mp) (hcertS : ∀ I ∈ S, ∀ G ∈ gs I, fp.Cert k G I) (huse : ∀ I ∈ S, ∀ G ∈ gs I, fp.ActualUse G I) {Np : ℝ} (hNp : ∀ (c d : Fin 4), ↑((D.toLeafQ qG).pe d).length * ↑((D.toLeafQ qG).pe c).length ≤ Np) {τ : ℝ} (hτ : 0 ≤ τ) (hpair : ∀ I ∈ S, ∀ (c d : Fin 4), c ≠ d → D.u ≠ some c → D.u ≠ some d → PairSmall (dyadicGridLeft A.G I.1 I.2) (dyadicGridLength A.G I.1) (A.w I) c d (A.Y I c) (A.Y I d) τ) {CF : ℝ} (hCF : 0 < CF) (hnormF : ∀ (l : Fin 4) (jb : Fin 2), ∀ U ∈ A.cells, ‖(columnL2Restriction (dyadicGridCell A.G U.1 U.2) ⋯) (bf.P l jb).Z‖ ^ 2 ≤ CF * dyadicGridLength A.G U.1) {η₀ E : ℝ} (hsub : A.SubRootProps η₀ E) {τr : ℕ → ℝ} (hpass : ∀ I ∈ S, ∀ (l : Fin 4), D.u ≠ some l → ∀ (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) (τr (fp.testOf l I (fun (x : Unit) => bf.basicIn fp.Mc l I) w).r) fp.mH (D.cat l)) {τH : ℝ} (hτH : 0 ≤ τH) {Bh : Type} (gE : ℤ × ℤ → Bh → bf.Grp) (hgE : ∀ I ∈ S, ∀ G ∈ gs I, ∃ (i : Bh), gE I i = G) (hhpass : ∀ I ∈ S, ∀ (a : Fin 4) (w : fp.HelperName I Bh), (fp.helperOf a I (fun (i : Bh) => (D.toLeafQ qG).sv a (gE I i) I) w).Pass A.G (bf.origCols a) I A.csrc A.Hsrc bf.vtag (A.w I) τH fp.mH (D.cat a)) {τ₃ Sz : ℝ} (hτ0 : ∀ (R : ℕ), 0 ≤ τr R) (n : ℕ → ℝ) (hn : Monotone n) (hn0 : 2 * A.colBudget ≤ n 0) (hτr : ∀ (R : ℕ), 1 ≤ R → R ≤ fp.Lc + 4 → τr R * (A.colBudget * √(n (R - 1))) ≤ τ₃) (hτH' : τH * (A.colBudget * √(n (fp.Lc + 4))) ≤ τ₃) (hSz : 2 * √CF ≤ Sz) (d₀ : bf.Vtx) {NH : ℝ} (hNl : ∀ I ∈ S, ∀ (l : Fin 4), ∀ r ≤ fp.Lc + 4, ∀ (M : bf.Vtx → Prop), ↑(mainLabelsM A.G fp.Mc (bf.origCols l) (D.cat l) I r M d₀).card ≤ n r) (hNH : ∀ I ∈ S, ∀ (a : Fin 4) (M : bf.Vtx → Prop), ↑(mainLabelsM A.G fp.Mc (bf.origCols a) (D.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) (G₀ : bf.Grp) (B : (D.toLeafQ qG).BallData gset) {ra rb : ℝ} (hroot' : ∀ I ∈ A.cells, dyadicGridCell A.G I.1 I.2 ⊆ Set.Icc ra rb) {τ' : ℝ} (hτ' : 0 < τ') (hτ1 : τ' ≤ 1) (hHed : Real.exp (↑A.Dg * (1 + Real.log A.Hsrc + Real.log τ'⁻¹) ^ A.Dg) ≤ fp.Hed) (hτN : τ' * ↑B.N * A.colBudget ^ 2 ≤ 1) (cc : ℕ) (hc : 1 ≤ cc) {kk : ℝ} (hk : 1 ≤ kk) (hDm : ∀ (l : Fin 4), Real.log (2 * (D.mbs l).B) ≤ kk ^ cc) (hDb : Real.log (2 * A.colBudget) ≤ kk ^ cc) (hJc : ↑Jm ≤ ↑cc * (Real.log kk + 1)) (hLs : ∀ (l : Fin 4), ↑(D.Lf.layers l).length ≤ ↑cc * (Real.log kk + 1)) {Vl : Fin 4 → ℝ} (hlin : ∀ (l : Fin 4), D.u ≠ some l → ∑ G ∈ gset, ∑ β ∈ Finset.range Bn, ‖(D.Ms l G).blockSide (D.S.withQ0 (qG G)) ⋯ D.SP (A.R.1 + ↑(D.S.K * β)) (fp.retainedV G (A.R.1 + ↑(D.S.K * β)) D.S.K) (D.c l G (A.R.1 + ↑(D.S.K * β)))‖ ^ 2 ≤ Vl l * dyadicGridLength A.G A.R.1) (hP : 1 ≤ fp.P) (Γa Γb : Fin 4 → ℝ) (ΓU : ℝ) (hΓa : ∀ (a : Fin 4), D.u ≠ some a → fp.stackEA (SideLeafM.nOs Lp Jm) (D.cat a) (D.mbs a) (D.toLeafQ qG).Dpre N (capV A cc kk) (sideB0 A cc kk (Vl a)) ≤ (↑fp.P + 2) * Γa a * dyadicGridLength A.G A.R.1) (hΓb : ∀ (b : Fin 4), D.u ≠ some b → ↑(SideLeafM.nOs Lp Jm).card * (↑N * capV A cc kk + sideB0 A cc kk (Vl b)) ≤ Γb b * dyadicGridLength A.G A.R.1) (hΓU : ↑(SideLeafM.nOs Lp Jm).card * (2 * (4 * E * dyadicGridLength A.G A.R.1)) ≤ ΓU * dyadicGridLength A.G A.R.1) {η p ρ : ℝ} (hη : 0 ≤ η) (hp : 2 / 3 < p) (hp1 : p ≤ 1) (hρ : 0 < ρ) (hρ1 : ρ < 1) : ∃ C ⊆ A.cells, dyadicRootLength A.G (maximalDyadicCells A.G C) ≤ 2 * ρ * dyadicGridLength A.G A.R.1 ∧ ∑ I ∈ S with ¬∃ e ∈ C, dyadicGridCell A.G I.1 I.2 ⊆ dyadicGridCell A.G e.1 e.2, dyadicGridLength A.G I.1 * min η ‖∑ σ : Fin 4 → Fin 3 with (∀ (l : Fin 4), σ l ≠ 2) ∧ {l : Fin 4 | σ l = 0}.card = 2 ∧ {l : Fin 4 | σ l = 1}.card = 2, ∑ G ∈ gs I, (fp.Λc I) fun (l : Fin 4) => if σ l = 0 then (D.toLeafQ qG).out l G I else (D.toLeafQ qG).sv l G I‖ ≤ 6 * 256 * Np * (τ + fp.farC fuel τ₃ Sz) * D.Tside qG Lp Jm CF E cc kk Vl ρ * dyadicGridLength A.G A.R.1 + 6 * ∑ a : Fin 4, ∑ b : Fin 4, ∑ e : Fin 4, (D.toLeafQ qG).nearBnd hq2 hq3 Nd N Lp Jm Mp (2 * √CF) (ρ / 64) Γa Γb ΓU a b e + η ^ (1 - p) * (D.Tside qG Lp Jm CF E cc kk Vl ρ ^ (p / 2) * D.Tside qG Lp Jm CF E cc kk Vl ρ ^ (p / 2) * D.Tside qG Lp Jm CF E cc kk Vl ρ ^ (p / 2) * dyadicGridLength A.G A.R.1) ∧ (∀ (core err : ℤ × ℤ → bf.Grp → Fin 4 → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))), ∀ S' ⊆ {I ∈ S | ¬∃ e ∈ C, dyadicGridCell A.G I.1 I.2 ⊆ dyadicGridCell A.G e.1 e.2}, ∀ {Bc : ℝ}, 0 ≤ Bc → (∀ I ∈ S', ∀ G ∈ gs I, ∀ (l : Fin 4), ‖core I G l‖ ≤ Bc * √(dyadicGridLength A.G I.1)) → ∑ I ∈ S', dyadicGridLength A.G I.1 * min η (∑ σ : Fin 4 → Fin 3 with (∀ (l : Fin 4), σ l ≠ 2) ∧ 3 ≤ patternCount σ 1, ‖∑ G ∈ gs I, (fp.Λc I) (patternPiece (core I G) (fun (l : Fin 4) => (D.toLeafQ qG).sv l G I) (err I G) σ)‖) ≤ η ^ (1 - p) * (81 * localFormUniformConstant κ' * max Bc √(D.Tside qG Lp Jm CF E cc kk Vl ρ)) ^ p * (D.Tside qG Lp Jm CF E cc kk Vl ρ ^ (p / 2) * D.Tside qG Lp Jm CF E cc kk Vl ρ ^ (p / 2) * D.Tside qG Lp Jm CF E cc kk Vl ρ ^ (p / 2) * dyadicGridLength A.G A.R.1)) ∧ ∀ (x : ℝ), ∑ I ∈ {I ∈ S | ¬∃ e ∈ C, dyadicGridCell A.G I.1 I.2 ⊆ dyadicGridCell A.G e.1 e.2} with x ∈ dyadicGridCell A.G I.1 I.2, ∑ G ∈ gs I, (D.toLeafQ qG).s2 G I ≤ D.Tside qG Lp Jm CF E cc kk Vl ρ

Blueprint lines 2446-2456, the unconditional side estimate of one localization leaf of the guarded search on its side states. The input consists of the finite base data (pair smallness of the full arguments hpair, the normalized root hnormF and the basic-side energy hsub, prop:base), the fixed localization leaf (hLf, with its actual uses, certificates and counts), the linear-side bound (hlin, prop:linear-side) and the instantiated helper catalog (all residual tests of the basic inputs hpass and all helper tests on the cell sides hhpass pass). The outputs, on one cut family of root fraction at most 2ρ, are:

• the two-side bound: the pair-small and far absolute bound (far_bound), six times the critical near-band bounds (eq:near-band) and the power cost of the three strong factors (with the freeze and restoration terms and the frozen complements);
• the power bound of the patterns with at least three sides on retained cells with bounded cores;
• the side cap eq:side-cap on the retained paths, with the joint path cap Tside.

def TrilinearHT.Auto.ActiveSetup.restrictTo {κ : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ c₀) (R' : ℤ × ℤ) (C : Finset (ℤ × ℤ)) (hC : ∀ I ∈ C, I ∈ A.cells ∧ dyadicGridCell A.G I.1 I.2 ⊆ dyadicGridCell A.G R'.1 R'.2) : ActiveSetup κ c₀

The restriction of an active setup to a sub-root R' and a subfamily C of its cells below R' (blueprint line 2451, "every hypothesis is available anew on a normalized subroot", and prop:normalized, lines 2840-2842: restarts act on the original base summands with unchanged basic arguments and inherited lists).

Equations

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

noncomputable def TrilinearHT.Auto.ActiveSetup.below {κ : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ c₀) (R' : ℤ × ℤ) : ActiveSetup κ c₀

The restriction of an active setup to all of its cells below a sub-root R'.

Equations

• A.below R' = A.restrictTo R' ({I ∈ A.cells | TrilinearHT.Auto.dyadicGridCell A.G I.1 I.2 ⊆ TrilinearHT.Auto.dyadicGridCell A.G R'.1 R'.2}) ⋯

@[simp]

theorem TrilinearHT.Auto.ActiveSetup.below_cells {κ : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ c₀) (R' : ℤ × ℤ) : (A.below R').cells = {I ∈ A.cells | dyadicGridCell A.G I.1 I.2 ⊆ dyadicGridCell A.G R'.1 R'.2}

@[simp]

theorem TrilinearHT.Auto.ActiveSetup.below_R {κ : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ c₀) (R' : ℤ × ℤ) : (A.below R').R = R'