pith. machine review for the scientific record. sign in
structure definition def or abbrev high

RSUnitSystem

show as:
view Lean formalization →

The RS unit system structure packages positive real scales for time and length together with the golden ratio value, constrained by the relation that length equals the CODATA speed of light times time. Researchers deriving constants from Recognition Science primitives cite this to construct canonical units. The definition consists of a direct record with field assertions for positivity and consistency.

claimAn RS unit system consists of positive real numbers $τ$ (time scale) and $ℓ$ (length scale) along with $φ = (1 + √5)/2$ such that $ℓ = c ⋅ τ$, where $c$ is the CODATA speed of light.

background

The module derives physical constants from Recognition Science using CODATA references for the speed of light, reduced Planck constant, and gravitational constant. Key definitions include c_codata as 299792458 and related quantities like tau0 defined via the square root expression from the mass formula. The structure provides the packaging for these scales with the golden ratio fixed at its algebraic value. Upstream results establish the positivity of c_codata and the definition of tau0 as the fundamental time scale satisfying tau0 squared equals hbar G over pi c to the fifth.

proof idea

The declaration is a plain structure definition that directly specifies the six fields without applying any lemmas or performing reductions.

why it matters in Recognition Science

This structure is the central interface for RS unit systems and is used to define canonicalUnits, which in turn supports theorems showing that the derived speed of light matches the CODATA value. It connects the phi-ladder and J-uniqueness from the forcing chain to concrete constants, enabling verification of the alpha band and other predictions. The construction touches the question of how the eight-tick octave manifests in measurable units.

scope and limits

formal statement (Lean)

  78structure RSUnitSystem where
  79  τ : ℝ
  80  ℓ : ℝ
  81  φ_val : ℝ
  82  τ_pos : 0 < τ
  83  ℓ_pos : 0 < ℓ
  84  φ_eq : φ_val = (1 + sqrt 5) / 2
  85  consistency : c_codata * τ = ℓ
  86

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.