boundaryDefectCoefficient_eq_euler_char
plain-language theorem explainer
The boundary Gauss-Bonnet defect coefficient of the one-cell curvature cost equals χ(S²) = 2. Anyone assembling the quadratic form of J_curv, or the curvature-cost certificate, cites this identification. The proof is a one-line term that reuses the already-proved equality of the underlying curvature coefficient with the Euler characteristic.
Claim. The boundary Gauss-Bonnet coefficient of the one-cell curvature cost equals the Euler characteristic of the bounding sphere $S^2$, i.e. equals $2$ as a real number.
background
This module is the M2B bridge from the Regge-to-J_curv cost-form plan. It separates bulk from boundary: under a uniform conformal scale, constant vertex potentials are graph-Laplacian zero modes, so the bulk Regge/Dirichlet quadratic cannot source the one-cell curvature cost. The curvature cost must therefore come from the boundary angle-defect term.
The boundary defect coefficient is defined as the total angular defect in units of one full turn; in this file it is an abbreviation for the curvature coefficient already studied in LambdaRecDerivation. Discrete Gauss-Bonnet identifies that coefficient with χ(S²). The Euler characteristic of the bounding sphere is the natural number 2, cast to ℝ.
Upstream, curvatureCoefficient_eq_euler_char records that discrete Gauss-Bonnet forces the defect-per-2π to equal χ(S²) = 2, so the coefficient in J_curv = 2λ² is derived rather than posited.
proof idea
One-line term proof. Because the boundary defect coefficient is definitionally the curvature coefficient, the claim reduces exactly to the upstream theorem that the curvature coefficient equals euler_S2. No extra rewriting or field arithmetic is needed at this site; that work already lives in the LambdaRecDerivation proof (unfold, rewrite by total_curvature_gauss_bonnet, field_simp).
why it matters
This lemma fills the coefficient_is_euler field of the curvature-cost form certificate. That certificate packages the two M2B facts: bulk uniform-scale Dirichlet energy vanishes on constants, and the boundary quadratic cost closes as 2λ² with Hessian coefficient 1 and Gauss-Bonnet coefficient χ(∂Q₃) = 2.
In the Recognition framework this is the theorem-tier justification that the prefactor in the quadratic boundary curvature cost is the topological Euler number, not a free fit parameter. It sits downstream of discrete Gauss-Bonnet and upstream of the equality between J_curv and the boundary curvature quadratic cost. The module is explicit that only the quadratic form is closed here; the full nonlinear J-cost identity is not claimed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.