17.4. The mereology clause, and the footprint audit🔗

Definition17.4.1

groupuses 0used by 0✓L∃∀N

The aggregation class of a produced port — the declared mereology of a boundary. Dybkær's §13.5 vocabulary, extended by the classes the mereology layer proves laws over: extensive, quasiExtensive (naming its per-join tolerance, a declaration whose type is a Quantity at the governed port's kind — without the name, "approximately" is not a claim), conditionallyExtensive (naming its condition), intensive, wholeProper, countKeyed (naming the sortal the count is of — a count is extensive over a fixed carving yet not a property of the whole, so it travels with its carving rather than surviving a re-carving), extensiveAbout (naming the transport law that prices a parameter change), and interfaceLicensed (naming the cancellation law that purchases additivity over interior interfaces). A contract carries one entry per classed port; the checks are hygiene — a class governs a produced port, and each name the class carries exists, a tolerance as a kinded quantity. The truth of a class is the author's curated claim, exactly as an Assembles entry is.

Lean code for Definition17.4.1●1 definition

inductive(8 constructors)defined in PropertyKindCalculus/Provenance.lean

complete

inductive PropertyKindCalculus.Provenance.AggregationClass : Type

inductive PropertyKindCalculus.Provenance.AggregationClass :
  Type

**The aggregation class of a produced port** — how the value behaves when the
module's computation is distributed over a carving of a batch axis and the pieces are
recombined. The vocabulary is Dybkær §13.5's, extended by the classes the mereology
layer has since earned, and each constructor points at the law that cashes it rather
than restating it:

  * `extensive` — §13.5.1: the total over the parts is the value of the whole
    (`Extensive`, `extensive_additive`), so the port's total survives any re-carving
    of the batch axis (`Recarving.leafSum_invariant`; the boundary-level form is
    `Recarving.distribution_license`);
  * `quasiExtensive tolerance` — §13.5.2: additive to within a *named* per-join
    tolerance, a declaration whose type is a `Quantity` at this port's kind — without
    the name, "approximately" is not a claim (`Uncertainty.QuasiExtensive`; what a
    whole carving costs is `joins · t`, and what a re-carving costs is both carvings'
    joins);
  * `conditionallyExtensive condition` — §13.5.3: additive only under a named
    condition the deployment must establish (volume off the mixing case;
    `mixing_subadditive` is what claiming §13.5.1 anyway reports);
  * `intensive` — §13.5.4: invariant with extent, of constant composition
    (`Intensive`, `intensive_uniform`) — a port a shard may *read off any part* and
    must never sum;
  * `wholeProper` — the parts do not determine the value at all (`WholeProper`):
    no distribution over a carving is licensed, and `assemble_ne_measured` is the
    number a library that shards it anyway reports;
  * `countKeyed sortal` — a count of a specified elementary entity, named by its
    sortal predicate (`countMeasurement`). Extensive over a *fixed* carving and not a
    property of the whole (`coalesce_count_ne`), so it travels with its carving — per
    pixel, per shard — and does not survive a re-carving;
  * `extensiveAbout transport` — additive only about a shared parameter (an axis, a
    frame, a datum: `ExtensiveAbout`), with the named transport law pricing what
    reading parts about different parameters costs (`Transports`,
    `extensiveAbout_mixed`);
  * `interfaceLicensed law` — additivity purchased by a named cancellation law over
    pair-indexed interior actions (`InterfaceLedger.netMeasurement_extensive`); a
    shard boundary is a cut, and `mutualTotal` is exactly what crossing it costs when
    the law is dropped (`netTotal_union`).

Constructors

PropertyKindCalculus.Provenance.AggregationClass.extensive :
  PropertyKindCalculus.Provenance.AggregationClass

§13.5.1: unconditionally additive over the parts.

PropertyKindCalculus.Provenance.AggregationClass.quasiExtensive
  (tolerance : Lean.Name) :
  PropertyKindCalculus.Provenance.AggregationClass

§13.5.2: additive to within the named per-join tolerance — a declaration whose
type is a `Quantity` at the governed port's kind.

PropertyKindCalculus.Provenance.AggregationClass.conditionallyExtensive
  (condition : Lean.Name) :
  PropertyKindCalculus.Provenance.AggregationClass

§13.5.3: additive only under the named condition.

PropertyKindCalculus.Provenance.AggregationClass.intensive :
  PropertyKindCalculus.Provenance.AggregationClass

§13.5.4: invariant with extent, of constant composition.

PropertyKindCalculus.Provenance.AggregationClass.wholeProper :
  PropertyKindCalculus.Provenance.AggregationClass

The parts do not determine the value: no aggregation is licensed.

PropertyKindCalculus.Provenance.AggregationClass.countKeyed
  (sortal : Lean.Name) :
  PropertyKindCalculus.Provenance.AggregationClass

A count keyed to the named sortal predicate — extensive over a fixed carving,
not a property of the whole.

PropertyKindCalculus.Provenance.AggregationClass.extensiveAbout
  (transport : Lean.Name) :
  PropertyKindCalculus.Provenance.AggregationClass

Additive about a shared parameter, with the named transport law pricing a
parameter change.

PropertyKindCalculus.Provenance.AggregationClass.interfaceLicensed
  (law : Lean.Name) :
  PropertyKindCalculus.Provenance.AggregationClass

Additivity purchased by the named cancellation law over interior interfaces.

Proof for Definition 17.4.1

uses 0

An eight-constructor enumeration whose payloads are the names the classes must answer for, plus the aggregations association list on the contract; the elaborator checks are pinned by acceptance and refusal probes, and the class renders in every #kind_contract report.

Theorem17.4.2

groupuses 1used by 1✓L∃∀N

EffortsmallTagscapstoneproved

The distribution license. A module whose batched outputs are all extensive commutes with a re-carving of its batch axis: one map, every output's total preserved, however the axis is cut into tiles, blocks, or shards. The quantified boundary-level form of re-carving invariance, stated over the list of output measurements because a boundary is a list. What it deliberately does not cover: a count-keyed output — the re-carving that merges parts preserves every extensive total while changing the count, which is why a count travels per pixel or per shard; and the quasi-extensive case, where each total stands within its carving's joins · t of the preserved whole, so a re-carving costs at most both carvings' joins times the per-join tolerance.

Lean code for Theorem17.4.2●1 theorem

theoremdefined in PropertyKindCalculus/Recarving.lean

complete

theorem PropertyKindCalculus.Recarving.distribution_license.{u} {O : Type u}
  (outs :
    List
      (PropertyKindCalculus.KindOfProperty ×
        PropertyKindCalculus.Measurement O))
  (map :
    PropertyKindCalculus.Decomposition O →
      PropertyKindCalculus.Decomposition O)
  (hext : ∀ o ∈ outs, PropertyKindCalculus.Extensive o.1 o.2)
  (hpres :
    ∀ o ∈ outs,
      ∀ (d : PropertyKindCalculus.Decomposition O),
        (o.2 (map d)).numeral = (o.2 d).numeral)
  (d : PropertyKindCalculus.Decomposition O)
  (o :
    PropertyKindCalculus.KindOfProperty ×
      PropertyKindCalculus.Measurement O) :
  o ∈ outs →
    PropertyKindCalculus.leafSum o.2 (map d) =
      PropertyKindCalculus.leafSum o.2 d

theorem PropertyKindCalculus.Recarving.distribution_license.{u}
  {O : Type u}
  (outs :
    List
      (PropertyKindCalculus.KindOfProperty ×
        PropertyKindCalculus.Measurement
          O))
  (map :
    PropertyKindCalculus.Decomposition O →
      PropertyKindCalculus.Decomposition
        O)
  (hext :
    ∀ o ∈ outs,
      PropertyKindCalculus.Extensive o.1
        o.2)
  (hpres :
    ∀ o ∈ outs,
      ∀
        (d :
          PropertyKindCalculus.Decomposition
            O),
        (o.2 (map d)).numeral =
          (o.2 d).numeral)
  (d :
    PropertyKindCalculus.Decomposition O)
  (o :
    PropertyKindCalculus.KindOfProperty ×
      PropertyKindCalculus.Measurement
        O) :
  o ∈ outs →
    PropertyKindCalculus.leafSum o.2
        (map d) =
      PropertyKindCalculus.leafSum o.2 d

**The distribution license — the boundary-level form.** A module whose batched
outputs are all extensive commutes with a re-carving of its batch axis: one map,
every output's total preserved, however the axis is cut into tiles, blocks, or
shards. Stated over the *list* of output measurements because a boundary is a list —
the quantifier over it is the module-level claim, and each output alone is
`leafSum_invariant`. This is what a declared `AggregationClass.extensive` clause
buys; a count-keyed output is exactly the one it does not cover — `coalesce_count_ne`
exhibits a map that preserves every extensive total while changing the count, which
is why a count travels *with its carving* (per pixel, per shard) rather than with the
whole. The §13.5.2 relaxation, where each total stands within `joins · t` of its
whole, is priced in `Uncertainty.QuasiExtensive`.

Proof for Theorem 17.4.2

uses 1

Each output alone is the re-carving invariance capstone; the license applies it under the quantifier. The quasi-extensive price is proved in the uncertainty layer beside the joins · t accumulation law.

What the vocabulary does already support module-by-module is the audit of how much checking the kind algebra gives a boundary for free. #kind_scc reads the kind vocabulary's inter-derivability clusters; #kind_footprint reads one declared boundary against them and reports the component partition of its port and interior kinds (a single-cluster collapse is flagged), the same-kind port groups (swappable however separated the components), and the review-strength sites (crossings, attests, exits) — closing with a pinnable verdict line answering one question per module: where does this module's guarantee actually come from?