Section 16.1: One attempt and its restarts #
This file was automatically generated by Claude.
Formalization of blueprint Section 16, "Normalized absorption and the operator estimate"
(sec:completion), subsection 1, "One attempt and its restarts" (lines 2826-2842) of
blueprint/formalization_blueprint.tex.
Exceptional roots and restarts (prop:normalized, blueprint lines 2838-2843) #
The quantitative inequality (prop:normalized, blueprint lines 2843-2858) #
Choice of q, α, P (prop:normalized, blueprint lines 2866-2888) #
Summing the update levels (prop:normalized, blueprint lines 2893-2899) #
The union of the cuts (blueprint lines 2839-2841) #
Blueprint lines 2839-2841 ("choose their thresholds so the union of exceptional roots has
length at most |R|/4"): finitely many cut families F_i inside the root, of lengths at most
ρ_i |R| with Σ ρ_i ≤ 1/4, have maximal union cells X that are inside the root, pairwise
disjoint, of total length at most |R|/4, and cover every cut cell.
Normalized absorption (prop:normalized, blueprint lines 2827-2904) #
Abstract stopping generations for blueprint thm:uniform-local, lines 2910-2925: a finite
laminar family of nonempty cells, roots, and a stopping relation bad J K ("K violates the
averages of J").
The stopping generations, starting from the roots.
Equations
- TrilinearHT.Auto.stopGen C cell bad roots 0 = roots
- TrilinearHT.Auto.stopGen C cell bad roots k.succ = (TrilinearHT.Auto.stopGen C cell bad roots k).biUnion (TrilinearHT.Auto.firstStops C cell bad)
Instances For
Normalized absorption from the active-final estimate (prop:normalized, lines 2827-2904) #
The depth weight of a setup: the sum of the depths of its cells below the root plus their number; it strictly decreases on passing to a nonempty proper restart root.
Instances For
Blueprint prop:normalized, lines 2840-2843 ("restart there ... the root packing gives total
length at most 4|R|/3; on a finite tree this recursion terminates, so a retained-attempt
estimate sums with this fixed factor"): if every setup with a property Pr inherited by restarts
has pairwise disjoint exceptional roots of total length at most |R|/4 and its retained cells
(those below no exceptional root) contribute at most A |R|, then all cells contribute at most
(4/3) A |R|.
A slot other than the marked slot of a pattern.
Instances For
The failed cells of the admission tree of the original basic columns for fixed delay arrays.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Blueprint lines 1745 and 2839 ("marking failures have the length bound already proved"), on
the original basic columns: the maximal failed cells of a monotone coloring are pairwise disjoint
cells below the root of total length at most 100 · 2001⁷ |R| / D, and every cell of the setup
below none of them succeeds.
The failure roots of an attempt on the original basic columns: the maximal failed cells of its coloring.
Equations
- fp.failRoots = TrilinearHT.Auto.maximalDyadicCells A.G (bf.failedCells fp.Hed (A.fcb1 fp.Hmax) (TrilinearHT.Auto.ActiveSetup.cb2 fp.Hmax) fp.ωp fp.ωh)
Instances For
failure_cut for an attempt: for a monotone coloring at the scales of the attempt, the failure
roots are disjoint cells below the root of total length at most 100 · 2001⁷ |R| / D, and at every
cell of the setup below no failure root all present vertices succeed (blueprint lines 1745,
2839).
The slot inputs of a pattern on the main columns (blueprint lines 2838-2839) #
The slot of the basic side of the pattern p: none for the all-basic pattern, the marked
slot otherwise.
Instances For
The slot inputs of the pattern p on the main columns (blueprint lines 1607-1623 and
2838-2839, the noninitial base tuple of an active pattern): the basic side U in the marked slot of
a side pattern, the basic inputs B elsewhere.
Instances For
On a cell of the setup the physical parts of the pattern inputs are the slot arguments of the pattern.
The pattern inputs have no template coordinates.
The pattern inputs vanish off their cell.
The pattern inputs have normalized size at most max 2 S on the cells of the setup.
The cell forms of the pattern inputs on the main columns are the local forms of the pattern (blueprint lines 2838-2839: the attempt acts on the noninitial base tuple of the active pattern).
Blueprint lines 1850, 1863 and 1876 on the main columns: at a cell of the setup whose present
vertices all succeed (a retained cell, below no failure root by failure_cut), every current
group of color k has a certificate and an actual use at the cell.
The parameters of an attempt on the main columns (blueprint lines 1800-1830, 2838-2839) #
The number of colors L = d₀^{30} + 1 of an attempt on the main columns (blueprint line 1734:
the colors are at most d₀^{30}).
Instances For
The search fuel ⌈log₂ L⌉ + 1 of an attempt (blueprint line 1850: O(log L) binary
steps).
Instances For
The pad bound H_max = 20 P (L + 1) + 40 P of an attempt with P pads (blueprint line 1808:
all neighbor enlargements of the pads lie below H_max).
Instances For
The parameters of an attempt on the main columns with P pads, edge threshold H_ed, delay
arrays ω_p, ω_h and M_c main labels: L = d₀^{30} + 1, m_H = 2 fuel + 2,
H_max = 20 P (L + 1) + 40 P.
Equations
Instances For
Blueprint lines 2838-2839 with lines 1800-1856 (one attempt on the noninitial base tuple of an
active pattern, on the main columns): with P pads, L = d₀^{30} + 1 colors, fuel
⌈log₂ L⌉ + 1 and m_H = 2 fuel + 2, the closure counts are fixed first (closure_poly; they
do not involve H_ed, line 1830), then the edge threshold H_ed above any prescribed function of
these counts and above the localization threshold, then the delays of the coloring and the label
room M_c. The main catalogs, closed on the test cells T_c of path multiplicity at most M_p,
then localize the weighted minima of the pattern forms on every set of test cells below no failure
root to the leaves of the guarded search, up to Σ |I| · #leaves · 9 (D + 1) τ₃ S⁴.
The packet width packetW dominates the width of lem:height at height H in the form used
by the linear sides: 8 (d_max + 1)^3 log(2H) / log 2 ≤ packetW d_max H.
The uniform first-match and mode parameter bounds of one attempt (blueprint line 2839) #
The clearing bound of the attempt, ⌈H_ed^(d_B²)⌉: every group center z has its clearing
integer Q₀(z) = clearInt C_z at most this bound (blueprint lines 1890 and 1934). It is the Q₀
of the leaf schedule; each group uses its own Q₀(z) (SideInput.withQ0).
Instances For
The common cutoff B_* = Q₀ 2^(K_*+1) of the attempt (blueprint line 1944), with Q₀ the
clearing bound and K_* the truncation exponent of the enlarged budget.
Instances For
Every group center has its clearing integer between 1 and the clearing bound.
The enlarged budget D_* dominates d_max = 2 d_B + 2 and the clearing bound.
Blueprint line 2839, the uniform first-match and mode parameter bounds of one attempt
(lines 1934, 1944 and eq:mode-parameters): for the absolute constants of the schedule there is
M such that, for every attempt with H_ed ≥ 2, center dimensions at most d_B and center
entries of height at most H_ed, and every main budget D_m ≥ 2, there is a schedule S with
d_max = 2 d_B + 2, the enlarged budget D_* = modeStarG, the common cutoff
B_* = Q₀ 2^(K_*+1), D_m, and the clearing bound Q₀ as S.Q0, satisfying
eq:mode-parameters with the packet width of lem:height at the chosen height. Moreover
d_max ≤ D_*, Q₀ ≤ D_*, every group center has its clearing integer in [1, Q₀] (the
per-group Q₀ of line 1890), the box of K_* fits in B_*, the width bound used by the linear
sides holds, and log H, log T, K are polynomial in
Λ = d_max + log D_* + log B_* + log D_m + log Q₀ + 1.
Offsets and fixed modes of one attempt (blueprint line 2839, lines 2135-2156) #
The lift without modes (for groups without an actual use, which never enter a sum).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The mode system without modes (for groups without an actual use, which never enter a sum).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The center vertex of a group (the vertex d for a group without a center).
Instances For
A group with an actual use has a center with nonnegative top score (blueprint line 1934).
The curvature bound B = exp(D X^D) of the modes of a group with top score g at the ball
level j (exists_mainModeSystem).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The exports of exists_mainModeSystem for the role l (catalog s, ball level j) and the
group G (center z, top score g), at the cutoff width δ, the correction size δ_c and an
offset in the unit cube (blueprint lines 1932-1940 and 1971-1975).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Blueprint line 2839 (the offsets, by the measurable majorant on pre-existing main uses; the
corresponding fixed modes), with lines 2135-2156: on one search leaf (catalogs cat l with main
budgets, ball levels j_l and shared histories of the four roles) and a finite set of groups with
actual uses, whose actual main uses U_{l,G} (fixed before the offsets) have at most N_use
members through each point, there are mode systems and lifts of every role and group such that
each group of the set has the exports of exists_mainModeSystem at one common offset per role and
group, chosen by the explicit majorant of physical_error_used, and the physical errors of
eq:physical-error satisfy
Σ_l Σ_G Σ_{I ∈ U_{l,G}} ∫_I |E_{l,G,b(I)}|² ≤ (8 d_B δ + 2 δ_c²) 4 N colBudget² C_F N_use |R|.
Classical choice is used only after the offsets are selected; groups outside the set get the empty
mode system.
An image of a finite set is not larger than a second image when the second map determines the first on the set.
The keys of the modes alive on a cell number at most N, the number of main labels of the
role at every active cell: a key is determined by the primary and the first-match cell of its
modes, the first-match cells of one primary are disjoint, and all these primaries are primaries at
the deepest of these first-match cells (primaries_of_firstCell, blueprint line 1888: "the mode
lists, including primaries whose coefficients are zero, are nested").
The schedule conditions on the mode systems of one attempt (blueprint lines 1934 and 1944): for
the exports of a role and group at a ball level j ≤ 4, the dimensions are at most
d_max = 2 d_B + 2; the enlarged budget D_* = modeStarG bounds the curvature bound, the gauge
norm (ζ^ρ)², the inverse private weights and the alive modes; the truncation exponent K_*
makes the gauge tails at most D_*^(-300); and the keys alive on a cell number at most N.
An ancestor of a cell in the admission tree contains it (the converse of admTree_anc).
A group with a mode through a point has a present central vertex at an active cell containing the point: the primary of the mode lies in the group's ball mask at its first-match cell, and the central vertices of a mask are historical (blueprint lines 1807-1808 and 1934).
Blueprint line 1934 ("all modes ... along a path across groups"): for the mode systems of the
groups of a finite set at one role and ball level j ≤ 4, the modes through any point number at
most D_* = modeStarG: at most D (potMax + 1) groups have a central vertex on the path
(card_groups_path_le), and each has at most N B (4 max(1, 4B/δ_c) + 1)^(4 d_B) modes through
the point, B ≤ exp(D X_max^D).
The clearing bound is at most H_ed^(d_B²) + 1.
The heights of the rescaled differences of mode differences are covered by the enlarged budget
(blueprint line 1934): for the exports of a role and group at a ball level j ≤ 4 and a clearing
integer Q ≤ H_ed^(d_B²) + 1, 2 (Q (3 B_σ²)²)² ≤ ⌊D_*⌋ (the hypothesis hBσ of the
representatives and first top counts).
The block start of a cell below the root in block β < B_n is one of the block starts
R + K β, β < B_n.
The frozen coefficients of a family of groups give RepAt at every cell whose block start is a
block of the family (the first export of first_top_count_main, per group with its clearing
integer).
The linear-side bound of a family of groups over the blocks R + K β, β < B_n, in the form of
the side input (the hypothesis hlin of core_reduction_leaf).
Helper templates leave the main objects unchanged (blueprint line 2168) #
Blueprint line 2168 ("helper ranks exceed every main rank, so their insertion leaves all
previously fixed main projections ... unchanged"): on an active cell of its depth, the basic coarse
output of a catalog extended by templates of the helper rank equals that of the catalog, for any
main budgets (both are the leaf outputs of the cell, basicOut_restrict, whose ball and cumulative
filters are unchanged).
The frozen output at a depth u ≤ I.1, restricted to an active cell I, is unchanged by
helper templates: it is the restriction of the output on the active ancestor of depth u.
The side state at the depth of an active cell, restricted to the cell, is unchanged by helper
templates (eq:sides: the rolling output, the frozen output at u_b ≤ I.1 and the
catalog-free side subtotal).
A retained v_b-cell is an active cell (it contains an actual use and lies below the root).
The side input with the slot catalogs extended by the helper templates t, with main budgets
of the extended catalogs (blueprint lines 2167-2169); all other data are those of D.
Equations
Instances For
Blueprint line 2168: the side values of the leaf are unchanged by the helper templates on the
active cells (sideState_restrict_append; the whole outputs of the basic U slot by the
unchanged filters).
The whole leaf outputs are unchanged by the helper templates (unchanged filters).
The frozen representation RepAt is unchanged by the helper templates: the frozen outputs on
the retained (active) v_b-cells are unchanged, and the lift commutes with restrictions.
The physical errors on the active cells are unchanged by the helper templates.
A weighted column on a set is fixed by the restriction to the set.
The main range of a cell is fixed by the restriction to the cell (its columns live on the cell).
The outputs of a ball filter at a cell live on the cell.
The outputs of a ball filter of a catalog avoid the fresh labels of the catalog.
The side values of the leaf avoid the fresh labels of their slot catalog (whole side states
are physical; the whole output of a basic U slot is a ball filter output).
The side values of the leaf live on their cell.
Blueprint lines 2167-2169 on the leaf: the helper tests closed on the whole side states of the
leaf with the main catalogs (bases restricted to the active cells, catalogs extended by the helper
templates t) are the helper tests of the leaf with the extended catalogs (appendCat), whose
side values on the active cells are those of the main catalogs.
Catalog columns of rank above r do not change the main labels of rank at most r.
Catalog columns of rank above r do not change the masked main labels of rank at most r.
A present vertex at an active cell is an available occurrence at its admission cell.
The vertices of a named mask are present vertices of the cell.
The localization data of the leaf with the catalogs extended by helper templates (of template form, with available tags and of rank above every ball rank): the ball labels are unchanged.
Equations
Instances For
Strong stack families cost G₀ (blueprint lines 2393-2420 and line 2839) #
Blueprint line 2839 ("the strong stack families cost G₀") with eq:small-overhead: the jump
constant of a helper product of n + 1 ≤ c (log k + 1) + 1 layers in the main column tree of a
catalog with log (2 D_m) ≤ k^c is at most (n + 1)² G₀², with
G₀ = exp(1024 (c + 1) (1024 (c + 1) + c + 7) (1 + log 2k)²) (compressionC_le_overhead).
Blueprint eq:stack-energy with the strong stack families costing G₀ (line 2839): the banded
stack energy over outer configurations whose helper prefixes have at most n ≤ c (log k + 1)
steps, in the main column tree of a catalog with log (2 D_m) ≤ k^c, is at most P + 2 times the
P-free quantity of stackEA_le with the jump constant (n + 1)² G₀² (bandJumpM_le).
The positive chains of a slot of a search leaf number at most 2^fuel.
Every positive chain of a slot of a search leaf has at most fuel steps.
The merged descriptors of two positive chains of a search leaf have at most 2 fuel + 2
steps.
The prefixes of the step descriptors of a search leaf have at most 2 fuel + 2 steps.
The squared norm of the physical error of a basic slot at a cell is the integral over the cell of its physical coordinate (the error is a difference of physical parts).
Blueprint eq:physical-error on the leaf: the physical errors of the retained cells, summed
over their groups and slots, are bounded by the physical errors of the actual uses of
exists_leaf_modes (the uses I ∈ S with G ∈ gs I).
The full Fourier norm bound of the multiplier of the principal bins is that of
gaugeMult_star.
Blueprint lines 1942-1944 for the principal bins of a group center z: with its clearing
integer Q₀ = clearInt C_z and C_m = H_ed, the full Fourier norms of the multiplier (cutoff
δ/2) and of the cutoff ζ are at most the enlarged budget D_*, their truncations at K_* are
within D_*^(-300), |C_{ab}| ≤ H_ed, and Q₀ C_z is integral.
The node of a successful final class at a cell is a node of the successful components of its
(block, pre-cell) pair: its chosen mode is good, its class contains a good core mode (the class of
a core component), and it is the good mode of least index of the class (goodRep_min).
Hereditary representatives of type classes (RepClass, as built by first_top_count_main)
whose nodes contain the typed class nodes of the cells Cs have the properties RepOK there:
representatives in the predecessors, and different representatives on comparable nodes of one
type class with predecessors in different later CURRENT components (RepClass.hsepP).
Blueprint lines 2167-2169 with line 1828 ("there are L + 5 ranks, so the resulting global
trial cap T = n_{L+5}"), the helper catalogs of one attempt on the closure counts of its main
catalogs: with the attempt's named-test bound K_t, path counts n_r (one sequence for the main
ranks ≤ L + 4 and the helper rank L + 5) and trial cap T_max (exists_attempt), the helper
tests of rank L + 5 on the whole side states close with helper templates such that the main
tests still pass, the ball and cumulative filters are unchanged, and the helper insertions per
active cell number at most n_{L+5} (helper_instantiation_main, as in helper_sides).
The setup with its coefficient bound raised to at least M ≥ 0. All other data are unchanged,
so the column budget is at least M when there is a label. The vertex bound D of an attempt
can then be taken as large as required (blueprint line 1745: the failure bound of the colors
"tends to zero as D grows").
Equations
- One or more equations did not get rendered due to their size.
Instances For
Without labels no cell is active.
The attempt parameters of a setup whose height and column budget are at most e^Y, Y ≥ 1,
are polynomial in Y: the vertex bound is at most e^{Y+3}, the colour degree d₀ at most
5000 Y, the colour count L = d₀^{30} + 1 at most 5000^{30} Y^{30} + 1, 2^{fuel} ≤ 4 L, and
log H_src and log max(H, padW) are at most Y plus constants.