identity_cost
plain-language theorem explainer
The identity recognition event carries zero J-cost. Researchers deriving observer emergence from coherent recognition structures cite this to fix the invariant reference frame. The proof is a direct term reduction to the upstream Jcost unit lemma after identifying the identity event with argument 1.
Claim. Let $e$ be the identity recognition event. Then its J-cost satisfies $J(e)=0$, where $J(x)=(x-1)^2/(2x)$ for positive ratio $x$.
background
Recognition events are structures carrying source, target, and positive ratio (LedgerForcing.RecognitionEvent). The J-cost function is defined on these ratios by $J(x)=(x-1)^2/(2x)$ and is known to be non-negative. The Observer-Forcing module shows that any non-trivial coherent recognition structure forces an observer by requiring a persistent zero-cost reference frame. The upstream lemma Jcost_unit0 states that Jcost 1 = 0 by direct simplification of the J-cost definition.
proof idea
Term-mode proof. The body first rewrites identity.cost as Cost.Jcost 1, then applies the lemma Jcost_unit0 exactly.
why it matters
This theorem supplies the zero-cost anchor used by identity_persistent (which concludes the identity event is persistent) and by the observer_forcing_certificate master theorem. It realizes step 5 of the module argument: the unique state with J-cost zero is the identity tick, thereby closing the forcing chain from non-trivial recognition to an observer substructure. It aligns with the Recognition Composition Law by locating the fixed point of the J-functional at argument 1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.