8.3. The carving — mereology as data, wholes by sortal🔗

With the square in place, the two levels of Dybkær's implied mereology get one carrier each, and the flexibility both sources demand is a theorem-shaped commitment rather than a mood. Marmodoro's distinction says why flexibility is forced: "physical structure unites; while metaphysical structure unifies. The former brings about wholes, the latter unities. But wholes are not always unities" — and a physical structure is "numberless", bringing no count principle with it: "Alternative carvings of the world deliver alternative numbers of entities" (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).. The particular-side mereology is therefore data, quantified over: a carving of a system, never the carving. Unification — being one whole of a sort, with a license to aggregate — is a separate act, supplied when a model declares a sort and instantiates a composite (the object-type chapter), "under the individuation principle of the sortal"; Dybkær's sort of system is that sortal under another name. The host library this work targets confirms the design from the other side: its rigid body is a single mass functional whose parts occur only as bound points inside integrands, so a foundation that made the parts of a system a stored fact would misdescribe the very objects it aims at.

Definition8.3.1

groupuses 1

Used by 4

Reverse dependency previews

Preview

Definition 15.1.1

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

A carving of a whole into parts drawn from an arbitrary type — a system's subsystems, a host library's own particles — as a binary tree of joins. Deliberately not a census: nothing in a carving claims the parts are disjoint, exhaustive, or all there are, and nothing fixes how many parts a system has. It is Dybkær's §3.2 "partition into components" with §3.3 Note 5's observer-relativity taken at face value: the carving is the observer's act, so every law that consumes one is quantified over all of them.

Lean code for Definition8.3.1●1 definition

inductive(2 constructors, 1 parameter)defined in PropertyKindCalculus/Mereology.lean

complete

inductive PropertyKindCalculus.Decomposition.{u} (O : Type u) : Type u

inductive PropertyKindCalculus.Decomposition.{u}
  (O : Type u) : Type u

A **decomposition** of a system into parts (Dybkær §3.3's demarcated arrangement, the
carving of the foundations chapter): an atomic part, or the union of two sub-carvings. The
leaves are the atomic parts; each node stands for the whole they compose. Disjointness and
exhaustiveness of the parts are the model's reading, not the type's claim — which is what
lets the laws quantify over all carvings and lets the refutations (`Recarving.lean`) build
the carvings a census would forbid.

Parameterized over the **part type** `O` for the reason `IndividualQuantity` is
parameterized over its object type: the mereology of a host library's own objects — the
particles of a mechanical system, the cells of a mesh — is the same mereology, and
nothing here reads a part except to hand it to the measurement. `Decomposition System`
is the nominal reading and the one the mixing counterexample (`Extensivity.lean`) uses.

Constructors

PropertyKindCalculus.Decomposition.atom.{u} {O : Type u} :
  O → PropertyKindCalculus.Decomposition O

An atomic, indivisible part.

PropertyKindCalculus.Decomposition.union.{u} {O : Type u} :
  PropertyKindCalculus.Decomposition O →
    PropertyKindCalculus.Decomposition O →
      PropertyKindCalculus.Decomposition O

The union of two parts.

Proof for Definition 8.3.1

uses 0

A two-constructor inductive Decomposition O — atom and union — with fold as its one eliminator, realized in the Mathlib-free core as the Mereology module, which imports nothing at all: the carving is pure structure, and the laws that consume it (the Extensivity module) import it rather than housing it. The abstinence is load-bearing: coalesce_count_ne and count_sortal_ne (the extensivity chapter) prove that a part count is not a function of the whole, which is exactly what a carving-as-census would wrongly supply.

Definition8.3.2

groupuses 1used by 0✓L∃∀N

Part and whole as roles. A portion of a thing is a quantity of the same kind as the thing — which is what leaves an interface taking a portion and its total open to a silent argument swap. Part k R and Whole k R put the two mereological roles into the type; Part.WithinWhole — the portion does not exceed its total — is the only relation between them, stated with the part on the left, where the mereology puts it, so the reversed reading is unwritable rather than merely wrong. Dybkær's improper case (§3.4 Note 3, system and component "designated identically") is the pair wrapping one quantity.

Lean code for Definition8.3.2●1 definition

structure(1 field)defined in PropertyKindCalculus/PartWhole.lean

complete

structure PropertyKindCalculus.Part (k : PropertyKindCalculus.KindOfProperty)
  (R : Type) : Type

structure PropertyKindCalculus.Part
  (k :
    PropertyKindCalculus.KindOfProperty)
  (R : Type) : Type

**A portion, as a role** — a quantity read as part of a larger total of its own kind:
the finite pixels within a reduction block, one tap's raw weight within a kernel's sum.
Distinct in *type* from the total it is taken from, which is what stops a call site from
handing over the two the wrong way round; the same *kind*, because a portion of a thing is
a quantity of the same kind as the thing.

Fields

q : PropertyKindCalculus.Quantity k R

The portion quantity.

Proof for Definition 8.3.2

uses 0

One-field role wrappers over Quantity k R, with castCarrier on each so a pair born as counts crosses to a float carrier in its roles. The eliminator Part.fractionOf writes the portion-over-total division once, in the only order the roles admit, and its result is deliberately a different kind, licensed by a quotient kind-law — dividing a portion by its total is what mints the "fraction of total" role. The roles claim no partition: exhaustiveness and disjointness are further commitments, and the kernels this serves do not make them.

Where the foundation does work downstream: the extensivity chapter states Dybkær's §13.5 aggregation modes as laws quantified over all carvings; the object-type chapter adds the whole a carving cannot supply (Composite, one sort at a time) and keys the license to aggregate by that sort (Assembles); the dedicated-kinds chapter consumes the sort as Dybkær's Ch. 20 asks; and the count — the SI's "count of a specified elementary entity" — is keyed by a sortal, because the refutations above leave it nowhere else to live.