lambda_rec_from_Jbit
plain-language theorem explainer
The definition extracts the recognition wavelength as the positive square root of half the bit cost J_bit_val. Researchers deriving the Planck length ratio from the ledger-curvature extremum cite this expression to close the algebraic step of Conjecture C8. It follows by direct rearrangement of the equation J_bit = 2 lambda squared.
Claim. Let $J_{bit} := J(phi)$ denote the bit cost. Define $lambda_{rec} := sqrt(J_{bit}/2)$, where the curvature cost satisfies $J_{curv}(lambda) = 2 lambda^2$.
background
The PlanckScaleMatching module derives lambda_rec from equating bit cost to curvature cost at equilibrium. J_bit_val is the bit cost J(phi) = cosh(ln phi) - 1, the fundamental cost of a ledger bit transition at the self-similar scale. J_curv(lambda) equals 2 lambda squared, obtained by distributing a plus-or-minus-four curvature packet over the eight faces of the Q3 hypercube.
proof idea
This is a direct definition that implements the algebraic rearrangement lambda equals sqrt(J_bit_val divided by 2) of the extremum equation.
why it matters
The definition supplies the explicit lambda_rec value required by extremum_condition, extremum_unique, and the PlanckScaleMatchingCert structure. It fills the algebraic step in the C8 derivation chain that produces lambda_rec approximately 0.564 Planck lengths, connecting the phi fixed point and the eight-tick octave to the final Planck ratio.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.