IndisputableMonolith.RRF.Core.Strain

   1import Mathlib.Data.Real.Basic
   2import Mathlib.Order.Basic
   3
   4
   5/-!
   6# RRF Core: Strain
   7
   8Strain is the fundamental measure of "how far from equilibrium/balance" a state is.
   9
  10In RRF:
  11- Strain → 0 is the law (J → 0)
  12- Strain encodes deviation from recognition/balance
  13- Lower strain = more consistent = more "real"
  14
  15This module provides the abstract interface for strain functionals.
  16-/
  17
  18namespace IndisputableMonolith
  19namespace RRF.Core
  20
  21/-- A strain functional on a state space.
  22
  23A strain functional assigns a non-negative cost to each state.
  24The key property: `J(x) = 0` iff `x` is at equilibrium/balanced.
  25
  26We use `ℝ` as the codomain and add nonnegativity as a class constraint.
  27-/
  28structure StrainFunctional (State : Type*) where
  29  /-- The strain/cost of a state. -/
  30  J : State → ℝ
  31
  32namespace StrainFunctional
  33
  34variable {State : Type*}
  35
  36/-- A strain functional is non-negative if J(x) ≥ 0 for all x. -/
  37class NonNeg (S : StrainFunctional State) : Prop where
  38  nonneg : ∀ x, 0 ≤ S.J x
  39
  40/-- A state is balanced/equilibrium if its strain is exactly zero. -/
  41def isBalanced (S : StrainFunctional State) (x : State) : Prop :=
  42  S.J x = 0
  43
  44/-- The set of equilibrium states. -/
  45def equilibria (S : StrainFunctional State) : Set State :=
  46  { x | S.isBalanced x }
  47
  48/-- A strain functional has a unique minimum if there's exactly one equilibrium. -/
  49def hasUniqueMin (S : StrainFunctional State) : Prop :=
  50  ∃! x, S.isBalanced x
  51
  52/-- Strict improvement: x is strictly better than y. -/
  53def strictlyBetter (S : StrainFunctional State) (x y : State) : Prop :=
  54  S.J x < S.J y
  55
  56/-- Weak improvement: x is at least as good as y. -/
  57def weaklyBetter (S : StrainFunctional State) (x y : State) : Prop :=
  58  S.J x ≤ S.J y
  59
  60/-- A state x is a minimizer if no state is strictly better. -/
  61def isMinimizer (S : StrainFunctional State) (x : State) : Prop :=
  62  ∀ y, S.weaklyBetter x y
  63
  64/-- For non-negative strain, equilibria are minimizers. -/
  65theorem equilibria_are_minimizers [NonNeg S] (x : State) (hx : S.isBalanced x) :
  66    S.isMinimizer x := by
  67  intro y
  68  simp only [weaklyBetter, isBalanced] at *
  69  rw [hx]
  70  exact NonNeg.nonneg y
  71
  72end StrainFunctional
  73
  74/-- A ledger constraint: the sum of debits equals the sum of credits. -/
  75structure LedgerConstraint (State : Type*) where
  76  /-- Total debit for a state. -/
  77  debit : State → ℤ
  78  /-- Total credit for a state. -/
  79  credit : State → ℤ
  80
  81namespace LedgerConstraint
  82
  83variable {State : Type*}
  84
  85/-- A state satisfies the ledger constraint if debit = credit. -/
  86def isClosed (L : LedgerConstraint State) (x : State) : Prop :=
  87  L.debit x = L.credit x
  88
  89/-- The net balance (should be zero for closed ledgers). -/
  90def net (L : LedgerConstraint State) (x : State) : ℤ :=
  91  L.debit x - L.credit x
  92
  93theorem closed_iff_net_zero (L : LedgerConstraint State) (x : State) :
  94    L.isClosed x ↔ L.net x = 0 := by
  95  simp [isClosed, net, sub_eq_zero]
  96
  97end LedgerConstraint
  98
  99/-- Combined strain and ledger: the full RRF state evaluation. -/
 100structure StrainLedger (State : Type*) where
 101  strain : StrainFunctional State
 102  ledger : LedgerConstraint State
 103
 104namespace StrainLedger
 105
 106variable {State : Type*}
 107
 108/-- A state is valid if it has zero strain and closed ledger. -/
 109def isValid (SL : StrainLedger State) (x : State) : Prop :=
 110  SL.strain.isBalanced x ∧ SL.ledger.isClosed x
 111
 112/-- The set of valid states. -/
 113def validStates (SL : StrainLedger State) : Set State :=
 114  { x | SL.isValid x }
 115
 116end StrainLedger
 117
 118end RRF.Core
 119end IndisputableMonolith
 120