WeakFieldConformalReggeCert
plain-language theorem explainer
The structure packages the exact conformal edge-length identity, its second-order Taylor expansion with explicit remainder, the graph-Laplacian decomposition of the quadratic form into a Dirichlet energy, and the reduction of the second-order Regge action to that Dirichlet form whenever the Schläfli row-sum condition holds. Discrete-gravity researchers cite it when passing from linearized Regge calculus on a flat background to a quadratic vertex-potential energy. The declaration is a bare structure definition that records the statements already
Claim. Let $L_{ij}(a,ε)=a·exp((ε_i+ε_j)/2)$ be the conformal edge length for scale $a>0$ and log-potential $ε$. The certificate asserts: $L_{ij}^2=a^2·exp(ε_i+ε_j)$ exactly; $L_{ij}^2/a^2=1+s+s^2/2+R(s)$ where $s=ε_i+ε_j$ and $R(s)=exp(s)-1-s-s^2/2$; for symmetric zero-row-sum $M$, the quadratic form equals the negative of the Dirichlet form $½∑M_{ij}(ε_i-ε_j)^2$; under the Schläfli row-sum condition on weak-field data $W$, the second-order Regge action equals $½$ times the Dirichlet form with edge-area weights, and likewise after division by nonzero $κ$; the Laplacian data satisfies the row-sum condition and both the action and Dirichlet form vanish at the zero potential.
background
The module isolates the algebraic core of the weak-field conformal reduction of the Regge action. The conformal edge-length field is the map $L_{ij}=a·exp((ε_i+ε_j)/2)$ with $ε$ a vertex log-potential. The remainder function is the explicit third-order term $R(t)=exp(t)-1-t-t^2/2$. The Dirichlet form generated by a symmetric matrix $M$ is $½∑{i,j}M{ij}(ε_i-ε_j)^2$. Edge-area weights are the negatives of the bilinear coefficients extracted from the linearization data $W$. The Schläfli row-sum condition requires these weights to sum to zero on each row, which holds automatically on a flat background by Schläfli’s identity.
proof idea
The declaration is a structure definition with no attached proof body. Its fields simply record the statements of the conformal exactness and Taylor lemmas, the graph-Laplacian decomposition, and the action-reduction identities. These statements are realized downstream by direct rewriting with the lemmas conformal_length_sq_exact, conformal_length_sq_taylor2, dirichlet_eq_neg_quadratic, and weak_field_conformal_reduction.
why it matters
The certificate supplies the unconditional algebraic reduction required by the gravity paper’s §6. It is instantiated by the theorem weakFieldConformalReggeCert. This completes the algebraic layer that converts the second-order Regge action into a Dirichlet energy on vertex potentials, the form needed for the continuum limit. In the Recognition Science framework the reduction supports the emergence of D=3 and the RS-native constants by ensuring the quadratic action takes the expected Dirichlet shape before geometric coefficients are supplied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.