conformal_length_sq_taylor2
plain-language theorem explainer
Algebraic identity giving the exact second-order expansion of squared conformal edge lengths under the log-potential ansatz. Workers reducing the Regge action in the weak-field conformal sector cite it to isolate the quadratic term before Dirichlet decomposition. The proof substitutes the exact exponential square identity, unfolds the remainder definition, and rearranges via field simplification and ring tactics.
Claim. For positive real $a$ and log-potential assignment $ε$ on $n$ vertices, the normalized squared edge length satisfies $ℓ_{ij}^2 / a^2 = 1 + (ε_i + ε_j) + (ε_i + ε_j)^2 / 2 + R(ε_i + ε_j)$, where the remainder is $R(t) = e^t - 1 - t - t^2/2$.
background
LogPotential n denotes assignments ε : Fin n → ℝ that record log-potentials at vertices. The conformal edge length field is the map sending each pair to length a · exp((ε_i + ε_j)/2), reducing to constant a in the flat vacuum. The upstream exact identity states that the squared length equals a² · exp(ε_i + ε_j). The remainder function is defined exactly as exp(t) − 1 − t − t²/2 to name the higher-order discrepancy without bounds.
proof idea
The proof invokes the exact squared-length identity, unfolds the remainder definition, applies field_simp to clear the denominator a², and finishes with ring to match the Taylor rearrangement of the exponential.
why it matters
This supplies the taylor2 form required by conformal_length_sq_decomposition and by the certificate weakFieldConformalReggeCert. It completes the algebraic core of the conformal expansion step that reduces the Regge action to a quadratic Dirichlet form on differences, as outlined in the module documentation for the weak-field limit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.