Right within-half factors in the unified R-324 partition

The right-copy blocks in the unified primitive partition are literal images of the Definition 3.1 extraction blocks under rightMomentIndex. This file identifies their canonical increasing enumerations and, consequently, their complete primitive covariance sums with the existing R-322 block sums.

Everything here is an exact signed finite-sum identity. No norm or integration is used.

The right block as an ambient partition block

theorem Anderson4D.rightExtractionBlock_image_mem_momentPrimitiveBlockPartition {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (B : ExtractionBlockIndex κm) : Finset.image rightMomentIndex ↑B ∈ (momentPrimitiveBlockPartition κp κm π).blocks

A right extraction block occurs literally in the unified primitive partition.

@[simp]

theorem Anderson4D.residualBlockOrder_image_rightMomentIndex_bridge {m : ℕ} (B : Finset (Fin m)) : residualBlockOrder (Finset.image rightMomentIndex B) = residualBlockOrder B

The perturbative order is unchanged by the right-copy embedding.

Compatibility of the canonical increasing enumerations

theorem Anderson4D.residualPrimitiveBlockOrderIso_image_rightMomentIndex_apply {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (B : ExtractionBlockIndex κm) (i : Fin (2 * residualBlockOrder (Finset.image rightMomentIndex ↑B))) : ↑((residualPrimitiveBlockOrderIso (momentCombinedPairing κp κm π) (Finset.image rightMomentIndex ↑B) ⋯) i) = rightMomentIndex ↑((residualPrimitiveBlockOrderIso κm ↑B ⋯) ((Fin.castOrderIso ⋯) i))

The canonical increasing enumeration of an image block is obtained by enumerating the original block and then applying rightMomentIndex.

The Fin.castOrderIso is the proof-relevant transport between the two definitionally different, but propositionally equal, primitive-order domains.

Equality of the complete primitive sums

@[reducible, inline]

abbrev Anderson4D.R324PrimitiveCoordinate (n : ℕ) : Type

The complete primitive-pairing coordinate type at order n.

Equations

• Anderson4D.R324PrimitiveCoordinate n = ↥(Anderson4D.primitiveFullPairings n)

def Anderson4D.r324PrimitiveCoordinateCastEquiv {a b : ℕ} (h : a = b) : R324PrimitiveCoordinate a ≃ R324PrimitiveCoordinate b

Pure equality transport of complete primitive-pairing coordinates.

Equations

• Anderson4D.r324PrimitiveCoordinateCastEquiv h = Equiv.cast ⋯

theorem Anderson4D.primitiveCovarianceProduct_castOrder_eq (ρ : SmoothCutoff) (ε : ℝ) {a b : ℕ} (h : a = b) (σ : R324PrimitiveCoordinate a) (x : Fin (2 * a) → T4) (y : Fin (2 * b) → T4) (hxy : ∀ (i : Fin (2 * a)), x i = y ((Fin.castOrderIso ⋯) i)) : primitiveCovarianceProduct ρ ε a (↑σ) x = primitiveCovarianceProduct ρ ε b (↑((r324PrimitiveCoordinateCastEquiv h) σ)) y

primitiveCovarianceProduct is compatible with equality transport of its perturbative order and the corresponding cast of tuple coordinates.

def Anderson4D.rightExtractionPrimitiveCoordinateEquiv {m : ℕ} (B : Finset (Fin m)) : ↥(primitiveFullPairings (residualBlockOrder (Finset.image rightMomentIndex B))) ≃ ↥(primitiveFullPairings (residualBlockOrder B))

Proof-only transport between the primitive-coordinate types carried by a right-copy image block and by its original extraction block.

Equations

• Anderson4D.rightExtractionPrimitiveCoordinateEquiv B = Anderson4D.r324PrimitiveCoordinateCastEquiv ⋯

theorem Anderson4D.r324PrimitivePartitionBlockSum_image_rightMomentIndex_eq {m : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (B : ExtractionBlockIndex κm) (v : Fin (2 * m) → T4) : r324PrimitivePartitionBlockSum ρ ε κp κm π (Finset.image rightMomentIndex ↑B) v = r322ExtractionBlockPrimitiveSum ρ ε κm B fun (i : Fin m) => v (rightMomentIndex i)

The complete ambient primitive-partition sum on a right-copy block is exactly the R-322 extraction-block primitive sum evaluated on the right half of the doubled coordinate tuple.