Section 15.1: An exact common-height selection #
This file was automatically generated by Claude.
Formalization of blueprint Section 15, "Common heights and concentration of the core terms"
(sec:core), subsection 1, "An exact common-height selection" (lines 2460-2481) of
blueprint/formalization_blueprint.tex.
An exact common-height selection (blueprint lines 2464-2480) #
Blueprint line 2467 (success probability): if each of m₀ roles is bad at a proportion at most
β of the heights H, then all roles are good at a proportion at least 1 - m₀ β.
Blueprint lines 2461-2462 and 2845-2848: the patterns split into those containing a physical error, those with at least three cores and no error, those with at least three sides and no error, and those with exactly two cores and two sides.
Blueprint lines 2461-2462 ("for terms with exactly two sides, replace the two core
complements by their whole current Z arguments; corrections have at least three sides"): for a
pattern σ without errors, the form of its pieces equals the form with the core slots restored
to Z_l = A_l + S_l + E_l minus the correction patterns, each of which contains an error or has
more sides than σ.
The corrections of form_restore_cores contain an error or more sides than the pattern.
Exact common-height selection (common-height, blueprint lines 2464-2476) #
Blueprint lines 2466-2467 ("the first-success rule has total weight exactly one for every
tuple, hence gives an exact identity in expectation for the finite multilinear expansion"): for a
finite family of tuples τ with one-trial success proportions p_τ ∈ (0, 1], the expansion
Σ_τ F_τ is the sum over trial counts n of Σ_τ (1 - p_τ)^n p_τ F_τ.
Blueprint line 2466 ("success probability is at least 1 - 2 m₀ δ_*"): if each of m₀ roles
has bad proportion at most 2δ among the sampled heights, the one-trial success proportion of a
tuple is at least 1 - 2 m₀ δ, positive when 2 m₀ δ < 1.
Selected modes in torus form (eq:core-torus-form, blueprint lines 2468-2476) #
The quadratic phase identity φ(y) - φ(x) = ω(x)(y - x) + λ(y - x)² for
φ(y) = λ(y-a)² + γ(y-a), ω(y) = 2λ(y-a) + γ.
Blueprint lines 2470-2471 ("a PRE path to the representative supplies an integer shift with
slope error at most D_* Ξ / r_{v_b} ... the quadratic Taylor error is likewise small"): if the
slope of a mode m at x* equals that of the representative a minus the shift s up to θ,
the phase of m on the cell is φ_m(x*) + (ω_a(x*) - s)(y - x*) up to
θ |y - x*| + |λ_m| (y - x*)².
Blueprint eq:core-torus-form (lines 2471-2476) for one role: the selected modes, each with
slope at x* equal to the representative's ω_a(x*) minus its shift s_m up to θ, and with
curvatures at most Λ, synthesize on the cell
Σ_m α_m e(φ_m(y)) = e(ω_a(x*)(y - x*)) Σ_m α_m e(φ_m(x*)) e(-s_m (y - x*)) up to the uniform
error 2π (θ |y - x*| + Λ (y - x*)²) Σ_m |α_m|.
Blueprint line 2470 ("a PRE path to the representative has at most D_* edges; it supplies
an integer shift of size at most D_* E_{h-Δ}, with slope error at most D_* Ξ / r_{v_b}"):
two modes in one PRE component at height h of the pre-cell J of block b differ in slope,
after a shift n·ϑ/L_h with |n| ≤ |alive| E_h, by at most |alive| Ξ / r_J on the pre-cell.
The quadratic phase φ_m(y) = λ_m (y - a_m)² + γ_m (y - a_m) of a mode.
Equations
Instances For
Blueprint eq:core-torus-form (lines 2468-2476) for one selected component: the selected
modes F of the PRE predecessor of the representative a at height h on the pre-cell J
synthesize, at points x*, y of the pre-cell, the representative phase times a trigonometric
polynomial in the integer shifts n_m (|n_m| ≤ |alive| E_h):
Σ_m α_m e(φ_m(y)) = e(ω_a(x*)(y - x*)) Σ_m α_m e(φ_m(x*)) e(-(n_m·ϑ/L_h)(y - x*)), up to
2π (|alive| Ξ/r_J |y - x*| + Λ (y - x*)²) Σ |α_m| when all curvatures are at most Λ.
A pattern containing an error slot: its form is at most the size cap cubed times the normalized error size of that slot.
Blueprint line 2461 and line 2166 ("every term containing a physical error is
O(e^{-k}|R|)"): the error patterns of all cells and groups are bounded, after Cauchy-Schwarz
over the cells and groups, by 324 C B³ (Σ_I |I| #G_I)^{1/2} (Σ_{I,G,l} ‖E‖²)^{1/2}.
Blueprint line 2461 ("for terms with exactly two sides, replace the two core complements by
their whole current Z arguments; corrections have at least three sides"): at one cell the
two-core two-side patterns differ from the restored ones by at most 81 times the error and the
three-side pattern sums.
First-success heights on the attempt cores (blueprint lines 2463-2467) #
Blueprint lines 2468-2469 (product masks): the heights whose first failing role is j:
failure at role j and success at every earlier role.
Equations
- TrilinearHT.Auto.failMask H bad j = {h ∈ H | h ∈ bad j ∧ ∀ j' < j, h ∉ bad j'}
Instances For
Every failed height lies in the failure mask of exactly one role (its first failing role).
Blueprint lines 2468-2469 ("there are at most m₀^n assignments; for a fixed assignment the
conditions form a product mask"): the words of n failed trials are the disjoint union, over the
assignments a : Fin n → Fin m₀ of trials to first failing roles, of the product masks.
Frequency box and the offset side (blueprint lines 2476-2479) #
The physical-error patterns of a leaf (blueprint lines 2149-2166) #
The slot values of a component tuple: the selected component subtotal in a core slot, the pattern piece otherwise.
Equations
Instances For
The index sets of the component tuples: the components of a core slot, a single dummy otherwise.
Equations
- TrilinearHT.Auto.compIdx σ Ks l = if σ l = 0 then Finset.map Function.Embedding.some (Ks l) else {none}
Instances For
Blueprint lines 2463-2467 (the finite multilinear expansion of the core slots): if each core slot of a pattern is the sum of its component subtotals, the pattern form is the sum over the component tuples of the forms of the tuple values.
The role mask of a component at a final height h after the failed trials w with the
assignment a of trials to first failing roles: good at h, bad at its own assigned trials and
good at the trials assigned to later roles.
Equations
Instances For
Blueprint lines 2466-2469 (first success, counted): for a tuple of components, the number of
triples (a, w, h) of an assignment of n failed trials to first failing roles, a word of n
heights and a final height, with every role in its mask, is |S| |H \ S|^n, S the heights at
which all roles are good.
Blueprint lines 2463-2469 (the exact common-height selection with failure assignments): if
every tuple of components has a height at which all its roles are good, the sum over the tuples
is the convergent sum over the trial counts n of the sums over the assignments a of the
failed trials to first failing roles, the words w of failed heights and the final heights h,
with weight |H|^{-(n+1)}, of the sums over the tuples in the product masks.
The goodness of a component is that of any mode it is the minimal PRE component of
(good_iff_of_minimal_pre).
Every core component is the minimal PRE component of a core mode.
Blueprint line 2466 for components: a core component is bad at a proportion at most 2δ of
the upper heights.
The upper heights are nonempty for δ ≤ 1/16.
Blueprint lines 2469-2470 ("group the selected modes at the final successful components"): the sum of a 4-linear form over a product of finite sets equals the sum over the tuples of classes of the forms of the class subtotals.
The common gauge factor of the waves of a mode system: the center cutoff times the center branch phase.
Equations
- Ms.gauge y = ↑(TrilinearHT.Auto.centerCut Ms.zc Ms.δc Ms.ρ y) * ↑(Real.fourierChar (↑Ms.cl * TrilinearHT.Auto.centerPhase Ms.zc Ms.ρ y))
Instances For
The wave of a mode is the gauge factor times the phase character.
Blueprint eq:core-torus-form (lines 2468-2476) for the waves of one group of selected modes:
inside the PRE component of the representative a at height h, the wave sum is the gauge factor
times the representative phase times the trigonometric polynomial in the integer shifts, up to
2π (|alive| Ξ/r_J |y - x*| + Λ (y - x*)²) Σ |α_m|.
The periodic cutoff w ↦ Π_i b({w_i - ρ_i}) on ℝ^d (the true cutoff ζ^ρ).
Equations
Instances For
The truncation error of the periodic cutoff (cutoffP_truncate).
Equations
Instances For
Blueprint lines 2470-2476 (the truncated cutoff of a slot along the cell line): with
QL ξ = θ, the re-centered truncated cutoff at the torus point ξ (y - x*) approximates the true
cutoff ζ^ρ(θ y) within τ_c.
A truncated slot cutoff, re-centered at x* and lifted to the torus by Q₀L, is bounded by
1 + τ_c at every torus point (the truncation approximates the periodic cutoff everywhere).
The error of the gauge multiplier with cutoff parameter δ'' on the true cutoff supports
(blueprint line 1942, "slightly enlarge the cutoffs inside each branch region, making them one on
the required supports"): zero for the enlarged cutoff δ'' = δ/2 (gauge_factors_eq_mult_exact)
and the thin-layer bound 8 d δ'' R_δ otherwise (gauge_factors_eq_mult).
Equations
Instances For
The four true cutoffs times the four gauge phases differ from the four true cutoffs times the
multiplier with cutoff parameter δ'' by at most gaugeErr d δ δ'' (exactly equal for
δ'' = δ/2).
Blueprint lines 2470-2479 (eq:gauge-cancel with the true cutoffs, then their Fourier
truncation): with ξ = θ/(Q₀ L), u = ξ(x - x*) and v = ξ t, the four gauge factors of a
common chart tag at y_j = x + j t are, up to E_g + 4 (1+τ_c)³ τ_c + (1+τ_c)⁴ τ_m, the
torus trigonometric polynomial R(u, v) Π_j K_j(u + j v), where K_j (truncated cutoffs, with
frequencies Q₀ L v) and R (truncated multiplier, with frequencies (L v₁, L v₂)) have
coefficients of modulus at most one.
The difference of two products of four factors with relative errors: if |a_j|, |b_j| ≤ M_j
and |a_j - b_j| ≤ η M_j, then |Π a - Π b| ≤ 4 η Π M_j.
Blueprint lines 2470-2479 (eq:core-torus-form for the four core roles together with the
gauge multiplier): if each input is, on the cell, within η Σ_k |c_{j,k}| of
gauge_j(y) e(γ_j (y - x*)) Σ_k c_{j,k} χ_{n_{j,k}}(ξ (y - x*)) and bounded by Σ_k |c_{j,k}|, and
the four gauges at y_j = x + j t are within E_g of R(u, v) Π_j K_j(u + j v), then on the cell
the product of the inputs is within (4 η + E_g) Π_j Σ_k |c_{j,k}| of
e(Σ_j γ_j (y_j - x*)) R(u, v) Π_j g_j(u + j v) with g_j = K_j · Σ_k c_{j,k} χ_{n_{j,k}}
expanded over box × F_j.
Blueprint line 2478 ("insert an independent offset cutoff ζ^{ρ_l} divided by its constant
expectation c_ζ ≥ 1/2"): for an integrable local form, inserting the offset cutoff
ζ^ρ(θ y) into the side slot l and averaging over the offset recovers c_ζ times the form,
so |Λ(f)| ≤ 2 E_ρ |Λ(f with ζ^ρ f_l in slot l)|.
Blueprint lines 2478-2480 (S' = ζ^{ρ_l} e(-c_l p_{ρ_l}) S_phys, the side gauge joins the
core product): with the side gauge G_l = ζ^ρ e(c_l p_ρ), the form with the offset cutoff inserted
in the side slot is the anchored form with core factor Π_{j ≠ l} f_j(y_j) · G_l(y_l) and side
e(-c_l p_ρ) f_l.
The physical function of a combination of cell modes on J: a.e. the combination of the
waves on J.
The truncated multiplier is bounded by the number of its frequencies (blueprint line 2476:
absolute Fourier costs are fixed powers of D_*).
The decision cell U = anc_{b-4K}(J) of the pre-cell of I.
Instances For
The final CURRENT class at height h of a component K of the block b on the pre-cell J
(blueprint line 2467, "group the selected modes at the final successful components"): the union of
the CURRENT components F_h(x) of the modes x whose minimal component is K.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The final class of the minimal component of x is the CURRENT component of x.
Blueprint lines 2461-2462: a pattern without physical errors and with at least three cores is
the four-core pattern or has exactly one side slot l.
The core reduction on the side states (blueprint line 2461) #
The cell forms of the main columns see only the physical parts of their inputs.
The physical coordinate is idempotent.
The full core subtotal A_{l,G,b} of the block of the cell I restricted to I, in
physical coordinates (zero in the basic U slot, which is a side; blueprint line 2461).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The physical error E_{l,G,b} of the block of the cell I for the lifts L, restricted to
I (zero in the basic U slot).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The frozen coefficients represent the lifted frozen outputs on the retained v_b-cells of
the block of I (the first export of linear_energy).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Blueprint eq:core-side-error on a cell (line 2129): the physical part of the whole leaf
output is the core plus the side plus the error (in the basic U slot the whole output is the
side).
Blueprint eq:core-side-error in the cell form (line 2461): the form of the whole leaf outputs
is the sum over the core/side/error patterns of the forms of their pieces.
The restored two-side patterns of the pieces are the two-side patterns of the whole outputs and the sides (the form sees only physical parts).
form_expand for the leaf data with per-group clearing integers.
restored_eq for the leaf data with per-group clearing integers.
Blueprint line 2461 on one cell: the form of the whole leaf outputs summed over the groups is
at most the restored two-side patterns of the whole outputs and sides, 82 times the error
patterns and the patterns with at least three sides, and the patterns with at least three cores
(a basic U role remains a side: its core and error vanish).
Blueprint line 2164 with the physical side subtotal: on a cell I inside a retained
v_b-cell, ‖1_I A‖ ≤ √5 (‖1_I Z_h‖ + ‖1_I (Z_h - Z_{u_b})‖) + ‖1_I V_phys‖.
The rolling increment Z_{l,G,h} - Z_{l,G,u_b} of the slot l at the depth h.
Equations
Instances For
The physical linear side V_{l,G,b} of the block of the depth h.
Equations
Instances For
Blueprint line 2159 (rolling sides): the rolling increments of a basic slot on the cells of
all groups have total square at most K (20 G₀ + 32) |R| (rolling_budget).
Blueprint line 2159 ("a fixed V_{l,G,b} is counted at most K times"): the physical linear
sides of a basic slot on the cells of all groups have total square at most K V_l |R| under the
linear-side bound.
Before the attempt there are no retained v_b-cells.
Before the attempt the physical error vanishes (the frozen output is zero).
The whole output of a basic slot on an active cell is the restriction of its coarse output.
Blueprint line 2164 on one cell of an actual use: with the whole output, the rolling increment
and the physical linear side of normalized sizes at most B₀, √T, √T, the core and the
physical error have normalized sizes at most coreBd B₀ T and errBd B₀ T.
sizes_at for the group's own schedule, with the output of the family leaf toLeafQ.
The cap of the rolling increments and the physical linear sides on the retained paths of the
second cut: Σ_l (K (20 G₀ + 32) + K V_l) / ρ₂ over the basic slots.
Equations
- One or more equations did not get rendered due to their size.