IsPersistent
plain-language theorem explainer
IsPersistent declares a recognition event persistent precisely when its J-cost is zero. Researchers deriving observer emergence from coherent recognition cite this to anchor the invariant reference frame required for multi-event comparison. The declaration is a direct abbreviation of the zero-cost condition on the event state.
Claim. A recognition event $ref$ (a positive real state) is persistent if its J-cost vanishes: $J(state(ref)) = 0$.
background
RecognitionEvent is the structure consisting of a positive real number state together with a proof of positivity. Its cost is defined as the J-cost of that state via the upstream cost function induced by the multiplicative recognizer. The module doc states that coherent comparison of multiple events requires a persistent reference frame whose cost is invariant across events, and that any non-zero cost would shift with context change. The identity event is the upstream canonical state at 1, which achieves the global J-cost minimum.
proof idea
This is a definition, not a theorem. It directly equates IsPersistent ref to the proposition ref.cost = 0, where cost is the J-cost abbreviation.
why it matters
This definition supplies the predicate used to equip the Observer structure with a fixed reference and appears in the observer_forcing_certificate that bundles the six structural facts. It fills step 4 of the module's seven-step argument that coherent recognition forces an observer. The zero-cost condition connects directly to J-uniqueness (T5) in the forcing chain, ensuring the invariant frame before the eight-tick octave and D=3 emerge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.