Concrete blocks removed by Definition 3.1

extract records only the endpoint pair chosen at each reduction step. For the R-322/R-324 analytic iteration one also needs the actual trace in the then-current carrier. This file runs the same recursion while recording those traces and proves:

• they are pairwise disjoint and cover the complement of finalActive;
• every recorded trace is fully paired;
• minimality of selectRel makes every recorded trace relatively primitive;
• the covariance product factors exactly over the recorded traces and the terminal active carrier.

theorem Anderson4D.finsetUnionList_map_image {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (f : α → β) (blocks : List (Finset α)) : finsetUnionList (List.map (fun (B : Finset α) => Finset.image f B) blocks) = Finset.image f (finsetUnionList blocks)

Finite union commutes with mapping every block by the same finset image.

theorem Anderson4D.list_map_image_pairwise_disjoint {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (f : α → β) (hf : Function.Injective f) (blocks : List (Finset α)) (hblocks : List.Pairwise Disjoint blocks) : List.Pairwise Disjoint (List.map (fun (B : Finset α) => Finset.image f B) blocks)

An injective image preserves pairwise disjointness of a block list.

def Anderson4D.extractionBlocksAux {m : ℕ} (κ : PartialPairing (Fin m)) : ℕ → Finset (Fin m) → List (Finset (Fin m))

The actual fully-paired trace removed at each execution of Definition 3.1.

Equations

• One or more equations did not get rendered due to their size.
• Anderson4D.extractionBlocksAux κ 0 x✝ = []

@[simp]

theorem Anderson4D.extractionBlocksAux_zero {m : ℕ} (κ : PartialPairing (Fin m)) (active : Finset (Fin m)) : extractionBlocksAux κ 0 active = []

@[simp]

theorem Anderson4D.extractionBlocksAux_succ_pos {m : ℕ} {κ : PartialPairing (Fin m)} {active : Finset (Fin m)} (fuel : ℕ) (h : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired κ active a b) : extractionBlocksAux κ (fuel + 1) active = relIcc active (selectRel κ active h).1 (selectRel κ active h).2 :: extractionBlocksAux κ fuel (active \ relIcc active (selectRel κ active h).1 (selectRel κ active h).2)

@[simp]

theorem Anderson4D.extractionBlocksAux_succ_neg {m : ℕ} {κ : PartialPairing (Fin m)} {active : Finset (Fin m)} (fuel : ℕ) (h : ¬∃ (a : Fin m) (b : Fin m), IsRelFullyPaired κ active a b) : extractionBlocksAux κ (fuel + 1) active = []

def Anderson4D.extractionBlocks {m : ℕ} (κ : PartialPairing (Fin m)) : List (Finset (Fin m))

Public block list for the full Definition 3.1 run.

Equations

• Anderson4D.extractionBlocks κ = Anderson4D.extractionBlocksAux κ m Finset.univ

theorem Anderson4D.extractionBlocksAux_forall_subset {m : ℕ} (κ : PartialPairing (Fin m)) (fuel : ℕ) (active : Finset (Fin m)) : List.Forall (fun (B : Finset (Fin m)) => B ⊆ active) (extractionBlocksAux κ fuel active)

Every block produced from active remains inside active.

theorem Anderson4D.extractionBlocksAux_pairwise_disjoint {m : ℕ} (κ : PartialPairing (Fin m)) (fuel : ℕ) (active : Finset (Fin m)) : List.Pairwise Disjoint (extractionBlocksAux κ fuel active)

The recorded blocks are pairwise disjoint.

theorem Anderson4D.extractionBlocksAux_forall_isFullyPairedOn {m : ℕ} (κ : PartialPairing (Fin m)) (fuel : ℕ) (active : Finset (Fin m)) : List.Forall (IsFullyPairedOn κ) (extractionBlocksAux κ fuel active)

Every recorded block is closed under the pairing and contains no single.

theorem Anderson4D.relIcc_subset_relIcc_of_endpoints_mem {m : ℕ} {active : Finset (Fin m)} {a b c d : Fin m} (hc : c ∈ relIcc active a b) (hd : d ∈ relIcc active a b) : relIcc active c d ⊆ relIcc active a b

A relative interval with both endpoints in an outer relative interval is a subset of that outer interval.

theorem Anderson4D.selectRel_trace_isRelPrimitiveOn {m : ℕ} (κ : PartialPairing (Fin m)) (active : Finset (Fin m)) (h : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired κ active a b) : IsRelPrimitiveOn κ (relIcc active (selectRel κ active h).1 (selectRel κ active h).2)

Minimality of the Definition 3.1 selector implies that its selected trace is primitive on its sparse carrier.

theorem Anderson4D.extractionBlocksAux_forall_isRelPrimitiveOn {m : ℕ} (κ : PartialPairing (Fin m)) (fuel : ℕ) (active : Finset (Fin m)) : List.Forall (IsRelPrimitiveOn κ) (extractionBlocksAux κ fuel active)

Every block produced by Definition 3.1 is relatively primitive.

theorem Anderson4D.finsetUnionList_extractionBlocksAux_union_final {m : ℕ} (κ : PartialPairing (Fin m)) (fuel : ℕ) (active : Finset (Fin m)) : finsetUnionList (extractionBlocksAux κ fuel active) ∪ (extractAuxS κ fuel active).2 = active

Removed blocks together with the terminal active carrier cover the initial active carrier exactly.

theorem Anderson4D.extractAuxS_final_subset {m : ℕ} (κ : PartialPairing (Fin m)) (fuel : ℕ) (active : Finset (Fin m)) : (extractAuxS κ fuel active).2 ⊆ active

The terminal active carrier remains a subset of the carrier supplied to the recursion.

theorem Anderson4D.extractionBlocksAux_disjoint_final {m : ℕ} (κ : PartialPairing (Fin m)) (fuel : ℕ) (active : Finset (Fin m)) : Disjoint (finsetUnionList (extractionBlocksAux κ fuel active)) (extractAuxS κ fuel active).2

The union of all removed blocks is disjoint from the terminal active carrier.

theorem Anderson4D.finsetUnionList_extractionBlocks_union_finalActive {m : ℕ} (κ : PartialPairing (Fin m)) : finsetUnionList (extractionBlocks κ) ∪ finalActive κ = Finset.univ

The public extraction blocks cover precisely the complement of finalActive.

theorem Anderson4D.extractionBlocks_disjoint_finalActive {m : ℕ} (κ : PartialPairing (Fin m)) : Disjoint (finsetUnionList (extractionBlocks κ)) (finalActive κ)

The terminal carrier is disjoint from every removed block.

theorem Anderson4D.extractionBlocks_pairwise_disjoint {m : ℕ} (κ : PartialPairing (Fin m)) : List.Pairwise Disjoint (extractionBlocks κ)

theorem Anderson4D.extractionBlocks_forall_isFullyPairedOn {m : ℕ} (κ : PartialPairing (Fin m)) : List.Forall (IsFullyPairedOn κ) (extractionBlocks κ)

theorem Anderson4D.extractionBlocks_forall_isRelPrimitiveOn {m : ℕ} (κ : PartialPairing (Fin m)) : List.Forall (IsRelPrimitiveOn κ) (extractionBlocks κ)

theorem Anderson4D.extractionBlock_isFullyPairedOn_of_mem {m : ℕ} (κ : PartialPairing (Fin m)) (B : Finset (Fin m)) (hB : B ∈ extractionBlocks κ) : IsFullyPairedOn κ B

theorem Anderson4D.extractionBlock_isRelPrimitiveOn_of_mem {m : ℕ} (κ : PartialPairing (Fin m)) (B : Finset (Fin m)) (hB : B ∈ extractionBlocks κ) : IsRelPrimitiveOn κ B

theorem Anderson4D.extractionBlock_residualPrimitiveBlockPairing_mem {m : ℕ} (κ : PartialPairing (Fin m)) (B : Finset (Fin m)) (hB : B ∈ extractionBlocks κ) : residualPrimitiveBlockPairing κ B ⋯ ∈ primitiveFullPairings (residualBlockOrder B)

Every concrete Definition 3.1 block transports to an actual member of the primitive full-pairing family used by Proposition 4.1.

theorem Anderson4D.pairingCovarianceProductOn_univ_eq_extractionBlocks_mul_final {m : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (κ : PartialPairing (Fin m)) (v : Fin m → T4) : pairingCovarianceProductOn ρ ε κ Finset.univ v = (List.map (fun (B : Finset (Fin m)) => pairingCovarianceProductOn ρ ε κ B v) (extractionBlocks κ)).prod * pairingCovarianceProductOn ρ ε κ (finalActive κ) v

Exact covariance factorization into all Definition 3.1 primitive blocks and the terminal carrier.

theorem Anderson4D.primitiveCovarianceProduct_eq_prod_extractionBlocks_of_full (ρ : SmoothCutoff) (ε : ℝ) (q : ℕ) (κ : PartialPairing (Fin (2 * q))) (hκ : κ.IsFull) (v : Fin (2 * q) → T4) : primitiveCovarianceProduct ρ ε q κ v = (List.map (fun (B : Finset (Fin (2 * q))) => pairingCovarianceProductOn ρ ε κ B v) (extractionBlocks κ)).prod

For a full pairing the terminal carrier is empty, so its entire covariance product is the product of the primitive extraction-block factors.