Section 13.1: One expansion at first match

This file was automatically generated by Claude.

Formalization of blueprint Section 13, "Fixed modes, the linear side, and hereditary representatives" (sec:modes), subsection 1, "One expansion at first match" (lines 1884-1977) of blueprint/formalization_blueprint.tex.

First-match expansions (blueprint §13.1)

theorem TrilinearHT.Auto.split_height_budget {H B : ℝ} {d : ℕ} (hH : Real.exp 2 ≤ H) (hB : 2 ≤ B) (hd : ↑d ≤ Real.log H) : 4 * H ^ d ^ 2 * (B ^ d ^ 2) ^ 2 * (H + ↑d ^ 2 * ((1 + B) * H * B) + 1) ≤ Real.exp (11 * (1 + Real.log H + Real.log B) ^ 3)

The height of the effective phase matrix is quasipolynomial in H and B.

theorem TrilinearHT.Auto.splitPhase (c₀ : ℕ) (hc : 1 ≤ c₀) (R : ℝ) (hR : 0 ≤ R) : ∃ (D : ℕ), 1 ≤ D ∧ ∃ (DJ : ℕ → ℕ), ∀ {d : ℕ} (H B r : ℝ) (A : QuadraticChartData d), QuadraticChartComplexity c₀ H A → 0 < r → 2 ≤ B → (WeylSplitData B (fun (i : Fin d) (x : Fin 1) => r * A.horizontal i) A.matrix fun (x x_1 : Fin 1) => r ^ 2 * A.quadratic) → have X := 1 + Real.log H + Real.log B; ∃ (M : Matrix (Fin d) (Fin d) ℚ), (∀ (i j : Fin d), ↑(rationalHeight (M i j)) ≤ Real.exp (↑D * X ^ D)) ∧ |A.quadratic + ∑ i : Fin d, ∑ j : Fin d, A.horizontal i * ↑(M i j) * A.horizontal j| * r ^ 2 ≤ Real.exp (↑D * X ^ D) ∧ ∃ (ι : Type) (x : Fintype ι) (σ : ι × (Fin (d + d) → ℤ) → Fin d → ℚ), ↑(Fintype.card ι) ≤ Real.exp (↑D * X ^ D) ∧ (∀ (p : ι × (Fin (d + d) → ℤ)) (i : Fin d), ↑(rationalHeight (σ p i)) ≤ Real.exp (↑D * X ^ D) * (1 + frequencyLength p.2)) ∧ ∃ (a : ι × (Fin (d + d) → ℤ) → ℂ), (∀ (t : ℝ), |t| ≤ R * r → HasSum (fun (p : ι × (Fin (d + d) → ℤ)) => a p * ↑(Real.fourierChar ((∑ i : Fin d, ↑(σ p i) * A.horizontal i) * t))) (↑(Real.fourierChar (-((A.quadratic + ∑ i : Fin d, ∑ j : Fin d, A.horizontal i * ↑(M i j) * A.horizontal j) * t ^ 2 + A.linear * t))) * quadraticChartAtom A t)) ∧ (Summable fun (p : ι × (Fin (d + d) → ℤ)) => ‖a p‖) ∧ ∑' (p : ι × (Fin (d + d) → ℤ)), ‖a p‖ ≤ Real.exp (↑D * X ^ D) ∧ ∀ (J : ℕ), (∀ (p : ι × (Fin (d + d) → ℤ)), ‖a p‖ * (1 + frequencyLength p.2) ^ (J * (d + 1) ^ 2) ≤ Real.exp (↑(DJ J) * X ^ DJ J)) ∧ ∀ (T : ℝ), 1 ≤ T → (∑ f : ι, ∑ v ∈ frequencyShell (d + d) T, ‖a (f, v)‖) * T ^ (J * (d + 1) ^ 2) ≤ Real.exp (↑(DJ J) * X ^ DJ J)

lem:chartfourier at a given splitting (blueprint §13.1, line 1922): a one-variable chart whose scale-r data admit eq:weyl-splitting with sizes and heights at most B has, on the window |t| ≤ R r, an exact absolutely convergent expansion into modes e(λ_* t² + (β + σ_ℓ·θ) t) with one common curvature λ_* = λ + θᵀ M θ, |λ_*| r² ≤ D, and rational frequency differences σ_ℓ of height D(1+|ℓ|), everything quasipolynomial in H and B.

theorem TrilinearHT.Auto.WeylSplitData.smul {B : ℝ} {d : ℕ} {V : Matrix (Fin d) (Fin 1) ℝ} {C : Matrix (Fin d) (Fin d) ℚ} {Λ : Matrix (Fin 1) (Fin 1) ℝ} {c : ℤ} (hc : c ≠ 0) (h : WeylSplitData B V C Λ) : WeylSplitData (|↑c| * B) V (↑c • C) (↑c • Λ)

A splitting of the data (V, C, Λ) is a splitting of (V, cC, cΛ) at size |c| B.

noncomputable def TrilinearHT.Auto.branchLift {d : ℕ} (ρ u : Fin d → ℝ) : Fin d → ℝ

The branch lift d_ρ(u) = ρ + {u - ρ}, with values in ρ + [0,1)ᵈ.

Equations

• TrilinearHT.Auto.branchLift ρ u i = ρ i + Int.fract (u i - ρ i)

theorem TrilinearHT.Auto.branchChart_atom {d : ℕ} (θ : Fin d → ℝ) (C : Matrix (Fin d) (Fin d) ℚ) (lam : ℝ) (c : ℤ) (ρ : Fin d → ℝ) {g : (Fin d → ℝ) → ℂ} (hg : ContDiff ℝ (↑⊤) g) (hgc : HasCompactSupport g) (hgs : ∀ (w : Fin d → ℝ), g w ≠ 0 → ∀ (i : Fin d), ρ i < w i ∧ w i < ρ i + 1) (y : ℝ) : quadraticChartAtom (mkQuadraticChart θ (-↑c * lam) 0 (↑(-c) • C) g hg hgc) y = g (branchLift ρ fun (i : Fin d) => θ i * y) * ↑(Real.fourierChar (-↑c * (lam * y ^ 2 + chartMatrixPhase C (fun (i : Fin d) => θ i * y) (branchLift ρ fun (i : Fin d) => θ i * y))))

Blueprint lines 1906-1908: a cut-off branch of the group-center phase is a chart. If the amplitude g vanishes outside the open branch cube ρ + (0,1)ᵈ, the chart with horizontal θ, matrix -cC, quadratic -cλ and amplitude g has atom g(d_ρ) e(-c p_ρ) with p_ρ(y) = λ y² + (θ y)ᵀ C d_ρ(θ y).

noncomputable def TrilinearHT.Auto.branchChart (z : ChartTag) (c : ℤ) {g : (Fin z.dim → ℝ) → ℂ} (hg : ContDiff ℝ (↑⊤) g) (hgc : HasCompactSupport g) : QuadraticChartData z.dim

The cut-off branch chart of a group center z in slot multiplier c (blueprint lines 1906-1908).

Equations

• TrilinearHT.Auto.branchChart z c hg hgc = TrilinearHT.Auto.mkQuadraticChart z.θ (-↑c * z.lam) 0 (↑(-c) • z.C) g hg hgc

The pointwise lift to modes (blueprint lines 1932-1940)

noncomputable def TrilinearHT.Auto.modeLift {Pr : Type u_1} {Md : Type u_2} [Fintype Pr] (own : Md → Pr) (s : ℂ) (q : Pr → ℂ) (a : Md → ℂ) (εP : Pr → ℝ) (εM : Md → ℝ) (F : ColumnHilbert Pr) : ColumnHilbert Md

The pointwise lift at one point: physical output s F_phys + Σ_Φ F_Φ ε_Φ^{-1/2} q_Φ and mode coordinates √ε_m a_m F_{Φ(m)} ε_{Φ(m)}^{-1/2}, where s = (ζ^ρ)².

Equations

• One or more equations did not get rendered due to their size.

noncomputable def TrilinearHT.Auto.augmentedMode {Md : Type u_2} [DecidableEq Md] (ψphys : Md → ℂ) (εM : Md → ℝ) (m : Md) : ColumnHilbert Md

The augmented mode ψ_m = (ψ_m^phys, √ε_m e_m).

Equations

• TrilinearHT.Auto.augmentedMode ψphys εM m = WithLp.toLp 2 fun (o : Option Md) => match o with | none => ψphys m | some m' => if m' = m then ↑√(εM m) else 0

noncomputable def TrilinearHT.Auto.augmentedMain {Pr : Type u_1} [Fintype Pr] (φ : Pr → ℂ) (εP : Pr → ℝ) (β : Pr → ℂ) : ColumnHilbert Pr

The augmented main column (φ_Φ, √ε_Φ e_Φ) with coefficient vector β.

Equations

• TrilinearHT.Auto.augmentedMain φ εP β = WithLp.toLp 2 fun (o : Option Pr) => match o with | none => ∑ Φ : Pr, β Φ * φ Φ | some Φ => ↑√(εP Φ) * β Φ

theorem TrilinearHT.Auto.modeLift_synthesis {Pr : Type u_1} {Md : Type u_2} [Fintype Pr] [Fintype Md] [DecidableEq Pr] [DecidableEq Md] (own : Md → Pr) (s : ℂ) (φ : Pr → ℂ) (a ψphys : Md → ℂ) (εP : Pr → ℝ) (hεP : ∀ (Φ : Pr), 0 < εP Φ) (εM : Md → ℝ) (q : Pr → ℂ) (hq : ∀ (Φ : Pr), q Φ = ∑ m : Md with own m = Φ, a m * ψphys m - s * φ Φ) (β : Pr → ℂ) : modeLift own s q a εP εM (augmentedMain φ εP β) = ∑ m : Md, (β (own m) * a m) • augmentedMode ψphys εM m

Blueprint lines 1934-1937: the lift carries every main output exactly to its mode synthesis Σ_{Φ,m} β_Φ a_{Φ,m} ψ_m, provided q_Φ = Σ_m a_{Φ,m} ψ_m^phys - s φ_Φ.

theorem TrilinearHT.Auto.columnHilbert_norm_sq {V : Type u_3} [Fintype V] (x : ColumnHilbert V) : ‖x‖ ^ 2 = ‖x.ofLp none‖ ^ 2 + ∑ v : V, ‖x.ofLp (some v)‖ ^ 2

theorem TrilinearHT.Auto.modeLift_norm_sq_le' {Pr : Type u_1} {Md : Type u_2} [Fintype Pr] [Fintype Md] [DecidableEq Pr] (own : Md → Pr) {s : ℂ} (hs : ‖s‖ ≤ 1) (q : Pr → ℂ) (a : Md → ℂ) (εP : Pr → ℝ) (hεP : ∀ (Φ : Pr), 0 < εP Φ) (hqs : ∑ Φ : Pr, ‖q Φ‖ ^ 2 / εP Φ ≤ 1) (εM : Md → ℝ) (hεM : ∀ (m : Md), 0 ≤ εM m) (hw : ∀ (Φ : Pr), ∑ m : Md with own m = Φ, εM m * ‖a m‖ ^ 2 ≤ εP Φ) (F : ColumnHilbert Pr) : ‖modeLift own s q a εP εM F‖ ^ 2 ≤ 5 * ‖F‖ ^ 2

modeLift_norm_sq_le with the physical corrections weighted pointwise: the lift has the absolute norm bound ‖R F‖² ≤ 5 ‖F‖² when |s| ≤ 1, Σ_Φ |q_Φ|² / ε_Φ ≤ 1 and the mode weights satisfy Σ_{m ∈ Φ} ε_m |a_m|² ≤ ε_Φ (blueprint lines 1930-1932: only the primaries matched at the point carry a correction).

Offset averages of the branch cutoff (eq:offset-mean)

noncomputable def TrilinearHT.Auto.branchProfile (δ s : ℝ) : ℝ

The one-dimensional branch profile: one on [2δ, 1-2δ], zero outside [δ, 1-δ].

Equations

• TrilinearHT.Auto.branchProfile δ s = TrilinearHT.Auto.gevreyIntervalCutoff 0 (2 * δ) (1 - 2 * δ) 1 s

theorem TrilinearHT.Auto.branchProfile_mem (δ s : ℝ) : branchProfile δ s ∈ Set.Icc 0 1

theorem TrilinearHT.Auto.branchProfile_eq_one {δ s : ℝ} (hδ : 0 < δ) (hs : 2 * δ ≤ s) (hs' : s ≤ 1 - 2 * δ) : branchProfile δ s = 1

theorem TrilinearHT.Auto.branchProfile_continuous (δ : ℝ) : Continuous (branchProfile δ)

theorem TrilinearHT.Auto.integral_fract_shift (f : ℝ → ℝ) (u : ℝ) : ∫ (ρ : ℝ) in Set.Icc 0 1, f (Int.fract (u - ρ)) = ∫ (s : ℝ) in Set.Icc 0 1, f s

The offset average of a function of {u - ρ} over ρ ∈ [0,1] is its mean over [0,1].

noncomputable def TrilinearHT.Auto.offsetMeasure (d : ℕ) : MeasureTheory.Measure (Fin d → ℝ)

The uniform offset measure on [0,1]ᵈ.

Equations

• TrilinearHT.Auto.offsetMeasure d = MeasureTheory.Measure.pi fun (x : Fin d) => MeasureTheory.volume.restrict (Set.Icc 0 1)

instance TrilinearHT.Auto.offsetMeasure_prob (d : ℕ) : MeasureTheory.IsProbabilityMeasure (offsetMeasure d)

noncomputable def TrilinearHT.Auto.branchCutoffValue {d : ℕ} (δ : ℝ) (ρ u : Fin d → ℝ) : ℝ

The periodic branch cutoff ζ^ρ(u) = Π_i β({u_i - ρ_i}).

Equations

• TrilinearHT.Auto.branchCutoffValue δ ρ u = ∏ i : Fin d, TrilinearHT.Auto.branchProfile δ (Int.fract (u i - ρ i))

theorem TrilinearHT.Auto.branchCutoffValue_mem {d : ℕ} (δ : ℝ) (ρ u : Fin d → ℝ) : branchCutoffValue δ ρ u ∈ Set.Icc 0 1

theorem TrilinearHT.Auto.one_sub_prod_le_sum {ι : Type u_1} (s : Finset ι) (x : ι → ℝ) (h0 : ∀ i ∈ s, 0 ≤ x i) (h1 : ∀ i ∈ s, x i ≤ 1) : 1 - ∏ i ∈ s, x i ≤ ∑ i ∈ s, (1 - x i)

theorem TrilinearHT.Auto.profile_mean_bounds {δ : ℝ} (hδ : 0 < δ) (hδ' : δ ≤ 1 / 4) : 1 - 4 * δ ≤ ∫ (s : ℝ) in Set.Icc 0 1, branchProfile δ s ∧ ∫ (s : ℝ) in Set.Icc 0 1, 1 - branchProfile δ s ^ 2 ≤ 4 * δ

theorem TrilinearHT.Auto.offsetMean {d : ℕ} {δ : ℝ} (hδ : 0 < δ) (hdδ : 8 * ↑d * δ ≤ 1) (hδ' : δ ≤ 1 / 8) (u : Fin d → ℝ) : ∫ (ρ : Fin d → ℝ), branchCutoffValue δ ρ u ∂offsetMeasure d = (∫ (s : ℝ) in Set.Icc 0 1, branchProfile δ s) ^ d ∧ 1 / 2 ≤ (∫ (s : ℝ) in Set.Icc 0 1, branchProfile δ s) ^ d ∧ ∫ (ρ : Fin d → ℝ), (1 - branchCutoffValue δ ρ u ^ 2) ^ 2 ∂offsetMeasure d ≤ 4 * ↑d * δ

Blueprint eq:offset-mean (line 1908): translation invariance gives, pointwise in u, E_ρ ζ^ρ = c_ζ ≥ 1/2 (with c_ζ independent of u) and E_ρ |1 - (ζ^ρ)²|² ≤ 4 d δ, for 0 < δ and 8 d δ ≤ 1.

theorem TrilinearHT.Auto.branchProfile_eq_zero_near_cut {δ s : ℝ} (hδ : 0 < δ) (hs : s ≤ δ ∨ 1 - δ ≤ s) : branchProfile δ s = 0

The branch profile vanishes within δ of the cuts (blueprint line 1897: the cutoff vanishes within δ_c of each branch cut).

noncomputable def TrilinearHT.Auto.branchAmp {d : ℕ} (δ : ℝ) (ρ w : Fin d → ℝ) : ℂ

The branch amplitude w ↦ Π_i β(w_i - ρ_i), supported in the open branch cube.

Equations

• TrilinearHT.Auto.branchAmp δ ρ w = ∏ i : Fin d, ↑(TrilinearHT.Auto.branchProfile δ (w i - ρ i))

theorem TrilinearHT.Auto.branchAmp_smooth {d : ℕ} (δ : ℝ) (ρ : Fin d → ℝ) : ContDiff ℝ (↑⊤) (branchAmp δ ρ)

theorem TrilinearHT.Auto.branchAmp_support {d : ℕ} {δ : ℝ} (hδ : 0 < δ) (_hδ' : δ < 1 / 4) {ρ w : Fin d → ℝ} (hw : branchAmp δ ρ w ≠ 0) (i : Fin d) : ρ i < w i ∧ w i < ρ i + 1

theorem TrilinearHT.Auto.branchAmp_hasCompactSupport {d : ℕ} {δ : ℝ} (hδ : 0 < δ) (hδ' : δ < 1 / 4) (ρ : Fin d → ℝ) : HasCompactSupport (branchAmp δ ρ)

theorem TrilinearHT.Auto.branchAmp_branchLift {d : ℕ} (δ : ℝ) (ρ u : Fin d → ℝ) : branchAmp δ ρ (branchLift ρ u) = ↑(branchCutoffValue δ ρ u)

The common progression multiplier and the schedule (blueprint lines 1942-1976)

noncomputable def TrilinearHT.Auto.gaugeCarry {d : ℕ} (θ : Fin d → ℝ) (ρ : Fin 4 → Fin d → ℝ) (x t : ℝ) (j : Fin 4) : Fin d → ℝ

The carries k_j = d_j - (1-j) d_0 - j d_1 of four branch lifts d_j = d_{ρ_j}(θ y_j).

Equations

• One or more equations did not get rendered due to their size.

theorem TrilinearHT.Auto.gauge_cancel {d : ℕ} (θ : Fin d → ℝ) (C : Matrix (Fin d) (Fin d) ℚ) (lam : ℝ) (ρ : Fin 4 → Fin d → ℝ) (x t : ℝ) : ∑ j : Fin 4, ↑(slotCoeff j) * (lam * (x + ↑↑j * t) ^ 2 + chartMatrixPhase C (fun (a : Fin d) => θ a * (x + ↑↑j * t)) (branchLift (ρ j) fun (a : Fin d) => θ a * (x + ↑↑j * t))) = ∑ j : Fin 4, ↑(slotCoeff j) * chartMatrixPhase C (fun (a : Fin d) => θ a * (x + ↑↑j * t)) (gaugeCarry θ ρ x t j)

Blueprint eq:gauge-cancel (line 1942): with four offsets, the product of the demodulation phases e(c_j p_{ρ_j}(y_j)) of a group center over the four slots is the linear carry character e(Σ_j c_j (θ y_j)ᵀ C k_j), by the three identities Σ c_j j^u = 0.

structure TrilinearHT.Auto.ModeSchedule : Type

The parameters of blueprint eq:mode-parameters and eq:lags (lines 1950-1962).

• dmax : ℕ

  Maximum dimension of the tags entering the mode schedule.

• Dstar : ℝ

  Common complexity budget controlling the mode schedule.

• Bstar : ℝ

  Coefficient-size budget entering the mode schedule.

• Dm : ℝ

  Mode-count parameter used in the logarithmic height budget.

• Q0 : ℕ

  Denominator-clearing bound for the rational chart matrices.

• Cstar : ℝ

  Base complexity constant for the height schedule.

• Rht : ℕ

  Height lag exceeding the binary logarithm of the base complexity.

• Jstar : ℕ

  Top height of the mode schedule.

• A0 : ℝ

  Growth base for the height-dependent witness budgets.

• H : ℝ

  Rational-height cutoff used to define the mode graphs.

• T : ℝ

  Gap threshold separating the mode graphs.

• K : ℕ

  Dyadic block length dominating the packet width and the logarithmic gap budgets.

noncomputable def TrilinearHT.Auto.ModeSchedule.Lh (h : ℕ) : ℝ

L_h = 6^h.

Equations

• TrilinearHT.Auto.ModeSchedule.Lh h = 6 ^ h

noncomputable def TrilinearHT.Auto.ModeSchedule.Eh (S : ModeSchedule) (h : ℕ) : ℝ

E_h = A₀^{h+1}.

Equations

• S.Eh h = S.A0 ^ (h + 1)

noncomputable def TrilinearHT.Auto.ModeSchedule.Ξ (S : ModeSchedule) : ℝ

Ξ = D_*^{1000}.

Equations

• S.Ξ = S.Dstar ^ 1000

structure TrilinearHT.Auto.ModeSchedule.Valid (S : ModeSchedule) (Cj CA CT CK : ℕ) (δs W : ℝ) : Prop

The defining inequalities of eq:mode-parameters, with absolute constants Cj, CA, CT, CK, a small absolute δ_* and the packet width W of lem:height at height H.

• Cstar_ge : (10 * ↑S.dmax * S.Dstar) ^ (100 * S.dmax ^ 4) ≤ S.Cstar
• Rht_ge : Real.logb 2 S.Cstar + 30 ≤ ↑S.Rht
• Jstar_ge : ↑Cj * δs⁻¹ ^ 2 * ↑S.dmax * ↑S.Rht * Real.log (2 * S.Dm) ≤ ↑S.Jstar
• A0_ge : (S.Cstar * 6 ^ S.Rht * S.Bstar * S.Dstar) ^ CA ≤ S.A0
• H_gt : (↑S.dmax * S.Cstar * S.Eh S.Jstar * S.Bstar * Lh S.Jstar * ↑S.Q0 * S.Ξ) ^ 10 < S.H
• T_gt : (↑S.dmax * S.H) ^ (CT * S.dmax ^ 4) * S.Ξ < S.T
• K_dyadic : ∃ (κ : ℕ), S.K = 2 ^ κ
• K_ge : W + 2 * Real.logb 2 S.T + ↑CK * Real.logb 2 S.Dstar ≤ ↑S.K

theorem TrilinearHT.Auto.logb_two_le_two_log {x : ℝ} (hx : 1 ≤ x) : Real.logb 2 x ≤ 2 * Real.log x