Realizing residual primitive coordinates in one refined R-324 fibre

The residual-coordinate Fubini expansion is useful analytically only if every selected tuple is represented by an actual contraction in the same residual-refined fibre. We fill the residual block coordinates with the selected tuple, retain the baseline coordinates on every other primitive block, and invert the two exact coordinate equivalences.

noncomputable def Anderson4D.r324PrimitiveCoordinatesWithResidual {m : ℕ} {s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentRefinedContractionFiber m s r) (coordinates : R324ResidualPrimitiveCoordinates e₀.fst e₀.snd.fst e₀.snd.snd) : PrimitivePartitionCoordinates (momentPrimitiveBlockPartition e₀.fst e₀.snd.fst e₀.snd.snd)

Primitive coordinates which agree with the baseline contraction away from the residual block family and use the prescribed tuple on that family.

Equations

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

@[simp]

theorem Anderson4D.r324PrimitiveCoordinatesWithResidual_apply_residual {m : ℕ} {s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentRefinedContractionFiber m s r) (coordinates : R324ResidualPrimitiveCoordinates e₀.fst e₀.snd.fst e₀.snd.snd) (B : R324ResidualPrimitiveBlockIndex e₀.fst e₀.snd.fst e₀.snd.snd) : r324PrimitiveCoordinatesWithResidual e₀ he₀ coordinates ⟨↑B, ⋯⟩ = coordinates B

Evaluation of the completed coordinate tuple on a residual block.

theorem Anderson4D.r324PrimitiveCoordinatesWithResidual_apply_nonresidual {m : ℕ} {s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentRefinedContractionFiber m s r) (coordinates : R324ResidualPrimitiveCoordinates e₀.fst e₀.snd.fst e₀.snd.snd) (B : PrimitivePartitionBlockIndex (momentPrimitiveBlockPartition e₀.fst e₀.snd.fst e₀.snd.snd)) (hB : ↑B ∉ nonemptyMomentResidualCollapseBlocks e₀.fst e₀.snd.fst e₀.snd.snd) : r324PrimitiveCoordinatesWithResidual e₀ he₀ coordinates B = primitivePartitionFiberCoordinates (momentPrimitiveBlockPartition e₀.fst e₀.snd.fst e₀.snd.snd) ((momentRefinedFiberEquivPrimitivePartitionFiber e₀ he₀) ⟨e₀, he₀⟩) B

Evaluation away from the residual block family retains the baseline primitive coordinate.

theorem Anderson4D.momentLeftExtractionBlock_not_mem_nonemptyResidual {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (B : Finset (Fin (2 * m))) (hB : B ∈ momentLeftExtractionBlocks κp) : B ∉ nonemptyMomentResidualCollapseBlocks κp κm π

A left extraction block cannot also be a nonempty residual block.

theorem Anderson4D.momentRightExtractionBlock_not_mem_nonemptyResidual {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (B : Finset (Fin (2 * m))) (hB : B ∈ momentRightExtractionBlocks κm) : B ∉ nonemptyMomentResidualCollapseBlocks κp κm π

A right extraction block cannot also be a nonempty residual block.

theorem Anderson4D.r324PrimitiveCoordinatesWithResidual_apply_left {m : ℕ} {s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentRefinedContractionFiber m s r) (coordinates : R324ResidualPrimitiveCoordinates e₀.fst e₀.snd.fst e₀.snd.snd) (B : PrimitivePartitionBlockIndex (momentPrimitiveBlockPartition e₀.fst e₀.snd.fst e₀.snd.snd)) (hB : ↑B ∈ momentLeftExtractionBlocks e₀.fst) : r324PrimitiveCoordinatesWithResidual e₀ he₀ coordinates B = primitivePartitionFiberCoordinates (momentPrimitiveBlockPartition e₀.fst e₀.snd.fst e₀.snd.snd) ((momentRefinedFiberEquivPrimitivePartitionFiber e₀ he₀) ⟨e₀, he₀⟩) B

Every left extraction-block coordinate is retained from the baseline.

theorem Anderson4D.r324PrimitiveCoordinatesWithResidual_apply_right {m : ℕ} {s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentRefinedContractionFiber m s r) (coordinates : R324ResidualPrimitiveCoordinates e₀.fst e₀.snd.fst e₀.snd.snd) (B : PrimitivePartitionBlockIndex (momentPrimitiveBlockPartition e₀.fst e₀.snd.fst e₀.snd.snd)) (hB : ↑B ∈ momentRightExtractionBlocks e₀.snd.fst) : r324PrimitiveCoordinatesWithResidual e₀ he₀ coordinates B = primitivePartitionFiberCoordinates (momentPrimitiveBlockPartition e₀.fst e₀.snd.fst e₀.snd.snd) ((momentRefinedFiberEquivPrimitivePartitionFiber e₀ he₀) ⟨e₀, he₀⟩) B

Every right extraction-block coordinate is retained from the baseline.

noncomputable def Anderson4D.r324RefinedContractionOfResidualCoordinates {m : ℕ} {s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentRefinedContractionFiber m s r) (coordinates : R324ResidualPrimitiveCoordinates e₀.fst e₀.snd.fst e₀.snd.snd) : MomentRefinedContractionFiberAt m s r

The contraction in the fixed refined fibre realizing an arbitrary tuple of residual primitive coordinates.

Equations

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

theorem Anderson4D.r324RefinedContractionOfResidualCoordinates_mem {m : ℕ} {s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentRefinedContractionFiber m s r) (coordinates : R324ResidualPrimitiveCoordinates e₀.fst e₀.snd.fst e₀.snd.snd) : ↑(r324RefinedContractionOfResidualCoordinates e₀ he₀ coordinates) ∈ momentRefinedContractionFiber m s r

The realized contraction belongs to the original residual-refined fibre by construction.

theorem Anderson4D.r324RefinedContractionOfResidualCoordinates_coordinates {m : ℕ} {s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentRefinedContractionFiber m s r) (coordinates : R324ResidualPrimitiveCoordinates e₀.fst e₀.snd.fst e₀.snd.snd) : primitivePartitionFiberCoordinates (momentPrimitiveBlockPartition e₀.fst e₀.snd.fst e₀.snd.snd) ((momentRefinedFiberEquivPrimitivePartitionFiber e₀ he₀) (r324RefinedContractionOfResidualCoordinates e₀ he₀ coordinates)) = r324PrimitiveCoordinatesWithResidual e₀ he₀ coordinates

Applying both forward coordinate maps to the realized contraction recovers the completed primitive-coordinate tuple.

theorem Anderson4D.r324RefinedContractionOfResidualCoordinates_apply_residual {m : ℕ} {s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentRefinedContractionFiber m s r) (coordinates : R324ResidualPrimitiveCoordinates e₀.fst e₀.snd.fst e₀.snd.snd) (B : R324ResidualPrimitiveBlockIndex e₀.fst e₀.snd.fst e₀.snd.snd) : primitivePartitionFiberCoordinates (momentPrimitiveBlockPartition e₀.fst e₀.snd.fst e₀.snd.snd) ((momentRefinedFiberEquivPrimitivePartitionFiber e₀ he₀) (r324RefinedContractionOfResidualCoordinates e₀ he₀ coordinates)) ⟨↑B, ⋯⟩ = coordinates B

The primitive coordinate seen on each residual block of the realized contraction is exactly the prescribed one.

theorem Anderson4D.r324RefinedContractionOfResidualCoordinates_apply_left {m : ℕ} {s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentRefinedContractionFiber m s r) (coordinates : R324ResidualPrimitiveCoordinates e₀.fst e₀.snd.fst e₀.snd.snd) (B : PrimitivePartitionBlockIndex (momentPrimitiveBlockPartition e₀.fst e₀.snd.fst e₀.snd.snd)) (hB : ↑B ∈ momentLeftExtractionBlocks e₀.fst) : primitivePartitionFiberCoordinates (momentPrimitiveBlockPartition e₀.fst e₀.snd.fst e₀.snd.snd) ((momentRefinedFiberEquivPrimitivePartitionFiber e₀ he₀) (r324RefinedContractionOfResidualCoordinates e₀ he₀ coordinates)) B = primitivePartitionFiberCoordinates (momentPrimitiveBlockPartition e₀.fst e₀.snd.fst e₀.snd.snd) ((momentRefinedFiberEquivPrimitivePartitionFiber e₀ he₀) ⟨e₀, he₀⟩) B

The realized contraction has the baseline coordinate on every left extraction block.

theorem Anderson4D.r324RefinedContractionOfResidualCoordinates_apply_right {m : ℕ} {s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentRefinedContractionFiber m s r) (coordinates : R324ResidualPrimitiveCoordinates e₀.fst e₀.snd.fst e₀.snd.snd) (B : PrimitivePartitionBlockIndex (momentPrimitiveBlockPartition e₀.fst e₀.snd.fst e₀.snd.snd)) (hB : ↑B ∈ momentRightExtractionBlocks e₀.snd.fst) : primitivePartitionFiberCoordinates (momentPrimitiveBlockPartition e₀.fst e₀.snd.fst e₀.snd.snd) ((momentRefinedFiberEquivPrimitivePartitionFiber e₀ he₀) (r324RefinedContractionOfResidualCoordinates e₀ he₀ coordinates)) B = primitivePartitionFiberCoordinates (momentPrimitiveBlockPartition e₀.fst e₀.snd.fst e₀.snd.snd) ((momentRefinedFiberEquivPrimitivePartitionFiber e₀ he₀) ⟨e₀, he₀⟩) B

The realized contraction has the baseline coordinate on every right extraction block.

The realized residual covariance product

theorem Anderson4D.r324ResidualPrimitiveCoordinateFactor_eq_realized {m : ℕ} {s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} (ρ : SmoothCutoff) (ε : ℝ) (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentRefinedContractionFiber m s r) (coordinates : R324ResidualPrimitiveCoordinates e₀.fst e₀.snd.fst e₀.snd.snd) (B : R324ResidualPrimitiveBlockIndex e₀.fst e₀.snd.fst e₀.snd.snd) (v : Fin (2 * m) → T4) : r324ResidualPrimitiveCoordinateFactor ρ ε e₀.fst e₀.snd.fst e₀.snd.snd B (coordinates B) v = pairingCovarianceProductOn ρ ε (momentCombinedPairing (↑(r324RefinedContractionOfResidualCoordinates e₀ he₀ coordinates)).fst (↑(r324RefinedContractionOfResidualCoordinates e₀ he₀ coordinates)).snd.fst (↑(r324RefinedContractionOfResidualCoordinates e₀ he₀ coordinates)).snd.snd) (↑B) v

On one residual block, the prescribed coordinate factor is the actual ambient covariance factor of the realized contraction.

theorem Anderson4D.r324ResidualPrimitiveCoordinateProduct_eq_realized_on_baseline {m : ℕ} {s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} (ρ : SmoothCutoff) (ε : ℝ) (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentRefinedContractionFiber m s r) (coordinates : R324ResidualPrimitiveCoordinates e₀.fst e₀.snd.fst e₀.snd.snd) (v : Fin (2 * m) → T4) : r324ResidualPrimitiveCoordinateProduct ρ ε e₀.fst e₀.snd.fst e₀.snd.snd coordinates v = pairingCovarianceProductOn ρ ε (momentCombinedPairing (↑(r324RefinedContractionOfResidualCoordinates e₀ he₀ coordinates)).fst (↑(r324RefinedContractionOfResidualCoordinates e₀ he₀ coordinates)).snd.fst (↑(r324RefinedContractionOfResidualCoordinates e₀ he₀ coordinates)).snd.snd) (momentResidualActive e₀.fst e₀.snd.fst) v

The complete prescribed residual-coordinate product is the covariance product of the realized contraction on the baseline residual carrier.

Structural invariants of the realization

theorem Anderson4D.r324RefinedContractionOfResidualCoordinates_momentSignature {m : ℕ} {s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentRefinedContractionFiber m s r) (coordinates : R324ResidualPrimitiveCoordinates e₀.fst e₀.snd.fst e₀.snd.snd) : momentContractionSignature ↑(r324RefinedContractionOfResidualCoordinates e₀ he₀ coordinates) = momentContractionSignature e₀

Filling residual coordinates does not change the fixed within-half endpoint signature.

theorem Anderson4D.r324RefinedContractionOfResidualCoordinates_residualChainSignature {m : ℕ} {s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentRefinedContractionFiber m s r) (coordinates : R324ResidualPrimitiveCoordinates e₀.fst e₀.snd.fst e₀.snd.snd) : momentResidualChainSignature (↑(r324RefinedContractionOfResidualCoordinates e₀ he₀ coordinates)).fst (↑(r324RefinedContractionOfResidualCoordinates e₀ he₀ coordinates)).snd.fst (↑(r324RefinedContractionOfResidualCoordinates e₀ he₀ coordinates)).snd.snd = momentResidualChainSignature e₀.fst e₀.snd.fst e₀.snd.snd

Filling residual coordinates also preserves the fixed residual-chain endpoint signature.

theorem Anderson4D.r324RefinedContractionOfResidualCoordinates_extractionBlocks {m : ℕ} {s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentRefinedContractionFiber m s r) (coordinates : R324ResidualPrimitiveCoordinates e₀.fst e₀.snd.fst e₀.snd.snd) : momentLeftExtractionBlocks (↑(r324RefinedContractionOfResidualCoordinates e₀ he₀ coordinates)).fst = momentLeftExtractionBlocks e₀.fst ∧ momentRightExtractionBlocks (↑(r324RefinedContractionOfResidualCoordinates e₀ he₀ coordinates)).snd.fst = momentRightExtractionBlocks e₀.snd.fst

The left and right extraction-block families remain literally the same after realizing residual coordinates.

theorem Anderson4D.r324RefinedContractionOfResidualCoordinates_greenSkeletons {m : ℕ} {s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentRefinedContractionFiber m s r) (coordinates : R324ResidualPrimitiveCoordinates e₀.fst e₀.snd.fst e₀.snd.snd) : renormalizedGreenSkeleton (↑(r324RefinedContractionOfResidualCoordinates e₀ he₀ coordinates)).fst = renormalizedGreenSkeleton e₀.fst ∧ renormalizedGreenSkeleton (↑(r324RefinedContractionOfResidualCoordinates e₀ he₀ coordinates)).snd.fst = renormalizedGreenSkeleton e₀.snd.fst

Both signed Green skeletons are unchanged by residual-coordinate realization.

theorem Anderson4D.r324RefinedContractionOfResidualCoordinates_residualActive {m : ℕ} {s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentRefinedContractionFiber m s r) (coordinates : R324ResidualPrimitiveCoordinates e₀.fst e₀.snd.fst e₀.snd.snd) : momentResidualActive (↑(r324RefinedContractionOfResidualCoordinates e₀ he₀ coordinates)).fst (↑(r324RefinedContractionOfResidualCoordinates e₀ he₀ coordinates)).snd.fst = momentResidualActive e₀.fst e₀.snd.fst

The residual active carrier of the realized contraction is the baseline carrier on which its prescribed residual coordinates were installed.

theorem Anderson4D.r324ResidualPrimitiveCoordinateProduct_eq_pairingCovarianceProductOn {m : ℕ} {s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} (ρ : SmoothCutoff) (ε : ℝ) (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentRefinedContractionFiber m s r) (coordinates : R324ResidualPrimitiveCoordinates e₀.fst e₀.snd.fst e₀.snd.snd) (v : Fin (2 * m) → T4) : r324ResidualPrimitiveCoordinateProduct ρ ε e₀.fst e₀.snd.fst e₀.snd.snd coordinates v = pairingCovarianceProductOn ρ ε (momentCombinedPairing (↑(r324RefinedContractionOfResidualCoordinates e₀ he₀ coordinates)).fst (↑(r324RefinedContractionOfResidualCoordinates e₀ he₀ coordinates)).snd.fst (↑(r324RefinedContractionOfResidualCoordinates e₀ he₀ coordinates)).snd.snd) (momentResidualActive (↑(r324RefinedContractionOfResidualCoordinates e₀ he₀ coordinates)).fst (↑(r324RefinedContractionOfResidualCoordinates e₀ he₀ coordinates)).snd.fst) v

Every residual coordinate tuple is realized by an actual contraction in the same refined fibre, and its coordinate product is exactly the covariance product on that contraction's own residual active carrier.