lemma
proved
ell0_ne_zero
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Constants.Derivation on GitHub at line 74.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
71def ell0 : ℝ := c_codata * tau0
72
73lemma ell0_pos : 0 < ell0 := mul_pos c_codata_pos tau0_pos
74lemma ell0_ne_zero : ell0 ≠ 0 := ne_of_gt ell0_pos
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 ⊢