AgentState

formal source

  29noncomputable section
  30
  31/-- An agent's state: sigma measures imbalance. -/
  32structure AgentState where
  33  sigma : ℝ
  34  lattice_size : ℕ
  35  lattice_pos : 0 < lattice_size
  36
  37/-- A single-lattice transform: acts on one agent's lattice.
  38    These correspond to the 13 sigma-preserving virtues. -/
  39structure SingleLatticeTransform where
  40  apply : AgentState → AgentState
  41  preserves_sigma : ∀ s, (apply s).sigma = s.sigma
  42
  43/-- A cross-lattice transform: acts on TWO agents simultaneously.
  44    Love is the only virtue of this type. -/
  45structure CrossLatticeTransform where
  46  apply : AgentState → AgentState → AgentState × AgentState
  47  conserves_total : ∀ s₁ s₂,
  48    let (s₁', s₂') := apply s₁ s₂
  49    s₁'.sigma + s₂'.sigma = s₁.sigma + s₂.sigma
  50
  51/-- Single-lattice transforms preserve individual sigma. -/
  52theorem automorphism_preserves_sigma (t : SingleLatticeTransform) (s : AgentState) :
  53    (t.apply s).sigma = s.sigma := t.preserves_sigma s
  54
  55/-- Cross-lattice transforms conserve TOTAL sigma but can change individual sigma. -/
  56theorem coupling_conserves_total (t : CrossLatticeTransform) (s₁ s₂ : AgentState) :
  57    let (s₁', s₂') := t.apply s₁ s₂
  58    s₁'.sigma + s₂'.sigma = s₁.sigma + s₂.sigma := t.conserves_total s₁ s₂
  59
  60/-- The Love operator: equilibrates sigma between two agents.
  61    Each agent's sigma moves toward the mean. -/
  62def loveOperator (alpha : ℝ) (ha : 0 < alpha) (ha1 : alpha ≤ 1) :