conformal_length_sq_decomposition
plain-language theorem explainer
The theorem decomposes the squared length of a conformally perturbed edge into its first-order linear term, quadratic term, and exact remainder under the weak-field ansatz. Researchers deriving the second-order Regge action from a conformal mode would cite this identity when reducing the bilinear form to a Dirichlet energy on vertex differences. The proof is a one-line wrapper that unfolds the order-one and order-two summands then invokes the Taylor expansion lemma conformal_length_sq_taylor2.
Claim. Let $a>0$, let $n$ be a natural number, let $ε$ be a log-potential on the $n$ vertices, and let $i,j$ be vertex indices. Denote by $ℓ_{ij}$ the length of the conformal edge field scaled by $a$. Then $ℓ_{ij}^2/a^2 = 1 + δ^1_{ij} + δ^2_{ij} + R(ε_i + ε_j)$, where $δ^1_{ij}$ is the first-order term $ε_i + ε_j$, $δ^2_{ij}$ is the second-order term $½(ε_i + ε_j)^2$, and $R(t) = e^t - 1 - t - t^2/2$.
background
The module WeakFieldConformalRegge isolates the algebraic core of the weak-field reduction of the Regge action. It starts from the conformal edge ansatz $ℓ_{ij} = a · exp((ε_i + ε_j)/2)$ and expands $ℓ_{ij}^2/a^2$ to second order, leaving an explicit remainder. The local setting is the finite-dimensional graph whose edges carry lengths derived from a vertex log-potential; the target is to convert the resulting quadratic form into a discrete Dirichlet energy. Upstream, the ContinuumBridge structure supplies the identification $(1/2) Σ w_{ij} (ε_i − ε_j)^2 = (1/κ) Σ δ_h A_h$, which this decomposition prepares for substitution.
proof idea
The proof is a one-line wrapper. It unfolds the definitions of edgeSqFirstOrder and edgeSqSecondOrder, then applies the exact Taylor identity conformal_length_sq_taylor2 a ha ε i j, which already encodes the expansion $exp(t) = 1 + t + t^2/2 + R(t)$ with $t = ε_i + ε_j$.
why it matters
This identity supplies the precise algebraic remainder required by any subsequent second-order action reduction in the conformal sector. It completes the §1 conformal-expansion claim listed in the module documentation and feeds the graph-Laplacian decomposition that follows in the same file. The parent result is the ContinuumBridge identification of the Regge bilinear form with the Dirichlet form on differences; the theorem therefore sits between the conformal ansatz and the final reduction to $Σ (ε_i − ε_j)^2$ terms. No open scaffolding remains inside the algebraic layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.