conformal_remainder_zero
plain-language theorem explainer
The declaration establishes that the remainder in the conformal edge-length expansion vanishes exactly at the flat vacuum. Workers on the algebraic reduction of the Regge action to a Dirichlet form cite this to justify truncating at second order without error at ξ = 0. The proof is a direct one-line wrapper unfolding the definition of the remainder and simplifying.
Claim. $R(0) = 0$, where the conformal remainder is defined by $R(t) := e^{t} - 1 - t - t^2/2$.
background
The module develops the weak-field conformal reduction of the Regge action from the ansatz ℓ_{ij} = ℓ_0 exp((ξ_i + ξ_j)/2). It expands the squared ratio ℓ_{ij}²/ℓ_0² to second order and isolates the remainder term R(t) with t = (ξ_i + ξ_j)/2. The upstream definition states: 'The Taylor expansion of exp(t) − 1 − t − t²/2 is the third-order remainder. We do not prove a quantitative bound here; we just expose the algebraic decomposition with the remainder named explicitly.' This step precedes the graph-Laplacian decomposition that converts the bilinear form into a sum of squared differences.
proof idea
The proof is a one-line wrapper that unfolds the definition of conformal_remainder and applies simp to evaluate the expression at zero.
why it matters
This result closes the algebraic verification of the second-order conformal expansion in the weak-field limit. It is invoked inside weakFieldConformalReggeCert to certify the full reduction of the Regge action to the Dirichlet form on edge differences. The module doc-comment positions it as part of §1, the conformal expansion that is fully proven, feeding the geometric hypothesis package for the Regge second-variation coefficients.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.