c_derived_pos
plain-language theorem explainer
The lemma establishes that the derived speed of light remains strictly positive for any valid RS unit system. Physicists deriving constants from Recognition Science primitives would cite it to confirm that constructed velocities stay physically sensible. The proof is a one-line wrapper that rewrites the derived quantity to the codata constant and invokes its known positivity.
Claim. For any RS unit system $u$ with positive time scale $τ$ and length scale $ℓ$ satisfying the consistency condition, the derived speed of light obeys $0 < ℓ/τ$.
background
The module derives physical constants from Recognition Science primitives, referencing CODATA values for $c$, $ℏ$, and $G$. RSUnitSystem is the structure with fields $τ > 0$, $ℓ > 0$, $φ_val = (1 + √5)/2$, and consistency $c_{codata} · τ = ℓ$. The derived speed of light is defined as $ℓ/τ$. Upstream results include the positivity lemma for the codata speed of light and the equality theorem showing the derived quantity equals the codata value.
proof idea
This is a one-line wrapper. It rewrites the derived speed using the equality to the codata constant, then applies the positivity lemma for that codata constant.
why it matters
The lemma secures positivity of the derived speed of light within the constants derivation module, supporting the overall claim that Recognition Science primitives recover positive physical constants. It closes a basic sanity check in the chain from unit system structure to codata matching. No downstream uses are recorded, but it underpins verification that the constructed $c$ aligns with the positive CODATA reference.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.