conformal_remainder
plain-language theorem explainer
Names the third-order remainder R(t) = exp(t) - 1 - t - t²/2 that appears after truncating the exponential in the conformal edge-length ansatz. Workers on the algebraic reduction of the Regge action to a Dirichlet form cite this explicit term to keep the second-order truncation exact before the graph-Laplacian step. The definition is a direct algebraic rearrangement of the Taylor series with no lemmas applied.
Claim. Define the remainder function by $R(t) := e^t - 1 - t - t^2/2$ for $t : ℝ$.
background
The module develops the weak-field conformal reduction of the Regge action. It begins from the conformal edge ansatz ℓ_ij = ℓ_0 exp((ξ_i + ξ_j)/2) on a finite vertex set, expands the squared lengths to second order in the log-potential ξ, and isolates the remainder after the constant, linear, and quadratic terms. Upstream results from EdgeLengthFromPsi supply the exponential form as an algebraic identity or hypothesis discharge, while SimplicialLedger and PhiForcingDerived calibrate the underlying J-cost and ledger factorization.
proof idea
One-line definition that isolates the remainder after subtracting the constant, linear, and quadratic terms from the exponential series.
why it matters
This remainder definition supports the exact decomposition theorems conformal_length_sq_decomposition and conformal_length_sq_taylor2, which feed the WeakFieldConformalReggeCert structure. It completes the algebraic layer of the reduction from Regge action to Dirichlet form on differences (ξ_i - ξ_j)², as described in the module layering for the gravity paper.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.