Cell integration after expanding only the marked residual edge

This file integrates the one-mode estimate from R324MarkedResidualPhysicalBridge on the genuine selected internal cell. Every unmarked covariance stays in physical space. The masses are stated as nonnegative extended integrals, so this Tonelli-safe step keeps the Proposition 4.1 block collapse explicit as a separate premise.

Measurability of the physical complement

theorem Anderson4D.SmoothCutoff.measurable_r324MarkedResidualBlockUnselectedCovarianceMass (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) : Measurable fun (v : Fin (2 * m) → T4) => ρ.r324MarkedResidualBlockUnselectedCovarianceMass ε κp κm π selected v

theorem Anderson4D.SmoothCutoff.measurable_r324UnmarkedResidualBlockProduct (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) : Measurable fun (v : Fin (2 * m) → T4) => ρ.r324UnmarkedResidualBlockProduct ε κp κm π selected v

theorem Anderson4D.SmoothCutoff.measurable_r324MarkedResidualPhysicalComplementMass (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) : Measurable fun (v : Fin (2 * m) → T4) => ρ.r324MarkedResidualPhysicalComplementMass ε κp κm π selected v

Exact one-mode norm ledger

noncomputable def Anderson4D.SmoothCutoff.r324MarkedResidualHighModeCoefficientNorm (ρ : SmoothCutoff) (ε L : ℝ) (k : Z4) : ℝ

Norm of one retained covariance coefficient. Evaluating the spatial mode at zero makes the coefficient nature explicit.

Equations

• ρ.r324MarkedResidualHighModeCoefficientNorm ε L k = ‖ρ.r324HighCovarianceModeTerm ε L 0 k‖

theorem Anderson4D.SmoothCutoff.r324MarkedResidualHighModeCoefficientNorm_nonneg (ρ : SmoothCutoff) (ε L : ℝ) (k : Z4) : 0 ≤ ρ.r324MarkedResidualHighModeCoefficientNorm ε L k

theorem Anderson4D.SmoothCutoff.r324MarkedResidualHighModeCoefficientNorm_eq_covarianceModeCoeff (ρ : SmoothCutoff) {ε L : ℝ} {k : Z4} (hk : k ∈ r324HighModeSet ε L) : ρ.r324MarkedResidualHighModeCoefficientNorm ε L k = ‖ρ.covarianceModeCoeff ε k‖

theorem Anderson4D.SmoothCutoff.summable_r324MarkedResidualHighModeCoefficientNorm (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (L : ℝ) : Summable (ρ.r324MarkedResidualHighModeCoefficientNorm ε L)

theorem Anderson4D.SmoothCutoff.norm_r324HighCovarianceModeTerm_eq_coefficientNorm (ρ : SmoothCutoff) (ε L : ℝ) (z : T4) (k : Z4) : ‖ρ.r324HighCovarianceModeTerm ε L z k‖ = ρ.r324MarkedResidualHighModeCoefficientNorm ε L k

theorem Anderson4D.SmoothCutoff.norm_r324MarkedResidualPhysicalOpenEdgeAmplitude (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (v : Fin (2 * m) → T4) : ‖ρ.r324MarkedResidualPhysicalOpenEdgeAmplitude ε κp κm π selected v‖ = ρ.r324MarkedResidualPhysicalComplementMass ε κp κm π selected v

theorem Anderson4D.SmoothCutoff.norm_r324MarkedResidualPhysicalInteriorModeTerm_eq (ρ : SmoothCutoff) {m : ℕ} (ε L : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (v : Fin (2 * m) → T4) (k : Z4) : ‖ρ.r324MarkedResidualPhysicalInteriorModeTerm ε L κp κm π selected v k‖ = ρ.r324MarkedResidualHighModeCoefficientNorm ε L k * ρ.r324MarkedResidualPhysicalComplementMass ε κp κm π selected v

theorem Anderson4D.SmoothCutoff.measurable_norm_r324MarkedResidualPhysicalInteriorModeTerm (ρ : SmoothCutoff) {m : ℕ} (ε L : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (k : Z4) : Measurable fun (v : Fin (2 * m) → T4) => ‖ρ.r324MarkedResidualPhysicalInteriorModeTerm ε L κp κm π selected v k‖

Tonelli-safe cell masses

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

Extended L¹ mass of one marked Fourier mode on a genuine selected internal cell.

Equations

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

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

Extended physical-complement mass on the same genuine selected cell. Its finiteness is exactly the analytic input still supplied by the within-half Proposition 4.1 collapse.

Equations

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

theorem Anderson4D.SmoothCutoff.r324MarkedResidualPhysicalInteriorModeCellLIntegral_eq (ρ : SmoothCutoff) {m : ℕ} (ε L : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (hε : 0 < ε) (cell : Fin (2 * m) → Z4) (k : Z4) : ρ.r324MarkedResidualPhysicalInteriorModeCellLIntegral ε L κp κm π selected hε cell k = ENNReal.ofReal (ρ.r324MarkedResidualHighModeCoefficientNorm ε L k) * ρ.r324MarkedResidualPhysicalComplementCellLIntegral ε κp κm π selected hε cell

Exact separation of the retained coefficient from the physical complement on one selected cell.

The integrated central-frequency payoff

theorem Anderson4D.SmoothCutoff.exists_r324MarkedResidualPhysicalInteriorModeCellLIntegral_le (ρ : SmoothCutoff) : ∃ (C : ℝ), 0 < C ∧ ∀ {m : ℕ} {ε L : ℝ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} {selected : R324ResidualCovarianceSlot κp} {hε : 0 < ε} {cell : Fin (2 * m) → Z4} {k : Z4}, ε ≤ 1 / 4 → 0 ≤ L → ρ.r324MarkedResidualPhysicalInteriorModeCellLIntegral ε L κp κm π selected hε cell k ≤ ENNReal.ofReal (C * eighthOrderFrequencyDecay (ε ^ 2 * L)) * ρ.r324MarkedResidualPhysicalComplementCellLIntegral ε κp κm π selected hε cell

The paper's uniform eighth-order payoff survives integration over every genuine selected internal cell, while the complete unmarked physical covariance structure stays inside the complement mass.

Absolute mode summation on the cell

theorem Anderson4D.SmoothCutoff.lintegral_tsum_norm_r324MarkedResidualPhysicalInteriorModeTerm (ρ : SmoothCutoff) {m : ℕ} (ε L : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (hε : 0 < ε) (cell : Fin (2 * m) → Z4) : (∫⁻ (v : Fin (2 * m) → T4) in r324SelectedInternalCell κp κm π selected ε hε cell, ∑' (k : Z4), ENNReal.ofReal ‖ρ.r324MarkedResidualPhysicalInteriorModeTerm ε L κp κm π selected v k‖ ∂MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure) = ∑' (k : Z4), ρ.r324MarkedResidualPhysicalInteriorModeCellLIntegral ε L κp κm π selected hε cell k

Tonelli exchange for the absolute one-marked-edge mode family. It is valid before the physical complement is known finite.

theorem Anderson4D.SmoothCutoff.tsum_r324MarkedResidualPhysicalInteriorModeCellLIntegral (ρ : SmoothCutoff) {m : ℕ} (ε L : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (hε : 0 < ε) (cell : Fin (2 * m) → Z4) : ∑' (k : Z4), ρ.r324MarkedResidualPhysicalInteriorModeCellLIntegral ε L κp κm π selected hε cell k = (∑' (k : Z4), ENNReal.ofReal (ρ.r324MarkedResidualHighModeCoefficientNorm ε L k)) * ρ.r324MarkedResidualPhysicalComplementCellLIntegral ε κp κm π selected hε cell

Exact factorization of the total absolute mode mass.

theorem Anderson4D.SmoothCutoff.tsum_ofReal_r324MarkedResidualHighModeCoefficientNorm_lt_top (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (L : ℝ) : ∑' (k : Z4), ENNReal.ofReal (ρ.r324MarkedResidualHighModeCoefficientNorm ε L k) < ⊤

The retained coefficient series has finite extended mass.

theorem Anderson4D.SmoothCutoff.tsum_r324MarkedResidualPhysicalInteriorModeCellLIntegral_lt_top (ρ : SmoothCutoff) {m : ℕ} {ε L : ℝ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (hε : 0 < ε) (cell : Fin (2 * m) → Z4) (hcomplement : ρ.r324MarkedResidualPhysicalComplementCellLIntegral ε κp κm π selected hε cell < ⊤) : ∑' (k : Z4), ρ.r324MarkedResidualPhysicalInteriorModeCellLIntegral ε L κp κm π selected hε cell k < ⊤

Finite complement mass implies absolute summability of the integrated marked-mode family.

Interface to the existing primitive-word consumer

theorem Anderson4D.SmoothCutoff.exists_r324MarkedResidualHighModePrimitiveConsumer (ρ : SmoothCutoff) : ∃ (C : ℝ), 0 < C ∧ ∀ {t : PlaneTree} {m M : ℕ} {κ : PartialPairing (Fin m)} {a b : Fin m} {w : Fin m → HeppLeaf t} {Nm : t.HeppMarking} {z : HeppLeaf t → Fin 4 → ℤ} {ε L : ℝ} {k : Z4}, 0 < m → κ a = b → a < b → κ.IsFull → IsPrimitive κ → (∀ (i : Fin m), i ≠ a → i ≠ b → w i = w (κ i)) → IsAdmissible Nm M z → 0 < ε → ε ≤ 1 / 4 → 0 ≤ L → 1 ≤ ε ^ 2 * L → k ∈ r324HighModeSet ε L → ↑M ≤ ε⁻¹ → NoProperLeafBlock (openEdgeAugmentedWord w a b) ∧ ρ.r324MarkedResidualHighModeCoefficientNorm ε L k * heppChainWeight z w ≤ C * eighthOrderFrequencyDecay (ε ^ 2 * L) * heppChainWeight z (openEdgeAugmentedWord w a b)

The exact coefficient extracted by the physical marked-edge bridge feeds the already proved one-open-edge primitive consumer.