Quantitative terminal estimate for one full-pairing half

This file joins three already certified pieces of the within-half reduction without changing the order of summation and integration:

• the exact integration of the complete grouped terminal primitive block;
• the exact 𝓔-symmetry reduction of the terminal phase to a cosine, followed by the frequency-independent Step 4 loss;
• the exact proper-prefix active-scale budget.

The primitive-pairing sum remains inside terminalGroupedPrimitiveCore until its exact integration theorem is used. In particular, no absolute value is moved through that finite sum. The result is a terminal half estimate used in the four-endpoint R-324 estimate.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingBudgetTerminalAdapter.lamEps_pow_integral_terminalGroupedPrimitiveCore_eq_predecessor_mul_primitiveKernelDiff {ρ : SmoothCutoff} {C lam ε K A : ℝ} {q : ℕ} {κ : PartialPairing (Fin (2 * q))} {budget : R324FullPairingBudgetStopTrace κ} (data : R324FullPairingBudgetTerminalAdapter budget) (x z w : T4) (hint : ∀ (κB : ↥(primitiveFullPairings (residualBlockOrder data.geometry.terminalData.terminal.2))), MeasureTheory.Integrable (fun (u : Fin (2 * residualBlockOrder data.geometry.terminalData.terminal.2 - 2) → T4) => detJclosedIntegrandWith ρ ε (2 * residualBlockOrder data.geometry.terminalData.terminal.2) (↑κB) (data.geometry.trace.stopPrefix.headContext data.geometry.terminalData.terminal [] ⋯).internalEdges (primitiveAssemble (residualBlockOrder data.geometry.terminalData.terminal.2) ⋯ z w u)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder data.geometry.terminalData.terminal.2 - 2)) => paperMeasure)) : (lamEps lam ε ^ (2 * residualBlockOrder data.geometry.terminalData.terminal.2) * ∫ (u : Fin (2 * residualBlockOrder data.geometry.terminalData.terminal.2 - 2) → T4), data.geometry.terminalGroupedPrimitiveCore x (primitiveAssemble (residualBlockOrder data.geometry.terminalData.terminal.2) ⋯ z w u) ∂MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder data.geometry.terminalData.terminal.2 - 2)) => paperMeasure) = data.geometry.trace.stopPrefix.state.edges (r324WithinHalfPredecessorSlot data.geometry.trace.stopPrefix.state data.geometry.terminalData.terminal) (x - z) * primitiveKernelDiff ρ lam ε (residualBlockOrder data.geometry.terminalData.terminal.2) ⋯ (data.geometry.trace.stopPrefix.headContext data.geometry.terminalData.terminal [] ⋯).internalEdges (z - w)

Exact fixed-endpoint form of the grouped terminal integration, with the heterogeneous primitive kernel written in the gap variable used by the endpoint Fourier argument.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingBudgetTerminalAdapter.integral_lamEps_pow_terminalGroupedPrimitiveCore_gap_mul_negCharacterSubOne_eq {ρ : SmoothCutoff} {C lam ε K A : ℝ} {q : ℕ} {κ : PartialPairing (Fin (2 * q))} {budget : R324FullPairingBudgetStopTrace κ} (data : R324FullPairingBudgetTerminalAdapter budget) (x z : T4) (hint : ∀ (w : T4) (κB : ↥(primitiveFullPairings (residualBlockOrder data.geometry.terminalData.terminal.2))), MeasureTheory.Integrable (fun (v : Fin (2 * residualBlockOrder data.geometry.terminalData.terminal.2 - 2) → T4) => detJclosedIntegrandWith ρ ε (2 * residualBlockOrder data.geometry.terminalData.terminal.2) (↑κB) (data.geometry.trace.stopPrefix.headContext data.geometry.terminalData.terminal [] ⋯).internalEdges (primitiveAssemble (residualBlockOrder data.geometry.terminalData.terminal.2) ⋯ z w v)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder data.geometry.terminalData.terminal.2 - 2)) => paperMeasure)) (β : Z4) : ∫ (u : T4), ↑(lamEps lam ε ^ (2 * residualBlockOrder data.geometry.terminalData.terminal.2) * ∫ (v : Fin (2 * residualBlockOrder data.geometry.terminalData.terminal.2 - 2) → T4), data.geometry.terminalGroupedPrimitiveCore x (primitiveAssemble (residualBlockOrder data.geometry.terminalData.terminal.2) ⋯ z (z - u) v) ∂MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder data.geometry.terminalData.terminal.2 - 2)) => paperMeasure) * (charT4 (-β) u - 1) ∂paperMeasure = ↑(data.geometry.trace.stopPrefix.state.edges (r324WithinHalfPredecessorSlot data.geometry.trace.stopPrefix.state data.geometry.terminalData.terminal) (x - z)) * ∫ (u : T4), ↑(primitiveKernelDiff ρ lam ε (residualBlockOrder data.geometry.terminalData.terminal.2) ⋯ (data.geometry.trace.stopPrefix.headContext data.geometry.terminalData.terminal [] ⋯).internalEdges u) * (charT4 (-β) u - 1) ∂paperMeasure

Exact gap-integral seam. The complete signed terminal primitive sum is integrated before the endpoint phase is introduced. The predecessor edge is independent of the gap and therefore factors outside the final Bochner integral.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingBudgetTerminalAdapter.norm_integral_terminalPrimitiveKernelDiff_mul_negCharacterSubOne_le_two_mul {ρ : SmoothCutoff} {C lam ε K A : ℝ} {q : ℕ} {κ : PartialPairing (Fin (2 * q))} {budget : R324FullPairingBudgetStopTrace κ} (data : R324FullPairingBudgetTerminalAdapter budget) (hε : 0 < ε) (supportConstant primitiveConstant : ℝ) (hbound : PrimitiveKernelBounds ρ lam ε (residualBlockOrder data.geometry.terminalData.terminal.2) ⋯ (data.geometry.trace.stopPrefix.headContext data.geometry.terminalData.terminal [] ⋯).internalEdges supportConstant primitiveConstant) (β : Z4) : ‖∫ (u : T4), ↑(primitiveKernelDiff ρ lam ε (residualBlockOrder data.geometry.terminalData.terminal.2) ⋯ (data.geometry.trace.stopPrefix.headContext data.geometry.terminalData.terminal [] ⋯).internalEdges u) * (charT4 (-β) u - 1) ∂paperMeasure‖ ≤ 2 * ∫ (u : T4), primitiveKernelMajorant primitiveConstant lam ε supportConstant (residualBlockOrder data.geometry.terminalData.terminal.2) u ∂paperMeasure

The exact cosine identity and the Step 4 domination give a bound for the genuine complex phase defect, rather than only for its real part.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingBudgetTerminalAdapter.norm_integral_terminalPrimitiveKernelDiff_mul_negCharacterSubOne_le_scaled {ρ : SmoothCutoff} {C lam ε K A : ℝ} {q : ℕ} {κ : PartialPairing (Fin (2 * q))} {budget : R324FullPairingBudgetStopTrace κ} (data : R324FullPairingBudgetTerminalAdapter budget) (hε : 0 < ε) (supportConstant primitiveConstant : ℝ) (hprimitive : 0 ≤ primitiveConstant) (hlam : 0 ≤ lam) (hprop : ∀ (H : Fin (2 * residualBlockOrder data.geometry.terminalData.terminal.2 - 1) → T4 → ℝ), IsAdmissiblePrimitiveInput (residualBlockOrder data.geometry.terminalData.terminal.2) H → MemEClassT4 (primitiveKernelDiff ρ lam ε (residualBlockOrder data.geometry.terminalData.terminal.2) ⋯ H) ∧ MemEClassT4 (primitiveKernelInsertedDiff ρ lam ε (residualBlockOrder data.geometry.terminalData.terminal.2) ⋯ H) ∧ PrimitiveKernelBounds ρ lam ε (residualBlockOrder data.geometry.terminalData.terminal.2) ⋯ H supportConstant primitiveConstant) (β : Z4) : ‖∫ (u : T4), ↑(primitiveKernelDiff ρ lam ε (residualBlockOrder data.geometry.terminalData.terminal.2) ⋯ (data.geometry.trace.stopPrefix.headContext data.geometry.terminalData.terminal [] ⋯).internalEdges u) * (charT4 (-β) u - 1) ∂paperMeasure‖ ≤ 2 * r324WithinHalfInternalEdgeScaleProduct (data.geometry.trace.stopPrefix.headContext data.geometry.terminalData.terminal [] ⋯) budget.stopScale * ∫ (u : T4), primitiveKernelMajorant primitiveConstant lam ε supportConstant (residualBlockOrder data.geometry.terminalData.terminal.2) u ∂paperMeasure

Certificate-scaled Step 4 estimate for the genuine heterogeneous terminal primitive kernel.

The Proposition 4.1 input is used only on normalized admissible kernels. The raw terminal edges are normalized by their stored positive scales, so the product of those scales occurs exactly once on the right. The value at the identity is discarded through the atomless Haar measure; no pointwise bound there is assumed.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingBudgetTerminalAdapter.fullPairingHalfTerminalEstimate {ρ : SmoothCutoff} {C lam ε K A : ℝ} {q : ℕ} {κ : PartialPairing (Fin (2 * q))} {budget : R324FullPairingBudgetStopTrace κ} (data : R324FullPairingBudgetTerminalAdapter budget) (x z : T4) (hxz : x ≠ z) (hε : 0 < ε) (hε1 : ε ≤ 1) (supportConstant primitiveConstant : ℝ) (hprimitive : 0 ≤ primitiveConstant) (hlam : 0 ≤ lam) (hprop : ∀ (H : Fin (2 * residualBlockOrder data.geometry.terminalData.terminal.2 - 1) → T4 → ℝ), IsAdmissiblePrimitiveInput (residualBlockOrder data.geometry.terminalData.terminal.2) H → MemEClassT4 (primitiveKernelDiff ρ lam ε (residualBlockOrder data.geometry.terminalData.terminal.2) ⋯ H) ∧ MemEClassT4 (primitiveKernelInsertedDiff ρ lam ε (residualBlockOrder data.geometry.terminalData.terminal.2) ⋯ H) ∧ PrimitiveKernelBounds ρ lam ε (residualBlockOrder data.geometry.terminalData.terminal.2) ⋯ H supportConstant primitiveConstant) (β : Z4) : ‖∫ (u : T4), ↑(lamEps lam ε ^ (2 * residualBlockOrder data.geometry.terminalData.terminal.2) * ∫ (v : Fin (2 * residualBlockOrder data.geometry.terminalData.terminal.2 - 2) → T4), data.geometry.terminalGroupedPrimitiveCore x (primitiveAssemble (residualBlockOrder data.geometry.terminalData.terminal.2) ⋯ z (z - u) v) ∂MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder data.geometry.terminalData.terminal.2 - 2)) => paperMeasure) * (charT4 (-β) u - 1) ∂paperMeasure‖ ≤ budget.stopScale (r324WithinHalfPredecessorSlot data.geometry.trace.stopPrefix.state data.geometry.terminalData.terminal) * invSqKer (x - z) * (2 * r324WithinHalfInternalEdgeScaleProduct (data.geometry.trace.stopPrefix.headContext data.geometry.terminalData.terminal [] ⋯) budget.stopScale * ∫ (u : T4), primitiveKernelMajorant primitiveConstant lam ε supportConstant (residualBlockOrder data.geometry.terminalData.terminal.2) u ∂paperMeasure)

One-half quantitative terminal estimate. The genuine signed terminal gap integral remains unscaled on the left. On the right, the predecessor edge is charged once through its stored certificate, while the raw terminal internal edges are charged once through normalized Proposition 4.1. The outgoing Green edge is not charged here: its exact Fourier multiplier is retained by the four-endpoint routing step.