extremum_condition
plain-language theorem explainer
The extremum condition theorem shows that the curvature cost J_curv evaluated at the recognition wavelength derived from the bit cost recovers exactly the bit cost value. Researchers deriving Planck-scale relations from Recognition Science ledger costs cite this to close the equilibrium step in the lambda_rec derivation. The proof unfolds the definitions of J_curv and lambda_rec_from_Jbit, invokes positivity of J_bit_val to apply the square root identity, and reduces the expression algebraically via ring.
Claim. Let $J_ {bit} := J(φ)$ and $λ_{rec} := √(J_{bit}/2)$. Then $J_{curv}(λ_{rec}) = J_{bit}$, where the curvature cost is defined by $J_{curv}(λ) = 2λ^2$.
background
In the PlanckScaleMatching module the recognition wavelength is obtained by setting the bit cost equal to the curvature cost. The bit cost J_bit_val is J(phi), the evaluation of the cost functional at the golden ratio. The curvature cost J_curv(lambda) equals 2 lambda squared and arises from distributing a ±4 curvature packet over the eight faces of the Q3 hypercube, as stated in the module documentation for Conjecture C8.
proof idea
The proof is a short term-mode reduction. It unfolds J_curv and lambda_rec_from_Jbit, establishes nonnegativity of J_bit_val/2 from the upstream positivity result J_bit_pos, rewrites via sq_sqrt, and finishes with ring simplification.
why it matters
This result supplies the extremum_determines field inside the planck_scale_matching_cert definition. It implements the equilibrium step J_bit = J_curv(lambda_rec) described in the module documentation, which yields lambda_rec ≈ 0.564 ell_P after restoring SI units and the 1/pi factor from face averaging. In the Recognition Science chain it connects the J-uniqueness and phi fixed-point steps to the spatial-scale matching.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.