K_pos
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not supply a numerical value or approximation for K.
- Does not connect K to the curvature functional appearing in LambdaRecDerivation.
- Does not derive any physical scaling or application from the positivity.
formal statement (Lean)
494lemma K_pos : 0 < K := by
proof body
Term-mode proof.
495 -- φ > 0, hence φ^(1/2) > 0
496 simpa [K] using Real.rpow_pos_of_pos phi_pos (1/2 : ℝ)
497