Norm Inequality for Disjoint Indicators

Establishes that the energy of the constant function is bounded by the sum of energies of complementary indicator functions. This is the key inequality that, combined with the splitting equality from Stage 6C, forces cross-terms to vanish.

Reference: lamportform.tex, Proposition 10, Steps 4–7 (lines 1371–1390).

Section 1: Pointwise norm inequality

For B ⊆ I, the zero-extended indicators satisfy: ‖h̃(u) - h̃(u-t)‖₊² ≤ ‖f̃(u) - f̃(u-t)‖₊² + ‖g̃(u) - g̃(u-t)‖₊² where h̃ = zeroExtend 1 I, f̃ = zeroExtend (1_B) I, g̃ = zeroExtend (1_{I\B}) I.

theorem ConnesLean.nnnorm_sq_indicator_le {B I : Set ℝ} (hB : B ⊆ I) (u t : ℝ) : ↑‖zeroExtend 1 I u - zeroExtend 1 I (u - t)‖₊ ^ 2 ≤ ↑‖zeroExtend (B.indicator 1) I u - zeroExtend (B.indicator 1) I (u - t)‖₊ ^ 2 + ↑‖zeroExtend ((I \ B).indicator 1) I u - zeroExtend ((I \ B).indicator 1) I (u - t)‖₊ ^ 2

Pointwise norm inequality for disjoint indicators. For B ⊆ I, at every point u and shift t: ‖h̃(u) - h̃(u-t)‖₊² ≤ ‖f̃(u) - f̃(u-t)‖₊² + ‖g̃(u) - g̃(u-t)‖₊² where h̃ = zeroExtend 1 I, f̃ = zeroExtend (1_B) I, g̃ = zeroExtend (1_{I\B}) I.

9-case analysis on (u ∈ B, u ∈ I\B, u ∉ I) × (u-t ∈ B, u-t ∈ I\B, u-t ∉ I). Each case computes concrete {0,1} values.

Reference: lamportform.tex, Proposition 10, Step 4 (line 1371).

Section 3: Integrated inequality

theorem ConnesLean.inner_integral_indicator_le {B I : Set ℝ} (hB : B ⊆ I) (hI : MeasurableSet I) (hBm : MeasurableSet B) (t : ℝ) : ∫⁻ (u : ℝ), ↑‖zeroExtend 1 I u - translationOp t (zeroExtend 1 I) u‖₊ ^ 2 ≤ (∫⁻ (u : ℝ), ↑‖zeroExtend (B.indicator 1) I u - translationOp t (zeroExtend (B.indicator 1) I) u‖₊ ^ 2) + ∫⁻ (u : ℝ), ↑‖zeroExtend ((I \ B).indicator 1) I u - translationOp t (zeroExtend ((I \ B).indicator 1) I) u‖₊ ^ 2

The integrated norm inequality: integrating the pointwise inequality gives ∫ ‖h̃ - S_t h̃‖² ≤ ∫ ‖f̃ - S_t f̃‖² + ∫ ‖g̃ - S_t g̃‖².

Reference: lamportform.tex, Proposition 10, Step 5 (line 1378).

Section 4: Weighted inequalities

theorem ConnesLean.archEnergyIntegrand_indicator_le {L : ℝ} {B : Set ℝ} (hB : B ⊆ logInterval L) (hBm : MeasurableSet B) (t : ℝ) : archEnergyIntegrand 1 L t ≤ archEnergyIntegrand (B.indicator 1) L t + archEnergyIntegrand ((logInterval L \ B).indicator 1) L t

Archimedean energy integrand inequality: multiplying by the archimedean weight preserves the inequality.

Reference: lamportform.tex, Proposition 10, Step 6 (line 1382).

theorem ConnesLean.primeEnergyTerm_indicator_le {L : ℝ} {B : Set ℝ} (hB : B ⊆ logInterval L) (hBm : MeasurableSet B) (p m : ℕ) : primeEnergyTerm p m 1 L ≤ primeEnergyTerm p m (B.indicator 1) L + primeEnergyTerm p m ((logInterval L \ B).indicator 1) L

Prime energy term inequality: multiplying by the prime weight preserves the inequality.

Reference: lamportform.tex, Proposition 10, Step 6 (line 1385).

Section 5: Full energy form inequality

theorem ConnesLean.energyForm_indicator_add_le {cutoffLambda : ℝ} (inv : EnergyFormSplit cutoffLambda) : energyForm cutoffLambda 1 ≤ energyForm cutoffLambda (inv.B.indicator 1) + energyForm cutoffLambda ((logInterval (Real.log cutoffLambda) \ inv.B).indicator 1)

Energy form inequality: E_λ(1) ≤ E_λ(1_B) + E_λ(1_{I\B}). Unfolds the energy form and applies the archimedean and prime inequalities.

Combined with the splitting equality E_λ(1) = E_λ(1_B) + E_λ(1_{I\B}) from Stage 6C, this forces cross-terms to vanish.

Reference: lamportform.tex, Proposition 10, Step 7 (line 1388).

Section 6: Soundness tests