The terminal primitive block in the R-322 reduction

Paper §4.1, Step 4 ends the interval-removal loop with one primitive full pairing on the remaining generalized interval. This file closes the part of that assertion which does not yet involve previously collapsed input kernels:

• a primitive full pairing on a nonempty interval has exactly one extraction, namely the whole interval;
• its closed J integrand is literally the integrand of Proposition 4.1;
• summing over every primitive full pairing gives the primitive kernel (4.2);
• consequently Proposition 4.1 gives the exact pointwise (4.3) majorant for this terminal sum.

This is a constructive component of R-322. It does not assume RenormReductionOutput, a pointwise bound for detJ, or any form of (3.22). The remaining general R-322 step is to show that successive proper-block collapses produce admissible generalized inputs and preserve this terminal identity.

A primitive full pairing has one whole-interval extraction

theorem Anderson4D.extract_eq_singleton_whole_of_full_of_primitive {m : ℕ} {κ : PartialPairing (Fin (m + 1))} (hfull : κ.IsFull) (hprimitive : IsPrimitive κ) : extract κ = [(0, Fin.last m)]

On a nonempty carrier, the extraction list of a primitive full pairing is the singleton consisting of the two endpoints of the whole interval.

theorem Anderson4D.extract_eq_singleton_whole_of_pos_full_primitive {n : ℕ} (hn : 0 < n) {κ : PartialPairing (Fin n)} (hfull : κ.IsFull) (hprimitive : IsPrimitive κ) : extract κ = [(⟨0, hn⟩, ⟨n - 1, ⋯⟩)]

Cardinality-generic form of extract_eq_singleton_whole_of_full_of_primitive.

theorem Anderson4D.isNonSplit_of_full_of_primitive {q : ℕ} (hq : 1 ≤ q) {σ : PartialPairing (Fin (2 * q))} (hfull : σ.IsFull) (hprimitive : IsPrimitive σ) : IsNonSplit σ

A primitive full pairing belongs to the non-concatenation class used by the renormalization constant. A fully paired proper prefix would itself be a proper fully paired interval, contradicting primitivity.

theorem Anderson4D.reductionEndpointSignature_eq_primitive {q : ℕ} (hq : 1 ≤ q) {σ : PartialPairing (Fin (2 * q))} (hfull : σ.IsFull) (hprimitive : IsPrimitive σ) : reductionEndpointSignature σ = ({⟨0, ⋯⟩}, {⟨2 * q - 1, ⋯⟩})

The extraction endpoint signature of a primitive full pairing is the single whole-interval signature.

Identification with the primitive kernel

theorem Anderson4D.detJintegrand_eq_primitiveIntegrand_of_full_of_primitive (ρ : SmoothCutoff) (ε : ℝ) (q : ℕ) (hq : 1 ≤ q) (σ : PartialPairing (Fin (2 * q))) (hfull : σ.IsFull) (hprimitive : IsPrimitive σ) (x : Fin (2 * q) → T4) : detJintegrand ρ ε q σ x = primitiveIntegrand ρ ε q hq (fun (x : Fin (2 * q - 1)) => greenFn) σ x

The terminal whole-interval difference factor is 1, so the closed J integrand of a primitive full pairing is exactly the Proposition 4.1 integrand with the free Green function in every chain slot.

theorem Anderson4D.sum_detJ_primitive_eq_primitiveKernel (ρ : SmoothCutoff) (lam ε : ℝ) (q : ℕ) (hq : 1 ≤ q) (z w : T4) : ∑ σ ∈ primitiveFullPairings q, detJ ρ lam ε q σ z w = primitiveKernel ρ lam ε q hq (fun (x : Fin (2 * q - 1)) => greenFn) z w

Summing detJ over the terminal primitive pairings is exactly the primitive kernel (4.2), before translating the second endpoint to zero.

theorem Anderson4D.sum_detJ_primitive_le_primitiveKernelMajorant (ρ : SmoothCutoff) {orderConstant supportConstant C lam ε : ℝ} {q : ℕ} (hq : 1 ≤ q) (hprop41 : Prop41BoundPredicate ρ lam ε q hq (fun (x : Fin (2 * q - 1)) => greenFn) orderConstant supportConstant C) (hreg : PrimitiveEstimateRegime q lam ε orderConstant supportConstant C) (hinput : IsAdmissiblePrimitiveInput q fun (x : Fin (2 * q - 1)) => greenFn) (z : T4) : |∑ σ ∈ primitiveFullPairings q, detJ ρ lam ε q σ z 0| ≤ primitiveKernelMajorant C lam ε supportConstant q z

Proposition 4.1 supplies the exact (4.3) majorant for the terminal primitive sum in the R-322 reduction.