ell_P
plain-language theorem explainer
The Planck length is defined as the square root of ħG/c³ using RS-native constants. Researchers working on Conjecture C8 and the recognition wavelength ratio would cite this when anchoring the 0.564 factor. The definition is a direct term that composes the square root with the imported constants ħ, G, and c.
Claim. The Planck length satisfies $ℓ_P = √(ℏG/c³)$, where ℏ is the reduced Planck constant and G is the gravitational constant in RS-native units.
background
The PlanckScaleMatching module derives λ_rec ≈ 0.564 ℓ_P from the ledger-curvature extremum argument of Conjecture C8. It starts from the unique cost functional J(x) = ½(x + x⁻¹) - 1 evaluated at the self-similar point φ, yielding J_bit, then equates it to curvature cost 2λ² on the Q₃ hypercube before restoring dimensions via face averaging that produces the 1/π factor. Upstream, G is given by λ_rec² c³ / (π ℏ) and ħ by φ⁻⁵ in native units, both drawn from the Constants module.
proof idea
This is a direct term-mode definition that applies the square root function to the quotient (hbar * G) / c^3. No additional lemmas or tactics are invoked beyond the imported constant declarations.
why it matters
This definition supplies the reference scale for the Planck-scale matching certificate. It is used by lambda_rec_over_ell_P to obtain the key ratio 1/√π and by ell_P_pos for positivity; it also appears in Gravity.RunningG for reference-scale comparisons. The placement completes the C8 derivation chain in the module documentation, relying on the eight-tick octave and D = 3 from the forcing chain together with Q₃ face averaging.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.