K_nonneg
plain-language theorem explainer
The lemma establishes non-negativity of the dimensionless bridge ratio K defined as the square root of phi. Researchers deriving stability bounds in the Recognition Science framework cite it when constructing uniform defect estimates. The proof is a one-line term application of le_of_lt to the already-proved positivity of K.
Claim. Let $K = ϕ^{1/2}$. Then $0 ≤ K$.
background
In the Constants module the dimensionless bridge ratio K is introduced as the non-circular definition $K = ϕ^{1/2}$, where ϕ denotes the golden ratio. The module works in RS-native units with the fundamental time quantum equal to one tick. The companion lemma K_pos already shows strict positivity of K by applying Real.rpow_pos_of_pos to the positivity of ϕ.
proof idea
The proof is a direct term-mode wrapper that applies the standard lemma le_of_lt to the positivity result K_pos.
why it matters
K_nonneg supplies the non-negativity hypothesis required by the StabilityBounds structure in the DAlembert stability analysis. It completes the basic algebraic properties of the bridge constant K that appears in the phi-ladder construction and the eight-tick octave of the forcing chain. The result closes a minor scaffolding gap between the definition of K and its use in uniform defect bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.