**§13.5.4 intensive kind-of-quantity.** A kind `k` is *intensive* under a measurement `m`
when (i) every part is measured as a value of kind `k`, and (ii) composing two parts **that
already agree** leaves the value where it was: temperature, density, the angular velocity of
a rigid body.

Condition (ii) is Dybkær's definition read literally, and the literal reading is the design.
His §13.5.4 asks that "a physical addition operation does not exist and … a quantity value is
invariant with the extent of a system of constant composition" — and *of constant
composition* is the clause a shorter phrasing drops. Without it the law would assert that
mixing water at 20 °C with water at 80 °C leaves either reading intact. With it, agreement
between the parts is the hypothesis, and what the structure says about parts that *disagree*
is nothing at all: an intensive kind licenses no reading of the whole from unequal parts,
which is a narrower claim than a total law and an honest one. 

ofKind : ∀ (d : PropertyKindCalculus.Decomposition O), (m d).kind = k

Every measured part is a value of the kind `k`. 

uniform : ∀ (a b : PropertyKindCalculus.Decomposition O), (m a).numeral = (m b).numeral → (m (a.union b)).numeral = (m a).numeral

The single-split constancy law, with its hypothesis explicit: two parts reading the
same value compose to a whole reading that value. 

**A whole-proper kind — the case Bunge's four types do not name.** The value of the whole
is produced by *no* aggregation over the parts: neither by summing them (`notAdditive`) nor
by sharing a common reading with them (`notUniform`). The normal-mode frequency of a coupled
pair is the standard case — a lone oscillator has no normal mode at all, so there is nothing
to sum and nothing to inherit. It is not §13.5.4 intensive: the value is not invariant with
the extent of the system, since a third oscillator moves every mode.

Both fields are **exhibited**, as pairs of atomic parts, rather than stated as negated
universals. That is deliberate: a negated universal is satisfied by a measurement that is
merely undefined somewhere, while a witness pins the failure to two parts a reader can point
at — the same discipline `mixing_subadditive` follows for volume, and the reason `assemble`
over such a kind can be shown to return the *wrong number* rather than merely an
unjustified one (`assemble_ne_measured`, `Composite.lean`).

This is Marmodoro's substantial power in the §13.5 vocabulary. Her structural powers
constitute a whole out of parts — the aggregable kinds — while the substantial power "*is*
the electron" (*Whole, but not One*, 2018, §4): borne by the whole, and not by anything the
whole is made of. 

ofKind : ∀ (d : PropertyKindCalculus.Decomposition O), (m d).kind = k

Every measured part is a value of the kind `k`. 

notAdditive : ∃ p q,
  (m ((PropertyKindCalculus.Decomposition.atom p).union (PropertyKindCalculus.Decomposition.atom q))).numeral ≠
    (m (PropertyKindCalculus.Decomposition.atom p)).numeral + (m (PropertyKindCalculus.Decomposition.atom q)).numeral

Two atomic parts whose union does **not** read their sum. 

notUniform : ∃ p q,
  (m (PropertyKindCalculus.Decomposition.atom p)).numeral = (m (PropertyKindCalculus.Decomposition.atom q)).numeral ∧
    (m ((PropertyKindCalculus.Decomposition.atom p).union (PropertyKindCalculus.Decomposition.atom q))).numeral ≠
      (m (PropertyKindCalculus.Decomposition.atom p)).numeral

Two atomic parts that **agree**, whose union does not read their common value.