2.7. Value representation in the structural sense: frames and variance (R20)
R20 — Components carry the frame they were read in and the variance they transform
with; a scalar product is invariant under an orthonormal change of frame and a
component is not. R11 above specifies the numerical half of ISO 80000-2 §18 and is
silent on the sentence the standard puts next to it: the quantity is independent of
the choice of coordinate system while its numerical components are not. Independence
of a choice is not a property an array has — it is a property of how the array
behaves when the choice changes — so Quantity k (Fin n → R) does not record that a
choice was made at all.
InFrame f var k R adds the two indices that do: the Frame the components were
read in, and the Variance (scalar, vector, rank-2) whose transformation law they
obey. Three points make this an axis of its own rather than a second kind of unit:
-
A frame change is dimension-blind. A unit change acts through the dimension — the factor
UnitScale.dimScalecomputes is a function of it — so the dimension layer supplies unit covariance unaided (R7, R17). A frame change acts through the carrier: position, velocity, force and field all turn by the same matrix, and their dimensions have no bearing on it. Nothing multiplicative reaches variance, so no refinement of the dimension basis reaches it either. -
The frame is an index, where the unit is not. A kind determines a canonical unit and a conversion is recoverable from the dimensions; neither holds of a frame, and two readings of one quantity in two frames agree in kind, dimension, unit, object and carrier. There is nothing else left to catch the mixture.
-
What survives is a theorem.
dot_toFrameVectorproves the scalar product invariant under an orthonormal change, andcomponent_not_invariantexhibits a component that differs — stated with a witness so the first result cannot be over-read. Together with the functoriality of the action (toFrameVector_id,toFrameVector_comp) these are the frame twin of R17's unit round-trip.
The definitions are carrier-parametric and Mathlib-free, so a change of frame runs
at Float and specifies at \mathbb{R}; the laws live in FrameReal, the same
split Quantity/QuantityReal already uses.
Scope, stated as scope. The transformations are linear changes of Cartesian
frame, and under an orthonormal change the covariant and contravariant laws coincide
(C^{-1} = C^{\top}), so one vector variance suffices. IsOrthonormal is a
hypothesis on the theorems that need it and never a field of FrameChange, so a
general linear change remains expressible while the results state their price. Still
owed, and named here rather than assumed away: the covariant/contravariant split for
non-orthogonal changes, curvilinear coordinates, bound-versus-free vectors, and
affine frames — an origin as well as a basis, which positions need and velocities do
not.