def PropertyKindCalculus.Examples.MiniObjectTypes.massK : KindOfProperty

Mass — extensive, licensed to assemble below.

Equations

• PropertyKindCalculus.Examples.MiniObjectTypes.massK = { id := "mass", scale := PropertyKindCalculus.ScaleType.ratio }

Theorems about this kind

• PropertyKindCalculus.Examples.MiniObjectTypes.instAssemblesGridSMassK

def PropertyKindCalculus.Examples.MiniObjectTypes.lengthK : KindOfProperty

Length — a second kind, so the kind gate can be exercised alongside the object gate.

Equations

• PropertyKindCalculus.Examples.MiniObjectTypes.lengthK = { id := "length", scale := PropertyKindCalculus.ScaleType.ratio }

def PropertyKindCalculus.Examples.MiniObjectTypes.gridS : SortOfSystem

The sort of whole this file assembles — §20's "sort of system", minted once. The license below is keyed by it: aggregation is a fact about what sort of whole is being composed, not about the kind alone (volume aggregates over a rigid assembly and contracts over a mixture — the probes in Tests/Core/Composite.lean pin both).

Equations

• PropertyKindCalculus.Examples.MiniObjectTypes.gridS = { id := "four-cell grid" }

instance PropertyKindCalculus.Examples.MiniObjectTypes.instAssemblesGridSMassK : Assembles gridS massK

Mass is licensed to assemble into a grid.

1. Nominal — identity is the name (System, §3.3)

The reading PKC shipped with, and the right one for a sample, an instrument, a rover: the object is a terminological identity and nothing else, so naming it and telling two apart are the same act. Both questions answered, for free.

def PropertyKindCalculus.Examples.MiniObjectTypes.soilA : Object

Two soil samples, named.

Equations

• PropertyKindCalculus.Examples.MiniObjectTypes.soilA = { id := "soil sample A" }

def PropertyKindCalculus.Examples.MiniObjectTypes.soilB : Object

The second sample.

Equations

• PropertyKindCalculus.Examples.MiniObjectTypes.soilB = { id := "soil sample B" }

2. Structural — identity is a position, and there is no name

The shape a host library hands over: a particle of a mechanical system, a cell of a mesh. Stated here at its full generality — an arbitrary type P, about which nothing whatever is assumed — because that is exactly how much the gate needs.

The two questions come apart here, and this is the finding the parameterization exposes: the gate costs nothing and the designation is absent, not merely inconvenient.

3. Indexed — the name is computed from the position

Between the two: a pixel (i, j), a spectral band, a layer. Identity is a position, as in §2, but the position determines a name, so Designated is derivable rather than absent — and the injectivity that makes it a designation is a real obligation, discharged here by decide because the index set is finite and concrete.

@[reducible, inline]

abbrev PropertyKindCalculus.Examples.MiniObjectTypes.Cell : Type

A four-cell grid, indexed.

Equations

• PropertyKindCalculus.Examples.MiniObjectTypes.Cell = Fin 4

@[instance_reducible]

instance PropertyKindCalculus.Examples.MiniObjectTypes.instDesignatedCell : Designated Cell

The cells designate themselves through their index. The injectivity field is the claim: distinct cells get distinct names, checked rather than assumed.

Equations

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

@[instance_reducible]

instance PropertyKindCalculus.Examples.MiniObjectTypes.instSortedCell : Sorted Cell

And the cells instantiate a sort — the arrow from the particular to its universal (Sorted), declared once per model. Nothing in this file consumes it yet; it is the seam the §20 dedicated kind attaches to, where a kind-of-property is dedicated to a sort of system rather than to a particular.

Equations

• PropertyKindCalculus.Examples.MiniObjectTypes.instSortedCell = { sortOf := fun (x : PropertyKindCalculus.Examples.MiniObjectTypes.Cell) => { id := "grid cell" } }

4. Composite — a derived object type, whole and parts in one

The construction Composite.lean ships, and the one an aggregation needs: the total mass characterizes an object that a bare part type does not contain, so the whole and the parts must inhabit one type or the arithmetic cannot relate them. Derived from any of the shapes above — here from the indexed cells.

def PropertyKindCalculus.Examples.MiniObjectTypes.grid : Decomposition Cell

The four cells, as the parts of one grid.

Equations

• PropertyKindCalculus.Examples.MiniObjectTypes.grid = PropertyKindCalculus.Decomposition.ofParts 0 [1, 2, 3]

def PropertyKindCalculus.Examples.MiniObjectTypes.cellMass (c : Cell) : IndividualQuantity (Composite.part c) massK Int

One kilogram per cell, each quantity characterizing its own cell.

Equations

• PropertyKindCalculus.Examples.MiniObjectTypes.cellMass c = { magnitude := 1 }

def PropertyKindCalculus.Examples.MiniObjectTypes.gridMass : IndividualQuantity Composite.whole massK Int

The total mass of the grid: assembled over the mereology, characterizing the whole.

Equations

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

5. Joint — one quantity, two objects (MR23)

A flow, a transfer, a torque delivered across a coupling characterizes an ordered pair of systems. Under the parameterization that is an object type like any other, O₁ × O₂, and the gate falls out with nothing added.

Designation is where this shape is instructive, and the lesson is a negative one.

@[reducible, inline]

abbrev PropertyKindCalculus.Examples.MiniObjectTypes.Interface : Type

The interface object: what a delivered quantity characterizes.

Equations

• PropertyKindCalculus.Examples.MiniObjectTypes.Interface = (PropertyKindCalculus.Object × PropertyKindCalculus.Object)

def PropertyKindCalculus.Examples.MiniObjectTypes.flowAB : IndividualQuantity (soilA, soilB) massK Int

A quantity of the coupling from soilA to soilB.

Equations

• PropertyKindCalculus.Examples.MiniObjectTypes.flowAB = { magnitude := 7 }

6. Singleton — one object, and the index costs nothing

The other end of the range, and the one that matters for the ergonomic objection: a model with exactly one system pays no ceremony for the object layer, because there is only one term to write and it is (). Worth stating because it is what makes the parameterization safe to adopt everywhere — the layer is not a tax on models that have nothing to disambiguate.

@[instance_reducible]

instance PropertyKindCalculus.Examples.MiniObjectTypes.instDesignatedUnit : Designated Unit

The single system a one-object model is about.

Equations

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

7. Combinations — and the two halves compose differently

The shapes above are not a closed list to choose from. They compose, because they are types and types compose, and a realistic model combines them: a quantity of this instrument (nominal), at this pixel (indexed), of that particle (structural) is a quantity of the triple.

What is worth knowing is that the gate and the designation compose under different conditions, and the difference is exactly the one the census is organized around.

@[reducible, inline]

abbrev PropertyKindCalculus.Examples.MiniObjectTypes.Site (P : Type) : Type

A three-way combination: a named instrument, an indexed cell, and a structural object supplied by a host library about which nothing is assumed.

Equations

• PropertyKindCalculus.Examples.MiniObjectTypes.Site P = (PropertyKindCalculus.Object × PropertyKindCalculus.Examples.MiniObjectTypes.Cell × P)

theorem PropertyKindCalculus.Examples.MiniObjectTypes.cellPairName_inj (a b c d : Cell) : "cell " ++ toString ↑a ++ "/" ++ toString ↑b = "cell " ++ toString ↑c ++ "/" ++ toString ↑d → a = c ∧ b = d

The naming is injective — 256 pairs of sites, checked. Over an infinite object type this is a lemma the author owes; over a finite one it is decide.

@[instance_reducible]

instance PropertyKindCalculus.Examples.MiniObjectTypes.instDesignatedProdCell : Designated (Cell × Cell)

When every factor is designated, one line does it. Designated.ofInjective is the composition principle: name the combination however the model names it, and show the naming is injective. That is the whole of what composing a designation requires.

Equations

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

So the shape of the answer is: the object index needs no taxonomy, because a type is already whatever discrimination the model has; and the designation needs one combinator per way of building an object type, each carrying its own obligation. The library ships the combinators (Composite, Designated.ofInjective, Designated.prod) and refuses to ship the naming conventions, which is why every one of them takes a proof.