The initial residual endpoint integral after the complete nested run

The first theorem integrates the a.e. endpoint-to-run seam without changing the order in which norms are taken. The second theorem chooses every cutoff-dependent constant before the coupling, scale, pairings and traces, then combines the two within-half scale ledgers with the exact initial nested-cross order ledger.

theorem Anderson4D.weighted_norm_le_of_collapsed_endpointIntegral {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {lam ε : ℝ} {m leftOrder rightOrder crossOrder : ℕ} (horder : leftOrder + rightOrder + crossOrder = m) (term : ℂ) (f : X → ℂ) (hcollapse : ↑(lamEps lam ε) ^ (2 * (leftOrder + rightOrder)) * term = ∫ (x : X), f x ∂μ) {majorant : ℝ} (hendpoint : ∫ (x : X), lamEps lam ε ^ (2 * crossOrder) * ‖f x‖ ∂μ ≤ majorant) : |lamEps lam ε| ^ (2 * m) * ‖term‖ ≤ majorant

Pure algebraic/Fubini bridge from a signed two-half collapse equality to the endpoint-norm form consumed below. The exact order identity is the only bookkeeping input; no pointwise estimate is used here.

theorem Anderson4D.R324TwoHalfTerminalData.integral_coupling_mul_norm_initialNestedEndpointIntegratedResidualDensity_le {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} {leftRes : R324WithinHalfResidualPrefix ρ lam ε κp} {rightRes : R324WithinHalfResidualPrefix ρ lam ε κm} {leftInitialScale rightInitialScale : Fin (m + 1) → ℝ} (leftTrace : leftRes.R324WithinHalfCertifiedAnalyticTrace leftInitialScale) (rightTrace : rightRes.R324WithinHalfCertifiedAnalyticTrace rightInitialScale) (π : ↥κp.singles ≃ ↥κm.singles) (hleft : leftTrace.terminalPrefix.state.active.Nonempty) (hright : rightTrace.terminalPrefix.state.active.Nonempty) (head : R324NestedCrossBlock κp κm π) (tail : List (R324NestedCrossBlock κp κm π)) (hremaining : (R324NestedCrossResidualPrefix.initial κp κm π).remaining = head :: tail) (α β : Z4) (hlam : 0 < lam) (hε : 0 < ε) (hε1 : ε ≤ 1) (hlog : 1 ≤ |Real.log ε|) (hmtrunc : m ≤ truncOrder ε) {B supportConstant : ℝ} : let terminal := ofCertifiedTraces leftTrace rightTrace; have step := r324InitialNestedCrossStepContext κp κm π head tail hremaining; ∀ (hleftInitial : (r324LeftHalfPullback step.residual.activeCarrier).Nonempty) (hrightInitial : (r324RightHalfPullback step.residual.activeCarrier).Nonempty), (∫ (v : step.SurvivingCoordinate → T4), terminal.completeNestedRunDensity step hleftInitial hrightInitial v ∂MeasureTheory.Measure.pi fun (x : step.SurvivingCoordinate) => paperMeasure) ≤ ∫ (z : T4), primitiveInsertedMajorant B lam ε supportConstant step.residual.remainingOrder z ∂paperMeasure → (∫ (v : terminal.NestedCoordinate π → T4), lamEps lam ε ^ (2 * step.residual.remainingOrder) * ‖terminal.initialNestedEndpointIntegratedResidualDensity π hleft hright α β v‖ ∂MeasureTheory.Measure.pi fun (x : terminal.NestedCoordinate π) => paperMeasure) ≤ ((∏ edge ∈ terminal.left.activeEdgeSlots, leftTrace.terminalScale edge) * ∏ edge ∈ terminal.right.activeEdgeSlots, rightTrace.terminalScale edge) * invSqKerMass ^ 4 * ∫ (z : T4), primitiveInsertedMajorant B lam ε supportConstant step.residual.remainingOrder z ∂paperMeasure

Integrate the pointwise endpoint seam against any supplied complete-run integral estimate. This fixed-data lemma keeps the two literal terminal scale products visible for the subsequent exact order ledger.

theorem Anderson4D.exists_r324InitialResidualEndpointIntegral_le_ambientMajorant (ρ : SmoothCutoff) : ∃ (phaseSupport : ℝ) (runSupport : ℝ) (C : ℝ) (K : ℝ) (A : ℝ) (B : ℝ), 0 < phaseSupport ∧ 0 < runSupport ∧ 0 < C ∧ 0 < K ∧ 1 ≤ A ∧ 0 < B ∧ (∀ (lam ε : ℝ) (m : ℕ) (pairing : PartialPairing (Fin m)), 0 < lam → 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → m ≤ truncOrder ε → Nonempty ((R324WithinHalfResidualPrefix.initial ρ lam ε pairing).R324CompatibleAnalyticBudgetTrace fun (x : Fin (m + 1)) => A)) ∧ ∀ {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (leftData : (R324WithinHalfResidualPrefix.initial ρ lam ε κp).R324CompatibleAnalyticBudgetTrace fun (x : Fin (m + 1)) => A) (rightData : (R324WithinHalfResidualPrefix.initial ρ lam ε κm).R324CompatibleAnalyticBudgetTrace fun (x : Fin (m + 1)) => A), 0 < lam → 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → 1 ≤ m → m ≤ truncOrder ε → ∀ (hleft : leftData.analytic.terminalPrefix.state.active.Nonempty) (hright : rightData.analytic.terminalPrefix.state.active.Nonempty) (head : R324NestedCrossBlock κp κm π) (tail : List (R324NestedCrossBlock κp κm π)) (hremaining : (R324NestedCrossResidualPrefix.initial κp κm π).remaining = head :: tail) (α β : Z4), let terminal := R324TwoHalfTerminalData.ofCertifiedTraces leftData.analytic rightData.analytic; have step := r324InitialNestedCrossStepContext κp κm π head tail hremaining; (∫ (v : terminal.NestedCoordinate π → T4), lamEps lam ε ^ (2 * step.residual.remainingOrder) * ‖terminal.initialNestedEndpointIntegratedResidualDensity π hleft hright α β v‖ ∂MeasureTheory.Measure.pi fun (x : terminal.NestedCoordinate π) => paperMeasure) ≤ ∫ (z : T4), primitiveInsertedMajorant (r324TwoHalfCompleteAbsorbedBase A C K B) lam ε runSupport m z ∂paperMeasure

Cutoff-uniform residual endpoint closure. The Phase-A provider and the complete-run provider are both chosen before all scale and combinatorial data. For any two compatible traces, the endpoint integral is controlled by one inserted majorant at the ambient order.