36.1. The dictionary
Term | Meaning | Declarations | Retired phrasings | Defined in |
|---|---|---|---|---|
assembly | The harvest's output for one declared boundary: its provenance hypergraph together with the signature positions found to carry no kind and the level each node belongs to. |
| — | |
assumption ledger | An output's influencers split by what each source is — the ports left open at the boundary, the gated ingests, the attested mints with their reasons. |
| — | |
attestation | A kind claim with no machine-checkable evidence, stated where used with its reason: a hypothesis of the model, not an axiom of the calculus. |
| — | |
blueprint dependency graph — short form dependency graph |
The graph of this blueprint's own nodes and their | — | — | |
boundary audit |
The environment walk | — | — | |
carrier ladder |
The number types one carrier-parametric definition is instantiated at, ordered from proof to execution — the reals for proof, binary32 as the rounding specification, |
| — | |
checked ingest |
The entry of raw, external data into the calculus through a check — the | — | — | |
compacted tape | A tape after its identical sub-expressions are merged: the object the code generator lowers to one kernel. |
| — | |
computational tape graph — short form tape graph | The unkinded, computational counterpart of the metrological provenance hypergraph: the directed acyclic graph a tape determines, one vertex per tape node, an edge from each parent to its node, in-edges ordered as the parents are; leaves are the named inputs and the baked constants, roots the recorded outputs. A tape node is its own operation, so a vertex's ordered in-edges are the one hyperedge into it and the hypergraph reading adds nothing — unlike the provenance hypergraph, whose occurrences are objects apart from its nodes. The object the second capstone relates to the provenance hypergraph. |
| computational graph, elementwise DAG, megakernel DAG | |
constant mint |
The entry of an adjudicated constant — a cited coefficient, a threshold, a structural constant of the model — through the | — | — | |
contracted tape graph | The computational tape graph with each realized occurrence's sub-graph collapsed to one ordered hyperedge — its operands the sub-graph's frontier in operand order, its results the sub-graph's roots, its label the family; defined under the clauses acceptance decides of the sub-graphs — closed, interior-private, progressing, used, pairwise disjoint, covering every operation. On it the kind-transporting weak bisimulation becomes strong, the silent steps gone. |
| — | |
crossing |
A re-typing of a value that already carries one kind as another, with no law of the algebra to derive it: trust granted by hand, tagged | — | — | |
declared boundary — short form contract | The interface a metrology module declares: its members, its kind-typed ports with the role each plays, its exits, and its deciders; decided against what the members compute, in both directions. |
| — | |
denotation bridge | The predicate relating a recording-carrier value to the tensor it computes, preserved by every carrier operation, so that a module's parity with its own eager value is a chain of per-operation lemmas. |
| — | |
dimensional homogeneity | The third capstone: along every occurrence of a well-formed provenance hypergraph the dimension of the result is the one the family's rule computes from the operands — dimension is a homomorphism along every path. |
| — | |
emission |
Where a kinded value leaves the calculus as a bare number for a consumer outside it — a deploy driver, a serializer, the parity apparatus — tagged | — | — | |
empirical requirement | A requirement whose statement names a referent the model does not define, so no theorem about the model alone can discharge it — the falsifiable kind, discharged by a gate against the referent or deferred by an attestation. |
| falsifiable requirement, validation requirement, observational requirement, testable requirement | |
evidence tier — short form tier | How a value came to carry its kind: derived through a law of the algebra, gated by a check at ingest, or attested by its author with a reason. |
| — | |
harvest | The elaboration-time walk that reads a declared boundary's member definitions and builds their provenance hypergraph: ports from the signatures, occurrences from the kinded operations, sources from the boundary audit's tiers and the attestations' reasons. |
| — | |
influencers | The sources among an output's pedigree: the term list of an uncertainty budget over the graph's edges, and the source set whose attached conditions a downstream flag may claim for that output. |
| — | |
kind-of-property — short form kind | The common defining aspect of mutually comparable properties, carried as a type index of every quantity; a kind-of-quantity when its scale has magnitude. |
| — | |
kind-transporting weak bisimulation — short form bisimulation | The relation tying the two graphs of one module together: the metrological provenance hypergraph, harvested from the source, where every kind originates, and the computational tape graph, recorded by evaluation, which carries none. It matches sources to leaves and each occurrence to the tape sub-graph realizing its family; weak because it is silent on the interior of a carrier-level expansion, a bisimulation because it simulates in both directions — every occurrence realized on the tape, every tape path projected to a hypergraph path — and along it the hypergraph's kinds are transported onto the tape graph. A weak bisimulation in the textbook sense, over labelled transition systems: the provenance layer's hops labelled by family and operand position, the tape's edges labelled through the match, wires and interior steps silent. As data it is a match — each node with the tape vertices realizing it, each occurrence with the interior of its sub-graph — whose acceptance is decidable. |
| kind-transporting simulation | |
license clause | The part of a measurement-model relation that extends its witness beyond the carrier rung it is proved at: one entry per further rung, each a named repair theorem — exact, where rounding is the identity on the values in play, or nonneg, where nonnegative on-grid weights rule cancellation out — or an independent witness restated at that rung; a rung with neither is refused. |
| — | |
measurement model | The VIM relation among the quantities involved in a measurement, attached to a declared boundary as a checked theorem edge rather than as prose. |
| — | |
metrological provenance hypergraph — short form provenance hypergraph | The object every audit report presents one relation of, and the one where every kind originates: kinded values as nodes, occurrences of the witness families as ordered hyperedges, sources carrying their evidence tier, and exits where a value leaves the calculus; prelude-only data, authored by hand in a probe or produced by the harvest from the source. |
| provenance graph, harvested graph, assembled graph | |
metrology module | A software component — the declarations one boundary names as its members, which need not be a file or a namespace — whose interface is a declared boundary, whose behavior is a measurement model attached as a theorem edge, whose implementation is a carrier-parametric measurement function, and whose licenses and mereology are declared. | — | unit of software, software unit | |
pedigree | Everything a node set is derived from, the set included: the backward closure through the occurrences. |
| — | |
propagation relation | Which source ports of a declared boundary reach which of its produced ports through the occurrences — the reading of an interface that says how information moves through it, not only what it takes and returns. |
| — | |
provable requirement | A requirement whose statement closes over the model's own declarations and kinded quantities, so a theorem about the model discharges it: a theorem edge from the governed boundary to a specification boundary, or a theorem, with spot checks where the model runs; a negative one, by the absence of a license. |
| — | |
recording carrier | The carrier whose values are thunks appending their sub-expression to a tape; instantiating a module at it builds the module's tape. |
| — | |
referent |
A kinded quantity the model does not define — a datasheet value, a prior, a reference measurement — marked |
| — | |
requirement | What a metrology module's quantities must satisfy, stated as data beside the declared boundary it governs: the statement in the author's words, the governed boundary and port, the objects it quantifies over, and the evidence by which it is met — provable or empirical, or attested with a reason. |
| — | |
requirement scope |
The objects a requirement quantifies over: every object the boundary is evaluated for, every object of a named sort (reached through |
| — | |
seal of a module | The first capstone: once a module's gates are declared, every leaf of an output's pedigree is a declared source — no undeclared raw datum reaches the outputs. |
| — | |
seal of the computation | The second capstone: the seal of a module carried onto the computational tape graph at every carrier — an output depends only on its influencers and the listed constants, and every kind change in the computation is one an occurrence of the hypergraph states. |
| — | |
specification boundary | A declared boundary whose one member computes the bound a requirement is checked against, told from a model boundary by its role: the right side of a provable requirement's theorem edge, and itself the subject of no requirement. |
| — | |
spot check |
A named |
| — | |
tape | Automatic differentiation's word for the record of the operations a program performs, in the order it performs them: a grow-only array of nodes, each one operation with its parent ids in operand order and its forward value, every operation appending one node. A carrier-generic module writes one when instantiated at the recording carrier; the calculus reads it forward and never runs the backward pass the name comes from. A straight-line program, not a graph, with kinds erased. |
| — | |
value-flow digraph — short form flow digraph | The binary shadow of a provenance hypergraph: one vertex per node, one edge per operand-to-result pair of an occurrence; the graph reachability is stated over, so that the executable closures can be proved to compute it. |
| — |