Pith. sign in
module module high

IndisputableMonolith.Constants.CurvatureCostForm

show as:
view Lean formalization →

Constant vertex potentials are zero modes of the canonical Dirichlet energy, so the bulk Regge Hessian only sees edge differences and cannot carry a single-cell uniform-scale curvature cost. The module equates the J-curvature cost with a boundary curvature quadratic form tied to Euler defect and packages a certificate. Planck-scale matching cites this bridge when fixing λ_rec against ℓ_P. The argument joins the local J-Hessian kernel to concrete Regge second-variation data.

claimConstant vertex potentials $\xi_i \equiv c$ are zero modes of the canonical Dirichlet energy (quadratic in differences $\xi_i-\xi_j$). Hence the bulk Regge Hessian does not encode the single-cell uniform-scale curvature cost. The module defines a boundary curvature quadratic cost, shows its coefficient matches the Euler-characteristic defect, normalizes the local $J$-cost Hessian coefficient to $1$, and equates $J_{\mathrm{curv}}$ with that boundary cost, recording a certificate of the identification.

background

Recognition Science builds curvature costs from the unique cost $J(x)=\frac12(x+x^{-1})-1$ and from discrete geometry. The C7 module supplies the exact local algebraic kernel $J(1+\varepsilon)=\varepsilon^2/(2(1+\varepsilon))$ at equilibrium, stronger than a bare second-order Taylor claim. On the geometric side, a concrete 3D Regge triangulation gives the action under a conformal ansatz and its second variation, packaged as Regge Hessian data.

Canonical Dirichlet energy on a cell complex is quadratic in vertex potentials and vanishes on constants because it only sees differences $\xi_i-\xi_j$. That zero-mode fact is why a uniform scale mode is invisible to the bulk Hessian and must be recovered from boundary or topological defect data. Upstream, the non-circular $\lambda_{\mathrm{rec}}$ derivation ties the recognition length to the composition law and $Q_3$ Gauss-Bonnet with no free parameter.

proof idea

Short constants bridge, not a long development. It records that canonical Dirichlet energy annihilates constant potentials; defines a boundary defect coefficient and equates it to the Euler-characteristic contribution; normalizes the local $J$-cost Hessian coefficient to one. It then introduces the boundary curvature quadratic cost, proves the closed-form equality, and identifies $J_{\mathrm{curv}}$ with that cost. A certificate structure packages the equalities for downstream import.

why it matters in Recognition Science

Planck-scale matching imports this module to derive $\lambda_{\mathrm{rec}}\approx 0.564,\ell_P$ from the ledger-curvature extremum (conjecture C8). That chain starts from the unique bit cost $J$ and needs a precise curvature quadratic once the bulk Dirichlet Hessian is known to miss the uniform-scale mode. Equating $J_{\mathrm{curv}}$ to the boundary curvature cost tied to Euler defect supplies the coefficient that seats the recognition length against the Planck length without free calibration. The module sits between the C7 local expansion, the concrete Regge Hessian, and the $\lambda_{\mathrm{rec}}$ derivation on the path to Planck matching.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (9)