  75
  76/-! ## RS Unit System Structure -/
  77
  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
  87def canonicalUnits : RSUnitSystem where
  88  τ := tau0
  89  ℓ := ell0
  90  φ_val := phi
  91  τ_pos := tau0_pos
  92  ℓ_pos := ell0_pos
  93  φ_eq := rfl
  94  consistency := rfl
  95
  96/-! ## Derived Constants -/
  97
  98def c_derived (u : RSUnitSystem) : ℝ := u.ℓ / u.τ
  99
 100theorem c_derived_eq_codata (u : RSUnitSystem) : c_derived u = c_codata := by
 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
 107lemma c_derived_pos (u : RSUnitSystem) : 0 < c_derived u := by
 108  rw [c_derived_eq_codata]; exact c_codata_pos

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.