Constants Curvature Cost Form Curvature Cost Form Cert

The curvature cost certificate

In discrete geometry, a curvature cost is a number assigned to a shape that measures how much it bends or deviates from flatness. The declaration CurvatureCostFormCert is a formal certificate, a machine-checked collection of theorems, that establishes the precise quadratic form of one such cost in the Recognition Science framework. It proves that the boundary angle-defect cost, the cost associated with the total angular deficit around a cell's boundary, is exactly 2 λ², where λ is the scale factor. The number 2 comes from the Gauss-Bonnet theorem, which states that the total curvature of a sphere's surface is 2, and the quadratic dependence on λ comes from the Hessian, or second derivative, of the canonical reciprocal cost at its equilibrium point.

The certificate also proves a negative result about the bulk energy. It shows that the standard Dirichlet energy, a quadratic form that measures differences between vertex potentials, cannot be the source of the single-cell curvature cost under a uniform scale change. Constant vertex potentials are zero modes of this energy, meaning it assigns them zero cost, so it only sees differences, not absolute scale. This formally rules out the bulk Regge term as the origin of the curvature cost.

In Recognition Science, the framework models physical structure from a discrete record of recognition events. This certificate is the M2B bridge in that program, connecting the abstract cost function to a specific geometric quantity. It isolates the only intended meaning of the J_curv term: it is the quadratic boundary angle-defect cost, not the bulk energy and not the full nonlinear expression. The certificate is a form-level closure, a precise statement about the quadratic approximation, not a claim about the entire nonlinear function.

The certificate does not claim that the full nonlinear expression Jcost(1 + λ) is exactly λ². In fact, away from λ = -1, it equals λ² / (2(1 + λ)). The theorem-grade statement is only about the Hessian and the quadratic form. This distinction is the honest boundary of the result: it closes the quadratic form used by J_curv, but it does not establish the exact nonlinear behavior.

/-- The boundary angle-defect J-cost quadratic form is exactly `2 λ²`.

This is the form-level closure: the `2` comes from Gauss-Bonnet
(`χ(∂Q₃) = 2`) and the quadratic dependence comes from the Hessian of the
canonical reciprocal cost at equilibrium. -/
theorem boundaryCurvatureQuadraticCost_eq (lam : ℝ) :
    boundaryCurvatureQuadraticCost lam = 2 * lam ^ (2 : ℕ) := by
  unfold boundaryCurvatureQuadraticCost boundaryDefectCoefficient
  rw [curvatureCoefficient_eq_euler_char, localJCostHessianCoefficient_eq_one]
  norm_num [euler_S2]

/-- Constant vertex potentials are zero modes of the canonical Dirichlet
energy. This is the formal reason the bulk Regge Hessian does not carry the
single-cell uniform-scale curvature cost: the Dirichlet quadratic only sees
differences `ξ i - ξ j`. -/
theorem canonicalDirichletEnergy_constant_zero
    (K : Triangulation3D) (hK : IncidenceConsistent K) (c : ℝ) :
    canonicalDirichletEnergy K hK (fun _ : Fin K.nV => c) = 0 := by
  unfold canonicalDirichletEnergy
  simp

/-- The existing `J_curv` definition agrees with the theorem-derived boundary
quadratic form. This isolates the only intended meaning of `J_curv`: it is the
quadratic boundary angle-defect J-cost, not the bulk Regge Dirichlet energy and
not the full nonlinear `Jcost (1+λ)`. -/
theorem J_curv_eq_boundaryCurvatureQuadraticCost (lam : ℝ) :
    LambdaRecDerivation.J_curv lam = boundaryCurvatureQuadraticCost lam := by
  rw [LambdaRecDerivation.J_curv_derivation, boundaryCurvatureQuadraticCost_eq]

/-- The curvature-cost form certificate is inhabited. -/
def curvatureCostFormCert : CurvatureCostFormCert where
  bulk_uniform_scale_zero := canonicalDirichletEnergy_constant_zero
  boundary_cost_eq := J_curv_eq_boundaryCurvatureQuadraticCost
  boundary_cost_closed := boundaryCurvatureQuadraticCost_eq
  coefficient_is_euler := boundaryDefectCoefficient_eq_euler_char
  j_hessian_one := localJCostHessianCoefficient_eq_one

What this page does not claim

The certificate does not claim the full nonlinear expression Jcost(1 + λ) is exactly λ². It does not establish the bulk Regge term as a source of curvature cost. It does not derive the value of the fine-structure constant.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Constants/CurvatureCostForm.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: