edgeSqSecondOrder
plain-language theorem explainer
This definition extracts the quadratic term in the weak-field expansion of the squared conformal edge length ratio as (ε_i + ε_j)^2 / 2. Researchers reducing the Regge action to a Dirichlet form on vertex differences cite it when assembling the second-order contribution. It is a direct algebraic definition pulled from the Taylor series of the exponential in the conformal ansatz.
Claim. The second-order term in the expansion of the squared conformal edge length ratio is defined by $δ^2_{ij} = (ε_i + ε_j)^2 / 2$, where $ε : Fin n → ℝ$ is the log-potential field on the vertices.
background
In the weak-field conformal reduction, edge lengths follow the ansatz ℓ_{ij} = ℓ_0 exp((ε_i + ε_j)/2) with ε a log-potential assignment (Fin n → ℝ). The module expands ℓ_{ij}^2 / ℓ_0^2 to isolate linear and quadratic pieces before the remainder. Upstream conformal_length_sq_taylor2 supplies the exact rearrangement exp(t) = 1 + t + t²/2 + R(t) that justifies naming the quadratic piece separately. LogPotential is the type alias for such assignments, also used in the Laplacian action identification (1/2) Σ w_{ij} (ε_i − ε_j)^2 = (1/κ) Σ δ_h A_h from ContinuumBridge.
proof idea
Direct definition that isolates the quadratic piece of the Taylor expansion of the squared conformal length. It is invoked by name-unfolding inside the decomposition theorem that assembles 1 + first-order term + second-order term + remainder.
why it matters
This definition supplies the quadratic piece required by conformal_length_sq_decomposition for the second-order Regge action reduction. It feeds the algebraic step that converts the symmetric zero-row-sum bilinear form into the Dirichlet form Σ (ξ_i − ξ_j)^2 A_{ij}. In the Recognition framework it supports the conformal sector of the weak-field limit that isolates the eight-tick octave and D = 3 structures en route to the T0–T8 forcing chain. The remaining open task is verification of the row-sum condition on the geometric coefficients.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.