Clause B as a Fourier coefficient of the real flat core

R324CappedBracketDensityLedger (clause B of R324CappedCrossLedgerStrong) asks for a bound on

‖∑_{e ∈ F} deterministicMomentContractionTerm ρ ε m α β e‖

that is graded by the external modes α, β. By r324CMFlatDensity_modes_indep this can never come from a modulus estimate: the four external characters are unimodular and entity independent. This file makes the only possible mechanism explicit.

The core

Every deterministicMomentIntegrand is charT4 α x * charT4 β y * charT4 (-α) z * charT4 (-β) w times a real number, and that real number does not depend on α, β. Summing over the entity set F gives one real function on the physical product space, the flat core r324CMFlatCore. Two exact identities follow:

• r324CMFlatDensity_eq_abs_core — the clause-A carrier is |core|;
• r324CM_sum_term_eq_core_fourier — the clause-B left-hand side is the modulus of one Fourier coefficient of the core, taken at the frozen four-fold external mode (α, β, -α, -β).

So clause A is the L¹ norm of the core and clause B is the decay of its external Fourier coefficients: exactly the paper's §4.2 mechanism ((4.16)–(4.20)), where the decay is produced by integrating the external coordinates x, y, z, w against their characters before any norm is taken.

Removing ε from the weight

r324CMBracketWeight ε α β = ε⁻⁸ ⟨α⟩⁻⁴⟨β⟩⁻⁴⟨ε‖α+β‖⟩⁻⁸ still carries the endpoint loss ε⁻⁸. For 0 < ε ≤ 1 that loss exactly absorbs the rescaling of the central bracket, so the ε-free weight r324BracketPaperWeight α β = ⟨α⟩⁻⁴⟨β⟩⁻⁴⟨‖α+β‖⟩⁻⁸ is smaller (r324BracketPaperWeight_le_cmBracketWeight). Clause B therefore follows from the sharper ε-free ledger R324BracketPaperLedger, which is what the harvest of the four endpoint characters produces.

The ε-free bracket weight

noncomputable def Anderson4D.r324BracketPaperWeight (α β : Z4) : ℝ

The ε-free paper weight ⟨α⟩⁻⁴ ⟨β⟩⁻⁴ ⟨‖α+β‖⟩⁻⁸: the two endpoint fourth-order mode decays produced by the four external Green integrations, times the central eighth-order bracket at the conserved mode α + β, with no ε rescaling anywhere.

Equations

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

theorem Anderson4D.r324BracketPaperWeight_nonneg (α β : Z4) : 0 ≤ r324BracketPaperWeight α β

theorem Anderson4D.r324BracketPaperWeight_le_cmBracketWeight {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (α β : Z4) : r324BracketPaperWeight α β ≤ r324CMBracketWeight ε α β

The ε-free weight is the smaller one. On 0 < ε ≤ 1 the endpoint loss ε⁻⁸ ≥ 1 and the central bracket only improves when the frequency is rescaled by ε ≤ 1, so the ε-free paper weight is dominated by r324CMBracketWeight. Consequently a bound against the ε-free weight is stronger than clause B.

The real flat core

noncomputable def Anderson4D.r324CMFlatCore (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (F : Finset (MomentContraction m)) (p : R324PhysicalPoint m) : ℝ

The real flat core. The entity-summed deterministic integrand with the four external characters stripped: a real function on the physical product space, independent of α and β. Clause A is its L¹ norm; clause B is the decay of its external Fourier coefficients.

Equations

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

noncomputable def Anderson4D.r324ExternalChar (m : ℕ) (α β : Z4) (p : R324PhysicalPoint m) : ℂ

The four frozen external characters of (4.18) at the modes (α, β, -α, -β), as a function on the physical product space.

Equations

• Anderson4D.r324ExternalChar m α β p = Anderson4D.charT4 α p.1 * Anderson4D.charT4 β p.2.1 * Anderson4D.charT4 (-α) p.2.2.1 * Anderson4D.charT4 (-β) p.2.2.2.1

theorem Anderson4D.norm_r324ExternalChar (m : ℕ) (α β : Z4) (p : R324PhysicalPoint m) : ‖r324ExternalChar m α β p‖ = 1

theorem Anderson4D.r324CM_sum_flatten_eq_char_mul_core (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (α β : Z4) (F : Finset (MomentContraction m)) (p : R324PhysicalPoint m) : ∑ e ∈ F, r324Flatten (deterministicMomentIntegrand ρ ε m α β e.fst e.snd.fst e.snd.snd) p = r324ExternalChar m α β p * ↑(r324CMFlatCore ρ ε m F p)

Character/core factorization of the summed flat integrand. The external characters are entity independent, so they factor out of the entity sum, leaving the real core.

theorem Anderson4D.r324CMFlatDensity_eq_abs_core (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (α β : Z4) (F : Finset (MomentContraction m)) (p : R324PhysicalPoint m) : r324CMFlatDensity ρ ε m α β F p = |r324CMFlatCore ρ ε m F p|

Clause A's carrier is the modulus of the core.

theorem Anderson4D.r324CM_sum_term_eq_core_fourier (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) {m : ℕ} (α β : Z4) (F : Finset (MomentContraction m)) : ∑ e ∈ F, deterministicMomentContractionTerm ρ ε m α β e = ∫ (p : R324PhysicalPoint m), r324ExternalChar m α β p * ↑(r324CMFlatCore ρ ε m F p) ∂r324PhysicalMeasure m

Clause B's left-hand side is one Fourier coefficient of the core. The four external coordinates are integrated against their characters before any norm is taken; this is the sole source of the mode grading.

The ε-free ledger and clause B

def Anderson4D.R324BracketPaperLedger (ρ : SmoothCutoff) (K : ℝ) : Prop

The ε-free bracket ledger. The same shape as clause B but against the sharper weight r324BracketPaperWeight: the two endpoint fourth-order mode decays and the central eighth-order bracket at the conserved mode α + β, with no ε⁻⁸ endpoint loss and no ε rescaling of the bracket. This is what the endpoint harvest of the four external characters produces.

Equations

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

theorem Anderson4D.R324CappedBracketDensityLedger_of_paperLedger {ρ : SmoothCutoff} {K : ℝ} (hK : 0 ≤ K) (h : R324BracketPaperLedger ρ K) : R324CappedBracketDensityLedger ρ K

Clause B from the ε-free ledger.