Independent residual primitive coordinates at one refined R-324 root

After the two within-half products have been identified with their signed R-322 traces, the remaining cross-block product is still a product of complete finite primitive sums. This module performs only the exact finite Fubini interchange that exposes one independent coordinate on every residual block.

@[reducible, inline]

abbrev Anderson4D.R324ResidualPrimitiveBlockIndex {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : Type

A nonempty residual block of the fixed three-way primitive schedule.

Equations

• Anderson4D.R324ResidualPrimitiveBlockIndex κp κm π = { B : Finset (Fin (2 * m)) // B ∈ Anderson4D.nonemptyMomentResidualCollapseBlocks κp κm π }

@[reducible, inline]

abbrev Anderson4D.R324ResidualPrimitiveCoordinate {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (B : R324ResidualPrimitiveBlockIndex κp κm π) : Type

Complete primitive pairing coordinate on one residual block.

Equations

• Anderson4D.R324ResidualPrimitiveCoordinate B = Anderson4D.R324PrimitiveCoordinate (Anderson4D.residualBlockOrder ↑B)

@[reducible, inline]

abbrev Anderson4D.R324ResidualPrimitiveCoordinates {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : Type

One independently selected complete primitive pairing on every nonempty residual block.

Equations

• Anderson4D.R324ResidualPrimitiveCoordinates κp κm π = ((B : Anderson4D.R324ResidualPrimitiveBlockIndex κp κm π) → Anderson4D.R324ResidualPrimitiveCoordinate B)

theorem Anderson4D.r324ResidualPrimitiveBlock_mem_partition {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (B : R324ResidualPrimitiveBlockIndex κp κm π) : ↑B ∈ (momentPrimitiveBlockPartition κp κm π).blocks

Every residual schedule block is a literal block of the fixed primitive partition.

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

Covariance factor selected by one primitive coordinate on one residual block.

Equations

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

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

Covariance product selected by one complete residual coordinate tuple.

Equations

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

theorem Anderson4D.r324ResidualPrimitiveSumProduct_eq_sum_coordinates {m : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (v : Fin (2 * m) → T4) : r324ResidualPrimitiveSumProduct ρ ε κp κm π v = ∑ coordinates : R324ResidualPrimitiveCoordinates κp κm π, r324ResidualPrimitiveCoordinateProduct ρ ε κp κm π coordinates v

Exact finite Fubini expansion of the residual product into independent primitive coordinates.

Pointwise residual-coordinate expansion

theorem Anderson4D.momentRefinedPhysicalIntegrand_eq_sum_residualCoordinates (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (α β : Z4) (s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentRefinedContractionFiber m s r) (x y z w : T4) (v : Fin (2 * m) → T4) : momentRefinedPhysicalIntegrand ρ ε m α β s r x y z w v = ∑ coordinates : R324ResidualPrimitiveCoordinates e₀.fst e₀.snd.fst e₀.snd.snd, momentFourierPhase α β x y z w * ↑((R324WithinHalfResidualPrefix.initial ρ lam ε e₀.fst).residualIntegrand ρ ε x y fun (i : Fin m) => v (leftMomentIndex i)) * ↑((R324WithinHalfResidualPrefix.initial ρ lam ε e₀.snd.fst).residualIntegrand ρ ε z w fun (i : Fin m) => v (rightMomentIndex i)) * ↑(r324ResidualPrimitiveCoordinateProduct ρ ε e₀.fst e₀.snd.fst e₀.snd.snd coordinates v)

The exact refined physical root is a finite signed sum over residual primitive coordinates, with both certified within-half initial traces still outside the sum.