IndisputableMonolith.Foundation.PreLogicalCost

   1import Mathlib
   2
   3namespace IndisputableMonolith
   4namespace Foundation
   5namespace PreLogicalCost
   6
   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
  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
  68    rfl
  69
  70end PreLogicalCost
  71end Foundation
  72end IndisputableMonolith
  73