Finiteness of the marked-residual physical complement

The marked-mode bridge leaves every covariance except the selected open edge in physical space. This file proves that the resulting complement has finite L¹ mass on every genuine selected cell.

The proof does not expand those covariances. Instead, it expands only the finite Green-difference product. Each resulting summand is an increasing Green tree on the internal vertices, hence is integrable by integrable_increasingTreeGreenProduct; the remaining physical covariances are bounded at every fixed positive mollifier scale.

The internal Green tree carried by one expanded branch

def Anderson4D.r324InteriorFullEdge (n : ℕ) (i : Fin (n + 1)) : Fin (n + 2 + 1)

The full chain edge corresponding to an internal edge.

Equations

• Anderson4D.r324InteriorFullEdge n i = ⟨↑i + 1, ⋯⟩

noncomputable def Anderson4D.r324InteriorShortcutParent {n : ℕ} (κ : PartialPairing (Fin (n + 2))) (i : Fin (n + 1)) (hi : r324InteriorFullEdge n i ∈ extractedRightEdges κ) : Fin (↑i + 1)

The internal parent of a shortcut edge.

Equations

• Anderson4D.r324InteriorShortcutParent κ i hi = ⟨↑(Anderson4D.extractedPairOfRightEdge κ (Anderson4D.r324InteriorFullEdge n i) hi).1, ⋯⟩

noncomputable def Anderson4D.r324InteriorExpandedTreeParent {n : ℕ} (κ : PartialPairing (Fin (n + 2))) (original : Finset (Fin (n + 1))) : IncreasingTreeParent (n + 1)

Parent map of one branch of the internal Green-difference product.

Equations

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

noncomputable def Anderson4D.r324InteriorOriginalGreenEdge {n : ℕ} (v : Fin (n + 2) → T4) (i : Fin (n + 1)) : ℂ

Original full-chain factor at an internal edge.

Equations

• Anderson4D.r324InteriorOriginalGreenEdge v i = Anderson4D.originalGreenEdge (Anderson4D.assemble 0 0 v) (Anderson4D.r324InteriorFullEdge n i)

noncomputable def Anderson4D.r324InteriorShortcutGreenEdge {n : ℕ} (κ : PartialPairing (Fin (n + 2))) (v : Fin (n + 2) → T4) (i : Fin (n + 1)) : ℂ

Shortcut factor at an internal edge, zero if no shortcut exists.

Equations

• Anderson4D.r324InteriorShortcutGreenEdge κ v i = Anderson4D.extractedShortcutGreenEdge κ (Anderson4D.assemble 0 0 v) (Anderson4D.r324InteriorFullEdge n i)

noncomputable def Anderson4D.r324InteriorExpandedGreenBranch {n : ℕ} (κ : PartialPairing (Fin (n + 2))) (original : Finset (Fin (n + 1))) (v : Fin (n + 2) → T4) : ℂ

One branch in the internal product-of-sums expansion.

Equations

• Anderson4D.r324InteriorExpandedGreenBranch κ original v = (∏ i ∈ original, Anderson4D.r324InteriorOriginalGreenEdge v i) * ∏ i ∈ originalᶜ, Anderson4D.r324InteriorShortcutGreenEdge κ v i

theorem Anderson4D.r324InteriorExpandedGreenBranch_eq_tree {n : ℕ} (κ : PartialPairing (Fin (n + 2))) (original : Finset (Fin (n + 1))) (hshortcut : ∀ i ∉ original, r324InteriorFullEdge n i ∈ extractedRightEdges κ) : r324InteriorExpandedGreenBranch κ original = increasingTreeGreenProduct (r324InteriorExpandedTreeParent κ original)

A nonzero internal branch is exactly an increasing Green tree.

theorem Anderson4D.integrable_r324InteriorExpandedGreenBranch {n : ℕ} (κ : PartialPairing (Fin (n + 2))) (original : Finset (Fin (n + 1))) : MeasureTheory.Integrable (r324InteriorExpandedGreenBranch κ original) (MeasureTheory.Measure.pi fun (x : Fin (n + 2)) => paperMeasure)

Every internal branch is integrable.

Integrability of the endpoint-independent Green profile

noncomputable def Anderson4D.r324InteriorExpandedGreenMajorant {n : ℕ} (κ : PartialPairing (Fin (n + 2))) (v : Fin (n + 2) → T4) : ℂ

The product-of-sums majorant for the internal Green differences.

Equations

• Anderson4D.r324InteriorExpandedGreenMajorant κ v = ∏ i : Fin (n + 1), (Anderson4D.r324InteriorOriginalGreenEdge v i + Anderson4D.r324InteriorShortcutGreenEdge κ v i)

theorem Anderson4D.r324InteriorExpandedGreenMajorant_eq_sum_branches {n : ℕ} (κ : PartialPairing (Fin (n + 2))) : r324InteriorExpandedGreenMajorant κ = fun (v : Fin (n + 2) → T4) => ∑ original : Finset (Fin (n + 1)), r324InteriorExpandedGreenBranch κ original v

theorem Anderson4D.integrable_r324InteriorExpandedGreenMajorant {n : ℕ} (κ : PartialPairing (Fin (n + 2))) : MeasureTheory.Integrable (r324InteriorExpandedGreenMajorant κ) (MeasureTheory.Measure.pi fun (x : Fin (n + 2)) => paperMeasure)

theorem Anderson4D.r324RenormalizedInteriorCore_eq_internalDifferenceProduct {n : ℕ} (κ : PartialPairing (Fin (n + 2))) (v : Fin (n + 2) → T4) : r324RenormalizedInteriorCore κ v = ∏ i : Fin (n + 1), (r324InteriorOriginalGreenEdge v i - r324InteriorShortcutGreenEdge κ v i)

The erased external-edge product is the standard internal-edge product.

theorem Anderson4D.norm_r324RenormalizedInteriorCore_le_internalMajorant {n : ℕ} (κ : PartialPairing (Fin (n + 2))) (v : Fin (n + 2) → T4) : ‖r324RenormalizedInteriorCore κ v‖ ≤ ‖r324InteriorExpandedGreenMajorant κ v‖

theorem Anderson4D.integrable_r324RenormalizedInteriorCore {m : ℕ} (κ : PartialPairing (Fin m)) : MeasureTheory.Integrable (r324RenormalizedInteriorCore κ) (MeasureTheory.Measure.pi fun (x : Fin m) => paperMeasure)

Every endpoint-independent renormalized interior profile is jointly integrable.

theorem Anderson4D.SmoothCutoff.integrable_r324SelectedInteriorSkeletonNormDensity {m : ℕ} (κp κm : PartialPairing (Fin m)) : MeasureTheory.Integrable (r324SelectedInteriorSkeletonNormDensity κp κm) (MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure)

The two independent endpoint-free Green profiles have integrable norm on the doubled internal space.

Boundedness of the unexpanded physical covariances

theorem Anderson4D.SmoothCutoff.exists_r324MarkedResidualPhysicalCovarianceFactor_bound (ρ : SmoothCutoff) {m : ℕ} {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) : ∃ (B : ℝ), 0 ≤ B ∧ ∀ (v : Fin (2 * m) → T4), ρ.r324MarkedResidualBlockUnselectedCovarianceMass ε κp κm π selected v * ‖ρ.r324UnmarkedResidualBlockProduct ε κp κm π selected v‖ ≤ B

At each fixed positive mollifier scale, the complete collection of unexpanded covariances left after deleting the selected edge is uniformly bounded in the spatial variables.

Genuine selected-cell complement finiteness

theorem Anderson4D.SmoothCutoff.integrable_r324MarkedResidualPhysicalComplementMass (ρ : SmoothCutoff) {m : ℕ} {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) : MeasureTheory.Integrable (ρ.r324MarkedResidualPhysicalComplementMass ε κp κm π selected) (MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure)

The physical complement is globally integrable at each fixed positive mollifier scale. No covariance has been Fourier-expanded in this proof.

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

The extended physical-complement mass on every genuine selected cell is finite. This discharges the qualitative hypothesis of the marked-mode Tonelli bridge.

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

Consequently, the complete marked Fourier-mode family is absolutely summable after integration on every genuine selected cell.