identity_persistent
plain-language theorem explainer
The identity recognition event at state 1 satisfies the persistence condition that its J-cost vanishes. Researchers building the observer-forcing argument cite this to fix the canonical reference frame. The proof is a direct one-line application of the zero-cost theorem for the unit state.
Claim. Let $e$ be the recognition event with state $1$. Then the J-cost of $e$ equals zero, hence $e$ is persistent.
background
In the ObserverForcing module a RecognitionEvent is a structure consisting of a positive real state equipped with its J-cost. The identity event is the canonical case with state exactly 1. IsPersistent holds for a reference precisely when its cost is zero; this guarantees invariance across arbitrary comparison contexts because zero is the global minimum of the J-cost function.
proof idea
The proof is a one-line wrapper that applies the identity_cost theorem, which rewrites the claim to Cost.Jcost 1 = 0 and invokes Cost.Jcost_unit0.
why it matters
This supplies clause (3) of the observer_forcing_certificate theorem that aggregates the structural facts for nontrivial_recognition_forces_observer. It realizes step 5 of the module's seven-step chain: the unique state with J-cost zero is the identity tick. In the Recognition Science framework it anchors the persistent reference required for any observer, consistent with J-uniqueness and the forcing chain from T5 to T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.