boundaryDefectCoefficient
plain-language theorem explainer
Names the boundary Gauss-Bonnet coefficient of the one-cell curvature cost as the total angular defect of the cube boundary in units of one full turn. Anyone writing the quadratic boundary cost or the M2B curvature-cost certificate cites it. The body is a one-line alias of the already-derived curvature coefficient from the lambda-rec ladder.
Claim. The boundary defect coefficient is the real number equal to the curvature-cost coefficient: total angular defect of $\partial Q_3$ measured in units of one full turn $2\pi$. By discrete Gauss-Bonnet this equals $\chi(S^2)=2$.
background
Module CurvatureCostForm is the M2B bridge from the Regge-to-$J_{\mathrm{curv}}$ cost-form plan. It separates two facts: bulk Regge/Dirichlet energy under uniform conformal scale is a graph-Laplacian zero mode (constant vertex potentials cost nothing), while the boundary angle-defect cost admits a theorem-tier quadratic form.
The curvature-cost coefficient (from LambdaRecDerivation) is defined as $(Q_3\text{ vertices})\times(\text{angular deficit per vertex})/(2\pi)$. Discrete Gauss-Bonnet forces that defect-per-$2\pi$ to equal the Euler characteristic of the topological 2-sphere, $\chi(S^2)=2$. The local J-cost Hessian coefficient at equilibrium is independently 1, so the quadratic boundary cost is expected to be $2\lambda^2$.
Honest scope of the module: the closed statement is the Hessian/quadratic form used by $J_{\mathrm{curv}}$, not the claim that the full nonlinear $J(1+\lambda)$ equals $\lambda^2$ (in fact $J(1+\lambda)=\lambda^2/(2(1+\lambda))$ away from $\lambda=-1$).
proof idea
Definitional one-line wrapper. The abbrev simply identifies the boundary defect coefficient with the already-constructed curvature coefficient. No tactics or algebraic rewriting occur at this site; equality to the Euler characteristic is discharged downstream by rewriting through curvatureCoefficient_eq_euler_char.
why it matters
This name is the Gauss-Bonnet factor in the boundary quadratic cost. Downstream, boundaryCurvatureQuadraticCost multiplies it by the J-cost Hessian coefficient and $\lambda^2$; the equality theorem then proves that product is exactly $2\lambda^2$, with the 2 coming from $\chi(\partial Q_3)=2$ and the quadratic dependence from the Hessian of the reciprocal cost at equilibrium.
The M2B certificate structure packages the bulk zero-mode fact with the identity $J_{\mathrm{curv}}(\lambda)=$ boundary quadratic cost, so this coefficient is the numeric hinge of that closure. In the broader Recognition chain it sits on the geometric side of the cost form (Regge angle defect on the cube boundary), not on the T5 J-uniqueness or T6 $\phi$ fixed-point steps, but it supplies the concrete coefficient that lets the one-cell curvature cost match the existing $J_{\mathrm{curv}}$ ladder entry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.