conformal_length_sq_exact
plain-language theorem explainer
The exact squared-length identity for the conformal edge ansatz states that the squared length between vertices i and j equals the base spacing squared times the exponential of the sum of the log-potentials at those vertices. Researchers reducing the Regge action to a Dirichlet form on potential differences would cite this identity as the algebraic starting point for the weak-field expansion. The proof is a short tactic sequence that unfolds the edge-length definition and rewrites the square of the exponential using the addition formula.
Claim. Let $a > 0$ be the base spacing and let $ε$ be a log-potential on $n$ vertices. Then the squared length of the conformally rescaled edge between vertices $i$ and $j$ satisfies $ℓ_{ij}^2 = a^2 · exp(ε_i + ε_j)$.
background
The module develops the algebraic reduction of the Regge action under a conformal ansatz for edge lengths. The key definition is the conformal edge length field, which sets the length between vertices i and j to $a · exp((ε_i + ε_j)/2)$, where $a$ is the base spacing and $ε$ is the log-potential. This ansatz is the standard conformal rescaling used when the recognition potential is identified with a scalar metric perturbation, as stated in the upstream definition of conformal_edge_length_field.
proof idea
The proof unfolds the definition of conformal_edge_length_field to expose the length as $a · exp((ε_i + ε_j)/2)$, then squares it. A helper shows that the square of the exponential equals the exponential of the sum by using the addition formula for exponentials and algebraic simplification. The main rewrite then multiplies through to obtain the claimed identity.
why it matters
This exact identity is the algebraic foundation for the second-order Taylor expansion in conformal_length_sq_taylor2 and is packaged into the certificate weakFieldConformalReggeCert that collects the conformal exactness, the Taylor expansion, the graph Laplacian decomposition, and the reduction. It fills the first step of the conformal expansion in the module's layering, providing the starting point for deriving the Dirichlet form from the Regge bilinear form. In the broader framework it supports the reduction of the Regge action to a quadratic form on the potential.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.