Scalar norm bound for the alternating-driver endgame

The driver root instantiation transports the weighted refined physical integral to the driver-terminal phased density carrying the accumulated multiplier. This module turns that transported identity into scalar norm estimates:

• a per-stop bound for the collapsed-head factor from the ordinary Proposition 4.1 charge, packaged once as a uniform head-collapse budget;
• the multiplicative bound for the driver multiplier, proved by the same strong recursion on the remaining list that built the driver;
• the unconditional scalarization of the transported identity, with the multiplier norm pulled out of the root integral;
• the constructor discharging the integrated residual-refined interface from a per-fibre scalar bound.

theorem Anderson4D.paperSecondOrderModeDecay_le_one (k : Z4) : paperSecondOrderModeDecay k ≤ 1

The paper's Euclidean second-order bracket never exceeds one.

Per-stop bound for the collapsed-head factor

theorem Anderson4D.R324WithinHalfResidualPrefix.norm_incomingExceptionalHeadCollapseFactor_le_two_mul {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (supportConstant primitiveConstant : ℝ) (hε : 0 < ε) (hGmeas : ∀ (j : Fin (2 * residualBlockOrder (res.headContext head tail hremaining).step.2 - 1)), Measurable ((res.headContext head tail hremaining).internalEdges j)) (hG : ∀ (j : Fin (2 * residualBlockOrder (res.headContext head tail hremaining).step.2 - 1)), MemEClassT4 ((res.headContext head tail hremaining).internalEdges j)) (hbound : PrimitiveKernelBounds ρ lam ε (residualBlockOrder head.2) ⋯ (res.headContext head tail hremaining).internalEdges supportConstant primitiveConstant) (k : Z4) : ‖res.incomingExceptionalHeadCollapseFactor head tail hremaining k‖ ≤ 2 * ∫ (u : T4), primitiveKernelMajorant primitiveConstant lam ε supportConstant (residualBlockOrder head.2) u ∂paperMeasure

Per-stop factor bound. One collapsed-head factor is one paper second-order decay times one primitive Step-4 defect; the decay is at most one and the defect carries the ordinary Proposition 4.1 charge.

The uniform head-collapse budget

def Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfHeadCollapseBudget (ρ : SmoothCutoff) (lam ε : ℝ) {m : ℕ} (pairing : PartialPairing (Fin m)) (k : Z4) (B : ℝ) : Prop

Uniform per-stop budget for the alternation: every reachable residual prefix with a literal remaining head has its collapsed-head factor bounded by B.

Equations

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

theorem Anderson4D.R324WithinHalfResidualPrefix.r324WithinHalfHeadCollapseBudget_of_kernelBounds {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (supportConstant primitiveConstant B : ℝ) (hε : 0 < ε) (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) (hmaj : ∀ (n : ℕ), 1 ≤ n → 2 * ∫ (u : T4), primitiveKernelMajorant primitiveConstant lam ε supportConstant n u ∂paperMeasure ≤ B) (k : Z4) : R324WithinHalfHeadCollapseBudget ρ lam ε pairing k B

Packaged discharge of the uniform budget: pointwise Proposition 4.1 kernel bounds at every reachable head, plus one uniform bound for the order-indexed majorant integrals.

Norm of the accumulated driver multiplier

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfCertifiedAnalyticTrace.multiplier_alternatingTransport {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {res : R324WithinHalfResidualPrefix ρ lam ε pairing} {scale : Fin (m + 1) → ℝ} (trace : res.R324WithinHalfCertifiedAnalyticTrace scale) (hordinary : trace.OrdinaryAlong) (k : Z4) : (trace.alternatingTransport hordinary).multiplier k = 1

The multiplier of the all-ordinary base transport is one.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfNextExceptionalStop.multiplier_alternatingTransport {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {res : R324WithinHalfResidualPrefix ρ lam ε pairing} {scale : Fin (m + 1) → ℝ} (data : res.R324WithinHalfNextExceptionalStop scale) (hε : 0 < ε) (hε1 : ε ≤ 1) (sub : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).R324WithinHalfAlternatingTransport) (k : Z4) : (data.alternatingTransport hε hε1 sub).multiplier k = sub.multiplier k * data.trace.stopPrefix.incomingExceptionalHeadCollapseFactor data.terminal data.suffix ⋯ k

The multiplier of one composed exceptional stop gains exactly the collapsed-head factor of the retained head.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfNextExceptionalStop.norm_multiplier_alternatingTransport_le {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {res : R324WithinHalfResidualPrefix ρ lam ε pairing} {scale : Fin (m + 1) → ℝ} (data : res.R324WithinHalfNextExceptionalStop scale) (hε : 0 < ε) (hε1 : ε ≤ 1) (sub : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).R324WithinHalfAlternatingTransport) (k : Z4) {B : ℝ} (hB0 : 0 ≤ B) (hsub : ‖sub.multiplier k‖ ≤ B ^ data.suffix.length) (hfactor : ‖data.trace.stopPrefix.incomingExceptionalHeadCollapseFactor data.terminal data.suffix ⋯ k‖ ≤ B) : ‖(data.alternatingTransport hε hε1 sub).multiplier k‖ ≤ B ^ (data.suffix.length + 1)

One exceptional stop composed with a bounded transport spends one budget factor.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfAlternatingTransport.norm_of_localBlockProvider_multiplier_le {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {C K : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (provider : R324WithinHalfLocalBlockProvider ρ C lam ε K pairing) (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (scale : Fin (m + 1) → ℝ) (certificate : R324WithinHalfEdgeCertificate res.state scale) (k : Z4) {B : ℝ} (hB1 : 1 ≤ B) (hbudget : R324WithinHalfHeadCollapseBudget ρ lam ε pairing k B) : ‖(of_localBlockProvider hε hε1 provider res scale certificate).multiplier k‖ ≤ B ^ res.remaining.length

Driver multiplier bound. By the strong recursion of the driver: the base all-ordinary run has multiplier one, and each exceptional stop multiplies by one collapsed-head factor while consuming at least one remaining step, so the accumulated multiplier is bounded by the uniform head-collapse budget raised to the remaining length.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.norm_afterHeadAlternatingTransport_multiplier_le {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {C K : ℝ} {κp : PartialPairing (Fin m)} {initialScale : Fin (m + 1) → ℝ} (data : R324IncomingExceptionalStopTraceAssembly κp initialScale) (hε : 0 < ε) (hε1 : ε ≤ 1) (provider : R324WithinHalfLocalBlockProvider ρ C lam ε K κp) (k : Z4) {B : ℝ} (hB1 : 1 ≤ B) (hbudget : R324WithinHalfHeadCollapseBudget ρ lam ε κp k B) : ‖(data.afterHeadAlternatingTransport hε hε1 provider).multiplier k‖ ≤ B ^ data.suffix.length

The multiplier of the provider-built after-head transport spends at most one budget factor per retained suffix step.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.norm_lamEps_pow_mul_r324RefinedPhysicalIntegral_le {ρ : 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) : ‖↑(lamEps lam ε) ^ (2 * (initial ρ lam ε e₀.fst).remainingOrder) * r324RefinedPhysicalIntegral ρ ε m α β p‖ ≤ ‖t.multiplier α‖ * ∫ (ω : R324IncomingExceptionalRootParameter ρ lam ε e₀.snd.fst), ‖∫ (u : t.final.SurvivingCoordinate → T4), t.final.incomingPhasedResidualDensity (data.incomingExceptionalRefinedRootDriverCoefficient t α β e₀.snd.snd ω u) α ρ ε 0 ω.1.1 u ∂MeasureTheory.Measure.pi fun (x : t.final.SurvivingCoordinate) => paperMeasure‖ ∂r324IncomingExceptionalRootParameterMeasure ρ lam ε e₀.snd.fst

Unconditional scalarization of the driver-terminal identity. The norm of the weighted refined physical integral is bounded by the norm of the accumulated driver multiplier times the root integral of the norm of the terminal coordinate integral carrying the collapsed-head refined coefficient alone.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.norm_lamEps_pow_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 * (initial ρ lam ε e₀.fst).remainingOrder) * r324RefinedPhysicalIntegral ρ ε m α β p‖ ≤ B ^ data.suffix.length * ∫ (ω : R324IncomingExceptionalRootParameter ρ lam ε e₀.snd.fst), ‖∫ (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

Scalar bound with the budgeted multiplier. The transported 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 of the collapsed-head refined coefficient.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.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) : ‖data.incomingExceptionalRefinedRootDriverCoefficient t α β π ω u‖ = paperSecondOrderModeDecay α ^ 2 * ‖incomingExceptionalPrimitiveDefect ρ lam ε (residualBlockOrder data.terminal.2) ⋯ data.stopContext.internalEdges α‖ * (|(initial ρ lam ε κm).residualIntegrand ρ ε ω.1.2.1 ω.1.2.2 ((initial ρ lam ε κm).reconstruct ω.2)| * |r324ResidualPrimitiveSumProduct ρ ε κp κm π (r324TwoHalfRootDoubledReconstruct t.final (initial ρ lam ε κm) (u, ω.2))|)

Norm of the collapsed-head refined driver coefficient: the character factors are unimodular, leaving the squared decay, the Step-4 defect charge, and the untouched right initial residual times the cross-cut primitive factor.

Terminal scalar form of the phased density

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

At a terminal prefix with nonempty active carrier, the norm of the phased density is the coefficient norm times the surviving signed chain magnitude.

theorem Anderson4D.R324WithinHalfResidualPrefix.norm_terminal_incomingPhasedResidualDensity_of_active_empty {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hnil : res.remaining = []) (hempty : res.state.active = ∅) (coefficient : ℂ) (k : Z4) (ρ' : SmoothCutoff) (ε' : ℝ) (x y : T4) (v : res.SurvivingCoordinate → T4) : ‖res.incomingPhasedResidualDensity coefficient k ρ' ε' x y v‖ = ‖coefficient‖

Degenerate terminal scalar form: with an empty active carrier the density norm is the coefficient norm.

theorem Anderson4D.R324WithinHalfResidualPrefix.norm_integral_terminal_incomingPhasedResidualDensity_le {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hnil : res.remaining = []) (hactive : res.state.active.Nonempty) (coefficient : (res.SurvivingCoordinate → T4) → ℂ) (k : Z4) (ρ' : SmoothCutoff) (ε' : ℝ) (x y : T4) : ‖∫ (v : res.SurvivingCoordinate → T4), res.incomingPhasedResidualDensity (coefficient v) k ρ' ε' x y v ∂MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure‖ ≤ ∫ (v : res.SurvivingCoordinate → T4), ‖coefficient v‖ * |res.outgoingBoundaryFactor hactive x y (res.reconstruct v) * res.endpointErasedSignedChain hactive x y (res.reconstruct v)| ∂MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure

Terminal scalar majorization of the coordinate integral. The norm of the terminal coordinate integral is unconditionally bounded by the integral of the coefficient norm weighted by the surviving signed chain magnitude.

Producer for the integrated residual-refined interface

theorem Anderson4D.norm_lamEps_pow_mul_eq_abs_pow_mul_norm (lam ε : ℝ) (N : ℕ) (I : ℂ) : ‖↑(lamEps lam ε) ^ N * I‖ = |lamEps lam ε| ^ N * ‖I‖

Norm bridge between the complex-weighted driver output and the real scalar interface consumed by the branch summation.

theorem Anderson4D.momentRefinedIntegratedReductionData_of_refinedPhysicalIntegral_bound {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {α β : Z4} {primitiveConstant supportConstant : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (h : ∀ (p : R324RefinedScheduleIndex m), |lamEps lam ε| ^ (2 * m) * ‖r324RefinedPhysicalIntegral ρ ε m α β p‖ ≤ ∫ (z : T4), primitiveInsertedMajorant primitiveConstant lam ε supportConstant m z ∂paperMeasure) : MomentRefinedIntegratedReductionData ρ lam ε m α β primitiveConstant supportConstant

Constructor for the integrated residual-refined interface. A scalar bound for every genuine refined physical integral, at the full 2m weight and against the integrated inserted majorant, discharges MomentRefinedIntegratedReductionData.refined_bound exactly.