weakFieldConformalReggeCert
plain-language theorem explainer
The weak-field conformal Regge certificate asserts that under the conformal edge-length ansatz the second-order Regge action reduces exactly to a weighted Dirichlet form on log-potential differences when the Schläfli row-sum condition holds. A researcher deriving discrete gravity actions from Regge calculus would cite this algebraic core to obtain the quadratic form without remainder in the flat sector. The proof is a term-mode construction that directly supplies each field of the certificate structure from the module's sibling lemmas on exact/
Claim. The certificate holds: for $a>0$ and log-potential $ε$, the squared conformal edge length satisfies $ℓ_{ij}^2 = a^2 exp(ε_i + ε_j)$ exactly and expands as $ℓ_{ij}^2/a^2 = 1 + (ε_i + ε_j) + (ε_i + ε_j)^2/2 + R(ε_i + ε_j)$ with explicit remainder $R$; for any symmetric zero-row-sum matrix $M$, the quadratic form $Q(ε;M)$ equals the negative Dirichlet form $D(ε;M)$; the second-order Regge action on Laplacian Regge data reduces to the Dirichlet form; both the action and Dirichlet form vanish at the flat configuration $ε≡0$; and the remainder vanishes at zero.
background
The module treats the algebraic reduction of the Regge action $S = (1/κ) Σ A_h δ_h$ under the conformal ansatz $ℓ_{ij} = a exp((ε_i + ε_j)/2)$ for a log-potential $ε$ on vertices. Key definitions are the conformal edge length field (which sets lengths from scale $a$ and $ε$), the quadratic form $Q(ε;M) = Σ_{i,j} M_{ij} ε_i ε_j$, and the Dirichlet form $D(ε;M) = ½ Σ_{i,j} M_{ij} (ε_i - ε_j)^2$ for symmetric edge weights $M$. The graph-Laplacian decomposition states that $Q(ε;M) = -D(ε;M)$ whenever $M$ is symmetric and has zero row sums. This builds directly on the exact identity $ℓ_{ij}^2 = a^2 exp(ε_i + ε_j)$ and its second-order Taylor expansion with remainder $R(t) = exp(t) - 1 - t - t^2/2$.
proof idea
The term proof constructs the certificate structure by supplying each required field with the corresponding sibling theorem: conformal_exact from conformal_length_sq_exact, conformal_taylor2 from conformal_length_sq_taylor2, graph_laplacian_decomp from dirichlet_eq_neg_quadratic, the reduction fields from weak_field_conformal_reduction and its kappa variant, row-sum discharge from schlaefliRowSum_laplacianReggeData, flat vanishing from secondOrderReggeAction_flat and dirichletForm_flat, and remainder vanishing from conformal_remainder_zero.
why it matters
This certificate packages the algebraic core of the weak-field conformal reduction, turning the Regge bilinear form into the Dirichlet form on potential differences once the Schläfli row-sum condition is met by the Laplacian Regge data. It completes the algebraic layer described in the module (exact expansion, graph decomposition, and flat vanishing) and supplies the finite-dimensional identity needed for the gravity paper's second-variation analysis. The result relies on the zero-row-sum property and touches the remaining geometric task of verifying that property from Cayley-Menger or dihedral formulas for concrete lattices.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.