Driver closure for the R-324 endgame

Three scoped closures on top of the driver scalar bound:

• the ambient exponent ledger for one complete contraction entity: the left initial order, the right initial order, and the nested-cross order partition the moment order m, so the full 2m coupling weight splits into the driver weight and a leftover right/cross weight;
• the uniform head-collapse budget instantiated from the integrated Proposition 4.1 kernel majorant, with the (Cλ)^{2n} factor absorbed by the small-coupling regime;
• the terminal y-Fourier evaluation of the driver-terminal phased density under the root measure, exchanging one raw outgoing Green leg for the paper second-order mode decay in the outgoing mode.

The ambient exponent ledger for one contraction entity

theorem Anderson4D.momentContraction_initial_remainingOrders_eq_ambient (ρ : SmoothCutoff) (lam ε : ℝ) {m : ℕ} (e₀ : MomentContraction m) : (R324WithinHalfResidualPrefix.initial ρ lam ε e₀.fst).remainingOrder + (R324WithinHalfResidualPrefix.initial ρ lam ε e₀.snd.fst).remainingOrder + (R324NestedCrossResidualPrefix.initial e₀.fst e₀.snd.fst e₀.snd.snd).remainingOrder = m

The two within-half initial suffixes and the nested-cross initial suffix of one complete contraction entity partition the ambient moment order.

theorem Anderson4D.momentContraction_two_mul_ambient_eq_ledger (ρ : SmoothCutoff) (lam ε : ℝ) {m : ℕ} (e₀ : MomentContraction m) : 2 * m = 2 * (R324WithinHalfResidualPrefix.initial ρ lam ε e₀.fst).remainingOrder + (2 * (R324WithinHalfResidualPrefix.initial ρ lam ε e₀.snd.fst).remainingOrder + 2 * (R324NestedCrossResidualPrefix.initial e₀.fst e₀.snd.fst e₀.snd.snd).remainingOrder)

The doubled ambient exponent splits into the driver exponent and the leftover right/cross exponents.

theorem Anderson4D.abs_lamEps_pow_ambient_eq_three_part (ρ : SmoothCutoff) (lam ε : ℝ) {m : ℕ} (e₀ : MomentContraction m) : |lamEps lam ε| ^ (2 * m) = |lamEps lam ε| ^ (2 * (R324WithinHalfResidualPrefix.initial ρ lam ε e₀.fst).remainingOrder) * (|lamEps lam ε| ^ (2 * (R324WithinHalfResidualPrefix.initial ρ lam ε e₀.snd.fst).remainingOrder) * |lamEps lam ε| ^ (2 * (R324NestedCrossResidualPrefix.initial e₀.fst e₀.snd.fst e₀.snd.snd).remainingOrder))

Three-part multiplicative split of the full ambient coupling weight along the ledger of one contraction entity.

The free Green function's L¹ mass

theorem Anderson4D.paperSecondOrderModeDecay_pos (k : Z4) : 0 < paperSecondOrderModeDecay k

The paper second-order bracket is strictly positive.

theorem Anderson4D.paperSecondOrderModeDecay_le_integral_abs_greenFn (k : Z4) : paperSecondOrderModeDecay k ≤ ∫ (z : T4), |greenFn z| ∂paperMeasure

Every second-order mode coefficient is dominated by the raw L¹ mass of the free Green function.

theorem Anderson4D.integral_abs_greenFn_pos : 0 < ∫ (z : T4), |greenFn z| ∂paperMeasure

The free Green function has strictly positive L¹ mass.

theorem Anderson4D.integral_abs_greenFn_sub (a : T4) : ∫ (y : T4), |greenFn (a - y)| ∂paperMeasure = ∫ (z : T4), |greenFn z| ∂paperMeasure

Reflected-translation invariance of the Green L¹ mass.

Regrouping the root parameter around the outgoing endpoint

def Anderson4D.r324DriverTerminalRegroupMeasurableEquiv (Y : Type u_1) (ZW : Type u_2) (VR : Type u_3) (U : Type u_4) [MeasurableSpace Y] [MeasurableSpace ZW] [MeasurableSpace VR] [MeasurableSpace U] : ((Y × ZW) × VR) × U ≃ᵐ (ZW × VR) × Y × U

Regroup the root/terminal product so that the free outgoing endpoint pairs with the terminal coordinates: ((y,zw),vr,u) ↦ ((zw,vr),(y,u)).

Equations

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

@[simp]

theorem Anderson4D.r324DriverTerminalRegroupMeasurableEquiv_apply {Y : Type u_1} {ZW : Type u_2} {VR : Type u_3} {U : Type u_4} [MeasurableSpace Y] [MeasurableSpace ZW] [MeasurableSpace VR] [MeasurableSpace U] (q : ((Y × ZW) × VR) × U) : (r324DriverTerminalRegroupMeasurableEquiv Y ZW VR U) q = ((q.1.1.2, q.1.2), q.1.1.1, q.2)

@[simp]

theorem Anderson4D.r324DriverTerminalRegroupMeasurableEquiv_symm_apply {Y : Type u_1} {ZW : Type u_2} {VR : Type u_3} {U : Type u_4} [MeasurableSpace Y] [MeasurableSpace ZW] [MeasurableSpace VR] [MeasurableSpace U] (p : (ZW × VR) × Y × U) : (r324DriverTerminalRegroupMeasurableEquiv Y ZW VR U).symm p = (((p.2.1, p.1.1), p.1.2), p.2.2)

theorem Anderson4D.measurePreserving_r324DriverTerminalRegroupMeasurableEquiv {Y : Type u_1} {ZW : Type u_2} {VR : Type u_3} {U : Type u_4} [MeasurableSpace Y] [MeasurableSpace ZW] [MeasurableSpace VR] [MeasurableSpace U] (μY : MeasureTheory.Measure Y) (μZW : MeasureTheory.Measure ZW) (μVR : MeasureTheory.Measure VR) (μU : MeasureTheory.Measure U) [MeasureTheory.SFinite μY] [MeasureTheory.SFinite μZW] [MeasureTheory.SFinite μVR] [MeasureTheory.SFinite μU] : MeasureTheory.MeasurePreserving (⇑(r324DriverTerminalRegroupMeasurableEquiv Y ZW VR U)) (((μY.prod μZW).prod μVR).prod μU) ((μZW.prod μVR).prod (μY.prod μU))

The outgoing-endpoint regrouping preserves the product measures.

Uniform kernel-majorant budget in the small-coupling regime

theorem Anderson4D.exists_uniform_integral_primitiveKernelMajorant_budget : ∃ (Cball : ℝ) (Creg : ℝ), 0 < Cball ∧ 0 < Creg ∧ ∀ (C lam ε supportConstant : ℝ) (n : ℕ), 0 < ε → 0 < supportConstant → 1 ≤ |Real.log ε| → |C * lam| ≤ 1 → 2 * ∫ (u : T4), primitiveKernelMajorant C lam ε supportConstant n u ∂paperMeasure ≤ max 1 (2 * ((Cball * supportConstant ^ 2 + Creg) * ε⁻¹ ^ 2 / |Real.log ε|))

Order-uniform integrated Proposition 4.1 budget. In the small-coupling regime |Cλ| ≤ 1 the order-dependent factor (Cλ)^{2n} of the integrated kernel majorant is at most one, so a single explicit ε⁻²/|log ε| budget dominates every primitive order at once.

theorem Anderson4D.R324WithinHalfResidualPrefix.exists_r324WithinHalfHeadCollapseBudget_of_kernelBounds {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (supportConstant primitiveConstant : ℝ) (hε : 0 < ε) (hsupport : 0 < supportConstant) (hlog : 1 ≤ |Real.log ε|) (hsmall : |primitiveConstant * lam| ≤ 1) (huniform : ∀ (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail), (∀ (j : Fin (2 * residualBlockOrder (res.headContext head tail hremaining).step.2 - 1)), Measurable ((res.headContext head tail hremaining).internalEdges j)) ∧ (∀ (j : Fin (2 * residualBlockOrder (res.headContext head tail hremaining).step.2 - 1)), MemEClassT4 ((res.headContext head tail hremaining).internalEdges j)) ∧ PrimitiveKernelBounds ρ lam ε (residualBlockOrder head.2) ⋯ (res.headContext head tail hremaining).internalEdges supportConstant primitiveConstant) : ∃ (B : ℝ), 1 ≤ B ∧ ∀ (k : Z4), R324WithinHalfHeadCollapseBudget ρ lam ε pairing k B

Gap (c): the head-collapse budget instantiated. Pointwise Proposition 4.1 kernel bounds at every reachable head, the small-coupling regime, and the logarithmic window discharge the uniform head-collapse budget with one explicit mode-independent B ≥ 1.

theorem Anderson4D.R324WithinHalfResidualPrefix.norm_terminal_incomingPhasedResidualDensity_eq_greenFn_mul {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hnil : res.remaining = []) (hactive : res.state.active.Nonempty) (hedge : res.state.edges (res.terminalOutgoingEdgeSlot hactive) = greenFn) (coefficient : ℂ) (k : Z4) (ρ' : SmoothCutoff) (ε' : ℝ) (x y : T4) (v : res.SurvivingCoordinate → T4) : ‖res.incomingPhasedResidualDensity coefficient k ρ' ε' x y v‖ = ‖coefficient‖ * |res.endpointErasedSignedChain hactive 0 0 (res.reconstruct v)| * |greenFn (res.terminalOutgoingAnchor hactive (res.reconstruct v) - y)|

Terminal density norm with the raw outgoing Green leg split off: under the direct outgoing geometry the whole y-dependence is one translated free Green factor.

theorem Anderson4D.R324WithinHalfResidualPrefix.integral_norm_terminal_incomingPhasedResidualDensity_eq {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hnil : res.remaining = []) (hactive : res.state.active.Nonempty) (hedge : res.state.edges (res.terminalOutgoingEdgeSlot hactive) = greenFn) (coefficient : ℂ) (k : Z4) (ρ' : SmoothCutoff) (ε' : ℝ) (x : T4) (v : res.SurvivingCoordinate → T4) : ∫ (y : T4), ‖res.incomingPhasedResidualDensity coefficient k ρ' ε' x y v‖ ∂paperMeasure = ‖coefficient‖ * |res.endpointErasedSignedChain hactive 0 0 (res.reconstruct v)| * ∫ (z : T4), |greenFn z| ∂paperMeasure

Exact y-marginal of the terminal density norm: the raw outgoing Green leg integrates to the Green L¹ mass, independently of the terminal coordinates.

theorem Anderson4D.R324WithinHalfResidualPrefix.norm_integral_rootProd_incomingPhasedResidualDensity_le_modeDecay {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hnil : res.remaining = []) (hactive : res.state.active.Nonempty) (hedge : res.state.edges (res.terminalOutgoingEdgeSlot hactive) = greenFn) {ZW : Type u_1} {VR : Type u_2} [MeasurableSpace ZW] [MeasurableSpace VR] (μZW : MeasureTheory.Measure ZW) (μVR : MeasureTheory.Measure VR) [MeasureTheory.SFinite μZW] [MeasureTheory.SFinite μVR] (red : ZW → VR → (res.SurvivingCoordinate → T4) → ℂ) (β k : Z4) (hjoint : MeasureTheory.Integrable (fun (q : ((T4 × ZW) × VR) × (res.SurvivingCoordinate → T4)) => res.incomingPhasedResidualDensity (charT4 β q.1.1.1 * red q.1.1.2 q.1.2 q.2) k ρ ε 0 q.1.1.1 q.2) (((paperMeasure.prod μZW).prod μVR).prod (MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure))) : ‖∫ (q : ((T4 × ZW) × VR) × (res.SurvivingCoordinate → T4)), res.incomingPhasedResidualDensity (charT4 β q.1.1.1 * red q.1.1.2 q.1.2 q.2) k ρ ε 0 q.1.1.1 q.2 ∂((paperMeasure.prod μZW).prod μVR).prod (MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure)‖ ≤ paperSecondOrderModeDecay β * (∫ (z : T4), |greenFn z| ∂paperMeasure)⁻¹ * ∫ (q : ((T4 × ZW) × VR) × (res.SurvivingCoordinate → T4)), ‖res.incomingPhasedResidualDensity (charT4 β q.1.1.1 * red q.1.1.2 q.1.2 q.2) k ρ ε 0 q.1.1.1 q.2‖ ∂((paperMeasure.prod μZW).prod μVR).prod (MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure)

The y-Fourier evaluation under the root measure. For a terminal prefix with the direct outgoing Green geometry, and a coefficient family carrying the outgoing character charT4 β at the free outgoing endpoint but otherwise independent of it, the joint root integral of the phased density is damped by the paper second-order mode decay at β, at the price of the raw Green L¹ mass. Joint integrability of the density is the only analytic hypothesis.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.abs_lamEps_pow_mul_norm_incomingExceptionalRefinedRootDriverCoefficient_eq {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {C K : ℝ} {κp κm : PartialPairing (Fin m)} {initialScale : Fin (m + 1) → ℝ} (data : R324IncomingExceptionalStopTraceAssembly κp initialScale) (t : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).R324WithinHalfAlternatingTransport) (α β : Z4) (π : ↥κp.singles ≃ ↥κm.singles) (ω : R324IncomingExceptionalRootParameter ρ lam ε κm) (u : t.final.SurvivingCoordinate → T4) (a b : ℕ) : |lamEps lam ε| ^ (2 * a + 2 * b) * ‖data.incomingExceptionalRefinedRootDriverCoefficient t α β π ω u‖ = paperSecondOrderModeDecay α ^ 2 * ‖incomingExceptionalPrimitiveDefect ρ lam ε (residualBlockOrder data.terminal.2) ⋯ data.stopContext.internalEdges α‖ * (|lamEps lam ε| ^ (2 * a) * |(initial ρ lam ε κm).residualIntegrand ρ ε ω.1.2.1 ω.1.2.2 ((initial ρ lam ε κm).reconstruct ω.2)| * (|lamEps lam ε| ^ (2 * b) * |r324ResidualPrimitiveSumProduct ρ ε κp κm π (r324TwoHalfRootDoubledReconstruct t.final (initial ρ lam ε κm) (u, ω.2))|))

Gap (b), coefficient form. The leftover right/cross coupling weight lands multiplicatively on the two untouched scalar factors of the collapsed-head refined driver coefficient: the right initial residual integrand receives the right-half weight and the cross-cut primitive factor receives the nested-cross weight.

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.incomingExceptionalRefinedRootDriverReducedCoefficient {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {C K : ℝ} {κp κm : PartialPairing (Fin m)} {initialScale : Fin (m + 1) → ℝ} (data : R324IncomingExceptionalStopTraceAssembly κp initialScale) (t : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).R324WithinHalfAlternatingTransport) (α β : Z4) (π : ↥κp.singles ≃ ↥κm.singles) (zw : T4 × T4) (vr : (initial ρ lam ε κm).SurvivingCoordinate → T4) (u : t.final.SurvivingCoordinate → T4) : ℂ

The multiplier-weighted collapsed-head refined driver coefficient with the outgoing character charT4 β at the free outgoing endpoint stripped off; it depends on the root parameter only through the two measured endpoints and the right initial tuple.

Equations

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

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.multiplier_mul_driverCoefficient_eq_char_mul_reduced {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {C K : ℝ} {κp κm : PartialPairing (Fin m)} {initialScale : Fin (m + 1) → ℝ} (data : R324IncomingExceptionalStopTraceAssembly κp initialScale) (t : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).R324WithinHalfAlternatingTransport) (α β : Z4) (π : ↥κp.singles ≃ ↥κm.singles) (ω : R324IncomingExceptionalRootParameter ρ lam ε κm) (u : t.final.SurvivingCoordinate → T4) : t.multiplier α * data.incomingExceptionalRefinedRootDriverCoefficient t α β π ω u = charT4 β ω.1.1 * data.incomingExceptionalRefinedRootDriverReducedCoefficient t α β π ω.1.2 ω.2 u

Stripping the outgoing character from the multiplier-weighted driver coefficient.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.norm_incomingExceptionalRefinedRootDriverReducedCoefficient_eq {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {C K : ℝ} {κp κm : PartialPairing (Fin m)} {initialScale : Fin (m + 1) → ℝ} (data : R324IncomingExceptionalStopTraceAssembly κp initialScale) (t : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).R324WithinHalfAlternatingTransport) (α β : Z4) (π : ↥κp.singles ≃ ↥κm.singles) (zw : T4 × T4) (vr : (initial ρ lam ε κm).SurvivingCoordinate → T4) (u : t.final.SurvivingCoordinate → T4) : ‖data.incomingExceptionalRefinedRootDriverReducedCoefficient t α β π zw vr u‖ = ‖t.multiplier α‖ * (paperSecondOrderModeDecay α ^ 2 * ‖incomingExceptionalPrimitiveDefect ρ lam ε (residualBlockOrder data.terminal.2) ⋯ data.stopContext.internalEdges α‖ * (|(initial ρ lam ε κm).residualIntegrand ρ ε zw.1 zw.2 ((initial ρ lam ε κm).reconstruct vr)| * |r324ResidualPrimitiveSumProduct ρ ε κp κm π (r324TwoHalfRootDoubledReconstruct t.final (initial ρ lam ε κm) (u, vr))|))

Norm of the reduced driver coefficient.

def Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.DriverTerminalJointIntegrable {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {C K : ℝ} {κp κm : PartialPairing (Fin m)} {initialScale : Fin (m + 1) → ℝ} (data : R324IncomingExceptionalStopTraceAssembly κp initialScale) (t : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).R324WithinHalfAlternatingTransport) (α β : Z4) (π : ↥κp.singles ≃ ↥κm.singles) : Prop

The gap-(a) interface: joint integrability of the driver-terminal phased density under the root measure. This is the only analytic input of the terminal y-Fourier evaluation.

Equations

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

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.norm_lamEps_pow_ambient_mul_r324RefinedPhysicalIntegral_le_budget {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {C K : ℝ} {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) {B : ℝ} (hB1 : 1 ≤ B) (hbudget : R324WithinHalfHeadCollapseBudget ρ lam ε e₀.fst α B) : |lamEps lam ε| ^ (2 * m) * ‖r324RefinedPhysicalIntegral ρ ε m α β p‖ ≤ B ^ data.suffix.length * ∫ (ω : R324IncomingExceptionalRootParameter ρ lam ε e₀.snd.fst), |lamEps lam ε| ^ (2 * (initial ρ lam ε e₀.snd.fst).remainingOrder + 2 * (R324NestedCrossResidualPrefix.initial e₀.fst e₀.snd.fst e₀.snd.snd).remainingOrder) * ‖∫ (u : (data.afterHeadAlternatingTransport hε hε1 provider).final.SurvivingCoordinate → T4), (data.afterHeadAlternatingTransport hε hε1 provider).final.incomingPhasedResidualDensity (data.incomingExceptionalRefinedRootDriverCoefficient (data.afterHeadAlternatingTransport hε hε1 provider) α β e₀.snd.snd ω u) α ρ ε 0 ω.1.1 u ∂MeasureTheory.Measure.pi fun (x : (data.afterHeadAlternatingTransport hε hε1 provider).final.SurvivingCoordinate) => paperMeasure‖ ∂r324IncomingExceptionalRootParameterMeasure ρ lam ε e₀.snd.fst

Gap (b), scalar form: the full-ambient-weight budget bound. The 2m-weighted refined physical integral is bounded by the head-collapse budget raised to the retained suffix length times the root integral of the terminal coordinate integral, with the leftover right-half and nested-cross coupling weights carried inside the root integrand.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.norm_lamEps_pow_mul_r324RefinedPhysicalIntegral_le_modeDecay {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {C K : ℝ} {initialScale : Fin (m + 1) → ℝ} (p : R324RefinedScheduleIndex m) (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentRefinedContractionFiber m ↑p.fst ↑p.snd) (data : R324IncomingExceptionalStopTraceAssembly e₀.fst initialScale) (t : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).R324WithinHalfAlternatingTransport) (hm : 0 < m) (hε : 0 < ε) (hε1 : ε ≤ 1) (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) (hjoint : data.DriverTerminalJointIntegrable t α β e₀.snd.snd) (hactive : t.final.state.active.Nonempty) (hedge : t.final.state.edges (t.final.terminalOutgoingEdgeSlot hactive) = greenFn) : ‖↑(lamEps lam ε) ^ (2 * (initial ρ lam ε e₀.fst).remainingOrder) * r324RefinedPhysicalIntegral ρ ε m α β p‖ ≤ paperSecondOrderModeDecay β * (∫ (z : T4), |greenFn z| ∂paperMeasure)⁻¹ * ∫ (q : R324IncomingExceptionalRootParameter ρ lam ε e₀.snd.fst × (t.final.SurvivingCoordinate → T4)), ‖t.final.incomingPhasedResidualDensity (t.multiplier α * data.incomingExceptionalRefinedRootDriverCoefficient t α β 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 : t.final.SurvivingCoordinate) => paperMeasure)

Gap (a) applied: the mode-decay upgrade of the driver-terminal scalar bound. Under the direct outgoing Green geometry and the joint integrability of the driver-terminal density under the root measure, the weighted refined physical integral gains the paper second-order mode decay in the outgoing mode β, at the price of the raw Green L¹ mass, against the joint L¹ mass of the driver-terminal density.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.norm_lamEps_pow_mul_r324RefinedPhysicalIntegral_le_modeDecay_of_not_shortcut {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {C K : ℝ} {initialScale : Fin (m + 1) → ℝ} (p : R324RefinedScheduleIndex m) (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentRefinedContractionFiber m ↑p.fst ↑p.snd) (data : R324IncomingExceptionalStopTraceAssembly e₀.fst initialScale) (t : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).R324WithinHalfAlternatingTransport) (hm : 0 < m) (hε : 0 < ε) (hε1 : ε ≤ 1) (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) (hjoint : data.DriverTerminalJointIntegrable t α β e₀.snd.snd) (hactive : t.final.state.active.Nonempty) (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 × (t.final.SurvivingCoordinate → T4)), ‖t.final.incomingPhasedResidualDensity (t.multiplier α * data.incomingExceptionalRefinedRootDriverCoefficient t α β 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 : t.final.SurvivingCoordinate) => paperMeasure)

Consumer form of the mode-decay upgrade: the direct-outgoing Green premise is discharged from the driver-terminal schedule completion and the boolean shortcut flag of the frozen pairing.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.norm_lamEps_pow_ambient_mul_r324RefinedPhysicalIntegral_le_modeDecay {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {C K : ℝ} {initialScale : Fin (m + 1) → ℝ} (p : R324RefinedScheduleIndex m) (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentRefinedContractionFiber m ↑p.fst ↑p.snd) (data : R324IncomingExceptionalStopTraceAssembly e₀.fst initialScale) (t : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).R324WithinHalfAlternatingTransport) (hm : 0 < m) (hε : 0 < ε) (hε1 : ε ≤ 1) (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) (hjoint : data.DriverTerminalJointIntegrable t α β e₀.snd.snd) (hactive : t.final.state.active.Nonempty) (hedge : t.final.state.edges (t.final.terminalOutgoingEdgeSlot hactive) = greenFn) : |lamEps lam ε| ^ (2 * m) * ‖r324RefinedPhysicalIntegral ρ ε m α β p‖ ≤ paperSecondOrderModeDecay β * (∫ (z : T4), |greenFn z| ∂paperMeasure)⁻¹ * ∫ (q : R324IncomingExceptionalRootParameter ρ lam ε e₀.snd.fst × (t.final.SurvivingCoordinate → T4)), |lamEps lam ε| ^ (2 * (initial ρ lam ε e₀.snd.fst).remainingOrder + 2 * (R324NestedCrossResidualPrefix.initial e₀.fst e₀.snd.fst e₀.snd.snd).remainingOrder) * ‖t.final.incomingPhasedResidualDensity (t.multiplier α * data.incomingExceptionalRefinedRootDriverCoefficient t α β 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 : t.final.SurvivingCoordinate) => paperMeasure)

Gaps (a)+(b) combined: the full-ambient-weight mode-decay bound. The 2m-weighted refined physical integral gains the outgoing mode decay, with the leftover right-half and nested-cross coupling weights carried against the joint terminal density mass.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.exists_norm_lamEps_pow_ambient_mul_r324RefinedPhysicalIntegral_le_budget {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {C K : ℝ} {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) (supportConstant primitiveConstant : ℝ) (hsupport : 0 < supportConstant) (hlog : 1 ≤ |Real.log ε|) (hsmall : |primitiveConstant * lam| ≤ 1) (huniform : ∀ (res : R324WithinHalfResidualPrefix ρ lam ε e₀.fst) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail), (∀ (j : Fin (2 * residualBlockOrder (res.headContext head tail hremaining).step.2 - 1)), Measurable ((res.headContext head tail hremaining).internalEdges j)) ∧ (∀ (j : Fin (2 * residualBlockOrder (res.headContext head tail hremaining).step.2 - 1)), MemEClassT4 ((res.headContext head tail hremaining).internalEdges j)) ∧ PrimitiveKernelBounds ρ lam ε (residualBlockOrder head.2) ⋯ (res.headContext head tail hremaining).internalEdges supportConstant primitiveConstant) : ∃ (B : ℝ), 1 ≤ B ∧ |lamEps lam ε| ^ (2 * m) * ‖r324RefinedPhysicalIntegral ρ ε m α β p‖ ≤ B ^ data.suffix.length * ∫ (ω : R324IncomingExceptionalRootParameter ρ lam ε e₀.snd.fst), |lamEps lam ε| ^ (2 * (initial ρ lam ε e₀.snd.fst).remainingOrder + 2 * (R324NestedCrossResidualPrefix.initial e₀.fst e₀.snd.fst e₀.snd.snd).remainingOrder) * ‖∫ (u : (data.afterHeadAlternatingTransport hε hε1 provider).final.SurvivingCoordinate → T4), (data.afterHeadAlternatingTransport hε hε1 provider).final.incomingPhasedResidualDensity (data.incomingExceptionalRefinedRootDriverCoefficient (data.afterHeadAlternatingTransport hε hε1 provider) α β e₀.snd.snd ω u) α ρ ε 0 ω.1.1 u ∂MeasureTheory.Measure.pi fun (x : (data.afterHeadAlternatingTransport hε hε1 provider).final.SurvivingCoordinate) => paperMeasure‖ ∂r324IncomingExceptionalRootParameterMeasure ρ lam ε e₀.snd.fst

Gaps (b)+(c) assembled. The pointwise Proposition 4.1 kernel bounds, the small-coupling regime, and the logarithmic window produce a head-collapse budget B ≥ 1 for which the full-ambient-weight refined physical bound holds.