SingleLatticeTransform

formal source

  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) :
  63    CrossLatticeTransform where
  64  apply := fun s₁ s₂ =>
  65    let mean := (s₁.sigma + s₂.sigma) / 2
  66    let s₁' := { s₁ with sigma := s₁.sigma + alpha * (mean - s₁.sigma) }
  67    let s₂' := { s₂ with sigma := s₂.sigma + alpha * (mean - s₂.sigma) }
  68    (s₁', s₂')
  69  conserves_total := by