Norm factorization on one selected R-324 physical cell

Before estimating a cell integral, its Fourier coefficient ledger can be separated exactly from the two deterministic Green skeletons. The selected high coefficient is then split from all unselected coefficients.

This file proves those equalities and the resulting norm-of-integral bound on the genuine physical cell fibre. That last inequality takes a norm before integrating the four endpoint phases, so it is only a uniform-branch ledger: it must not be used for the decaying branch of (3.24), where the endpoint-first route in R324SelectedCellEndpointFactorization is mandatory. No singular Green estimate, cell-volume bound, tree-incidence denominator, or automorphism factor is assumed or hidden here.

The selected coefficient ledger

noncomputable def Anderson4D.SmoothCutoff.r324SelectedUnselectedConfigurationWeight (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (q : R324CombinedFourierConfiguration κp κm π) (selected : R324ResidualCovarianceSlot κp) : ℝ

Product of the absolute Fourier coefficients away from the selected cross slot.

Equations

• ρ.r324SelectedUnselectedConfigurationWeight ε κp κm π q selected = ∏ j ∈ Finset.univ.erase (Anderson4D.SmoothCutoff.r324CrossSlotPairIndex κp κm π selected), ‖ρ.covarianceModeCoeff ε (q j)‖

theorem Anderson4D.SmoothCutoff.r324SelectedUnselectedConfigurationWeight_nonneg (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (q : R324CombinedFourierConfiguration κp κm π) (selected : R324ResidualCovarianceSlot κp) : 0 ≤ ρ.r324SelectedUnselectedConfigurationWeight ε κp κm π q selected

theorem Anderson4D.SmoothCutoff.r324CovarianceConfigurationWeight_eq_selected_mul_unselected (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (q : R324CombinedFourierConfiguration κp κm π) (selected : R324ResidualCovarianceSlot κp) : ρ.r324CovarianceConfigurationWeight ε (momentCombinedPairing κp κm π) q = ‖ρ.covarianceModeCoeff ε (q (r324CrossSlotPairIndex κp κm π selected))‖ * ρ.r324SelectedUnselectedConfigurationWeight ε κp κm π q selected

Exact extraction of the canonical selected coefficient from the complete configuration weight.

The genuine skeleton cell mass

noncomputable def Anderson4D.SmoothCutoff.r324SelectedSkeletonNormDensity {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (p : R324PhysicalPoint m) : ℝ

Nonnegative two-skeleton density after discarding the unit Fourier phase and all configuration coefficients.

Equations

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

theorem Anderson4D.SmoothCutoff.r324SelectedSkeletonNormDensity_nonneg {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (p : R324PhysicalPoint m) : 0 ≤ r324SelectedSkeletonNormDensity κp κm π p

noncomputable def Anderson4D.SmoothCutoff.r324SelectedSkeletonCellMass {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (ε : ℝ) (hε : 0 < ε) (cell : Fin (2 * m) → Z4) : ℝ

Integral of the bare two-skeleton norm on one genuine selected physical cell.

Equations

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

theorem Anderson4D.SmoothCutoff.r324SelectedSkeletonCellMass_nonneg {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (ε : ℝ) (hε : 0 < ε) (cell : Fin (2 * m) → Z4) : 0 ≤ r324SelectedSkeletonCellMass κp κm π selected ε hε cell

Exact cellwise factorization

theorem Anderson4D.SmoothCutoff.norm_r324SelectedHighFullPairingFourierIntegrand_eq_weight_mul_skeleton (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (ω : ρ.R324NonzeroCombinedFourierConfiguration ε α β κp κm π) (p : R324PhysicalPoint m) : ‖r324Flatten (ρ.r324SelectedHighFullPairingFourierIntegrand ε α β κp κm π hexternal hε hε1 hmtrunc ω) p‖ = ρ.r324CovarianceConfigurationWeight ε (momentCombinedPairing κp κm π) ↑ω * r324SelectedSkeletonNormDensity κp κm π p

Pointwise norm of the selected physical integrand is the constant configuration weight times the bare two-skeleton density.

theorem Anderson4D.SmoothCutoff.integral_norm_r324SelectedHighFullPairingFourierIntegrand_on_cell (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (ω : ρ.R324NonzeroCombinedFourierConfiguration ε α β κp κm π) (cell : Fin (2 * m) → Z4) : ∫ (p : R324PhysicalPoint m) in (r324SelectedPhysicalOpenEdgeCells κp κm π (ρ.r324FirstLargeCrossSlotForNonzeroConfiguration ε α β κp κm π hexternal hε hε1 hmtrunc ω) ε hε).index ⁻¹' {cell}, ‖r324Flatten (ρ.r324SelectedHighFullPairingFourierIntegrand ε α β κp κm π hexternal hε hε1 hmtrunc ω) p‖ ∂r324PhysicalMeasure m = ρ.r324CovarianceConfigurationWeight ε (momentCombinedPairing κp κm π) ↑ω * r324SelectedSkeletonCellMass κp κm π (ρ.r324FirstLargeCrossSlotForNonzeroConfiguration ε α β κp κm π hexternal hε hε1 hmtrunc ω) ε hε cell

Exact integral of the pointwise norm on one genuine selected cell.

theorem Anderson4D.SmoothCutoff.norm_integral_r324SelectedHighFullPairingFourierIntegrand_on_cell_le (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (ω : ρ.R324NonzeroCombinedFourierConfiguration ε α β κp κm π) (cell : Fin (2 * m) → Z4) : ‖∫ (p : R324PhysicalPoint m) in (r324SelectedPhysicalOpenEdgeCells κp κm π (ρ.r324FirstLargeCrossSlotForNonzeroConfiguration ε α β κp κm π hexternal hε hε1 hmtrunc ω) ε hε).index ⁻¹' {cell}, r324Flatten (ρ.r324SelectedHighFullPairingFourierIntegrand ε α β κp κm π hexternal hε hε1 hmtrunc ω) p ∂r324PhysicalMeasure m‖ ≤ ‖ρ.covarianceModeCoeff ε (↑ω (r324CrossSlotPairIndex κp κm π (ρ.r324FirstLargeCrossSlotForNonzeroConfiguration ε α β κp κm π hexternal hε hε1 hmtrunc ω)))‖ * ρ.r324SelectedUnselectedConfigurationWeight ε κp κm π (↑ω) (ρ.r324FirstLargeCrossSlotForNonzeroConfiguration ε α β κp κm π hexternal hε hε1 hmtrunc ω) * r324SelectedSkeletonCellMass κp κm π (ρ.r324FirstLargeCrossSlotForNonzeroConfiguration ε α β κp κm π hexternal hε hε1 hmtrunc ω) ε hε cell

The norm of one genuine selected cell integral is bounded by the selected coefficient, the remaining coefficient ledger, and the exact bare skeleton cell mass.