The conditional main theorem along the paper's own §4.2

Paper: R-324 — §4.2 assembled: Steps 1–4 ⇒ (3.24) ⇒ Theorem 1.1

The proved top-level route mainConditional_of_analyticResiduals_capped reaches MainConditional from R324CappedCrossLedgerStrong, whose two clauses take absolute values of the refined fibre cores before any subinterval has been removed. The paper does the opposite: Step 2(f) is explicit that absolute values come last, after every removal, and not_r324InteriorCoreLogBudget_two shows that taking them early at m ≥ 2 discards the renormalizing Green-difference factor.

This module gives the route that follows the paper's ordering. Its input is the paper's own Steps 2–3 output, per interval configuration (R324Step23ConfigReduction: the successive removal has been performed and only then is a norm taken), together with Step 4(B)'s summable route budget. Everything else — Step 1, the positional 16^m count, the nested chain of Step 3, Step 4's two decay mechanisms, the counterterm bound (3.22) — is already unconditional.

def Anderson4D.R324PaperStep23Input (ρ : SmoothCutoff) (Cred supportConstant : ℝ) : Prop

The Steps 2–3 interface from paper §4.2.

At every coupling, every small scale, and every order inside the paper truncation, the successive removal of §4.1 has been carried out on each Definition 3.1 interval configuration, and only afterwards is a modulus taken — this is exactly Step 2(f). R324Step23ConfigReduction records the result: per configuration, the gained (Cλ)^{2m-2k} times one integrated inserted majorant of (4.4).

Equations

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

def Anderson4D.R324PaperStep4Input (ρ : SmoothCutoff) (amp : ℝ → ℝ → ℕ → ℝ) : Prop

The Step 4(B) interface from paper §4.2.

The central ⟨ε²(α+β)⟩⁻⁸ factor comes from the ε^{1/2} pigeonhole over the at most |log ε| composition factors. After countableCentralRoutedMomentReductionOutput_of_tsum_le the whole mechanism rests on one summable series and its total mass; amp is the amplitude Steps 2–3 have already produced.

Equations

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

theorem Anderson4D.r324Paper_endpoint_premise {ε : ℝ} {α β : Z4} {amp amplitude : ℝ} (hloss : 0 ≤ r324EndpointLoss ε α β) (h : 16 * amp ≤ amplitude) : 16 * amp * r324EndpointLoss ε α β ≤ amplitude * (r324Step4EndpointBudget ε α * r324Step4EndpointBudget ε β * (r324Step4EndpointBudget ε α * r324Step4EndpointBudget ε β))

Step 4(A)'s endpoint premise, in the form the routed budget produces.

countableCentralRoutedMomentReductionOutput_of_tsum_le delivers the routed output at total weight (16·amp)·r324EndpointLoss, while r324Step4_fourEndpoint_budget_eq says the product of the four endpoint budgets is r324EndpointLoss. So the premise of r324Step4_deterministicMomentRHS_of_step23 holds as soon as 16·amp does not exceed the Steps 2–3 amplitude.

theorem Anderson4D.r324Paper_deterministicMoment_bound (ρ : SmoothCutoff) {Cred supportConstant : ℝ} (hCred : 0 < Cred) (hsupport : 0 < supportConstant) (hstep23 : R324PaperStep23Input ρ Cred supportConstant) : ∃ (outerC : ℝ) (powerC : ℝ), 0 < outerC ∧ 0 < powerC ∧ ((R324PaperStep4Input ρ fun (lam ε : ℝ) (m : ℕ) => lamEps lam ε ^ 2 * outerC * (powerC * lam) ^ (2 * m - 2) / 16) → ∀ (lam ε : ℝ) (m : ℕ) (α β : Z4), 0 ≤ lam → 0 < ε → ε ≤ 1 / 4 → 1 ≤ |Real.log ε| → 1 ≤ m → m ≤ truncOrder ε → ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ deterministicMomentRHS outerC powerC lam ε m α β)

§4.2 assembled: the fixed-scale (3.24) bound from the paper's own inputs.

Steps 2–3 give the amplitude; Step 4(B) turns the summable route budget into the countable routed decomposition; Step 4(A)'s endpoint premise is the arithmetic above; r324Step4_deterministicMomentRHS_of_step23 lands the two together in the frozen right side deterministicMomentRHS.

theorem Anderson4D.r324Paper_hdet (ρ : SmoothCutoff) {Cred supportConstant : ℝ} (hCred : 0 < Cred) (hsupport : 0 < supportConstant) (hstep23 : R324PaperStep23Input ρ Cred supportConstant) : ∃ (outerC : ℝ) (powerC : ℝ), 0 < outerC ∧ 0 < powerC ∧ ((R324PaperStep4Input ρ fun (lam ε : ℝ) (m : ℕ) => lamEps lam ε ^ 2 * outerC * (powerC * lam) ^ (2 * m - 2) / 16) → ∀ (lam : ℝ), 0 < lam → ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (m : ℕ), 1 ≤ m → m ≤ truncOrder ε → ∀ (α β : Z4), ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ deterministicMomentRHS outerC powerC lam ε m α β)

The hdet hypothesis of mainConditional_of_deterministic_bounds, from the paper's own §4.2 inputs.

theorem Anderson4D.mainConditional_of_paperStep23_and_step4 {M : NoiseModel} {ρ : SmoothCutoff} {Cred supportConstant : ℝ} (hCred : 0 < Cred) (hsupport : 0 < supportConstant) (hstep23 : R324PaperStep23Input ρ Cred supportConstant) (hstep4 : ∀ (outerC powerC : ℝ), R324PaperStep4Input ρ fun (lam ε : ℝ) (m : ℕ) => lamEps lam ε ^ 2 * outerC * (powerC * lam) ^ (2 * m - 2) / 16) : MainConditional M ρ

The conditional main theorem, along the paper's own §4.2.

MainConditional M ρ from the paper's Steps 2–3 output — taken after every removal, per Step 2(f) — together with Step 4(B)'s summable route budget. The counterterm side is the proved unconditional R322AnalyticResidualPrefix.exists_r322_renormC2q_bound (paper (3.22)).

This is the sound replacement of mainConditional_of_analyticResiduals_capped: its input respects the paper's ordering of the modulus, so it is not exposed to the obstruction not_r324InteriorCoreLogBudget_two records for pre-collapse norms.