Paper Steps 2--3 plus the post-collapse bracket ledger

This module assembles the deterministic estimate (3.24) from the two interfaces that respect the order of operations in paper §4.2. The canonical route is residual-signature refined:

• R324PaperRefinedStep23Input takes the norm only after the complete residual-refined fibre has been integrated and carries the paper's truncation cap explicitly;
• R324HdetBracketLedgerBound takes the norm only after summing the complete residual-refined contraction fibre and retains the central frequency bracket needed in Step 4.

The R324PaperStep23Input form uses positional intervalConfigs; the residual-signature form below avoids that representation.

In particular, this assembly does not use R324PaperStep4Input, R324HdetCrossIntegralBound, or R324LedgerThreeMixedLedger. The order-one decay branch is already unconditional; at orders at least two the bracket ledger is summed by r324HdetAssembly_pairingSum_le_of_bracketLedger.

The residual-signature form of Steps 2--3

def Anderson4D.R324PaperRefinedStep23Input (ρ : SmoothCutoff) (primitiveConstant supportConstant : ℝ) : Prop

Paper Steps 2--3 at the residual-refined fibre level.

One cutoff-dependent primitive constant controls every complete refined fibre at every order in the paper's truncation range. The modulus in MomentRefinedIntegratedReductionOutputAt is outside the contraction-fibre sum and all physical integrations. Thus this interface records the same post-removal ordering as Step 2(f), without encoding the laminar extraction schedule as a family of pairwise-disjoint ambient intervals.

Equations

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

Fixed-scale deterministic estimate

theorem Anderson4D.r324PaperBracket_exists_deterministicMoment_bound (ρ : SmoothCutoff) {Cred supportConstant : ℝ} (hCred : 0 < Cred) (hsupport : 0 < supportConstant) (hstep23 : R324PaperStep23Input ρ Cred supportConstant) (hbracket : ∃ (K : ℝ), 0 ≤ K ∧ R324HdetBracketLedgerBound ρ K) : ∃ (outerC : ℝ) (powerC : ℝ), 0 < outerC ∧ 0 < powerC ∧ ∀ (lam : ℝ), 0 ≤ lam → ∀ {ε : ℝ}, 0 < ε → ε ≤ 1 / 4 → 1 ≤ |Real.log ε| → ∀ (m : ℕ), 1 ≤ m → m ≤ truncOrder ε → ∀ (α β : Z4), ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ deterministicMomentRHS outerC powerC lam ε m α β

The fixed-scale deterministic estimate (3.24) from the paper's Steps 2--3 and the post-collapse bracket ledger.

The uniform branch is exists_r324Step23_config_bound. The decay branch is the unconditional order-one routed estimate at m = 1, and the summed bracket ledger at m >= 2. The two estimates are combined only after the full deterministic pairing sum has been formed.

Eventually-small-scale hdet and the conditional main theorem

theorem Anderson4D.r324PaperBracket_hdet (ρ : SmoothCutoff) {Cred supportConstant : ℝ} (hCred : 0 < Cred) (hsupport : 0 < supportConstant) (hstep23 : R324PaperStep23Input ρ Cred supportConstant) (hbracket : ∃ (K : ℝ), 0 ≤ K ∧ R324HdetBracketLedgerBound ρ K) : ∃ (outerC : ℝ) (powerC : ℝ), 0 < outerC ∧ 0 < powerC ∧ ∀ (lam : ℝ), 0 < lam → ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (m : ℕ), 1 ≤ m → m ≤ truncOrder ε → ∀ (α β : Z4), ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ deterministicMomentRHS outerC powerC lam ε m α β

The exact deterministic hypothesis of mainConditional_of_deterministic_bounds, obtained without either of the pre-collapse norm interfaces.

theorem Anderson4D.mainConditional_of_paperStep23_and_bracketLedger {M : NoiseModel} {ρ : SmoothCutoff} {Cred supportConstant : ℝ} (hCred : 0 < Cred) (hsupport : 0 < supportConstant) (hstep23 : R324PaperStep23Input ρ Cred supportConstant) (hbracket : ∃ (K : ℝ), 0 ≤ K ∧ R324HdetBracketLedgerBound ρ K) : MainConditional M ρ

Conditional Theorem 1.1 from the paper's Steps 2--3 and the post-collapse bracket ledger.

The counterterm estimate (3.22) is unconditional. Consequently the only remaining deterministic premise is the bracket ledger, whose norm is taken after every interval removal and after the full residual-fibre sum.

Canonical residual-refined assembly

theorem Anderson4D.r324PaperRefinedBracket_exists_deterministicMoment_bound (ρ : SmoothCutoff) {primitiveConstant supportConstant : ℝ} (hprimitive : 0 < primitiveConstant) (hsupport : 0 < supportConstant) (hstep23 : R324PaperRefinedStep23Input ρ primitiveConstant supportConstant) (hbracket : ∃ (K : ℝ), 0 ≤ K ∧ R324HdetBracketLedgerBound ρ K) : ∃ (outerC : ℝ) (powerC : ℝ), 0 < outerC ∧ 0 < powerC ∧ ∀ (lam : ℝ), 0 ≤ lam → ∀ {ε : ℝ}, 0 < ε → ε ≤ 1 / 4 → 1 ≤ |Real.log ε| → ∀ (m : ℕ), 1 ≤ m → m ≤ truncOrder ε → ∀ (α β : Z4), ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ deterministicMomentRHS outerC powerC lam ε m α β

The fixed-scale deterministic estimate (3.24) from the residual-refined Steps 2--3 interface and the post-collapse bracket ledger.

Unlike the compatibility theorem above, this statement has no positional configuration input. The uniform branch is produced directly by exists_deterministicMoment_uniform_bound_of_refinedIntegratedReduction.

theorem Anderson4D.r324PaperRefinedBracket_hdet (ρ : SmoothCutoff) {primitiveConstant supportConstant : ℝ} (hprimitive : 0 < primitiveConstant) (hsupport : 0 < supportConstant) (hstep23 : R324PaperRefinedStep23Input ρ primitiveConstant supportConstant) (hbracket : ∃ (K : ℝ), 0 ≤ K ∧ R324HdetBracketLedgerBound ρ K) : ∃ (outerC : ℝ) (powerC : ℝ), 0 < outerC ∧ 0 < powerC ∧ ∀ (lam : ℝ), 0 < lam → ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (m : ℕ), 1 ≤ m → m ≤ truncOrder ε → ∀ (α β : Z4), ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ deterministicMomentRHS outerC powerC lam ε m α β

The exact eventually-small-scale deterministic hypothesis, now from the residual-refined Steps 2--3 interface rather than positional configurations.

theorem Anderson4D.mainConditional_of_paperRefinedStep23_and_bracketLedger {M : NoiseModel} {ρ : SmoothCutoff} {primitiveConstant supportConstant : ℝ} (hprimitive : 0 < primitiveConstant) (hsupport : 0 < supportConstant) (hstep23 : R324PaperRefinedStep23Input ρ primitiveConstant supportConstant) (hbracket : ∃ (K : ℝ), 0 ≤ K ∧ R324HdetBracketLedgerBound ρ K) : MainConditional M ρ

Canonical conditional Theorem 1.1 from the residual-refined Steps 2--3 output and the post-collapse bracket ledger.

This theorem has no dependency on R324PaperStep23Input or its intervalConfigs encoding.