The outgoing-shortcut terminal Step-4 charge

This file closes the local analytic seam at a shortcut terminal block for an arbitrary partial pairing. It follows paper §4.2, Step 4 in the required order: the outgoing endpoint is Fourier-integrated exactly, the complete signed primitive sum is integrated into the ordinary primitive kernel, and only then is 𝓔 symmetry used to expose the cosine defect. The final bound therefore uses the ordinary primitiveKernelMajorant, with the paper's one ε⁻² loss for this endpoint; no inserted kernel occurs here.

No trace or routing structure is introduced. The input is precisely the existing R324ShortcutStopTraceAssembly, which leaves the terminal shortcut visible after the proper-prefix reduction.

Exact endpoint phase

theorem Anderson4D.r324EndpointCoefficient_first_sub_gap_eq_defect (k : Z4) (first gap : T4) : r324EndpointCoefficient k (first - gap) first true = ↑(paperSecondOrderModeDecay k) * charT4 k first * (charT4 (-k) gap - 1)

With the paper gap orientation u = first - last, the outgoing shortcut coefficient is the free Green multiplier times the genuine phase defect. This is an exact identity, before taking a norm.

theorem Anderson4D.R324WithinHalfStepContext.outgoingErasedTranslatedRawLocalCore_eq_predecessor_mul_completePrimitive {m : ℕ} {κ : PartialPairing (Fin m)} (ctx : R324WithinHalfStepContext κ) (ρ : SmoothCutoff) (ε : ℝ) (x : T4) (t : Fin (2 * residualBlockOrder ctx.step.2) → T4) : ctx.outgoingErasedTranslatedRawLocalCore ρ ε x t = ↑(ctx.state.edges (r324WithinHalfPredecessorSlot ctx.state ctx.step) (x - ctx.outgoingBlockFirst t)) * ↑(∑ κB : ↥(primitiveFullPairings (residualBlockOrder ctx.step.2)), detJclosedIntegrandWith ρ ε (2 * residualBlockOrder ctx.step.2) (↑κB) ctx.internalEdges t)

The core left by outgoing endpoint Fourier integration is one genuine predecessor edge times the complete signed primitive density.

theorem Anderson4D.R324WithinHalfStepContext.lamEps_pow_integral_outgoingErasedTranslatedRawLocalCore_eq {m : ℕ} {κ : PartialPairing (Fin m)} (ctx : R324WithinHalfStepContext κ) (ρ : SmoothCutoff) (lam ε : ℝ) (x first last : T4) (hint : ∀ (κB : ↥(primitiveFullPairings (residualBlockOrder ctx.step.2))), MeasureTheory.Integrable (fun (r : Fin (2 * residualBlockOrder ctx.step.2 - 2) → T4) => detJclosedIntegrandWith ρ ε (2 * residualBlockOrder ctx.step.2) (↑κB) ctx.internalEdges (primitiveAssemble (residualBlockOrder ctx.step.2) ⋯ first last r)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder ctx.step.2 - 2)) => paperMeasure)) : (↑(lamEps lam ε) ^ (2 * residualBlockOrder ctx.step.2) * ∫ (r : Fin (2 * residualBlockOrder ctx.step.2 - 2) → T4), ctx.outgoingErasedTranslatedRawLocalCore ρ ε x (primitiveAssemble (residualBlockOrder ctx.step.2) ⋯ first last r) ∂MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder ctx.step.2 - 2)) => paperMeasure) = ↑(ctx.state.edges (r324WithinHalfPredecessorSlot ctx.state ctx.step) (x - first) * primitiveKernelDiff ρ lam ε (residualBlockOrder ctx.step.2) ⋯ ctx.internalEdges (first - last))

Integrating the internal coordinates of the outgoing-erased terminal core produces the ordinary heterogeneous primitive kernel. The complete finite primitive-pairing sum remains inside the integral until this exact identity is applied.

theorem Anderson4D.R324WithinHalfStepContext.lamEps_pow_integral_terminalOutgoingFourier_internal_eq_defect {m : ℕ} {κ : PartialPairing (Fin m)} (ctx : R324WithinHalfStepContext κ) (ρ : SmoothCutoff) (lam ε : ℝ) (houtgoing : ctx.state.edges ctx.outgoingSlot = greenFn) (k : Z4) (x first gap : T4) (outer : ℂ) (hint : ∀ (κB : ↥(primitiveFullPairings (residualBlockOrder ctx.step.2))), MeasureTheory.Integrable (fun (r : Fin (2 * residualBlockOrder ctx.step.2 - 2) → T4) => detJclosedIntegrandWith ρ ε (2 * residualBlockOrder ctx.step.2) (↑κB) ctx.internalEdges (primitiveAssemble (residualBlockOrder ctx.step.2) ⋯ first (first - gap) r)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder ctx.step.2 - 2)) => paperMeasure)) : (↑(lamEps lam ε) ^ (2 * residualBlockOrder ctx.step.2) * ∫ (r : Fin (2 * residualBlockOrder ctx.step.2 - 2) → T4), ∫ (y : T4), charT4 k y * (↑(ctx.rawLocalIntegrand ρ ε (x - y) fun (j : Fin (2 * residualBlockOrder ctx.step.2)) => primitiveAssemble (residualBlockOrder ctx.step.2) ⋯ first (first - gap) r j - y) * outer) ∂paperMeasure ∂MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder ctx.step.2 - 2)) => paperMeasure) = ↑(ctx.state.edges (r324WithinHalfPredecessorSlot ctx.state ctx.step) (x - first)) * ↑(primitiveKernelDiff ρ lam ε (residualBlockOrder ctx.step.2) ⋯ ctx.internalEdges gap) * ↑(paperSecondOrderModeDecay k) * charT4 k first * (charT4 (-k) gap - 1) * outer

Fixed-first, fixed-gap form of the shortcut endpoint operation for an arbitrary stopped terminal R324WithinHalfStepContext. The y integral is performed first, then the complete signed primitive sum is integrated in the internal block coordinates.

theorem Anderson4D.R324WithinHalfStepContext.integral_lamEps_pow_terminalOutgoingFourier_gap_eq_defect {m : ℕ} {κ : PartialPairing (Fin m)} (ctx : R324WithinHalfStepContext κ) (ρ : SmoothCutoff) (lam ε : ℝ) (houtgoing : ctx.state.edges ctx.outgoingSlot = greenFn) (k : Z4) (x first : T4) (outer : ℂ) (hint : ∀ (gap : T4) (κB : ↥(primitiveFullPairings (residualBlockOrder ctx.step.2))), MeasureTheory.Integrable (fun (r : Fin (2 * residualBlockOrder ctx.step.2 - 2) → T4) => detJclosedIntegrandWith ρ ε (2 * residualBlockOrder ctx.step.2) (↑κB) ctx.internalEdges (primitiveAssemble (residualBlockOrder ctx.step.2) ⋯ first (first - gap) r)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder ctx.step.2 - 2)) => paperMeasure)) : ∫ (gap : T4), ↑(lamEps lam ε) ^ (2 * residualBlockOrder ctx.step.2) * ∫ (r : Fin (2 * residualBlockOrder ctx.step.2 - 2) → T4), ∫ (y : T4), charT4 k y * (↑(ctx.rawLocalIntegrand ρ ε (x - y) fun (j : Fin (2 * residualBlockOrder ctx.step.2)) => primitiveAssemble (residualBlockOrder ctx.step.2) ⋯ first (first - gap) r j - y) * outer) ∂paperMeasure ∂MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder ctx.step.2 - 2)) => paperMeasure ∂paperMeasure = (↑(ctx.state.edges (r324WithinHalfPredecessorSlot ctx.state ctx.step) (x - first)) * ↑(paperSecondOrderModeDecay k) * charT4 k first * ∫ (gap : T4), ↑(primitiveKernelDiff ρ lam ε (residualBlockOrder ctx.step.2) ⋯ ctx.internalEdges gap) * (charT4 (-k) gap - 1) ∂paperMeasure) * outer

After the exact endpoint and internal-coordinate operations, integrating the terminal gap leaves precisely the ordinary primitive phase defect. No absolute value has yet been taken.

theorem Anderson4D.R324WithinHalfStepContext.integral_lamEps_pow_terminalOutgoingFourier_gap_eq_cos {m : ℕ} {κ : PartialPairing (Fin m)} (ctx : R324WithinHalfStepContext κ) (ρ : SmoothCutoff) (lam ε : ℝ) (houtgoing : ctx.state.edges ctx.outgoingSlot = greenFn) (k : Z4) (x first : T4) (outer : ℂ) (hint : ∀ (gap : T4) (κB : ↥(primitiveFullPairings (residualBlockOrder ctx.step.2))), MeasureTheory.Integrable (fun (r : Fin (2 * residualBlockOrder ctx.step.2 - 2) → T4) => detJclosedIntegrandWith ρ ε (2 * residualBlockOrder ctx.step.2) (↑κB) ctx.internalEdges (primitiveAssemble (residualBlockOrder ctx.step.2) ⋯ first (first - gap) r)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder ctx.step.2 - 2)) => paperMeasure)) (hG : ∀ (j : Fin (2 * residualBlockOrder ctx.step.2 - 1)), MemEClassT4 (ctx.internalEdges j)) (hcos : MeasureTheory.Integrable (fun (gap : T4) => primitiveKernelDiff ρ lam ε (residualBlockOrder ctx.step.2) ⋯ ctx.internalEdges gap * (r324CharacterCos k gap - 1)) paperMeasure) (hsin : MeasureTheory.Integrable (fun (gap : T4) => primitiveKernelDiff ρ lam ε (residualBlockOrder ctx.step.2) ⋯ ctx.internalEdges gap * r324CharacterSin (-k) gap) paperMeasure) : ∫ (gap : T4), ↑(lamEps lam ε) ^ (2 * residualBlockOrder ctx.step.2) * ∫ (r : Fin (2 * residualBlockOrder ctx.step.2 - 2) → T4), ∫ (y : T4), charT4 k y * (↑(ctx.rawLocalIntegrand ρ ε (x - y) fun (j : Fin (2 * residualBlockOrder ctx.step.2)) => primitiveAssemble (residualBlockOrder ctx.step.2) ⋯ first (first - gap) r j - y) * outer) ∂paperMeasure ∂MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder ctx.step.2 - 2)) => paperMeasure ∂paperMeasure = (↑(ctx.state.edges (r324WithinHalfPredecessorSlot ctx.state ctx.step) (x - first)) * ↑(paperSecondOrderModeDecay k) * charT4 k first * ∫ (gap : T4), ↑(primitiveKernelDiff ρ lam ε (residualBlockOrder ctx.step.2) ⋯ ctx.internalEdges gap * (r324CharacterCos k gap - 1)) ∂paperMeasure) * outer

𝓔 symmetry is applied only after both endpoint and interval variables have been removed. The resulting kernel is the ordinary J, not the inserted J̃.

theorem Anderson4D.R324WithinHalfStepContext.norm_integral_lamEps_pow_terminalOutgoingFourier_gap_le_two_mul {m : ℕ} {κ : PartialPairing (Fin m)} (ctx : R324WithinHalfStepContext κ) (ρ : SmoothCutoff) (lam ε : ℝ) (houtgoing : ctx.state.edges ctx.outgoingSlot = greenFn) (k : Z4) (x first : T4) (outer : ℂ) (hint : ∀ (gap : T4) (κB : ↥(primitiveFullPairings (residualBlockOrder ctx.step.2))), MeasureTheory.Integrable (fun (r : Fin (2 * residualBlockOrder ctx.step.2 - 2) → T4) => detJclosedIntegrandWith ρ ε (2 * residualBlockOrder ctx.step.2) (↑κB) ctx.internalEdges (primitiveAssemble (residualBlockOrder ctx.step.2) ⋯ first (first - gap) r)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder ctx.step.2 - 2)) => paperMeasure)) (hGmeas : ∀ (j : Fin (2 * residualBlockOrder ctx.step.2 - 1)), Measurable (ctx.internalEdges j)) (hG : ∀ (j : Fin (2 * residualBlockOrder ctx.step.2 - 1)), MemEClassT4 (ctx.internalEdges j)) (supportConstant primitiveConstant : ℝ) (hε : 0 < ε) (hbound : PrimitiveKernelBounds ρ lam ε (residualBlockOrder ctx.step.2) ⋯ ctx.internalEdges supportConstant primitiveConstant) : ‖∫ (gap : T4), ↑(lamEps lam ε) ^ (2 * residualBlockOrder ctx.step.2) * ∫ (r : Fin (2 * residualBlockOrder ctx.step.2 - 2) → T4), ∫ (y : T4), charT4 k y * (↑(ctx.rawLocalIntegrand ρ ε (x - y) fun (j : Fin (2 * residualBlockOrder ctx.step.2)) => primitiveAssemble (residualBlockOrder ctx.step.2) ⋯ first (first - gap) r j - y) * outer) ∂paperMeasure ∂MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder ctx.step.2 - 2)) => paperMeasure ∂paperMeasure‖ ≤ |ctx.state.edges (r324WithinHalfPredecessorSlot ctx.state ctx.step) (x - first)| * paperSecondOrderModeDecay k * (2 * ∫ (gap : T4), primitiveKernelMajorant primitiveConstant lam ε supportConstant (residualBlockOrder ctx.step.2) gap ∂paperMeasure) * ‖outer‖

Certificate-ready numerical endpoint charge. The Fourier multiplier ⟨k⟩⁻² remains explicit and the terminal primitive block is charged by the ordinary Proposition 4.1 majorant.

theorem Anderson4D.R324WithinHalfStepContext.norm_integral_lamEps_pow_terminalOutgoingFourier_gap_le_scaled {m : ℕ} {κ : PartialPairing (Fin m)} (ctx : R324WithinHalfStepContext κ) (ρ : SmoothCutoff) (C lam ε supportConstant : ℝ) (scale : Fin (m + 1) → ℝ) (certificate : R324WithinHalfEdgeCertificate ctx.state scale) (houtgoing : ctx.state.edges ctx.outgoingSlot = greenFn) (k : Z4) (x first : T4) (outer : ℂ) (hint : ∀ (gap : T4) (κB : ↥(primitiveFullPairings (residualBlockOrder ctx.step.2))), MeasureTheory.Integrable (fun (r : Fin (2 * residualBlockOrder ctx.step.2 - 2) → T4) => detJclosedIntegrandWith ρ ε (2 * residualBlockOrder ctx.step.2) (↑κB) ctx.internalEdges (primitiveAssemble (residualBlockOrder ctx.step.2) ⋯ first (first - gap) r)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder ctx.step.2 - 2)) => paperMeasure)) (hε : 0 < ε) (hC : 0 ≤ C) (hlam : 0 ≤ lam) (hprop : ∀ (H : Fin (2 * residualBlockOrder ctx.step.2 - 1) → T4 → ℝ), IsAdmissiblePrimitiveInput (residualBlockOrder ctx.step.2) H → MemEClassT4 (primitiveKernelDiff ρ lam ε (residualBlockOrder ctx.step.2) ⋯ H) ∧ MemEClassT4 (primitiveKernelInsertedDiff ρ lam ε (residualBlockOrder ctx.step.2) ⋯ H) ∧ PrimitiveKernelBounds ρ lam ε (residualBlockOrder ctx.step.2) ⋯ H supportConstant C) : ‖∫ (gap : T4), ↑(lamEps lam ε) ^ (2 * residualBlockOrder ctx.step.2) * ∫ (r : Fin (2 * residualBlockOrder ctx.step.2 - 2) → T4), ∫ (y : T4), charT4 k y * (↑(ctx.rawLocalIntegrand ρ ε (x - y) fun (j : Fin (2 * residualBlockOrder ctx.step.2)) => primitiveAssemble (residualBlockOrder ctx.step.2) ⋯ first (first - gap) r j - y) * outer) ∂paperMeasure ∂MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder ctx.step.2 - 2)) => paperMeasure ∂paperMeasure‖ ≤ |ctx.state.edges (r324WithinHalfPredecessorSlot ctx.state ctx.step) (x - first)| * paperSecondOrderModeDecay k * (2 * r324WithinHalfInternalEdgeScaleProduct ctx scale * ∫ (gap : T4), primitiveKernelMajorant C lam ε supportConstant (residualBlockOrder ctx.step.2) gap ∂paperMeasure) * ‖outer‖

The usable certificate-scaled form of the outgoing shortcut charge. The stopped block's internal edges carry their actual inverse-square constants in certificate; Proposition 4.1 is applied only after those constants are normalized out.