15.7. Re-carving, and what a count is keyed to
A carving is not a census, and the two halves of that claim are provable. What survives a re-carving is every licensed aggregate; what does not is how many parts there are.
A re-carving is a map from one carving of a whole to another, carrying the obligation that the measured whole is the same whole. It is the generalization of a pattern physics libraries prove one functional at a time — merging indiscernible parts and checking that each additive functional is unchanged.
Lean code for Definition15.7.1●1 definition
Associated Lean declarations
-
PropertyKindCalculus.Recarving[complete]
-
PropertyKindCalculus.Recarving[complete]
-
structuredefined in PropertyKindCalculus/Recarving.leancomplete
structure PropertyKindCalculus.Recarving.{u} {O : Type u} (m : PropertyKindCalculus.Measurement O) : Type u
structure PropertyKindCalculus.Recarving.{u} {O : Type u} (m : PropertyKindCalculus.Measurement O) : Type u
**A re-carving of a whole**: a map on carvings, with the obligation that the measured whole is left where it was. The obligation is a field rather than a side condition for the reason `WeightedCarving`'s nonzero total is a field — a map that does not preserve the whole is not a re-carving of it, and should not be a term of this type.
Fields
map : PropertyKindCalculus.Decomposition O → PropertyKindCalculus.Decomposition O
The map from one carving of the whole to another.
preserves : ∀ (d : PropertyKindCalculus.Decomposition O), (m (self.map d)).numeral = (m d).numeral
**The obligation**: the whole is the same whole.
Realized as Recarving m, a map and its preserves field. The witness coalesce replaces any
carving by the single part whose mass is the total: fewer entities, same whole, with preserves
holding by rfl.
Every licensed aggregate is re-carving invariant. For an extensive kind the total over the parts is the value of the whole, so a map that preserves the whole preserves the total — whatever it does to the parts. Builds on re-carvings and extensive aggregation.
Lean code for Theorem15.7.2●1 theorem
Associated Lean declarations
-
theoremdefined in PropertyKindCalculus/Recarving.leancomplete
theorem PropertyKindCalculus.Recarving.leafSum_invariant.{u} {O : Type u} {k : PropertyKindCalculus.KindOfProperty} {m : PropertyKindCalculus.Measurement O} (h : PropertyKindCalculus.Extensive k m) (r : PropertyKindCalculus.Recarving m) (d : PropertyKindCalculus.Decomposition O) : PropertyKindCalculus.leafSum m (r.map d) = PropertyKindCalculus.leafSum m d
theorem PropertyKindCalculus.Recarving.leafSum_invariant.{u} {O : Type u} {k : PropertyKindCalculus.KindOfProperty} {m : PropertyKindCalculus.Measurement O} (h : PropertyKindCalculus.Extensive k m) (r : PropertyKindCalculus.Recarving m) (d : PropertyKindCalculus.Decomposition O) : PropertyKindCalculus.leafSum m (r.map d) = PropertyKindCalculus.leafSum m d
**Every licensed aggregate is re-carving invariant.** For an extensive kind the total over the parts *is* the value of the whole, so a map that preserves the whole preserves the total — whatever it does to the parts. This is the law `reduce_sum_eq_sum_toCharges` establishes for one functional in one corner of PhysLib, proved once for every extensive kind.
Two rewrites by the extensive capstone reduce the claim to the preserves field. This is what
makes the \forall-quantified form the deliverable rather
than a convenience: a total that depended on how the whole was cut would fail exactly here.
The count does not survive. The same re-carving that preserves the mass takes a two-part carving to a one-part one. So there is no function from the whole to how many parts it has, and a count is licensed by a sortal rather than by the whole — the SI's own reading of amount of substance as a count of a specified elementary entity. Uses re-carvings.
Lean code for Theorem15.7.3●1 theorem
Associated Lean declarations
-
PropertyKindCalculus.coalesce_count_ne[complete]
-
PropertyKindCalculus.coalesce_count_ne[complete]
-
theoremdefined in PropertyKindCalculus/Recarving.leancomplete
theorem PropertyKindCalculus.coalesce_count_ne : PropertyKindCalculus.Decomposition.count (fun x => true) (PropertyKindCalculus.coalesce.map PropertyKindCalculus.twoParts) ≠ PropertyKindCalculus.Decomposition.count (fun x => true) PropertyKindCalculus.twoParts
theorem PropertyKindCalculus.coalesce_count_ne : PropertyKindCalculus.Decomposition.count (fun x => true) (PropertyKindCalculus.coalesce.map PropertyKindCalculus.twoParts) ≠ PropertyKindCalculus.Decomposition.count (fun x => true) PropertyKindCalculus.twoParts
**The count does not.** The same re-carving takes two parts to one. So there is no function from the whole to how many parts it has, and a library that reports a count is reporting a fact about its carving — which is why a count needs a sortal to be a quantity of the whole at all.
decide on the exhibited pair, against thm_recarving_invariant on the same map: 2 kg before
and after, two parts before and one after. countMeasurement takes the sortal as an argument
and count_sortal_ne checks that the argument matters — one carving, two predicates, counts 2
and 0 — so a count is extensive over a fixed carving and yet not a property of the whole. This
is Marmodoro's "It is an open question how many entities a physical structure is"
(Marmodoro, 2018)Anna Marmodoro, 2018. “Whole, but not One”. In Ontology, Modality, and Mind: Themes from the Metaphysics of E. J. Lowe (Oxford University Press). as a refutation rather than a remark.