The doubled pairing behind the deterministic moment expansion

Paper §4.2 combines the two within-copy partial pairings and the bijection between their single sets into one full pairing of the doubled carrier. This file constructs that pairing explicitly. It is the combinatorial input required before the R-322 interval reducer can be reused for R-324.

def Anderson4D.momentCombinedSumMap {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : Fin m ⊕ Fin m → Fin m ⊕ Fin m

The involution on the disjoint union of the two copies. Paired indices stay in their own copy; single indices are joined across the two copies using π.

Equations

• Anderson4D.momentCombinedSumMap κp κm π (Sum.inl i) = if hi : i ∈ κp.singles then Sum.inr ↑(π ⟨i, hi⟩) else Sum.inl (κp i)
• Anderson4D.momentCombinedSumMap κp κm π (Sum.inr j) = if hj : j ∈ κm.singles then Sum.inl ↑(π.symm ⟨j, hj⟩) else Sum.inr (κm j)

theorem Anderson4D.momentCombinedSumMap_involutive {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : Function.Involutive (momentCombinedSumMap κp κm π)

def Anderson4D.momentCombinedSumPairing {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : PartialPairing (Fin m ⊕ Fin m)

The combined pairing before identifying the disjoint union with Fin (2m).

Equations

• Anderson4D.momentCombinedSumPairing κp κm π = { toFun := Anderson4D.momentCombinedSumMap κp κm π, involutive := ⋯ }

def Anderson4D.momentDoubleFinEquiv (m : ℕ) : Fin m ⊕ Fin m ≃ Fin (2 * m)

Order-preserving identification of the left and right copies with the two consecutive halves of Fin (2m).

Equations

• Anderson4D.momentDoubleFinEquiv m = finSumFinEquiv.trans (finCongr ⋯)

@[simp]

theorem Anderson4D.momentDoubleFinEquiv_apply_inl {m : ℕ} (i : Fin m) : (momentDoubleFinEquiv m) (Sum.inl i) = leftMomentIndex i

@[simp]

theorem Anderson4D.momentDoubleFinEquiv_apply_inr {m : ℕ} (j : Fin m) : (momentDoubleFinEquiv m) (Sum.inr j) = rightMomentIndex j

@[simp]

theorem Anderson4D.momentDoubleFinEquiv_symm_leftMomentIndex {m : ℕ} (i : Fin m) : (momentDoubleFinEquiv m).symm (leftMomentIndex i) = Sum.inl i

@[simp]

theorem Anderson4D.momentDoubleFinEquiv_symm_rightMomentIndex {m : ℕ} (j : Fin m) : (momentDoubleFinEquiv m).symm (rightMomentIndex j) = Sum.inr j

def Anderson4D.momentCombinedPairing {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : PartialPairing (Fin (2 * m))

The full pairing of the doubled carrier described between paper (4.16) and (4.18).

Equations

• Anderson4D.momentCombinedPairing κp κm π = (Anderson4D.PartialPairing.congr (Anderson4D.momentDoubleFinEquiv m)) (Anderson4D.momentCombinedSumPairing κp κm π)

theorem Anderson4D.momentCombinedSumPairing_isFull {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : (momentCombinedSumPairing κp κm π).IsFull

theorem Anderson4D.momentCombinedPairing_isFull {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : (momentCombinedPairing κp κm π).IsFull

Every contraction triple produces a full pairing, even though the two within-copy pairings may have singles.

Evaluation on the two copies

@[simp]

theorem Anderson4D.momentCombinedPairing_left_single {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (i : Fin m) (hi : i ∈ κp.singles) : (momentCombinedPairing κp κm π) (leftMomentIndex i) = rightMomentIndex ↑(π ⟨i, hi⟩)

@[simp]

theorem Anderson4D.momentCombinedPairing_left_pair {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (i : Fin m) (hi : i ∉ κp.singles) : (momentCombinedPairing κp κm π) (leftMomentIndex i) = leftMomentIndex (κp i)

@[simp]

theorem Anderson4D.momentCombinedPairing_right_single {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (j : Fin m) (hj : j ∈ κm.singles) : (momentCombinedPairing κp κm π) (rightMomentIndex j) = leftMomentIndex ↑(π.symm ⟨j, hj⟩)

@[simp]

theorem Anderson4D.momentCombinedPairing_right_pair {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (j : Fin m) (hj : j ∉ κm.singles) : (momentCombinedPairing κp κm π) (rightMomentIndex j) = rightMomentIndex (κm j)

Lower-endpoint classification

@[simp]

theorem Anderson4D.leftMomentIndex_lt_leftMomentIndex_iff {m : ℕ} (i j : Fin m) : leftMomentIndex i < leftMomentIndex j ↔ i < j

@[simp]

theorem Anderson4D.rightMomentIndex_lt_rightMomentIndex_iff {m : ℕ} (i j : Fin m) : rightMomentIndex i < rightMomentIndex j ↔ i < j

@[simp]

theorem Anderson4D.leftMomentIndex_lt_rightMomentIndex {m : ℕ} (i j : Fin m) : leftMomentIndex i < rightMomentIndex j

@[simp]

theorem Anderson4D.not_rightMomentIndex_lt_leftMomentIndex {m : ℕ} (i j : Fin m) : ¬rightMomentIndex i < leftMomentIndex j

theorem Anderson4D.leftMomentIndex_lt_combined_iff {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (i : Fin m) : leftMomentIndex i < (momentCombinedPairing κp κm π) (leftMomentIndex i) ↔ i ∈ κp.singles ∨ i ∉ κp.singles ∧ i < κp i

A left-copy index is the lower endpoint either of its within-copy pair or, when it is single in κp, of its cross-copy pair.

theorem Anderson4D.rightMomentIndex_lt_combined_iff {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (j : Fin m) : rightMomentIndex j < (momentCombinedPairing κp κm π) (rightMomentIndex j) ↔ j ∉ κm.singles ∧ j < κm j

A right-copy index is a lower endpoint precisely when it is the lower endpoint of a within-right-copy pair. Cross pairs are already counted from their left-copy endpoints.

Lower-endpoint finset decomposition

def Anderson4D.momentCombinedLowerEndpoints {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : Finset (Fin (2 * m))

Equations

• Anderson4D.momentCombinedLowerEndpoints κp κm π = {i ∈ (Anderson4D.momentCombinedPairing κp κm π).pairSupport | i < (Anderson4D.momentCombinedPairing κp κm π) i}

def Anderson4D.leftMomentPairLowerEndpoints {m : ℕ} (κp : PartialPairing (Fin m)) : Finset (Fin (2 * m))

Equations

• Anderson4D.leftMomentPairLowerEndpoints κp = Finset.image Anderson4D.leftMomentIndex ({i ∈ κp.pairSupport | i < κp i})

def Anderson4D.rightMomentPairLowerEndpoints {m : ℕ} (κm : PartialPairing (Fin m)) : Finset (Fin (2 * m))

Equations

• Anderson4D.rightMomentPairLowerEndpoints κm = Finset.image Anderson4D.rightMomentIndex ({j ∈ κm.pairSupport | j < κm j})

def Anderson4D.momentCrossLowerEndpoints {m : ℕ} (κp : PartialPairing (Fin m)) : Finset (Fin (2 * m))

Equations

• Anderson4D.momentCrossLowerEndpoints κp = Finset.image Anderson4D.leftMomentIndex κp.singles

theorem Anderson4D.leftMomentIndex_injective {m : ℕ} : Function.Injective leftMomentIndex

theorem Anderson4D.rightMomentIndex_injective {m : ℕ} : Function.Injective rightMomentIndex

Fully paired sets embedded in either half

theorem Anderson4D.IsFullyPairedOn.image_leftMomentIndex {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} {B : Finset (Fin m)} (hB : IsFullyPairedOn κp B) : IsFullyPairedOn (momentCombinedPairing κp κm π) (Finset.image leftMomentIndex B)

A fully paired set in the left copy remains fully paired for the combined doubled pairing. In particular, every interval extracted from κp in paper §4.2 Step 2 is a legitimate primitive block of the combined contraction pairing.

theorem Anderson4D.IsFullyPairedOn.image_rightMomentIndex {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} {B : Finset (Fin m)} (hB : IsFullyPairedOn κm B) : IsFullyPairedOn (momentCombinedPairing κp κm π) (Finset.image rightMomentIndex B)

Right-copy counterpart of IsFullyPairedOn.image_leftMomentIndex.

theorem Anderson4D.image_leftMomentIndex_relIcc {m : ℕ} (active : Finset (Fin m)) (a b : Fin m) : Finset.image leftMomentIndex (relIcc active a b) = relIcc (Finset.image leftMomentIndex active) (leftMomentIndex a) (leftMomentIndex b)

Relative intervals commute with the order-preserving left-copy embedding into the doubled carrier.

theorem Anderson4D.image_rightMomentIndex_relIcc {m : ℕ} (active : Finset (Fin m)) (a b : Fin m) : Finset.image rightMomentIndex (relIcc active a b) = relIcc (Finset.image rightMomentIndex active) (rightMomentIndex a) (rightMomentIndex b)

Relative intervals commute with the order-preserving right-copy embedding into the doubled carrier.

theorem Anderson4D.IsRelFullyPaired.image_leftMomentIndex {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} {active : Finset (Fin m)} {a b : Fin m} (h : IsRelFullyPaired κp active a b) : IsRelFullyPaired (momentCombinedPairing κp κm π) (Finset.image leftMomentIndex active) (leftMomentIndex a) (leftMomentIndex b)

A relative fully paired interval selected in the left copy is still a relative fully paired interval of the combined pairing on the embedded active carrier.

theorem Anderson4D.IsRelFullyPaired.image_rightMomentIndex {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} {active : Finset (Fin m)} {a b : Fin m} (h : IsRelFullyPaired κm active a b) : IsRelFullyPaired (momentCombinedPairing κp κm π) (Finset.image rightMomentIndex active) (rightMomentIndex a) (rightMomentIndex b)

Right-copy counterpart of IsRelFullyPaired.image_leftMomentIndex.

theorem Anderson4D.not_mem_singles_of_combined_mem_image_left {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} {B : Finset (Fin m)} {i : Fin m} (hi : (momentCombinedPairing κp κm π) (leftMomentIndex i) ∈ Finset.image leftMomentIndex B) : i ∉ κp.singles

If the combined image of a left-copy index stays in a left-image set, then that index was not a single.

theorem Anderson4D.not_mem_singles_of_combined_mem_image_right {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} {B : Finset (Fin m)} {j : Fin m} (hj : (momentCombinedPairing κp κm π) (rightMomentIndex j) ∈ Finset.image rightMomentIndex B) : j ∉ κm.singles

Right-copy counterpart of not_mem_singles_of_combined_mem_image_left.

theorem Anderson4D.IsFullyPairedOn.of_image_leftMomentIndex {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} {B : Finset (Fin m)} (hB : IsFullyPairedOn (momentCombinedPairing κp κm π) (Finset.image leftMomentIndex B)) : IsFullyPairedOn κp B

Full pairing on an embedded left-copy set reflects back to the original partial pairing.

theorem Anderson4D.IsFullyPairedOn.of_image_rightMomentIndex {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} {B : Finset (Fin m)} (hB : IsFullyPairedOn (momentCombinedPairing κp κm π) (Finset.image rightMomentIndex B)) : IsFullyPairedOn κm B

Full pairing on an embedded right-copy set reflects back to the original partial pairing.

theorem Anderson4D.isRelFullyPaired_image_leftMomentIndex_iff {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} {active : Finset (Fin m)} {a b : Fin m} : IsRelFullyPaired (momentCombinedPairing κp κm π) (Finset.image leftMomentIndex active) (leftMomentIndex a) (leftMomentIndex b) ↔ IsRelFullyPaired κp active a b

Exact left-copy reflection principle for relative fully paired intervals.

theorem Anderson4D.isRelFullyPaired_image_rightMomentIndex_iff {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} {active : Finset (Fin m)} {a b : Fin m} : IsRelFullyPaired (momentCombinedPairing κp κm π) (Finset.image rightMomentIndex active) (rightMomentIndex a) (rightMomentIndex b) ↔ IsRelFullyPaired κm active a b

Exact right-copy reflection principle for relative fully paired intervals.

The doubled residual carrier after within-half reduction

def Anderson4D.momentResidualActive {m : ℕ} (κp κm : PartialPairing (Fin m)) : Finset (Fin (2 * m))

The active carrier left after running Definition 3.1 separately in the two copies, embedded into the doubled order.

Equations

• Anderson4D.momentResidualActive κp κm = Finset.image Anderson4D.leftMomentIndex (Anderson4D.finalActive κp) ∪ Finset.image Anderson4D.rightMomentIndex (Anderson4D.finalActive κm)

theorem Anderson4D.momentResidualActive_isFullyPairedOn {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : IsFullyPairedOn (momentCombinedPairing κp κm π) (momentResidualActive κp κm)

The within-half extraction removes only closed paired blocks. Consequently the remaining within-copy pairs stay inside the residual carrier, while every surviving single is joined by π to a surviving single in the other half. Thus the combined pairing is full on the residual doubled carrier.

theorem Anderson4D.disjoint_leftMomentPair_rightMomentPair {m : ℕ} (κp κm : PartialPairing (Fin m)) : Disjoint (leftMomentPairLowerEndpoints κp) (rightMomentPairLowerEndpoints κm)

theorem Anderson4D.disjoint_leftMomentPair_cross {m : ℕ} (κp : PartialPairing (Fin m)) : Disjoint (leftMomentPairLowerEndpoints κp) (momentCrossLowerEndpoints κp)

theorem Anderson4D.disjoint_rightMomentPair_cross {m : ℕ} (κm κp : PartialPairing (Fin m)) : Disjoint (rightMomentPairLowerEndpoints κm) (momentCrossLowerEndpoints κp)

theorem Anderson4D.momentCombinedLowerEndpoints_eq {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : momentCombinedLowerEndpoints κp κm π = leftMomentPairLowerEndpoints κp ∪ rightMomentPairLowerEndpoints κm ∪ momentCrossLowerEndpoints κp

The lower endpoints of the doubled full pairing split into the within-left, within-right, and cross-copy classes.

theorem Anderson4D.prod_momentCombinedLowerEndpoints {M : Type u_1} [CommMonoid M] {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (f : Fin (2 * m) → M) : ∏ a ∈ momentCombinedLowerEndpoints κp κm π, f a = ((∏ a ∈ leftMomentPairLowerEndpoints κp, f a) * ∏ a ∈ rightMomentPairLowerEndpoints κm, f a) * ∏ a ∈ momentCrossLowerEndpoints κp, f a

Product form of the three-way lower-endpoint partition.

theorem Anderson4D.prod_leftMomentPairLowerEndpoints {M : Type u_1} [CommMonoid M] {m : ℕ} (κp : PartialPairing (Fin m)) (f : Fin (2 * m) → M) : ∏ a ∈ leftMomentPairLowerEndpoints κp, f a = ∏ i ∈ κp.pairSupport with i < κp i, f (leftMomentIndex i)

theorem Anderson4D.prod_rightMomentPairLowerEndpoints {M : Type u_1} [CommMonoid M] {m : ℕ} (κm : PartialPairing (Fin m)) (f : Fin (2 * m) → M) : ∏ a ∈ rightMomentPairLowerEndpoints κm, f a = ∏ j ∈ κm.pairSupport with j < κm j, f (rightMomentIndex j)

theorem Anderson4D.prod_momentCrossLowerEndpoints {M : Type u_1} [CommMonoid M] {m : ℕ} (κp : PartialPairing (Fin m)) (f : Fin (2 * m) → M) : ∏ a ∈ momentCrossLowerEndpoints κp, f a = ∏ i ∈ κp.singles, f (leftMomentIndex i)

Covariance-product identification

theorem Anderson4D.primitiveCovarianceProduct_momentCombinedPairing (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (v : Fin (2 * m) → T4) : primitiveCovarianceProduct ρ ε m (momentCombinedPairing κp κm π) v = ((∏ i ∈ κp.pairSupport with i < κp i, ρ.etaEpsT4 ε (v (leftMomentIndex i) - v (leftMomentIndex (κp i)))) * ∏ j ∈ κm.pairSupport with j < κm j, ρ.etaEpsT4 ε (v (rightMomentIndex j) - v (rightMomentIndex (κm j)))) * momentCrossCovarianceProduct ρ ε m κp κm π v

The three covariance products in (4.18) are exactly the covariance product of the combined full pairing on the doubled carrier.

Finite contraction entities and extraction signatures

@[reducible, inline]

abbrev Anderson4D.MomentContraction (m : ℕ) : Type

One complete contraction choice in (4.18): a partial pairing in each copy and a bijection between their single sets.

Equations

• Anderson4D.MomentContraction m = ((κp : Anderson4D.PartialPairing (Fin m)) × (κm : Anderson4D.PartialPairing (Fin m)) × (↥κp.singles ≃ ↥κm.singles))

def Anderson4D.momentWithinHalfEndpointSignature {m : ℕ} (κp κm : PartialPairing (Fin m)) : Finset (Fin (2 * m)) × Finset (Fin (2 * m))

Endpoint roles of the Def. 3.1 intervals extracted separately in the left and right copies, embedded into the doubled carrier. This is the structure fixed in paper §4.2 Step 2 before (4.18); cross-copy intervals of the residual pairing are reduced only later, after (4.20).

Equations

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

def Anderson4D.momentContractionSignature {m : ℕ} (e : MomentContraction m) : Finset (Fin (2 * m)) × Finset (Fin (2 * m))

The within-half extraction signature associated with a complete contraction entity. The cross-single bijection does not change these initial intervals.

Equations

• Anderson4D.momentContractionSignature e = Anderson4D.momentWithinHalfEndpointSignature e.fst e.snd.fst

def Anderson4D.momentContractionSignatures (m : ℕ) : Finset (Finset (Fin (2 * m)) × Finset (Fin (2 * m)))

The finite set of doubled extraction signatures realized at order m.

Equations

• Anderson4D.momentContractionSignatures m = Finset.image Anderson4D.momentContractionSignature Finset.univ

theorem Anderson4D.card_momentContractionSignatures_le (m : ℕ) : (momentContractionSignatures m).card ≤ 4 ^ (2 * m)

The two within-half R-324 extraction structures have the same coarse 4^(2m) endpoint-role count as a role assignment on the doubled carrier.

theorem Anderson4D.sum_momentContractions_eq_nested {M : Type u_1} [AddCommMonoid M] (m : ℕ) (F : MomentContraction m → M) : ∑ e : MomentContraction m, F e = ∑ κp : PartialPairing (Fin m), ∑ κm : PartialPairing (Fin m), ∑ π : ↥κp.singles ≃ ↥κm.singles, F ⟨κp, ⟨κm, π⟩⟩

Nested sums over (κ⁺, κ⁻, π) are ordinary finite sums over the single contraction-entity type.

theorem Anderson4D.sum_momentContractions_by_signature {M : Type u_1} [AddCommMonoid M] (m : ℕ) (F : MomentContraction m → M) : ∑ s ∈ momentContractionSignatures m, ∑ e : MomentContraction m with momentContractionSignature e = s, F e = ∑ e : MomentContraction m, F e

Exact regrouping of the complete contraction sum by the extraction signature of its doubled full pairing.