Section 16.2: The quantitative inequality #
This file was automatically generated by Claude.
Formalization of blueprint Section 16, "Normalized absorption and the operator estimate"
(sec:completion), subsection 2, "The quantitative inequality" (lines 2843-2892) of
blueprint/formalization_blueprint.tex.
The patterns with at least three cores and no error are the four-core pattern and the four
single-side patterns (core_pattern_cases).
Blueprint lines 2820-2822 (declaration core-estimate) on one leaf: the weighted active minimum
of the patterns with at least three cores is at most the sum of the bounds of eq:core-final for
the four-core pattern and the four three-core patterns (core_final_patterns, the triangle
inequality over the patterns and groups).
Without alive modes of the role l at the decision cell of I there are no core components
of the role at I.
Without alive modes of the role l at the decision cell of I the core of the role at I
vanishes.
A pattern form with a core slot whose core vanishes is zero.
Blueprint lines 2467-2470: without anchors (some role has no alive mode at the decision cell) the four-core pattern form vanishes.
Without anchors of the core roles the three-core pattern form with side role l vanishes.
The absolute tuple errors of eq:core-numerical for the four-core pattern at a cell and group
(the error term of four_core_principal_bins).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The absolute tuple errors of eq:core-numerical for the three-core pattern with side role l
at a cell and group (the error term of three_core_principal_bins).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Blueprint eq:core-final (lines 2808-2817) for the four-core pattern of one leaf, in terms of
the pattern forms: at the cells and groups with anchors the principal bound of
eq:principal-core holds (four_core_principal_bins, hypothesis hPB in its conclusion form),
at the others the pattern form vanishes (four_form_zero); so four_core_final_side applies with
K₁ = 2⁴/(1 - 4(2δ_*)^{1/4}), the upper heights and the absolute tuple errors fourErr.
Blueprint eq:core-final (lines 2808-2817) for the three-core pattern with side role l of
one leaf, in terms of the pattern forms: the principal bound of eq:principal-core at the cells
and groups with anchors of the core roles (three_core_principal_bins, hypothesis hPB in its
conclusion form), the vanishing of the pattern form at the others (three_form_zero), and
three_core_final_side with K₁ = 2⁴/(1 - 4(2δ_*)^{1/4}), the upper heights and the absolute
tuple errors threeErr.
The anchors of the four-core leaf estimate (blueprint line 2467, "let a_j be its
representative"): at a cell and group with alive modes of every role at the decision cell, the
representatives repAnc of the final classes for the side input of the group, and a default alive
mode for the classes that are not successful.
Equations
Instances For
The anchors of the three-core leaf estimate with side role l (alive modes of the core roles
at the decision cell).
Equations
Instances For
On the successful classes the leaf anchors are the representative anchors.
On the successful classes of the core roles the three-core leaf anchors are the representative anchors.
The leaf anchors satisfy AnchorOK (repAnc_ok).
The three-core leaf anchors satisfy AnchorOKAt in the core roles (repAnc_ok).
Blueprint eq:top-count along the retained paths for the four-core leaf estimate (lines
2783-2800, "the path estimates give Σ_G M_i^G ≤ C P^C σ_i^{-2} in every role"): the distinct used
representatives of a role along the path of y, with the leaf anchors, are values of the
representatives on use instances at the retained cells containing y with σ_i² ≤ σ_F²
(four_usedReps_subset_tops), so a retained-path count of those at the retained dyadic amplitudes
gives the path caps hcap of four_core_leaf.
Blueprint eq:top-count and eq:side-cap along the retained paths for the three-core leaf
estimate with side role l: the core roles as in four_hcap_leaf (three_usedReps_subset_tops),
and the side role from the retained side cap Σ_{I ∋ y} Σ_G Σ_l ‖S_{l,G,I}‖²/|I| ≤ K of the side
estimate (side_estimate_leaf), since M_l^G = σ_l^{-2} Σ_s ‖S_{l,G,s}‖²_{2,I_s} and the physical
part of a column has normalized square at most its normalized square norm (physSq_le).
A mode lies in its own predecessor set (the identity representatives).
A final class of a role at a cell lies on a retained pre-cell of its block: its class node is
a successful node over the retained pairs of the blocks Bs containing the block of the cell.
The representatives of the leaf core estimate: those of the type classes of the groups of
gset (first_top_count_main), the identity representatives outside gset.
Equations
Instances For
The nodes of the type classes of the leaf representatives (empty outside gset and the
types Ts).
Equations
Instances For
The leaf representatives have the properties RepOK on the cells T (repOK_of_repClass)
when the type-class nodes are the successful nodes of their type over the retained pairs of the
blocks Bs (as in first_top_count_main) and the blocks of the cells of T lie in Bs.
The class nodes of the leaf classes lie in the type-class nodes of their type.
Blueprint eq:top-count (lines 2212-2229) at the retained dyadic amplitudes of a leaf: from the
retained-path top counts of first_top_count_main (thresholds σ ∈ Thr, all σ ≥ D_*^{-1}, the
cells of T outside the top-count cuts Cut j) and, for σ < D_*^{-1}, the full mode budget
along a path (usedReps_le_Dstar, then D_* ≤ σ^{-2}), the counts of distinct used
representatives over the groups of the path of y are at most max(1, M_t) σ^{-2} (the input
hcount of four_hcap_leaf and three_hcap_leaf).
The per-group hypotheses of the principal bins (four_core_principal_bins,
three_core_principal_bins, blueprint lines 1932-1944 and eq:mode-parameters): a common chart
of the roles, the cutoff width δ, the coefficients and offsets of the modes, the clearing of the
center by Q₀, its entry bound C_m, the truncations at K_t and K_f, the full Fourier norms,
the inverse weights and the mode curvature bound.
Instances For
The constant K₁ = 2⁴/(1 - 4(2δ_*)^{1/4}) of eq:principal-core.
Instances For
The bound M_τ of eq:core-final for the four-core pattern (four_core_leaf).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The bound M_τ of eq:core-final for the three-core pattern with side role l
(three_core_leaf).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The absolute errors of eq:core-final at a cell: the tuple errors of eq:core-numerical and
the negligible amplitudes, over the groups and the patterns with at least three cores.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Blueprint lines 2820-2822 (declaration core-estimate) on one leaf of the side states: the
weighted active minimum of the patterns with at least three cores over the retained cells T
(outside the top-count cuts Cut j) is at most η^{1/1200} |R| (M₄ + Σ_l M₃(l)) plus the
absolute errors coreE. The ingredients: the principal bins of every group (per-group side
inputs D.withQ0 (qG G), hypotheses PrinOK, stabilization), the leaf anchors from the
type-class representatives Rr of first_top_count_main (leafRep, leafAnc, leafAnc3),
the path caps from the retained-path top counts and the side cap (leaf_hcount,
four_hcap_leaf, three_hcap_leaf, cap K = max(1, M_t, K_s)), and eq:core-final for the
four-core pattern and the three-core patterns (four_core_leaf, three_core_leaf,
core_leaf_patterns).
Blueprint line 2844 (the quantitative inequality on one leaf): the whole leaf outputs of a
localization leaf, after the cuts C (root fraction 2ρ) and C₂ (ρ₂) of
core_reduction_leaf, are bounded by the two-side, near-band and three-side terms of the side
estimate, the error patterns (eq:physical-error), the three-side power bound with cores of size
coreBd, and the core estimate on the retained cells (leaf_core_estimate: the patterns with at
least three cores give η^{1/1200} |R| (M₄ + Σ_l M₃(l)) plus the absolute errors coreE). The
retained cells lie outside the top-count cuts; the side cap is the one exported by the side
estimate, and the local side sizes are at most √T_c ≤ U.
Blueprint lines 2873-2876: if G₀ ≤ P^{1/8}, K + 2 ≤ C P^{C₅} with C ≥ 1, q ∈ (2, 3)
and 2 C₅ (q-2)/(q-1) ≤ 1/8, then P^{-1/2} G₀ (K+2)^{2(q-2)/(q-1)} ≤ C P^{-1/4}, and with
P ≥ η^{-α} this is at most C η^{α/4}.
Blueprint eq:active-final from eq:before-absorption (lines 2851-2888): a retained-attempt
bound C_q [η^ε P^{C₄} + (1 + C_N) P^{-1/2} G₀ (K+2)^{2(q-2)/(q-1)}] |R| + e becomes
C_q (2^{C₄} + C) η^{c_*} (1 + C_N) |R| + e with c_* = min(ε/2, α/4), for the choice
α = ε/(4(C₄+1)), P = ⌈η^{-α}⌉ and parameters G₀ ≤ P^{1/8}, K + 2 ≤ C P^{C₅}.
The data of one attempt on the main columns for the pattern p (blueprint lines 2838-2839,
exists_attempt): the attempt parameters fp with their monotone coloring, the main catalogs
closed on the active test cells T_c of path multiplicity at most M_p, the closure counts
K_t, n_r, T_max at the threshold scale τ₃ (with the helper names on famVtxBound base names
per cell), and the edge threshold above the graph thresholds of the helper residuals (τ₂) and
of the joint ball variation (τ').
- fp : bf.FamParams
Catalog and coloring parameters of the basic-family attempt.
Chart catalog in each slot of the attempt.
Finite collection of certified cells used by the attempt.
- Mp : ℕ
Maximum number of certified ancestors containing a given cell.
- Dst : ℕ
Exponent in the same-tag counting bound used by the attempt.
- hst : SameTagBound κ A.csrc self.Dst
- τ₃ : ℝ
Positive catalog-test threshold, at most one.
- Kt : ℕ
Dyadic truncation parameter used by the attempt's mode expansions.
Monotone path-count budget as a function of catalog rank.
- Tmax : ℕ
Uniform upper bound for the number of catalog entries contributed at one cell.
- hcol : IsMonotoneColoring bf.admT (bf.tagDist self.fp.Hed) A.famVtxBound (A.fcb1 self.fp.Hmax) (cb2 self.fp.Hmax) Finset.univ admCellSet (dyadicGridCell A.G A.R.1 A.R.2) self.fp.ωp self.fp.ωh
- hpassM (l : Fin 4) (I : ℤ × ℤ) : I ∈ self.Tc → ∀ (w : self.fp.TestName I Unit), (self.fp.testOf l I (fun (x : Unit) => bf.patIn self.fp.Mc p I l) w).Pass A.G (bf.origCols l) I A.csrc A.Hsrc bf.vtag (A.w I) (catThreshold A.famVtxBound self.τ₃ self.n (self.fp.testOf l I (fun (x : Unit) => bf.patIn self.fp.Mc p I l) w).r) self.fp.mH (self.cat l)
Instances For
The vertex of an original column is the same at every cell of the setup below a cell where the column is available: its admission cell is its shallowest available ancestor.
The tag of a main label is the same at every cell of the setup below a cell where it is a main label.
At most eight column budgets of original columns and the template path count of main labels occur at the cells of the setup containing a point.
A downstream use certificate determines the color of its group.
Blueprint lem:whole-ranges ("group and label counts on paths"), with lem:masks: along the path of a point, the main label of a ball range on a certified endpoint cell determines its group among the groups of one color (the tags of a label agree along a path, and pad masks of distinct groups of one color on overlapping certified endpoints are separated). Hence the group-label pairs of the ball ranges at a point number at most the main labels on its path.
A count of list entries whose key lies in a finite set of keys is at most the sum of the counts of the single keys.
The template path count is the number of templates whose birth cell contains the point.
Template path counts are additive under appending catalogs.
The main labels at a cell are at most two column budgets of original columns and the templates whose birth cell contains the left end of the cell.
The templates of a catalog born on a family of cells with at most M_p members containing
each point and at most n_b templates born at each cell have path counts at most M_p n_b.
The dyadic thresholds 2^j in [ε, U] (with j between ⌊log₂ ε⌋ and ⌈log₂ U⌉) that are at
least D⁻¹.
Equations
- TrilinearHT.Auto.dyThr ε U Dst = {σ ∈ Finset.image (fun (j : ℤ) => 2 ^ j) (Finset.Icc ⌊Real.logb 2 ε⌋ ⌈Real.logb 2 U⌉) | Dst⁻¹ ≤ σ}
Instances For
The joint path cap T_c of the side estimate on the side states (SideInput.Tside) as an
explicit function of the block length K, the basic U slot u and the number of pads P.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The side cap of a side input is its explicit form.
The private weights of a column tree are at most the squared budget: the private coordinate is a component of the column value, which the budget bounds on the birth cell.
The main weights of the attempt are at most colBudget².
The augmented mode of a cell has squared norm at most (1 + ε_m) |J|.
The component sizes of eq:component-size are at most (√(1 + W) + 1) D_* √C_c when the
private weights of the modes are at most W, the coefficients of the alive modes have squared
sum at most C_c and at most D_* modes are alive.
The catalog threshold of rank r times the column budget and the path count of rank r - 1
is at most τ₃ when the vertex bound dominates the column budget.
The core components of a slot at a cell number at most the alive modes of its pre-cell, and each of them consists of alive modes.
The coefficient sum of a core component is at most √D_* √C_c when the coefficients of the
alive modes have squared sum at most C_c and at most D_* modes are alive.
The four-core tuple errors at a cell are at most C D_*^{-100} (D_* √D_* √C_c)⁴.
The three-core tuple errors at a cell are at most C D_*^{-100} U_s (D_* (√D_* √C_c + 1))⁴
when the normalized size of the side slot is at most U_s.
SideLeafM.nearBnd of a leaf as an explicit function of the block length K, the U slot
u and the number of pads P.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The role types [0, log₂ D_*]^{2·4} of a schedule.
Equations
- TrilinearHT.Auto.fourTypesF S = Fintype.piFinset fun (x : Fin 4) => Finset.range (Nat.log 2 ⌊S.Dstar⌋₊ + 1) ×ˢ Finset.range (Nat.log 2 ⌊S.Dstar⌋₊ + 1)
Instances For
The four-core frequency constant of a schedule.
Equations
- One or more equations did not get rendered due to their size.
Instances For
SideInput.coreM4 as an explicit function of the schedule.
Equations
- One or more equations did not get rendered due to their size.
Instances For
SideInput.coreM3 as an explicit function of the schedule.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The near-band bound of a leaf is its explicit form.
The four-core bound of a side input is its explicit form in the schedule.
The three-core bound of a side input is its explicit form in the schedule.
The inverses of the slot coefficients have rational height at most 3.
The negated slot coefficients have rational height at most 3.
The dimension bound d_B = ⌈log max(H, padW)⌉ of the vertex tags of an active setup.
Instances For
Every vertex tag has dimension at most d_B (vchart_complexity).
The entries of every vertex tag matrix have rational height at most 18 (max H padW)².
The entries of the rescaled vertex tag matrices -c_l C have chart height at most
5832 (max H padW)⁴.
A family of cells with at most M members above each cell has at most M members containing
each point (the cells containing a point are the ancestors of the deepest one).
The uses of the groups of a family of cells: at a point, the pairs (group, cell containing the
point) with the group current at the cell number at most M V when at most M cells contain
the point and at most V groups are current at each cell.
The groups of a cell at the color k have color k.
The top height of a valid schedule is at most log H: H > A₀^{10(J_*+1)} ≥ 6^{J_*}.