`identity`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.ObserverForcing
domain: Foundation
line: 58 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.ObserverForcing on GitHub at line 58.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  55  Cost.Jcost_nonneg e.state_pos
  56
  57/-- The canonical identity event sits at the J-cost minimum (`x = 1`). -/
  58def identity : RecognitionEvent where
  59  state := 1
  60  state_pos := by norm_num
  61
  62/-- The identity event has zero cost. -/
  63theorem identity_cost : identity.cost = 0 := by
  64  show Cost.Jcost 1 = 0
  65  exact Cost.Jcost_unit0
  66
  67end RecognitionEvent
  68
  69/-! ## §2. Coherent Recognition Structures -/
  70
  71/-- A coherent recognition structure: a sequence of recognition events
  72    with at least two distinguishable states, plus a reference event
  73    used for comparison. -/
  74structure CoherentRecognition where
  75  events : ℕ → RecognitionEvent
  76  reference : RecognitionEvent
  77  nontrivial : ∃ n m : ℕ, (events n).state ≠ (events m).state
  78
  79/-! ## §3. The Persistent Reference -/
  80
  81/-- A reference is *persistent* if its J-cost is zero.
  82
  83    Justification: if the reference cost were `c > 0`, then the
  84    comparison `J(eᵢ) − c` against this reference would shift if `c`
  85    itself depended on the comparison context. The only invariant
  86    cost across arbitrary recognition events is `c = 0`, since
  87    `Jcost = 0` is the unique global minimum (`Cost.Jcost_eq_zero_iff`).
  88    A reference at any other cost is not a fixed frame; it is itself

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.