7.6. What the capstones do not claim🔗

• The host that receives an emitted kernel. An emitter hands a host the program and nothing else — the denotation of the rendering says the program runs as the tape and has the tape's graph, so the seal is a theorem about the program (semantic_seal_program); that the printed text means in the host language what the program means in Lean's Float — which is core's IEEE binary64 model for every op but exp/log (examples.tape_host_float_model), so a conformance claim about the host — the host's compiler, its exp/log, and every line of the host's own model are its trusted base, named in the methodology chapter and measured — not proved — by julia_parity and the landing stubs.

• The truth of an attestation. It is a hypothesis of the model; the seal says only that the build's list of them is complete. Where the attestation defers a requirement, the requirement clause counts it, with its reason, as one the apparatus still owes.

• The harvest's kind readings. The bisimulation transports them and does not re-derive them.

• Anything below the tape — the code generator, the toolchain, the foreign interface — which the deployment template lists as what remains trusted.

• Accuracy against nature, which needs a true value the kernel never has; that boundary is the uncertainty chapter's, and the requirement clause is where a demand of that kind is stated as an empirical requirement against a named referent, gated or attested, rather than left unsaid.