Final assembly of the R-324 deterministic moment bound

This file assembles the R-324 deterministic estimate:

• the driver mode-decay bounds of R324DriverClosure are restated with the joint-integrability premise discharged for the canonical transport afterHeadAlternatingTransport, using R324TerminalJointIntegrability);
• the uniform-branch middle estimate is isolated as the named Prop R324RefinedInsertedMajorantBound and wired into MomentRefinedIntegratedReductionOutputAt;
• the deterministic-moment paper bound (the P-3.5b-det shape) is produced from these inputs through the signed routed collapse.

The routed branch is consumed in countable-series form. Its production is packaged by SignedRoutedPrimitiveSlotCollapseData, which derives CountableCentralRoutedMomentReductionOutput at the endpoint-weighted budget.

The complementary incoming branch

The remaining middle estimate R324RefinedInsertedMajorantBound is a per-schedule-index bound, and the incoming-endpoint case split (⟨0, hm⟩ ∈ finalActive e₀.1) versus (∉) lives inside it, per contraction entity: the driver assemblies (R324IncomingExceptionalStopTraceAssembly.exists_of_localBlockProvider) exist exactly on the ∉ branch, while on the ∈ branch the incoming endpoint's vertex survives the whole schedule and the state keeps the direct Green factor at slot zero (state_edges_zero_eq_greenFn_of_first_mem_finalActive), selecting the .directFourier case of r324IncomingEndpointReductionCase — the branch with one more raw Green leg and fewer collapsed heads. On the outgoing side the analogous split is the boolean r324OutgoingIsShortcut; the non-shortcut branch is closed below with gap (a) discharged.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.norm_lamEps_pow_mul_r324RefinedPhysicalIntegral_le_modeDecay_of_provider {ρ : SmoothCutoff} {C lam ε K : ℝ} {m : ℕ} {initialScale : Fin (m + 1) → ℝ} (p : R324RefinedScheduleIndex m) (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentRefinedContractionFiber m ↑p.fst ↑p.snd) (data : R324IncomingExceptionalStopTraceAssembly e₀.fst initialScale) (hm : 0 < m) (hε : 0 < ε) (hε1 : ε ≤ 1) (provider : R324WithinHalfLocalBlockProvider ρ C lam ε K e₀.fst) (hG : ∀ (j : Fin (2 * residualBlockOrder data.stopContext.step.2 - 1)), MemEClassT4 (data.stopContext.internalEdges j)) (hint : ∀ (gap first : T4) (κB : ↥(primitiveFullPairings (residualBlockOrder data.terminal.2))), MeasureTheory.Integrable (fun (r : Fin (2 * residualBlockOrder data.terminal.2 - 2) → T4) => detJclosedIntegrandWith ρ ε (2 * residualBlockOrder data.terminal.2) (↑κB) data.stopContext.internalEdges (primitiveAssemble (residualBlockOrder data.terminal.2) ⋯ first (first + gap) r)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder data.terminal.2 - 2)) => paperMeasure)) (α β : Z4) (hdirect : r324OutgoingIsShortcut e₀.fst = false) : ‖↑(lamEps lam ε) ^ (2 * (initial ρ lam ε e₀.fst).remainingOrder) * r324RefinedPhysicalIntegral ρ ε m α β p‖ ≤ paperSecondOrderModeDecay β * (∫ (z : T4), |greenFn z| ∂paperMeasure)⁻¹ * ∫ (q : R324IncomingExceptionalRootParameter ρ lam ε e₀.snd.fst × ((data.afterHeadAlternatingTransport hε hε1 provider).final.SurvivingCoordinate → T4)), ‖(data.afterHeadAlternatingTransport hε hε1 provider).final.incomingPhasedResidualDensity ((data.afterHeadAlternatingTransport hε hε1 provider).multiplier α * data.incomingExceptionalRefinedRootDriverCoefficient (data.afterHeadAlternatingTransport hε hε1 provider) α β e₀.snd.snd q.1 q.2) α ρ ε 0 q.1.1.1 q.2‖ ∂(r324IncomingExceptionalRootParameterMeasure ρ lam ε e₀.snd.fst).prod (MeasureTheory.Measure.pi fun (x : (data.afterHeadAlternatingTransport hε hε1 provider).final.SurvivingCoordinate) => paperMeasure)

Gap (a) consumed: the outgoing mode-decay upgrade holds unconditionally for the canonical driver transport. Both the joint integrability premise and the nonempty-active premise of norm_lamEps_pow_mul_r324RefinedPhysicalIntegral_le_modeDecay_of_not_shortcut are discharged: the first by the terminal certificate extracted from the driver recursion, the second because the non-shortcut outgoing frozen pairing keeps the last internal vertex active.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.norm_lamEps_pow_ambient_mul_r324RefinedPhysicalIntegral_le_modeDecay_of_provider {ρ : SmoothCutoff} {C lam ε K : ℝ} {m : ℕ} {initialScale : Fin (m + 1) → ℝ} (p : R324RefinedScheduleIndex m) (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentRefinedContractionFiber m ↑p.fst ↑p.snd) (data : R324IncomingExceptionalStopTraceAssembly e₀.fst initialScale) (hm : 0 < m) (hε : 0 < ε) (hε1 : ε ≤ 1) (provider : R324WithinHalfLocalBlockProvider ρ C lam ε K e₀.fst) (hG : ∀ (j : Fin (2 * residualBlockOrder data.stopContext.step.2 - 1)), MemEClassT4 (data.stopContext.internalEdges j)) (hint : ∀ (gap first : T4) (κB : ↥(primitiveFullPairings (residualBlockOrder data.terminal.2))), MeasureTheory.Integrable (fun (r : Fin (2 * residualBlockOrder data.terminal.2 - 2) → T4) => detJclosedIntegrandWith ρ ε (2 * residualBlockOrder data.terminal.2) (↑κB) data.stopContext.internalEdges (primitiveAssemble (residualBlockOrder data.terminal.2) ⋯ first (first + gap) r)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder data.terminal.2 - 2)) => paperMeasure)) (α β : Z4) (hdirect : r324OutgoingIsShortcut e₀.fst = false) : |lamEps lam ε| ^ (2 * m) * ‖r324RefinedPhysicalIntegral ρ ε m α β p‖ ≤ paperSecondOrderModeDecay β * (∫ (z : T4), |greenFn z| ∂paperMeasure)⁻¹ * ∫ (q : R324IncomingExceptionalRootParameter ρ lam ε e₀.snd.fst × ((data.afterHeadAlternatingTransport hε hε1 provider).final.SurvivingCoordinate → T4)), |lamEps lam ε| ^ (2 * (initial ρ lam ε e₀.snd.fst).remainingOrder + 2 * (R324NestedCrossResidualPrefix.initial e₀.fst e₀.snd.fst e₀.snd.snd).remainingOrder) * ‖(data.afterHeadAlternatingTransport hε hε1 provider).final.incomingPhasedResidualDensity ((data.afterHeadAlternatingTransport hε hε1 provider).multiplier α * data.incomingExceptionalRefinedRootDriverCoefficient (data.afterHeadAlternatingTransport hε hε1 provider) α β e₀.snd.snd q.1 q.2) α ρ ε 0 q.1.1.1 q.2‖ ∂(r324IncomingExceptionalRootParameterMeasure ρ lam ε e₀.snd.fst).prod (MeasureTheory.Measure.pi fun (x : (data.afterHeadAlternatingTransport hε hε1 provider).final.SurvivingCoordinate) => paperMeasure)

Gaps (a)+(b) combined, unconditional form: the full-ambient-weight mode-decay bound for the canonical driver transport, with the joint integrability and active-carrier premises discharged.

The remaining middle estimate, as a named interface

def Anderson4D.R324RefinedInsertedMajorantBound (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (α β : Z4) (primitiveConstant supportConstant : ℝ) : Prop

Gap (b), the middle estimate (open). The 2m-weighted refined physical integral is bounded, uniformly over the refined schedule index, by the integrated inserted majorant. On the driver branch this is the estimate connecting the mode-decay output of norm_lamEps_pow_ambient_mul_r324RefinedPhysicalIntegral_le_modeDecay_of_provider (with gap (a) discharged) to ∫ primitiveInsertedMajorant; it contains the per-contraction case splits ⟨0, hm⟩ ∈/∉ finalActive (incoming) and r324OutgoingIsShortcut (outgoing).

Equations

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

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

The middle estimate discharges the integrated residual-refined reduction interface MomentRefinedIntegratedReductionOutputAt.

The deterministic moment paper bound (P-3.5b-det shape)

theorem Anderson4D.exists_deterministicMoment_paper_bound_of_insertedMajorant_and_signedCollapse {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 ε → R324RefinedInsertedMajorantBound ρ lam ε m α β primitiveConstant supportConstant → ∀ (a : ρ.SignedRoutedPrimitiveSlotCollapseData lam ε m hm primitiveConstant supportConstant), ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ paperDeterministicMomentRHS outerConstant (16 * primitiveConstant) lam ε m α β

The R-324 final assembly (P-3.5b-det shape). Given the middle estimate R324RefinedInsertedMajorantBound and the signed routed primitive slot collapse data (the routing input, consumed through the countable central interface), the deterministic moment pairing sum obeys the paper bound of (3.24), including the ⟨α⟩⁻⁴⟨β⟩⁻⁴⟨ε²(α+β)⟩⁻⁸ decay bracket carried by paperDeterministicMomentRHS.

The realized P-3.5b-det shape is this bound on deterministicMomentPairingSum against paperDeterministicMomentRHS outerConstant (16 * primitiveConstant), as in R324FinalDeterministicClosure and R324SignedFinalClosure.

theorem Anderson4D.exists_deterministicMoment_paper_bound_of_insertedMajorant_and_countable {primitiveConstant supportConstant : ℝ} (hprimitive : 0 < primitiveConstant) (hsupport : 0 < supportConstant) : ∃ (outerConstant : ℝ), 0 < outerConstant ∧ ∀ (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (α β : Z4), 0 ≤ lam → 0 < ε → ε ≤ 1 / 4 → 1 ≤ |Real.log ε| → 1 ≤ m → R324RefinedInsertedMajorantBound ρ lam ε m α β primitiveConstant supportConstant → CountableCentralRoutedMomentReductionOutput ρ lam ε m α β (lamEps lam ε ^ 2 * outerConstant * (16 * primitiveConstant * lam) ^ (2 * m - 2) * r324EndpointLoss ε α β) → ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ paperDeterministicMomentRHS outerConstant (16 * primitiveConstant) lam ε m α β

Variant of the final assembly consuming the countable central routed interface directly, for callers that produce CountableCentralRoutedMomentReductionOutput by other means (the _of_zeroShift / _of_nonzeroRoutes branch producers of R324NonzeroRoutedDensity).