`preCost`

definition

show as: view math explainer →

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

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

used by

formal source

  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

papers checked against this theorem

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