c_pos
plain-language theorem explainer
The lemma establishes positivity of the speed of light when expressed in RS-native units. Researchers deriving other constants or verifying physical assumptions in bridge data cite it to discharge positivity requirements. The proof is a one-line term wrapper that simplifies the definition of c directly to 1.
Claim. $c > 0$, where $c$ is the speed of light in RS-native units of voxel per tick.
background
In the Constants module the speed of light is fixed at 1 in RS-native units, with the fundamental length quantum defined as the voxel (voxel := 1) and the time quantum as the tick (τ₀ = 1). This yields the relation c = ℓ₀/τ₀ = 1 voxel/tick. The upstream ConstantDerivations result states c_rs > 0 and discharges it by rewriting to 1 followed by norm_num. The module treats all constants in these units, with c serving as the reference scale for subsequent derivations such as G and ħ.
proof idea
The proof is a one-line term-mode wrapper. It invokes simp on the definition of c, which unfolds to the constant 1 and immediately produces the required inequality 0 < 1.
why it matters
This lemma supplies the c_pos field required by the Physical structure in Bridge.DataCore, which is then used to prove lambda_rec_pos, lambda_rec_dimensionless_id_physical, G_pos, and kappa_einstein_pos. It anchors the RS-native convention c = 1 that appears throughout the constant derivations and the eight-tick octave scaling. The result closes the basic positivity anchor for the speed-of-light reference used by 22 downstream declarations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.