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 Julia emitter beside the CUDA/C pair, with its rendering table over the whole alphabet and the min/max reading as Lean's ite; the coverage and ABI #guards on the recorded AVS tape; the julia_parity executable that runs the emitted file against the tape evaluator.

• The denotation of the rendering, for every backend at once: the one straight-line program genSL reads off the tape, the three emitters as printers of it, genSL_denotes (the program runs as evalTapeT, node for node), its completeness (genSL_isOk_iff_evalTapeT: a program exists exactly when the interpreter runs the tape) and the literal and input clauses genSL_lit_iff/genSL_input_iff as equivalences about the emitted program.

• The seal of the computation over the emitted program: ofProg, the program's graph, equal to the tape's under genSL (ofProg_eq_ofTape), and semantic_seal_program, the second capstone restated with the program's graph and SL.run in place of the tape and evalTape.

• Slot discipline on the program: every operand slot of line i precedes it on a well-formed tape (genSL_slots_lt, ofProg_ordered); the generators decide that invariant (checkWF, gen_wf, genJulia_wf) and reject an output id outside the tape (checkOutputs, gen_outIds_lt, genJulia_outIds_lt) — the printed kernels are well-scoped, for any tape handed to them.

• The scalar-leaf obligation: the generators decide that every constant leaf stores exactly one scalar (checkScalarLeaves, gen_scalar_leaves, genJulia_scalar_leaves), so the literal baked at a const leaf (genSL_lit_iff) is the leaf's whole stored value, never the head of a buffer read as 0.0.

• The chain composed: pipeline_denotes (examples.tape_end_to_end_chain) — for every well-formed tape, const leaves included, tape, compacted tape and emitted program hold the same value at every original node; the program's existence supplies the compacted tape's evaluation, and Batteries' Float.toBits_inj (cseCompact_denotation_unconditional) the merged-const-leaf case.

• The host Float as a specification: Float is a structure over core's Float.Model (IEEE 754 binary64, round-to-nearest-even), and BinOp.eval/UnOp.eval unfold by rfl to model arithmetic for every op of the alphabet but the two opaque externs exp/log (examples.tape_host_float_model), so the per-printer obligation is the host's IEEE conformance, not a claim about Lean.

• One min/max reading on NaN across the interpreter and the three renderings: Lean's ite, written as the ≤-ternary in C and CUDA and as ifelse in Julia; the table fetch's clamp likewise follows refFetch in every rendering.

• 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.