recoverEps_conformal
plain-language theorem explainer
The theorem asserts that the recovery map applied to the conformal edge-length field constructed from a log-potential ε returns ε exactly at each vertex index. Researchers discharging the Regge deficit linearization hypothesis for the cubic lattice in Recognition Science cite this identity. The tactic proof unfolds the two definitions, reduces the averaged exponent via ring, cancels the base-spacing factor, and invokes the log-exp identity.
Claim. Let $a > 0$ be the base spacing and let $ε : Fin n → ℝ$ be a log-potential. Define the conformal edge-length field $L$ by $L_{ij} = a · exp((ε_i + ε_j)/2)$. Then the recovery map satisfies $log(L_{ii}/a) = ε_i$.
background
A LogPotential is an assignment ε : Fin n → ℝ with ε_i = ln ψ(σ_i). The conformal edge-length field is the map L_ij = a · exp((ε_i + ε_j)/2) that reduces to the constant spacing a when ε ≡ 0. recoverEps inverts this construction by taking log(L_ii / base_spacing) at each vertex i.
proof idea
The proof unfolds recoverEps and conformal_edge_length_field, then applies simp. It proves the exponential argument equals ε_i by ring arithmetic on the average, cancels the division by a using positivity of a, and finishes with the identity log(exp x) = x.
why it matters
This identity is invoked by the downstream theorem singletonHinge_product that evaluates the area-deficit product on a singleton hinge. It supplies the exact leading-order discharge of the ReggeDeficitLinearizationHypothesis for the cubic lattice, completing Phase A toward the paper's Theorem 5.1 on the field-curvature identity. The result confirms that the quadratic truncation of the deficit matches the Laplacian action exactly under the canonical conformal ansatz.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.