The minimal signed-harvest input for the refined R-324 bracket

The four external integrations are already exact identities in r324Beta_sum_eq_endpointDecays_mul_quadHarvest. Consequently the refined post-collapse bracket reduces directly to a bound on r324BetaQuadHarvest for the realized refined fibre.

This is the last cancellation-preserving carrier before an analytic estimate: the entity sum remains inside r324BetaQuadCore, the two transported character differences remain inside the physical integral, and the norm is taken only after that complete signed integral. In particular, the interface below contains neither a raw-route positive mass nor a norm inside a covariance-key sum.

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

Minimal refined signed-harvest bracket input. On each realized residual-refined fibre, the complete quadruple harvest carries the natural ε-scaled central bracket. The factor ε⁻⁸ is not an estimate here: the exact external endpoint factorization later combines it with ⟨α⟩⁻⁴⟨β⟩⁻⁴ to give r324EndpointLoss.

The order cap is part of the statement, and the norm is outside the full physical integral defining r324BetaQuadHarvest.

Equations

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

theorem Anderson4D.R324RefinedPostCollapseQuadHarvestBound.toPostCollapseBracket {ρ : SmoothCutoff} {K : ℝ} (h : R324RefinedPostCollapseQuadHarvestBound ρ K) : R324RefinedPostCollapseBracketBound ρ K

The signed quadruple-harvest input implies the physical refined-fibre bracket. Both transitions used here are exact:

• r324RefinedPhysicalIntegral_eq_sum_contractionTerms identifies the refined physical integral with its finite contraction fibre;
• r324Beta_sum_eq_endpointDecays_mul_quadHarvest performs all four external integrations before any norm is taken.

Thus the proof loses no cancellation and merely regroups the endpoint factors into r324EndpointLoss.

theorem Anderson4D.R324RefinedPostCollapseQuadHarvestBound.toHdetBracketLedger {ρ : SmoothCutoff} {K : ℝ} (h : R324RefinedPostCollapseQuadHarvestBound ρ K) : R324HdetBracketLedgerBound ρ K

Direct capstone adapter from the minimal signed harvest to the Hdet ledger.

theorem Anderson4D.R324ScaledQuadBracketLedger.toRefinedPostCollapseQuadHarvest {ρ : SmoothCutoff} {K : ℝ} (hK : 0 ≤ K) (h : R324ScaledQuadBracketLedger ρ K) : R324RefinedPostCollapseQuadHarvestBound ρ K

The existing arbitrary-finite-set scaled quadruple ledger specializes to the minimal refined signed-harvest input. The Hdet allowance m⁸ is free on the range m ≥ 2; no phase-free density clause is introduced.