IsPersistent
plain-language theorem explainer
A recognition event counts as persistent precisely when its J-cost is zero. Researchers constructing observer structures from coherent recognition cite this predicate to enforce an invariant reference frame. The definition is a direct abbreviation of the zero-cost condition on the event state.
Claim. A recognition event $ref$ is persistent when its J-cost satisfies $cost(ref)=0$.
background
RecognitionEvent is the structure of a positive real state under recognition, with cost defined as Cost.Jcost of that state. The module sets out seven steps from coherent recognition to an observer, where step 3 requires a persistent reference frame whose cost is invariant across events and step 4 forces that cost to be zero. The supplied justification states that any positive cost would shift under context change, while zero is the unique global minimum.
proof idea
One-line definition that directly equates IsPersistent ref to the proposition ref.cost = 0, using the in-module cost abbreviation of Jcost.
why it matters
This predicate is the field type inside the Observer structure and appears in the bundled facts of observer_forcing_certificate. It closes step 4 of the module argument, linking the zero-cost minimum to the identity tick and to T5 J-uniqueness in the forcing chain. Downstream theorems such as identity_persistent and cooper_pairing_yields_persistent apply it directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.