lambda_rec_SI
plain-language theorem explainer
The definition supplies the SI recognition wavelength as the square root of ħG over πc³. Researchers on Conjecture C8 cite this expression when matching the curvature extremum to the bit cost at the phi scale. It is introduced as a direct algebraic restatement of the face-averaged Planck gate identity.
Claim. The recognition wavelength in SI units is defined by $λ_{rec} = √(ℏG/(πc³))$.
background
This module formalizes the derivation of λ_rec ≈ 0.564 ℓ_P from the ledger-curvature extremum argument for Conjecture C8. The chain begins with the bit cost J_bit = J(φ) = cosh(ln φ) - 1 from the unique cost functional, sets it equal to the curvature cost J_curv(λ) = 2λ² on the Q₃ hypercube, and introduces the 1/π factor via face averaging over eight faces when restoring SI dimensions.
proof idea
The declaration is a direct definition of the square root expression. It encodes the Planck gate identity without invoking any lemmas or tactics.
why it matters
This definition feeds the theorem lambda_rec_over_ell_P that proves λ_rec / ℓ_P = 1/√π, the central numerical result of Conjecture C8. It also supports the PlanckScaleMatchingCert structure that verifies the full derivation chain from J_bit to the extremum condition. The construction links the J-uniqueness at T5 and the eight-tick octave to the three spatial dimensions through the Q3 geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.