Collapsing the three capped residual Props to one

R324CappedRebaseAssembly.mainConditional_of_analyticResiduals_capped consumes three analytic obligations: R324CappedCrossLedger, R324CappedMixedLedger and R324CappedBracketLedger. This file replaces all three by a single ledger R324CappedCrossLedgerStrong stated at the level of the physical density on arbitrary finite sets of order-m contraction entities, and proves the three reductions and the resulting single-obligation conditional main theorem.

The carrier

r324CMFlatDensity ρ ε m α β F p = ‖∑_{e ∈ F} flatten(integrand e) p‖ — the pointwise norm of the summed flattened contraction integrand. Two proved facts make it the right carrier:

• on an all-cross F it equals the proved nonnegative pure-cross density r324LedgerThreeCrossDensity (r324LedgerThree_norm_sum_flatten_eq), so a density ledger specializes back to the plain R324CappedCrossLedger;
• for an arbitrary F its integral dominates the norm of the summed contraction terms (r324CM_norm_sum_le_integral_flatDensity: proved joint integrability plus one Bochner triangle inequality), so with F the residual-refined fibre it dominates momentRefinedDeterministicTermSum on every fibre — cross or mixed. The sum stays inside the norm, so the renormalization difference factors of within-half pairs keep their cancellation and no factorial entity count is spent.

Why two clauses are needed

The bracket Prop grades its right-hand side by the external modes α, β through r324EndpointLoss ε α β · ⟨ε‖freq(α+β)‖⟩⁻⁸, a weight that tends to 0 as ‖α‖ → ∞. But the density above is exactly independent of α and β (r324CMFlatDensity_modes_indep): the external modes enter the integrand only through four unimodular characters, which factor out of the entity sum. So no bound on a modulus density — however strong — can imply the bracket ledger: the mode decay lives in the cancellation of the external x, y, z, w integrations, which any pointwise norm destroys. The strong ledger therefore has a second, phase-retaining clause, stated on the summed contraction terms, i.e. after the physical integration.

The absolute flat fibre density

noncomputable def Anderson4D.r324CMFlatDensity (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (α β : Z4) (F : Finset (MomentContraction m)) (p : R324PhysicalPoint m) : ℝ

The absolute flat fibre density. Pointwise norm of the summed flattened deterministic integrand over a finite set F of order-m contraction entities. No positivity is assumed of the entities: F may contain entities with within-half pairs, whose flat integrands carry the signed renormalization difference factors.

Equations

• Anderson4D.r324CMFlatDensity ρ ε m α β F p = ‖∑ e ∈ F, Anderson4D.r324Flatten (Anderson4D.deterministicMomentIntegrand ρ ε m α β e.fst e.snd.fst e.snd.snd) p‖

theorem Anderson4D.r324CMFlatDensity_nonneg (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (α β : Z4) (F : Finset (MomentContraction m)) (p : R324PhysicalPoint m) : 0 ≤ r324CMFlatDensity ρ ε m α β F p

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

The density is blind to the external modes. The four external characters are unimodular and do not depend on the entity, so they factor out of the sum and disappear under the norm. Consequently a ledger on this density can never see the mode decay demanded by R324HdetBracketLedgerBound: that decay is a property of the external integrations, not of the pointwise density.

theorem Anderson4D.r324CMFlatDensity_eq_crossDensity (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} (α β : Z4) {F : Finset (MomentContraction m)} (hF : ∀ e ∈ F, R324LedgerThreeAllCrossEntity e) (p : R324PhysicalPoint m) : r324CMFlatDensity ρ ε m α β F p = r324LedgerThreeCrossDensity ρ ε m F p

On a pure-cross entity set the absolute flat density is the proved nonnegative pure-cross density: the external phase is unimodular and every remaining factor is nonnegative.

The integral representation on an arbitrary entity set

theorem Anderson4D.r324CM_sum_term_eq_integral (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) {m : ℕ} (α β : Z4) (F : Finset (MomentContraction m)) : ∑ e ∈ F, deterministicMomentContractionTerm ρ ε m α β e = ∫ (p : R324PhysicalPoint m), ∑ e ∈ F, r324Flatten (deterministicMomentIntegrand ρ ε m α β e.fst e.snd.fst e.snd.snd) p ∂r324PhysicalMeasure m

The summed contraction terms of an arbitrary finite entity set are one physical integral of the summed flat integrand.

theorem Anderson4D.r324CM_norm_sum_le_integral_flatDensity (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) {m : ℕ} (α β : Z4) (F : Finset (MomentContraction m)) : ‖∑ e ∈ F, deterministicMomentContractionTerm ρ ε m α β e‖ ≤ ∫ (p : R324PhysicalPoint m), r324CMFlatDensity ρ ε m α β F p ∂r324PhysicalMeasure m

The cancellation-preserving domination on an arbitrary entity set. Only the Bochner triangle inequality is used; the sum stays inside the norm, so no factorial entity count is spent.

theorem Anderson4D.r324CM_norm_termSum_le_integral_flatDensity (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) {m : ℕ} (α β : Z4) (s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) : ‖momentRefinedDeterministicTermSum ρ ε m α β s r‖ ≤ ∫ (p : R324PhysicalPoint m), r324CMFlatDensity ρ ε m α β (momentRefinedContractionFiber m s r) p ∂r324PhysicalMeasure m

Fibre form: every residual-refined fibre sum — cross or mixed — is dominated by the integral of the absolute flat density of the fibre.

The bracket weight

noncomputable def Anderson4D.r324CMBracketWeight (ε : ℝ) (α β : Z4) : ℝ

The bracket-retaining weight of R324HdetBracketLedgerBound: ε⁻⁸⟨α⟩⁻⁴⟨β⟩⁻⁴ · ⟨ε‖freq(α+β)‖⟩⁻⁸.

Equations

• Anderson4D.r324CMBracketWeight ε α β = Anderson4D.r324EndpointLoss ε α β * Anderson4D.eighthOrderFrequencyDecay (ε * ‖Anderson4D.z4EuclideanFrequency (α + β)‖)

theorem Anderson4D.r324CMBracketWeight_nonneg (ε : ℝ) (α β : Z4) : 0 ≤ r324CMBracketWeight ε α β

The unified obligation

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

Clause A — the capped density ledger. The plain R324CappedCrossLedger is exactly this restricted to pure-cross entity sets and to orders m ≥ 3 (R324CappedCrossLedgerStrong.toCross). The strengthening is that F ranges over arbitrary order-m entity sets, so the signed renormalization difference factors of within-half pairs are covered: this is the parity-gain peel content missing from the plain form. The external modes are frozen at 0 — by r324CMFlatDensity_modes_indep the density does not depend on them.

Equations

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

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

Clause B — the capped bracket density ledger. The phase-retaining companion of clause A: the same entity sets, the same capped order range, but the norm is taken after the physical integration, so the external x, y, z, w cancellation survives and the mode-graded weight r324CMBracketWeight is available. This clause cannot be dropped: by r324CMFlatDensity_modes_indep no modulus-density ledger implies mode decay. It is stated for arbitrary entity sets F, whereas R324HdetBracketLedgerBound asks only for the residual-refined fibres and grants an extra m⁸.

Equations

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

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

The strengthened capped cross ledger: one Prop, two clauses, both stated for arbitrary entity sets on the physical measure at every capped order 2 ≤ m ≤ truncOrder ε. It implies all three residual Props of R324CappedRebaseAssembly.

Equations

• Anderson4D.R324CappedCrossLedgerStrong ρ K = (Anderson4D.R324CappedDensityLedger ρ K ∧ Anderson4D.R324CappedBracketDensityLedger ρ K)

The three reductions

theorem Anderson4D.R324CappedCrossLedgerStrong.toCross {ρ : SmoothCutoff} {K : ℝ} (h : R324CappedCrossLedgerStrong ρ K) : R324CappedCrossLedger ρ K

Reduction 1: the plain capped cross ledger. On an all-cross entity set the absolute flat density equals the proved pure-cross density, so clause A returns the uniform budget verbatim.

theorem Anderson4D.R324CappedCrossLedgerStrong.toMixed {ρ : SmoothCutoff} {K : ℝ} (h : R324CappedCrossLedgerStrong ρ K) : R324CappedMixedLedger ρ K

Reduction 2: the capped mixed ledger. The fibre hypothesis ¬ R324LedgerThreeCrossFibre is never used: clause A covers arbitrary entity sets, so the same estimate holds on every fibre. The external modes are removed by r324CMFlatDensity_modes_indep.

theorem Anderson4D.R324CappedCrossLedgerStrong.toBracket {ρ : SmoothCutoff} {K : ℝ} (hK : 0 ≤ K) (h : R324CappedCrossLedgerStrong ρ K) : R324CappedBracketLedger ρ K

Reduction 3: the bracket-retaining fibre ledger. Clause B at the residual-refined fibre supplies the endpoint loss and the central eighth-order bracket; the proved m⁸ allowance is then free.

Conditional closure from the capped density ledger

theorem Anderson4D.mainConditional_of_cappedCrossLedgerStrong {M : NoiseModel} {ρ : SmoothCutoff} (h : ∃ (K : ℝ), 0 ≤ K ∧ R324CappedCrossLedgerStrong ρ K) : MainConditional M ρ

The single-obligation conditional main theorem. The complete MainConditional M ρ follows from the one capped density ledger R324CappedCrossLedgerStrong. All three capped residual Props of R324CappedRebaseAssembly — the pure-cross density bound, the mixed fibre ledger and the bracket-retaining routed ledger — are supplied by it, and every other input of the proved capped assembly (mainConditional_of_analyticResiduals_capped) is unconditional.