`stable_iff_boundary`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.PreLogicalCost
domain: Foundation
line: 21 · 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 21.

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

formal source

  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
  41/-- Arithmetic conjunction on stable states (`0/1` multiplication). -/
  42def band (a b : StableState) : StableState := by
  43  refine ⟨a.bit * b.bit, ?_⟩
  44  rcases a.is_bit with ha | ha <;> rcases b.is_bit with hb | hb <;> simp [ha, hb]
  45
  46/-- Arithmetic disjunction on stable states (`a + b - ab` on `0/1`). -/
  47def bor (a b : StableState) : StableState := by
  48  refine ⟨a.bit + b.bit - a.bit * b.bit, ?_⟩
  49  rcases a.is_bit with ha | ha <;> rcases b.is_bit with hb | hb <;> simp [ha, hb]
  50
  51/-- Arithmetic negation on stable states (`1 - a` on `0/1`). -/

papers checked against this theorem

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