A Property Kind Calculus for Measurement Metrology

7.1. The layers and their ladders🔗

Each capstone is stated over one object, and those objects are the calculus's three layers.

  • The provenance layer — its object the metrological provenance hypergraph: what the source declares. Every node has a kind, every source has a tier, every hyperedge is a use of a law. Its value is that a module's assumptions become one object, and the seal of a module says that object's list of gates is complete for every output.

  • The computation layer — its object the computational tape graph: what the code computes, at every carrier. Its value is that the seal becomes a claim about the executable rather than about a reading of the source.

  • The dimension layer — its object the dimension functor over the kinds the hypergraph carries: what the laws in use must satisfy. Its value is that it is the only layer able to refute an authored law. Witnesses and attestations are claims; dimension can say no wherever the kinds carry one.

There is no single ladder from the first layer through the second to the third. There are two ladders, and both stand on the provenance layer, because the computation layer checks that the computation realizes the hypergraph while the dimension layer checks that the laws inside the hypergraph cohere. A rung below both carries the source up to the provenance layer. Each rung's status is the status of the nodes it names, which the dependency graph and the ledger at the end of this chapter carry.

Rung

What carries it

Lost without it

Source to the provenance layer

the boundary audit; the harvest; well-formedness and agreement of the declared boundary, decided per boundary; the reachability reading; the seal of a module

Per-site verdicts never compose to outputs: an anonymous mint two hops upstream of an output is visible only to a reader of the report.

Provenance layer to computation layer

the cone lemma; the bisimulation with its soundness and its strong form after contraction; the denotation bridge and the closure tactic tape_hom; the seal of the computation

The seal is about the harvest's transcript. A constant the recorder bakes, a path compaction introduces, an opaque callee the harvest saw as one node: all go unseen, and the harvest's attributions stay trusted instead of cross-checked.

Provenance layer to dimension layer

the curated homomorphism; the coverage command's verdict per authored edge; dimensional homogeneity

Outputs rest on declared sources through possibly wrong laws: a wrong edge is a kind-level fact nobody checks.

The kind-transporting weak bisimulation is therefore the relation between the provenance layer and the computation layer. It never touches the dimension layer directly, but that layer's verdicts ride along it: every tape sub-graph that realizes an occurrence realizes a law the dimension layer has judged coherent.

The three layers and the two ladders, drawn on one module — y = a · b + e, the module the bisimulation witnesses below decide — seen at three granularities:

DIMENSIONPROVENANCECOMPUTATIONLT⁻¹L·T⁻¹L·T⁻¹L·T⁻¹add exponentssame dimensiondimproductadditiveak₁ingestbk₂ingestck₃ek₃constyk₃exitproduct ↦(ac−bd) + (ad+bc)jadditive ↦ componentwisea.rea.imb.reb.im×τ×τ×τ×τ−c.re+c.ime.reconste.imconst+y.re+y.imRdimension layer — what the laws must satisfycapstone 3 — dimensional homogeneitydim is a functor: each node to its dimension,each occurrence to its family's rule. The bandis the hypergraph's image under dim; thecapstone says the image is exact along everyoccurrence, so an output's dimension iscomputed from the sources' alone. A wrongedge, ω·τ → ω, has no image here: refuted.provenance layer — what the source declarescapstone 1 — the seal of a moduleThe metrological provenance hypergraph; kindsoriginate here. Every leaf of an output'spedigree is a declared source — a checkedingest, a constant mint, an attestation — sono undeclared raw datum reaches y. Decidedper boundary by the kernel; stated over thisgraph, not over the code.computation layer — what the code computesThe computational tape graph, with no kinds of its own.R — the kind-transporting weak bisimulationtotal: every observable vertex (a leaf, a root,an operand or result of a matched occurrence)has exactly one kinded partner;weak: the interior vertices τ of a carrierexpansion are silent — no kinded node names ac;bi: every occurrence is realized by a sub-graph(down), every tape path between observablevertices projects to a hypergraph path (up).Not a bijection: one kinded operation is severalcarrier operations, and compaction merges.capstone 2 — the seal of the computationThe seal carried onto the tape at every carrier:y depends only on the images of its influencers.declared node / observable vertexsilent interior vertex τrealization of one occurrenceRdim, a functor along every occurrence

Figure 3. The three layers and their two ladders, drawn on the module y = a · b + e at three granularities.

The middle band is the metrological provenance hypergraph, the kinded one. The top band is its image under the dimension functor, node by node and occurrence by occurrence, with the family rule each occurrence must satisfy. The bottom band is the computational tape graph the same module records at a complex carrier, where the one product occurrence expands to four multiplications, a subtraction and an addition: the four products are the interior vertices no node of the hypergraph names, the silent steps that make the bisimulation weak, and the additive occurrence expands componentwise, with no interior at all. R runs from each node to each of its observable components; the dotted boxes are the realizations of the two occurrences.