Entanglement = Geometry, kernel-checked: the MERA causal cone is a discrete hyperbolic space

We machine-check in Lean 4 + Mathlib the finite content of Swingle's "MERA = AdS" correspondence — that entanglement is geometry. The MERA causal cone is a binary tree whose graph metric d(s,t) = |s|+|t|−2·lcp(s,t) is proven a genuine metric (symmetry, triangle inequality) satisfying Gromov's four-point condition (0-hyperbolicity), with exponential volume growth (a ball of radius r has 2^(r+1)−1 sites, overtaking the Euclidean (r+1)² at radius 5: 63 > 36). The entanglement side checks the algebraic core of the Ryu–Takayanagi area law (m bonds of dimension D carry D^m configurations), logarithmic depth, and the causal-cone doubling 2^(k+1)=2·2^k. Together these are the discrete signature of a hyperbolic space — the machine-checked form of entanglement = geometry. Not proved: the continuous N→∞ limit to the smooth AdS metric ds² = dr² + sinh²(r) dθ².