15.3. Additivity to within a tolerance (§13.5.2)
The remaining branch of Bunge's four says the value for the total is "approximately equal" to
the sum over the parts. Approximately is a claim about measurement, so the predicate is
stated where the uncertainty is, over \mathbb{R} rather than over the numeral, and its
tolerance is a coverage factor rather than a number chosen to make the claim come out true.
A kind is quasiextensive to within t (§13.5.2) when composing two parts is additive up to
t — at each join, not once for the whole. Naming the tolerance is what turns
"approximately" into a claim: two quasiextensive claims about one measurement are then
comparable, and the sharper is the one with the smaller t. Refines
extensivity.
Lean code for Definition15.3.1●1 definition
Associated Lean declarations
-
structuredefined in PropertyKindCalculus/Uncertainty/QuasiExtensive.leancomplete
structure PropertyKindCalculus.Uncertainty.QuasiExtensive.{u'} {O : Type u'} (k : PropertyKindCalculus.KindOfProperty) (m : PropertyKindCalculus.Measurement O) (t : ℝ) : Prop
structure PropertyKindCalculus.Uncertainty.QuasiExtensive.{u'} {O : Type u'} (k : PropertyKindCalculus.KindOfProperty) (m : PropertyKindCalculus.Measurement O) (t : ℝ) : Prop
**§13.5.2 quasiextensive kind.** A kind `k` is *quasiextensive to within `t`* under a measurement `m` when (i) every part is measured as a value of kind `k` and (ii) the numeral on a disjoint union differs from the sum of its parts' numerals by at most `t`. The tolerance is per **join**, not per whole: it is the balance's rounding, the calibration residual, the contraction on one mixing — one act of composition. What it costs over a whole carving is `quasiExtensive_leafSum`.
Fields
ofKind : ∀ (d : PropertyKindCalculus.Decomposition O), (m d).kind = k
Every measured part is a value of the kind `k`.
nearlyAdditive : ∀ (a b : PropertyKindCalculus.Decomposition O), |↑(m (a.union b)).numeral - (↑(m a).numeral + ↑(m b).numeral)| ≤ t
The single-split law, additive **to within `t`**.
Realized as Uncertainty.QuasiExtensive k m t, the same two-field shape as
Extensive with the additivity equation replaced by
\lvert v(a \sqcup b) - (v(a) + v(b)) \rvert \le t. Where the tolerance comes from is R18's
business: join_within_tolerance specializes the Chebyshev
coverage bound to a mean-zero join discrepancy, so a
per-join tolerance of k standard uncertainties carries probability at least 1 - 1/k^2.
Quasiextensive aggregation. For a kind quasiextensive to within t, the value measured on
the whole differs from the sum over all atomic parts by at most the carving's join count times
the tolerance,
\Bigl\lvert v\Bigl(\bigsqcup_i s_i\Bigr) - \sum_i v(s_i) \Bigr\rvert \le \mathrm{joins} \cdot t.
That the bound grows with the carving is the content, not a weakness of the proof: a library
reporting one tolerance for a total however the total was assembled is reporting the wrong
number, and this says by how much. Builds on quasiextensive kinds.
Lean code for Theorem15.3.2●1 theorem
Associated Lean declarations
-
theoremdefined in PropertyKindCalculus/Uncertainty/QuasiExtensive.leancomplete
theorem PropertyKindCalculus.Uncertainty.quasiExtensive_leafSum.{u'} {O : Type u'} {k : PropertyKindCalculus.KindOfProperty} {m : PropertyKindCalculus.Measurement O} {t : ℝ} (h : PropertyKindCalculus.Uncertainty.QuasiExtensive k m t) (d : PropertyKindCalculus.Decomposition O) : |↑(m d).numeral - ↑(PropertyKindCalculus.leafSum m d)| ≤ ↑d.joins * t
theorem PropertyKindCalculus.Uncertainty.quasiExtensive_leafSum.{u'} {O : Type u'} {k : PropertyKindCalculus.KindOfProperty} {m : PropertyKindCalculus.Measurement O} {t : ℝ} (h : PropertyKindCalculus.Uncertainty.QuasiExtensive k m t) (d : PropertyKindCalculus.Decomposition O) : |↑(m d).numeral - ↑(PropertyKindCalculus.leafSum m d)| ≤ ↑d.joins * t
**Quasiextensive aggregation (the capstone).** The value measured on the whole differs from the sum over all atomic parts by at most `joins · t` — the per-join tolerance times the number of joins the carving actually has. Proved by induction on the decomposition, exactly as `extensive_additive` is: at a leaf the discrepancy is zero over zero joins, and at a union the triangle inequality splits it into this join's tolerance plus the two sub-carvings' accumulated bounds. That the bound depends on the carving and not only on the whole is not a weakness of the proof — it is the reason §13.5.2 needed a formalization separate from §13.5.1.
By induction on the decomposition, exactly as the §13.5.1 capstone: at a leaf the discrepancy is zero over zero joins, and at a union the triangle inequality splits it into this join's tolerance plus the two sub-carvings' accumulated bounds. The witness is a balance whose composite readings carry one digit of rounding — quasiextensive to within 1, and not extensive, so the branch is occupied by something §13.5.1 excludes.
§13.5.1 is §13.5.2 at zero tolerance. A kind is extensive exactly when it is quasiextensive to within nothing at all — so the branches are nested rather than parallel, and a tolerance is not hiding a weaker law. Uses quasiextensive kinds and extensive kinds.
Lean code for Theorem15.3.3●1 theorem
Associated Lean declarations
-
theoremdefined in PropertyKindCalculus/Uncertainty/QuasiExtensive.leancomplete
theorem PropertyKindCalculus.Uncertainty.extensive_iff_quasiExtensive_zero.{u'} {O : Type u'} {k : PropertyKindCalculus.KindOfProperty} {m : PropertyKindCalculus.Measurement O} : PropertyKindCalculus.Extensive k m ↔ PropertyKindCalculus.Uncertainty.QuasiExtensive k m 0
theorem PropertyKindCalculus.Uncertainty.extensive_iff_quasiExtensive_zero.{u'} {O : Type u'} {k : PropertyKindCalculus.KindOfProperty} {m : PropertyKindCalculus.Measurement O} : PropertyKindCalculus.Extensive k m ↔ PropertyKindCalculus.Uncertainty.QuasiExtensive k m 0
**§13.5.1 is §13.5.2 at zero tolerance**, in both directions.
Forward, the additivity equation makes the discrepancy zero; backward, \lvert x \rvert \le 0
forces x = 0. The tolerance is shown to be doing work by the other direction of the same
witness family: volume on mixing refutes every tolerance below the 4 mL water and ethanol
actually contract by (mixing_not_quasiExtensive), so §13.5.3 reads as §13.5.2 with a
tolerance the conditions set.