persistent_state_unique
plain-language theorem explainer
Persistent reference events must occupy state value 1. Researchers building observer structures from coherent recognition cite this to fix the reference frame. The argument reduces directly to the equivalence that J-cost is zero only at the identity.
Claim. Let $r$ be a recognition event. If the J-cost of $r$ equals zero, then the state of $r$ equals 1.
background
The ObserverForcing module derives an observer from any nontrivial coherent recognition structure. A recognition event is a positive real state equipped with its J-cost. IsPersistent holds precisely when that J-cost vanishes, because only a zero-cost frame remains invariant when the comparison context changes across multiple events.
proof idea
One-line wrapper that applies the Jcost zero equivalence lemma to the persistence hypothesis.
why it matters
This supplies the fourth structural fact inside the observer_forcing_certificate. It closes the step from any persistent reference to the identity tick, which is then used to prove the reference unit state equals 1 and to reach the master theorem that nontrivial recognition forces an observer. The result instantiates J-uniqueness (T5) from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.