A Property Kind Calculus for Measurement Metrology

Blueprint Summary🔗

Overview
Total entries290completed: 285; deps incomplete: 0; sorries: 0; no proof: 0
Ready now5Entries with an actionable next formalization step.
Fully closed285Local code and prerequisite closure are both complete.
Actionable priorities0Entries ready now and already unlocking downstream work.
Entry index (290)
Definitions121completed: 116; deps incomplete: 0; sorries: 0; no proof: 0
Theorems169completed: 169; deps incomplete: 0; sorries: 0; no proof: 0
Informal-only entries5
Definition Index (121)
Theorem / Proposition / Lemma / Corollary Index (169)
By parent groups (54)
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 . (3)
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. (3)
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. (2)
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. (4)
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. (4)
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. (2)
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. (2)
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. (2)
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). (1)
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. (2)
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. (1)
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. (2)
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³ . (1)
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. (2)
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. (3)
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. (1)
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. (2)
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. (5)
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. (1)
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. (2)
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. (3)
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. (1)
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. (2)
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. (1)
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. (2)
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. (3)
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 . (3)
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² . (3)
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. (2)
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). (3)
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 . (3)
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. (2)
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. (2)
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). (2)
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. (18)
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. (3)
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. (4)
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. (3)
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. (3)
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. (21)
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. (2)
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. (2)
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 . (2)
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. (1)
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. (2)
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. (1)
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. (6)
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. (1)
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. (3)
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. (2)
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. (2)
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. (2)
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. (2)
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. (2)
Dependency insights
Statement-used entries92Entries reused in statement dependencies.
Proof-used entries26Entries reused in proof-only dependencies.
Tracked parent groups60Grouped health rollups for parents with more than one child entry.
Most used in statements (92)
Most used in proofs (26)
Group health (60)
  • 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.«write-once»
    Grouped view over entries sharing the same parent.
    total: 5closed: 0local-only: 0ready: 5blocked: 0incomplete Lean: 0unlock score: 0
    Next: «wo-boundary» stage: statementdownstream unlocks: 0
  • 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.spine_scale
    Grouped view over entries sharing the same parent.
    total: 3closed: 3local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 167
    Next: no ready child currently unlocks downstream work.
  • 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.units
    Grouped view over entries sharing the same parent.
    total: 15closed: 15local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 134
    Next: no ready child currently unlocks downstream work.
  • 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).spine_kind
    Grouped view over entries sharing the same parent.
    total: 6closed: 6local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 132
    Next: no ready child currently unlocks downstream work.
  • 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.dimension
    Grouped view over entries sharing the same parent.
    total: 3closed: 3local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 77
    Next: no ready child currently unlocks downstream work.
  • 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.extensivity
    Grouped view over entries sharing the same parent.
    total: 31closed: 31local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 64
    Next: no ready child currently unlocks downstream work.
  • 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.foundations_square
    Grouped view over entries sharing the same parent.
    total: 4closed: 4local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 50
    Next: no ready child currently unlocks downstream work.
  • 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.uncertainty
    Grouped view over entries sharing the same parent.
    total: 29closed: 29local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 38
    Next: no ready child currently unlocks downstream work.
  • 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.spine_value
    Grouped view over entries sharing the same parent.
    total: 4closed: 4local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 32
    Next: no ready child currently unlocks downstream work.
  • 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.spine_unit
    Grouped view over entries sharing the same parent.
    total: 4closed: 4local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 29
    Next: no ready child currently unlocks downstream work.
  • Show all 50 more groups
    • 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.foundations_carving
      Grouped view over entries sharing the same parent.
      total: 2closed: 2local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 25
      Next: no ready child currently unlocks downstream work.
    • 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.spine_examination
      Grouped view over entries sharing the same parent.
      total: 7closed: 7local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 22
      Next: no ready child currently unlocks downstream work.
    • 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.capstones_semantic
      Grouped view over entries sharing the same parent.
      total: 9closed: 9local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 18
      Next: no ready child currently unlocks downstream work.
    • 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).functions
      Grouped view over entries sharing the same parent.
      total: 5closed: 5local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 18
      Next: no ready child currently unlocks downstream work.
    • 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.capstones_seal
      Grouped view over entries sharing the same parent.
      total: 5closed: 5local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 17
      Next: no ready child currently unlocks downstream work.
    • 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.spine_specialization
      Grouped view over entries sharing the same parent.
      total: 4closed: 4local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 16
      Next: no ready child currently unlocks downstream work.
    • 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.interaction
      Grouped view over entries sharing the same parent.
      total: 4closed: 4local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 13
      Next: no ready child currently unlocks downstream work.
    • 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.classification
      Grouped view over entries sharing the same parent.
      total: 5closed: 5local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 12
      Next: no ready child currently unlocks downstream work.
    • 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.metrological_modularity
      Grouped view over entries sharing the same parent.
      total: 4closed: 4local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 10
      Next: no ready child currently unlocks downstream work.
    • 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.scale_spanning
      Grouped view over entries sharing the same parent.
      total: 7closed: 7local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 8
      Next: no ready child currently unlocks downstream work.
    • 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.spine_dedicated
      Grouped view over entries sharing the same parent.
      total: 6closed: 6local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 8
      Next: no ready child currently unlocks downstream work.
    • 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.object_types
      Grouped view over entries sharing the same parent.
      total: 8closed: 8local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 6
      Next: no ready child currently unlocks downstream work.
    • 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.metrological_modularity_requirement
      Grouped view over entries sharing the same parent.
      total: 5closed: 5local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 1
      Next: no ready child currently unlocks downstream work.
    • 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.complex
      Grouped view over entries sharing the same parent.
      total: 3closed: 3local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 1
      Next: no ready child currently unlocks downstream work.
    • 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.metrological_modularity_mereology
      Grouped view over entries sharing the same parent.
      total: 2closed: 2local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 1
      Next: no ready child currently unlocks downstream work.
    • 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.iso80000
      Grouped view over entries sharing the same parent.
      total: 2closed: 2local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 1
      Next: no ready child currently unlocks downstream work.
    • 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.iso80000_part3
      Grouped view over entries sharing the same parent.
      total: 5closed: 5local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • 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² .iso80000_part3_area
      Grouped view over entries sharing the same parent.
      total: 5closed: 5local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • 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.iso80000_part11_homonyms
      Grouped view over entries sharing the same parent.
      total: 4closed: 4local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • 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.iso80000_part3_length
      Grouped view over entries sharing the same parent.
      total: 4closed: 4local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • 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.iso80000_part11
      Grouped view over entries sharing the same parent.
      total: 3closed: 3local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • 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.iso80000_part6
      Grouped view over entries sharing the same parent.
      total: 3closed: 3local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • 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.iso80000_part5
      Grouped view over entries sharing the same parent.
      total: 3closed: 3local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • 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.iso80000_part4
      Grouped view over entries sharing the same parent.
      total: 3closed: 3local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • 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.iso80000_part10_collision
      Grouped view over entries sharing the same parent.
      total: 3closed: 3local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • 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 .iso80000_part12_collision
      Grouped view over entries sharing the same parent.
      total: 3closed: 3local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • 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).iso80000_part13_units
      Grouped view over entries sharing the same parent.
      total: 3closed: 3local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • 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.iso80000_part5_energy
      Grouped view over entries sharing the same parent.
      total: 3closed: 3local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • 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.iso80000_part4_force
      Grouped view over entries sharing the same parent.
      total: 3closed: 3local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • 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 .iso80000_part6_power
      Grouped view over entries sharing the same parent.
      total: 3closed: 3local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • 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.iso80000_part7_trios
      Grouped view over entries sharing the same parent.
      total: 3closed: 3local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • 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 .iso80000_part3_collision
      Grouped view over entries sharing the same parent.
      total: 3closed: 3local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • 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 .iso80000_part4_collision
      Grouped view over entries sharing the same parent.
      total: 3closed: 3local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • 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.iso80000_part5_collision
      Grouped view over entries sharing the same parent.
      total: 3closed: 3local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • 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.iso80000_part6_collision
      Grouped view over entries sharing the same parent.
      total: 3closed: 3local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • 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.iso80000_part11_kind_not_constant
      Grouped view over entries sharing the same parent.
      total: 2closed: 2local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • 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.iso80000_part7
      Grouped view over entries sharing the same parent.
      total: 2closed: 2local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • 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.iso80000_part3_classified
      Grouped view over entries sharing the same parent.
      total: 2closed: 2local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • 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.trustmodel
      Grouped view over entries sharing the same parent.
      total: 2closed: 2local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • 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.iso80000_part5_scale
      Grouped view over entries sharing the same parent.
      total: 2closed: 2local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • 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³ .iso80000_part3_volume
      Grouped view over entries sharing the same parent.
      total: 2closed: 2local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • 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.iso80000_part3_prefix
      Grouped view over entries sharing the same parent.
      total: 2closed: 2local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • 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.iso80000_part6_relations
      Grouped view over entries sharing the same parent.
      total: 2closed: 2local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • 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.iso80000_part4_relations
      Grouped view over entries sharing the same parent.
      total: 2closed: 2local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • 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.iso80000_part5_relations
      Grouped view over entries sharing the same parent.
      total: 2closed: 2local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • 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.iso80000_part3_relations
      Grouped view over entries sharing the same parent.
      total: 2closed: 2local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • 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.iso80000_part8_levels
      Grouped view over entries sharing the same parent.
      total: 2closed: 2local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • 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.iso80000_part6_scale
      Grouped view over entries sharing the same parent.
      total: 2closed: 2local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • 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.iso80000_part7_collision
      Grouped view over entries sharing the same parent.
      total: 2closed: 2local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
    • 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.iso80000_part9_mole
      Grouped view over entries sharing the same parent.
      total: 2closed: 2local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
Metadata
Owners in use1Distinct owners referenced by the current blueprint entries.
Tags in use2Distinct tags currently attached to blueprint entries.
Owner rollups (1)
  • Nicolas Rouquetteauthor_nfr
    entries: 14actionable: 0quick wins: 0linked PRs: 0
Tag rollups (2)
  • tag: proved
    entries: 164actionable: 0quick wins: 0linked PRs: 0
  • tag: capstone
    entries: 37actionable: 0quick wins: 0linked PRs: 0
Metadata audit
Missing owner276
Missing effort156
Untagged126
Missing owner (276)
Missing effort (156)
Untagged (126)
Structure and coverage
Informal-only5Statements with no associated Lean code yet.
Ready to formalize5Entries with an actionable next formalization step.
Fully closed285Local code and ancestor closure are both complete.
Heaviest prerequisites (227)
No prerequisites (63)
No dependents (190)