The actual lattice-mode producer boundary for the refined quad composition

The physical projected-covariance machinery does not expose a bare fourierR4 ρ ξ whose Euclidean frequency also sums to the external lattice frequency. Its exact factor is instead

covarianceModeCoeff ε k = whiteNoiseFourierScale^2 * ‖symbol ε k‖^2,

with unscaled lattice modes k : Z4 satisfying frequency conservation. The symbol itself is evaluated at the scaled argument ε k. Therefore the earlier abstract R324RefinedQuadProjectedCompositionData, which asks its fourierR4 arguments both to be the actual cutoff arguments and to have unscaled conserved Euclidean frequencies, is not constructible from the physical Fourier expansion without an additional false scaling equality.

This module records the correct producer boundary:

• an exact, integration-level removal of one marked covariance coefficient, retaining the complete signed open-edge physical amplitude;
• a lattice-mode composition interface for the complete signed refined quad harvest; and
• the paper Step 4(B) payoff from that interface.

No entity-wise norm and no sum of positive route masses is used.

Exact removal of the selected covariance coefficient

noncomputable def Anderson4D.SmoothCutoff.r324MarkedResidualPhysicalOpenCovarianceIntegrand (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (phase : (Fin (2 * m) → T4) → ℂ) (k : Z4) (v : Fin (2 * m) → T4) : ℂ

The signed physical integrand left after removing the sole marked covariance Fourier coefficient. Every unselected covariance remains inside r324MarkedResidualPhysicalOpenEdgeAmplitude.

Equations

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

theorem Anderson4D.SmoothCutoff.r324MarkedResidualPhysicalModeTerm_mul_phase_eq_coeff_mul_open (ρ : SmoothCutoff) {m : ℕ} (ε L : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (phase : (Fin (2 * m) → T4) → ℂ) (k : Z4) (hk : k ∈ r324HighModeSet ε L) (v : Fin (2 * m) → T4) : phase v * ρ.r324MarkedResidualPhysicalInteriorModeTerm ε L κp κm π selected v k = ρ.covarianceModeCoeff ε k * ρ.r324MarkedResidualPhysicalOpenCovarianceIntegrand ε κp κm π selected phase k v

Pointwise exact factor removal on a retained high mode.

theorem Anderson4D.SmoothCutoff.integral_phase_mul_r324MarkedResidualPhysicalModeTerm_eq (ρ : SmoothCutoff) {m : ℕ} (ε L : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (phase : (Fin (2 * m) → T4) → ℂ) (k : Z4) (hk : k ∈ r324HighModeSet ε L) : (∫ (v : Fin (2 * m) → T4), phase v * ρ.r324MarkedResidualPhysicalInteriorModeTerm ε L κp κm π selected v k ∂MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure) = ρ.covarianceModeCoeff ε k * ∫ (v : Fin (2 * m) → T4), ρ.r324MarkedResidualPhysicalOpenCovarianceIntegrand ε κp κm π selected phase k v ∂MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure

Integral-level exact factor removal. The norm is still absent: the complete signed physical integral is factored before any estimate.

Correct lattice-mode composition data

structure Anderson4D.R324RefinedQuadCovarianceCompositionData (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (α β : Z4) (hm : 0 < m) (p : R324RefinedScheduleIndex m) (amplitude : ℝ) : Type

The post-factor-removal inequality for one complete signed refined quad harvest. Frequencies are the actual unscaled lattice modes from the covariance expansion.

• factorCount : ℕ
• factorMode : Fin self.factorCount → Z4
• factorCount_pos : 0 < self.factorCount
• factorCount_le_trunc : self.factorCount ≤ truncOrder ε
• factorFrequency_sum : ∑ i : Fin self.factorCount, z4EuclideanFrequency (self.factorMode i) = z4EuclideanFrequency (α + β)
• harvest_le_covarianceFactor (i : Fin self.factorCount) : ‖r324BetaQuadHarvest ρ ε m α β hm (momentRefinedContractionFiber m ↑p.fst ↑p.snd)‖ ≤ amplitude * ‖ρ.covarianceModeCoeff ε (self.factorMode i)‖

theorem Anderson4D.R324RefinedQuadCovarianceCompositionData.actualSymbolFrequency_sum {ρ : SmoothCutoff} {ε amplitude : ℝ} {m : ℕ} {α β : Z4} {hm : 0 < m} {p : R324RefinedScheduleIndex m} (d : R324RefinedQuadCovarianceCompositionData ρ ε m α β hm p amplitude) : (∑ i : Fin d.factorCount, SmoothCutoff.euclideanFrequency fun (j : Fin dim) => ε * ↑(d.factorMode i j)) = (ε / (2 * Real.pi)) • z4EuclideanFrequency (α + β)

The exact frequency sum of the actual cutoff arguments. It is the scaled external frequency, not the unscaled frequency required by R324RefinedQuadProjectedCompositionData.factorFrequency_sum. This is the precise normalization obstruction to constructing the abstract structure from lattice covariance modes.

structure Anderson4D.R324RefinedQuadCovarianceFactorization (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (α β : Z4) (hm : 0 < m) (p : R324RefinedScheduleIndex m) (amplitude : ℝ) : Type

Exact factorization form of the remaining algebraic obligation. For each composition factor the complete signed refined quad harvest must equal that covariance coefficient times a complete signed open-factor amplitude. This equality, after the already-proved physical single-edge identity above is reassembled over the refined fibre, is the one missing algebraic bridge in the repository.

• factorCount : ℕ
• factorMode : Fin self.factorCount → Z4
• factorCount_pos : 0 < self.factorCount
• factorCount_le_trunc : self.factorCount ≤ truncOrder ε
• factorFrequency_sum : ∑ i : Fin self.factorCount, z4EuclideanFrequency (self.factorMode i) = z4EuclideanFrequency (α + β)
• openAmplitude : Fin self.factorCount → ℂ
• harvest_eq_covarianceFactor_mul_openAmplitude (i : Fin self.factorCount) : r324BetaQuadHarvest ρ ε m α β hm (momentRefinedContractionFiber m ↑p.fst ↑p.snd) = ρ.covarianceModeCoeff ε (self.factorMode i) * self.openAmplitude i
• norm_openAmplitude_le (i : Fin self.factorCount) : ‖self.openAmplitude i‖ ≤ amplitude

def Anderson4D.R324RefinedQuadCovarianceFactorization.toCompositionData {ρ : SmoothCutoff} {ε amplitude : ℝ} {m : ℕ} {α β : Z4} {hm : 0 < m} {p : R324RefinedScheduleIndex m} (d : R324RefinedQuadCovarianceFactorization ρ ε m α β hm p amplitude) : R324RefinedQuadCovarianceCompositionData ρ ε m α β hm p amplitude

Exact factorization implies the corresponding complete-signed-harvest inequality, without splitting the refined fibre.

Equations

• d.toCompositionData = { factorCount := d.factorCount, factorMode := d.factorMode, factorCount_pos := ⋯, factorCount_le_trunc := ⋯, factorFrequency_sum := ⋯, harvest_le_covarianceFactor := ⋯ }

Paper Step 4(B) from the actual covariance factor

theorem Anderson4D.R324RefinedQuadCovarianceCompositionData.exists_harvest_le_paperScale {ρ : SmoothCutoff} {ε amplitude : ℝ} {m : ℕ} {α β : Z4} {hm : 0 < m} {p : R324RefinedScheduleIndex m} (d : R324RefinedQuadCovarianceCompositionData ρ ε m α β hm p amplitude) (hε : 0 < ε) (hεsmall : ε ≤ 1 / 4) (hA : 0 ≤ amplitude) : ∃ (C : ℝ), 0 < C ∧ ‖r324BetaQuadHarvest ρ ε m α β hm (momentRefinedContractionFiber m ↑p.fst ↑p.snd)‖ ≤ amplitude * C * eighthOrderFrequencyDecay (ε ^ 2 * ‖z4EuclideanFrequency (α + β)‖)

A true lattice-mode composition produces the paper's ε² central bracket. The constant is cutoff-dependent only.

Uniform residual producer

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

The sole remaining producer in the actual lattice-mode representation. It asks for exact covariance-factor removal on the complete signed refined quad harvest, uniformly on the capped range.

Equations

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

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

Inequality form of the same actual lattice-mode producer.

Equations

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

theorem Anderson4D.R324RefinedQuadCovarianceFactorizationBound.toCompositionBound {ρ : SmoothCutoff} {K : ℝ} (h : R324RefinedQuadCovarianceFactorizationBound ρ K) : R324RefinedQuadCovarianceCompositionBound ρ K

Forgetting the exact equality leaves the covariance-composition inequality, still on the complete signed refined fibre.

theorem Anderson4D.R324RefinedQuadCovarianceCompositionBound.exists_paperQuadHarvest {ρ : SmoothCutoff} {K : ℝ} (hK : 0 ≤ K) (h : R324RefinedQuadCovarianceCompositionBound ρ K) : ∃ (K' : ℝ), 0 ≤ K' ∧ R324RefinedPostCollapsePaperQuadHarvestBound ρ K'

The true lattice composition closes the paper-scale refined quad ledger. The single cutoff-dependent covariance constant is absorbed into the geometric base.