A marked residual physical interior object before Fourier expansion

This module stays on the physical-covariance side of the R-324 argument. It packages the two signed renormalized interior Green profiles with the residual physical covariance product containing one projected cross edge, then factors the genuine residual schedule without duplicating that marker.

This packaging is an interface object rather than a phase-A closure theorem; no equality with the original pre-collapse physical core is asserted here.

This object is deliberately distinct from r324SelectedInteriorSkeletonCellMass. In that later object every covariance has already been Fourier-expanded and its fixed coefficient has been pulled outside the spatial integral. A representation-order bridge collapses first and then expands only the surviving marked edge; the two cell masses are deliberately kept distinct here.

A signed marked-residual interface object

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

Candidate physical interior object at the residual-active interface. No theorem here claims that phase A has already produced this object, and no norm has yet been taken.

Equations

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

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

The same signed core after the exact residual schedule factorization. The unique marked primitive block stays visible; every other residual block carries its complete physical covariance product.

Equations

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

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

Exact marker-preserving residual collapse while both Green profiles remain signed.

Pointwise analytic ledger with one open block

theorem Anderson4D.SmoothCutoff.norm_r324MarkedResidualPhysicalInteriorCore_eq_markedBlock (ρ : SmoothCutoff) {m : ℕ} (ε L : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (v : Fin (2 * m) → T4) : ‖ρ.r324MarkedResidualPhysicalInteriorCore ε L κp κm π selected v‖ = r324SelectedInteriorSkeletonNormDensity κp κm v * ‖ρ.r324MarkedPairingCovarianceProductOn ε L (momentCombinedPairing κp κm π) (r324ResidualMarkedLowerEndpoint selected) (r324MarkedResidualBlock κp κm π selected) v‖ * ‖ρ.r324UnmarkedResidualBlockProduct ε κp κm π selected v‖

Exact norm ledger after the residual collapse. This is the first nonnegative form: the marked block is not estimated or replaced.

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

Expanding only the surviving marked block exposes precisely one projected open edge and leaves every other covariance physical.

The genuine selected internal cell

noncomputable def Anderson4D.SmoothCutoff.r324MarkedResidualPhysicalInteriorCellMass (ρ : SmoothCutoff) {m : ℕ} (ε L : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (hε : 0 < ε) (cell : Fin (2 * m) → Z4) : ℝ

Physical marked-residual interface mass on the same genuine open-edge cell used by the endpoint-first representation.

Equations

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

theorem Anderson4D.SmoothCutoff.r324MarkedResidualPhysicalInteriorCellMass_nonneg (ρ : SmoothCutoff) {m : ℕ} (ε L : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (hε : 0 < ε) (cell : Fin (2 * m) → Z4) : 0 ≤ ρ.r324MarkedResidualPhysicalInteriorCellMass ε L κp κm π selected hε cell

theorem Anderson4D.SmoothCutoff.r324MarkedResidualPhysicalInteriorCellMass_eq_projectedEdge (ρ : SmoothCutoff) {m : ℕ} (ε L : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (hε : 0 < ε) (cell : Fin (2 * m) → Z4) : ρ.r324MarkedResidualPhysicalInteriorCellMass ε L κp κm π selected hε cell = ∫ (v : Fin (2 * m) → T4) in r324SelectedInternalCell κp κm π selected ε hε cell, r324SelectedInteriorSkeletonNormDensity κp κm v * ‖ρ.r324ProjectedCovarianceC ε L (v (r324ResidualMarkedLowerEndpoint selected) - v (r324ResidualMarkedUpperEndpoint π selected))‖ * ρ.r324MarkedResidualBlockUnselectedCovarianceMass ε κp κm π selected v * ‖ρ.r324UnmarkedResidualBlockProduct ε κp κm π selected v‖ ∂MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure

Exact cellwise ledger after all unmarked residual factors have been separated and only the projected edge remains distinguished.