Section 12.3 (b): Finite same-tag catalogs on the main columns

This file was automatically generated by Claude.

Formalization of blueprint Section 12, "Curvature localization" (sec:localization), subsection 3, "Finite same-tag catalogs" (lines 1796-1836) of blueprint/formalization_blueprint.tex, on the main columns: the rank-r main projections use the original basic columns of rank zero with their own private weights together with the catalog templates of private weight one (lines 1805-1806), the vertices are the original basic column occurrences (line 1676), and the catalog tests act on augmented bases (lines 1809-1815). Split from Sec12_3FiniteSameTagCatalogs for size.

Main columns: original columns and templates (blueprint lines 1803-1809)

noncomputable def TrilinearHT.Auto.wColumn {W : Type u_1} [Fintype W] (s : Set ℝ) (φ : W → ℝ → ℂ) (ε : W → ℝ) (x : W) : ↥(ColumnL2 W)

The weighted column 1_s (φ_x, √ε_x e_x) of the label x (blueprint line 473), zero when it is not square integrable.

Equations

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

theorem TrilinearHT.Auto.wColumn_coeFn {W : Type u_1} [Fintype W] {s : Set ℝ} {φ : W → ℝ → ℂ} {ε : W → ℝ} {x : W} (h : MeasureTheory.MemLp (s.indicator (privateColumnValue φ ε x)) 2 MeasureTheory.volume) : ↑↑(wColumn s φ ε x) =ᵐ[MeasureTheory.volume] s.indicator (privateColumnValue φ ε x)

theorem TrilinearHT.Auto.norm_privateColumnValue_le {W : Type u_1} [Fintype W] (φ : W → ℝ → ℂ) (ε : W → ℝ) (x : W) (y : ℝ) : ‖privateColumnValue φ ε x y‖ ≤ ‖φ x y‖ + √(ε x)

theorem TrilinearHT.Auto.wColumn_memLp {W : Type u_1} [Fintype W] {s : Set ℝ} (hs : MeasurableSet s) (hsv : MeasureTheory.volume s < ⊤) {φ : W → ℝ → ℂ} (ε : W → ℝ) {x : W} (hφ : Measurable (φ x)) {C : ℝ} (hC : ∀ y ∈ s, ‖φ x y‖ ≤ C) : MeasureTheory.MemLp (s.indicator (privateColumnValue φ ε x)) 2 MeasureTheory.volume

A scalar bounded on a set of finite measure gives a square-integrable column.

theorem TrilinearHT.Auto.wColumn_congr {W : Type u_1} [Fintype W] {s : Set ℝ} {φ φ' : W → ℝ → ℂ} {ε ε' : W → ℝ} {x : W} (hφ : φ x = φ' x) (hε : ε x = ε' x) : wColumn s φ ε x = wColumn s φ' ε' x

The column of a label depends only on its own scalar and weight.

theorem TrilinearHT.Auto.wColumn_some_ne {W : Type u_1} [Fintype W] {s : Set ℝ} {φ : W → ℝ → ℂ} {ε : W → ℝ} {x x' : W} (hne : x' ≠ x) : ∀ᵐ (y : ℝ), (↑↑(wColumn s φ ε x) y).ofLp (some x') = 0

The private coordinates of a column vanish off its own label.

structure TrilinearHT.Auto.OrigCols (V : Type) [Fintype V] (Tg : Type u_2) : Type u_2

The original columns of a basic family as seen by the catalogs: scalars, private weights, availability at the cells and the vertex (tag) of an available label at a cell (blueprint lines 1676-1680, 1805).

• scalar : V → ℝ → ℂ

  Scalar function carried by each original column label.

• weight : V → ℝ

  Positive private-coordinate weight of each original column.

• weight_pos (v : V) : 0 < self.weight v
• avail : ℤ × ℤ → V → Prop

  Availability of each original column label at a dyadic cell.

• tag : ℤ × ℤ → V → Tg

  Cell-dependent chart tag of each original column.

noncomputable def TrilinearHT.Auto.mainScalar {V : Type} [Fintype V] {Tg : Type u_1} (Mc : ℕ) (O : OrigCols V Tg) (s : List (CatCol Tg)) : V ⊕ Fin Mc → ℝ → ℂ

The scalars of the main labels: original scalars and catalog atoms.

Equations

• TrilinearHT.Auto.mainScalar Mc O s = Sum.elim O.scalar fun (n : Fin Mc) => TrilinearHT.Auto.catAtom s ↑n

def TrilinearHT.Auto.mainWeight {V : Type} [Fintype V] {Tg : Type u_1} (Mc : ℕ) (O : OrigCols V Tg) : V ⊕ Fin Mc → ℝ

The private weights of the main labels: original weights, and weight one for new labels (blueprint line 1806).

Equations

• TrilinearHT.Auto.mainWeight Mc O = Sum.elim O.weight fun (x : Fin Mc) => 1

noncomputable def TrilinearHT.Auto.mainCol {V : Type} [Fintype V] {Tg : Type u_1} (G : RealDyadicGrid) (Mc : ℕ) (O : OrigCols V Tg) (s : List (CatCol Tg)) (I : ℤ × ℤ) (x : V ⊕ Fin Mc) : ↥(ColumnL2 (V ⊕ Fin Mc))

The main column of a label at the cell I.

Equations

• TrilinearHT.Auto.mainCol G Mc O s I x = TrilinearHT.Auto.wColumn (TrilinearHT.Auto.dyadicGridCell G I.1 I.2) (TrilinearHT.Auto.mainScalar Mc O s) (TrilinearHT.Auto.mainWeight Mc O) x

def TrilinearHT.Auto.mainSel {V : Type} [Fintype V] {Tg : Type u_1} (G : RealDyadicGrid) (Mc : ℕ) (O : OrigCols V Tg) (s : List (CatCol Tg)) (I : ℤ × ℤ) (r : ℕ) (M : Tg → Prop) : Set ↥(ColumnL2 (V ⊕ Fin Mc))

The available main columns at the cell I of rank at most r with tag in the vertex mask M: the original columns available at I whose vertex lies in M (rank zero) and the catalog templates born above I of rank at most r with tag in M (blueprint lines 1805-1806).

Equations

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

noncomputable def TrilinearHT.Auto.mainRange {V : Type} [Fintype V] {Tg : Type u_1} (G : RealDyadicGrid) (Mc : ℕ) (O : OrigCols V Tg) (s : List (CatCol Tg)) (I : ℤ × ℤ) (r : ℕ) (M : Tg → Prop) : Submodule ℂ ↥(ColumnL2 (V ⊕ Fin Mc))

The range of the rank-r main projection with vertex mask M at the cell I.

Equations

• TrilinearHT.Auto.mainRange G Mc O s I r M = Submodule.span ℂ (TrilinearHT.Auto.mainSel G Mc O s I r M)

theorem TrilinearHT.Auto.mainSel_finite {V : Type} [Fintype V] {Tg : Type u_1} (G : RealDyadicGrid) (Mc : ℕ) (O : OrigCols V Tg) (s : List (CatCol Tg)) (I : ℤ × ℤ) (r : ℕ) (M : Tg → Prop) : (mainSel G Mc O s I r M).Finite

instance TrilinearHT.Auto.instFiniteDimensionalComplexSubtypeAEEqFunRealColumnHilbertSumFinVolumeMemAddSubgroupColumnL2SubmoduleMainRange {V : Type} [Fintype V] {Tg : Type u_1} (G : RealDyadicGrid) (Mc : ℕ) (O : OrigCols V Tg) (s : List (CatCol Tg)) (I : ℤ × ℤ) (r : ℕ) (M : Tg → Prop) : FiniteDimensional ℂ ↥(mainRange G Mc O s I r M)

noncomputable def TrilinearHT.Auto.mainProj {V : Type} [Fintype V] {Tg : Type u_1} (G : RealDyadicGrid) (Mc : ℕ) (O : OrigCols V Tg) (s : List (CatCol Tg)) (I : ℤ × ℤ) (r : ℕ) (M : Tg → Prop) : ↥(ColumnL2 (V ⊕ Fin Mc)) →L[ℂ] ↥(ColumnL2 (V ⊕ Fin Mc))

The rank-r main projection with vertex mask M at the cell I (blueprint line 1806: a rank-r projection uses all available columns of ranks at most r in its vertex mask).

Equations

• TrilinearHT.Auto.mainProj G Mc O s I r M = (TrilinearHT.Auto.mainRange G Mc O s I r M).starProjection

theorem TrilinearHT.Auto.mainProj_isStarProjection {V : Type} [Fintype V] {Tg : Type u_1} (G : RealDyadicGrid) (Mc : ℕ) (O : OrigCols V Tg) (s : List (CatCol Tg)) (I : ℤ × ℤ) (r : ℕ) (M : Tg → Prop) : IsStarProjection (mainProj G Mc O s I r M)

theorem TrilinearHT.Auto.catAtom_append_of_lt {Tg : Type u_1} (s : List (CatCol Tg)) (d : CatCol Tg) {n : ℕ} (hn : n < s.length) : catAtom (s ++ [d]) n = catAtom s n

theorem TrilinearHT.Auto.mainCol_append {V : Type} [Fintype V] {Tg : Type u_1} (G : RealDyadicGrid) (Mc : ℕ) (O : OrigCols V Tg) (s : List (CatCol Tg)) (d : CatCol Tg) (I : ℤ × ℤ) (x : V ⊕ Fin Mc) (hx : ∀ (n : Fin Mc), x = Sum.inr n → ↑n < s.length) : mainCol G Mc O (s ++ [d]) I x = mainCol G Mc O s I x

theorem TrilinearHT.Auto.mainSel_append {V : Type} [Fintype V] {Tg : Type u_1} (G : RealDyadicGrid) (Mc : ℕ) (O : OrigCols V Tg) (s : List (CatCol Tg)) (d : CatCol Tg) (I : ℤ × ℤ) (r : ℕ) (M : Tg → Prop) : mainSel G Mc O s I r M ⊆ mainSel G Mc O (s ++ [d]) I r M

theorem TrilinearHT.Auto.mainRange_append {V : Type} [Fintype V] {Tg : Type u_1} (G : RealDyadicGrid) (Mc : ℕ) (O : OrigCols V Tg) (s : List (CatCol Tg)) (d : CatCol Tg) (I : ℤ × ℤ) (r : ℕ) (M : Tg → Prop) : mainRange G Mc O s I r M ≤ mainRange G Mc O (s ++ [d]) I r M

theorem TrilinearHT.Auto.mainProj_nest {V : Type} [Fintype V] {Tg : Type u_1} (G : RealDyadicGrid) (Mc : ℕ) (O : OrigCols V Tg) (s : List (CatCol Tg)) (d : CatCol Tg) (I : ℤ × ℤ) (r : ℕ) (M : Tg → Prop) : mainProj G Mc O s I r M ∘SL mainProj G Mc O (s ++ [d]) I r M = mainProj G Mc O s I r M

Main projections are nested in the insertion index (blueprint line 1828).

theorem TrilinearHT.Auto.mainRange_mono {V : Type} [Fintype V] {Tg : Type u_1} (G : RealDyadicGrid) (Mc : ℕ) (O : OrigCols V Tg) (s : List (CatCol Tg)) (I : ℤ × ℤ) {r r' : ℕ} {M M' : Tg → Prop} (hr : r ≤ r') (hM : ∀ (t : Tg), M t → M' t) : mainRange G Mc O s I r M ≤ mainRange G Mc O s I r' M'

Main projections grow with the rank and the vertex mask (nested in the pad, blueprint line 1807).

def TrilinearHT.Auto.MainFresh {V : Type} [Fintype V] (Mc n : ℕ) (x : ↥(ColumnL2 (V ⊕ Fin Mc))) : Prop

Vectors whose template coordinates from the label n on vanish.

Equations

• TrilinearHT.Auto.MainFresh Mc n x = ∀ (m : Fin Mc), n ≤ ↑m → ∀ᵐ (y : ℝ), (↑↑x y).ofLp (some (Sum.inr m)) = 0

theorem TrilinearHT.Auto.MainFresh.add {V : Type} [Fintype V] {Mc n : ℕ} {x x' : ↥(ColumnL2 (V ⊕ Fin Mc))} (h : MainFresh Mc n x) (h' : MainFresh Mc n x') : MainFresh Mc n (x + x')

theorem TrilinearHT.Auto.MainFresh.smul {V : Type} [Fintype V] {Mc n : ℕ} {x : ↥(ColumnL2 (V ⊕ Fin Mc))} (h : MainFresh Mc n x) (c : ℂ) : MainFresh Mc n (c • x)

theorem TrilinearHT.Auto.MainFresh.sub {V : Type} [Fintype V] {Mc n : ℕ} {x x' : ↥(ColumnL2 (V ⊕ Fin Mc))} (h : MainFresh Mc n x) (h' : MainFresh Mc n x') : MainFresh Mc n (x - x')

theorem TrilinearHT.Auto.mainFresh_zero {V : Type} [Fintype V] {Mc : ℕ} (n : ℕ) : MainFresh Mc n 0

theorem TrilinearHT.Auto.MainFresh.mono {V : Type} [Fintype V] {Mc n n' : ℕ} (hn : n ≤ n') {x : ↥(ColumnL2 (V ⊕ Fin Mc))} (h : MainFresh Mc n x) : MainFresh Mc n' x

theorem TrilinearHT.Auto.mainRange_fresh {V : Type} [Fintype V] {Tg : Type u_1} {G : RealDyadicGrid} {Mc : ℕ} {O : OrigCols V Tg} (s : List (CatCol Tg)) (I : ℤ × ℤ) (r : ℕ) (M : Tg → Prop) {x : ↥(ColumnL2 (V ⊕ Fin Mc))} (hx : x ∈ mainRange G Mc O s I r M) : MainFresh Mc s.length x

The main ranges have no template coordinates beyond the current catalog length.

theorem TrilinearHT.Auto.mainProj_fresh {V : Type} [Fintype V] {Tg : Type u_1} {G : RealDyadicGrid} {Mc : ℕ} {O : OrigCols V Tg} (s : List (CatCol Tg)) (I : ℤ × ℤ) (r : ℕ) (M : Tg → Prop) (x : ↥(ColumnL2 (V ⊕ Fin Mc))) : MainFresh Mc s.length ((mainProj G Mc O s I r M) x)

theorem TrilinearHT.Auto.inner_wColumn {W : Type u_1} [Fintype W] {s : Set ℝ} (hs : MeasurableSet s) {φ : W → ℝ → ℂ} {ε : W → ℝ} {x : W} (h : MeasureTheory.MemLp (s.indicator (privateColumnValue φ ε x)) 2 MeasureTheory.volume) (X : ↥(ColumnL2 W)) (hX : ∀ᵐ (y : ℝ), (↑↑X y).ofLp (some x) = 0) : inner ℂ (wColumn s φ ε x) X = ∫ (y : ℝ) in s, (starRingEnd ℂ) (φ x y) * (↑↑X y).ofLp none

The inner product of a weighted column with a vector without the column's private coordinate is the moment of the physical part against the scalar.

theorem TrilinearHT.Auto.norm_wColumn_sq_le {W : Type u_1} [Fintype W] {s : Set ℝ} (hs : MeasurableSet s) (hsv : MeasureTheory.volume s < ⊤) {φ : W → ℝ → ℂ} {ε : W → ℝ} {x : W} (hφm : Measurable (φ x)) (hφ : ∀ (y : ℝ), ‖φ x y‖ ≤ 1) (hε0 : 0 ≤ ε x) (hε1 : ε x ≤ 1) : ‖wColumn s φ ε x‖ ^ 2 ≤ 2 * MeasureTheory.volume.real s

A column with scalar bounded by one and weight at most one has squared norm at most twice the measure of its set.

theorem TrilinearHT.Auto.mainCol_last_mem {V : Type} [Fintype V] {Tg : Type u_1} {G : RealDyadicGrid} {Mc : ℕ} {O : OrigCols V Tg} (s : List (CatCol Tg)) (d : CatCol Tg) (I : ℤ × ℤ) (r : ℕ) (M : Tg → Prop) (hlen : s.length < Mc) (hI : dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G d.birth.1 d.birth.2) (hr : d.rank ≤ r) (hM : M d.tag) : mainCol G Mc O (s ++ [d]) I (Sum.inr ⟨s.length, hlen⟩) ∈ mainRange G Mc O (s ++ [d]) I r M

The template column appended at the end of the catalog lies in the new range when it qualifies.

theorem TrilinearHT.Auto.catAtom_append_length {Tg : Type u_1} (s : List (CatCol Tg)) (d : CatCol Tg) : catAtom (s ++ [d]) s.length = d.atom

theorem TrilinearHT.Auto.mainProj_gain {V : Type} [Fintype V] {Tg : Type u_1} {G : RealDyadicGrid} {Mc : ℕ} {O : OrigCols V Tg} (s : List (CatCol Tg)) (d : CatCol Tg) (I : ℤ × ℤ) (r : ℕ) (M : Tg → Prop) (hlen : s.length < Mc) (hI : dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G d.birth.1 d.birth.2) (hr : d.rank ≤ r) (hM : M d.tag) (X : ↥(ColumnL2 (V ⊕ Fin Mc))) (hX : MainFresh Mc s.length X) : ‖∫ (y : ℝ) in dyadicGridCell G I.1 I.2, (starRingEnd ℂ) (d.atom y) * (↑↑(X - (mainProj G Mc O s I r M) X) y).ofLp none‖ ≤ 2 * √(dyadicGridLength G I.1) * ‖(mainProj G Mc O (s ++ [d]) I r M - mainProj G Mc O s I r M) X‖

The gain of a template insertion (blueprint line 1825): the target projection grows on a vector without fresh template coordinates by at least the residual moment of the new column.

noncomputable def TrilinearHT.Auto.cellNorm {W : Type u_2} [Fintype W] (G : RealDyadicGrid) (I : ℤ × ℤ) (x : ↥(ColumnL2 W)) : ℝ

The normalized L² norm on the cell I of a column-space vector.

Equations

• TrilinearHT.Auto.cellNorm G I x = √((TrilinearHT.Auto.dyadicGridLength G I.1)⁻¹ * ∫ (y : ℝ) in TrilinearHT.Auto.dyadicGridCell G I.1 I.2, ‖↑↑x y‖ ^ 2)

structure TrilinearHT.Auto.MainTest (Tg : Type u_1) (V : Type) [Fintype V] (Mc : ℕ) : Type u_1

A named main catalog test (blueprint eq:catalog-test, lines 1809-1815): the residual slot t, the target rank and vertex mask, a history of at most m main filters (ranks, masks and complement flags) and its base, a fixed augmented vector (a basic B, a basic side U, or for the helper rank a fixed vector-valued base).

• t : Fin 4

  Residual slot selected by the main catalog test.

• r : ℕ

  Rank cutoff of the residual-slot main projection.

• M : Tg → Prop

  Tag mask of the residual-slot main projection.

• m : ℕ

  Number of historical high-slot factors in the main test.

• hr : ℕ → ℕ

  Rank cutoff for each historical main-test factor.

• hM : ℕ → Tg → Prop

  Tag mask for each historical main-test factor.

• θ : ℕ → Bool

  Boolean choices specifying the historical main-test projection factors.

• base : ↥(ColumnL2 (V ⊕ Fin Mc))

  Column L² input containing original labels and finite catalog labels.

noncomputable def TrilinearHT.Auto.MainTest.Q {V : Type} [Fintype V] {Tg : Type u_1} (G : RealDyadicGrid) (Mc : ℕ) (O : OrigCols V Tg) (I : ℤ × ℤ) (w : MainTest Tg V Mc) (s : List (CatCol Tg)) (l : ℕ) : ↥(ColumnL2 (V ⊕ Fin Mc)) →L[ℂ] ↥(ColumnL2 (V ⊕ Fin Mc))

The history factor of index l (the identity beyond the history length).

Equations

• TrilinearHT.Auto.MainTest.Q G Mc O I w s l = if l < w.m then TrilinearHT.Auto.mainProj G Mc O s I (w.hr l) (w.hM l) else ContinuousLinearMap.id ℂ ↥(TrilinearHT.Auto.ColumnL2 (V ⊕ Fin Mc))

noncomputable def TrilinearHT.Auto.MainTest.hist {V : Type} [Fintype V] {Tg : Type u_1} (G : RealDyadicGrid) (Mc : ℕ) (O : OrigCols V Tg) (I : ℤ × ℤ) (w : MainTest Tg V Mc) (mH : ℕ) (s : List (CatCol Tg)) : ↥(ColumnL2 (V ⊕ Fin Mc))

The history value on the base.

Equations

• TrilinearHT.Auto.MainTest.hist G Mc O I w mH s = (TrilinearHT.Auto.operatorComplementProduct (fun (l : ℕ) => TrilinearHT.Auto.MainTest.Q G Mc O I w s l) w.θ mH) w.base

noncomputable def TrilinearHT.Auto.MainTest.resid {V : Type} [Fintype V] {Tg : Type u_1} (G : RealDyadicGrid) (Mc : ℕ) (O : OrigCols V Tg) (I : ℤ × ℤ) (w : MainTest Tg V Mc) (mH : ℕ) (s : List (CatCol Tg)) : ↥(ColumnL2 (V ⊕ Fin Mc))

The target residual of the history value.

Equations

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

theorem TrilinearHT.Auto.MainTest.Q_isStarProjection {V : Type} [Fintype V] {Tg : Type u_1} (G : RealDyadicGrid) (Mc : ℕ) (O : OrigCols V Tg) (I : ℤ × ℤ) (w : MainTest Tg V Mc) (s : List (CatCol Tg)) (l : ℕ) : IsStarProjection (Q G Mc O I w s l)

theorem TrilinearHT.Auto.MainTest.Q_nest {V : Type} [Fintype V] {Tg : Type u_1} (G : RealDyadicGrid) (Mc : ℕ) (O : OrigCols V Tg) (I : ℤ × ℤ) (w : MainTest Tg V Mc) (s : List (CatCol Tg)) (d : CatCol Tg) (l : ℕ) : Q G Mc O I w s l ∘SL Q G Mc O I w (s ++ [d]) l = Q G Mc O I w s l

theorem TrilinearHT.Auto.MainTest.fresh_complementProduct {V : Type} [Fintype V] {Tg : Type u_1} {G : RealDyadicGrid} {Mc : ℕ} {O : OrigCols V Tg} {I : ℤ × ℤ} {w : MainTest Tg V Mc} (s : List (CatCol Tg)) (θ : ℕ → Bool) (n : ℕ) (hn : s.length ≤ n) (k : ℕ) {x : ↥(ColumnL2 (V ⊕ Fin Mc))} : MainFresh Mc n x → MainFresh Mc n ((operatorComplementProduct (fun (l : ℕ) => Q G Mc O I w s l) θ k) x)

theorem TrilinearHT.Auto.MainTest.hist_fresh {V : Type} [Fintype V] {Tg : Type u_1} {G : RealDyadicGrid} {Mc : ℕ} {O : OrigCols V Tg} {I : ℤ × ℤ} {w : MainTest Tg V Mc} (mH : ℕ) (s : List (CatCol Tg)) (hb : MainFresh Mc s.length w.base) : MainFresh Mc s.length (hist G Mc O I w mH s)

def TrilinearHT.Auto.MainTest.Pass {V : Type} [Fintype V] {Tg : Type u_1} {Mc : ℕ} (w : MainTest Tg V Mc) (G : RealDyadicGrid) (O : OrigCols V Tg) (I : ℤ × ℤ) (c₀ : ℕ) (H : ℝ) (tagOf : Tg → ChartTag) (wI : ℝ × ℝ → ℂ) (τ : ℝ) (mH : ℕ) (s : List (CatCol Tg)) : Prop

The test passes (blueprint eq:catalog-test): every pure source whose tag lies in the vertex mask, in any slot other than the residual slot, has form norm at most τ ‖base‖_{2,I} against the target residual and two arbitrary normalized L² spectators.

Equations

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

The original basic columns of an active setup (blueprint lines 1613, 1676-1686)

structure TrilinearHT.Auto.ActiveSetup.BasicFamilies {κ : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ c₀) : Type 1

The basic projections of a column representation of the setup, two per slot, with their column budgets and charts, representing B_l = P_{l,0} - P_{l,1} on the cells of the setup (blueprint prop:base, lines 1607 and 1613).

• P : Fin 4 → Fin 2 → BasicProjection A.G A.R 1

  The two basic projection systems representing each of the four slots.

• budget (l : Fin 4) (j : Fin 2) : (self.P l j).Ψ.D.budget ≤ A.colBudget
• charts (l : Fin 4) (j : Fin 2) : (self.P l j).HasChartsOn (↑A.cells) c₀ A.H
• energy (l : Fin 4) (j : Fin 2) : (self.P l j).CellEnergyOn ↑A.cells
• rep (l : Fin 4) (I : ℤ × ℤ) : I ∈ A.cells → ∀ᵐ (y : ℝ), y ∈ dyadicGridCell A.G I.1 I.2 → A.B l I y = (self.P l 0).val I y - (self.P l 1).val I y

theorem TrilinearHT.Auto.ActiveSetup.HasColumnRep.families {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} (h : A.HasColumnRep 1) : Nonempty A.BasicFamilies

noncomputable def TrilinearHT.Auto.ActiveSetup.famVtxBound {κ : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ c₀) : ℕ

The vertex bound D of an attempt on the original basic columns: the original columns available at a cell number at most 8 column budgets of the setup (blueprint line 1679: at most D members along a path).

Equations

• A.famVtxBound = ⌊8 * A.colBudget⌋₊ + 1

theorem TrilinearHT.Auto.ActiveSetup.one_le_famVtxBound {κ : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ c₀) : 1 ≤ A.famVtxBound

theorem TrilinearHT.Auto.ActiveSetup.exists_cell_depth_ge {κ : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ c₀) {I : ℤ × ℤ} (hI : I ∈ dyadicFiniteTree A.G A.R A.treeDepth) (hne : A.cells.Nonempty) : ∃ c ∈ A.cells, I.1 ≤ c.1

A cell of the admission tree is not deeper than some cell of the setup.

@[reducible, inline]

abbrev TrilinearHT.Auto.ActiveSetup.BasicFamilies.SLab {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} (bf : A.BasicFamilies) (l : Fin 4) : Type

The labels of the original basic columns of the slot l: family index and family label.

Equations

• bf.SLab l = ((j : Fin 2) × (bf.P l j).V)

@[reducible, inline]

abbrev TrilinearHT.Auto.ActiveSetup.BasicFamilies.Lab {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} (bf : A.BasicFamilies) : Type

The labels of the original basic columns: slot and slot label.

Equations

• bf.Lab = ((l : Fin 4) × bf.SLab l)

def TrilinearHT.Auto.ActiveSetup.BasicFamilies.occAvail {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} (bf : A.BasicFamilies) (I : ℤ × ℤ) (x : bf.Lab) : Prop

An original basic column occurrence is available at a cell of the setup when its label lies in the mask of its family there (blueprint line 1676: a vertex is an original basic column occurrence).

Equations

• bf.occAvail I x = (I ∈ A.cells ∧ x.snd.snd ∈ (bf.P x.fst x.snd.fst).Ψ.A.labels I)

@[reducible, inline]

abbrev TrilinearHT.Auto.ActiveSetup.BasicFamilies.Vtx {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} (bf : A.BasicFamilies) : Type

The vertices of the attempt: original basic column occurrences with their admission cells.

Equations

• bf.Vtx = TrilinearHT.Auto.AdmVertex

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.admT {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} (bf : A.BasicFamilies) : AdmTree bf.Vtx

The admission tree of the original basic columns.

Equations

• bf.admT = TrilinearHT.Auto.admTree bf.occAvail

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.exists_vchart {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} (bf : A.BasicFamilies) (x : bf.Vtx) : ∃ (p : (d : ℕ) × QuadraticChartData d), 1 ≤ p.fst ∧ QuadraticChartComplexity (max c₀ (2 * tagKρ)) (max A.H padW) p.snd ∧ (bf.occAvail (↑x.2) x.1 → QuadraticChartComplexity (max c₀ (2 * tagKρ)) (max A.H padW) p.snd ∧ IsBoundedQuadraticChart p.snd ∧ ∀ y ∈ dyadicGridCell A.G (↑x.2).1 (↑x.2).2, (bf.P x.1.fst x.1.snd.fst).Ψ.D.scalar x.1.snd.snd y = quadraticChartAtom p.snd y)

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.vchart {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} (bf : A.BasicFamilies) (x : bf.Vtx) : (d : ℕ) × QuadraticChartData d

The chart of a vertex at its admission cell (a fixed default when unavailable).

Equations

• bf.vchart x = Classical.choose ⋯

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.vchart_spec {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} (bf : A.BasicFamilies) (x : bf.Vtx) (h : bf.occAvail (↑x.2) x.1) : QuadraticChartComplexity (max c₀ (2 * tagKρ)) (max A.H padW) (bf.vchart x).snd ∧ IsBoundedQuadraticChart (bf.vchart x).snd ∧ ∀ y ∈ dyadicGridCell A.G (↑x.2).1 (↑x.2).2, (bf.P x.1.fst x.1.snd.fst).Ψ.D.scalar x.1.snd.snd y = quadraticChartAtom (bf.vchart x).snd y

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.one_le_vchart_dim {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} (bf : A.BasicFamilies) (x : bf.Vtx) : 1 ≤ (bf.vchart x).fst

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.vchart_complexity {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} (bf : A.BasicFamilies) (x : bf.Vtx) : QuadraticChartComplexity (max c₀ (2 * tagKρ)) (max A.H padW) (bf.vchart x).snd

The chart of every vertex (available or not) has the complexity of the setup's charts: the default chart of an unavailable vertex is the zero chart of dimension one.

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.vtag {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} (bf : A.BasicFamilies) (x : bf.Vtx) : ChartTag

The normalized tag of a vertex: its slot multiplier c_l is removed from the matrix and the quadratic coefficient (blueprint line 1677).

Equations

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

def TrilinearHT.Auto.ActiveSetup.BasicFamilies.tagGraphEdge {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} (bf : A.BasicFamilies) (Hed : ℝ) (s : ℤ) (x y : bf.Vtx) : Prop

The tag graph at depth s: tags joined by an edge at the cell length of depth s, or equal tags (blueprint lines 1682-1686).

Equations

• bf.tagGraphEdge Hed s x y = (TrilinearHT.Auto.tagEdge Hed (TrilinearHT.Auto.dyadicGridLength A.G s) (bf.vtag x) (bf.vtag y) ∨ bf.vtag x = bf.vtag y)

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.tagDist {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} (bf : A.BasicFamilies) (Hed : ℝ) : DepthDistance bf.Vtx

The graph distances of the tag graph; they decrease with depth.

Equations

• bf.tagDist Hed = TrilinearHT.Auto.DepthDistance.ofEdges (bf.tagGraphEdge Hed) ⋯ ⋯

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.mem_labels_of_admAnc {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} (bf : A.BasicFamilies) {I : AdmCell A.G A.R A.treeDepth} {x : bf.Lab} (h : (admAnc bf.occAvail I x).Nonempty) : ↑I ∈ (bf.P x.fst x.snd.fst).Ψ.D.cells ∧ x.snd.snd ∈ (bf.P x.fst x.snd.fst).Ψ.A.labels ↑I

A label available at an ancestor of a cell of the admission tree is in its family mask at the cell.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.admT_X_card_le {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} (bf : A.BasicFamilies) (c : bf.admT.Cell) : (bf.admT.X c).card ≤ A.famVtxBound

At most 8 column budgets of original columns are present at any cell.

Colors and masks on the original basic columns (blueprint lines 1712-1773, 1804-1807)

noncomputable def TrilinearHT.Auto.ActiveSetup.fcd0 {κ : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ c₀) : ℕ

The primary depth d₀ = ⌈1000 log 2D⌉ of an attempt on the original basic columns.

Equations

• A.fcd0 = TrilinearHT.Auto.colorDegree A.famVtxBound

noncomputable def TrilinearHT.Auto.ActiveSetup.fcb1 {κ : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ c₀) (Hmax : ℕ) : ℕ

The primary scale b₁ = d₀^{10} b₂ (H_max + 1) (blueprint line 1716).

Equations

• A.fcb1 Hmax = A.fcd0 ^ 10 * TrilinearHT.Auto.ActiveSetup.cb2 Hmax * (Hmax + 1)

@[instance_reducible]

noncomputable instance TrilinearHT.Auto.ActiveSetup.BasicFamilies.instFintypeCellVtxAdmT {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} (bf : A.BasicFamilies) : Fintype bf.admT.Cell

Equations

• bf.instFintypeCellVtxAdmT = { elems := TrilinearHT.Auto.ActiveSetup.BasicFamilies.instFintypeCellVtxAdmT._aux_1 bf, complete := ⋯ }

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.coloring {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} (bf : A.BasicFamilies) (Hed : ℝ) (b1 b2 : ℕ) : ∃ (ωp : Fin (colorDegree A.famVtxBound) → bf.Vtx → Fin (colorDegree A.famVtxBound + 1)) (ωh : Fin (colorDegree A.famVtxBound) → bf.Vtx → Fin (colorDegree A.famVtxBound + 1)), IsMonotoneColoring bf.admT (bf.tagDist Hed) A.famVtxBound b1 b2 Finset.univ admCellSet (dyadicGridCell A.G A.R.1 A.R.2) ωp ωh

Blueprint lines 1720-1734 for one attempt on the original basic columns: the delays of the decreasing colors can be fixed so that the failed cells have total length at most 100 · 2001⁷ |R| / D.

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.colorSetup {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} (bf : A.BasicFamilies) (Hed : ℝ) (Hmax : ℕ) (ωp ωh : Fin A.fcd0 → bf.Vtx → Fin (A.fcd0 + 1)) : ColorSetup bf.Vtx

The color data of the attempt for fixed delay arrays.

Equations

• bf.colorSetup Hed Hmax ωp ωh = TrilinearHT.Auto.ColorSetup.ofArrays (bf.tagDist Hed) A.fcd0 (A.fcb1 Hmax) (TrilinearHT.Auto.ActiveSetup.cb2 Hmax) ωp ωh

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.colorParams {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} (bf : A.BasicFamilies) (Hed : ℝ) (Hmax : ℕ) (ωp ωh : Fin A.fcd0 → bf.Vtx → Fin (A.fcd0 + 1)) : ColorParams (bf.colorSetup Hed Hmax ωp ωh) Hmax

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.masks {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} (bf : A.BasicFamilies) (Hed : ℝ) (Hmax : ℕ) (ωp ωh : Fin A.fcd0 → bf.Vtx → Fin (A.fcd0 + 1)) : let K := bf.colorSetup Hed Hmax ωp ωh; have T := bf.admT; (∀ (I : T.Cell), ∀ v ∈ T.X I, K.Success (K.colorData (T.st I) v) → ∀ b ∈ T.X I, ∀ (h δ : ℕ), K.dist.d (T.depth I) b v = ↑δ → δ ≤ h → h ≤ Hmax → b ∈ K.mask T A.famVtxBound (K.grp T A.famVtxBound I v) h I) ∧ (∀ (I : T.Cell), ∀ v ∈ T.X I, K.Success (K.colorData (T.st I) v) → ∀ h < Hmax, ∀ (b b' : bf.Vtx), b ∈ K.mask T A.famVtxBound (K.grp T A.famVtxBound I v) h I → b' ∈ T.X I → K.dist.d (T.depth I) b b' ≤ 1 → b' ∈ K.mask T A.famVtxBound (K.grp T A.famVtxBound I v) (h + 1) I) ∧ (∀ (G : ℕ × Option (Fin K.d0 × bf.Vtx × ℤ) × ℕ × (ℕ × ℕ) × Option (Fin K.d0 × bf.Vtx × ℤ)) (ρ : Fin (bf.colorSetup Hed Hmax ωp ωh).d0) (z : bf.Vtx) (g : ℤ), G.2.1 = some (ρ, z, g) → ∀ (h : ℕ) (I : T.Cell), ∀ b ∈ K.mask T A.famVtxBound G h I, ∃ (k : ℕ), K.dist.d (T.depth I) z b = ↑k ∧ k ≤ (K.d0 + 1) * K.b1 + h) ∧ ∀ (I J u₀ u : T.Cell) (v₁ v₂ : bf.Vtx), T.Anc I J → T.Anc I u₀ → T.Anc J u → v₁ ∈ T.X u₀ → v₂ ∈ T.X u → K.Success (K.colorData (T.st u₀) v₁) → K.Success (K.colorData (T.st u) v₂) → K.color T A.famVtxBound u₀ v₁ = K.color T A.famVtxBound u v₂ → K.grp T A.famVtxBound u₀ v₁ ≠ K.grp T A.famVtxBound u v₂ → ∀ (h h' : ℕ), h ≤ Hmax → h' ≤ Hmax → ∀ (b b' : bf.Vtx), b ∈ K.mask T A.famVtxBound (K.grp T A.famVtxBound u₀ v₁) h I → b' ∈ K.mask T A.famVtxBound (K.grp T A.famVtxBound u v₂) h' J → ¬K.dist.d (T.depth J) b b' ≤ 1

Blueprint lem:masks for one attempt on the original basic columns: the pad masks of the colors contain the present vertices near a center, are closed under neighbors, have short paths to the primary winner, and separate distinct groups of one color.

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.admAt {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} (bf : A.BasicFamilies) (I : ℤ × ℤ) : bf.admT.Cell

The admission cell of a cell of the setup (the top otherwise).

Equations

• bf.admAt I = if h : I ∈ A.cells then some ⟨I, ⋯⟩ else none

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.vtxAt {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} (bf : A.BasicFamilies) (I : ℤ × ℤ) (x : bf.Lab) : bf.Vtx

The vertex of the original column x at a cell of the setup: the label with its admission cell along the path of the cell.

Equations

• bf.vtxAt I x = if h : I ∈ A.cells then (x, TrilinearHT.Auto.admCellOf bf.occAvail ⟨I, ⋯⟩ x) else (x, ⟨A.R, ⋯⟩)

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.vtxAt_mem {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} (bf : A.BasicFamilies) {I : ℤ × ℤ} {x : bf.Lab} (h : bf.occAvail I x) : bf.vtxAt I x ∈ bf.admT.X (bf.admAt I)

An available original column is present at its cell with its vertex.

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.origCols {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} (bf : A.BasicFamilies) (l : Fin 4) : OrigCols bf.Lab bf.Vtx

The original columns of the slot l as seen by the catalogs (blueprint lines 1676 and 1805), in the common column space of all original basic columns: every original basic column has its family scalar and private weight; at a cell exactly the columns of the two basic families of the slot l that lie in their family masks are available, with their vertices. The columns of the other slots are never available for the slot l, so the slot-l projections act in the coordinates of the slot l.

Equations

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

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

The parameters of an attempt on the original basic columns: the edge threshold, the pad bound, the delays, the number of pads P, the number of colors L, the label capacity and the history bound, with all needed neighbor enlargements of the pads below H_max (blueprint line 1808).

• Hed : ℝ

  Rational-height budget for edges between basic-family chart tags.

• Hmax : ℕ

  Maximum graph radius used by the basic-family tag masks.

• ωp : Fin A.fcd0 → bf.Vtx → Fin (A.fcd0 + 1)

  Primary coloring choices for basic-family labels in each round.

• ωh : Fin A.fcd0 → bf.Vtx → Fin (A.fcd0 + 1)

  High coloring choices for basic-family labels in each round.

• P : ℕ

  Positive number of search steps allocated to each basic-family level.

• hP : 0 < self.P
• Lc : ℕ

  Base catalog rank for the basic-family search.

• Mc : ℕ

  Number of main column labels available to the basic-family tests.

• mH : ℕ

  Maximum number of historical factors in a basic-family test.

• pads_le : 20 * self.P * (self.Lc + 1) + 31 * self.P + 2 ≤ self.Hmax

@[reducible, inline]

noncomputable abbrev TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.K {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) : ColorSetup bf.Vtx

The color data of the attempt.

Equations

• fp.K = bf.colorSetup fp.Hed fp.Hmax fp.ωp fp.ωh

def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.crank {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (m : ℕ) : ℕ

The rank of the cumulative split m: L - m + 1 (blueprint line 1807).

Equations

• fp.crank m = fp.Lc - m + 1

def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.cbase {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (m : ℕ) : ℕ

The base pad of the cumulative split m: 10 P (L - m + 1) (blueprint line 1807).

Equations

• fp.cbase m = 10 * fp.P * (fp.Lc - m + 1)

def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.brank {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (j : ℕ) : ℕ

The rank of the ball insertion j: L + j (blueprint line 1807).

Equations

• fp.brank j = fp.Lc + j

def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.bbase {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (j : ℕ) : ℕ

The base pad of the ball insertion j: 20 P (L + 1) + 10 (j - 1) P (blueprint line 1807).

Equations

• fp.bbase j = 20 * fp.P * (fp.Lc + 1) + 10 * (j - 1) * fp.P

def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.hrank {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) : ℕ

The helper rank L + 5 (blueprint line 1815).

Equations

• fp.hrank = fp.Lc + 5

def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.cmask {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (I : ℤ × ℤ) (m p : ℕ) : bf.Vtx → Prop

The cumulative mask of the cell I at the split m and the pad index p: the cumulative mask U_{m, h} at the pad h = 10 P (L - m + 1) + p (blueprint lines 1804-1807).

Equations

• fp.cmask I m p x = (x ∈ fp.K.cumMask bf.admT A.famVtxBound m (fp.cbase m + p) (bf.admAt I))

def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.bmask {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (I : ℤ × ℤ) (G : ℕ × Option (Fin A.fcd0 × bf.Vtx × ℤ) × ℕ × (ℕ × ℕ) × Option (Fin A.fcd0 × bf.Vtx × ℤ)) (j p : ℕ) : bf.Vtx → Prop

The ball mask of the cell I for the group G at the ball level j and the pad index p (blueprint lines 1807-1808).

Equations

• fp.bmask I G j p x = (x ∈ fp.K.mask bf.admT A.famVtxBound G (fp.bbase j + p) (bf.admAt I))

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.cbase_le {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) {m p : ℕ} (hp : p ≤ fp.P) : fp.cbase m + p + 2 ≤ fp.Hmax

Every pad used by a filter, with two neighbor enlargements, lies below H_max (blueprint line 1808).

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.bbase_le {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) {j p : ℕ} (hj : j ≤ 4) (hp : p ≤ fp.P) : fp.bbase j + p + 2 ≤ fp.Hmax

Positive smeared filters and the catalog tests (blueprint lines 1807-1815)

theorem TrilinearHT.Auto.opAvg_norm_le_one {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {P : ℕ} (hP : 0 < P) (Q : Fin P → E →L[ℂ] E) (hQ : ∀ (p : Fin P), ‖Q p‖ ≤ 1) : ‖opAvg Q‖ ≤ 1

An average of contractions is a contraction (blueprint line 1807).

theorem TrilinearHT.Auto.opAvg_starProjection_contraction {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {P : ℕ} (hP : 0 < P) (Q : Fin P → E →L[ℂ] E) (hQ : ∀ (p : Fin P), IsStarProjection (Q p)) : ‖opAvg Q‖ ≤ 1 ∧ ‖ContinuousLinearMap.id ℂ E - opAvg Q‖ ≤ 1

The averages of orthogonal projections and their complements are contractions (blueprint line 1807).

theorem TrilinearHT.Auto.avg_residual_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {P : ℕ} (hP : 0 < P) (Q : ℕ → Fin P → E →L[ℂ] E) (θ : ℕ → Bool) (m : ℕ) (T : Fin P → E →L[ℂ] E) (z : E) : (operatorComplementProduct (fun (l : ℕ) => opAvg (Q l)) θ m) z - (opAvg T) ((operatorComplementProduct (fun (l : ℕ) => opAvg (Q l)) θ m) z) = (↑Finset.univ.card)⁻¹ • ∑ pc : Fin P × (Fin m → Fin P), ((operatorComplementProduct (fun (l : ℕ) => Q l (choiceExt hP pc.2 l)) θ m) z - (T pc.1) ((operatorComplementProduct (fun (l : ℕ) => Q l (choiceExt hP pc.2 l)) θ m) z))

The target residual of an averaged history, against an averaged target, is the average over all individual pad choices of the residuals of the single-choice histories (blueprint lines 1810-1811: histories include every individual pad choice).

@[reducible, inline]

abbrev TrilinearHT.Auto.ResidOK {W : Type u_1} [Fintype W] {Tg : Type u_2} (G : RealDyadicGrid) (I : ℤ × ℤ) (c₀ : ℕ) (H : ℝ) (tagOf : Tg → ChartTag) (wI : ℝ × ℝ → ℂ) (t : Fin 4) (M : Tg → Prop) (R : ↥(ColumnL2 W)) (β : ℝ) : Prop

A residual R in slot t passes at level β on the cell I (blueprint eq:catalog-test): against every pure source whose tag lies in the mask, in another slot, and two arbitrary normalized L² spectators, the local form is at most β.

Equations

• TrilinearHT.Auto.ResidOK G I c₀ H tagOf wI t M R β = TrilinearHT.Auto.ResidPass G I c₀ H tagOf wI t M R β

theorem TrilinearHT.Auto.phys_avg_ae {W : Type u_1} [Fintype W] {ι : Type u_2} (s : Finset ι) (R : ι → ↥(ColumnL2 W)) : (fun (y : ℝ) => (↑↑((↑s.card)⁻¹ • ∑ i ∈ s, R i) y).ofLp none) =ᵐ[MeasureTheory.volume] fun (y : ℝ) => ∑ i ∈ s, (↑s.card)⁻¹ * (↑↑(R i) y).ofLp none

The physical coordinate of an average of column vectors is the average of their physical coordinates.

theorem TrilinearHT.Auto.ResidOK.avg {W : Type u_1} [Fintype W] {κ : LocalKernelClass} {Tg : Type u_2} {G : RealDyadicGrid} {I : ℤ × ℤ} {c₀ : ℕ} {H : ℝ} {tagOf : Tg → ChartTag} {wI : ℝ × ℝ → ℂ} (hwI : IsAdmissibleLocalKernel κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) wI) {t : Fin 4} {M : Tg → Prop} {ι : Type u_3} (s : Finset ι) (hs : s.Nonempty) (R : ι → ↥(ColumnL2 W)) {β : ℝ} (h : ∀ i ∈ s, ResidOK G I c₀ H tagOf wI t M (R i) β) : ResidOK G I c₀ H tagOf wI t M ((↑s.card)⁻¹ • ∑ i ∈ s, R i) β

Blueprint lines 1810-1811 ("histories include every individual pad choice, so the tests also hold for averages"): an average of residuals passing at level β passes at level β.

Nesting of the main projections in the pad and in depth (blueprint line 1807)

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.admAt_of_mem {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} (bf : A.BasicFamilies) {I : ℤ × ℤ} (hI : I ∈ A.cells) : bf.admAt I = some ⟨I, ⋯⟩

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.admAt_anc {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} (bf : A.BasicFamilies) {I J : ℤ × ℤ} (hI : I ∈ A.cells) (hJ : J ∈ A.cells) (h : dyadicGridCell A.G I.1 I.2 ⊆ dyadicGridCell A.G J.1 J.2) : bf.admT.Anc (bf.admAt J) (bf.admAt I)

Nested cells of the setup have admission cells in ancestor relation.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.admCellOf_desc {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} (bf : A.BasicFamilies) {I J : AdmCell A.G A.R A.treeDepth} {x : bf.Lab} (hIJ : dyadicGridCell A.G (↑I).1 (↑I).2 ⊆ dyadicGridCell A.G (↑J).1 (↑J).2) (h : (admAnc bf.occAvail J x).Nonempty) : admCellOf bf.occAvail I x = admCellOf bf.occAvail J x

The admission cell of a label available above a cell is the same at the cell.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.vtxAt_desc {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} (bf : A.BasicFamilies) {I J : ℤ × ℤ} (hI : I ∈ A.cells) (hJ : J ∈ A.cells) (h : dyadicGridCell A.G I.1 I.2 ⊆ dyadicGridCell A.G J.1 J.2) {x : bf.Lab} (hx : bf.occAvail J x) : bf.vtxAt I x = bf.vtxAt J x

The vertex of an original column available at a cell is its vertex at every subcell of the setup.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.occAvail_desc {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} (bf : A.BasicFamilies) {I J : ℤ × ℤ} (hI : I ∈ A.cells) (h : dyadicGridCell A.G I.1 I.2 ⊆ dyadicGridCell A.G J.1 J.2) {x : bf.Lab} (hx : bf.occAvail J x) : bf.occAvail I x

Availability of original columns is inherited by the subcells of the setup.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.origCol_memLp {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} (bf : A.BasicFamilies) (l : Fin 4) {Mc : ℕ} (s : List (CatCol bf.Vtx)) {I : ℤ × ℤ} {v : bf.Lab} (hv : bf.occAvail I v) : MeasureTheory.MemLp ((dyadicGridCell A.G I.1 I.2).indicator (privateColumnValue (mainScalar Mc (bf.origCols l) s) (mainWeight Mc (bf.origCols l)) (Sum.inl v))) 2 MeasureTheory.volume

An original column available at a cell of the setup is square integrable on the cell.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.cmask_mono {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) {I J : ℤ × ℤ} (hI : I ∈ A.cells) (hJ : J ∈ A.cells) (h : dyadicGridCell A.G I.1 I.2 ⊆ dyadicGridCell A.G J.1 J.2) (m p : ℕ) (x : bf.Vtx) (hx : fp.cmask J m p x) : fp.cmask I m p x

Cumulative masks grow in depth (blueprint line 1807).

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.bmask_mono {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) {I J : ℤ × ℤ} (hI : I ∈ A.cells) (hJ : J ∈ A.cells) (h : dyadicGridCell A.G I.1 I.2 ⊆ dyadicGridCell A.G J.1 J.2) (G : ℕ × Option (Fin A.fcd0 × bf.Vtx × ℤ) × ℕ × (ℕ × ℕ) × Option (Fin A.fcd0 × bf.Vtx × ℤ)) (j p : ℕ) (x : bf.Vtx) (hx : fp.bmask J G j p x) : fp.bmask I G j p x

Ball masks grow in depth (blueprint line 1807).

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.cmask_pad_mono {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (I : ℤ × ℤ) (m : ℕ) {p p' : ℕ} (hp : p ≤ p') (x : bf.Vtx) (hx : fp.cmask I m p x) : fp.cmask I m p' x

Cumulative masks grow with the pad (blueprint line 1807).

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.bmask_pad_mono {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (I : ℤ × ℤ) (G : ℕ × Option (Fin A.fcd0 × bf.Vtx × ℤ) × ℕ × (ℕ × ℕ) × Option (Fin A.fcd0 × bf.Vtx × ℤ)) (j : ℕ) {p p' : ℕ} (hp : p ≤ p') (x : bf.Vtx) (hx : fp.bmask I G j p x) : fp.bmask I G j p' x

Ball masks grow with the pad (blueprint line 1807).

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

The positive smeared cumulative filter of the slot l at the split m on the cell I: the average over the pads 10 P (L - m + 1) + p, 1 ≤ p ≤ P, of the rank-(L - m + 1) main projections with the cumulative masks (blueprint line 1807).

Equations

• fp.cumFilt l s I m = TrilinearHT.Auto.opAvg fun (p : Fin fp.P) => TrilinearHT.Auto.mainProj A.G fp.Mc (bf.origCols l) s I (fp.crank m) (fp.cmask I m (↑p + 1))

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.ballFilt {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (l : Fin 4) (s : List (CatCol bf.Vtx)) (I : ℤ × ℤ) (G : ℕ × Option (Fin A.fcd0 × bf.Vtx × ℤ) × ℕ × (ℕ × ℕ) × Option (Fin A.fcd0 × bf.Vtx × ℤ)) (j : ℕ) : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc)) →L[ℂ] ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))

The positive smeared ball filter of the slot l for the group G at the ball level j on the cell I (blueprint line 1807).

Equations

• fp.ballFilt l s I G j = TrilinearHT.Auto.opAvg fun (p : Fin fp.P) => TrilinearHT.Auto.mainProj A.G fp.Mc (bf.origCols l) s I (fp.brank j) (fp.bmask I G j (↑p + 1))

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.cumFilt_contraction {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (l : Fin 4) (s : List (CatCol bf.Vtx)) (I : ℤ × ℤ) (m : ℕ) : ‖fp.cumFilt l s I m‖ ≤ 1 ∧ ‖ContinuousLinearMap.id ℂ ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc)) - fp.cumFilt l s I m‖ ≤ 1

The smeared filters and their complements are contractions (blueprint line 1807).

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.ballFilt_contraction {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (l : Fin 4) (s : List (CatCol bf.Vtx)) (I : ℤ × ℤ) (G : ℕ × Option (Fin A.fcd0 × bf.Vtx × ℤ) × ℕ × (ℕ × ℕ) × Option (Fin A.fcd0 × bf.Vtx × ℤ)) (j : ℕ) : ‖fp.ballFilt l s I G j‖ ≤ 1 ∧ ‖ContinuousLinearMap.id ℂ ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc)) - fp.ballFilt l s I G j‖ ≤ 1

The catalog tests on averaged histories (blueprint lines 1809-1815)

theorem TrilinearHT.Auto.MainTest.pass_iff {V : Type} [Fintype V] {Tg : Type u_1} {Mc : ℕ} (w : MainTest Tg V Mc) (G : RealDyadicGrid) (O : OrigCols V Tg) (I : ℤ × ℤ) (c₀ : ℕ) (H : ℝ) (tagOf : Tg → ChartTag) (wI : ℝ × ℝ → ℂ) (τ : ℝ) (mH : ℕ) (s : List (CatCol Tg)) : w.Pass G O I c₀ H tagOf wI τ mH s ↔ ResidOK G I c₀ H tagOf wI w.t w.M (resid G Mc O I w mH s) (τ * cellNorm G I w.base)

A main catalog test passes exactly when its target residual passes at the level τ ‖base‖_{2,I} (blueprint eq:catalog-test).

theorem TrilinearHT.Auto.avg_history_pass {W : Type u_1} [Fintype W] {κ : LocalKernelClass} {Tg : Type u_2} {G : RealDyadicGrid} {I : ℤ × ℤ} {c₀ : ℕ} {H : ℝ} {tagOf : Tg → ChartTag} {wI : ℝ × ℝ → ℂ} (hwI : IsAdmissibleLocalKernel κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) wI) {t : Fin 4} {M : Tg → Prop} {P : ℕ} (hP : 0 < P) (Q : ℕ → Fin P → ↥(ColumnL2 W) →L[ℂ] ↥(ColumnL2 W)) (θ : ℕ → Bool) (m : ℕ) (T : Fin P → ↥(ColumnL2 W) →L[ℂ] ↥(ColumnL2 W)) (z : ↥(ColumnL2 W)) {β : ℝ} (h : ∀ (pc : Fin P × (Fin m → Fin P)), ResidOK G I c₀ H tagOf wI t M ((operatorComplementProduct (fun (l : ℕ) => Q l (choiceExt hP pc.2 l)) θ m) z - (T pc.1) ((operatorComplementProduct (fun (l : ℕ) => Q l (choiceExt hP pc.2 l)) θ m) z)) β) : ResidOK G I c₀ H tagOf wI t M ((operatorComplementProduct (fun (l : ℕ) => opAvg (Q l)) θ m) z - (opAvg T) ((operatorComplementProduct (fun (l : ℕ) => opAvg (Q l)) θ m) z)) β

Blueprint lines 1810-1811 ("histories include every individual pad choice, so the tests also hold for averages"): if the residuals of the histories of all individual pad choices pass at a level, the residual of the averaged history against the averaged target passes at that level.

Catalog closure on the main columns (blueprint lem:closure, lines 1819-1828)

theorem TrilinearHT.Auto.catAtom_append_left {Tg : Type u_1} (s t : List (CatCol Tg)) {n : ℕ} (hn : n < s.length) : catAtom (s ++ t) n = catAtom s n

theorem TrilinearHT.Auto.mainCol_append_left {V : Type} [Fintype V] {Tg : Type u_1} {G : RealDyadicGrid} {Mc : ℕ} {O : OrigCols V Tg} (s t : List (CatCol Tg)) (I : ℤ × ℤ) (x : V ⊕ Fin Mc) (hx : ∀ (n : Fin Mc), x = Sum.inr n → ↑n < s.length) : mainCol G Mc O (s ++ t) I x = mainCol G Mc O s I x

theorem TrilinearHT.Auto.mainSel_mono_append {V : Type} [Fintype V] {Tg : Type u_1} {G : RealDyadicGrid} {Mc : ℕ} {O : OrigCols V Tg} (s t : List (CatCol Tg)) (I : ℤ × ℤ) (r : ℕ) (M : Tg → Prop) : mainSel G Mc O s I r M ⊆ mainSel G Mc O (s ++ t) I r M

theorem TrilinearHT.Auto.mainSel_append_irrel {V : Type} [Fintype V] {Tg : Type u_1} {G : RealDyadicGrid} {Mc : ℕ} {O : OrigCols V Tg} (s t : List (CatCol Tg)) (I : ℤ × ℤ) (r : ℕ) (M : Tg → Prop) (ht : ∀ d ∈ t, ¬dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G d.birth.1 d.birth.2) : mainSel G Mc O (s ++ t) I r M = mainSel G Mc O s I r M

Templates born at cells not containing I do not change the main projections at I.

theorem TrilinearHT.Auto.mainProj_append_irrel {V : Type} [Fintype V] {Tg : Type u_1} {G : RealDyadicGrid} {Mc : ℕ} {O : OrigCols V Tg} (s t : List (CatCol Tg)) (I : ℤ × ℤ) (r : ℕ) (M : Tg → Prop) (ht : ∀ d ∈ t, ¬dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G d.birth.1 d.birth.2) : mainProj G Mc O (s ++ t) I r M = mainProj G Mc O s I r M

theorem TrilinearHT.Auto.MainTest.resid_append_irrel {V : Type} [Fintype V] {Tg : Type u_1} {G : RealDyadicGrid} {Mc : ℕ} {O : OrigCols V Tg} (w : MainTest Tg V Mc) (I : ℤ × ℤ) (mH : ℕ) (s t : List (CatCol Tg)) (ht : ∀ d ∈ t, ¬dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G d.birth.1 d.birth.2) : resid G Mc O I w mH (s ++ t) = resid G Mc O I w mH s

theorem TrilinearHT.Auto.MainTest.pass_append_irrel {V : Type} [Fintype V] {Tg : Type u_1} {G : RealDyadicGrid} {Mc : ℕ} {O : OrigCols V Tg} (w : MainTest Tg V Mc) (I : ℤ × ℤ) (c₀ : ℕ) (H : ℝ) (tagOf : Tg → ChartTag) (wI : ℝ × ℝ → ℂ) (τ : ℝ) (mH : ℕ) (s t : List (CatCol Tg)) (ht : ∀ d ∈ t, ¬dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G d.birth.1 d.birth.2) : w.Pass G O I c₀ H tagOf wI τ mH (s ++ t) ↔ w.Pass G O I c₀ H tagOf wI τ mH s

theorem TrilinearHT.Auto.MainTest.gain {V : Type} [Fintype V] {Tg : Type u_1} {G : RealDyadicGrid} {Mc : ℕ} {O : OrigCols V Tg} {I : ℤ × ℤ} (w : MainTest Tg V Mc) {κ : LocalKernelClass} {c₀ D : ℕ} (hst : SameTagBound κ c₀ D) {H : ℝ} (hH : Real.exp 2 ≤ H) {tagOf : Tg → ChartTag} (hdim : ∀ (x : Tg), 1 ≤ (tagOf x).dim) {wI : ℝ × ℝ → ℂ} (hwI : IsAdmissibleLocalKernel κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) wI) {τ : ℝ} {mH : ℕ} {s : List (CatCol Tg)} (hlen : s.length < Mc) (hb : MainFresh Mc s.length w.base) (hfail : ¬w.Pass G O I c₀ H tagOf wI τ mH s) : ∃ (d : CatCol Tg), d.rank = w.r ∧ d.birth = I ∧ w.M d.tag ∧ (∃ R ∈ residueBox (tagOf d.tag).dim 9, ∃ (γ : ℝ), d = templateCol (tagOf d.tag) w.t R γ I w.r d.tag) ∧ τ / (2 * Real.exp (↑D * (1 + Real.log H) ^ D)) * (√(dyadicGridLength G I.1) * cellNorm G I w.base) < ‖(mainProj G Mc O (s ++ [d]) I w.r w.M - mainProj G Mc O s I w.r w.M) (hist G Mc O I w mH s)‖

A failed main test is repaired by inserting a same-tag template at the cell (blueprint lines 1823-1825): the target projection grows on the old history value by more than τ / (2 H₀) times the norm of the base on the cell.

theorem TrilinearHT.Auto.main_cell_closure {κ : LocalKernelClass} {c₀ D : ℕ} (hst : SameTagBound κ c₀ D) {V : Type} [Fintype V] {G : RealDyadicGrid} {Tg : Type u_1} {Mc : ℕ} {O : OrigCols V Tg} {H : ℝ} (hH : Real.exp 2 ≤ H) {tagOf : Tg → ChartTag} (hdim : ∀ (x : Tg), 1 ≤ (tagOf x).dim) {I : ℤ × ℤ} {wI : ℝ × ℝ → ℂ} (hwI : IsAdmissibleLocalKernel κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) wI) {W : Type u_2} [Fintype W] (tests : W → MainTest Tg V Mc) (mH : ℕ) (τ : ℕ → ℝ) (hτ : ∀ (w : W), 0 < τ (tests w).r) (s₀ : List (CatCol Tg)) (hbase : ∀ (w : W), MainFresh Mc s₀.length (tests w).base ∧ ‖(tests w).base‖ ≤ √(dyadicGridLength G I.1) * cellNorm G I (tests w).base) {Tmax : ℕ} (hMc : s₀.length + Tmax ≤ Mc) (hcap : ∑ r ∈ Finset.image (fun (w : W) => (tests w).r) Finset.univ, ↑(Fintype.card W) * (4 ^ mH * projectionPrefixConstant Tmax ^ (2 * mH)) / (τ r / (2 * Real.exp (↑D * (1 + Real.log H) ^ D))) ^ 2 < ↑Tmax) : ∃ (s : List (CatCol Tg)), (∀ d ∈ s, d.birth = I ∧ ∃ (w : W), d.rank = (tests w).r ∧ (tests w).M d.tag ∧ ∃ R ∈ residueBox (tagOf d.tag).dim 9, ∃ (γ : ℝ), d = templateCol (tagOf d.tag) (tests w).t R γ I (tests w).r d.tag) ∧ s.length < Tmax ∧ (∀ (w : W), (tests w).Pass G O I c₀ H tagOf wI (τ (tests w).r) mH (s₀ ++ s)) ∧ ∀ (r : ℕ), ↑{j ∈ Finset.range s.length | ∃ (hj : j < s.length), s[j].rank = r}.card * (τ r / (2 * Real.exp (↑D * (1 + Real.log H) ^ D))) ^ 2 ≤ ↑(Fintype.card W) * (4 ^ mH * projectionPrefixConstant Tmax ^ (2 * mH)) ∨ τ r / (2 * Real.exp (↑D * (1 + Real.log H) ^ D)) ≤ 0

Blueprint lem:closure at one active cell (lines 1819-1828) on the main columns: for finitely many named main tests at the cell whose bases are supported on the cell and have no coordinates on template labels beyond a fixed prefix catalog s₀, inserting same-tag templates born at the cell after s₀ closes the catalog: every test passes, fewer than T_max columns are inserted, and the insertions of each rank number at most |W| 4^m L^{2m} (2H₀/τ_r)², provided this allowance summed over the ranks stays below T_max. The fresh template coordinates of the inserted columns are absent from the old state.

theorem TrilinearHT.Auto.norm_eq_cellNorm_of_support {W : Type u_1} [Fintype W] (G : RealDyadicGrid) (I : ℤ × ℤ) (x : ↥(ColumnL2 W)) (hx : ∀ᵐ (y : ℝ), y ∉ dyadicGridCell G I.1 I.2 → ↑↑x y = 0) : ‖x‖ = √(dyadicGridLength G I.1) * cellNorm G I x

A vector supported on a cell has norm √|I| times its normalized norm on the cell.

theorem TrilinearHT.Auto.exists_coarse_first (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) : ∃ (L : List (ℤ × ℤ)), L.Nodup ∧ (∀ (I : ℤ × ℤ), I ∈ L ↔ I ∈ S) ∧ ∀ (i j : ℕ) (hi : i < L.length) (hj : j < L.length), i < j → ¬dyadicGridCell G L[i].1 L[i].2 ⊆ dyadicGridCell G L[j].1 L[j].2

The cells of a finite set can be listed without repetition with coarser cells first: no cell is contained in a later one.

theorem TrilinearHT.Auto.main_tree_closure {κ : LocalKernelClass} {c₀ D : ℕ} (hst : SameTagBound κ c₀ D) {V : Type} [Fintype V] {G : RealDyadicGrid} {Tg : Type u_1} {Mc : ℕ} {O : OrigCols V Tg} {H : ℝ} (hH : Real.exp 2 ≤ H) {tagOf : Tg → ChartTag} (hdim : ∀ (x : Tg), 1 ≤ (tagOf x).dim) (L : List (ℤ × ℤ)) (hnd : L.Nodup) (hord : ∀ (i j : ℕ) (hi : i < L.length) (hj : j < L.length), i < j → ¬dyadicGridCell G L[i].1 L[i].2 ⊆ dyadicGridCell G L[j].1 L[j].2) (wI : ℤ × ℤ → ℝ × ℝ → ℂ) (hwI : ∀ I ∈ L, IsAdmissibleLocalKernel κ (dyadicGridLeft G I.1 I.2) (dyadicGridLength G I.1) (wI I)) (W : ℤ × ℤ → Type u_2) [(I : ℤ × ℤ) → Fintype (W I)] (tests : (I : ℤ × ℤ) → W I → MainTest Tg V Mc) (mH : ℕ) (τ : ℕ → ℝ) (hτ : ∀ (I : ℤ × ℤ) (w : W I), 0 < τ (tests I w).r) (s₀ : List (CatCol Tg)) (hbase : ∀ I ∈ L, ∀ (w : W I), MainFresh Mc s₀.length (tests I w).base ∧ ‖(tests I w).base‖ ≤ √(dyadicGridLength G I.1) * cellNorm G I (tests I w).base) {Tmax : ℕ} (hMc : s₀.length + L.length * Tmax ≤ Mc) (hcap : ∀ I ∈ L, ∑ r ∈ Finset.image (fun (w : W I) => (tests I w).r) Finset.univ, ↑(Fintype.card (W I)) * (4 ^ mH * projectionPrefixConstant Tmax ^ (2 * mH)) / (τ r / (2 * Real.exp (↑D * (1 + Real.log H) ^ D))) ^ 2 < ↑Tmax) : ∃ (cat : List (CatCol Tg)), (∀ I ∈ L, ∀ (w : W I), (tests I w).Pass G O I c₀ H tagOf (wI I) (τ (tests I w).r) mH (s₀ ++ cat)) ∧ (∀ d ∈ cat, d.birth ∈ L ∧ ∃ (w : W d.birth), d.rank = (tests d.birth w).r ∧ (tests d.birth w).M d.tag ∧ ∃ R ∈ residueBox (tagOf d.tag).dim 9, ∃ (γ : ℝ), d = templateCol (tagOf d.tag) (tests d.birth w).t R γ d.birth (tests d.birth w).r d.tag) ∧ (∀ I ∈ L, ∀ (r : ℕ), ↑(List.filter (fun (d : CatCol Tg) => decide (d.birth = I ∧ d.rank = r)) cat).length * (τ r / (2 * Real.exp (↑D * (1 + Real.log H) ^ D))) ^ 2 ≤ ↑(Fintype.card (W I)) * (4 ^ mH * projectionPrefixConstant Tmax ^ (2 * mH)) ∨ τ r / (2 * Real.exp (↑D * (1 + Real.log H) ^ D)) ≤ 0) ∧ cat.length ≤ L.length * Tmax

Blueprint lem:closure over a finite tree on the main columns (lines 1819-1828): processing the cells with ancestors first and closing the catalog at each cell (main_cell_closure) after a fixed prefix s₀ gives one extension passing all tests at all cells; its columns born at a cell are that cell's own insertions, with the rank counts of main_cell_closure.

Path counts of the main labels (blueprint line 1820)

theorem TrilinearHT.Auto.length_filter_le_sum {α : Type u_1} {β : Type u_2} [DecidableEq β] (s : List α) (key : α → β) (T : Finset β) (p : α → Bool) (hT : ∀ d ∈ s, p d = true → key d ∈ T) : (List.filter p s).length ≤ ∑ b ∈ T, (List.filter (fun (d : α) => decide (key d = b) && p d) s).length

The elements of a list satisfying p are counted by their keys in a finite set.

noncomputable def TrilinearHT.Auto.mainLabels {V : Type} [Fintype V] {Tg : Type u_1} (G : RealDyadicGrid) (Mc : ℕ) (O : OrigCols V Tg) (s : List (CatCol Tg)) (I : ℤ × ℤ) (r : ℕ) : Finset (V ⊕ Fin Mc)

The main labels at the cell I of rank at most r: the original labels available at I (rank zero) and the catalog templates born above I of rank at most r. Their number is the path count n_r (blueprint line 1820).

Equations

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

theorem TrilinearHT.Auto.card_mainLabels_le {V : Type} [Fintype V] {Tg : Type u_1} (G : RealDyadicGrid) (Mc : ℕ) (O : OrigCols V Tg) (s : List (CatCol Tg)) (I : ℤ × ℤ) (r : ℕ) (T : Finset ((ℤ × ℤ) × ℕ)) (hT : ∀ d ∈ s, dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G d.birth.1 d.birth.2 → d.rank ≤ r → (d.birth, d.rank) ∈ T) : (mainLabels G Mc O s I r).card ≤ {v : V | O.avail I v}.card + ∑ b ∈ T, (List.filter (fun (d : CatCol Tg) => decide (d.birth = b.1 ∧ d.rank = b.2)) s).length

The main labels of rank at most r at I are the available originals and the templates, counted by their birth cells and ranks.

The closure on the active cells of an attempt (blueprint lem:closure, lines 1819-1828)

noncomputable def TrilinearHT.Auto.catThreshold (Dv : ℕ) (τ₃ : ℝ) (n : ℕ → ℝ) (r : ℕ) : ℝ

The catalog threshold of eq:catalog-test for the target rank r: τ₃ / (D √n_{r-1}) with the vertex bound D and the path counts n (blueprint lines 1809-1812).

Equations

• TrilinearHT.Auto.catThreshold Dv τ₃ n r = τ₃ / (↑Dv * √(n (r - 1)))

noncomputable def TrilinearHT.Auto.closureRatio (Dv Kt mH Tmax : ℕ) (H₀ τ₃ : ℝ) : ℝ

The closure ratio K_t Q (2 H₀ D / τ₃)² (blueprint line 1828): the number of named tests at a cell, the binary-prefix factor Q = 4^m L_T^{2m} of the trial cap T with history bound m, the same-tag constant H₀, the vertex bound D and the threshold scale τ₃.

Equations

• TrilinearHT.Auto.closureRatio Dv Kt mH Tmax H₀ τ₃ = ↑Kt * (4 ^ mH * TrilinearHT.Auto.projectionPrefixConstant Tmax ^ (2 * mH)) * (2 * H₀ * ↑Dv / τ₃) ^ 2

theorem TrilinearHT.Auto.closureRatio_nonneg (Dv Kt mH Tmax : ℕ) (H₀ τ₃ : ℝ) : 0 ≤ closureRatio Dv Kt mH Tmax H₀ τ₃

theorem TrilinearHT.Auto.catThreshold_pos {Dv : ℕ} (hDv : 0 < Dv) {τ₃ : ℝ} (hτ₃ : 0 < τ₃) {n : ℕ → ℝ} {r : ℕ} (hn : 0 < n (r - 1)) : 0 < catThreshold Dv τ₃ n r

theorem TrilinearHT.Auto.allowance_eq {Dv : ℕ} (hDv : 0 < Dv) {τ₃ : ℝ} (hτ₃ : 0 < τ₃) {n : ℕ → ℝ} {r : ℕ} (hn : 0 < n (r - 1)) (c Q : ℝ) {H₀ : ℝ} (hH₀ : 0 < H₀) : c * Q / (catThreshold Dv τ₃ n r / (2 * H₀)) ^ 2 = c * Q * (2 * H₀ * ↑Dv / τ₃) ^ 2 * n (r - 1)

The trial allowance of a rank at the threshold catThreshold.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.card_avail_le {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} (bf : A.BasicFamilies) (l : Fin 4) (I : ℤ × ℤ) : ↑{x : bf.Lab | (bf.origCols l).avail I x}.card ≤ 2 * A.colBudget

At most two column budgets of original columns of a slot are available at a cell.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.main_closure {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (Tc : Finset (ℤ × ℤ)) (hTc : Tc ⊆ A.cells) {cS Dst : ℕ} (hst : SameTagBound κ cS Dst) {HS : ℝ} (hHS : Real.exp 2 ≤ HS) (W : Fin 4 → ℤ × ℤ → Type u_1) [(l : Fin 4) → (I : ℤ × ℤ) → Fintype (W l I)] (tests : (l : Fin 4) → (I : ℤ × ℤ) → W l I → MainTest bf.Vtx bf.Lab fp.Mc) (ht : ∀ (l : Fin 4) (I : ℤ × ℤ) (w : W l I), (tests l I w).t = l) (hr : ∀ (l : Fin 4) (I : ℤ × ℤ) (w : W l I), 1 ≤ (tests l I w).r ∧ (tests l I w).r ≤ fp.Lc + 5) (hbase : ∀ (l : Fin 4), ∀ I ∈ Tc, ∀ (w : W l I), MainFresh fp.Mc 0 (tests l I w).base ∧ ∀ᵐ (y : ℝ), y ∉ dyadicGridCell A.G I.1 I.2 → ↑↑(tests l I w).base y = 0) {Kt : ℕ} (hKt : ∀ (l : Fin 4) (I : ℤ × ℤ), Fintype.card (W l I) ≤ Kt) {Mp : ℕ} (hMp : 1 ≤ Mp) {τ₃ : ℝ} (hτ₃ : 0 < τ₃) {Tmax : ℕ} (n : ℕ → ℝ) (hn0 : 2 * A.colBudget ≤ n 0) (hratio : ∀ (r : ℕ), (1 + (↑fp.Lc + 6) * ↑Mp * closureRatio A.famVtxBound Kt fp.mH Tmax (Real.exp (↑Dst * (1 + Real.log HS) ^ Dst)) τ₃) * n r ≤ n (r + 1)) (hT : n (fp.Lc + 5) ≤ ↑Tmax) (hMc : Tc.card * Tmax ≤ fp.Mc) : ∃ (cat : Fin 4 → List (CatCol bf.Vtx)), ∀ (l : Fin 4), (∀ I ∈ Tc, ∀ (w : W l I), (tests l I w).Pass A.G (bf.origCols l) I cS HS bf.vtag (A.w I) (catThreshold A.famVtxBound τ₃ n (tests l I w).r) fp.mH (cat l)) ∧ (∀ d ∈ cat l, d.birth ∈ Tc ∧ (∃ (w : W l d.birth), d.rank = (tests l d.birth w).r ∧ (tests l d.birth w).M d.tag) ∧ ∃ R ∈ residueBox (bf.vtag d.tag).dim 9, ∃ (γ : ℝ), d = templateCol (bf.vtag d.tag) l R γ d.birth d.rank d.tag) ∧ (∀ I ∈ Tc, ∀ (r : ℕ), ↑(List.filter (fun (d : CatCol bf.Vtx) => decide (d.birth = I ∧ d.rank = r)) (cat l)).length ≤ closureRatio A.famVtxBound Kt fp.mH Tmax (Real.exp (↑Dst * (1 + Real.log HS) ^ Dst)) τ₃ * n (r - 1)) ∧ (∀ (I : ℤ × ℤ), {I' ∈ Tc | dyadicGridCell A.G I.1 I.2 ⊆ dyadicGridCell A.G I'.1 I'.2}.card ≤ Mp → ∀ r ≤ fp.Lc + 5, ↑(mainLabels A.G fp.Mc (bf.origCols l) (cat l) I r).card ≤ n r) ∧ (cat l).length ≤ Tc.card * Tmax

Blueprint lem:closure (lines 1819-1828) on the main columns of an attempt: for any finite families of named main tests on the active cells (at most K_t per cell and slot, residual slot the slot of the catalog, target ranks 1 ≤ r ≤ L + 5, bases supported on the cell without template coordinates) with the thresholds τ₃ / (D √n_{r-1}) of eq:catalog-test, path counts n_r with n_0 at least the original labels of a cell and ratios n_r / n_{r-1} ≥ 1 + (L + 6) M_p K (K the closure ratio) and trial cap T ≥ n_{L+5}, the catalog closure terminates on every active cell: there are slot catalogs of same-tag templates of their slot born at the active cells, with rank and tag of a named test there, passing all named tests; the rank-r insertions at one cell number at most K n_{r-1}; at every cell lying in at most M_p active cells the main labels of rank at most r ≤ L + 5 number at most n_r. The counts do not involve the edge threshold H_ed (blueprint line 1820).

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.helper_closure {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (Tc : Finset (ℤ × ℤ)) (hTc : Tc ⊆ A.cells) {cS Dst : ℕ} (hst : SameTagBound κ cS Dst) {HS : ℝ} (hHS : Real.exp 2 ≤ HS) (cat : Fin 4 → List (CatCol bf.Vtx)) (W : Fin 4 → ℤ × ℤ → Type u_1) [(l : Fin 4) → (I : ℤ × ℤ) → Fintype (W l I)] (tests : (l : Fin 4) → (I : ℤ × ℤ) → W l I → MainTest bf.Vtx bf.Lab fp.Mc) (ht : ∀ (l : Fin 4) (I : ℤ × ℤ) (w : W l I), (tests l I w).t = l) (hr : ∀ (l : Fin 4) (I : ℤ × ℤ) (w : W l I), (tests l I w).r = fp.Lc + 5) (hbase : ∀ (l : Fin 4), ∀ I ∈ Tc, ∀ (w : W l I), MainFresh fp.Mc (cat l).length (tests l I w).base ∧ ∀ᵐ (y : ℝ), y ∉ dyadicGridCell A.G I.1 I.2 → ↑↑(tests l I w).base y = 0) {Kt : ℕ} (hKt : ∀ (l : Fin 4) (I : ℤ × ℤ), Fintype.card (W l I) ≤ Kt) {τ₃ : ℝ} (hτ₃ : 0 < τ₃) {Tmax : ℕ} (n : ℕ → ℝ) (hn : 0 < n (fp.Lc + 4)) (hcapH : closureRatio A.famVtxBound Kt fp.mH Tmax (Real.exp (↑Dst * (1 + Real.log HS) ^ Dst)) τ₃ * n (fp.Lc + 4) < ↑Tmax) (hMc : ∀ (l : Fin 4), (cat l).length + Tc.card * Tmax ≤ fp.Mc) : ∃ (hcat : Fin 4 → List (CatCol bf.Vtx)), ∀ (l : Fin 4), (∀ I ∈ Tc, ∀ (w : W l I), (tests l I w).Pass A.G (bf.origCols l) I cS HS bf.vtag (A.w I) (catThreshold A.famVtxBound τ₃ n (fp.Lc + 5)) fp.mH (cat l ++ hcat l)) ∧ (∀ d ∈ hcat l, d.birth ∈ Tc ∧ d.rank = fp.Lc + 5 ∧ (∃ (w : W l d.birth), (tests l d.birth w).M d.tag) ∧ ∃ R ∈ residueBox (bf.vtag d.tag).dim 9, ∃ (γ : ℝ), d = templateCol (bf.vtag d.tag) l R γ d.birth d.rank d.tag) ∧ (∀ I ∈ Tc, ↑(List.filter (fun (d : CatCol bf.Vtx) => decide (d.birth = I)) (hcat l)).length ≤ closureRatio A.famVtxBound Kt fp.mH Tmax (Real.exp (↑Dst * (1 + Real.log HS) ^ Dst)) τ₃ * n (fp.Lc + 4)) ∧ (hcat l).length ≤ Tc.card * Tmax

Blueprint lem:closure, the reserved helper closure (lines 1815, 1820, 1828): for any slot catalogs and any finite families of helper tests of rank L + 5 on the active cells (at most K_t per cell and slot, residual slot the slot of the catalog) on fixed whole bases supported on the cell whose coordinates avoid the fresh helper labels beyond the catalog, helper templates of rank L + 5 born at the active cells close the helper tests at the thresholds τ₃ / (D √n_{L+4}), with at most K n_{L+4} insertions per cell, whenever this allowance stays below the trial cap.

Sizes of the closure (blueprint lem:closure, lines 1820, 1823, 1828-1830)

@[reducible, inline]

abbrev TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.MaskName {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (I : ℤ × ℤ) : Type

The mask names at a cell (blueprint line 1823): a cumulative split m ≤ L with a pad h ≤ H_max, or an original vertex present at the cell (naming its group) with a pad.

Equations

• fp.MaskName I = (Fin (fp.Lc + 1) × Fin (fp.Hmax + 1) ⊕ ↥(bf.admT.X (bf.admAt I)) × Fin (fp.Hmax + 1))

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

The vertex mask of a mask name: the cumulative mask U_{m,h} or the ball mask of the group of the vertex at the pad h.

Equations

• fp.maskOf I (Sum.inl (m, h)) = fun (x : bf.Vtx) => x ∈ fp.K.cumMask bf.admT A.famVtxBound (↑m) (↑h) (bf.admAt I)
• fp.maskOf I (Sum.inr (v, h)) = fun (x : bf.Vtx) => x ∈ fp.K.mask bf.admT A.famVtxBound (fp.K.grp bf.admT A.famVtxBound (bf.admAt I) ↑v) (↑h) (bf.admAt I)

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.cmask_named {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (I : ℤ × ℤ) {m p : ℕ} (hm : m ≤ fp.Lc) (hp : p ≤ fp.P) : ∃ (M : fp.MaskName I), fp.maskOf I M = fp.cmask I m p

The cumulative masks of the filters are named.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.bmask_named {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (I : ℤ × ℤ) {v : bf.Vtx} (hv : v ∈ bf.admT.X (bf.admAt I)) {j p : ℕ} (hj : j ≤ 4) (hp : p ≤ fp.P) : ∃ (M : fp.MaskName I), fp.maskOf I M = fp.bmask I (fp.K.grp bf.admT A.famVtxBound (bf.admAt I) v) j p

The ball masks of the filters of the groups of present vertices are named.

@[reducible, inline]

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

The names of the main tests of a slot at a cell with base names Bn (blueprint lines 1809-1815, 1823): a target rank 1 ≤ r ≤ L + 5 (stored as r - 1), a target mask name, a history of at most m factors, each a rank, a mask name and a complement flag, and a base name.

Equations

• fp.TestName I Bn = (Fin (fp.Lc + 5) × fp.MaskName I × ((ℓ : Fin (fp.mH + 1)) × (Fin ↑ℓ → Fin (fp.Lc + 6) × fp.MaskName I × Bool)) × Bn)

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.testOf {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (l : Fin 4) (I : ℤ × ℤ) {Bn : Type} (base : Bn → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (w : fp.TestName I Bn) : MainTest bf.Vtx bf.Lab fp.Mc

The main test of a name, with the base vectors base (blueprint lines 1809-1815).

Equations

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

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.testOf_t {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (l : Fin 4) (I : ℤ × ℤ) {Bn : Type} (base : Bn → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (w : fp.TestName I Bn) : (fp.testOf l I base w).t = l

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.testOf_r {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (l : Fin 4) (I : ℤ × ℤ) {Bn : Type} (base : Bn → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (w : fp.TestName I Bn) : 1 ≤ (fp.testOf l I base w).r ∧ (fp.testOf l I base w).r ≤ fp.Lc + 5

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.card_maskName_le {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (I : ℤ × ℤ) : Fintype.card (fp.MaskName I) ≤ (fp.Lc + 1 + A.famVtxBound) * (fp.Hmax + 1)

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.sum_pow_le (N m : ℕ) (hN : 1 ≤ N) : ∑ ℓ : Fin (m + 1), N ^ ↑ℓ ≤ (m + 1) * N ^ m

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.card_testName_le {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (I : ℤ × ℤ) (Bn : Type) [Fintype Bn] : Fintype.card (fp.TestName I Bn) ≤ (fp.Lc + 5) * ((fp.Lc + 1 + A.famVtxBound) * (fp.Hmax + 1)) * ((fp.mH + 1) * ((fp.Lc + 6) * ((fp.Lc + 1 + A.famVtxBound) * (fp.Hmax + 1)) * 2) ^ fp.mH) * Fintype.card Bn

The number of test names at a cell (blueprint line 1823).

theorem TrilinearHT.Auto.names_count_poly (c : ℕ) {k : ℝ} (hk : 6 * ↑c + 6 ≤ k) (Lc D Hmax mH b : ℕ) (hL : ↑Lc + 6 ≤ k ^ c) (hD : ↑D ≤ Real.exp (k ^ c)) (hH : ↑Hmax + 1 ≤ Real.exp (k ^ c)) (hm : ↑mH ≤ ↑c * (Real.log k + 1)) (hb : ↑b ≤ Real.exp (k ^ c)) : ↑((Lc + 6) * ((Lc + 1 + D) * (Hmax + 1)) * ((mH + 1) * ((Lc + 6) * ((Lc + 1 + D) * (Hmax + 1)) * 2) ^ mH) * b) ≤ Real.exp (k ^ (c + 2))

The test-name count is exp(k^{O(1)}) (blueprint line 1823): with L + 6 ≤ k^c, vertex bound, pad bound and base-name count at most exp(k^c) and histories of length at most c (1 + log k), the count of card_testName_le is at most exp(k^{c+2}).

theorem TrilinearHT.Auto.pathCounts_poly (c : ℕ) : ∃ (C : ℕ) (k₀ : ℝ), 2 ≤ k₀ ∧ ∀ {k : ℝ}, k₀ ≤ k → ∀ (Lc Mp Kt mH Dv : ℕ) (H₀ τ₃ n₀ : ℝ), ↑Lc + 6 ≤ k ^ c → ↑mH ≤ ↑c * (Real.log k + 1) → 1 + (↑Lc + 6) * ↑Mp * (↑Kt * (2 * H₀ * ↑Dv / τ₃) ^ 2) ≤ Real.exp (k ^ c) → n₀ ≤ Real.exp (k ^ c) → ∃ (n : ℕ → ℝ) (Tmax : ℕ), n₀ ≤ n 0 ∧ (∀ (r : ℕ), (1 + (↑Lc + 6) * ↑Mp * closureRatio Dv Kt mH Tmax H₀ τ₃) * n r ≤ n (r + 1)) ∧ n (Lc + 5) ≤ ↑Tmax ∧ Real.log ↑Tmax ≤ k ^ C

Blueprint lem:closure, lines 1820 and 1828: with L + 6 ≤ k^c ranks, histories of length at most c (1 + log k), closure data 1 + (L + 6) M_p K_t (2 H₀ D / τ₃)² ≤ exp(k^c) and n_0-requirement at most exp(k^c), the path counts can be chosen with ratios n_{r+1} / n_r ≥ 1 + (L + 6) M_p K (no trial cap is attained) and a trial cap T ≥ n_{L+5} with polynomial logarithm log T ≤ k^C.

@[reducible, inline]

abbrev TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.HelperName {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (I : ℤ × ℤ) (Bh : Type) : Type

The names of the helper tests of a slot at a cell with fixed base names Bh (blueprint line 1815): the helper rank L + 5, a target mask name, a history of at most m factors and a base name.

Equations

• fp.HelperName I Bh = (fp.MaskName I × ((ℓ : Fin (fp.mH + 1)) × (Fin ↑ℓ → Fin (fp.Lc + 6) × fp.MaskName I × Bool)) × Bh)

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.helperOf {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (l : Fin 4) (I : ℤ × ℤ) {Bh : Type} (base : Bh → ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (w : fp.HelperName I Bh) : MainTest bf.Vtx bf.Lab fp.Mc

The helper test of a name, with the fixed base vectors base (blueprint line 1815).

Equations

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

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.card_helperName_le {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} (fp : bf.FamParams) (I : ℤ × ℤ) (Bh : Type) [Fintype Bh] : Fintype.card (fp.HelperName I Bh) ≤ (fp.Lc + 5) * ((fp.Lc + 1 + A.famVtxBound) * (fp.Hmax + 1)) * ((fp.mH + 1) * ((fp.Lc + 6) * ((fp.Lc + 1 + A.famVtxBound) * (fp.Hmax + 1)) * 2) ^ fp.mH) * Fintype.card Bh

The number of helper names at a cell is at most the main count with the helper base names.

theorem TrilinearHT.Auto.closureData_le (c Dst : ℕ) {k : ℝ} (hk : 9 + 2 * ↑Dst * 2 ^ Dst ≤ k) (Lc Mp Kt Dv : ℕ) {HS τ₃ : ℝ} (hL : ↑Lc + 6 ≤ k ^ c) (hMp : ↑Mp ≤ Real.exp (k ^ c)) (hKt : ↑Kt ≤ Real.exp (k ^ c)) (hDv : ↑Dv ≤ Real.exp (k ^ c)) (hHS : Real.exp 2 ≤ HS) (hlog : Real.log HS ≤ k ^ c) (hτ : 0 < τ₃) (hτ' : τ₃⁻¹ ≤ Real.exp (k ^ c)) : 1 + (↑Lc + 6) * ↑Mp * (↑Kt * (2 * Real.exp (↑Dst * (1 + Real.log HS) ^ Dst) * ↑Dv / τ₃) ^ 2) ≤ Real.exp (k ^ (c * Dst + c + 1))

The closure data are exp(k^{O(1)}): with L + 6 ≤ k^c, path multiplicity, name count and vertex bound at most exp(k^c), source complexity log H ≤ k^c and 1 / τ₃ ≤ exp(k^c), the quantity 1 + (L + 6) M_p K_t (2 H₀ D / τ₃)² of the closure ratio, with the same-tag constant H₀ = exp(D_st (1 + log H)^{D_st}), is at most exp(k^{c D_st + c + 1}) for large k.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.closure_poly (c Dst : ℕ) : ∃ (C : ℕ) (k₀ : ℝ), 2 ≤ k₀ ∧ ∀ {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} {bf : A.BasicFamilies} {k : ℝ}, k₀ ≤ k → ∀ (fp : bf.FamParams) {HS τ₃ : ℝ} {Mp : ℕ} (Bn Bh : Type) [inst : Fintype Bn] [inst_1 : Fintype Bh], ↑fp.Lc + 6 ≤ k ^ c → ↑A.famVtxBound ≤ Real.exp (k ^ c) → ↑fp.Hmax + 1 ≤ Real.exp (k ^ c) → ↑fp.mH ≤ ↑c * (Real.log k + 1) → Real.exp 2 ≤ HS → Real.log HS ≤ k ^ c → 0 < τ₃ → τ₃⁻¹ ≤ Real.exp (k ^ c) → 1 ≤ Mp → ↑Mp ≤ Real.exp (k ^ c) → 2 * A.colBudget ≤ Real.exp (k ^ c) → ↑(Fintype.card Bn) ≤ Real.exp (k ^ c) → ↑(Fintype.card Bh) ≤ Real.exp (k ^ c) → ∃ (Kt : ℕ) (n : ℕ → ℝ) (Tmax : ℕ), (∀ (I : ℤ × ℤ), Fintype.card (fp.TestName I Bn) ≤ Kt) ∧ (∀ (I : ℤ × ℤ), Fintype.card (fp.HelperName I Bh) ≤ Kt) ∧ Real.log ↑Kt ≤ k ^ C ∧ 2 * A.colBudget ≤ n 0 ∧ (∀ (r : ℕ), (1 + (↑fp.Lc + 6) * ↑Mp * closureRatio A.famVtxBound Kt fp.mH Tmax (Real.exp (↑Dst * (1 + Real.log HS) ^ Dst)) τ₃) * n r ≤ n (r + 1)) ∧ n (fp.Lc + 5) ≤ ↑Tmax ∧ closureRatio A.famVtxBound Kt fp.mH Tmax (Real.exp (↑Dst * (1 + Real.log HS) ^ Dst)) τ₃ * n (fp.Lc + 4) < ↑Tmax ∧ Real.log (n (fp.Lc + 5)) ≤ k ^ C ∧ Real.log ↑Tmax ≤ k ^ C

Blueprint lem:closure, lines 1820, 1823 and 1828-1830: for fixed degrees c and same-tag exponent D_st there are a degree C and a threshold k₀ such that for k ≥ k₀ and every attempt with L + 6 ≤ k^c ranks, vertex bound, pad bound, path multiplicity, the two column budgets of n_0 and base-name counts at most exp(k^c), histories of length at most c (1 + log k), source complexity log H ≤ k^c and 1 / τ₃ ≤ exp(k^c): the named main and helper tests number at most K_t per cell with log K_t ≤ k^C (line 1823), and there are path counts n and a trial cap T with n_0 ≥ 2 colBudget, ratios n_{r+1} / n_r ≥ 1 + (L + 6) M_p K for the closure ratio K of T (the binary-prefix factor is below the ratio, so no cap is attained), n_{L+5} ≤ T, the helper allowance K n_{L+4} < T, and log T ≤ k^C (line 1828). None of these bounds involves the edge threshold H_ed, so they are fixed before H_ed (line 1830). With main_closure and helper_closure this gives lem:closure with log n_{L+5} ≤ k^{O(1)}.

Expansion of main primals (blueprint line 1835)

theorem TrilinearHT.Auto.inner_single_privateColumnValue {W : Type u_1} [Fintype W] [DecidableEq W] (φ : W → ℝ → ℂ) (ε : W → ℝ) (v w : W) (y : ℝ) : inner ℂ (EuclideanSpace.single (some w) 1) (privateColumnValue φ ε v y) = if v = w then ↑√(ε v) else 0

The private coordinate of a private column value.

theorem TrilinearHT.Auto.mainCombination_coeFn {V : Type} [Fintype V] {Tg : Type u_1} {G : RealDyadicGrid} {Mc : ℕ} {O : OrigCols V Tg} (s : List (CatCol Tg)) (I : ℤ × ℤ) (F : Finset (V ⊕ Fin Mc)) (c : V ⊕ Fin Mc → ℂ) (hmem : ∀ v ∈ F, MeasureTheory.MemLp ((dyadicGridCell G I.1 I.2).indicator (privateColumnValue (mainScalar Mc O s) (mainWeight Mc O) v)) 2 MeasureTheory.volume) : ∀ᵐ (y : ℝ), y ∈ dyadicGridCell G I.1 I.2 → ↑↑(∑ v ∈ F, c v • mainCol G Mc O s I v) y = ∑ v ∈ F, c v • privateColumnValue (mainScalar Mc O s) (mainWeight Mc O) v y

The pointwise form of a combination of main columns on the cell.

theorem TrilinearHT.Auto.mainCoeff_sum_le {V : Type} [Fintype V] {Tg : Type u_1} {G : RealDyadicGrid} {Mc : ℕ} {O : OrigCols V Tg} (s : List (CatCol Tg)) (I : ℤ × ℤ) (F : Finset (V ⊕ Fin Mc)) (c : V ⊕ Fin Mc → ℂ) (hmem : ∀ v ∈ F, MeasureTheory.MemLp ((dyadicGridCell G I.1 I.2).indicator (privateColumnValue (mainScalar Mc O s) (mainWeight Mc O) v)) 2 MeasureTheory.volume) {D : ℝ} (hD0 : 0 ≤ D) (hD : ∀ v ∈ F, (mainWeight Mc O v)⁻¹ ≤ D ^ 2) : ∑ v ∈ F, ‖c v‖ ≤ √↑F.card * D * ‖∑ v ∈ F, c v • mainCol G Mc O s I v‖ / √(dyadicGridLength G I.1)

The coefficients of a combination of main columns are controlled by the private coordinates: their absolute sum is at most √N D ‖x‖ / √|I| for N labels whose inverse private weights are at most D² (blueprint line 1835: only original columns have small private weights).

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.mainLabel_memLp {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} (bf : A.BasicFamilies) (l : Fin 4) {Mc : ℕ} (s : List (CatCol bf.Vtx)) (I : ℤ × ℤ) (r : ℕ) {v : bf.Lab ⊕ Fin Mc} (hv : v ∈ mainLabels A.G Mc (bf.origCols l) s I r) : MeasureTheory.MemLp ((dyadicGridCell A.G I.1 I.2).indicator (privateColumnValue (mainScalar Mc (bf.origCols l) s) (mainWeight Mc (bf.origCols l)) v)) 2 MeasureTheory.volume

The columns of the main labels of a slot are square integrable on the cell.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.inv_mainWeight_le {κ : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ c₀} (bf : A.BasicFamilies) (l : Fin 4) {Mc : ℕ} (v : bf.Lab ⊕ Fin Mc) : (mainWeight Mc (bf.origCols l) v)⁻¹ ≤ A.colBudget ^ 2

The inverse private weights of the main labels are at most colBudget²: original columns by the column budgets of the basic families, new labels have private weight one (blueprint line 1835: only original columns have small private weights).

theorem TrilinearHT.Auto.ActiveSetup.two_le_colBudget {κ : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ c₀) : 2 ≤ A.colBudget

theorem TrilinearHT.Auto.ActiveSetup.colBudget_le_famVtxBound {κ : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ c₀) : A.colBudget ≤ ↑A.famVtxBound

The inverse-weight budget is at most the vertex bound D of eq:catalog-test, so the expansion cost colBudget √n_{r-1} of a lower-rank primal times the threshold τ₃ / (D √n_{r-1}) is at most τ₃ (blueprint line 1835).