7.5. Status ledger🔗

Done — what each capstone rests on, and the capstones themselves.

• The provenance hypergraph with its well-formedness judgment, the pedigree closure and its reachability reading, the boundary judgments agrees and discharges, and the per-boundary kernel theorems the worked model pins for each of its declared boundaries.

• The recording carrier, the compaction pass, the code generator, and the denotation bridge with whole-kernel parity theorems for the branchless dielectric chain, its reflectivity, and the fit's forward, residual and Jacobian kernels.

• The dimension functor, the curated homomorphism, and the coverage command with its pinned refutation of an incoherent edge.

• The three capstones and their supporting lemmas, each linked above: the seal of a module in the graph library, with its executable form, its boundary reading and the induction principle of the conjunctive closure it and the third capstone share; the kind-transporting weak bisimulation in cslib's labelled transition systems, factored as the strong bisimulation with the contracted tape graph composed with the contraction; the cone lemma and the seal of the computation on the tape evaluator; dimensional homogeneity over any rule algebra, instantiated on PhysLib's dimensions. Each with its instance, its mutant and its pinned axiom profile.

Open — each item with whose move it is.

• Capstone 2, the matcher: acceptance is decided on a match a probe authors. A matcher that finds the match from the leaves of a recorded tape — ports by name, constants by recording site, each occurrence by a realization table per family and carrier — is the instrument to run on the dielectric pair, where the hypergraph, the tape and the parity theorem all exist, reading what disagrees before the seal of the computation is claimed of the worked model; the expected disagreement classes are the four named in the bisimulation's definition (cap_def_bisimulation). Library and worked model.

• Capstone 2, the recorder decision: scope markers per member call, or membership widened to the closure the tape sees through — the choice that fixes the matcher's cost, and what makes an assembly's procedure edges matchable beside the occurrences they summarize. Owner.

• Capstone 2, the iterated retrieval's parity theorem, today a bit-exact runtime gate. Worked model.

• Capstone 3, the declared dimensions from the environment: the coverage command resolves each kind to its DimensionedKind by elaboration; the assignment the capstone consumes is authored per probe today, and the walk that reads it off the registry for a harvested hypergraph is the bridge from the command's report to the theorem's hypothesis. Library.