traceClosureClaim
plain-language theorem explainer
Audit record that tags the K4.13 trace-closure boundary claim: completed traces and completed orbit ledgers extend finite primitive recognition calculus by closing under infinite traces. Citation target for anyone assembling the TraceClosureCertificate. The body is a pure StrengthClaim record (label, tag, statement string), not a proved proposition.
Claim. The K4.13 audit record asserts, under the strength tag for trace closure, that completed traces and completed orbit ledgers extend finite primitive recognition calculus by trace closure. It is a labeled strength claim (string label, strength tag, human-readable statement), not a mathematical proposition.
background
Primitive Recognition Calculus (PRC) works with finite prefixes of recognition acts. The TraceClosure module introduces completed traces and completed orbit ledgers: infinite objects that close those finite prefixes. Sibling constructions include CompletedTrace, finite prefixes with zero/successor rules, a canonical completed orbit ledger, and faithfulness of the canonical position map to natural numbers.
A StrengthClaim is a small audit record: a string label, a StrengthTag, and a one-line statement. It does not carry a proof obligation; it only classifies how strong a nearby claim is meant to be. The local tag here is trace closure.
Upstream, stable trace predicates can be conjoined, and the broader foundation links eight-tick structure to Clifford grading. Those facts set the vocabulary; this definition only registers the K4.13 boundary claim in that vocabulary.
proof idea
No proof. The declaration is a structure value of type StrengthClaim: it sets the label to the K4.13 trace-closure boundary string, the tag to the trace-closure strength tag, and the statement to the fixed English sentence about completed traces and orbit ledgers. Downstream certificates read this record; they do not discharge it as a theorem.
why it matters
Feeds TraceClosureCertificate, the first K4.13 certificate, which packages existence of completed traces, a canonical completed trace, a completed orbit ledger, and faithfulness of the canonical orbit verifier (position at $n$ recovers $n$). In the Recognition forcing picture this sits at the boundary between finite PRC bookkeeping and infinite closed traces, the same eight-tick / period-$2^3$ layer that later ties to Clifford grading. It is scaffolding for audit trails (K1/R9), not a step that forces $\phi$, $J$, or $D=3$ by itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.