identity
plain-language theorem explainer
The identity definition constructs the canonical RecognitionEvent whose state equals one. Workers on the observer-forcing chain cite it as the zero-cost reference required for persistent frames. The construction is a direct structure instance whose positivity obligation is discharged by norm_num.
Claim. The identity recognition event is the instance of the structure with state field equal to $1$, satisfying the positivity requirement $0 < 1$.
background
RecognitionEvent is the structure whose sole data is a positive real state together with the proof that the state exceeds zero; its cost is defined to be the J-cost of that state. The module ObserverForcing shows that any coherent recognition structure forces a persistent reference frame whose J-cost must vanish, and the unique state achieving J-cost zero is the identity tick at value one. Upstream RecognitionEvent structures in LedgerForcing and InformationIsLedger encode the same positivity requirement on ratios so that J-cost remains defined.
proof idea
One-line structure instance that supplies state := 1 and closes the state_pos field with the norm_num tactic.
why it matters
This definition supplies the zero-cost identity required by CostAlgebraData (which normalizes cost at the identity to zero) and by defectDist (which vanishes at the identity). It realizes step 5 of the module argument that a persistent reference frame exists only when its J-cost is zero, thereby feeding the master theorem nontrivial_recognition_forces_observer. It aligns with the J-uniqueness landmark (T5) that fixes the minimum of J at x = 1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.