Superseded. This is an earlier draft of the methodology chapter, retained as a record of what the work believed at the time. It is not current: the composition it describes includes constrained elevation, which the design chapter withdrew after implementation established that no axis of a basis is elevatable. The current chapter is the one published under the methodology category.
The typing section fixed what the instantiation is for: it is what stops the model and the methods being a proposal, and the question it answers is whether the discipline can be enforced at a machine handover with no person present. It did not say how the implementation is built or how anyone would know it is the right one. This section states both, and states one problem the artefact has not solved.
What makes an implementation faithful
A library can run, return verdicts, and not be this discipline. The model fixes five record fields, an origin set composed by union at derivation, and a conjunctive combination over four comparisons. An implementation that scored the axes instead of conjoining them, or that dropped an axis a demand did not mention, would execute and would be a different artefact. So faithfulness needs a test that does not reduce to reading the code and agreeing with it.
The test is that the model's decisions must be recoverable from the implementation's behaviour. For each design decision the chapter records as settled, there is an observation that distinguishes an implementation honouring it from one that does not. Conjunction is distinguished by a case failing on one axis and passing on three, which must refuse. Union at derivation is distinguished by a derived claim whose origin set is checked against its parents. Silence as permission is distinguished by a demand omitting an axis, which must not refuse on that axis. Where a decision has no such observation, the implementation cannot be shown faithful to it, and the decision is recorded as untestable rather than assumed honoured.
This is deliberately weaker than proving the implementation correct. It establishes that the artefact demonstrated is the artefact designed, which is the claim the dissertation actually needs, and not that the code is free of error.
What the library exposes
The division between what the library does and what a caller supplies is where the discipline's claim sits, so it is fixed rather than left to implementation taste. The library holds the model and the methods: it constructs and carries basis records, composes origin sets under derivation, and decides admissibility given a record and a demand. The caller supplies the claim, the basis facts from which a record is built, and the demand attaching to the act it proposes.
One consequence is load-bearing. The library must not accept a caller-supplied verdict, and must not offer a way to bypass the comparison for a claim the caller asserts is fine. A library that did would enforce nothing, and the discipline's whole claim is that the judgement is made mechanically at the boundary rather than by whoever is standing there. Any override is therefore outside the library, visible, and recorded as an override rather than a verdict.
Two things stay outside. The mechanism for checking whether a vouching has lapsed is authorisation infrastructure and is consumed rather than implemented: the record carries that a vouching has a validity, and the library asks something else whether it still holds. Transport is likewise assumed, since the problem statement puts the cryptographic carriage of attestations out of scope.
Where basis records come from, and what is unsolved
The model assumes a basis record arrives with the claim. That assumption is free for a demonstration, where the scenarios supply records, and it is not free for a tool. An engineer asked to use this library would ask first who writes a record, from what, and at what cost, and the artefact as designed has no answer.
The problem is not that record construction is unimplemented. It is that the model gives no account of how a plant's existing signals become the fields the record requires. Means and establishment time are usually available from the source that produced a value. Established scope is sometimes implicit in an instrument's placement and sometimes nowhere. Authority is often a convention rather than a recorded fact. Origin identity, the identifier of the means event a claim descends from, has no counterpart in most existing systems at all, and the structure entry already records that the record presupposes such an identity without making it a field.
So a faithful implementation can be built and demonstrated against the scenarios, and a tool of use to an engineer requires something the design does not yet contain: a method for producing records from the signals a plant actually has. That is stated here as an open problem of the artefact rather than a task of the implementation, because it is a gap in the model and not in the code. What the instantiation can do is make the gap concrete, since a library that must be handed complete records shows precisely which fields a real deployment would have to manufacture.
What is read against the implementation
Two neighbouring formalisms were deferred to this part and are read once it exists and is found wanting on a specific question: contract-based design and runtime assurance, for the shape of an enforcement barrier and its pre-condition and post-condition machinery, and proof-carrying code, for the pattern of carrying a justification alongside the artefact it justifies. Both are read under the same two rules as every other field, and both were deferred rather than read early because a field consulted about an undrafted part is invited to design it.