The full-pairing terminal primitive kernel and its cosine seam

The endpoint Fourier identity leaves a complete, signed primitive-pairing density on the retained terminal block. This file performs the next two exact operations from paper §4.2 Step 1:

• the terminal internal variables are integrated while the complete finite pairing sum remains inside the integral, producing the genuine heterogeneous primitiveKernel;
• after translation to the endpoint gap, membership in the paper's class 𝓔 kills the odd character component under the integral and leaves the real character cosine minus one.

No pointwise sine cancellation is asserted. The cosine theorem carries the two precise real integrability assumptions needed for Bochner linearity; proving them from the reachable edge certificate is a separate analytic step.

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

The complete signed density on the retained terminal block, expressed with the generalized closed integrand. For primitive full pairings this is exactly the standard primitive density; the formulation is chosen so finite-sum Fubini feeds directly into the production terminal-collapse theorem.

Equations

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

theorem Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingStopTraceAssembly.terminalCompletePrimitiveDensity_eq_sum_primitiveIntegrand {ρ : SmoothCutoff} {C lam ε K : ℝ} {q : ℕ} {κ : PartialPairing (Fin (2 * q))} {initialScale : Fin (2 * q + 1) → ℝ} (data : R324FullPairingStopTraceAssembly κ initialScale) (t : Fin (2 * residualBlockOrder data.terminalData.terminal.2) → T4) : data.terminalCompletePrimitiveDensity t = ∑ κB ∈ primitiveFullPairings (residualBlockOrder data.terminalData.terminal.2), primitiveIntegrand ρ ε (residualBlockOrder data.terminalData.terminal.2) ⋯ (data.trace.stopPrefix.headContext data.terminalData.terminal [] ⋯).internalEdges κB t

The generalized terminal density is literally the complete standard primitive-pairing sum.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingStopTraceAssembly.terminalGroupedPrimitiveCore_eq_predecessor_mul_completeDensity {ρ : 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) : data.terminalGroupedPrimitiveCore x t = data.trace.stopPrefix.state.edges (r324WithinHalfPredecessorSlot data.trace.stopPrefix.state data.terminalData.terminal) (x - t ⟨0, ⋯⟩) * data.terminalCompletePrimitiveDensity t

The scalar left by endpoint Fourier integration is one genuine predecessor edge times the complete terminal primitive density.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingStopTraceAssembly.lamEps_pow_integral_terminalCompletePrimitiveDensity_eq_primitiveKernel {ρ : SmoothCutoff} {C lam ε K : ℝ} {q : ℕ} {κ : PartialPairing (Fin (2 * q))} {initialScale : Fin (2 * q + 1) → ℝ} (data : R324FullPairingStopTraceAssembly κ initialScale) (z w : T4) (hint : ∀ (κB : ↥(primitiveFullPairings (residualBlockOrder data.terminalData.terminal.2))), MeasureTheory.Integrable (fun (u : Fin (2 * residualBlockOrder data.terminalData.terminal.2 - 2) → T4) => detJclosedIntegrandWith ρ ε (2 * residualBlockOrder data.terminalData.terminal.2) (↑κB) (data.trace.stopPrefix.headContext data.terminalData.terminal [] ⋯).internalEdges (primitiveAssemble (residualBlockOrder data.terminalData.terminal.2) ⋯ z w u)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder data.terminalData.terminal.2 - 2)) => paperMeasure)) : (lamEps lam ε ^ (2 * residualBlockOrder data.terminalData.terminal.2) * ∫ (u : Fin (2 * residualBlockOrder data.terminalData.terminal.2 - 2) → T4), data.terminalCompletePrimitiveDensity (primitiveAssemble (residualBlockOrder data.terminalData.terminal.2) ⋯ z w u) ∂MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder data.terminalData.terminal.2 - 2)) => paperMeasure) = primitiveKernel ρ lam ε (residualBlockOrder data.terminalData.terminal.2) ⋯ (data.trace.stopPrefix.headContext data.terminalData.terminal [] ⋯).internalEdges z w

Exact terminal-kernel integration. The complete pairing sum is integrated as one grouped density and becomes the heterogeneous primitiveKernel on the two retained endpoints.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingStopTraceAssembly.terminalPrimitiveKernel_eq_diff {ρ : SmoothCutoff} {C lam ε K : ℝ} {q : ℕ} {κ : PartialPairing (Fin (2 * q))} {initialScale : Fin (2 * q + 1) → ℝ} (data : R324FullPairingStopTraceAssembly κ initialScale) (z w : T4) : primitiveKernel ρ lam ε (residualBlockOrder data.terminalData.terminal.2) ⋯ (data.trace.stopPrefix.headContext data.terminalData.terminal [] ⋯).internalEdges z w = primitiveKernelDiff ρ lam ε (residualBlockOrder data.terminalData.terminal.2) ⋯ (data.trace.stopPrefix.headContext data.terminalData.terminal [] ⋯).internalEdges (z - w)

The terminal heterogeneous primitive kernel depends only on its endpoint gap.

Odd-character cancellation under 𝓔 symmetry

noncomputable def Anderson4D.r324CharacterCos (β : Z4) (u : T4) : ℝ

The real and odd parts of a torus character. The first is the coordinate-free formal representative of cos(β · u), avoiding any choice of lift at the torus cut.

Equations

• Anderson4D.r324CharacterCos β u = (Anderson4D.charT4 β u).re

noncomputable def Anderson4D.r324CharacterSin (β : Z4) (u : T4) : ℝ

Equations

• Anderson4D.r324CharacterSin β u = (Anderson4D.charT4 β u).im

@[simp]

theorem Anderson4D.r324CharacterCos_neg_argument (β : Z4) (u : T4) : r324CharacterCos β (-u) = r324CharacterCos β u

@[simp]

theorem Anderson4D.r324CharacterSin_neg_argument (β : Z4) (u : T4) : r324CharacterSin β (-u) = -r324CharacterSin β u

@[simp]

theorem Anderson4D.r324CharacterCos_neg_frequency (β : Z4) (u : T4) : r324CharacterCos (-β) u = r324CharacterCos β u

theorem Anderson4D.integral_memEClass_mul_r324CharacterSin_eq_zero {J : T4 → ℝ} (hJ : MemEClassT4 J) (β : Z4) (_hint : MeasureTheory.Integrable (fun (u : T4) => J u * r324CharacterSin β u) paperMeasure) : ∫ (u : T4), J u * r324CharacterSin β u ∂paperMeasure = 0

The sine component of a character has zero integral against an 𝓔-kernel. Cancellation is obtained by the measure-preserving involution u ↦ -u; it is not a pointwise assertion.

theorem Anderson4D.integral_memEClass_mul_characterSubOne_eq_cos {J : T4 → ℝ} (hJ : MemEClassT4 J) (β : Z4) (hcos : MeasureTheory.Integrable (fun (u : T4) => J u * (r324CharacterCos β u - 1)) paperMeasure) (hsin : MeasureTheory.Integrable (fun (u : T4) => J u * r324CharacterSin β u) paperMeasure) : ∫ (u : T4), ↑(J u) * (charT4 β u - 1) ∂paperMeasure = ∫ (u : T4), ↑(J u * (r324CharacterCos β u - 1)) ∂paperMeasure

Cosine seam. Under an 𝓔-kernel the integrated phase difference is real and equals the same integral with the literal factor Re(e^{iβ·u}) - 1 = cos(β·u) - 1.

The separate cosine and sine integrability assumptions are exactly what is used by integral_add; in particular this theorem does not exploit the junk value of a non-integrable Bochner integral.

theorem Anderson4D.integral_terminalPrimitiveKernelDiff_mul_negCharacterSubOne_eq_cos (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (hG : ∀ (j : Fin (2 * n - 1)), MemEClassT4 (G j)) (β : Z4) (hcos : MeasureTheory.Integrable (fun (u : T4) => primitiveKernelDiff ρ lam ε n hn G u * (r324CharacterCos β u - 1)) paperMeasure) (hsin : MeasureTheory.Integrable (fun (u : T4) => primitiveKernelDiff ρ lam ε n hn G u * r324CharacterSin (-β) u) paperMeasure) : ∫ (u : T4), ↑(primitiveKernelDiff ρ lam ε n hn G u) * (charT4 (-β) u - 1) ∂paperMeasure = ∫ (u : T4), ↑(primitiveKernelDiff ρ lam ε n hn G u * (r324CharacterCos β u - 1)) ∂paperMeasure

Terminal specialization in the exact gap orientation left by charT4 β w - charT4 β z: after factoring charT4 β z, the gap phase is charT4 (-β) (z-w) - 1, whose real part is the same cosine.