Three-way block split of the exact R-324 primitive partition

The exact primitive-coordinate fibre of one residual-refined R-324 signature is indexed by the concatenation of three literal block families: the left extraction blocks, the right extraction blocks, and the nonempty residual cross blocks. This file records that concatenation and the corresponding exact product split while all factors are still signed.

This is algebraic bookkeeping only. It does not take a norm, integrate an endpoint, or claim that the concatenation order is the analytic Phase-A order inside either half.

The literal three-family list

theorem Anderson4D.momentNonemptyPrimitiveBlocks_eq_threeFamilies {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : momentNonemptyPrimitiveBlocks κp κm π = momentLeftExtractionBlocks κp ++ momentRightExtractionBlocks κm ++ nonemptyMomentResidualCollapseBlocks κp κm π

Removing empty blocks affects only the residual family: extraction blocks in either half are already nonempty.

A proof-independent complete sum attached to an ambient block

noncomputable def Anderson4D.r324PrimitivePartitionBlockSum {m : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (B : Finset (Fin (2 * m))) (v : Fin (2 * m) → T4) : ℝ

Complete primitive-pairing sum on one block of the concrete R-324 partition. The default branch is irrelevant on the literal schedule and makes the function convenient for list products.

Equations

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

theorem Anderson4D.r324PrimitivePartitionBlockSum_of_mem {m : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (B : Finset (Fin (2 * m))) (hB : B ∈ (momentPrimitiveBlockPartition κp κm π).blocks) (v : Fin (2 * m) → T4) : r324PrimitivePartitionBlockSum ρ ε κp κm π B v = ∑ σ : ↥(primitiveFullPairings (residualBlockOrder B)), primitivePartitionBlockCovarianceFactor ρ ε (momentPrimitiveBlockPartition κp κm π) ⟨B, hB⟩ σ v

Exact split of the dependent block product

theorem Anderson4D.prod_primitivePartitionBlockSums_eq_threeFamilies {m : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (v : Fin (2 * m) → T4) : ∏ B : PrimitivePartitionBlockIndex (momentPrimitiveBlockPartition κp κm π), ∑ σ : ↥(primitiveFullPairings (residualBlockOrder ↑B)), primitivePartitionBlockCovarianceFactor ρ ε (momentPrimitiveBlockPartition κp κm π) B σ v = (List.map (fun (B : Finset (Fin (2 * m))) => r324PrimitivePartitionBlockSum ρ ε κp κm π B v) (momentLeftExtractionBlocks κp)).prod * (List.map (fun (B : Finset (Fin (2 * m))) => r324PrimitivePartitionBlockSum ρ ε κp κm π B v) (momentRightExtractionBlocks κm)).prod * (List.map (fun (B : Finset (Fin (2 * m))) => r324PrimitivePartitionBlockSum ρ ε κp κm π B v) (nonemptyMomentResidualCollapseBlocks κp κm π)).prod

The dependent complete-coordinate product is exactly the product of the left, right, and residual list products.