K_pos
plain-language theorem explainer
The lemma establishes that the dimensionless bridge ratio K, defined as the positive square root of the golden ratio phi, is strictly positive. Researchers deriving RS constants and mass ladders would cite it to secure the sign before further inequalities. The proof is a one-line term application of real power positivity to the upstream fact that phi > 0.
Claim. Let $K = ϕ^{1/2}$. Then $0 < K$.
background
The Constants module fixes the RS-native time quantum at one tick. K is introduced there as the bridge ratio with the explicit non-circular definition $K := ϕ^{1/2}$, where ϕ denotes the golden ratio. This construction supports downstream constant derivations without circularity.
proof idea
The proof is a term-mode one-liner. It unfolds the definition of K via simpa and directly invokes Real.rpow_pos_of_pos on the hypothesis phi_pos together with the exponent 1/2.
why it matters
K_pos is the immediate predecessor of the nonnegativity lemma K_nonneg in the same module, which applies le_of_lt to it. The result anchors the sign of the bridge ratio used in the Recognition Science constant set, consistent with the forcing chain that fixes ϕ at T6 and the eight-tick octave at T7.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.