K_nonneg
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not compute a numerical approximation to K.
- Does not relate K to G, alpha, or the mass ladder.
- Does not establish any functional equation satisfied by K.
formal statement (Lean)
498lemma K_nonneg : 0 ≤ K := le_of_lt K_pos
proof body
Term-mode proof.
499
500/-- Alias matching parallel-work naming convention. -/