inductive PropertyKindCalculus.Decomposition (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.

• atom {O : Type u} : O → Decomposition O

  An atomic, indivisible part.

• union {O : Type u} : Decomposition O → Decomposition O → Decomposition O

  The union of two parts.

def PropertyKindCalculus.instReprDecomposition.repr {O✝ : Type u_1} [Repr O✝] : Decomposition O✝ → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance PropertyKindCalculus.instReprDecomposition {O✝ : Type u_1} [Repr O✝] : Repr (Decomposition O✝)

Equations

• PropertyKindCalculus.instReprDecomposition = { reprPrec := PropertyKindCalculus.instReprDecomposition.repr }

def PropertyKindCalculus.Decomposition.fold {O : Type u} {R : Type} (leaf : O → R) (op : R → R → R) : Decomposition O → R

The fold over a decomposition: a value per leaf, combined at every union. The one recursion this module has over the mereology, so leafSum (Extensivity.lean) and the quantity-level assemble (Composite.lean) are the same traversal at two carriers rather than two traversals that happen to agree.

Equations

• PropertyKindCalculus.Decomposition.fold leaf op (PropertyKindCalculus.Decomposition.atom s) = leaf s
• PropertyKindCalculus.Decomposition.fold leaf op (a.union b) = op (PropertyKindCalculus.Decomposition.fold leaf op a) (PropertyKindCalculus.Decomposition.fold leaf op b)

def PropertyKindCalculus.Decomposition.ofParts {O : Type u} (p : O) (ps : List O) : Decomposition O

A decomposition from a nonempty list of parts — the head and the rest, so nonemptiness is in the signature rather than a side condition. The shape a host library hands over (a List, a Multiset's elements, a Fintype's enumeration) reaching the mereology without an empty case to invent a value for.

Equations

• One or more equations did not get rendered due to their size.

def PropertyKindCalculus.Decomposition.joins {O : Type u} : Decomposition O → Nat

The number of joins of a carving — its union nodes. The one number this module reads off the shape of a decomposition rather than off a measured value, and it is read for two reasons: it bounds how far a per-join tolerance can accumulate (§13.5.2, Uncertainty.QuasiExtensive), and it is precisely what a re-carving is free to change while the whole stays put (Recarving.lean).

Equations

• (PropertyKindCalculus.Decomposition.atom a).joins = 0
• (a.union a_1).joins = a.joins + a_1.joins + 1

def PropertyKindCalculus.Decomposition.Forall {O : Type u} (p : O → Prop) : Decomposition O → Prop

A property of every atomic part of a carving. The leaf-wise quantifier the intensive law needs: Extensive reaches its leaves through arithmetic (leafSum), and intensivity has no arithmetic to reach them with.

Equations

• PropertyKindCalculus.Decomposition.Forall p (PropertyKindCalculus.Decomposition.atom s) = p s
• PropertyKindCalculus.Decomposition.Forall p (a.union b) = (PropertyKindCalculus.Decomposition.Forall p a ∧ PropertyKindCalculus.Decomposition.Forall p b)

def PropertyKindCalculus.Decomposition.count {O : Type u} (p : O → Bool) : Decomposition O → Int

A count over a carving: how many atomic parts fall under a sortal predicate. The predicate is the argument that makes this a count of something — "a count of a specified elementary entity", in the SI's phrasing of amount of substance.

Equations

• PropertyKindCalculus.Decomposition.count p = PropertyKindCalculus.Decomposition.fold (fun (s : O) => if p s = true then 1 else 0) fun (x1 x2 : Int) => x1 + x2

theorem PropertyKindCalculus.count_true_eq_joins_succ {O : Type u} (d : Decomposition O) : Decomposition.count (fun (x : O) => true) d = ↑d.joins + 1

The count and the join count are the same number. A carving with n joins exhibits n + 1 parts, so "how many entities" is a fact about the tree and about nothing else.