Cross-Term Vanishing

From the energy form equality + norm inequality, the inner integrals must agree pointwise. On the overlap region where both u and u-t lie in I, this forces 1_B(u) = 1_B(u-t) a.e., giving translation invariance. The null-or-conull theorem then concludes.

Reference: lamportform.tex, Proposition 10, Steps 9–10 (lines 1400–1425).

Section 1: Pointwise norm equality a.e.

theorem ConnesLean.nnnorm_sq_indicator_ae_eq {cutoffLambda : ℝ} (hLam : 1 < cutoffLambda) (inv : EnergyFormSplit cutoffLambda) {t : ℝ} (ht : t ∈ Set.Ioo 0 (2 * Real.log cutoffLambda)) : ∀ᵐ (u : ℝ), ↑‖zeroExtend 1 (logInterval (Real.log cutoffLambda)) u - zeroExtend 1 (logInterval (Real.log cutoffLambda)) (u - t)‖₊ ^ 2 = ↑‖zeroExtend (inv.B.indicator 1) (logInterval (Real.log cutoffLambda)) u - zeroExtend (inv.B.indicator 1) (logInterval (Real.log cutoffLambda)) (u - t)‖₊ ^ 2 + ↑‖zeroExtend ((logInterval (Real.log cutoffLambda) \ inv.B).indicator 1) (logInterval (Real.log cutoffLambda)) u - zeroExtend ((logInterval (Real.log cutoffLambda) \ inv.B).indicator 1) (logInterval (Real.log cutoffLambda)) (u - t)‖₊ ^ 2

Pointwise norm equality a.e. For each t ∈ (0, 2L): ‖ze(1)(u) - ze(1)(u-t)‖₊² = ‖ze(1_B)(u) - ze(1_B)(u-t)‖₊² + ‖ze(1_{I\B})(u) - ze(1_{I\B})(u-t)‖₊² a.e. in u.

Proof: apply ae_eq_of_ae_le_of_lintegral_le with the pointwise ≤ from nnnorm_sq_indicator_le and the integral equality from inner_integral_indicator_everywhere_eq.

Reference: lamportform.tex, Proposition 10, Step 9 (line 1411).

Section 2: Indicator ae invariance on overlap

theorem ConnesLean.indicator_B_ae_invariant {cutoffLambda : ℝ} (hLam : 1 < cutoffLambda) (inv : EnergyFormSplit cutoffLambda) {t : ℝ} (ht : t ∈ Set.Ioo 0 (2 * Real.log cutoffLambda)) : ∀ᵐ (u : ℝ) ∂MeasureTheory.volume.restrict (logInterval (Real.log cutoffLambda) ∩ (fun (x : ℝ) => x - t) ⁻¹' logInterval (Real.log cutoffLambda)), inv.B.indicator 1 u = inv.B.indicator 1 (u - t)

Indicator ae invariance on overlap. For each t ∈ (0, 2L), 1_B(u) = 1_B(u-t) a.e. on the overlap I ∩ preimage (·-t) I.

On the overlap, ze(1)(u) = 1 and ze(1)(u-t) = 1, so the LHS norm vanishes. The pointwise equality then forces both RHS norms to vanish, giving ze(1_B)(u) = ze(1_B)(u-t), which unfolds to 1_B(u) = 1_B(u-t).

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

Section 3: Translation invariance construction

theorem ConnesLean.indicator_translation_invariant_of_split {cutoffLambda : ℝ} (hLam : 1 < cutoffLambda) (inv : EnergyFormSplit cutoffLambda) : IndicatorTranslationInvariant inv.B (logInterval (Real.log cutoffLambda)) (2 * Real.log cutoffLambda)

Translation invariance of 1_B. Constructs the IndicatorTranslationInvariant hypothesis for inv.B on I = (-L, L) with ε = 2L.

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

Section 4: Null or conull conclusion

theorem ConnesLean.invariant_ideal_null_or_conull {cutoffLambda : ℝ} (hLam : 1 < cutoffLambda) (inv : EnergyFormSplit cutoffLambda) : MeasureTheory.volume inv.B = 0 ∨ MeasureTheory.volume (logInterval (Real.log cutoffLambda) \ inv.B) = 0

Invariant ideal is null or conull. From the translation invariance of 1_B, apply the null-or-conull theorem: either volume B = 0 or volume (I \ B) = 0.

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

Section 5: Soundness tests