The comparison density rhoA a (the proof notes (8′), (11′), (15′)).

rhoA a = ∫ g(c) ρ_c dc (CIntegrals); Tonelli/Fubini in (t, c) turns ∫ φ · rhoA into ∫ g(c) ∫ φ · ρ_c. With the per-component potentials (Poisson) and the g-integrals of kC, wC this gives 2L − W = ℓ on [-a, a], 2L − W ≤ ℓ everywhere, and 2I − W = ℓ, ℓ = ellA a, when massA a = 1.

theorem Zeta32.Analytic.EnergyI.rhoC_nonneg {a : ℝ} (ha : 0 < a) {c : ℝ} (hc : 0 ≤ c) (t : ℝ) : 0 ≤ rhoC a c t

theorem Zeta32.Analytic.EnergyI.measurable_rhoC (a : ℝ) : Measurable fun (p : ℝ × ℝ) => rhoC a p.2 p.1

theorem Zeta32.Analytic.EnergyI.mass_rhoC {a : ℝ} (ha : 0 < a) {c : ℝ} (hc : 0 < c) : ∫ (t : ℝ) in -a..a, rhoC a c t = (1 - c / uC a c) / 2

Mass of the component: ∫ ρ_c = (1 − c/u_c)/2.

theorem Zeta32.Analytic.EnergyI.ae_good {a : ℝ} : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (-a) a), t ≠ 0 ∧ |t| < a

theorem Zeta32.Analytic.EnergyI.intervalIntegral_eq_Ioo {a : ℝ} (f : ℝ → ℝ) (ha : 0 < a) : ∫ (t : ℝ) in -a..a, f t = ∫ (t : ℝ) in Set.Ioo (-a) a, f t

theorem Zeta32.Analytic.EnergyI.fubini_rhoA {a : ℝ} (ha : 0 < a) (φ : ℝ → ℝ) (hφm : Measurable φ) (hφ : IntervalIntegrable (fun (t : ℝ) => |φ t| * rhoA a t) MeasureTheory.volume (-a) a) : MeasureTheory.IntegrableOn (fun (c : ℝ) => gtil c * ∫ (t : ℝ) in -a..a, φ t * rhoC a c t) (Set.Ioi 0) MeasureTheory.volume ∧ ∫ (t : ℝ) in -a..a, φ t * rhoA a t = ∫ (c : ℝ) in Set.Ioi 0, gtil c * ∫ (t : ℝ) in -a..a, φ t * rhoC a c t

Fubini in (t, c): ∫ φ · rhoA = ∫ g(c) ∫ φ · ρ_c.

theorem Zeta32.Analytic.EnergyI.mass_rhoA {a : ℝ} (ha : 0 < a) : ∫ (t : ℝ) in -a..a, rhoA a t = massA a

theorem Zeta32.Analytic.EnergyI.potA_eq_integral {a : ℝ} (ha : 0 < a) (x : ℝ) : MeasureTheory.IntegrableOn (fun (c : ℝ) => gtil c * potC a c x) (Set.Ioi 0) MeasureTheory.volume ∧ potA a x = ∫ (c : ℝ) in Set.Ioi 0, gtil c * potC a c x

theorem Zeta32.Analytic.EnergyI.exists_massA_eq_one : ∃ (a : ℝ), 0 < a ∧ massA a = 1

The mass equation has a positive root.

theorem Zeta32.Analytic.EnergyI.rhoA_good {a : ℝ} (ha : 0 < a) (hm : massA a = 1) : GoodDensity (rhoA a) a

theorem Zeta32.Analytic.EnergyI.potA_eq {a : ℝ} (ha : 0 < a) (hm : massA a = 1) {x : ℝ} (hx : |x| ≤ a) : 2 * potA a x = ellA a + Wt |x|

(8′) on the support: 2L − W = ℓ.

theorem Zeta32.Analytic.EnergyI.potA_le {a : ℝ} (ha : 0 < a) (hm : massA a = 1) (x : ℝ) : 2 * potA a x ≤ ellA a + Wt |x|

(8′) everywhere: 2L − W ≤ ℓ.

theorem Zeta32.Analytic.EnergyI.potA_le_log {a : ℝ} (ha : 0 < a) (hm : massA a = 1) (x : ℝ) : potA a x ≤ Real.log (|x| + a)

Crude growth of the potential.

theorem Zeta32.Analytic.EnergyI.intervalIntegrable_Wt_abs_rhoA {a : ℝ} (ha : 0 < a) : IntervalIntegrable (fun (x : ℝ) => Wt |x| * rhoA a x) MeasureTheory.volume 0 a

theorem Zeta32.Analytic.EnergyI.IA_eq {a : ℝ} (ha : 0 < a) (hm : massA a = 1) : 2 * IA a = ellA a + 2 * ∫ (x : ℝ) in 0..a, Wt x * rhoA a x

(15′): 2I − W = ℓ, with W = 2∫₀^a Wt·rhoA.