Integrated terminal primitive block for a full pairing

The budget/geometry adapter identifies the residual state reached by the complete quantitative proper-prefix trace with the state used by the terminal Fourier geometry. This file uses that identification twice:

• the edge certificate supplies 𝓔-membership for every heterogeneous internal edge of the retained primitive block;
• integration of the signed, grouped terminal core produces one literal predecessor edge times the heterogeneous primitive kernel.

The terminal lamEps power is kept separate from the proper-prefix budget, and the complete finite primitive-pairing sum stays grouped until the exact primitive-kernel integration theorem is applied.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingBudgetTerminalAdapter.terminalInternalEdges_memE {ρ : SmoothCutoff} {C lam ε K A : ℝ} {q : ℕ} {κ : PartialPairing (Fin (2 * q))} {budget : R324FullPairingBudgetStopTrace κ} (data : R324FullPairingBudgetTerminalAdapter budget) (j : Fin (2 * residualBlockOrder (data.geometry.trace.stopPrefix.headContext data.geometry.terminalData.terminal [] ⋯).step.2 - 1)) : MemEClassT4 ((data.geometry.trace.stopPrefix.headContext data.geometry.terminalData.terminal [] ⋯).internalEdges j)

Every heterogeneous internal edge of the retained terminal primitive block belongs to the paper's symmetry class, directly from the complete budget certificate on the adapter's identified residual state.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingBudgetTerminalAdapter.lamEps_pow_integral_terminalGroupedPrimitiveCore_eq_predecessor_mul_primitiveKernel {ρ : 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) * primitiveKernel ρ lam ε (residualBlockOrder data.geometry.terminalData.terminal.2) ⋯ (data.geometry.trace.stopPrefix.headContext data.geometry.terminalData.terminal [] ⋯).internalEdges z w

Exact integrated terminal core. After integrating precisely the internal coordinates of the terminal primitive block, the grouped signed primitive-pairing density becomes the heterogeneous primitiveKernel. The remaining factor is the genuine predecessor edge evaluated from the external point to the retained first endpoint.