2.15. Out of scope (for now)🔗

User-specified base units — making the dimension system parametric in the chosen base set (so a quantity's dimensional decomposition is relative to a choice of generators, expressing e.g. Gaussian-CGS electromagnetism, natural units, or the four-base Finkelstein system) — was out of scope in an earlier draft and is now delivered. We made PhysLib's Dimension itself parametric in its basis and contributed the change upstream (github.com/leanprover-community/physlib/issues/1441, pull request 1447), where it has since been merged; PKC consumes it from leanprover-community/physlib master. The former fixed five-generator type is recovered as the default instance, so no existing result changes. The contribution did not stop at the dimension side: the unit twin is parametrized in the same basis (UnitScale B with its conversion-factor homomorphism dimScale, which PKC's VIM4 §1.22 prefix conversion instantiates at a single generator), and the seven-generator ISQ basis together with the embedding/projection bridge to the five-generator one are upstream as well. The division of labour that leaves is the one this development argues for throughout: the dimensional algebra — bases, homomorphisms between them, unit scaling — belongs in the physics library, while the kind layer and the catalogue's stances belong here. PKC then realizes the angle-augmented basis — PhysLib's five generators together with angle — as one instantiation among several (Gaussian-CGS, natural units, the four-base Finkelstein system, the seven-generator current-based ISQ of ISO/IEC 80000-1): in it plane angle, solid angle, and a pure number are dimensionally distinct (solid angle the square of plane angle, sr = rad²) and torque is energy per angle (so torque ≠ energy), the very separations the five-generator group cannot draw. The ISO 80000 catalogue stays faithful to the standard (SI convention, plane angle dimension one) in the five-generator basis and lifts into any of these along the injective embedding of those generators, with every kind invariant under the lift — a proved change-of-basis theorem. Not every such lift is an embedding of generators: passing to the current-based ISQ sends the charge generator to the product I·T (the coulomb as ampere-second), so it is realized not by reindexing generators but as a genuine group homomorphism, proved injective and hence lossless, and paired upstream with a projection that retracts it (Dimension.toISQHom, toISQHom_injective, fromISQHom_comp_toISQHom; consumed in IsqBase). The catalogue turns this to account for citation: its kinds are dimensioned internally over PhysLib's charge generator, yet the item-index dimensional formulae it prints are rendered in the ISQ base quantity current, so a capacitance reads M⁻¹·L⁻²·T⁴·I² exactly as IEC 80000-6 tabulates it rather than in the internal charge encoding. The same instantiation shows the mole/candela reduction to be a stance rather than a lack: the ISQ offers independent generators for amount of substance and luminous intensity, and the catalogue declines them (the mole stays dimension one, the candela stays power under the lift), so R13 is a modeling choice the change of basis preserves, not an artifact of the five-generator type. Committing the catalogue to one reformed basis would merely privilege a single contested proposal, which is exactly what the parametricity avoids. So the controversy over which units are base is answered on both layers: a kind is invariant under the choice of base, and only its dimensional shadow changes. R13 captures the specific base/scale-spanning/derived controversy over the five-generator basis.

Value representation in the structural sense — coordinate frames, tensor variance, bound-versus-free vectors, and frame transformations — is a separate, orthogonal axis, distinct from R10's numeric carrier R and R11's numerical array. Its principled home is an index over the kind, never a layer the kind hangs beneath (the inversion the Why a calculus, not a taxonomy section charges against SysML v2), and R20 above now occupies exactly that position: InFrame f var k R indexes a reading by its frame and its variance, and the invariance of a scalar product under an orthonormal change of frame is a theorem rather than a convention.

The axis is specified for Cartesian frames, which is less than the full requirement. What R20 states as owed, and this section keeps owed with it: the covariant/contravariant split for non-orthogonal changes (under an orthonormal change the two laws coincide, which is why one vector variance suffices there), curvilinear coordinates, bound-versus-free vectors, and affine frames. Naming the remainder is what keeps the boundary honest now that the first part is discharged.