Left-block compatibility for the R-324 primitive partition

The left family in the doubled primitive partition is obtained by applying leftMomentIndex to the ordinary extraction blocks of the first half. This file proves that the canonical increasing enumeration is transported by that embedding and consequently that the complete ambient block sum is literally the existing R-322 extraction-block sum.

Everything remains signed and pointwise: no norm or integration is taken.

Canonical order transport

@[simp]

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

theorem Anderson4D.r324LeftBlockOrderIso_transport {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (B : ExtractionBlockIndex κp) (himage : IsFullyPairedOn (momentCombinedPairing κp κm π) (Finset.image leftMomentIndex ↑B)) (j : Fin (2 * residualBlockOrder (Finset.image leftMomentIndex ↑B))) : ↑((residualPrimitiveBlockOrderIso (momentCombinedPairing κp κm π) (Finset.image leftMomentIndex ↑B) himage) j) = leftMomentIndex ↑((residualPrimitiveBlockOrderIso κp ↑B ⋯) ((Fin.castOrderIso ⋯) j))

The canonical increasing enumeration of an extraction block commutes with the order-preserving embedding into the left doubled copy.

Exact complete-sum compatibility

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

Every ordinary left extraction block is a block of the concrete doubled primitive partition.

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

Proof-only transport between the complete primitive-coordinate types of a left image block and its original extraction block.

Equations

• Anderson4D.leftExtractionPrimitiveCoordinateEquiv B = Anderson4D.r324PrimitiveCoordinateCastEquiv ⋯

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

The ambient complete primitive sum on a left doubled block is exactly the ordinary R-322 complete extraction-block sum on the first-half tuple.