c_pos
plain-language theorem explainer
The lemma establishes positivity of the speed of light constant c taken from CODATA values. Bridge data structures and physical assumption packages cite the result to keep derived quantities such as lambda_rec well-defined under square roots and divisions. The proof is a one-line wrapper that unfolds the constant and applies numerical normalization.
Claim. The speed of light satisfies $0 < c$.
background
The module quarantines empirical SI/CODATA numeric constants (speed of light c, reduced Planck constant, gravitational constant) from the certified derivation chain; explicit import is required for any numeric comparison. Upstream results supply the matching positivity statement for c in RS-native units (voxel/tick) together with the derivation that reduces the RS-native speed to one and normalizes the inequality.
proof idea
The proof is a one-line wrapper that unfolds the definition of c and applies norm_num to obtain the strict inequality from the explicit numeric value.
why it matters
The result supplies the c_pos field inside the Physical structure that is required by lambda_rec_pos and lambda_rec_dimensionless_id_physical in the bridge layer. It therefore closes the positivity requirement for the empirical speed of light while preserving the separation between quarantined constants and the T0-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.