The concrete endpoint fibre for R-322

This file connects the endpoint-signature grouping used in the statement of the deterministic renormalization bound to the exact finite fibre exposed by the primitive-block replacement engine.

The non-split filter cannot simply be discarded: doing so would enlarge a signed sum and destroy the cancellation supplied by Proposition 4.1. We therefore prove that fullness and the absence of a fully paired proper prefix are invariants of the complete reduction endpoint signature. Consequently a realized non-split endpoint fibre is exactly ReductionEndpointFiberAt, and its first primitive coordinate is exposed with no cardinality loss.

Fullness is fixed by the endpoint signature

theorem Anderson4D.isFull_of_reductionEndpointSignature_eq {m : ℕ} (κ τ : PartialPairing (Fin m)) (hκ : κ.IsFull) (hsignature : reductionEndpointSignature τ = reductionEndpointSignature κ) : τ.IsFull

If the reduction endpoint signature agrees with that of a full pairing, then the second pairing is full as well.

Fully paired intervals are fixed by the block signature

theorem Anderson4D.relIcc_min'_max'_eq_inter_Icc {m : ℕ} (B : Finset (Fin m)) (a b : Fin m) (hne : (B ∩ Finset.Icc a b).Nonempty) : relIcc B ((B ∩ Finset.Icc a b).min' hne) ((B ∩ Finset.Icc a b).max' hne) = B ∩ Finset.Icc a b

The intersection of a sparse carrier with an ordinary interval is the relative interval between the minimum and maximum points of the intersection.

theorem Anderson4D.mem_extractionBlock_of_full {m : ℕ} (κ : PartialPairing (Fin m)) (hκ : κ.IsFull) (i : Fin m) : ∃ B ∈ extractionBlocks κ, i ∈ B

On a full pairing, the concrete extraction blocks cover every index.

theorem Anderson4D.isFullyPairedOn_Icc_of_extractionBlocks_eq {m : ℕ} (κ τ : PartialPairing (Fin m)) (hκ : κ.IsFull) (hblocks : extractionBlocks τ = extractionBlocks κ) (a b : Fin m) (hIτ : IsFullyPairedOn τ (Finset.Icc a b)) : IsFullyPairedOn κ (Finset.Icc a b)

If two full pairings have the same concrete primitive blocks, every ordinary interval fully paired by the second pairing is fully paired by the first. The proof uses relative primitivity: a block which meets a fully paired interval must lie wholly inside it.

theorem Anderson4D.isFullyPairedOn_Icc_iff_of_reductionEndpointSignature_eq {m : ℕ} (κ τ : PartialPairing (Fin m)) (hκ : κ.IsFull) (hsignature : reductionEndpointSignature τ = reductionEndpointSignature κ) (a b : Fin m) : IsFullyPairedOn τ (Finset.Icc a b) ↔ IsFullyPairedOn κ (Finset.Icc a b)

Endpoint-signature equality preserves every fully paired ordinary interval, in either direction, once one (hence both) pairing is full.

The non-split filter is fixed by the endpoint signature

theorem Anderson4D.univ_filter_val_le_eq_Icc {m p : ℕ} (hp : p < m) : {i : Fin m | ↑i ≤ p} = Finset.Icc ⟨0, ⋯⟩ ⟨p, hp⟩

The paper's prefix set is an ordinary interval from zero.

theorem Anderson4D.isNonSplit_of_reductionEndpointSignature_eq {q : ℕ} (κ τ : PartialPairing (Fin (2 * q))) (hκ : IsNonSplit κ) (hsignature : reductionEndpointSignature τ = reductionEndpointSignature κ) : IsNonSplit τ

IsNonSplit is an invariant of the complete reduction endpoint signature.

Exact identification of the grouped finite sum

def Anderson4D.reductionEndpointFiberEquivNonSplitFinset {q : ℕ} (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) : ReductionEndpointFiberAt κ ≃ ↥({τ ∈ nonSplitPairings q | reductionEndpointSignature τ = reductionEndpointSignature κ})

A realized non-split endpoint fibre is exactly the complete endpoint signature fibre used by the replacement engine.

Equations

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

theorem Anderson4D.endpointFiberDetJSum_eq_fintype (ρ : SmoothCutoff) (lam ε : ℝ) {q : ℕ} (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (z : T4) : endpointFiberDetJSum ρ lam ε q (reductionEndpointSignature κ) z = ∑ τ : ReductionEndpointFiberAt κ, detJ ρ lam ε q (↑τ) z 0

The definition-level endpoint sum is a genuine Fintype sum over the complete signature fibre, with no omitted or extra pairings.

theorem Anderson4D.endpointFiberDetJSum_eq_firstBlock (ρ : SmoothCutoff) (lam ε : ℝ) {q : ℕ} (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (h : ∃ (a : Fin (2 * q)) (b : Fin (2 * q)), IsRelFullyPaired κ Finset.univ a b) (z : T4) : endpointFiberDetJSum ρ lam ε q (reductionEndpointSignature κ) z = ∑ κB : ↥(primitiveFullPairings (residualBlockOrder (selectedExtractionBlock κ Finset.univ h))), ∑ κC : ExtractionComplementFiberAt κ (2 * q - 1) Finset.univ h, detJ ρ lam ε q (↑((reductionEndpointFiberEquivBlockComplement κ h).symm (κB, κC))) z 0

First exact R-322 coordinate of the grouped kernel sum. This is the concrete bridge from endpointFiberDetJSum to a complete primitive block sum, without absolute values or multiplicity factors.