persistent_state_unique
plain-language theorem explainer
Any reference event whose J-cost vanishes must occupy state value 1. Workers on the observer-forcing chain cite the result to anchor the canonical reference frame at the identity tick. The proof is a direct one-line application of the zero-cost equivalence lemma to the persistence hypothesis.
Claim. Let $e$ be a recognition event (positive real state). If the J-cost of $e$ is zero, then the state of $e$ equals $1$.
background
RecognitionEvent packages a positive real state with its positivity witness. IsPersistent is the predicate that this event's J-cost equals zero; the module documentation justifies the predicate by noting that only zero cost remains invariant under arbitrary comparison contexts. The surrounding module develops seven steps from coherent recognition to an observer, with the present result supplying the uniqueness claim that the sole zero-cost state is the identity tick at one.
proof idea
One-line term proof that applies the forward implication of Jcost_eq_zero_iff to the hypothesis that cost equals zero.
why it matters
The lemma supplies the uniqueness step required by observer_forcing_certificate and is invoked directly by reference_unit_state to fix an observer reference at state one. It implements the module claim that the unique state with vanishing J-cost is the identity tick, thereby linking the local argument to the J-uniqueness property in the Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.