Proved solution

The substantive proof development is in the lean/ directory. This module exposes the same declarations as Challenge.lean and connects them to the machine-checked flat-coordinate and fork-packing theorems.

theorem PalomarHS.main_result {k d : ℕ} (hk : 2 ≤ k) : have x := ⋯; ↑k.factorial * |HsVirial.hardSphereBk| = ∑ T ∈ HsVirial.treeUniverse, HsVirial.hardSphereNBCVolumeFlat T

theorem PalomarHS.signed_coefficient_sign {k d : ℕ} (hk : 2 ≤ k) : have x := ⋯; HsVirial.hardSphereBk = (-1) ^ (k - 1) * |HsVirial.hardSphereBk|

theorem PalomarHS.nbc_region_measure_le_fork_avoidance {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} {P : Finset (HsVirial.HardSphereForkTriple k)} (hP : HsVirial.hardSphereForkPacking T P) : MeasureTheory.volume (HsVirial.nbcRegion HsVirial.hardSphereActiveExact T) ≤ MeasureTheory.volume (HsVirial.hardSphereForkAvoidanceRegion T P)

theorem PalomarHS.nbc_region_subset_fork_packing_separated {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} {P : Finset (HsVirial.HardSphereForkTriple k)} (hP : HsVirial.hardSphereForkPacking T P) : HsVirial.nbcRegion HsVirial.hardSphereActiveExact T ⊆ HsVirial.hardSphereForkPackingSeparatedRegion P

theorem PalomarHS.fork_packing_two_mul_card_le_pred {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} {P : Finset (HsVirial.HardSphereForkTriple k)} (hP : HsVirial.hardSphereForkPacking T P) : 2 * P.card ≤ k - 1

theorem PalomarHS.nbc_region_real_volume_le_kappa {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} (hT : T ∈ HsVirial.treeUniverse) : MeasureTheory.volume.real (HsVirial.nbcRegion HsVirial.hardSphereActiveExact T) ≤ HsVirial.hardSphereKappa ^ (k - 1)

theorem PalomarHS.nbc_region_real_volume_le_fork_factor {k : ℕ} [NeZero k] {T : Finset (Sym2 (Fin k))} (hT : T ∈ HsVirial.treeUniverse) : HsVirial.hardSphereNBCVolume T ≤ (17 / 32) ^ HsVirial.hardSphereNu T * HsVirial.hardSphereKappa ^ (k - 1)

theorem PalomarHS.close_pair_real_volume : MeasureTheory.volume.real HsVirial.hardSphereClosePairRegion = 5 * Real.pi ^ 2 / 6

theorem PalomarHS.separated_pair_real_volume_ratio : MeasureTheory.volume.real HsVirial.hardSphereSeparatedPairRegion = 17 / 32 * HsVirial.hardSphereKappa ^ 2