Exact bridge from one projected cross covariance to the marked residual core

The residual carrier contains three disjoint kinds of lower endpoints: within-left pairs, within-right pairs, and cross-copy pairs. A R324ResidualCovarianceSlot indexes only the third kind. This file keeps the other two complete physical covariance products explicit and proves that their product with the single-projected cross factor is exactly the marker-preserving covariance product on momentResidualActive.

No selector fibre is enlarged here. In particular, this equality is a pointwise physical-space identity and makes no assertion that a Fourier-selector fibre constrained by all of its modes is an unrestricted projected-covariance series.

The three disjoint residual lower-endpoint carriers

def Anderson4D.r324LeftResidualPairLowerEndpoints {m : ℕ} (κp : PartialPairing (Fin m)) : Finset (Fin (2 * m))

Lower endpoints of within-left pairs which survive the left reduction.

Equations

• Anderson4D.r324LeftResidualPairLowerEndpoints κp = Finset.image Anderson4D.leftMomentIndex ({i ∈ Anderson4D.finalActive κp | i < κp i})

def Anderson4D.r324RightResidualPairLowerEndpoints {m : ℕ} (κm : PartialPairing (Fin m)) : Finset (Fin (2 * m))

Lower endpoints of within-right pairs which survive the right reduction.

Equations

• Anderson4D.r324RightResidualPairLowerEndpoints κm = Finset.image Anderson4D.rightMomentIndex ({i ∈ Anderson4D.finalActive κm | i < κm i})

theorem Anderson4D.disjoint_r324LeftResidualPair_right {m : ℕ} (κp κm : PartialPairing (Fin m)) : Disjoint (r324LeftResidualPairLowerEndpoints κp) (r324RightResidualPairLowerEndpoints κm)

theorem Anderson4D.disjoint_r324LeftResidualPair_cross {m : ℕ} (κp : PartialPairing (Fin m)) : Disjoint (r324LeftResidualPairLowerEndpoints κp) (momentCrossLowerEndpoints κp)

theorem Anderson4D.disjoint_r324RightResidualPair_cross {m : ℕ} (κp κm : PartialPairing (Fin m)) : Disjoint (r324RightResidualPairLowerEndpoints κm) (momentCrossLowerEndpoints κp)

theorem Anderson4D.r324ResidualLowerEndpoints_eq_threeWay {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : {a ∈ momentResidualActive κp κm | a < (momentCombinedPairing κp κm π) a} = r324LeftResidualPairLowerEndpoints κp ∪ r324RightResidualPairLowerEndpoints κm ∪ momentCrossLowerEndpoints κp

The lower endpoints used by the combined pairing on the residual carrier are covered exactly once by the within-left, within-right, and cross-copy carriers.

Exact factor on each carrier

theorem Anderson4D.SmoothCutoff.prod_r324LeftResidualPairLowerEndpoints_marked_eq (ρ : SmoothCutoff) {m : ℕ} (ε L : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (v : Fin (2 * m) → T4) : (∏ a ∈ r324LeftResidualPairLowerEndpoints κp, if a = r324ResidualMarkedLowerEndpoint selected then ρ.r324ProjectedCovarianceC ε L (v a - v ((momentCombinedPairing κp κm π) a)) else ↑(ρ.etaEpsT4 ε (v a - v ((momentCombinedPairing κp κm π) a)))) = ↑(pairingCovarianceProductOn ρ ε κp (finalActive κp) fun (i : Fin m) => v (leftMomentIndex i))

theorem Anderson4D.SmoothCutoff.prod_r324RightResidualPairLowerEndpoints_marked_eq (ρ : SmoothCutoff) {m : ℕ} (ε L : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (v : Fin (2 * m) → T4) : (∏ a ∈ r324RightResidualPairLowerEndpoints κm, if a = r324ResidualMarkedLowerEndpoint selected then ρ.r324ProjectedCovarianceC ε L (v a - v ((momentCombinedPairing κp κm π) a)) else ↑(ρ.etaEpsT4 ε (v a - v ((momentCombinedPairing κp κm π) a)))) = ↑(pairingCovarianceProductOn ρ ε κm (finalActive κm) fun (i : Fin m) => v (rightMomentIndex i))

theorem Anderson4D.SmoothCutoff.prod_momentCrossLowerEndpoints_marked_eq (ρ : SmoothCutoff) {m : ℕ} (ε L : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (v : Fin (2 * m) → T4) : (∏ a ∈ momentCrossLowerEndpoints κp, if a = r324ResidualMarkedLowerEndpoint selected then ρ.r324ProjectedCovarianceC ε L (v a - v ((momentCombinedPairing κp κm π) a)) else ↑(ρ.etaEpsT4 ε (v a - v ((momentCombinedPairing κp κm π) a)))) = ρ.r324SingleProjectedResidualCovarianceProduct ε L κp κm π v selected

The exact three-factor marked product and signed core

theorem Anderson4D.SmoothCutoff.r324MarkedResidualActiveProduct_eq_threeFactor (ρ : SmoothCutoff) {m : ℕ} (ε L : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (v : Fin (2 * m) → T4) : ρ.r324MarkedPairingCovarianceProductOn ε L (momentCombinedPairing κp κm π) (r324ResidualMarkedLowerEndpoint selected) (momentResidualActive κp κm) v = ↑(pairingCovarianceProductOn ρ ε κp (finalActive κp) fun (i : Fin m) => v (leftMomentIndex i)) * ↑(pairingCovarianceProductOn ρ ε κm (finalActive κm) fun (i : Fin m) => v (rightMomentIndex i)) * ρ.r324SingleProjectedResidualCovarianceProduct ε L κp κm π v selected

The marker-preserving covariance product on the complete residual carrier is exactly:

1. the complete within-left residual covariance product;
2. the complete within-right residual covariance product; and
3. the cross-copy product with precisely one projected slot.

The equality is pointwise and retains all three factors inside the same physical integrand.

noncomputable def Anderson4D.SmoothCutoff.r324SingleProjectedResidualPhysicalInteriorCore (ρ : SmoothCutoff) {m : ℕ} (ε L : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (v : Fin (2 * m) → T4) : ℂ

Signed physical residual core written in the original three-factor coordinates. The Green profiles and all covariance factors remain in one physical-space product.

Equations

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

theorem Anderson4D.SmoothCutoff.r324SingleProjectedResidualPhysicalInteriorCore_eq_marked (ρ : SmoothCutoff) {m : ℕ} (ε L : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (v : Fin (2 * m) → T4) : ρ.r324SingleProjectedResidualPhysicalInteriorCore ε L κp κm π selected v = ρ.r324MarkedResidualPhysicalInteriorCore ε L κp κm π selected v

Exact signed-core bridge. The original three residual covariance factors are literally the marked physical core; no covariance factor is Fourier-expanded, estimated, or separated from the Green profiles.

theorem Anderson4D.SmoothCutoff.norm_r324SingleProjectedResidualPhysicalInteriorCore_eq (ρ : SmoothCutoff) {m : ℕ} (ε L : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (v : Fin (2 * m) → T4) : ‖ρ.r324SingleProjectedResidualPhysicalInteriorCore ε L κp κm π selected v‖ = ‖ρ.r324ProjectedCovarianceC ε L (v (r324ResidualMarkedLowerEndpoint selected) - v (r324ResidualMarkedUpperEndpoint π selected))‖ * ρ.r324MarkedResidualPhysicalComplementMass ε κp κm π selected v

Exact complement ledger for the original three-factor core. Removing only the projected edge leaves precisely the already-defined complete physical complement mass.