c_derived_eq_codata
plain-language theorem explainer
The theorem shows that any RSUnitSystem obeying the consistency axiom c_codata * τ = ℓ yields derived speed ℓ/τ exactly equal to the CODATA reference value of c. Researchers deriving physical constants inside Recognition Science cite it to close the loop between the unit-system structure and the fixed numerical constant. The proof is a short algebraic reduction: unfold the definition of c_derived, invoke consistency together with τ ≠ 0, then finish with field_simp and linarith.
Claim. Let $u$ be an RSUnitSystem with components $τ$, $ℓ$ satisfying the consistency relation $c_0 τ = ℓ$, where $c_0$ denotes the CODATA speed of light. Then the derived speed $ℓ/τ$ equals $c_0$.
background
RSUnitSystem is the structure carrying a time scale τ > 0, length scale ℓ > 0, and golden-ratio value φ_val, together with the consistency axiom c_codata * τ = ℓ. The derived speed is defined by c_derived u := ℓ / τ. The constant c_codata is fixed at the exact SI value 299792458. The module derives all three CODATA constants (c, ℏ, G) from Recognition Science primitives by imposing this unit-system consistency and the tau0 relation τ₀² = ℏG/(π c⁵).
proof idea
Unfold the definition of c_derived to obtain ℓ/τ. Extract the consistency hypothesis c_codata * τ = ℓ and the positivity fact τ > 0 (hence τ ≠ 0). Apply field_simp to clear the denominator and finish with linarith on the resulting linear equation.
why it matters
The result supplies the equality needed by the downstream lemma c_derived_pos, which asserts positivity of the derived speed. It therefore anchors the entire Constants.Derivation module to the CODATA reference value of c, confirming that the RSUnitSystem construction reproduces the observed speed of light once consistency is imposed. The step sits inside the broader program of obtaining all constants from the Recognition Science forcing chain and the phi-ladder without external numerical input beyond the three CODATA anchors.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.