Legend View Full Graph Group View A dedicated kind joins three things the spine already carries — a sort of system (the definition's "given sort of system"), a component, and a kind-of-property (Ch. 6) — into the IUPAC/IFCC System — Component ; kind designation, the System slot naming the sort. It is a Mathlib-free core module; the worked example "Soil — Water ; volume fraction" versus "… ; mass fraction" is checked in the Examples library. A dimension -one quantity-kind is not a carrier constant. A carrier constant ( π , e ) is a magnitude in the numeric representation, below the kind layer; a characteristic number is a ratio-scale kind of dimension one, above the carrier, formed by the quotient calculus. Distinct characteristic numbers stay distinct kinds at one shared dimension — the measurement principle separates them, never a value. A kind is given a dimension by forgetting everything but its SI base-quantity exponents. To keep the core spine Mathlib-free, the dimension is paired with the kind in this separate library rather than stored on KindOfProperty : an application declares a dimensioned kind with a def , exactly as it declares a kind. The forgetful map then drops the kind identity and keeps the dimension. A kind is the "common defining aspect of mutually comparable properties" (§6.19). It is an open value — applications declare new kinds as def s — and it carries its scale and an optional examination principle (§7.5) used to individuate otherwise-comparable kinds (width vs. height). A kind-of-property is a "common defining aspect" (§6.19). One such defining aspect is how the property is examined : its examination principle (§7.5, VIM4 2CD 2.4) — the phenomenon serving as the basis — a method based on that principle (VIM4 2CD 2.5), and a procedure based on that method (VIM4 2CD 2.7). These refine one another and individuate kinds that scale and dimension alone cannot tell apart: width and height are both rational lengths, separated only by the principle under which each is examined. A description logic can record a link to a defining aspect; it cannot state that refinement is a preorder, nor that refinement preserves the principle. A metrological unit (§18.12) is one quantity of a kind chosen as the reference : "with which any other quantity of the same kind can be compared" (VIM4 2CD 1.12). It belongs to a unitary kind-of-quantity (§13.3.3), whose magnitudes are "a reference quantity multiplied by a number" — the differential (§13.3.4) and rational (§13.3.5) kinds. The two laws specified here are ones a description logic can record an instance of but neither state nor prove: that commensurability — being "of the same kind", the only relation along which a value converts — is an equivalence relation (a relation that is reflexive, symmetric, and transitive, so it partitions units into convertible classes); and that the number-and-reference form is a faithful round-trip. This is the symbolic (numeral-and-reference) layer; the real-valued Quantity k with conversion ratios and the dimension-1 disambiguation are the planned PhysLib refinement, stated in the Units and the Dimension-1 Problem chapter. A property value (§9.15) is an inherent feature of a property used in comparing it with other properties of the same kind-of-property; it is a member of a value scale (§10.14), the ordered set of possible, mutually comparable values of a kind. A quantity value (§16.10) is the special case carried as a numerical value times a reference — Dybkær's "reference quantity multiplied by a number". The laws below — that comparability of values is an equivalence, that a value scale holds only mutually comparable values, that a value's scale type fixes which operations are defined — quantify over relations, operations, and a scale's members; a description logic can record an instance of the link but can neither state nor prove the laws. A quantity carries a magnitude in some numbers ; many physical quantities take that magnitude in the complex numbers. The key observation is metrological, not numerical: complex-ness is a property of the carrier, not of the kind . A complex permittivity (a real part plus j times an imaginary part) is one kind of quantity — a relative permittivity, dimension one, ratio-scale — whose value is complex. It is not two real quantities, and not a new dimension. In the two-index design it is exactly Quantity k (Complex R) : the same kind layer over a complexified carrier, so the algebraic calculus applies verbatim, now computing complex products and quotients. Combination of kinds is a ternary relation, not a binary function: a pair of input kinds may produce a specific output kind (torque × angle → energy) or no kind at all (a category error). Description logic role chains are binary, regular, and arithmetic-free, so they cannot express this; here it is an ordinary relation with proofs. An interaction algebra bundles the sanctioned products an application asserts with a proof that each is dimensionally coherent — so the coherence law below holds for any algebra by construction. Dybkær divides ⟨property⟩ by which algebraic operators are defined between properties of a kind. This is the axis a description logic cannot represent: it is about operations, and DL has none. Each catalogued kind reuses the dimension functor dim over PhysLib's Dimension , but here every kind maps to the same value, dimension one. The distinguishing datum is moved entirely onto the examination principle — the measurement principle, this work's terse descriptor of the defining ratio, paired with the transport-phenomena context (the clause). Each kind still bears values and a coherent unit ( 1 for all); commensurability is a type-level fact, so two characteristic numbers with the same unit symbol 1 are still not interchangeable. Each catalogued kind reuses the dimension functor dim over PhysLib's Dimension , here over mass, length, and time only: the radiation reductions make the candela the dimension of power and the steradian and mole dimension one. The standard's dimensional facts — a radiant flux is M·L²·T⁻³ , an irradiance M·T⁻³ , a molar absorption coefficient an area L² — are checked computations . Each unit is a metrological unit of its kind; commensurability is a type-level fact, so the watt of radiant flux and the lumen of luminous flux are not interchangeable though they share one dimension. Each catalogued kind reuses the dimension functor dim over PhysLib's Dimension , now over the charge generator C (with electric current as C·T⁻¹ ), so the standard's dimensional facts — a capacitance is C²·M⁻¹·L⁻²·T² , a resistance M·L²·T⁻¹·C⁻² , a magnetic flux M·L²·T⁻¹·C⁻¹ — are checked computations rather than annotations. The kinds are dimensioned internally over this charge generator — so the checked facts read in C (a capacitance's charge-exponent is 2 ) — but the item-index tables cite each dimension in the ISQ base quantity current via the change of basis C = I·T , so the printed capacitance is M⁻¹·L⁻²·T⁴·I² exactly as IEC 80000-6 tabulates it. Each unit is a metrological unit of its kind; commensurability is a type-level fact, so an ampere and a volt are not interchangeable. Each catalogued kind reuses the dimension functor dim over PhysLib's Dimension , now over the temperature generator Θ , so the standard's dimensional facts — heat is M·L²·T⁻² , entropy M·L²·T⁻²·Θ⁻¹ , a linear expansion coefficient Θ⁻¹ — are checked computations rather than annotations. Each unit is a metrological unit of its kind; commensurability is a type-level fact, so a kelvin and a joule are not interchangeable. Each catalogued kind reuses the dimension functor dim over PhysLib's Dimension , so the standard's dimensional facts — area is L² , volume is L³ , speed is L·T⁻¹ — are checked computations rather than annotations. Each unit is a metrological unit of its kind; commensurability is a type-level fact, so a metre and a second are not interchangeable. Each catalogued kind reuses the dimension functor dim over PhysLib's Dimension , so the standard's dimensional facts — force is M·L·T⁻² , energy M·L²·T⁻² , pressure M·L⁻¹·T⁻² , power M·L²·T⁻³ — are checked computations rather than annotations. Each unit is a metrological unit of its kind; commensurability is a type-level fact, so a kilogram and a newton are not interchangeable. Following the VIM4 2CD principle (measurement unit, 1.12: a "reference quantity with which any other quantity of the same kind can be compared by ratio") and Dybkær §13.3.3 (a unitary kind value is "a reference quantity multiplied by a number"), units are indexed by the kind they measure. Mass is extensive: the mass of a whole is the sum of the masses of its parts. Volume on mixing is not: ethanol and water mix sub-additively. Tracking which kinds are extensive is a precondition for soundly aggregating measurements. Specializes relates kinds to kinds. Flater (NIST TN 1943 §6.2) stresses the result is a lattice, not a tree. We generate it as the reflexive–transitive closure of an application-supplied direct-parent edge relation, so each "system of quantities" supplies its own hierarchy. The algebraic calculus rides on the toolchain classes for multiplication, division, and reciprocal. There is no toolchain class for exp , sin , or square root, so the one genuinely new artifact is a carrier capability — the function-layer analogue of the numeric carrier — and a family of smart constructors that each carry their own metrological discipline. The functions split into five families with genuinely different kind signatures: kind-preserving ( abs , min , max ); powers and roots (the dimension scales by the exponent); dimensionless transcendentals ( exp , log — pure number in, pure number out); the trigonometric functions (a plane angle in, a number out — curated so that sin of a reflectivity stays a category error); and logarithmic levels (dB, neper — where log of a ratio demotes the scale, so the product calculus correctly refuses it). The canonical pattern is the product , which covers a large fraction of the ISQ (area = length · length, volume = area · length, energy = force · length). The general machinery lives in the Mathlib-free core; the dimensional refinement ( k.dim = k₁.dim · k₂.dim ) lives in the dimension layer, and analysis-shaped relations (area as a surface integral) in the Mathlib-backed layer. The closed-form certificate is the product (a rectangle's area is width × height); the general certificate is the integral (an area is the area of an actual surface). Both classify the one area kind, and a property of the defining relation transports to every quantity certified under it. The dimension layer can detect some scale-spanning units: a unit whose dimension is mechanically reducible — expressible in mass, length, and time alone — is by that fact not dimensionally independent. The candela (power) and the mole (one) are reducible this way. The kelvin is the sharp case: this work keeps thermodynamic temperature Θ as an independent dimension (the Thermodynamics chapter needs it), so the dimension layer sees the kelvin as if it were a base — its scale-spanning character is visible only once one adopts k_B as a defining coefficient, which the dimension layer does not. So scale-spanning is carried, like a kind's identity , above the dimension. The dimension-collision capstone, on standard quantities: the dimension map identifies absorbed dose with dose equivalent, while the kind layer keeps them apart, both as kinds and as units (the gray and the sievert). The becquerel collision ( T⁻¹ ) is the companion. The dimension-collision capstones, on standard quantities: the dimension map identifies the members of each family, while the kind layer keeps them apart, both as kinds and as units . The dimension-one collision capstone, on standard quantities: the dimension map identifies information content, traffic intensity, and storage capacity, while the kind layer keeps them apart, both as kinds and as units (the shannon, the erlang, the bit). The energy species are individuated by an examination principle — here the potential's defining construction — and arranged as a specialization lattice over the general energy kind. The sharpest case is the Helmholtz versus the Gibbs energy: both "free energies" of the same dimension, they are nonetheless different kinds — and the calculus proves it from their differing natural variables, not from a naming convention. The fifth clause is declared aggregation, and it is the port-level form of the mereology chapter's vocabulary: a kind is extensive , intensive , whole-proper , or quasi-extensive , and a weighted carving carries the aggregation license. The clause puts that vocabulary on the boundary — each produced port declares its class — so the license to shard, tile, or stitch a module's batch axis is derived from the declarations rather than held as deployment convention. Requirement R27 states the obligation; the distribution license below is the theorem that discharges it. The force species are individuated by an examination principle and arranged as a specialization lattice over the general force kind. The sharpest case is static versus kinetic friction: physically the same dimension and both "friction forces", they are nonetheless different kinds — and the calculus proves it from their differing measurement conditions, not from a naming convention. The four corners of Lowe's square, as the calculus carries them: the system (substantial particular), its sort (substantial universal), the kind-of-property (non-substantial universal, from the spine), and the individual quantity (mode). The identity discipline Designated is what makes naming a corner a claim. The homonym families are individuated by the examination principle alone — distinct_of_examPrinciple , not the id strings, which are equal. Every characteristic number has the same coherent unit symbol 1 , so the unit cannot tell them apart either; yet two are not commensurable, because they reference different kinds. The interaction algebra is curated , and it pays to be precise about what the type system guarantees for a curated edge: explicitness and propagation, not truth . Every kind-changing operation demands a witness naming the full kind equation at its call site, and no mechanism — no inference, no instance search, no coercion — can introduce an edge silently. But whether a written edge is metrologically right is the author's claim, exactly as an axiom is a claim a proof assistant checks everything against but never for . This section fixes the two poles the discipline sits between, and shows the residue between them is finite, local, and mechanically enumerable. The interface clause and the judgments on it. A boundary is declared , so a membership choice can be wrong about it — and the two decidable comparisons below are exactly the two ways it can be wrong: not the boundary the members compute, or not a faithful deployment of the tier below. The kelvin and the degree Celsius are both well-formed metrological units — a kind bears a unit from the differential (interval) scale upward, not only from ratio scale, so the degree Celsius is a legitimate unit even though × , ÷ are undefined on Celsius temperatures. What separates the two kinds is the scale type : ratio versus interval. The length species are individuated by an examination principle and arranged as a specialization lattice over the general length kind. This is what lets the calculus answer the question the standard leaves to prose — why is a width not a distance? — with a proof rather than a naming convention, while keeping the two comparable so an explicit up-cast to length is still available. The metric tensor is realized as the Gram matrix of the two tangent vectors ∂r/∂u , ∂r/∂v (its entries are the classical E , F , G ); its determinant is g ; and the surface element is dA = √g . The standard writes the element with g ; the area-consistent Riemannian element is its square root , and the formalization makes that convention explicit by proving that a flat patch then recovers its Euclidean area. The kind whose magnitudes these areas are is the catalogued quantity -kind area, dimension L² . The metric tensor of a region is the 3 × 3 Gram matrix of its three tangent vectors; its determinant is g ; the volume element is dV = √g , and the volume is its integral. The kind is the catalogued quantity -kind volume, dimension L³ . The object of an individual quantity (the foundations chapter's mode) ranges over an arbitrary type. The gate needs nothing from it; the designation needs Designated , whose injectivity field is what distinguishes a designation from a formality. The particular-side mereology as data: the carving (a description of a whole into parts, one among many) and the part/whole roles a single portion-total pair carries. The power species are individuated by an examination principle — here which component of the periodic process the quantity isolates — and arranged as a specialization lattice over the general power kind. The sharpest case is active versus reactive power: both "powers" of the same dimension, they are nonetheless different kinds — and the calculus proves it from their differing defining constructions, not from a naming convention, while the standard itself separates their units, W from var . The prefix layer is added beside the metrological-unit layer, not inside it: a prefixed unit carries its provenance — which prefix, which base — and projects to an ordinary metrological unit of the same kind. So every fact already proved about units (commensurability, well-formedness) transfers to the projection unchanged, while the provenance lets the conversion factor and the multiple/submultiple distinction be read off rather than restated. The product , quotient , and reciprocal families carry the kind-laws. Three payoffs on the standard's own definitions: the constitutive structure of circuit theory is made explicit; the dimension follows from the relation as a checked computation; and a verified-by-construction quantity carries its classification certificate. The quotient , reciprocal , and product families carry the kind-laws. Three payoffs on the standard's own remarks: the cross-part dependency structure of the ISQ is made explicit; the dimension follows from the relation as a checked computation; and a verified-by-construction quantity carries its classification certificate. The quotient and reciprocal families carry the kind-laws. Three payoffs on the standard's own remarks: the cross-part dependency structure of the ISQ is made explicit; the dimension follows from the relation as a checked computation; and a verified-by-construction quantity carries its classification certificate. The quotient and reciprocal families generalize the product kind-law. Two payoffs on the standard's own remarks: the dimension follows from the relation as a checked computation, and a verified-by-construction quantity carries its classification certificate, instantiable at the quantity level. The seal of a module and what it rests on: well-formedness of the provenance hypergraph, agreement of the declared boundary with the computed one ( the declared boundary ), and the reachability reading of the pedigree. Everything the statement rests on exists and is proved; the theorem is the one statement nobody has yet made over it. The seal of the computation: the second capstone relates the tape graph to the provenance hypergraph, transports the hypergraph's kinds onto it through a weak bisimulation, and states the seal for the computation at every carrier through the denotation bridge. The series is a joint ISO/IEC project, and this work catalogues thirteen of its parts. Each part is issued under one body — in the catalogued copies parts 6 ( Electromagnetism ) and 13 ( Information science and technology ) are IEC and the rest are ISO — and carries an edition designation and a publication date on its cover. Recording these as typed data lets a downstream model render or audit a citation rather than carry it as free text. The sixth clause is a stated requirement per produced port: what the port's quantity must satisfy, and the evidence by which it is met — a theorem edge to a specification boundary or a theorem, with spot checks where the model runs; a gate against a marked referent; or an attestation with its reason. The four definitions carry the data, the commands beside them check, survey, census and gate it, and the witness at the end of the chapter is the tutorial's oscillator carrying the clause in both categories. The three levels are distinct dimension-one quantity -kinds. Their decibel units share the symbol dB and the dimension one, yet are not commensurable — the kind layer keeps the level of pressure from being read as the level of power. The trio members are individuated by an examination principle — the radiation mode — and (the luminous and radiant members) collide in dimension. The sharpest case is radiant versus luminous flux: both M·L²·T⁻³ , they are nonetheless different kinds, and the calculus proves it from their differing radiation modes, not from a naming convention. The uncertainty layer rests on one additive descriptor placed alongside a quantity's magnitude. It has two faces, matching its two consumers: carrier-parametric moment data (what the linearized methods consume and what the ℝ -level theorems are proved about), and a sampler (the inverse-CDF, the single primitive shared by the Monte Carlo and systematic methods). The support range is carried too, because it is exactly the datum the numerical-adequacy check needs — the architectural hinge that makes the two halves of this chapter one design. The volt of electric potential and the volt of electric potential difference are both well-formed metrological units — a kind bears a unit from the differential (interval) scale upward, not only from ratio scale, so the gauge-dependent potential still bears the volt even though × , ÷ are undefined on it. What separates the two kinds is the scale type : interval versus ratio — and so the two volts, the same string over the same dimension, are not commensurable. These are the dimension-1 disambiguation capstone, now on standard quantities rather than a constructed example: the dimension map identifies the members of each pair, while the kind layer keeps them apart, both as kinds and as units . These are the dimension-disambiguation capstone, on standard quantities: the dimension map identifies the members of each pair, while the kind layer keeps them apart, both as kinds and as units . These are the dimension-disambiguation capstone, on standard quantities: the dimension map identifies the members of each pair, while the kind layer keeps them apart, both as kinds and as units — here even when the units share a symbol. These are the dimension-disambiguation capstone, on standard quantities: the dimension map identifies the members of each pair, while the kind layer keeps them apart, both as kinds and as units — here even where the standard spends a different unit string on each kind of one dimension. These are the dimension-disambiguation capstones, on standard quantities: the dimension map identifies the members of each set, while the kind layer keeps them apart, both as kinds and as units . The sharpest is the scale-spanning collision — a base-quantity unit (the candela) sharing a dimension with a derived one (the watt), separated only by kind. These five steps are the order in which a PropertyKindCalculus model is authored. Each rests on the layer beneath it; the first four are shown with where the MiniWriteOnce worked example realizes them, the fifth with the tutorial's oscillator exhibit. With Dim.amountOfSubstance = 1 , the dimension map sends every molar quantity to the dimension of its non-molar counterpart. The reduction is a checked computation , not a stipulation.
Graph options