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