J_curv
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.