`PreState`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.PreLogicalCost on GitHub at line 10.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

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.