Fourier integration of the retained full-pairing head

For a full within-half pairing, the certified trace stops immediately before its unique terminal block. The exact geometry of that block leaves one outgoing Green difference. This file identifies that literal difference with r324OutgoingEndpointKernel and integrates the external endpoint before taking any norm.

The remaining scalar keeps the complete primitive-pairing sum grouped. Consequently these identities do not move an absolute value through the Proposition 4.1 cancellation. The later cosine reduction still has to be performed after the terminal spatial variables have been integrated into the corresponding MemEClassT4 kernel; it is deliberately not asserted pointwise for the raw primitive density here.

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingStopTraceAssembly.terminalGroupedPrimitiveCore {ρ : SmoothCutoff} {C lam ε K : ℝ} {q : ℕ} {κ : PartialPairing (Fin (2 * q))} {initialScale : Fin (2 * q + 1) → ℝ} (data : R324FullPairingStopTraceAssembly κ initialScale) (x : T4) (t : Fin (2 * residualBlockOrder data.terminalData.terminal.2) → T4) : ℝ

Everything in the retained terminal raw local density except its outgoing Green difference. In particular, the primitive-pairing sum is the complete signed finite sum and remains inside this single scalar.

Equations

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

theorem Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingStopTraceAssembly.terminal_rawLocal_translated_eq_groupedCore_mul_greenDifference {ρ : SmoothCutoff} {C lam ε K : ℝ} {q : ℕ} {κ : PartialPairing (Fin (2 * q))} {initialScale : Fin (2 * q + 1) → ℝ} (data : R324FullPairingStopTraceAssembly κ initialScale) (x y : T4) (t : Fin (2 * residualBlockOrder data.terminalData.terminal.2) → T4) : ((data.trace.stopPrefix.headContext data.terminalData.terminal [] ⋯).rawLocalIntegrand ρ ε (x - y) fun (j : Fin (2 * residualBlockOrder (data.trace.stopPrefix.headContext data.terminalData.terminal [] ⋯).step.2)) => t j - y) = data.terminalGroupedPrimitiveCore x t * (greenFn (t (primitiveLast (residualBlockOrder data.terminalData.terminal.2) ⋯) - y) - greenFn (t ⟨0, ⋯⟩ - y))

Exact real factorization of the translated terminal raw local density. The endpoint-dependent factor is literally the outgoing Green difference of paper (4.17); the predecessor kernel, internal chain, and complete primitive sum stay grouped in terminalGroupedPrimitiveCore.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingStopTraceAssembly.terminal_rawLocal_translated_eq_groupedCore_mul_outgoingKernel {ρ : SmoothCutoff} {C lam ε K : ℝ} {q : ℕ} {κ : PartialPairing (Fin (2 * q))} {initialScale : Fin (2 * q + 1) → ℝ} (data : R324FullPairingStopTraceAssembly κ initialScale) (x y : T4) (t : Fin (2 * residualBlockOrder data.terminalData.terminal.2) → T4) : ↑((data.trace.stopPrefix.headContext data.terminalData.terminal [] ⋯).rawLocalIntegrand ρ ε (x - y) fun (j : Fin (2 * residualBlockOrder (data.trace.stopPrefix.headContext data.terminalData.terminal [] ⋯).step.2)) => t j - y) = ↑(data.terminalGroupedPrimitiveCore x t) * r324OutgoingEndpointKernel (t (primitiveLast (residualBlockOrder data.terminalData.terminal.2) ⋯)) (t ⟨0, ⋯⟩) true y

Complex form of the preceding identity. It identifies the terminal outgoing factor with the existing endpoint kernel without taking a norm.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingStopTraceAssembly.integral_char_mul_terminal_rawLocal_translated {ρ : SmoothCutoff} {C lam ε K : ℝ} {q : ℕ} {κ : PartialPairing (Fin (2 * q))} {initialScale : Fin (2 * q + 1) → ℝ} (data : R324FullPairingStopTraceAssembly κ initialScale) (β : Z4) (x : T4) (t : Fin (2 * residualBlockOrder data.terminalData.terminal.2) → T4) : ∫ (y : T4), charT4 β y * ↑((data.trace.stopPrefix.headContext data.terminalData.terminal [] ⋯).rawLocalIntegrand ρ ε (x - y) fun (j : Fin (2 * residualBlockOrder (data.trace.stopPrefix.headContext data.terminalData.terminal [] ⋯).step.2)) => t j - y) ∂paperMeasure = ↑(data.terminalGroupedPrimitiveCore x t) * r324EndpointCoefficient β (t (primitiveLast (residualBlockOrder data.terminalData.terminal.2) ⋯)) (t ⟨0, ⋯⟩) true

Terminal endpoint-first identity. The external endpoint is Fourier-integrated while the predecessor factor and the complete primitive pairing sum are still signed and grouped.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingStopTraceAssembly.integral_char_mul_terminal_rawLocal_translated_eq_phaseDifference {ρ : SmoothCutoff} {C lam ε K : ℝ} {q : ℕ} {κ : PartialPairing (Fin (2 * q))} {initialScale : Fin (2 * q + 1) → ℝ} (data : R324FullPairingStopTraceAssembly κ initialScale) (β : Z4) (x : T4) (t : Fin (2 * residualBlockOrder data.terminalData.terminal.2) → T4) : ∫ (y : T4), charT4 β y * ↑((data.trace.stopPrefix.headContext data.terminalData.terminal [] ⋯).rawLocalIntegrand ρ ε (x - y) fun (j : Fin (2 * residualBlockOrder (data.trace.stopPrefix.headContext data.terminalData.terminal [] ⋯).step.2)) => t j - y) ∂paperMeasure = ↑(data.terminalGroupedPrimitiveCore x t) * (translatedGreenMode β (t (primitiveLast (residualBlockOrder data.terminalData.terminal.2) ⋯)) - translatedGreenMode β (t ⟨0, ⋯⟩))

Expanded phase-difference form of the terminal endpoint coefficient. This is still an exact identity, prior to the later 𝓔-symmetry/cosine reduction.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingStopTraceAssembly.integral_char_mul_terminal_rawLocal_translated_eq_characterDifference {ρ : SmoothCutoff} {C lam ε K : ℝ} {q : ℕ} {κ : PartialPairing (Fin (2 * q))} {initialScale : Fin (2 * q + 1) → ℝ} (data : R324FullPairingStopTraceAssembly κ initialScale) (β : Z4) (x : T4) (t : Fin (2 * residualBlockOrder data.terminalData.terminal.2) → T4) : ∫ (y : T4), charT4 β y * ↑((data.trace.stopPrefix.headContext data.terminalData.terminal [] ⋯).rawLocalIntegrand ρ ε (x - y) fun (j : Fin (2 * residualBlockOrder (data.trace.stopPrefix.headContext data.terminalData.terminal [] ⋯).step.2)) => t j - y) ∂paperMeasure = ↑(data.terminalGroupedPrimitiveCore x t) * ((charT4 β (t (primitiveLast (residualBlockOrder data.terminalData.terminal.2) ⋯)) - charT4 β (t ⟨0, ⋯⟩)) * ↑(paperSecondOrderModeDecay β))

Fully explicit character form of the exact endpoint phase difference. The Green multiplier is retained exactly; no ≤ 2 shortcut bound has been used.