`PreState`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.PreLogicalCost
domain: Foundation
line: 10 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.PreLogicalCost on GitHub at line 10.

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

   7open Real
   8
   9/-- Pre-logical configuration value constrained to the unit interval. -/
  10structure PreState where
  11  val : ℝ
  12  in_unit_interval : 0 ≤ val ∧ val ≤ 1
  13
  14/-- Pre-logical cost landscape on `[0,1]`: minima occur at the boundary states. -/
  15noncomputable def preCost (s : PreState) : ℝ := s.val * (1 - s.val)
  16
  17/-- Stable configurations are exactly cost minima. -/
  18def IsStable (s : PreState) : Prop := preCost s = 0
  19
  20/-- Stability is equivalent to the two boundary values `0` and `1`. -/
  21theorem stable_iff_boundary (s : PreState) :
  22    IsStable s ↔ s.val = 0 ∨ s.val = 1 := by
  23  unfold IsStable preCost
  24  constructor
  25  · intro h
  26    have hfact : s.val * (1 - s.val) = 0 := h
  27    rcases mul_eq_zero.mp hfact with h0 | h1
  28    · exact Or.inl h0
  29    · right
  30      linarith
  31  · intro h
  32    rcases h with h0 | h1
  33    · simp [h0]
  34    · simp [h1]
  35
  36/-- Stable states as arithmetic 0/1 encodings. -/
  37structure StableState where
  38  bit : ℝ
  39  is_bit : bit = 0 ∨ bit = 1
  40

papers checked against this theorem

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