Mode-free reduction of the R-324 middle estimate

The middle estimate R324RefinedInsertedMajorantBound is a per-fibre bound depending on the Fourier modes α, β. Through the scalarized direct Fourier evaluation of R324DirectFourierBranch — which covers every refined fibre, in particular realizing the .directFourier incoming branch with no case split — it reduces to a single mode-independent interior estimate: the weighted interior L¹ mass of each refined fibre against the integrated inserted majorant. Combined with the slot-budget producer of the signed collapse datum, the final deterministic moment bound of R324FinalAssembly follows from two scalar inequalities, neither mentioning Fourier modes, endpoint case splits, or density data.

theorem Anderson4D.paperFourthOrderModeDecay_le_one (k : Z4) : paperFourthOrderModeDecay k ≤ 1

def Anderson4D.R324InteriorCoreMajorantBound (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (primitiveConstant supportConstant : ℝ) : Prop

The mode-free interior form of the middle estimate. The 2m-weighted interior L¹ mass of every refined fibre, with the universal endpoint factor 16, is bounded by the integrated inserted majorant. This is the mode-free Proposition-4.1 content: no Fourier mode, endpoint flag, or incoming case split remains.

Equations

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

theorem Anderson4D.r324RefinedInsertedMajorantBound_of_interiorCore {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {primitiveConstant supportConstant : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (hm : 0 < m) (α β : Z4) (h : R324InteriorCoreMajorantBound ρ lam ε m primitiveConstant supportConstant) : R324RefinedInsertedMajorantBound ρ lam ε m α β primitiveConstant supportConstant

The interior estimate discharges the middle estimate at every pair of Fourier modes: the ⟨α⟩⁻⁴⟨β⟩⁻⁴ decay produced by the direct endpoint evaluation is simply dropped against 1.

theorem Anderson4D.exists_deterministicMoment_paper_bound_of_interiorCore_and_slotBudget {primitiveConstant supportConstant : ℝ} (hprimitive : 0 < primitiveConstant) (hsupport : 0 < supportConstant) : ∃ (outerConstant : ℝ), 0 < outerConstant ∧ ∀ (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (hm : 0 < m) (α β : Z4), 0 ≤ lam → 0 < ε → ε ≤ 1 / 4 → 1 ≤ |Real.log ε| → m ≤ truncOrder ε → R324InteriorCoreMajorantBound ρ lam ε m primitiveConstant supportConstant → (∀ (i : Fin m), ∑' (p : R324RefinedScheduleIndex m × ℕ), ρ.r324SignedRouteSlotWeight lam hm ε i p ≤ ∫ (z : T4), primitiveInsertedMajorant primitiveConstant lam ε supportConstant m z ∂paperMeasure) → ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ paperDeterministicMomentRHS outerConstant (16 * primitiveConstant) lam ε m α β

Final assembly from the two mode-free scalar inputs. The deterministic moment pairing sum obeys the paper bound (3.24) — the P-3.5b-det shape realized by paperDeterministicMomentRHS, including its ⟨α⟩⁻⁴⟨β⟩⁻⁴⟨ε²(α+β)⟩⁻⁸ bracket — given only the interior inserted-majorant estimate and the per-slot signed route budget. Both hypotheses are inequalities of real numbers against the same integrated inserted majorant; the Fourier-mode layers of (3.24) are unconditional.

theorem Anderson4D.paperDeterministicMomentRHS_le_decayBracket (outerConstant powerConstant lam ε : ℝ) (m : ℕ) (α β : Z4) (houter : 0 ≤ outerConstant) (hbase : 0 ≤ powerConstant * lam) : paperDeterministicMomentRHS outerConstant powerConstant lam ε m α β ≤ lamEps lam ε ^ 2 * outerConstant * (powerConstant * lam) ^ (2 * m - 2) * paperDeterministicMomentDecay ε α β

Alignment with the P-3.5b-det decay bracket. The (3.24) bound paperDeterministicMomentRHS has a min bracket that dominates the decay form ε⁻⁸⟨α⟩⁻⁴⟨β⟩⁻⁴⟨ε²(α+β)⟩⁻⁸ carried by paperDeterministicMomentDecay.