7.2. The seal of a module — the provenance hypergraph
The first capstone is stated over the metrological provenance hypergraph — the object every audit report presents one relation of. Its nodes are kinded values; its hyperedges are occurrences of the witness families, each relating its operands to its result in order, since a quotient's numerator and denominator are different ports of one edge; its sources carry the evidence tier the boundary audit assigns them; and its exits mark where a value leaves the calculus for the bare carrier. It is data — prelude-only, parametric in the node and kind types — so it can be authored by hand in a probe or produced by the harvest: the elaboration-time walk that reads a declared boundary's member definitions and builds their hypergraph from them, ports from the members' signatures, occurrences from the kinded operations in their bodies, sources from the tiers the boundary audit assigns and from the reason each attestation states at its call site. The harvest's output for one boundary is its assembly: the hypergraph together with the signature positions found to carry no kind and the level each node belongs to. The capstone's hypotheses are the two judgments already decided per boundary: structural well-formedness of the hypergraph, and agreement between the declared boundary and the one its members compute. The order matters for what the seal rests on: the audit's tiers and the attestations' reasons are inputs to the harvest, the harvest builds the hypergraph, and the theorem is stated over that hypergraph with the two judgments as its hypotheses — the audits establish the hypotheses, the harvest builds the object, and the theorem gives the seal.
Structural well-formedness of the provenance hypergraph: every node declared exactly once;
every occurrence typed at its family's operand count, with operands and result carrying
their nodes' declared kinds; every occurrence result a derivation target — a derived
introduction or a produced port, never a source; and every derived node, produced port and
exit reached from the sources through the conjunctive closure of the occurrences. The last
clause is the boundary audit's "raw mints = 0" made compositional: a derived node no
occurrence chain produces is an anonymous mint, and an occurrence cycle feeding itself
licenses nothing, because the closure starts from the sources. #kind_assembly_decide
reflects the judgment into a kernel theorem per boundary.
Lean code for Definition7.2.1●1 definition
Associated Lean declarations
-
defdefined in PropertyKindCalculus/Provenance.leancomplete
def PropertyKindCalculus.Provenance.wellFormed {ν κ : Type} [BEq ν] [BEq κ] (g : PropertyKindCalculus.Provenance ν κ) : Bool
def PropertyKindCalculus.Provenance.wellFormed {ν κ : Type} [BEq ν] [BEq κ] (g : PropertyKindCalculus.Provenance ν κ) : Bool
Structural well-formedness of the provenance hypergraph: unique declarations, typed occurrences, results on derivation targets only, and sources reaching every derived node, output, and exit. Decided by evaluation in a probe and by kernel reduction in a proof; the truth of each edge remains the authored claim the trust model reviews by enumeration.
Four structural recursions over lists, conjoined; decided by evaluation in a probe and by
kernel reduction in a theorem. The sources are the non-produced ports together with the
gated and attested introductions (sources), and the closure is a fuel-bounded fixpoint
that saturates in one sweep per occurrence (reachableFrom).
The pedigree of a node set: everything it is derived from, the set itself included — the backward closure through the occurrences, computed as the forward influence closure of the reversed incidence, one reversed unit occurrence per operand position. The sources among an output's pedigree are its influencers: the term list of an uncertainty budget over the hypergraph's edges, and the source set whose attached conditions a downstream flag may claim for that output. Split by what each source is, the same set is the output's assumption ledger: the ports left open at the boundary, the gated ingests, the attested mints with their harvested reasons.
Lean code for Definition7.2.2●1 definition
Associated Lean declarations
-
defdefined in PropertyKindCalculus/Influence.leancomplete
def PropertyKindCalculus.Provenance.ancestorsOf {ν κ : Type} [BEq ν] (g : PropertyKindCalculus.Provenance ν κ) (of : List ν) : List ν
def PropertyKindCalculus.Provenance.ancestorsOf {ν κ : Type} [BEq ν] (g : PropertyKindCalculus.Provenance ν κ) (of : List ν) : List ν
The pedigree of a node set: everything it is derived from, including the set itself — the ancestor set the backward closure reaches through the occurrences, computed as the forward closure of the reversed incidence.
One engine for both directions: the disjunctive sweep that adds a result when some operand is known, run over the occurrence list reversed edge by edge. Fuel is one sweep per reversed occurrence plus one, the sweep that observes saturation.
Membership in the executable pedigree is reachability in the
value-flow digraph — the binary shadow of the
provenance hypergraph, one vertex per node and one edge per operand-to-result pair of an
occurrence: a is among the ancestors of b exactly when a path of such edges leads from
a to b. This is the lemma that lets the capstone below be argued over paths while its
hypotheses are decided over lists.
Lean code for Theorem7.2.3●1 theorem
Associated Lean declarations
-
theoremdefined in PropertyKindCalculus/Graph/Flow.leancomplete
theorem PropertyKindCalculus.Provenance.mem_ancestorsOf_iff {ν κ : Type} [BEq ν] [LawfulBEq ν] {g : PropertyKindCalculus.Provenance ν κ} {of : List ν} {a : ν} : a ∈ g.ancestorsOf of ↔ ∃ b ∈ of, g.flowDigraph.Reachable a b
theorem PropertyKindCalculus.Provenance.mem_ancestorsOf_iff {ν κ : Type} [BEq ν] [LawfulBEq ν] {g : PropertyKindCalculus.Provenance ν κ} {of : List ν} {a : ν} : a ∈ g.ancestorsOf of ↔ ∃ b ∈ of, g.flowDigraph.Reachable a b
The saturation argument for the forward closure — a sweep only appends, appended nodes are pairwise-distinct occurrence results, so with one sweep per occurrence plus one the closure has either observed a fixpoint or would have outgrown its own bound — applied to the reversed incidence, whose step relation is the converse of the flow digraph's adjacency.
The seal of a module. Let g be a provenance
hypergraph and c a declared boundary, with g well-formed
and c agreeing with g — the two judgments #kind_assembly_decide and
#kind_contract_decide pin (the declared boundary). Then for every
produced port or exit y of c, every node a in the pedigree
of y is either a source of g — a non-produced port of c, a gated ingest, or an
attested mint carrying its reason — or the result of some occurrence all of whose operands
are themselves in the pedigree of y. Equivalently: the pedigree of an output has no leaf
outside the sources, and the assumption ledger the build prints for y is the complete
list of what y rests on. In the paradigm's words, once the module's gates are declared,
no other raw datum reaches its outputs.
Lean code for Theorem7.2.4●1 theorem
Associated Lean declarations
-
theoremdefined in PropertyKindCalculus/Graph/Seal.leancomplete
theorem PropertyKindCalculus.Provenance.pedigree_seal {ν κ : Type} [BEq ν] [LawfulBEq ν] [BEq κ] {g : PropertyKindCalculus.Provenance ν κ} (hwf : g.WellFormed) {y : ν} (hy : y ∈ g.outputs) {a : ν} (ha : a ∈ g.ancestorsOf [y]) : a ∈ g.sources ∨ ∃ o ∈ g.occurrences, o.result = a ∧ ∀ oc ∈ o.operands, oc.1 ∈ g.ancestorsOf [y]
theorem PropertyKindCalculus.Provenance.pedigree_seal {ν κ : Type} [BEq ν] [LawfulBEq ν] [BEq κ] {g : PropertyKindCalculus.Provenance ν κ} (hwf : g.WellFormed) {y : ν} (hy : y ∈ g.outputs) {a : ν} (ha : a ∈ g.ancestorsOf [y]) : a ∈ g.sources ∨ ∃ o ∈ g.occurrences, o.result = a ∧ ∀ oc ∈ o.operands, oc.1 ∈ g.ancestorsOf [y]
**The seal of a module.** In a well-formed provenance hypergraph, every node in the pedigree of an output — a produced port or an exit — is a source, or the result of some occurrence all of whose operands are themselves in that pedigree. Once the module's gates are declared, no other raw datum reaches its outputs.
By the reachability reading, a node a in the
pedigree of y lies on a path to y, so a is an operand of some occurrence, and
occurrencesTyped makes it a declared node — a port or an introduction. If a is a
non-produced port or a gated or attested introduction, it is a source. Otherwise a is a
derived introduction or a produced port, and sourcesReach places it in the conjunctive
closure known, so some occurrence produces a with every operand in known; each such
operand is an ancestor of a, hence of y by transitivity of reachability. The hypothesis
on c enters only to identify the non-produced ports of g with the boundary's declared
inputs, configuration and parameters, so that the conclusion speaks of the declared
interface rather than of whatever the harvest happened to port. The case a = y and the
step from a known node to a source or an occurrence result are the induction principle of
the conjunctive closure (reachableFrom_sound, in the core), which the dimension capstone
reuses. The executable form — a decidable undeclaredLeaves g y, empty exactly under the
conclusion — is sealed_of_wellFormed, what an instance pins with decide; the boundary
reading, seal_of_agrees, adds the hypothesis on c. All three stand beside the
reachability reading, in the graph library.
Non-vacuity of the seal. Three witnesses, each a pinned probe. (i) Two instances: an
authored hypergraph — the influence probe, labelled by numbers so the kernel decides it —
whose well-formedness and seal decide closes, with the theorem applied to it; and a
harvested one, the interval composition's declared boundary, whose well-formedness and
agreement the kernel already decides, for which #kind_seal_decide adds the seal theorem by
kernel reduction of the executable conclusion at every output. (ii) A mutant: the same
hypergraph with one anonymous mint added — a derived introduction no occurrence produces,
wired into an output — fails wellFormed and has a non-empty undeclaredLeaves at that
output, exactly the mint, so the hypothesis is the discriminating one and the conclusion is
not closed by the shape of the statement. (iii) The axiom profile of
the seal, pinned to the three classical axioms.
Lean code for Theorem7.2.5●1 theorem
Associated Lean declarations
-
theoremdefined in PropertyKindCalculus/Tests/Graph/Seal.leancomplete
theorem PropertyKindCalculus.Tests.GraphSeal.seal_witnesses : PropertyKindCalculus.Tests.GraphSeal.GN.WellFormed ∧ PropertyKindCalculus.Tests.GraphSeal.GN.Sealed ∧ ¬PropertyKindCalculus.Tests.GraphSeal.GNmut.WellFormed ∧ ¬PropertyKindCalculus.Tests.GraphSeal.GNmut.Sealed
theorem PropertyKindCalculus.Tests.GraphSeal.seal_witnesses : PropertyKindCalculus.Tests.GraphSeal.GN.WellFormed ∧ PropertyKindCalculus.Tests.GraphSeal.GN.Sealed ∧ ¬PropertyKindCalculus.Tests.GraphSeal.GNmut.WellFormed ∧ ¬PropertyKindCalculus.Tests.GraphSeal.GNmut.Sealed
**Non-vacuity of the seal**: the instance satisfies the hypothesis and the conclusion; the mutant fails both. The axiom profile of the seal itself is pinned below.
(i) and (ii) are decide theorems over the authored hypergraph and its mutant, conjoined
as the linked declaration, and a kernel-decided seal over the harvested one; (iii) is
#print axioms under #guard_msgs. The mutant is the check the methodology asks of every
gate — a tactic that closes a goal is not evidence that the hypothesis fired — carried into
the capstone itself.
What the first capstone does not claim: it is a theorem about the provenance hypergraph the harvest produced. That the hypergraph is the code — that the harvest attributed every mint, erasure and occurrence to the right node and missed none — is what the boundary audit, the mint ratchet and the unkinded sweep assert about the source, and each of those is an instrument, not a hypothesis of the theorem. The seal of the computation is what turns that residual trust into a cross-check.