J_curv
plain-language theorem explainer
The curvature cost functional assigns 2λ² to a recognition token at scale λ. This arises from distributing four curvature quanta over the eight vertices of Q3 and normalizing via Gauss-Bonnet on S². Workers deriving λ_rec non-circularly cite it to equate against the unit bit cost before defining G. The definition is a direct algebraic encoding of the curvature packet axiom.
Claim. $J(λ) = 2λ²$, where $J$ is the curvature cost of embedding one recognition token at scale $λ$.
background
The LambdaRecDerivation module formalizes a non-circular derivation of the recognition length λ_rec. It sets the normalized bit cost of one recognition event equal to the curvature cost without presupposing Newton's constant G, which is then defined as a consequence: G := π · λ_rec² · c³ / ℏ. The local setting uses only the bit cost (=1) and curvature cost (=2λ²) from Q3 Gauss-Bonnet normalization.
proof idea
Direct definition implementing the curvature packet axiom: a ±4 curvature packet distributed over the 8 vertices of Q3 yields total cost 2λ² after normalization on S² with χ=2 and area 4πλ².
why it matters
This supplies the curvature side of the balance equation used in balance_at_lambda_0, balance_determines_lambda, and GDerivationChain. It completes step 3 of the chain from Q3 geometry to G = λ_rec² c³/(π ℏ), relying on cost uniqueness from T5. It closes the non-circular path to the gravitational constant in RS-native units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.