lambda_rec
plain-language theorem explainer
The fundamental recognition wavelength is defined to equal the base length unit in RS-native units. Researchers deriving constants from the eight-tick cycle cite this when normalizing all lengths to the voxel scale. The definition is a direct abbreviation that sets the wavelength to 1.
Claim. The fundamental recognition wavelength satisfies $λ_{rec} = ℓ_0 = 1$ in RS-native units.
background
The module establishes the fundamental RS time quantum τ₀ = 1 tick. Upstream, ell0 is the fundamental length unit ℓ₀ in RS-native units (voxel) and equals 1. The Derivation module supplies ell0 := c_codata * tau0 together with the lemma τ₀² = ħG/(π c⁵). The Bridge.DataCore version expresses an equivalent recognition length as √(ħG/c³).
proof idea
One-line definition that aliases the wavelength directly to ell0.
why it matters
This anchors the length scale used to derive Newton's constant via G = λ_rec² c³/(π ħ) and Einstein's kappa via kappa_einstein = 8 phi^5. It supports the T7 eight-tick octave step by fixing the recognition wavelength in native units. Downstream lemmas establish positivity and the dimensionless identity (c³ λ_rec²)/(ħ G) = 1/π.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.