lambda_rec
plain-language theorem explainer
This definition supplies the recognition length as the square root of ħ times G divided by pi times c to the third power, using values from the bridge data structure. Researchers in Recognition Science cite it when connecting the fundamental length to gravitational and Planck constants. The code is a direct one-line square root computation on the supplied anchors.
Claim. For a structure $B$ supplying real anchors $G$, $ħ$, and $c$, define the recognition length by $λ_{rec}(B) := √(ħ · G / (π · c³))$.
background
BridgeData is a structure holding external anchors G (Newton's gravitational constant), ħ (reduced Planck constant), c (speed of light), plus display values τ₀ and ℓ₀. The module isolates these core anchors and the recognition length expression to keep the certified import closure small, avoiding larger subsystems. Upstream results include the Constants definition of G as λ_rec² c³ / (π ħ), which inverts the present relation, and the native recognition length set to ℓ₀ in the eight-tick cycle.
proof idea
This declaration is a one-line definition that applies the real square root directly to the product of the hbar and G fields divided by pi times the cube of the c field.
why it matters
The definition underpins the lemma lambda_rec_dimensionless_id establishing the identity (c³ λ_rec²) / (ħ G) = 1/π under positivity assumptions. It also supports the derivation of G in Constants and anchors the recognition length in the eight-tick octave (T7) of the forcing chain. This closes a key relation for the fundamental length scale in the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.