Physlib.Units.ParametricDimensionExamples
Examples: parametric dimensions and comparing dimensioned quantities
`Dimension B` is parameterised by a basis `B` of base dimensions. This module illustrates two consequences.
Comparing a length with a velocity times a time
A recurring question is how to compare a quantity of dimension `length` with a product of a quantity of dimension `length / time` and a quantity of dimension `time`. The two dimensions are *equal*, but this equality is a **group cancellation law** on the rational exponents — it holds *propositionally*, never *definitionally*:
* `(L𝓭 / T𝓭) * T𝓭 = L𝓭` cannot be closed by `rfl`: cancellation is not a reduction rule. * nor by `decide`: the exponents are rational, so the kernel has nothing to evaluate.
Consequently `WithDim ((L𝓭 / T𝓭) * T𝓭) ℝ` and `WithDim L𝓭 ℝ` are genuinely different types, and a bare `x = v * t` is a type error. The bridge is `WithDim.cast`, whose default argument discharges the propositional dimension equality automatically, so the comparison is a one-liner. This is not a limitation of the representation: no representation of `Dimension` makes the equality definitional, so a cast on a proven equality is the correct idiom.
A non-standard basis
Because `Dimension` is parametric, the same dimensional algebra and the same `cast`-based comparison are available over *any* basis — not just the physical `LTMCTDimensionBase`. The unit-scaling layer (`LTMCTUnitChoices`, `dimScale`) is not needed for either the algebra or the comparison, so neither is referenced here.
This module is illustrative and should not be imported by other modules.
The same comparison over a non-standard basis
A basis with two base dimensions of its own — `bit` and `symbol` — that `LTMCTDimensionBase` does not have. Nothing in the standard units system is involved.
4 declarations
Information-theoretic base dimensions
The inductive type `Info` defines a basis for information-theoretic dimensions. It serves as a set of base dimensions for a dimensional analysis system, specifically containing constructors for the base dimensions of a "bit" and a "symbol".
The bit dimension in the basis
The dimension is an element of the dimension space over the information-theoretic basis . It is defined by assigning an exponent of to the "bit" base dimension and an exponent of to the "symbol" base dimension.
Base dimension of a in
The dimension representing a within the information-theoretic basis . It is defined by assigning an exponent of to the base dimension and an exponent of to the base dimension.
Dimension basis for information-theoretic dimensions
The instance `instDimensionBasisInfo` establishes the type `Info` as a valid basis for a system of dimensions. This allows for the construction of dimensions based on the information-theoretic base units of a "bit" and a "symbol".