persists
plain-language theorem explainer
If a trace predicate holds on a finite recognition trace, it still holds on every extension of that trace. Cited by anyone assembling the first PRC logic layer or needing persistence of ledger propositions along growing distinction histories. The proof is a one-line unpacking of the stability field built into the predicate structure.
Claim. Let $P$ be a predicate on finite traces that is required to be stable under extension, and let $T,U$ be finite traces. If $U$ extends $T$ (i.e., $U$ is $T$ followed by some suffix) and $P$ holds at $T$, then $P$ holds at $U$.
background
In Primitive Recognition Calculus, a finite trace is an inductive history: empty, or one distinction act appended to a shorter trace. Extension means the longer trace is the shorter one concatenated with a suffix.
A trace predicate is not an arbitrary Prop on traces. By definition it pairs a holding relation with a stability law: whenever the history grows by extension, truth is preserved. The module treats this as the proposition surface of the first PRC logic pass.
Upstream, extension is the K2.5 relation on the K2.4 inductive traces. The local setting is pure finite-history logic, before continuum or operator-level structure is imposed.
proof idea
One-line term proof. Apply the stability component of the given trace predicate to the extension hypothesis and the holding hypothesis. No auxiliary lemmas are invoked; the claim is exactly that packaged stability axiom.
why it matters
Supplies the persistence step used by the headline trace-logic certificate, which packages truth introduction, conjunction introduction, and the proposition surface for the first PRC logic pass. Downstream call sites include Regge/Bloch transport identities, flat-path goodness at zero amplitude, double-slit which-path scaffolding, Page-curve ledger-transfer scaffolding, and RecogSpec band-acceptance witnesses. In framework terms it is the elementary reason ledger propositions remain valid as distinction history lengthens, the discrete-history counterpart of forcing-chain finiteness before continuum limits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.