Exact residual block product with one surviving marker

After the signed within-half collapses, the residual carrier is partitioned by the genuine nonempty residual blocks. This module performs only the finite-product part of the residual collapse: it extracts the unique marked block and proves that every remaining block is still its complete physical covariance factor.

No spatial norm, tree cover, cell volume, or automorphism factor is used here. In particular, the marked block remains open for the later analytic cell estimate.

A marked product over a disjoint block list

theorem Anderson4D.SmoothCutoff.r324MarkedPairingCovarianceProductOn_finsetUnionList {n : ℕ} (ρ : SmoothCutoff) (ε L : ℝ) (κ : PartialPairing (Fin n)) (marked : Fin n) (blocks : List (Finset (Fin n))) (hblocks : List.Pairwise Disjoint blocks) (v : Fin n → T4) : ρ.r324MarkedPairingCovarianceProductOn ε L κ marked (finsetUnionList blocks) v = (List.map (fun (B : Finset (Fin n)) => ρ.r324MarkedPairingCovarianceProductOn ε L κ marked B v) blocks).prod

Exact multiplicative decomposition of a marked covariance product over a pairwise-disjoint list of blocks. The distinguished factor occurs in at most one block because the list is disjoint.

The concrete residual schedule

theorem Anderson4D.nonemptyMomentResidualCollapseBlocks_nodup {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : (nonemptyMomentResidualCollapseBlocks κp κm π).Nodup

Pairwise-disjoint nonempty residual blocks cannot repeat.

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

Product of the complete physical covariance factors on every residual block except the unique marked block.

Equations

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

theorem Anderson4D.SmoothCutoff.r324MarkedResidualActiveProduct_eq_marked_mul_unmarked {m : ℕ} (ρ : SmoothCutoff) (ε 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 = ρ.r324MarkedPairingCovarianceProductOn ε L (momentCombinedPairing κp κm π) (r324ResidualMarkedLowerEndpoint selected) (r324MarkedResidualBlock κp κm π selected) v * ρ.r324UnmarkedResidualBlockProduct ε κp κm π selected v

Exact marker-preserving residual block collapse.

The marked covariance product on the actual residual carrier is the genuine marked-block factor times complete covariance factors on all other primitive blocks. Thus the preliminary collapses neither duplicate nor discard the selected projected edge.