lambda_rec_pos
plain-language theorem explainer
Positivity of the recognition length λ_rec is required for taking roots in the definition of G and for uniqueness arguments in the forcing chain. It is cited by derivations of the gravitational constant and minimal area eigenvalues. The proof reduces the claim to the definition λ_rec := ell0 via simplification, inheriting positivity from the base length scale.
Claim. The fundamental recognition wavelength satisfies $0 < λ_{rec}$, where $λ_{rec} = ℓ_0$ in RS-native units.
background
In the Constants module the recognition length is defined by λ_rec := ell0, the base length in the eight-tick cycle. The module_doc states that τ₀ = 1 tick is the fundamental RS time quantum. Upstream, Bridge.DataCore defines λ_rec = √(ħ G / c³) and proves its positivity under Physical assumptions via Real.sqrt_pos and div_pos; the Constants version aligns with that definition through the forcing chain.
proof idea
Term-mode proof consisting of the single tactic simp [lambda_rec]. The simplification unfolds λ_rec to ell0 and reduces the inequality to the already-established positivity of the base length ell0.
why it matters
Invoked by G_pos to obtain 0 < G, by lambda_rec_is_forced to select the unique positive root of K, and by minimal_area_eigenvalue to bound the area spectrum from below by ell0². It supplies the positivity step inside the T7 eight-tick octave and the RS-native expression G = λ_rec² c³ / (π ħ). It touches the embedding of the phi-ladder into length scales.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.