canonicalUnits
plain-language theorem explainer
The canonicalUnits definition constructs the base RS unit system by assigning the time coordinate to the fundamental tick duration τ₀ and the length coordinate to the voxel size ℓ₀, with the golden ratio fixed as the scaling parameter. Workers deriving ħ, G or the fine-structure constant from Recognition Science primitives cite this record to anchor all subsequent codata conversions. The construction is a direct structure literal that discharges the positivity and consistency fields by reflexivity.
Claim. Define the unit system by τ = τ₀, ℓ = ℓ₀, φ = (1 + √5)/2 where τ₀ > 0, ℓ₀ > 0 and c ⋅ τ₀ = ℓ₀, with c the reference speed of light.
background
RSUnitSystem is the record type that packages a time unit τ, length unit ℓ, golden-ratio value φ, the two positivity proofs, the equation φ = (1 + √5)/2, and the light-cone consistency c ⋅ τ = ℓ. The module derives all physical constants from Recognition Science primitives and supplies CODATA reference values for c, ħ and G as targets. Upstream, tau0 supplies the fundamental tick duration (placeholder equal to the tick constant) while ell0 supplies the fundamental length (set to 1 in native units); both carry explicit positivity lemmas.
proof idea
The definition is a direct record constructor. It populates τ with tau0, ℓ with ell0 and φ_val with phi, then supplies the four required fields by reflexivity on the positivity lemmas and the consistency equation.
why it matters
This definition fixes the native units that convert the Recognition Science primitives into the CODATA targets for ħ, G and α. It supplies the base for the derived-constant codata records that follow in the same module and thereby closes the first step of the constant-derivation chain. No open question is attached; the record is fully discharged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.