lambda_rec_from_Jbit_pos
plain-language theorem explainer
The recognition wavelength defined by equating bit cost to curvature cost satisfies λ_rec > 0. Researchers matching Recognition Science ledger quantities to Planck units would cite this to guarantee the derived length is physical. The proof is a one-line wrapper that unfolds the square-root definition and applies the positivity lemma for square roots to the already-established positivity of J_bit.
Claim. $λ_{rec} = √(J_{bit}/2)$ satisfies $λ_{rec} > 0$.
background
The module derives λ_rec from the extremum condition J_bit = J_curv(λ) where J_bit = J(φ) = cosh(ln φ) - 1 and J_curv(λ) = 2λ² in RS-native units. J_bit itself is shown positive in multiple upstream results because φ > 1 forces ln φ > 0 and therefore cosh(ln φ) > 1. The definition lambda_rec_from_Jbit is the explicit solution λ = √(J_bit_val / 2) of that equilibrium equation.
proof idea
One-line wrapper that unfolds lambda_rec_from_Jbit and applies sqrt_pos.mpr to the division of J_bit_pos by the positive constant 2 (via norm_num).
why it matters
This result closes the positivity step inside the Planck-Scale Matching derivation chain that produces λ_rec ≈ 0.564 ℓ_P from the ledger-curvature extremum (Conjecture C8). It sits immediately after the family of J_bit_pos lemmas that trace back to the J-uniqueness theorem (T5) and the self-similar fixed point φ (T6). No downstream uses are recorded yet; the declaration simply guarantees the square root remains inside the positive reals before the 1/π face-averaging step restores SI dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.