Marker-preserving residual collapse for R-324

After the signed within-copy collapses, a selected cross-copy covariance must remain visible while the residual primitive blocks are collapsed. This file records that visibility directly on the genuine residual block schedule.

The marked covariance product below differs from the physical covariance product at exactly one lower endpoint. The residual blocks partition the post-phase-A carrier and are closed under the combined pairing, so:

• the two endpoints of the marked cross slot lie in one unique nonempty residual block;
• every other block contains neither endpoint and retains its complete etaEpsT4 covariance product;
• collapsing an unmarked head block leaves the marked product on the tail; and
• collapsing the marked head block leaves a completely unmarked tail.

These are exact finite-product identities. No equality with the final R-324 moment, no analytic estimate, and no abstract output predicate is asserted here.

A single marked lower endpoint

noncomputable def Anderson4D.SmoothCutoff.r324MarkedPairingCovarianceProductOn {n : ℕ} (ρ : SmoothCutoff) (ε L : ℝ) (κ : PartialPairing (Fin n)) (marked : Fin n) (B : Finset (Fin n)) (v : Fin n → T4) : ℂ

Covariance product on an ambient block with exactly one distinguished lower endpoint replaced by the R-324 high-frequency projection.

Equations

• ρ.r324MarkedPairingCovarianceProductOn ε L κ marked B v = ∏ i ∈ B with i < κ i, if i = marked then ρ.r324ProjectedCovarianceC ε L (v i - v (κ i)) else ↑(ρ.etaEpsT4 ε (v i - v (κ i)))

theorem Anderson4D.SmoothCutoff.r324MarkedPairingCovarianceProductOn_eq_complete {n : ℕ} (ρ : SmoothCutoff) (ε L : ℝ) (κ : PartialPairing (Fin n)) (marked : Fin n) (B : Finset (Fin n)) (v : Fin n → T4) (hmarked : marked ∉ B) : ρ.r324MarkedPairingCovarianceProductOn ε L κ marked B v = ↑(pairingCovarianceProductOn ρ ε κ B v)

An unmarked block is literally the existing complete physical covariance product (coerced to ℂ).

theorem Anderson4D.SmoothCutoff.r324MarkedPairingCovarianceProductOn_union {n : ℕ} (ρ : SmoothCutoff) (ε L : ℝ) (κ : PartialPairing (Fin n)) (marked : Fin n) (A B : Finset (Fin n)) (hAB : Disjoint A B) (v : Fin n → T4) : ρ.r324MarkedPairingCovarianceProductOn ε L κ marked (A ∪ B) v = ρ.r324MarkedPairingCovarianceProductOn ε L κ marked A v * ρ.r324MarkedPairingCovarianceProductOn ε L κ marked B v

Marked covariance products multiply over disjoint blocks without creating another projected factor.

The genuine marked residual block

def Anderson4D.r324ResidualMarkedLowerEndpoint {m : ℕ} {κp : PartialPairing (Fin m)} (selected : R324ResidualCovarianceSlot κp) : Fin (2 * m)

The lower endpoint of a selected residual cross covariance.

Equations

• Anderson4D.r324ResidualMarkedLowerEndpoint selected = Anderson4D.leftMomentIndex ↑selected

def Anderson4D.r324ResidualMarkedUpperEndpoint {m : ℕ} {κp κm : PartialPairing (Fin m)} (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) : Fin (2 * m)

The upper endpoint of a selected residual cross covariance.

Equations

• Anderson4D.r324ResidualMarkedUpperEndpoint π selected = Anderson4D.rightMomentIndex ↑(π selected)

theorem Anderson4D.r324ResidualMarkedLowerEndpoint_mem_active {m : ℕ} (κp κm : PartialPairing (Fin m)) (selected : R324ResidualCovarianceSlot κp) : r324ResidualMarkedLowerEndpoint selected ∈ momentResidualActive κp κm

theorem Anderson4D.r324ResidualMarkedUpperEndpoint_mem_active {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) : r324ResidualMarkedUpperEndpoint π selected ∈ momentResidualActive κp κm

@[simp]

theorem Anderson4D.momentCombinedPairing_r324ResidualMarkedLowerEndpoint {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) : (momentCombinedPairing κp κm π) (r324ResidualMarkedLowerEndpoint selected) = r324ResidualMarkedUpperEndpoint π selected

theorem Anderson4D.r324ResidualMarkedLowerEndpoint_lt_upper {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) : r324ResidualMarkedLowerEndpoint selected < r324ResidualMarkedUpperEndpoint π selected

theorem Anderson4D.exists_residualBlock_mem_of_marked {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) : ∃ B ∈ nonemptyMomentResidualCollapseBlocks κp κm π, r324ResidualMarkedLowerEndpoint selected ∈ B

The selected cross lower endpoint belongs to a residual block in the actual post-phase-A schedule.

theorem Anderson4D.existsUnique_residualBlock_mem_of_marked {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) : ∃! B : Finset (Fin (2 * m)), B ∈ nonemptyMomentResidualCollapseBlocks κp κm π ∧ r324ResidualMarkedLowerEndpoint selected ∈ B

Pairwise disjointness makes the residual block containing the marked cross slot unique.

noncomputable def Anderson4D.r324MarkedResidualBlock {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) : Finset (Fin (2 * m))

The unique block carrying the projected cross covariance.

Equations

• Anderson4D.r324MarkedResidualBlock κp κm π selected = Classical.choose ⋯

theorem Anderson4D.r324MarkedResidualBlock_mem {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) : r324MarkedResidualBlock κp κm π selected ∈ nonemptyMomentResidualCollapseBlocks κp κm π

theorem Anderson4D.r324ResidualMarkedLowerEndpoint_mem_markedBlock {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) : r324ResidualMarkedLowerEndpoint selected ∈ r324MarkedResidualBlock κp κm π selected

theorem Anderson4D.r324ResidualMarkedUpperEndpoint_mem_markedBlock {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) : r324ResidualMarkedUpperEndpoint π selected ∈ r324MarkedResidualBlock κp κm π selected

Closedness of the genuine residual block carries the other endpoint of the marked cross covariance in the same unique block.

theorem Anderson4D.SmoothCutoff.r324MarkedResidualBlockProduct_eq {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) (r324MarkedResidualBlock κp κm π selected) v = ρ.r324ProjectedCovarianceC ε L (v (r324ResidualMarkedLowerEndpoint selected) - v (r324ResidualMarkedUpperEndpoint π selected)) * ∏ i ∈ {i ∈ r324MarkedResidualBlock κp κm π selected | i < (momentCombinedPairing κp κm π) i}.erase (r324ResidualMarkedLowerEndpoint selected), ↑(ρ.etaEpsT4 ε (v i - v ((momentCombinedPairing κp κm π) i)))

The genuine marked block contains exactly the selected projected cross covariance; every other covariance in that block is still the complete physical covariance.

theorem Anderson4D.r324ResidualMarkedEndpoints_not_mem_otherBlock {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (B : Finset (Fin (2 * m))) (hB : B ∈ nonemptyMomentResidualCollapseBlocks κp κm π) (hne : B ≠ r324MarkedResidualBlock κp κm π selected) : r324ResidualMarkedLowerEndpoint selected ∉ B ∧ r324ResidualMarkedUpperEndpoint π selected ∉ B

Every other residual block contains neither endpoint of the selected cross covariance.

Exact one-step preservation

theorem Anderson4D.SmoothCutoff.r324MarkedResidualCollapseStep_unmarked {m : ℕ} (ρ : SmoothCutoff) (ε L : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (B : Finset (Fin (2 * m))) (rest : List (Finset (Fin (2 * m)))) (hdisjoint : Disjoint B (finsetUnionList rest)) (hB : r324ResidualMarkedLowerEndpoint selected ∉ B) (v : Fin (2 * m) → T4) : ρ.r324MarkedPairingCovarianceProductOn ε L (momentCombinedPairing κp κm π) (r324ResidualMarkedLowerEndpoint selected) (finsetUnionList (B :: rest)) v = ↑(pairingCovarianceProductOn ρ ε (momentCombinedPairing κp κm π) B v) * ρ.r324MarkedPairingCovarianceProductOn ε L (momentCombinedPairing κp κm π) (r324ResidualMarkedLowerEndpoint selected) (finsetUnionList rest) v

If the next residual block is unmarked, its covariance factor is complete and the unique projected factor remains on the tail.

theorem Anderson4D.SmoothCutoff.r324MarkedResidualCollapseStep_marked {m : ℕ} (ρ : SmoothCutoff) (ε L : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (B : Finset (Fin (2 * m))) (rest : List (Finset (Fin (2 * m)))) (hdisjoint : Disjoint B (finsetUnionList rest)) (hB : r324ResidualMarkedLowerEndpoint selected ∈ B) (v : Fin (2 * m) → T4) : ρ.r324MarkedPairingCovarianceProductOn ε L (momentCombinedPairing κp κm π) (r324ResidualMarkedLowerEndpoint selected) (finsetUnionList (B :: rest)) v = ρ.r324MarkedPairingCovarianceProductOn ε L (momentCombinedPairing κp κm π) (r324ResidualMarkedLowerEndpoint selected) B v * ↑(pairingCovarianceProductOn ρ ε (momentCombinedPairing κp κm π) (finsetUnionList rest) v)

If the next residual block carries the marker, its tail is literally the complete unprojected covariance product. Thus the marked factor is consumed once and cannot be duplicated by later primitive collapses.

theorem Anderson4D.SmoothCutoff.r324MarkedResidualBlockFactor_eq_complete_of_ne {m : ℕ} (ρ : SmoothCutoff) (ε L : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (B : Finset (Fin (2 * m))) (hB : B ∈ nonemptyMomentResidualCollapseBlocks κp κm π) (hne : B ≠ r324MarkedResidualBlock κp κm π selected) (v : Fin (2 * m) → T4) : ρ.r324MarkedPairingCovarianceProductOn ε L (momentCombinedPairing κp κm π) (r324ResidualMarkedLowerEndpoint selected) B v = ↑(pairingCovarianceProductOn ρ ε (momentCombinedPairing κp κm π) B v)

On every genuine residual block other than the unique marked one, all covariances remain the complete physical etaEpsT4 factors.