J_curv_nonneg
plain-language theorem explainer
The curvature cost J_curv(λ) = 2λ² is nonnegative for every real λ. Researchers deriving the recognition wavelength λ_rec from the extremum condition J_bit = J_curv(λ_rec) cite this to guarantee the curvature term stays nonnegative. The proof is a one-line wrapper that unfolds the definition, applies nonnegativity of squares, and closes with linear arithmetic.
Claim. For every real number $λ$, the curvature cost satisfies $J_{curv}(λ) ≥ 0$, where $J_{curv}(λ) := 2λ²$.
background
In the Planck-Scale Matching module the curvature cost is introduced by the axiom that a ±4 curvature packet distributed over the 8 vertices of the Q₃ hypercube produces total cost 2λ². This matches the upstream definition in LambdaRecDerivation, where J_curv(λ) = 2λ² follows from |κ| = 4 quanta, Gauss-Bonnet normalization on S² with χ = 2, and bounding area 4πλ². The module derives λ_rec ≈ 0.564 ℓ_P by setting J_bit = J_curv(λ_rec), restoring SI dimensions via c³λ²/(ℏG), and averaging over the 8-face geometry to insert the factor 1/π.
proof idea
The proof unfolds J_curv to obtain 2 lam^2, invokes sq_nonneg lam to obtain lam^2 ≥ 0, and closes with linarith.
why it matters
This positivity anchors the curvature term inside the extremum equation J_bit = J_curv(λ) that determines λ_rec in the Planck-Scale Matching derivation of Conjecture C8. It supplies the nonnegativity needed for the chain that begins with J-uniqueness (T5), passes through the phi-ladder, and reaches the recognition wavelength. No open questions are addressed; the result is an immediate algebraic consequence of the quadratic definition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.