Closing the all-order R-322 reduction

This file contains the final multi-block interfaces for paper Section 4.1. It starts with the concrete Definition 3.1 block schedule and the generalized-input terminal primitive identity. The subsequent section iterates the exact block coordinates and connects their analytic collapse to RenormFiberReductionOutput.

The concrete extraction schedule is a complete partition

theorem Anderson4D.extractionBlocksAux_forall_nonempty {m : ℕ} (κ : PartialPairing (Fin m)) (fuel : ℕ) (active : Finset (Fin m)) : List.Forall Finset.Nonempty (extractionBlocksAux κ fuel active)

theorem Anderson4D.extractionBlocks_forall_nonempty {m : ℕ} (κ : PartialPairing (Fin m)) : List.Forall Finset.Nonempty (extractionBlocks κ)

def Anderson4D.extractionPrimitiveBlockPartition {m : ℕ} (κ : PartialPairing (Fin m)) (hκ : κ.IsFull) : PrimitiveBlockPartition κ

For a full pairing, its Definition 3.1 extraction list is a complete partition by nonempty closed primitive blocks.

Equations

• Anderson4D.extractionPrimitiveBlockPartition κ hκ = { blocks := Anderson4D.extractionBlocks κ, pairwise_disjoint := ⋯, cover := ⋯, nonempty := ⋯, fullyPaired := ⋯, primitive := ⋯ }

@[simp]

theorem Anderson4D.extractionPrimitiveBlockPartition_blocks {m : ℕ} (κ : PartialPairing (Fin m)) (hκ : κ.IsFull) : (extractionPrimitiveBlockPartition κ hκ).blocks = extractionBlocks κ

theorem Anderson4D.sum_extractionBlockOrders_of_full {q : ℕ} (κ : PartialPairing (Fin (2 * q))) (hκ : κ.IsFull) : (List.map residualBlockOrder (extractionBlocks κ)).sum = q

Exact R-322 order ledger: the primitive block orders add to q.

theorem Anderson4D.extractionBlockOrder_le_truncOrder {q : ℕ} (κ : PartialPairing (Fin (2 * q))) (hκ : κ.IsFull) {B : Finset (Fin (2 * q))} (hB : B ∈ extractionBlocks κ) (ε : ℝ) (hq : q ≤ truncOrder ε) : residualBlockOrder B ≤ truncOrder ε

Every concrete R-322 primitive block lies in the global perturbative range.

Generalized-input terminal primitive identity

noncomputable def Anderson4D.detJWith (ρ : SmoothCutoff) (lam ε : ℝ) (q : ℕ) (hq : 1 ≤ q) (G : Fin (2 * q - 1) → T4 → ℝ) (σ : PartialPairing (Fin (2 * q))) (z w : T4) : ℝ

A generalized closed J kernel. Unlike detJ, its chain inputs are an arbitrary family accepted by Proposition 4.1.

Equations

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

theorem Anderson4D.detJclosedIntegrandWith_eq_primitiveIntegrand_of_full_primitive (ρ : SmoothCutoff) (ε : ℝ) (q : ℕ) (hq : 1 ≤ q) (G : Fin (2 * q - 1) → T4 → ℝ) (σ : PartialPairing (Fin (2 * q))) (hfull : σ.IsFull) (hprimitive : IsPrimitive σ) (x : Fin (2 * q) → T4) : detJclosedIntegrandWith ρ ε (2 * q) σ G x = primitiveIntegrand ρ ε q hq G σ x

On a primitive full pairing, the terminal whole-interval replacement is invalid and hence contributes 1; the generalized closed J integrand is exactly the Proposition 4.1 integrand.

theorem Anderson4D.sum_detJWith_primitive_eq_primitiveKernel (ρ : SmoothCutoff) (lam ε : ℝ) (q : ℕ) (hq : 1 ≤ q) (G : Fin (2 * q - 1) → T4 → ℝ) (z w : T4) : ∑ σ ∈ primitiveFullPairings q, detJWith ρ lam ε q hq G σ z w = primitiveKernel ρ lam ε q hq G z w

Exact terminal equality after summing the complete primitive pairing coordinate.

theorem Anderson4D.detJWith_green_eq_detJ (ρ : SmoothCutoff) (lam ε : ℝ) (q : ℕ) (hq : 1 ≤ q) (σ : PartialPairing (Fin (2 * q))) (z w : T4) : detJWith ρ lam ε q hq (fun (x : Fin (2 * q - 1)) => greenFn) σ z w = detJ ρ lam ε q σ z w

The generalized kernel specializes exactly to the frozen detJ kernel at the free Green family.