Gravity from Information Geometry: A Lean 4 Formalization of Emergent Spacetime | Heykuki News