edgeSqFirstOrder
plain-language theorem explainer
edgeSqFirstOrder extracts the linear coefficient δ¹(ℓ_{ij}²/ℓ₀²) = ε_i + ε_j from the conformal edge-length ansatz. Researchers reducing the Regge action to a Dirichlet form on vertex potentials cite it when assembling the second-order expansion. The definition is a direct sum of the two endpoint values of the supplied log-potential assignment.
Claim. Let $n$ be a natural number and let $ε : Fin n → ℝ$ be a log-potential assignment. For vertices $i,j ∈ Fin n$ the first-order coefficient in the weak-field expansion of squared edge lengths is $ε(i) + ε(j)$.
background
The module develops the algebraic core of the weak-field conformal reduction of the Regge action. Under the ansatz ℓ_{ij} = ℓ_0 exp((ξ_i + ξ_j)/2) the squared length ratio expands as 1 + (ξ_i + ξ_j) + ½(ξ_i + ξ_j)² + remainder, where the linear term is supplied by this definition. LogPotential n is the abbreviation Fin n → ℝ that records vertex log-potentials ε_i = ln ψ(σ_i) and is the same object used by the Laplacian action on the simplicial ledger.
proof idea
The definition is a direct one-line extraction that returns the sum of the two endpoint values of the log-potential.
why it matters
It supplies the first-order building block required by conformal_length_sq_decomposition, which isolates the remainder and feeds the reduction of the Regge action to the Dirichlet form −½ Σ M_{ij} (ξ_i − ξ_j)². The construction realizes the algebraic step that converts the symmetric zero-row-sum bilinear form into a sum of squared differences, consistent with the conformal sector of the gravity paper. It touches the open geometric task of verifying the row-sum condition from Cayley–Menger data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.