`StableState`

definition

show as: view math explainer →

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

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

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.