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

persistent_event_state_eq_identity

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 105theorem persistent_event_state_eq_identity
 106    (ref : RecognitionEvent) (h : IsPersistent ref) :
 107    ref.state = RecognitionEvent.identity.state := by

proof body

Term-mode proof.

 108  rw [persistent_state_unique ref h]
 109  rfl
 110
 111/-! ## §4. Cooper Pairing as the Constructive Source of Persistence -/
 112
 113/-- For any positive `x`, the pair state `x · x⁻¹` collapses to the
 114    identity tick. This is the structural origin of persistence: even
 115    when no event sits at `x = 1` directly, any pair of inverse states
 116    constructs a persistent reference. -/

depends on (19)

Lean names referenced from this declaration's body.