`StableState`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.PreLogicalCost on GitHub at line 37.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

used by

formal source

  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`). -/
  52def bnot (a : StableState) : StableState := by
  53  refine ⟨1 - a.bit, ?_⟩
  54  rcases a.is_bit with ha | ha <;> simp [ha]
  55
  56/-- The stable arithmetic states form a Boolean-style algebraic fragment. -/
  57theorem stable_forms_boolean_algebra :
  58    (∀ a b : StableState, (band a b).bit = a.bit * b.bit) ∧
  59    (∀ a b : StableState, (bor a b).bit = a.bit + b.bit - a.bit * b.bit) ∧
  60    (∀ a : StableState, (bnot a).bit = 1 - a.bit) := by
  61  constructor
  62  · intro a b
  63    rfl
  64  constructor
  65  · intro a b
  66    rfl
  67  · intro a

papers checked against this theorem

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