reference_zero_cost
plain-language theorem explainer
An observer's reference recognition event has J-cost exactly zero. Researchers constructing the forcing chain from coherent recognition to observers cite this to fix the invariant reference frame. The proof is a one-line term that applies the persistence field of the observer structure.
Claim. Let $obs$ be an observer. Then the J-cost of the reference event in $obs$'s coherent recognition structure equals zero.
background
The module proves that non-trivial coherent recognition forces an observer. A RecognitionEvent carries cost defined as the J-cost of its state. An Observer is a CoherentRecognition equipped with a proof that its reference is persistent (IsPersistent). Upstream cost is the derivedCost induced by a multiplicative recognizer on positive ratios, and J-cost is non-negative by the Recognition Composition Law. The module states that a reference frame can be persistent only if its J-cost is zero.
proof idea
The proof is the term obs.persistent. This one-line wrapper directly invokes the IsPersistent field of the observer structure, which encodes the zero-cost requirement for invariance across events.
why it matters
This fills step 4 of the module argument: a persistent reference frame must have J-cost zero, supplying the identity-tick reference (x=1) required for the master theorem nontrivial_recognition_forces_observer. It anchors the observer definition in the T5 J-uniqueness and T6 phi fixed-point landmarks of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.