structure
definition
DimensionedQuantity
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Constants.Dimensions on GitHub at line 94.
browse module
All declarations in this module, on Recognition.
explainer page
Derivations using this theorem
depends on
-
of -
of -
of -
Dimension -
mul -
T -
T -
T -
of -
of -
of -
Dimension -
mul -
A -
of -
of -
of -
mul -
of -
of -
of -
for -
for -
T -
T -
T -
of -
of -
of -
A -
Status -
A -
dim -
dim -
dim -
dim -
value -
value -
value -
value
used by
formal source
91/-! ## Dimensioned Quantities -/
92
93/-- A dimensioned physical quantity with its value and dimensional signature. -/
94structure DimensionedQuantity where
95 value : ℝ
96 dim : Dimension
97
98/-- A positive dimensioned quantity (for physical constants). -/
99structure PositiveDimensionedQuantity extends DimensionedQuantity where
100 value_pos : 0 < value
101
102/-- Multiplication of dimensioned quantities. -/
103noncomputable def DimensionedQuantity.mul (q1 q2 : DimensionedQuantity) : DimensionedQuantity :=
104 ⟨q1.value * q2.value, ⟨q1.dim.L + q2.dim.L, q1.dim.T + q2.dim.T, q1.dim.M + q2.dim.M⟩⟩
105
106/-- Division of dimensioned quantities. -/
107noncomputable def DimensionedQuantity.div (q1 q2 : DimensionedQuantity) : DimensionedQuantity :=
108 ⟨q1.value / q2.value, ⟨q1.dim.L - q2.dim.L, q1.dim.T - q2.dim.T, q1.dim.M - q2.dim.M⟩⟩
109
110/-- Square root of a dimensioned quantity (for even dimension exponents). -/
111noncomputable def DimensionedQuantity.sqrt (q : DimensionedQuantity) : DimensionedQuantity :=
112 ⟨Real.sqrt q.value, ⟨q.dim.L / 2, q.dim.T / 2, q.dim.M / 2⟩⟩
113
114/-! ## Status Report -/
115
116/-- Summary of dimensional analysis module. -/
117def dimensions_status : String :=
118 "✓ Dimension structure [L, T, M] defined\n" ++
119 "✓ Physical constant dimensions (c, ℏ, G) specified\n" ++
120 "✓ Planck unit dimensions documented\n" ++
121 "✓ τ₀ dimension documented as [T]\n" ++
122 "✓ DimensionedQuantity algebra defined"
123
124#eval dimensions_status