pith. machine review for the scientific record. sign in
def definition def or abbrev high

J_curv

show as:
view Lean formalization →

The curvature cost functional assigns total cost 2λ² to a recognition token of wavelength λ. Researchers deriving the recognition wavelength from cost balance cite it when equating bit cost to curvature cost. It arises by direct definition from the axiom that a ±4 curvature packet is distributed over the eight vertices of the three-cube.

claimThe curvature cost is given by $J(λ) = 2λ^2$, where λ is the recognition wavelength.

background

In the Planck-Scale Matching module the derivation of λ_rec proceeds by balancing bit cost against curvature cost. The J functional is the unique cost J(x) = (x + x^{-1})/2 - 1 evaluated at the self-similar fixed point φ, normalized so that J_bit = 1. The curvature cost is obtained from |κ| = 4 curvature quanta on Q3, Gauss-Bonnet normalization on S² with χ = 2, and bounding area 4πλ², which simplifies to the factor 2λ² as recorded in the upstream derivation.

proof idea

This is a direct definition that encodes the curvature packet axiom by setting the total cost to twice the square of the wavelength. No lemmas are applied; the expression follows immediately from counting eight vertices each contributing λ²/4.

why it matters in Recognition Science

This definition supplies the curvature term in the balance residual used by balance_determines_lambda and GDerivationChain. It completes the curvature cost step in the Conjecture C8 chain, linking Q3 geometry through the balance condition to the derivation of G = λ_rec² c³ / (π ℏ) with ℏ = φ^{-5}. It relies on J-uniqueness from the forcing chain that guarantees the unique positive root.

scope and limits

formal statement (Lean)

 132noncomputable def J_curv (lam : ℝ) : ℝ := 2 * lam^2

proof body

Definition body.

 133
 134/-- J_curv(0) = 0. -/

used by (19)

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

depends on (1)

Lean names referenced from this declaration's body.