c_derived_eq_codata
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not derive the numerical value of c from Recognition Science axioms alone.
- Does not address the derivation of ℏ or G.
- Does not apply outside the RSUnitSystem structure.
- Does not relax the consistency axiom.
Lean usage
lemma c_derived_pos (u : RSUnitSystem) : 0 < c_derived u := by rw [c_derived_eq_codata]; exact c_codata_posformal statement (Lean)
100theorem c_derived_eq_codata (u : RSUnitSystem) : c_derived u = c_codata := by
proof body
Term-mode proof.
101 unfold c_derived
102 have h := u.consistency
103 have hτ : u.τ ≠ 0 := ne_of_gt u.τ_pos
104 field_simp at h ⊢
105 linarith
106