Indicator Energy Criterion — Lemma 7

If the energy form vanishes on an indicator 1_B for measurable B ⊆ I, then B is either null or conull. Extracts archimedean and prime energy components, upgrades ae vanishing to pointwise via strong continuity of translations, and applies the null-or-conull theorem from Stage 4.

Reference: lamportform.tex, Lemma 7 (lines 647–696).

Energy form component extraction

theorem ConnesLean.archEnergy_eq_zero_of_energyForm_eq_zero {cutoffLambda : ℝ} {G : ℝ → ℂ} (h : energyForm cutoffLambda G = 0) : archEnergyIntegral G (Real.log cutoffLambda) = 0

If the energy form vanishes, the archimedean energy integral is zero.

theorem ConnesLean.primeEnergy_eq_zero_of_energyForm_eq_zero {cutoffLambda : ℝ} {G : ℝ → ℂ} (h : energyForm cutoffLambda G = 0) (p : ℕ) : p ∈ primeFinset cutoffLambda → totalPrimeEnergy p cutoffLambda G (Real.log cutoffLambda) = 0

If the energy form vanishes, each prime energy term is zero.

theorem ConnesLean.translationOp_normSq_zero_of_weighted_zero {G : ℝ → ℂ} {L t : ℝ} (ht : 0 < t) (h : archEnergyIntegrand G L t = 0) : ∫⁻ (u : ℝ), ↑‖zeroExtend G (logInterval L) u - translationOp t (zeroExtend G (logInterval L)) u‖₊ ^ 2 = 0

If the weighted energy integrand vanishes at a positive time, the norm-squared integral is zero.

theorem ConnesLean.measurable_archWeight_toNNReal : Measurable fun (t : ℝ) => (archWeight t).toNNReal

The map t ↦ (archWeight t).toNNReal is measurable.

Continuity and ae-zero upgrade

theorem ConnesLean.continuous_ae_zero_imp_zero {f : ℝ → ENNReal} {a b : ℝ} (hf : Continuous f) (h_ae : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), f t = 0) (t : ℝ) : t ∈ Set.Ioo a b → f t = 0

A continuous ENNReal-valued function that is ae-zero on an open interval is pointwise zero on that interval.

L² norm zero implies ae equality

theorem ConnesLean.ae_eq_of_lintegral_nnnorm_rpow_zero {f g : ℝ → ℂ} (hf : Measurable f) (hg : Measurable g) (h : ∫⁻ (u : ℝ), ↑‖f u - g u‖₊ ^ 2 = 0) : ∀ᵐ (u : ℝ), f u = g u

If the L² distance (as ∫⁻ ‖f - g‖₊ ^ 2) is zero, then f = g a.e.

Indicator equality conversion (ℂ → ℝ)

theorem ConnesLean.indicator_ae_eq_on_overlap {B : Set ℝ} {L t : ℝ} (h_ae : ∀ᵐ (u : ℝ), zeroExtend (B.indicator 1) (logInterval L) u = zeroExtend (B.indicator 1) (logInterval L) (u - t)) : ∀ᵐ (u : ℝ) ∂MeasureTheory.volume.restrict (logInterval L ∩ (fun (x : ℝ) => x - t) ⁻¹' logInterval L), B.indicator 1 u = B.indicator 1 (u - t)

Convert ae equality of ℂ-valued zero-extended indicators to ae equality of ℝ-valued indicators on the overlap region.

Main theorem

theorem ConnesLean.energyForm_indicator_null_or_conull {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 ∨ MeasureTheory.volume (logInterval (Real.log cutoffLambda) \ B) = 0

Lemma 7 (Indicator Energy Criterion): If E_λ(1_B) = 0 for measurable B ⊆ I, then volume B = 0 or volume (I \ B) = 0.

Reference: lamportform.tex, Lemma 7 (lines 647–696).