Signed refined-quad bridge to the paper Step 4(B) composition factor

The proved CountableCentralRoutedMomentDecomposition is tied to the full deterministicMomentPairingSum; it cannot be specialized to one R324RefinedScheduleIndex without a new exact representation theorem. Moreover its existing concrete producers estimate a positive sum of configuration weights, whereas the refined bracket must retain the complete signed fibre sum.

This module therefore records the deepest cancellation-preserving bridge. For one refined fibre, R324RefinedQuadSignedCompositionData attaches the frequency increments of one operator composition directly to the complete signed r324BetaQuadHarvest. There is no entity-wise norm and no route-mass sum. The paper's Step 4(B) pigeonhole then gives the ε^2-scale bracket.

The scale is important: Step 4(B) proves eighthOrderFrequencyDecay (ε^2 * ‖freq (α+β)‖). It does not imply the stronger ε-scale bracket required by R324HdetBracketLedgerBound. The output here is consequently a separate paper-scale interface; no false adapter to the Hdet ledger is provided.

A composition attached to the complete signed quad harvest

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

One paper Step 4(B) composition for a complete signed refined-fibre quadruple harvest. The final field is deliberately a bound on the entire harvest for every factor of the composition. Thus cancellation inside the refined fibre has already occurred before the norm is taken.

• incrementCount : ℕ
• increment : Fin self.incrementCount → EuclideanSpace ℝ (Fin dim)
• incrementCount_pos : 0 < self.incrementCount
• incrementCount_le_trunc : self.incrementCount ≤ truncOrder ε
• increment_sum : ∑ i : Fin self.incrementCount, self.increment i = z4EuclideanFrequency (α + β)
• harvest_le_increment_decay (i : Fin self.incrementCount) : ‖r324BetaQuadHarvest ρ ε m α β hm (momentRefinedContractionFiber m ↑p.fst ↑p.snd)‖ ≤ amplitude * eighthOrderFrequencyDecay ‖self.increment i‖

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

The Step 4(B) pigeonhole, replayed on one complete signed quad harvest. No summation of positive route weights occurs: the sole estimated value is the full r324BetaQuadHarvest.

The exact projected-factor residue

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

Pre-decay representation of the same signed composition. Each factor is an actual Fourier argument of the cutoff, the factor frequencies conserve α+β, and removing any one cutoff factor leaves a common signed amplitude bound on the whole refined quad harvest.

No theorem in the current repository constructs this structure from r324BetaQuadHarvest; that missing representation equality/inequality is the precise gap between the physical signed harvest and the already-proved Schwartz decay of the projected symbol.

• factorCount : ℕ
• factorArgument : Fin self.factorCount → R4
• factorCount_pos : 0 < self.factorCount
• factorCount_le_trunc : self.factorCount ≤ truncOrder ε
• factorFrequency_sum : ∑ i : Fin self.factorCount, SmoothCutoff.euclideanFrequency (self.factorArgument i) = z4EuclideanFrequency (α + β)
• harvest_le_factorSymbol (i : Fin self.factorCount) : ‖r324BetaQuadHarvest ρ ε m α β hm (momentRefinedContractionFiber m ↑p.fst ↑p.snd)‖ ≤ amplitude * ‖fourierR4 ρ.toFun (self.factorArgument i)‖

theorem Anderson4D.R324RefinedQuadProjectedCompositionData.toSignedComposition {ρ : SmoothCutoff} {ε amplitude : ℝ} {m : ℕ} {α β : Z4} {hm : 0 < m} {p : R324RefinedScheduleIndex m} (d : R324RefinedQuadProjectedCompositionData ρ ε m α β hm p amplitude) (hA : 0 ≤ amplitude) : ∃ (C : ℝ), 0 < C ∧ Nonempty (R324RefinedQuadSignedCompositionData ρ ε m α β hm p (amplitude * C))

The cutoff's unconditional Schwartz bound converts a genuine projected factor representation into the post-projection signed composition data. The cutoff constant is fixed before all scale, order and mode parameters.

theorem Anderson4D.R324RefinedQuadProjectedCompositionData.exists_harvest_le_paperScale {ρ : SmoothCutoff} {ε amplitude : ℝ} {m : ℕ} {α β : Z4} {hm : 0 < m} {p : R324RefinedScheduleIndex m} (d : R324RefinedQuadProjectedCompositionData ρ ε 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 genuine projected-factor representation therefore yields the paper ε²-scale decay of the whole signed quad harvest.

Uniform paper-scale interfaces

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

The sole post-projection producer obligation, uniformly on the capped range. It is a composition statement about the complete signed refined fibre, not a positive route-mass budget.

Equations

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

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

Paper-scale quadruple-harvest ledger. This differs intentionally from R324RefinedPostCollapseQuadHarvestBound: its central bracket is at ε², the scale actually produced by paper Step 4(B).

Equations

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

theorem Anderson4D.R324RefinedQuadSignedCompositionBound.toPaperQuadHarvest {ρ : SmoothCutoff} {K : ℝ} (hK : 0 ≤ K) (h : R324RefinedQuadSignedCompositionBound ρ K) : R324RefinedPostCollapsePaperQuadHarvestBound ρ K

The signed composition producer closes the paper-scale quadruple ledger by the Step 4(B) pigeonhole.

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

Physical refined-fibre form of the paper-scale bracket.

Equations

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

theorem Anderson4D.R324RefinedPostCollapsePaperQuadHarvestBound.toPaperBracket {ρ : SmoothCutoff} {K : ℝ} (h : R324RefinedPostCollapsePaperQuadHarvestBound ρ K) : R324RefinedPostCollapsePaperBracketBound ρ K

Exact external endpoint harvesting turns the paper-scale quadruple ledger into the corresponding physical refined-fibre ledger.