lambda_rec_SI_pos
plain-language theorem explainer
The theorem establishes positivity of the recognition wavelength in SI units. Researchers matching Planck-scale lengths in Recognition Science cite it to confirm the derived scale is physically admissible. The proof unfolds the definition then chains sqrt_pos.mpr with div_pos and mul_pos lemmas on the positivity of ħ, G, π, and c.
Claim. $λ_{rec,SI} > 0$ where $λ_{rec,SI} = √(ℏG/(π c³))$.
background
The module formalizes the ledger-curvature extremum argument for Conjecture C8. Bit cost is defined as J_bit = J(φ) = cosh(ln φ) - 1 from the unique functional J(x) = ½(x + x⁻¹) - 1. Curvature cost is J_curv(λ) = 2λ² in RS-native units; equilibrium sets J_bit = J_curv(λ_rec). Face averaging over the Q₃ cube then introduces the factor 1/π when restoring SI dimensions via c³λ²/(ℏG).
proof idea
Term-mode proof. Unfold lambda_rec_SI reduces the claim to positivity of the radicand. Apply sqrt_pos.mpr, then div_pos. The numerator is positive by mul_pos hbar_pos G_pos; the denominator is positive by mul_pos Real.pi_pos (pow_pos c_pos 3).
why it matters
It supplies the positivity step required for the Planck ratio λ_rec/ℓ_P = 1/√π in Conjecture C8. The result closes the sign check after the extremum condition and the eight-tick geometry, allowing safe insertion of the 0.564 factor into downstream constant matching without sign contradictions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.