Section 13.2: Two graphs and height stabilization #
This file was automatically generated by Claude.
Formalization of blueprint Section 13, "Fixed modes, the linear side, and hereditary
representatives" (sec:modes), subsection 2, "Two graphs and height stabilization" (lines
1978-2045) of blueprint/formalization_blueprint.tex.
Exceptional blocks and the tiny span (blueprint lines 1987-2000) #
Blueprint lines 1991-1993: if the logarithmic evaluations x(a) of all height-H vectors
lie in at most d packets of width W, a block start b = βK is exceptional when some
x(a) ∈ (b - 2K - log₂T, b + K + log₂T), and W + 3K + 2 log₂ T ≤ 4K, then at most 4d
blocks are exceptional.
The height of a rational vector: the largest entry height.
Equations
- TrilinearHT.Auto.vecHeight a = Finset.univ.sup fun (i : Fin d) => TrilinearHT.Auto.rationalHeight (a i)
Instances For
Blueprint lines 1995-1997: at a nonexceptional block (every height-H vector is tiny,
|a·Θ| ≤ ε, or large, |a·Θ| ≥ Λ), every height-H vector in the rational span of the tiny
height-H vectors is tiny, provided (n+1) d! H^{d²+d} ε < Λ for any spanning family size
n (here all tiny vectors of height at most H).
Height stabilization (lem:stabilize, blueprint lines 2002-2029) #
Blueprint lines 2016-2018: in the free quotient of ℤⁿ by a saturated lattice Λ, a
relation q x ≡ 6^R z (mod Λ) with 0 < q < 2^(R - Δ) forces x ≡ 6^Δ y (mod Λ) for an integer
vector y.
Blueprint lines 2010-2028 (core of lem:stabilize): let K be a rational subspace,
ι the inclusion of the ϑ-coordinates, and U ⊆ K_B = ι⁻¹ K spanned by integer generators
g_i with entries at most G. Suppose a = Σ_j (β_j/Q) a_j with 0 < Q < 2^(R-Δ), witnesses
a_j + ι(m_j / 6^(h-R)) ∈ K and a + ι(m_h / 6^h) ∈ K, and that the integer vector
Q m_h - 6^R Σ_j β_j m_j (which lies in K_B) lies in U (this is U_h = U_{h-R} together with
its size bound). Then some integer m' gives a PRE witness a + ι(m' / 6^(h-Δ)) ∈ K with
|m'| ≤ 6^(R-Δ) Σ_j |β_j/Q| |m_j| + k G.
Blueprint line 2012: for an increasing family of subspaces of a d-dimensional space, at most
d R heights h ≥ R have V_{h-R} ≠ V_h.
The span U_S of integer vectors of K_B = ι⁻¹ K with entries at most S (blueprint
line 2012).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Blueprint lem:stabilize (lines 2002-2029), witness form: at a height h ≥ R where the
kernel spans are stable, U_{S_{h-R}} = U_{S_h}, a CURRENT relation a + ι(m_h/6^h) ∈ K
together with a bounded expansion a = Σ_j (β_j/Q) a_j in vectors with height-(h-R) witnesses
(the defining basis of the stable V_{h-R}) yields a direct PRE witness at height h - Δ,
of size at most 6^(R-Δ) Σ_j |β_j/Q| |m_j| + n S_{h-R}.
Coherence of the good predicates (blueprint lines 2031-2047) #
Height-indexed PRE components E_h(m) and CURRENT components F_h(m) of a finite mode set
with primary labels π, abstracting the two graphs of eq:PRE and eq:CURRENT: components
contain their mode and are determined by any member, PRE refines CURRENT, and both increase with
height.
Predecessor graph component of a mode at each height.
Current graph component of a mode at each height.
- π : Mode → P
Primary label associated with each mode.
Instances For
The primary labels π(S).
Equations
- C.labels S = Finset.image C.π S
Instances For
Blueprint eq:good: a mode is good at height h ≥ Δ when its PRE predecessor carries
nine tenths of the primaries of its CURRENT component, and nine tenths of those primaries are
nonexceptional and good for the primary (goodP h).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Blueprint lines 2034-2035: two good modes in one CURRENT component at height h have the
same PRE predecessor at h - Δ, when good primaries satisfy the conclusion of lem:stabilize
(two of their modes in one CURRENT component at h are PRE-joined at h - Δ).
Equations
- C.instDecidableGood Δ goodP h m = id inferInstance
The predicate eq:good depends only on the two components.
Blueprint line 2035: modes in one minimal PRE component have identical predicates at every height.
The bad heights h ≤ J of a mode.
Equations
- C.badHeights Δ goodP J m = {h ∈ Finset.range (J + 1) | ¬C.Good Δ goodP h m}
Instances For
A core mode has at most δ (J + 1) bad heights.
Instances For
Blueprint line 2045: a core mode has bad proportion at most 2δ on the upper heights,
for δ ≤ 1/16 and J ≥ 2.
Components of the PRE and CURRENT graphs (blueprint lines 1980-1988) #
The components of two height-indexed edge relations (eq:PRE and eq:CURRENT): PRE edges
are CURRENT edges and both grow with height.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The edge relation of eq:PRE / eq:CURRENT at height h with threshold θr on the
interval [a, a + r]: some integer vector n with |n|_∞ ≤ E_h brings the frequency difference
within θr after the shift n·ϑ/L_h.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The PRE and CURRENT components on a pre-cell [a, a + r_v] (blueprint lines 1980-1988):
PRE uses Ξ/r_v, CURRENT Ξ/r_t with r_t ≤ r_v.
Equations
- S.preCurrent hA ω ϑ π a rv rt hrt = TrilinearHT.Auto.ModeComponents.ofEdges (S.gapEdge ω ϑ a rv (S.Ξ / rv)) (S.gapEdge ω ϑ a rv (S.Ξ / rt)) π ⋯ ⋯ ⋯
Instances For
Lem:stabilize on the attempt (blueprint lines 2002-2029) #
A walk in the graph of gapEdge sums its witnesses: the endpoint frequencies differ by a
shift with integer vector of size at most k E_h up to k θ, k the length.
Reachability in the graph of gapEdge within a finite mode set gives a summed witness with
fewer steps than modes.
A rational vector of height at most B in the span of vectors of height at most B in
ℚⁿ is Σ_k (β_k / Q) v_{e k} over a subfamily, with integers 0 < Q and |β_k| at most
n! (B · B^{n(n+1)})^n.
The tiny span of a nonexceptional block (blueprint lines 1995-1997) #
The rational span K_rat of the tiny vectors.
Equations
- TrilinearHT.Auto.tinySpan Θ H ε = Submodule.span ℚ (TrilinearHT.Auto.tinySet Θ H ε)
Instances For
Blueprint lines 1995-1997: at a nonexceptional block every height-H vector of the tiny
span is tiny.
The stabilization core (blueprint lem:stabilize, lines 2002-2029) #
The witness spans V_i: height-D vectors q with an integer m, |m|_∞ ≤ D E_i,
such that q + (0, m/6^i) lies in K.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The expansion constant d! (D · D^{d(d+1)})^d of rational_span_expand_bounded.
Instances For
Blueprint lem:stabilize, core: if the witness spans and the kernel spans are stable between
h - R and h, a vector a of height at most D with a CURRENT relation
a + (0, m_h/6^h) ∈ K, |m_h| ≤ D E_h, has a witness m' at height h - Δ of size at most
6^{R-Δ} J C D E_{h-R} + d_z S_{h-R}, where C is the expansion constant and J the number of
height-D vectors.
Blueprint lem:stabilize (lines 2002-2029) on a pre-cell [a₀, a₀ + r_v]: let the modes of
a fixed primary p differ in frequency by a·Θ with a of height at most D, let the block be
nonexceptional for Θ (eq:gap with T) and let the witness and kernel spans be stable between
h - R and h. Then two modes of the primary in one CURRENT component at height h are
directly PRE-adjacent at height h - Δ. The numeric side conditions are those of
eq:mode-parameters.
Blueprint line 2012 for one primary: all but (1 + d + d_z) R heights h < N are good for
the primary (the witness spans and the kernel spans are stable between h - R and h).
The goodness of a primary p at height h (blueprint lines 2006 and 2031): the block is
nonexceptional for its frequency vector Θ_p (eq:gap with thresholds ε, Λ at height Hn),
R ≤ h, and its witness and kernel spans are stable between h - R and h.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Blueprint lem:stabilize, counting part: for a primary that is nonexceptional at the block,
at most (1 + d + d_z) R heights h < N are not good for it.
Blueprint lines 1913 and 2005: keyed modes (one key = one primary on its first-match cell,
with one curvature and one recentring point) with slopes ω_m(y) = 2λ_m(y - a_m) + γ_m and
same-key frequency differences (a - b)·(θ_v, θ_z) with entries of height at most B differ
in slope by a'·Θ' for the normalized vector Θ' = (θ_v, θ_z/Q₀), with a' of height at most
2 (Q₀ · 3 B⁴)².
keyed_hsame in the form used by ModeSchedule.hstab_of_primaryGood: on any set of modes
(e.g. those alive on a pre-cell), with keys as primaries, slopes ω_m(y) = 2λ_m(y - a_m) + γ_m
and the integral height bound D ≥ 2 (Q₀ · 3 B⁴)².
Persistence of edges across pre-cells (blueprint lines 2084-2086) #
An edge on a cell persists on a sub-cell with a larger threshold, for modes transported by
f with unchanged slopes on the sub-cell.
Reachability in the edge graph transports along f.
Blueprint lines 1984-1986: both graphs on one pre-cell transport to a later pre-cell with the same thresholds.
Blueprint line 2005 for the frozen modes: two modes of one key differ in slope by a·Θ',
Θ' = (θ_v, θ_z/Q₀), with a of height at most D.
The frozen mode graphs on retained pre-cells (blueprint lines 1980-1988) #
The block thresholds r_t ≤ r_v give Ξ/r_v ≤ Ξ/r_t.
The PRE and CURRENT components of the frozen list at the decision depth u on the pre-cell
J (depth J.1 = v), with CURRENT threshold at depth t ≥ v (blueprint lines 1980-1988).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The frozen mode graphs of the block b (u_b = b - 4K, v_b = b - 2K, t_b = b + K) on the
pre-cell J.
Equations
Instances For
Inclusion of alive sets for nested decision cells.
Instances For
Blueprint lines 1984-1986 and 2178 (persistence): both graphs of the pre-cell J of block b
transport into those of the pre-cell J' ⊆ J of any later block b' ≥ b.
Exceptional blocks on a path (blueprint line 1996) #
Blueprint eq:gap (lines 1991-1995): the block with start b is exceptional for the
frequency vector Θ at height H when some rational vector a of height at most H has
T⁻¹ / r_{v_b} < |a·Θ| < T / r_{t_b} (neither tiny nor large), where r_n = r₀ 2^{-n},
v_b = b - 2K and t_b = b + K.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Blueprint line 1996 ("zero evaluations are always tiny"): a witness of an exceptional block has a nonzero evaluation.
Blueprint line 1996: each primary is exceptional in at most 4 dim Θ blocks on a path
(C d_max). By lem:height the logarithms x(a) = log₂(|a·Θ| r₀) of the nonzero evaluations of
height-H vectors lie in at most dim Θ packets of width W = 8 (d+1)³ log(2H) / log 2; a block
start b = b₀ + βK is exceptional only if some x(a) lies in (b - 2K - log₂ T, b + K + log₂ T),
and a packet meets this window for at most four starts when W + 2 log₂ T ≤ K.
Blueprint line 1996 at the chosen mode schedule (eq:mode-parameters, with the inputs
d_max, D_*, B_* ≥ 2 and Q₀ ≥ 1 of chooseSchedule): when the packet width W of the schedule
is at least the width 8 (d+1)³ log(2H) / log 2 of lem:height at the schedule height H in
dimension d, each primary of frequency dimension d is exceptional in at most 4d blocks
(K ≥ W + 2 log₂ T + C_K log₂ D_*).
The tiny span at a nonexceptional block of the schedule (blueprint lines 1997-1998) #
Elementary consequences of eq:mode-parameters #
Blueprint line 1998 at the chosen schedule: the spanning constant (3H²)^d d! H^(d²+d) of the
tiny span (tiny_of_mem_tinySpan) times the tiny threshold T⁻¹ / r_{v_b} is below the large
threshold T / r_{t_b}, because the threshold ratio is T² 2^{3K} and
T > (d_max H)^(C_T d_max⁴) Ξ with C_T ≥ 4 (eq:mode-parameters).
Lem:stabilize at the chosen schedule (blueprint lines 2002-2028) #
A block that is not exceptional (¬ExceptionalAt) satisfies eq:gap for every rational
vector of height at most ⌊H⌋.
The PRE and CURRENT components of the block with start b on the v_b-cell
[a₀, a₀ + r_{v_b}] (eq:PRE with Ξ/r_{v_b}, eq:CURRENT with Ξ/r_{t_b}), r_n = r₀ 2^{-n},
v_b = b - 2K, t_b = b + K.
Equations
Instances For
The size bound of the generators of the spans U_i (blueprint line 2012): integer vectors
z with |z|_∞ ≤ ⌊C_*³ D_* E_i⌋, that is |z|_∞ ≤ C_*³ D_* E_i.
Instances For
Blueprint lem:stabilize: the height h is good for the primary p of the block with start
b (frequency vector Θ_p) when p is nonexceptional at the block (eq:gap at height H),
h ≥ R_*^{ht}, and neither the span V_i of the height-D_* vectors q' with witnesses
q' + (0, m/L_i) ∈ K_rat, |m|_∞ ≤ D_* E_i, nor the span U_i of the integer vectors of K_B of
size at most C_*³ D_* E_i changes between i = h - R_*^{ht} and i = h.
Equations
Instances For
The expansion constant of rational_span_expand_bounded in dimension d ≤ d_max at height
D ≤ D_* is at most C_* ("coefficients and common denominator at most C_*").
The fixed-power choice of A₀ (A₀ ≥ (C_* 6^{R_*^{ht}} B_* D_*)^{C_A} with C_A ≥ 5)
dominates C_*² D_* 6^{R_*^{ht}} + d_max C_*³ D_*.
The heights of the CURRENT and PRE relations in the proof of lem:stabilize are at most H:
max(D, 3 (D M)²) ≤ ⌊H⌋ for D = ⌊D_*⌋ and M ≤ 3 D_* E_{J_*} L_{J_*}.
⌈e⌉ + 6^i ≤ 3 D_* E_{J_*} L_{J_*} for 0 ≤ e ≤ D_* E_{J_*} and i ≤ J_*.
Blueprint lem:stabilize, counting part, at the chosen schedule: for a primary p that is
nonexceptional at the block with start b, at most 3 d_max R_*^{ht} heights are not good for
it (C d_max R_*^{ht}): the heights below R_*^{ht}, and those where the rank of V_i or U_i
changes between h - R_*^{ht} and h.
Blueprint lem:stabilize at the chosen schedule, the PRE edge: let the modes of the frozen list
on the v_b-cell [a₀, a₀ + r_{v_b}] be at most D_* in number, with primaries π whose
frequency vectors are Θ_p = (θ_{v,p}, ϑ) of dimension at most d_max, two modes of one primary
differing in slope by a·Θ_p with a of height at most D_* (eq:mode-differences). If h ≤ J_*
is good for the primary of x (stabGood), then a mode x' of the same primary in the CURRENT
component of x at height h is directly PRE-adjacent to x at height h - Δ, Δ = 10. All
numeric side conditions are derived from eq:mode-parameters with C_A ≥ 5 and C_T ≥ 4 as the
choice of the absolute constants.
Lem:stabilize at the chosen schedule, in component form: under the hypotheses of
Valid.stabGood_pre, x' lies in the PRE component of x at height h - Δ.
Coherence of the good predicates at the chosen schedule (blueprint lines 2030-2045) #
Blueprint line 2039: modes in one minimal PRE component have the same bad heights, so the core/side decision is constant there.
The side parameters of the coherence argument read off a schedule (blueprint lines
2006-2024): heights ⌊H⌋, mode-difference height ⌊D_*⌋, gap threshold T, witness bounds
⌊D_*⌋ · witE h = ⌊D_* E_h⌋, kernel sizes ⌊C_*³ D_* E_h⌋, lag R_*^{ht}, shift Δ = 10, top
height J_*, core fraction δ_*.
Equations
Instances For
J_* ≥ 2 from J_* ≥ C δ_*^{-2} d_max R_*^{ht} log(2 D_m) with C ≥ 1, δ_* ≤ 1,
D_m ≥ 2.