pith. machine review for the scientific record. sign in
theorem proved term proof high

reference_unit_state

show as:
view Lean formalization →

Any observer carries a reference recognition event fixed at state 1. Researchers deriving observers from coherent recognition structures cite this to anchor the reference frame at the identity tick. The proof is a direct one-line application of the uniqueness result for zero-cost persistent states.

claimLet obs be an observer, that is a coherent recognition structure equipped with a persistent reference event. Then the state of the reference event equals 1.

background

The module establishes that non-trivial coherent recognition forces an observer substructure through seven steps. An observer is a coherent recognition structure together with an IsPersistent witness on its reference event. The upstream theorem persistent_state_unique asserts that any persistent reference satisfies state exactly equal to 1, via the equivalence between zero J-cost and the identity tick.

proof idea

The proof is a one-line wrapper that applies persistent_state_unique to the reference event of the observer's recognition structure and the supplied persistence witness.

why it matters in Recognition Science

This result supplies step 5 of the module's argument: the unique zero J-cost state is the identity tick. It supports the master theorem that every non-trivial recognition stream yields an observer by attaching the canonical reference. In the Recognition Science framework it fixes the persistent frame required for coherent comparison of multiple events under the Recognition Composition Law.

scope and limits

formal statement (Lean)

 153theorem reference_unit_state (obs : Observer) :
 154    obs.recognition.reference.state = 1 :=

proof body

Term-mode proof.

 155  persistent_state_unique obs.recognition.reference obs.persistent
 156
 157/-- An observer always carries at least two distinguishable events. -/

depends on (4)

Lean names referenced from this declaration's body.