c_derived
plain-language theorem explainer
Defines the derived speed of light in an RSUnitSystem as the ratio of its length scale to its time scale. Researchers deriving constants from Recognition Science primitives cite it to confirm consistency with the CODATA value of c. The definition is a direct field projection from the RSUnitSystem structure.
Claim. For a unit system $u$ with time scale $τ$ and length scale $ℓ$ satisfying the consistency condition $c_{codata} · τ = ℓ$, the derived speed of light is $c_{derived}(u) := ℓ / τ$.
background
RSUnitSystem is a structure that encodes a consistent unit system in Recognition Science. It consists of a time scale τ, length scale ℓ, golden ratio value φ_val, positivity proofs, the equation φ_val = (1 + sqrt(5))/2, and the key consistency relation c_codata * τ = ℓ. The module derives physical constants from Recognition Science primitives using CODATA reference values for c, ℏ, and G. This definition depends directly on the RSUnitSystem structure, which enforces the relation between length and time scales via the speed of light.
proof idea
The definition is a one-line wrapper that applies the field projection u.ℓ / u.τ from the RSUnitSystem structure.
why it matters
This definition supports the downstream theorems c_derived_eq_codata and c_derived_pos that establish equality to the CODATA value and positivity. It forms part of the constants derivation chain linking the fundamental scales tau0 and ell0 to observed c. It touches the Recognition Science goal of deriving constants from the phi-ladder and unit consistency without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.