c_pos
plain-language theorem explainer
c_rs > 0 follows from the algebraic identity c_rs = 1 in RS-native units. Researchers deriving constants from the recognition composition law cite it to anchor positivity of c, ℏ, and G. The tactic proof rewrites via c_rs_eq_one then applies norm_num to verify the inequality.
Claim. $c_{RS} > 0$, where $c_{RS}$ is the ratio of fundamental length to the eight-tick period derived from the recognition composition law.
background
The ConstantDerivations module derives physical constants from the RS foundation rather than postulating them. Speed of light emerges as ℓ₀/τ₀ with τ₀ the eight-tick octave; upstream forcing chain yields J-uniqueness, φ as fixed point, and c_rs = 1 in native units. Module documentation states these constants are ratios algebraic in φ, not free parameters.
proof idea
One-line wrapper that rewrites the goal using c_rs_eq_one to obtain 1 > 0, then invokes norm_num to discharge the numerical inequality.
why it matters
Supplies the c_pos hypothesis required by the Physical structure in Bridge.DataCore and by G_pos, kappa_einstein_pos in Constants. It closes the derivation step from the T0-T8 forcing chain to explicit constants c = 1, ℏ = φ^{-5}, G = φ^5 / π. Supports the claim that no free parameters enter at this level.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.