recoverEps
plain-language theorem explainer
recoverEps extracts the vertex log-potential ε_i from a conformal edge-length field L by taking the natural logarithm of the ratio of the self-loop length L_ii to the base spacing. It is invoked when building the cubic deficit functional that discharges the Regge linearization hypothesis on cubic lattices. The definition is a direct one-line computation inverting the conformal ansatz L_ii = a exp(ε_i).
Claim. Given an edge-length field $L$ on $n$ vertices with positive base spacing $a$, the recovered potential at index $i$ is defined by $ε_i := log(L(i,i)/a)$.
background
An EdgeLengthField on $n$ vertices consists of a positive base spacing $a$ together with a symmetric positive length map $L : Fin n → Fin n → ℝ$ obeying $L(i,j)=L(j,i)$ and $L(i,j)>0$ for all indices. The canonical conformal construction sets $L(i,j)=a exp((ε_i + ε_j)/2)$ for a log-potential $ε$, reducing to the constant $a$ when $ε≡0$ (flat vacuum). This definition lives inside the CubicDeficitDischarge module, whose purpose is to discharge the ReggeDeficitLinearizationHypothesis unconditionally for the RS-canonical cubic lattice presentation as Phase A of the program to promote the paper's Theorem 5.1 from pattern-matching to a Lean theorem.
proof idea
The definition is a one-line wrapper that applies the real logarithm to the ratio of the diagonal entry L.length i i to the base spacing L.base_spacing, directly inverting the exponential factor in the conformal ansatz.
why it matters
recoverEps supplies the ε_i values required to evaluate cubicDeficit at each hinge, which in turn feeds the cubicDeficit and cubicDeficit_singleton constructions. These discharge the linearization hypothesis so that the paper's Theorem 5.1 (field-curvature identity) follows by invoking field_curvature_identity_under_linearization. It closes Phase A of the four-phase program by providing the exact inversion of the conformal edge-length ansatz inside the simplicial ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.