Terminal primitive block in signed R-324 phase A

When the selected primitive block is the whole current carrier there is no right gap to update. The complete primitive pairing coordinate is summed and integrated directly, producing the Proposition 4.1 primitive kernel. No r322Collapse or replacement-edge object occurs in this branch.

The whole-block integrand is the genuine primitive integrand

theorem Anderson4D.sum_terminal_detJclosedIntegrandWith_eq_primitiveIntegrand (ρ : SmoothCutoff) (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (x : Fin (2 * n) → T4) : ∑ κB : ↥(primitiveFullPairings n), detJclosedIntegrandWith ρ ε (2 * n) (↑κB) G x = ∑ κ ∈ primitiveFullPairings n, primitiveIntegrand ρ ε n hn G κ x

Pointwise, the complete terminal coordinate of generalized closed J integrands is exactly the complete Proposition 4.1 primitive-integrand sum.

Exact signed terminal integration

theorem Anderson4D.integral_sum_terminal_detJclosedIntegrandWith_eq_primitiveKernel (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (z w : T4) (hint : ∀ (κB : ↥(primitiveFullPairings n)), MeasureTheory.Integrable (fun (u : Fin (2 * n - 2) → T4) => detJclosedIntegrandWith ρ ε (2 * n) (↑κB) G (primitiveAssemble n hn z w u)) (MeasureTheory.Measure.pi fun (x : Fin (2 * n - 2)) => paperMeasure)) : (lamEps lam ε ^ (2 * n) * ∫ (u : Fin (2 * n - 2) → T4), ∑ κB : ↥(primitiveFullPairings n), detJclosedIntegrandWith ρ ε (2 * n) (↑κB) G (primitiveAssemble n hn z w u) ∂MeasureTheory.Measure.pi fun (x : Fin (2 * n - 2)) => paperMeasure) = primitiveKernel ρ lam ε n hn G z w

Exact terminal phase-A identity.

The finite primitive sum stays inside the whole-block integral. After finite-sum linearity it is exactly primitiveKernel; in particular no adjacent edge is introduced or replaced.

Direct Proposition 4.1 terminal output

theorem Anderson4D.abs_integral_sum_terminal_detJclosedIntegrandWith_le_majorant (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (orderConstant supportConstant C : ℝ) (hprop41 : Prop41BoundPredicate ρ lam ε n hn G orderConstant supportConstant C) (hreg : PrimitiveEstimateRegime n lam ε orderConstant supportConstant C) (hinput : IsAdmissiblePrimitiveInput n G) (z : T4) (hint : ∀ (κB : ↥(primitiveFullPairings n)), MeasureTheory.Integrable (fun (u : Fin (2 * n - 2) → T4) => detJclosedIntegrandWith ρ ε (2 * n) (↑κB) G (primitiveAssemble n hn z 0 u)) (MeasureTheory.Measure.pi fun (x : Fin (2 * n - 2)) => paperMeasure)) : |lamEps lam ε ^ (2 * n) * ∫ (u : Fin (2 * n - 2) → T4), ∑ κB : ↥(primitiveFullPairings n), detJclosedIntegrandWith ρ ε (2 * n) (↑κB) G (primitiveAssemble n hn z 0 u) ∂MeasureTheory.Measure.pi fun (x : Fin (2 * n - 2)) => paperMeasure| ≤ primitiveKernelMajorant C lam ε supportConstant n z

At the translated endpoint w=0, Proposition 4.1 applies directly to the terminal block produced above.