Section 13.4: Side states and fixed offsets #
This file was automatically generated by Claude.
Formalization of blueprint Section 13, "Fixed modes, the linear side, and hereditary
representatives" (sec:modes), subsection 4, "Side states and fixed offsets" (lines 2123-2170) of
blueprint/formalization_blueprint.tex.
Side states and fixed offsets (blueprint lines 2123-2166) #
Blueprint line 2133: the physical error E = (1 - ζ²) Z_phys - Σ_Φ β_Φ q_Φ with
|q_Φ| ≤ δ_c and Σ |β_Φ| ≤ S satisfies |E|² ≤ 2 |1 - ζ²|² |Z_phys|² + 2 δ_c² S².
Blueprint lines 2135-2139: for each point, the offset mean of the majorant
B(ρ, y) = 2 |1 - ζ^ρ(y)²|² |Z(y)|² + 2 δ_c² K is at most 8 d δ_c |Z(y)|² + 2 δ_c² K
(by offsetMean).
The physical error of the frozen lift and its offset majorant (lines 2125-2139) #
Selection of the branch offsets (blueprint lines 2135-2140) #
Blueprint lines 2135-2140 (first moment): for finitely many independent uniform offsets and measurable nonnegative majorants, some choice of offsets in the unit cubes makes the total majorant at most its expectation.
Blueprint lines 2135-2147 (eq:physical-error before the domination): there are offsets in
the unit cubes for which the total majorant Σ_i Σ_k ∫_{I_k} (2|1 - ζ_i²|² Z_k + 2δ²K) is at most
Σ_i Σ_k ∫_{I_k} (8 d_i δ Z_k + 2 δ² K).
Side caps from integrated budgets (blueprint lines 2159-2166, eq:side-cap) #
Blueprint eq:side-cap via lem:cuts: finitely many families of nonnegative cell weights with
integrated budgets Σ_I |I| a_ν(I) ≤ A_ν |R| are capped simultaneously by one first-crossing cut
at (Σ_ν A_ν)/ρ, of total length at most ρ |R|.
Expansion of catalog outputs into columns (blueprint lemma coeff, lines 488-497) #
Helper instantiation on whole side states (blueprint lines 2167-2169) #
Cores, sides and errors in the active form (blueprint lines 2461-2462, 2845-2848) #
Blueprint eq:core-side-error in a 4-linear form: with Z_l = A_l + S_l + E_l,
H(Z) = Σ_σ H(pieces σ) over all core/side/error patterns.
The data of the core-side-error split of the leaf outputs of an attempt (blueprint
eq:sides, eq:core-side-error, lines 2120-2135): the block length K, the schedule and side
parameters, the mode systems of the slots and groups, the pre-cells of the blocks and the frozen
coefficients, and the slots carrying a basic U (whole sides).
- S : ModeSchedule
Numerical height and block schedule for the leaf split.
- SP : SideParams
Side-event and coherence parameters for the leaf split.
- Ms : Fin 4 → A.Grp → ModeSystem A.G ap.Mc
Frozen mode system in each slot and group.
Pre-cells assigned to each slot, group and block start.
Frozen coefficient of each mode on a pre-cell at a block start.
Predicate selecting slots that carry a whole basic L² side.
Instances For
The block start of a depth: the largest R.1 + K β ≤ h.
Instances For
The squared norm of the physical input of a cell function is its L² energy on the cell.
Distinct cells of one depth are pairwise disjoint.
The core as a sum of minimal CURRENT component subtotals (blueprint lines 2124, 2460) #
The components at one height partition the modes: a sum over all modes is the sum over the components of the sums over their members.
The minimal CURRENT components of the block b on the pre-cell J, as sets of modes.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The core components: the minimal CURRENT components that are not side events.
Equations
- Ms.coreComps S hA SP b J = Ms.allComps S hA b J \ Ms.sideEvents S hA SP b J
Instances For
The frozen evaluation is the sum of the subtotals of all minimal CURRENT components.
Blueprint lines 2124 and 2460 (A = ZTilde - V): on a pre-cell, the frozen evaluation minus the
side subtotal is the sum of the subtotals of the core components.
A cell mode is fixed by the restriction to its cell.
A cell mode vanishes after restriction to a disjoint cell.
Restricting the block side subtotal to one of its pre-cells keeps exactly the side events of that pre-cell (the pre-cells of a block are disjoint).
The rolling mass of a basic leaf slot (blueprint lines 2159-2162, eq:rolling-energy) #
Restrictions to smaller sets have smaller norm.
Whole outputs of leaf slots: U slots and cells without decision cell (lines 2159-2162) #
The linear sides of a basic leaf slot (blueprint lines 2104-2118, 2160) #
The whole outputs of a U slot of a leaf (blueprint lines 2159-2162) #
The side mass of a basic leaf slot (blueprint lines 2159-2162) #
The side mass of a U leaf slot (blueprint lines 2159-2162) #
Size cuts from integrated budgets (blueprint lines 2163-2166) #
A sum over a union of finite sets of nonnegative terms is at most the sum of the sums.
Piece sizes on retained cells of a leaf (blueprint lines 2163-2166) #
Side caps and three sides on a leaf (blueprint lines 2159-2166, 2372-2384) #
Variation of single ball pads over global histories (blueprint lines 2390-2391) #
Variation of single cumulative pads over global histories (blueprint lines 2390-2391) #
Global pads of the transfer steps (blueprint lines 2386-2391, 2412-2420) #
Intertwining transfer steps with a restriction (blueprint line 2386) #
Two raw transfer steps (slot flag, helper pads, complement pads) are intertwined by r when
their flags agree and r intertwines all their pads.
Equations
Instances For
Single pads after global histories on any catalog (blueprint lines 2390-2391, 2414-2420) #
lem:cuts for finitely many families of nonnegative cell weights with integrated budgets
Σ_I |I| a_ν(I) ≤ B_ν |R|: one first-crossing cut of total length at most ρ |R| makes all
retained path sums of every family at most (Σ_ν B_ν)/ρ.
The pre-cell J = anc_{b-2K}(I) of a leaf cell I (blueprint line 1975).
Instances For
Side states of the basic roles on the main columns (blueprint lines 2124-2133) #
The full core subtotal A_{l,G,b} of the block b (blueprint line 2124): the subtotals of
the core components (the minimal CURRENT components that are not side events) on the retained
pre-cells, with the frozen coefficients.
Equations
Instances For
Blueprint lines 2124-2133 (ZTilde = A + V): a column function supported on the disjoint
retained
pre-cells of a block, which restricts on each of them to the frozen evaluation of its
coefficients, is the sum of the full core subtotal and the side subtotal of the block. Every
mode alive at the decision cell lies in exactly one minimal CURRENT component, which is either a
core component or a side event.
The retained v_b-cells of a block are pairwise disjoint (they have one depth).
Blueprint line 1967 and lines 2124-2133: the frozen lifted output of a block,
ZTilde_{l,G,b} = R_{l,G} Z_{l,G,u_b} on the retained branches, is the sum A_{l,G,b} + V_{l,G,b} of
its full core subtotal and its side subtotal, for frozen coefficients representing it on the
retained v_b-cells (as produced by linear_energy).
The physical coordinate of a column function, in the main column space.
Instances For
Blueprint eq:sides (line 2125): in a basic B role the side state at the depth h of the
block b, S_{l,G,h} = Z_{l,G,h} - Z_{l,G,u_b} + V_{l,G,b}, in physical coordinates. Here
Z_{l,G,h} is the coarse output, Z_{l,G,u_b} the output frozen at u_b = b - 4K (zero before
the attempt) and V_{l,G,b} the side subtotal of prop:linear-side.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A restricted side state splits into its rolling energy and its fixed block subtotal.
Blueprint eq:core-side-error (line 2129): the physical error
E_{l,G,b} = (Z_{l,G,u_b})_phys - (ZTilde_{l,G,b})_phys of a block.
Equations
Instances For
Blueprint eq:core-side-error (lines 2127-2130) in a basic B role: in physical coordinates
the coarse output at any depth h of the block b is the full core subtotal plus the side state
plus the physical error, Z_{l,G,h} = A_{l,G,b} + S_{l,G,h} + E_{l,G,b}, for frozen coefficients
representing ZTilde_{l,G,b} on the retained v_b-cells. (In a basic U role the whole output is
the side state, with no core and no error.)
The physical error of the frozen lift on the main columns (blueprint lines 2131-2156) #
Blueprint line 2131 ("physical supremum"): on an active cell the scalars of its main labels are bounded atoms or bounded templates, hence at most one.
Blueprint line 2131 ("on a normalized u_b-cell the already fixed main output
Z_{l,G,u_b} = Σ_Φ β_Φ Φ has coefficient sum and physical supremum at most D_m^C, with no
pre-lag loss"): on an active cell U of depth u the frozen main output is the main
combination Σ_Φ β_Φ (φ_Φ, √ε_Φ e_Φ) of the primaries at U, with
Σ_Φ |β_Φ| ≤ √N colBudget ‖Z‖_U / √|U| (private-coordinate recovery) and physical supremum on U
at most Σ_Φ |β_Φ|.
Blueprint lines 2132-2143: on a retained v_b-cell J of a block, for a main representation
Z_{u_b} = Σ_Φ β_Φ Φ on a cell U ⊇ J (frozenZ_main_rep), every lift with the main private
weights and gauge s = ζ² (every admissible choice of first-match expansions) has physical error
E = (1 - ζ²) (Z_{u_b})_phys - Σ_Φ β_Φ q_Φ on J, hence
|E|² ≤ 2 |1 - ζ²|² |(Z_{u_b})_phys|² + 2 δ_c² (Σ_Φ |β_Φ|)² (|q_Φ| ≤ δ_c).
Blueprint lines 2144-2150: for the actual main uses I ∈ U_i of the roles and groups i
(fixed before the offsets), at most N_use of them through each point of the root R, and
majorants B_i(ρ, y) = 2 |1 - ζ_i^ρ(y)²|² Z_{i,I}(y) + C with Z_{i,I} ≤ M on I,
eq:offset-mean and the path multiplicity bound the offset mean of Σ_i Σ_{I ∈ U_i} ∫_I B_i by
(8 d_max δ M + C) N_use |R|, and the first moment method selects offsets in the unit cubes
attaining this bound (no measurable selection of expansions is needed).
Blueprint line 1967 (retention rule): the v_b-ancestor of a cell with an actual use of the
group in the block [b, b + K) is retained, when it lies below the attempt root.
Blueprint eq:physical-error (lines 2151-2156), with the selection of lines 2144-2150: for the
roles and groups i of a search leaf (role l_i, group G_i with center tag z_i, catalog,
ball level and shared history), the actual main uses I ∈ U_i (fixed before the offsets, at most
N_use through each point of the root) in their blocks [b(I), b(I) + K), active cells closed
under ancestors, fresh normalized attempt roots (‖1_V F_{l,j}‖² ≤ C_F |V| on active cells) and at
most N main labels at each active cell, there are offsets in the unit cubes such that every
choice of first-match lifts at these offsets (main private weights, gauge (ζ_i^ρ)², corrections
|q_Φ| ≤ δ_c) has physical errors
Σ_i Σ_{I ∈ U_i} ∫_I |E_{l_i,G_i,b(I)}|² ≤ (8 d_max δ + 2 δ_c²) · 4 N colBudget² C_F · N_use |R|
(δ the cutoff width; with δ = δ_c this is the blueprint's 2 D_m^{C''} d_max δ_c |R|). No
measurable selection of expansions is used: the offsets are chosen by the explicit majorant
B(ρ, y) = 2 |1 - ζ^ρ(y)²|² |(Z_{u_b})_phys(y)|² + 2 δ_c² (Σ|β|)², which dominates every
admissible choice.
Integrated budgets of the side states (blueprint line 2159) #
Blueprint lem:variation with the loss G₀ and bounded overlap: if the depth intervals are
colored with M colors such that intervals of one color are disjoint, the bound of
basic_variation_G0 is multiplied by M.
Blueprint line 2159 ("rolling sides have integrated square budget K G₀ |R| by
eq:variation, since the intervals [u_b, s] have overlap O(K)"): with the blocks
[b, b + K) starting on R.1 + Kℤ, u_b = b - 4K and the frozen output zero before the attempt,
the rolling sides Z_{l,G,s} - Z_{l,G,u_b} on certified cells of the depths s ∈ S_d have total
square at most K (20 G₀ + 32) |R|. Depths with b - 4K ≥ R.1 use eq:variation with intervals
colored modulo 5K; the first 4K depths use the one-time projection estimate.
Blueprint lines 2393-2399 and 2415-2419 (eq:stack-energy, "its base term uses
Lemma variation on [u_b, b], whose overlap over blocks is bounded"): at the block starts
t ∈ K ℕ (blocks [b, b + K) starting on R.1 + K ℤ, u_b = b - 4K, the frozen output zero
before the attempt) the rolling block inputs Z_{l,G,b} - Z_{l,G,u_b} on certified cells have total
square at most (20 G₀ + 32) |R|: the intervals [u_b, b] of block starts are colored by b / K
modulo 5 (eq:variation per color), and at most four block starts lie in the first 4K depths
(one-time projection estimate).
Blueprint line 2159 for the side states of a basic B role (eq:sides): on the certified
cells of the depths s ∈ S_d, Σ_{s,G} ‖1_E S_{l,G,s}‖² ≤ 2 K (20 G₀ + 32) |R| + 2 K Σ_{b,G} ‖V_{l,G,b}‖², the rolling sides by rolling_budget and each fixed V_{l,G,b} counted
at most K times (sum_block_le); eq:linear-energy then bounds the second sum.
Blueprint lines 2393-2399 and 2415-2419 (eq:stack-energy) for the block inputs of a basic B
role: at the block starts t ∈ K ℕ the side states are the block inputs
W_{l,G,b} = Z_b - Z_{u_b} + V_{l,G,b}, and on certified cells
Σ_{b,G} ‖1_E W_{l,G,b}‖² ≤ 2 (20 G₀ + 32) |R| + 2 Σ_{b,G} ‖V_{l,G,b}‖²: the rolling block inputs
by rolling_budget_blocks (bounded overlap of the intervals [u_b, b]) and each fixed
V_{l,G,b} once.
The side caps (blueprint eq:side-cap, lines 2160-2163) #
The restriction to a disjoint union of cells has squared norm the sum over the cells.
The integrated budget of side states over the needed cells of each depth, written cell by
cell: the needed cells of one depth are disjoint (norm_sq_restrict_biUnion).
Terms containing a physical error (blueprint line 2164) #
Blueprint eq:absolute with all four exponents two, for the cell form: its modulus is at
most C_κ times the product of the normalized L² sizes of the physical parts.
Blueprint line 2164 ("the lift is pointwise bounded and Z_{u_b} = Z_s - (Z_s - Z_{u_b}), so
the full core and error sizes on retained cells are also at most P^C"): on a cell I inside a
retained v_b-cell of the block, the physical error and the full core subtotal are bounded by
the coarse output, the rolling side and the side subtotal on I:
‖1_I E‖ ≤ (1 + √5)(‖1_I Z_h‖ + ‖1_I (Z_h - Z_{u_b})‖) and
‖1_I A‖ ≤ √5 (‖1_I Z_h‖ + ‖1_I (Z_h - Z_{u_b})‖) + ‖1_I V‖.
The normalized L² size of the physical part on a cell is the square root of its cell
integral divided by the length (so that |I| e_I² = ∫_I |x_phys|², as in eq:physical-error).
Helper instantiation on the main columns (blueprint lines 2167-2169) #
Blueprint lines 2167-2169 ("helper ranks exceed every main rank, so their insertion leaves all
previously fixed main projections ... unchanged"): catalog columns of rank above r do not
change the main selections of rank at most r.
Main tests whose target and history ranks lie below every inserted column keep passing.
The ball filters of the levels j ≤ 4 are unchanged by helper columns of rank L + 5.
The cumulative filters are unchanged by helper columns of rank L + 5.
Blueprint "Helper instantiation" (lines 2167-2169) on the main columns: for helper tests of
rank L + 5 on fixed whole bases at the active cells (the entire side states, sideState_base),
there are helper templates of rank L + 5 born at the active cells such that all helper tests pass
on the extended catalogs, every main test of ranks at most L + 4 that passed still passes, and
the ball filters of the levels j ≤ 4 and the cumulative filters are unchanged (so are the main
projections, offsets and side states built from them); the insertions per cell are counted as in
lem:closure (helper_closure).
Blueprint line 2168 ("the helper bases are these entire states"): a side state (any physical column function) restricted to an active cell is an admissible helper base: its template coordinates vanish and it is supported on the cell.