Energy Positivity — Remark 4

Sharpens the indicator energy criterion (Lemma 7) to rule out the conull case by proving E_λ(1) > 0. The archimedean energy integral of the constant function is positive because translation by any t ∈ (0, 2L) moves the support boundary, creating a region where 1_I and S_t(1_I) disagree.

Reference: lamportform.tex, Remark 4 (lines 698–723).

Inner integral positivity

theorem ConnesLean.lintegral_indicator_diff_pos {L t : ℝ} (_hL : 0 < L) (ht : 0 < t) (htL : t < 2 * L) : 0 < ∫⁻ (u : ℝ), ↑‖zeroExtend 1 (logInterval L) u - translationOp t (zeroExtend 1 (logInterval L)) u‖₊ ^ 2

For 0 < t < 2L with L > 0, the L² norm of zeroExtend 1 I - S_t(zeroExtend 1 I) is positive. The functions disagree on Ioo (-L) (-L + t).

Archimedean energy positivity

theorem ConnesLean.archEnergyIntegral_one_pos {cutoffLambda : ℝ} (hLam : 1 < cutoffLambda) : 0 < archEnergyIntegral 1 (Real.log cutoffLambda)

The archimedean energy integral of the constant function 1 is positive when cutoffLambda > 1. Each point t ∈ (0, 2L) contributes a positive integrand since archWeight(t) > 0 and the inner integral is positive.

Energy form positivity

theorem ConnesLean.energyForm_one_pos {cutoffLambda : ℝ} (hLam : 1 < cutoffLambda) : 0 < energyForm cutoffLambda 1

The energy form of the constant function 1 is positive: E_λ(1) > 0. This is the key fact that rules out the conull case in the indicator energy criterion.

Conull indicator has the same energy as 1

theorem ConnesLean.zeroExtend_indicator_ae_eq_of_conull {B : Set ℝ} {L : ℝ} (_hB_sub : B ⊆ logInterval L) (hB_conull : MeasureTheory.volume (logInterval L \ B) = 0) : zeroExtend (B.indicator 1) (logInterval L) =ᵐ[MeasureTheory.volume] zeroExtend 1 (logInterval L)

If B is conull in I, zero-extending 1_B and 1 over I are ae-equal. The disagreement set is contained in I \ B, which has measure zero.

theorem ConnesLean.energyForm_indicator_eq_one_of_conull {cutoffLambda : ℝ} {B : Set ℝ} (hB_sub : B ⊆ logInterval (Real.log cutoffLambda)) (hB_conull : MeasureTheory.volume (logInterval (Real.log cutoffLambda) \ B) = 0) : energyForm cutoffLambda (B.indicator 1) = energyForm cutoffLambda 1

If B is conull in I, then E_λ(1_B) = E_λ(1). The ae-equality of the zero-extended functions propagates through the energy form via lintegral_congr_ae.

Main theorem

theorem ConnesLean.energyForm_indicator_null {cutoffLambda : ℝ} {B : Set ℝ} (hLam : 1 < cutoffLambda) (hB_meas : MeasurableSet B) (hB_sub : B ⊆ logInterval (Real.log cutoffLambda)) (h_energy : energyForm cutoffLambda (B.indicator 1) = 0) : MeasureTheory.volume B = 0

Remark 4 (Energy positivity): If E_λ(1_B) = 0 for measurable B ⊆ I, then volume B = 0.

Combines energyForm_indicator_null_or_conull (Lemma 7) with energyForm_one_pos to rule out the conull case: if B were conull, then E_λ(1_B) = E_λ(1) > 0, contradicting E_λ(1_B) = 0.

Reference: lamportform.tex, Remark 4 (lines 698–723).