Exact primitive coordinates of one refined R-324 fibre

The common primitive-block schedule of a residual-refined contraction fibre does not merely give an embedding into the generic block fibre: fullness and relative primitivity on every scheduled block recover the two within-half extraction signatures and the residual interval chain. Consequently the embedding is an equivalence.

One-half active carriers inside the doubled order

def Anderson4D.momentLeftAugmentedActive (m : ℕ) (active : Finset (Fin m)) : Finset (Fin (2 * m))

Keep an active subset of the left copy and all of the right copy.

Equations

• Anderson4D.momentLeftAugmentedActive m active = Finset.image Anderson4D.leftMomentIndex active ∪ Finset.image Anderson4D.rightMomentIndex Finset.univ

def Anderson4D.momentRightAugmentedActive (m : ℕ) (active : Finset (Fin m)) : Finset (Fin (2 * m))

Keep all of the left copy and an active subset of the right copy.

Equations

• Anderson4D.momentRightAugmentedActive m active = Finset.image Anderson4D.leftMomentIndex Finset.univ ∪ Finset.image Anderson4D.rightMomentIndex active

@[simp]

theorem Anderson4D.leftMomentIndex_mem_momentLeftAugmentedActive {m : ℕ} (active : Finset (Fin m)) (i : Fin m) : leftMomentIndex i ∈ momentLeftAugmentedActive m active ↔ i ∈ active

@[simp]

theorem Anderson4D.rightMomentIndex_mem_momentRightAugmentedActive {m : ℕ} (active : Finset (Fin m)) (i : Fin m) : rightMomentIndex i ∈ momentRightAugmentedActive m active ↔ i ∈ active

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

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

@[simp]

theorem Anderson4D.momentLeftAugmentedActive_univ (m : ℕ) : momentLeftAugmentedActive m Finset.univ = Finset.univ

@[simp]

theorem Anderson4D.momentRightAugmentedActive_univ (m : ℕ) : momentRightAugmentedActive m Finset.univ = Finset.univ

theorem Anderson4D.momentLeftAugmentedActive_sdiff_image {m : ℕ} (active I : Finset (Fin m)) : momentLeftAugmentedActive m (active \ I) = momentLeftAugmentedActive m active \ Finset.image leftMomentIndex I

theorem Anderson4D.momentRightAugmentedActive_sdiff_image {m : ℕ} (active I : Finset (Fin m)) : momentRightAugmentedActive m (active \ I) = momentRightAugmentedActive m active \ Finset.image rightMomentIndex I

Saturated subcovers of a primitive partition

def Anderson4D.primitiveBlocksInside {n : ℕ} (blocks : List (Finset (Fin n))) (active : Finset (Fin n)) : List (Finset (Fin n))

Blocks of a list which lie wholly in a current active carrier.

Equations

• Anderson4D.primitiveBlocksInside blocks active = List.filter (fun (B : Finset (Fin n)) => decide (B ⊆ active)) blocks

theorem Anderson4D.finsetUnionList_primitiveBlocksInside_eq {n : ℕ} (blocks : List (Finset (Fin n))) (active : Finset (Fin n)) (hcover : finsetUnionList blocks = Finset.univ) (hsaturated : ∀ B ∈ blocks, (B ∩ active).Nonempty → B ⊆ active) : finsetUnionList (primitiveBlocksInside blocks active) = active

If a current carrier is saturated by a complete block partition, filtering to the blocks contained in that carrier still covers it exactly.

theorem Anderson4D.primitiveBlocksInside_forall {n : ℕ} (blocks : List (Finset (Fin n))) (active : Finset (Fin n)) (P : Finset (Fin n) → Prop) (hP : List.Forall P blocks) : List.Forall P (primitiveBlocksInside blocks active)

theorem Anderson4D.blockPartitionSaturated_sdiff {n : ℕ} (blocks : List (Finset (Fin n))) (hpairwise : List.Pairwise Disjoint blocks) (active S : Finset (Fin n)) (hS : S ∈ blocks) (hsaturated : ∀ B ∈ blocks, (B ∩ active).Nonempty → B ⊆ active) (B : Finset (Fin n)) : B ∈ blocks → (B ∩ (active \ S)).Nonempty → B ⊆ active \ S

Removing one whole member of a pairwise-disjoint saturated partition preserves saturation.

Candidate reflection through the augmented carriers

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

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

Recovery of the two within-half extraction recursions

theorem Anderson4D.extractAux_eq_of_common_momentPrimitivePartition_left {m : ℕ} (e₀ e : MomentContraction m) (htarget : ∀ B ∈ (momentPrimitiveBlockPartition e₀.fst e₀.snd.fst e₀.snd.snd).blocks, IsFullyPairedOn (momentCombinedPairing e.fst e.snd.fst e.snd.snd) B ∧ IsRelPrimitiveOn (momentCombinedPairing e.fst e.snd.fst e.snd.snd) B) (fuel : ℕ) (active : Finset (Fin m)) : (∀ B ∈ (momentPrimitiveBlockPartition e₀.fst e₀.snd.fst e₀.snd.snd).blocks, (B ∩ momentLeftAugmentedActive m active).Nonempty → B ⊆ momentLeftAugmentedActive m active) → (∀ B ∈ extractionBlocksAux e₀.fst fuel active, Finset.image leftMomentIndex B ∈ (momentPrimitiveBlockPartition e₀.fst e₀.snd.fst e₀.snd.snd).blocks) → extractAux e.fst fuel active = extractAux e₀.fst fuel active

theorem Anderson4D.extract_left_eq_of_common_momentPrimitivePartition {m : ℕ} (e₀ e : MomentContraction m) (htarget : ∀ B ∈ (momentPrimitiveBlockPartition e₀.fst e₀.snd.fst e₀.snd.snd).blocks, IsFullyPairedOn (momentCombinedPairing e.fst e.snd.fst e.snd.snd) B ∧ IsRelPrimitiveOn (momentCombinedPairing e.fst e.snd.fst e.snd.snd) B) : extract e.fst = extract e₀.fst

theorem Anderson4D.extractAux_eq_of_common_momentPrimitivePartition_right {m : ℕ} (e₀ e : MomentContraction m) (htarget : ∀ B ∈ (momentPrimitiveBlockPartition e₀.fst e₀.snd.fst e₀.snd.snd).blocks, IsFullyPairedOn (momentCombinedPairing e.fst e.snd.fst e.snd.snd) B ∧ IsRelPrimitiveOn (momentCombinedPairing e.fst e.snd.fst e.snd.snd) B) (fuel : ℕ) (active : Finset (Fin m)) : (∀ B ∈ (momentPrimitiveBlockPartition e₀.fst e₀.snd.fst e₀.snd.snd).blocks, (B ∩ momentRightAugmentedActive m active).Nonempty → B ⊆ momentRightAugmentedActive m active) → (∀ B ∈ extractionBlocksAux e₀.snd.fst fuel active, Finset.image rightMomentIndex B ∈ (momentPrimitiveBlockPartition e₀.fst e₀.snd.fst e₀.snd.snd).blocks) → extractAux e.snd.fst fuel active = extractAux e₀.snd.fst fuel active

theorem Anderson4D.extract_right_eq_of_common_momentPrimitivePartition {m : ℕ} (e₀ e : MomentContraction m) (htarget : ∀ B ∈ (momentPrimitiveBlockPartition e₀.fst e₀.snd.fst e₀.snd.snd).blocks, IsFullyPairedOn (momentCombinedPairing e.fst e.snd.fst e.snd.snd) B ∧ IsRelPrimitiveOn (momentCombinedPairing e.fst e.snd.fst e.snd.snd) B) : extract e.snd.fst = extract e₀.snd.fst

theorem Anderson4D.momentContractionSignature_eq_of_commonPrimitivePartition {m : ℕ} (e₀ e : MomentContraction m) (htarget : ∀ B ∈ (momentPrimitiveBlockPartition e₀.fst e₀.snd.fst e₀.snd.snd).blocks, IsFullyPairedOn (momentCombinedPairing e.fst e.snd.fst e.snd.snd) B ∧ IsRelPrimitiveOn (momentCombinedPairing e.fst e.snd.fst e.snd.snd) B) : momentContractionSignature e = momentContractionSignature e₀

theorem Anderson4D.momentResidualIntervalChain_eq_of_commonPrimitivePartition {m : ℕ} (e₀ e : MomentContraction m) (htarget : ∀ B ∈ (momentPrimitiveBlockPartition e₀.fst e₀.snd.fst e₀.snd.snd).blocks, IsFullyPairedOn (momentCombinedPairing e.fst e.snd.fst e.snd.snd) B ∧ IsRelPrimitiveOn (momentCombinedPairing e.fst e.snd.fst e.snd.snd) B) : momentResidualIntervalChain e.fst e.snd.fst e.snd.snd = momentResidualIntervalChain e₀.fst e₀.snd.fst e₀.snd.snd

theorem Anderson4D.momentResidualChainSignature_eq_of_commonPrimitivePartition {m : ℕ} (e₀ e : MomentContraction m) (htarget : ∀ B ∈ (momentPrimitiveBlockPartition e₀.fst e₀.snd.fst e₀.snd.snd).blocks, IsFullyPairedOn (momentCombinedPairing e.fst e.snd.fst e.snd.snd) B ∧ IsRelPrimitiveOn (momentCombinedPairing e.fst e.snd.fst e.snd.snd) B) : momentResidualChainSignature e.fst e.snd.fst e.snd.snd = momentResidualChainSignature e₀.fst e₀.snd.fst e₀.snd.snd

Exact refined-fibre equivalence

theorem Anderson4D.momentRefinedFiberToPrimitivePartitionFiber_surjective {m : ℕ} {s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentRefinedContractionFiber m s r) : Function.Surjective (momentRefinedFiberToPrimitivePartitionFiber e₀ he₀)

noncomputable def Anderson4D.momentRefinedFiberEquivPrimitivePartitionFiber {m : ℕ} {s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentRefinedContractionFiber m s r) : MomentRefinedContractionFiberAt m s r ≃ PrimitivePartitionFiber (momentPrimitiveBlockPartition e₀.fst e₀.snd.fst e₀.snd.snd)

The realized refined contraction fibre is exactly, rather than merely embedded in, the generic fibre of pairings full and primitive on every block of its common schedule.

Equations

• Anderson4D.momentRefinedFiberEquivPrimitivePartitionFiber e₀ he₀ = Equiv.ofBijective (Anderson4D.momentRefinedFiberToPrimitivePartitionFiber e₀ he₀) ⋯

@[simp]

theorem Anderson4D.momentRefinedFiberEquivPrimitivePartitionFiber_apply {m : ℕ} {s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentRefinedContractionFiber m s r) (e : MomentRefinedContractionFiberAt m s r) : (momentRefinedFiberEquivPrimitivePartitionFiber e₀ he₀) e = momentRefinedFiberToPrimitivePartitionFiber e₀ he₀ e

theorem Anderson4D.sum_refinedCovariance_eq_sum_primitivePartitionFiber (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) {s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentRefinedContractionFiber m s r) (v : Fin (2 * m) → T4) : ∑ e ∈ momentRefinedContractionFiber m s r, primitiveCovarianceProduct ρ ε m (momentCombinedPairing e.fst e.snd.fst e.snd.snd) v = ∑ τ : PrimitivePartitionFiber (momentPrimitiveBlockPartition e₀.fst e₀.snd.fst e₀.snd.snd), primitiveCovarianceProduct ρ ε m (↑τ) v

Exact finite-sum reindexing of a residual-refined covariance fibre by the complete primitive-partition fibre.