Trilinear Hilbert transform: chooseSchedule #
Blueprint mode-schedule (line 1976, THT.Modes.chooseSchedule): given the main budget
D_m, the dimension bound d_max, the mode budget D_*, the cutoff B_*, the clearing
integer Q₀ and the packet width W(H) as a function of the height H (lem:height), the
parameters of eq:mode-parameters can be chosen in the displayed order (K last, using
W(H) at the chosen H), and all their logarithms are polynomial in
Λ = d_max + log D_* + log B_* + log D_m + log Q₀ + 1: log H ≤ M Λ^{12},
log T ≤ M Λ^{16}, K ≤ 2 W(H) + M Λ^{16}, with M depending only on the absolute constants.
The averaging projection of the doubled coordinates onto the diagonal.
Equations
- TrilinearHT.Auto.diagAvgQ d i j = if TrilinearHT.Auto.foldIdx d i = TrilinearHT.Auto.foldIdx d j then 1 / 2 else 0
Instances For
Primaries of a ball are joined to the group center (blueprint lines 1893-1903) #
Complexity of the branch charts of a group center (blueprint lines 1893-1903) #
The Gevrey constant of the bump normalization.
Equations
Instances For
Blueprint lines 1893-1903: the branch chart of a center tag z in a slot of multiplier
c (phase -c p_ρ, amplitude the periodic Gevrey branch cutoff of width δ) has Gevrey order
32 complexity at every height H ≥ d A 8³² (2/δ) dominating e², its dimension and matrix
heights (offsets in [0,1]).
Recentred first-match expansions (blueprint lines 1903-1922: "recentring adds only a #
common unrestricted linear phase")
Blueprint first-match, recentred at an arbitrary point a₀: for a primary Φ of tag v
matched to a center z by an edge at length r, the product chart P = Φ ⊗ branchChart has,
on the window |t| ≤ R r around a₀, an exact absolutely convergent expansion
φ_P(a₀ + t) = Σ_ℓ a_ℓ e(λ_* t² + (β + σ_ℓ·θ) t) with one common curvature and rational
frequency differences, everything quasipolynomial in the translated complexity and B.
First-match expansions of attempt primaries (blueprint lines 1903-1922) #
Finite first-match expansions (blueprint line 1907: + O(δ_c)) #
The global mode lift (blueprint lines 1932-1940) #
The pointwise lift as a linear map.
Equations
- TrilinearHT.Auto.modeLiftLin own s q a εP εM = { toFun := TrilinearHT.Auto.modeLift own s q a εP εM, map_add' := ⋯, map_smul' := ⋯ }
Instances For
The lift written in coordinates: each output coordinate is a combination of the input coordinates.
The data of a global mode lift: measurable gauge s = (ζ^ρ)² with |s| ≤ 1, measurable
physical corrections |q_Φ| ≤ δ, mode coefficients and private weights obeying the hypotheses
of modeLift_norm_sq_le (blueprint lines 1932-1940).
- own : Md → Pr
Primary label owning each mode.
Bounded measurable gauge multiplying the physical component of the lift.
Small physical correction associated with each primary label.
Measurable coefficient of each lifted mode.
- εP : Pr → ℝ
Positive private-coordinate weight assigned to each primary label.
- εM : Md → ℝ
Nonnegative private-coordinate weight assigned to each mode.
- δ : ℝ
Uniform norm bound for the primary physical corrections.
- a_meas (m : Md) : Measurable (self.a m)
- s_meas : Measurable self.s
- q_meas (Φ : Pr) : Measurable (self.q Φ)
Instances For
The lift at the point y.
Equations
Instances For
The global lift R on square-integrable columns.
Equations
- L.op = { toFun := fun (F : ↥(TrilinearHT.Auto.ColumnL2 Pr)) => MeasureTheory.MemLp.toLp (fun (y : ℝ) => (L.at_ y) (↑↑F y)) ⋯, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous √5 ⋯
Instances For
Blueprint lines 1934-1937 with the zero convention before the match: the lift carries a main output exactly to its mode synthesis whenever the physical corrections are exact on the primaries with nonzero coefficient.
First-match cells (blueprint line 1891: "At its first match on I₀") #
The maximal cells of a finite family of dyadic cells.
Equations
- TrilinearHT.Auto.maxCells G C = {I ∈ C | ∀ J ∈ C, TrilinearHT.Auto.dyadicGridCell G I.1 I.2 ⊆ TrilinearHT.Auto.dyadicGridCell G J.1 J.2 → J = I}
Instances For
Every cell of the family lies in a maximal one.
Two maximal cells sharing a point coincide.
The gauge of a group center (blueprint lines 1893-1900) #
The atom of a primary times the branch chart of a center is the primary atom times the gauge
ζ^ρ e(-c p_ρ).
Counted first-match truncation (blueprint line 1913: the number of modes is at most #
D₁)
Frequencies outside the box of radius 2^(K+1) lie in the dyadic shells from 2^K on.
The absolute tail outside a frequency box from dyadic shell bounds (Σ_shell |a|) T ≤ B.
Truncation of an absolutely convergent unimodular expansion to a frequency box, with the remainder controlled by the shell bounds.
Bounded expansions in a basis (blueprint line 1958: "Expressing a height-D_* vector in a #
basis of such vectors in dimension at most d_max costs coefficients and common denominator at
most C_*")
Cramer numerators of a pivot minor reproduce every vector of the column span.
The normalized frequency vector Θ' = (θ_v, ϑ), ϑ = θ_z/Q₀ (blueprint line 1893) #
Scaling the ϑ-coordinates of a rational vector by Q₀.
Equations
- TrilinearHT.Auto.scaleZ dv dz Q0 a = Fin.append (fun (j : Fin dv) => a (Fin.castAdd dz j)) fun (l : Fin dz) => ↑Q0 * a (Fin.natAdd dv l)
Instances For
Augmented modes on cells (eq:modes, blueprint line 1928) #
The augmented mode 1_J (ψ e_phys + √ε e_m) on a cell J.
Equations
- TrilinearHT.Auto.augMode J ψ ε m = J.indicator fun (y : ℝ) => ψ y • EuclideanSpace.single none 1 + ↑√ε • EuclideanSpace.single (some m) 1
Instances For
The frozen-mode data interface of one role and group (blueprint lines 1971-1975) #
The frozen modes of one role, group and offset (blueprint "Frozen-mode data interface",
lines 1971-1975): for each primary and first-match cell, the finite list of modes with one
curvature, the coefficient functions, the rational frequency differences eq:mode-differences
and the private indices, together with the pointwise lift.
- Md : Type
Finite type of frozen modes.
- deq : DecidableEq self.Md
Pointwise global lift from primary columns to frozen modes.
- zc : ChartTag
Common curvature tag of the frozen modes.
- δc : ℝ
Core fraction controlling the frozen-mode branch profiles.
Horizontal branch offset in the coordinates of the common curvature tag.
- cl : ℤ
Integer slot index used as the frozen reference slot.
First-match cell associated with each frozen mode.
Quadratic phase coefficient of each frozen mode.
Linear phase coefficient of each frozen mode.
- Key : Type
Type of keys identifying a primary label together with its first-match cell.
- kdeq : DecidableEq self.Key
Key assigned to each frozen mode.
Dimension of the primary tag associated with a mode key.
Horizontal direction of the primary tag associated with a mode key.
- Bσ : ℝ
Uniform rational-frequency coefficient budget for mode differences.
- Λ : ℝ
Uniform quadratic phase budget for the frozen modes.
- key_diff (m m' : self.Md) : self.keyOf m = self.keyOf m' → ∃ (a : Fin (self.dvOf (self.keyOf m) + self.zc.dim) → ℚ) (b : Fin (self.dvOf (self.keyOf m) + self.zc.dim) → ℚ), (∀ (i : Fin (self.dvOf (self.keyOf m) + self.zc.dim)), ↑(rationalHeight (a i)) ≤ self.Bσ) ∧ (∀ (i : Fin (self.dvOf (self.keyOf m) + self.zc.dim)), ↑(rationalHeight (b i)) ≤ self.Bσ) ∧ self.γOf m - self.γOf m' = ∑ i : Fin (self.dvOf (self.keyOf m) + self.zc.dim), ↑((a - b) i) * Fin.append (self.θvOf (self.keyOf m)) self.zc.θ i
Instances For
The physical wave of a mode (eq:modes).
Equations
Instances For
The slope ω_m(y) = 2λ_m (y - a_m) + γ_m of a mode.
Equations
Instances For
The modes alive on a cell U: their first-match cell contains U.
Equations
- Ms.alive U = {m : Ms.Md | TrilinearHT.Auto.dyadicGridCell Gd U.1 U.2 ⊆ TrilinearHT.Auto.dyadicGridCell Gd (Ms.cellOf m).1 (Ms.cellOf m).2}
Instances For
Blocks, goodness, side modes and side events of a frozen mode system (lines 1952-2047) #
The numerical data of the coherence argument: heights Hn, the mode-difference height D,
the gap threshold T, witness and kernel size sequences, the stability lag R, the shift Δ,
the top height J_* and the core fraction δ_*.
- Hn : ℕ
Number of height levels used by the coherence argument.
- D : ℕ
Rational-height bound for mode differences in the coherence argument.
- Tt : ℝ
Gap threshold used to separate coherent mode components.
Witness-size sequence indexed by height.
Kernel-size sequence indexed by height.
- R : ℕ
Stability lag used when comparing components at different heights.
- Δ : ℕ
Height shift between predecessor and current mode components.
- Jst : ℕ
Top height in the mode-coherence schedule.
- δs : ℝ
Core fraction retained by the side-event estimates.
Instances For
The frozen evaluation on a pre-cell as a mode synthesis (blueprint lines 1934-1937, 1959) #
The augmented mode of m on the cell J.
Equations
- Ms.cellMode J m = MeasureTheory.MemLp.toLp (TrilinearHT.Auto.augMode (TrilinearHT.Auto.dyadicGridCell Gd J.1 J.2) (Ms.wave m) (Ms.L.εM m) m) ⋯
Instances For
Frozen evaluations as lifted ball outputs (blueprint lines 1959, 2112-2116) #
The slot positions θ y_j = Q₀ (u + (j - l') v) in the torus variables x = (u, v),
u = ϑ y_{l'}, v = ϑ t, ϑ = θ / Q₀.
Equations
- TrilinearHT.Auto.torusW Q0 l' j x a = ↑Q0 * (x (Fin.castAdd d a) + (↑↑j - ↑↑l') * x (Fin.natAdd d a))
Instances For
One carry piece of the gauge multiplier: the shifted branch profiles of the four slots times the integer-carry character.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Blueprint eq:gauge-cancel (lines 1938-1944): the common progression multiplier, the carry
piece of the actual branch lattice points.
Equations
- TrilinearHT.Auto.gaugeMult δ Q0 l' C ρ x = TrilinearHT.Auto.gaugeTerm δ Q0 l' C ρ (TrilinearHT.Auto.gaugeFloor Q0 l' ρ x) x
Instances For
Near any point the multiplier is the sum of the carry pieces of the lattice tuples within one step of the local lattice points.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The slot position as a continuous linear map of the torus variables.
Equations
- TrilinearHT.Auto.torusWL Q0 l' j = ContinuousLinearMap.pi fun (a : Fin d) => ↑Q0 • (ContinuousLinearMap.proj (Fin.castAdd d a) + (↑↑j - ↑↑l') • ContinuousLinearMap.proj (Fin.natAdd d a))
Instances For
The carry phase of a lattice tuple as a continuous linear form of the torus variables.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The common progression multiplier is smooth: near every point it is a finite sum of smooth carry pieces, since the branch profiles vanish to infinite order at the cuts.
The carries of the lattice tuples in the local box are bounded by 18 when the offsets lie
in [0, 1].
The derivative constant of the branch profiles up to order m.
Equations
- TrilinearHT.Auto.profR δ m = TrilinearHT.Auto.bumpConst * (8 * (↑m + 1)) ^ 32 * (2 / δ)
Instances For
Blueprint lines 1942-1944 ("its Gevrey and absolute Fourier bounds are uniform in offsets"):
for offsets in [0, 1] and |C_{ab}| ≤ C_m, the derivatives of the multiplier obey
‖D^m M‖ ≤ 3^{4d} (16 Q₀ d R + 2π · 8 d² C_m · 18 · 4 Q₀)^m everywhere.
Blueprint line 1942 ("for fixed carries the right side is an integer character on
(ϑ y_{l'}, ϑ t) ... because Q₀ clears C_z"): the multiplier is 1-periodic in the torus
variables.
Blueprint lines 1942-1944 and 2479 ("on all true cutoff supports the four gauge factors have
the bounded smooth periodic multiplier"), with the thin enlargement of ErrorReport 2026-10-12:
the four true cutoffs times the four gauge phases e(c_j p_{ρ_j}(y_j)) differ from the four true
cutoffs times the multiplier with cutoff parameter δ'' by at most 8 d δ'' R_δ.
The four gauge factors of a common chart tag at the progression points
y_j = x + j t are the four true cutoffs times the gauge phase of eq:gauge-cancel.
Primaries and first-match cells on the main columns (blueprint line 1888) #
The primaries of a role (slot l, outer ball of the group G at the ball level j) at the
cell I: the main columns available to the maximal pad P and the rank L + j of the outer ball
(blueprint line 1888).
Equations
Instances For
The labels of every individual ball projection of the role are primaries.
The primaries are nested in depth (blueprint line 1888: "the mode lists, including primaries whose coefficients are zero, are nested"; a primary keeps its role on every descendant).
The first-match cells of a primary among a family cs of active cells: the maximal cells of
cs at which it is a primary (blueprint line 1888: "at its first match on I₀").
Equations
- fp.firstCells cs l s G j d v = TrilinearHT.Auto.maxCells A.G ({I ∈ cs | v ∈ fp.primaries l s G j d I})
Instances For
A primary at a cell of the family has a first-match cell containing the cell.
The first-match cell of a primary above a cell is unique.
A primary is a primary on every active descendant of its first-match cell (blueprint line 1888: "keep its modes and labels on every descendant").
The first-match expansion on the main columns (blueprint lines 1888, 1903-1910) #
A walk of length n in the tag graph of the original basic columns collapses to a path of at
most n tag edges between the endpoint tags (equal-tag steps are removed).
Blueprint lem:graph, short paths, for the original basic columns: two vertices at tag-graph
distance at most n carry equal tags or tags joined by an edge of height
exp(10⁵ ((n+1)(d+1))⁸ log(2 H_ed)), given tag dimensions at most d and matrix heights at most
H_ed.
The graph radius of a ball mask around its center.
Instances For
The edge height of the ball radius n in the tag graph.
Instances For
Blueprint line 1903 (first match, short-path part of lem:graph): a vertex of the ball mask of
a group at an active cell carries a tag joined to the tag of the group center by an edge at the
cell length, of height ballEdgeH of the ball radius.
An available main label is, on the cell, a pure chart of its tag in the slot, of the common source complexity (blueprint line 1798: pure main columns; line 1903: the primary at first match).
Blueprint first-match (lines 1903-1916, eq:firstmatch, eq:mode-differences) on the main
columns: a primary v of the role (slot l, outer ball of the group G at the level j) at an
active cell I is, on the cell, a pure chart Φ of its tag (an original column occurrence or a
template), and on the window |t| ≤ R |I| at the left end a_I of the cell, the product chart
P of Φ with the branch chart of the group center (cutoff of width δ, demodulation
e(-c_l p_ρ)) has an exact absolutely convergent mode expansion
φ_P(a_I + t) = Σ a_ℓ e(λ_* t² + (β + σ_ℓ·θ) t) with one common curvature, rational frequency
differences, and counts, heights and coefficient sums at most exp(D X^D),
X = 1 + log T(H⁶) + log(3B) (T the translation budget, B the edge height of the ball
radius at the maximal pad).
Blueprint eq:firstmatch (lines 1903-1910) on the main columns: at an active cell where v
is a primary of the role, finitely many modes e(λ (y - a_I)² + γ_k (y - a_I)), with one
curvature and frequencies γ_k = β + σ_k·Θ (σ_k rational, Θ = (θ_v, θ_z)), approximate
φ_v ζ^ρ e(-c_l p_ρ) within δ_c on the whole cell, with coefficient sum and |λ| |I|² at most
exp(D X^D); the count and the heights are bounded as in eq:mode-differences.
The main-column lift with local mode weights (blueprint line 1932) #
At every point, the primaries matched there (those with a first-match cell containing the
point) are primaries at the deepest such cell; hence they number at most the main labels there
(blueprint line 1932: the physical correction runs over the primaries matched at y).