Section 14.5b: The exported side estimate #
This file was automatically generated by Claude.
Formalization of blueprint Section 14, "The two-side estimate" (sec:sides), subsection 5, "Common
cuts, hull maxima, and summation" (lines 2425-2459), from the paragraph "Exported side estimate"
(side-estimate, lines 2454-2456) of blueprint/formalization_blueprint.tex: the assembly, on the
main columns, of the transfer identity, the pair-small and far terms, the frozen near bands, the
freeze and flag errors and the critical near-band bound into the side estimate of a localization
leaf. Split from Sec14_5CommonCutsHullMaximaSummation (which has 6936 lines) at this numbered
item of the blueprint.
The restored form at one cell on the main columns (blueprint lines 2241-2263) #
Blueprint lines 2241-2263 at one cell and group of a leaf on the main columns: the form of the
sides and the whole leaf outputs in the complement slots is at most the sum over the pairs of
positive chains of the transferred main term with the full arguments Y_c, Y_d, the three
restoration corrections (each with a basic side U), the far band defects, and 2/P times the
near band sums of the global steps at the depth of the cell, over the steps and the five
offsets.
Flags on the main columns (blueprint line 2393) #
The block start lies in (h - K, h].
The unflagged uses (blueprint line 2393), on the main columns: both frozen complements of the
step j at the offset o at the block start have normalized squares at most (2 C₀)² on every
active ancestor of the use within its block.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The bound of one slot tuple at one cell on the main columns (blueprint lines 2241-2394) #
Blueprint lines 2241-2262 and 2384-2394 at one cell and group of a leaf on the main columns,
for basic complements: the restored form (sides x in the slots a, b, whole leaf outputs in the
complement slots c, d) is at most the sum over the pairs of positive chains of the pair-small
main bound τ S_a S_b, the three restoration corrections C_κ S_a S_b S_u S_v with a basic side
U, the far bound c_F S_a S_b and, over the steps and offsets, 2/P times the frozen near band
forms of unflagged uses plus the freeze and flag errors (near_useM). Here the side of a is the
restriction of a global side x_a in the range of the relabeling of its catalog.
The two-side leaf data on the main columns (blueprint lines 2241-2456) #
The data of the two-side estimate of one localization leaf on the main columns: the slot
catalogs with their main budgets, the search leaf, the slot u of the basic U argument (none
for the all-basic pattern), the block length K, the slot inputs, the cell side values (the whole
output for the slot u) and
the global sides of the basic slots, restricting to the cell sides, in the range of the
relabeling of their catalogs, and of the rolling form S_h = Z_h - Z_b + W_b within the depth
block starting at b (blueprint eq:sides, line 2125, with W_b = Z_b - Z_{u_b} + V_b).
Catalog columns in each slot of the abstract side-leaf data.
- mbs (l : Fin 4) : bf.MainBudget (self.cat l)
Pathwise main-label budgets for the side-leaf catalogs.
- Lf : SearchLeaf
Search leaf whose side outputs are being estimated.
Optional outer slot treated separately from the basic side inputs.
- K : ℕ
Positive block length used to decompose the side inputs.
Column input in each slot and cell.
Cell-local side vector in each slot and group.
Global side vector at each depth before restriction to a cell.
Depth-indexed vectors supplying the within-block side increment.
Boundary vectors supplying the side value at a block start.
Instances For
The whole leaf output of the slot l and group G at a cell.
Equations
Instances For
The normalized size of the side of the slot l and group G at a cell.
Instances For
The sum over the slots of the squared normalized side sizes.
Instances For
The positive chains of the slot l of the leaf.
Instances For
The merged descriptors of a pair of positive chains of the complement slots c, d.
Instances For
The admissible slot tuples of the 2+2 estimate: distinct slots, transferred side a ≠ u.
Instances For
A complement slot is the basic U slot (its core vanishes).
Instances For
Blueprint lines 2446-2456 at one cell, on the main columns: the restored 2+2 patterns (whole
outputs in the two core slots, sides in the two side slots) are at most six times the sum over the
groups and slot tuples of bounds of the restored forms with the transferred side a not the slot
u.
Absolute and strong parts of one slot tuple at one cell (blueprint lines 2384-2394) #
The frozen complement band family of a step and offset at the block start of a cell.
Equations
Instances For
The frozen other complement of a step at the block start of a cell.
Equations
Instances For
The unflagged uses of a step and offset.
Equations
Instances For
The helper bands of the global side of a after the global helper prefix of the step j.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The frozen near band form of a step and offset at a use.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The absolute part of a slot tuple at a cell and group: the pair-small and far parts and the
frozen near band forms of the unflagged uses, with the transfer coefficients 2/P.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The strong part of a slot tuple at a cell and group: the restoration corrections with a basic
side U, and the freeze differences and flags of the near band forms.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Blueprint lines 2241-2262 and 2384-2394 at one cell and group of the leaf, for a valid slot tuple with basic complements: the restored form is at most the absolute part plus the strong part.
Blocks and near band uses of the leaf (blueprint lines 2425-2443) #
The block index of a cell: (I.1 - R.1) / K.
Instances For
The offset of a cell in its block: (I.1 - R.1) mod K.
Instances For
Below the root, a cell depth is its block start plus its offset, the offset is less than K
and the block start is blkStart.
The offset of a cell at depth R.1 + K β + m with m < K is m.
The chain of index i of the positive chains of slot l.
Instances For
The outer indices (c, d, i, i', j, o) of the near band applications.
Equations
Instances For
The uses of an index ((c, d, i, i', j, o), G, β) for the slots a, b and the banded
complement slot e: the cells of S of block β carrying the group, with a valid slot tuple
with basic complements, step j banding e, and unflagged.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The near band applications of the leaf (blueprint lines 2425-2443) #
The constant of near_band_criticalM.
Equations
- TrilinearHT.Auto.nbCM κ hq2 hq3 = Classical.choose ⋯
Instances For
The step descriptors before the step j of an outer index.
Equations
Instances For
The step descriptor j of an outer index.
Equations
Instances For
Frozen spectator inputs indexed by the common near-band use data.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Frozen helper bands indexed by the same near-band use data.
Equations
- One or more equations did not get rendered due to their size.
Instances For
An unflagged near-band use supplies both normalized energy side conditions. This includes the zero spectator slots, so both near-band variants use the same proof.
Transport a leaf helper band to the global band operator on its physical side.
Blueprint lines 2425-2443 (eq:near-band) for the slots a, b (basic, a, b ≠ u) and the
banded complement slot e on the main columns: off one cut family of root fraction ρ, the
frozen near band forms of the unflagged uses, with the transfer coefficient 2/P, are at most the
critical bound of near_band_criticalM for the actual stacks of the leaf (the rolling sides
S_h = Z_h - Z_b + W_b and the global helper bands of the steps).
The near bands with a basic U side (blueprint lines 2409, 2425-2443) #
Blueprint eq:near-band (lines 2409 and 2425-2443) when the untouched side is a basic U
side ("for a basic U side use each depth directly as a position"), on the main columns: with the
actual banded stacks of near_band_actualM (global helper bands of the steps on the rolling side
S_a) and the local values W_m(I) of the U side of total square E_U ≤ Γ_b |R| over the uses,
the transfer coefficient o/P (|o| ≤ 2) times the near-band sums has, off one cut family of
root fraction ρ, the critical absolute bound
4 C_q (1 + C_N) log K (K+2)^{2(q-2)/(q-1)} (64 B_c B_d) G₀ P^{-1/2} |R|.
The constant of near_band_critical_UM.
Equations
- TrilinearHT.Auto.nbCUM κ hq2 hq3 = Classical.choose ⋯
Instances For
Blueprint lines 2409 and 2425-2443 (eq:near-band) for the slots a (basic, a ≠ u),
b = u (the basic U side, its local values used directly as positions) and the banded
complement slot e on the main columns: off one cut family of root fraction ρ, the frozen near
band forms of the unflagged uses, with the transfer coefficient 2/P, are at most the critical
bound of near_band_critical_UM, with the U energy |outer indices| E_U.
The near parts of the cells as sums over the near band uses (blueprint lines 2425-2443) #
Summing over the range L the terms with index below n ≤ L.
The frozen near band forms of the unflagged uses of a slot tuple at a cell, summed over the
pairs of positive chains, the steps and the offsets with the transfer coefficients 2/P.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The absolute part is the pair-small and far part plus the near part.
Collapsing the block and group indices of the uses of a cell.
Expanding the outer indices of the uses of a cell and group into the slot, chain, step and offset sums.
The near parts of a cell, summed over its groups and slot tuples, are 2/P times the use
indicator sums of the near band applications over the slot triples (a, b, e).
The near parts of a leaf (blueprint eq:near-band, lines 2425-2443) #
The uses of a near band application have distinct slots a, b, e and a ≠ u.
The critical bound of one near band application of the leaf (near_tripleM for a basic
untouched side, near_triple_UM for the U side).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Blueprint eq:near-band (lines 2425-2443) on one leaf, on the main columns: one cut family
of root fraction ρ (the union of the cut families of the near band applications of all slot
triples, each of root fraction ρ/64) such that the near parts of the retained cells, weighted by
length and summed over the groups and slot tuples, are at most the sum over the slot triples of
the critical near-band bounds nearBnd.
The third strong factor of a slot tuple (blueprint lines 2372-2394) #
The third strong factor of a slot tuple with basic complements: the restoration corrections
with a basic side U, and the freeze differences and flags of the near band forms.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The third strong factor of a slot tuple at a cell and group: strTh for basic complements,
C_κ B₀ (S_c + S_d) when a complement slot is the U slot (three sides), zero for invalid
tuples.
Equations
Instances For
The absolute part of a slot tuple at a cell and group, zero for invalid tuples and tuples with
a U complement.
Equations
Instances For
The algebra of the strong part: moving the side sizes out of the near band errors.
The strong part of a slot tuple with basic complements is at most S_a S_b times the third
strong factor.
Blueprint lines 2241-2262 and 2372-2394 at one cell and group, for every valid slot tuple:
the restored form is at most the absolute part plus S_a S_b times the third strong factor. For a
complement in the U slot the form has three sides and is at most C_κ S_a S_b S_u B₀.
The integrated budget of the third strong factors (blueprint lines 2384-2394) #
The square of the restoration correction factor with basic sides U, times the cell length:
L (C (x y' + x' y + x y))² ≤ 8 C² C_y² (u² + v²) with x = u/√L, y = v/√L and
x', y', y ≤ C_y.
Freeze budgets on the main columns (blueprint lines 2386-2394) #
An ancestor at or below the block start of a cell lies in the same block.
A block flag of a cell for the energies E at the threshold c: some active ancestor of the
cell in its block has energy above c times its length.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Blueprint line 2393 ("propagating the event through its block costs at most K in integrated
square energy"): the flagged cells have total length at most K / c times the energies on the
ancestors in their blocks.
Blueprint lines 2389-2390 ("differences from their values at b have integrated square
budgets ... by Lemma variation, paying ... the O(K) overlap"): for outputs Z_g with certified
variation capacity B, the differences from the block starts over certified active cells have
total square at most K B (one variation application per block offset, on the disjoint block
intervals).
Shared and group-indexed frozen complements (blueprint lines 2263, 2386-2394) #
If the entries of slot v of a list in order are x₀ :: xs, then the entries of slot v
strictly after an entry of slot v lie in xs.
One step of a complement value.
The cumulative pad masks do not depend on the group.
Blueprint line 2263 ("its complementary band history is shared across groups"): a global step of a cumulative descriptor does not depend on the group.
The slot of a global step is its descriptor slot.
A complement value after global steps whose descriptors of its slot are cumulative does not depend on the group.
Blueprint line 2263 ("if the outgoing filter is cumulative, its outer ball has already been removed"): in the merged descriptors of a chain pair, the descriptors of the slot of a step that come after it are cumulative.
The pad output n of the step j of a chain pair at the depth h (pad family Q_0 = 0,
Q_n for 1 ≤ n ≤ P, Q_{P+1} = 1), after the later complement history of its slot, on the
global basic input.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The complement bands are differences of consecutive pad outputs.
The squared freeze difference of the pad output n at a cell (from its block start).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The freeze energy of the pads 1, …, P of a step at a cell.
Instances For
The freeze energy of the identity output (the terminal band endpoint Q_{P+1} = 1).
Instances For
The freeze energy of the other complement of a step at a cell.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Blueprint lines 2389-2390 ("paying the polynomial number of bands"): the freeze differences of the complement bands of one offset are at most four times the freeze energies of the pads and of the identity output.
The square of a vector is at most twice the square of its difference from a second vector plus twice the square of the second one.
Blueprint line 2393 ("on unflagged uses both frozen complements have bounded local sizes on
their entire ancestor hull within the block"): if the current complements are bounded by C₀
on the active cells, a use without block flags of the pad, identity and other complement freeze
energies (at the thresholds C₀²/8, C₀²/8, C₀²) is unflagged.
The flag indicator of a use is at most the sum of the three block flag indicators.
The terminal pad of a step is the identity.
A cumulative step does not depend on the group.
The later history of a slot whose descriptors are cumulative does not depend on the group.
The step j of a chain pair is cumulative: its pads are shared across groups.
Instances For
The later history of the other complement of the step j is cumulative: the other complement
is shared across groups.
Equations
Instances For
The later history of the slot of the step j is cumulative.
Blueprint line 2263 ("the terminal complementary band ... shared identity"; "its complementary band history is shared across groups"): the identity output of a step, and every pad output of a cumulative step, do not depend on the group.
The indicator of a block flag.
Instances For
The shared part of the freeze and flag factor of a step at a cell: the identity output always, the pads of a cumulative step, the other complement with a cumulative history.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The group-indexed part of the freeze and flag factor of a step at a cell: the pads of a ball step and the other complement with a ball in its history.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Blueprint lines 2386-2394 at one step and offset: with current complements bounded by C₀,
the freeze differences and the flag of a use are at most the shared part plus the group-indexed
part (pads, identity output and other complement, each with its block flag).
The shared part of the third strong factor of a slot tuple with basic complements: the
restoration corrections with a basic side U and the shared freeze and flag factors.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The group-indexed part of the third strong factor of a slot tuple with basic complements: the group-indexed freeze and flag factors.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Blueprint lines 2263 and 2386-2394: with basic inputs of the complement slots bounded by C₀
on the active cells, the third strong factor of a basic tuple is at most its shared part plus its
group-indexed part.
The shared part of the third strong factor of a slot tuple.
Instances For
The group-indexed part of the third strong factor of a slot tuple: the group-indexed freeze
factors for basic complements, C_κ B₀ (S_c + S_d) when a complement slot is the U slot.
Equations
Instances For
The cell value of the third strong factors (blueprint line 2375: "a third factor is shared or bounded by its group square sum"): the shared parts (evaluated at any fixed group, being independent of it) plus the root of the group square sum of the group-indexed parts.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Blueprint lines 2375-2382: the third strong factors of every group at a cell are bounded by the cell value.
The integrated square of the cell values is at most twice the shared and twice the group-summed integrated squares.
The energy of the shared freeze and flag factor.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The energy of the group-indexed freeze and flag factor.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The length times the square of the shared freeze factor is at most six times its energy.
The length times the square of the group-indexed freeze factor is at most six times its energy.
The length times the square of the shared part of the third factor of a basic tuple.
The length times the square of the group-indexed part of the third factor of a basic tuple.
The flagged length of the uses is at most K / c times the energies on their ancestors.
The uses lie among their ancestors.
Blueprint lines 2389-2393 for the shared freeze factors of one step: their energies over the
uses are at most C₀² ((64 + 8K)(E_i + E_p) + (1 + K) E_F) in terms of the freeze energies of
the identity output, the pads and the other complement over the ancestors in the blocks.
Blueprint lines 2389-2393 for the group-indexed freeze factors of one step ("joint group
budgets for positive ball ranges"): their energies over the uses and groups are at most
C₀² ((64 + 8K) E_p + (1 + K) E_F) in terms of the joint freeze energies of the pads and of the
other complement over the ancestors of the uses of each group.
Moving an outer sum inside four nested index sums.
Four nested index sums of terms bounded by F.
The freeze budget of one step (both for its shared and its group-indexed factors).