c_positive
plain-language theorem explainer
The theorem asserts that the speed of light in RS-native units is strictly positive. Researchers deriving constants from the unified forcing chain cite it to close the positivity requirement for c in the predictions registry. The proof is a one-line wrapper that rewrites via the equality c = 1 and applies norm_num to confirm 1 > 0.
Claim. In RS-native units the speed of light satisfies $c > 0$.
background
The module supplies calculated proofs for registry items C-001 (0 < α < 0.1), C-005 (c = 1), and C-006 (0 < k_R < 0.5). All proofs use norm_num, nlinarith and positivity with explicit bounds. The constant c is the speed of light forced to 1 in the native system where ħ = φ^{-5} and G = φ^5 / π. The upstream theorem c_eq_one states c = 1 by reflexivity. The Boltzmann analog k_R is defined as ln(φ) in Constants.BoltzmannConstant, the information cost per recognition event.
proof idea
The proof rewrites the goal with the upstream equality c_eq_one and invokes norm_num to evaluate the numerical inequality 1 > 0.
why it matters
This result supplies the positivity half of the C-005 entry and is assembled into the certificate theorem constants_predictions_cert_exists. It confirms the RS-native setting c = 1 that follows from T5 J-uniqueness and the eight-tick octave. The declaration closes one cell of the constants predictions table; the remaining open question is the conversion factor to SI units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.