IndisputableMonolith.Ethics.CostModel

   1import Mathlib
   2-- import IndisputableMonolith.Measurement
   3import IndisputableMonolith.Gap45.Beat
   4
   5namespace IndisputableMonolith
   6namespace Ethics
   7
   8noncomputable section
   9open Classical
  10
  11universe w
  12
  13/-- A minimal cost model over actions of type `A`. Costs are nonnegative reals. -/
  14structure CostModel (A : Type u) where
  15  cost : A → ℝ
  16  nonneg : ∀ a, 0 ≤ cost a
  17
  18variable {A : Type u}
  19
  20/-- Ethical preference: `a ≼ b` iff `cost a ≤ cost b` (lower cost is better). -/
  21def Prefer (M : CostModel A) (a b : A) : Prop := M.cost a ≤ M.cost b
  22
  23infix:50 "≼" => Prefer
  24
  25/-- Net improvement predicate: `a` strictly improves on `b`. -/
  26def Improves (M : CostModel A) (a b : A) : Prop := M.cost a < M.cost b
  27
  28/-- Reflexivity: every action is at least as good as itself. -/
  29lemma prefer_refl (M : CostModel A) (a : A) : Prefer M a a := by
  30  dsimp [Prefer]
  31  exact le_rfl
  32
  33/-- Transitivity: if `a ≼ b` and `b ≼ c`, then `a ≼ c`. -/
  34lemma prefer_trans (M : CostModel A) {a b c : A}
  35  (hab : Prefer M a b) (hbc : Prefer M b c) : Prefer M a c := by
  36  dsimp [Prefer] at hab hbc ⊢; exact le_trans hab hbc
  37
  38/-- Preorder instance for preference. -/
  39instance (M : CostModel A) : Preorder A where
  40  le := fun a b => Prefer M a b
  41  le_refl := fun a => prefer_refl M a
  42  le_trans := fun a b c hab hbc => prefer_trans M hab hbc
  43
  44/-- Composable actions under a cost model: binary composition with subadditivity and monotonicity. -/
  45structure Composable (M : CostModel A) where
  46  comp : A → A → A
  47  subadd : ∀ a b, M.cost (comp a b) ≤ M.cost a + M.cost b
  48  mono : ∀ a a' b b', Prefer M a a' → Prefer M b b' → Prefer M (comp a b) (comp a' b')
  49  strict_mono_left : ∀ a a' x, Improves M a a' → Improves M (comp a x) (comp a' x)
  50
  51/-- Monotonicity of composition w.r.t. preference. -/
  52theorem prefer_comp_mono (M : CostModel A) (C : Composable M)
  53  {a₁ a₂ b₁ b₂ : A}
  54  (ha : Prefer M a₁ a₂) (hb : Prefer M b₁ b₂) :
  55  Prefer M (C.comp a₁ b₁) (C.comp a₂ b₂) := by
  56  dsimp [Prefer] at ha hb ⊢
  57  exact C.mono a₁ a₂ b₁ b₂ ha hb
  58
  59/-- Composition preserves improvement. -/
  60theorem improves_comp_left (M : CostModel A) (C : Composable M)
  61  {a b x : A} (h : Improves M a b) : Improves M (C.comp a x) (C.comp b x) := by
  62  exact C.strict_mono_left a b x h
  63
  64/-- CQ alignment at threshold θ ∈ [0,1]: score ≥ θ. -/
  65/- Placeholder removed: use concrete CQ and score from Measurement. -/
  66abbrev CQ := IndisputableMonolith.Measurement.CQ
  67@[simp] abbrev score (c : CQ) : ℝ := IndisputableMonolith.Measurement.score c
  68def CQAligned (θ : ℝ) (c : CQ) : Prop :=
  69  0 ≤ θ ∧ θ ≤ 1 ∧ score c ≥ θ
  70
  71/-- Ethical admissibility under 45‑gap: either no experience required, or the plan includes experience. -/
  72/- Placeholder removed: use Gap45 gating rule (experience required iff 8 ∤ period). -/
  73abbrev requiresExperience : CQ → Nat → Prop := IndisputableMonolith.Gap45.requiresExperience
  74def Admissible (period : Nat) (c : CQ) (hasExperience : Prop) : Prop :=
  75  ¬ requiresExperience c period ∨ hasExperience
  76
  77/-- Prefer alignment: higher CQ never hurts in the costless tie (axiom placeholder to be specialized).
  78    Prefer higher CQ does not break ties: if costs are equal and `c₁` is at least as aligned as `c₂`,
  79    then `a` is preferred to `b`. -/
  80theorem prefer_by_cq (M : CostModel A) (a b : A) (c₁ c₂ : CQ) (θ : ℝ)
  81  (_ : 0 ≤ θ ∧ θ ≤ 1) (_ : CQAligned θ c₂ → CQAligned θ c₁)
  82  (hcost : M.cost a = M.cost b) : Prefer M a b := by
  83  dsimp [Prefer]
  84  simp [hcost]
  85
  86/-- Lexicographic ethical preference with admissibility first, then cost preference. -/
  87def PreferLex (M : CostModel A) (period : Nat) (cq : CQ)
  88  (hasExpA hasExpB : Prop) (a b : A) : Prop :=
  89  (Admissible period cq hasExpA ∧ ¬ Admissible period cq hasExpB)
  90  ∨ (Admissible period cq hasExpA ∧ Admissible period cq hasExpB ∧ Prefer M a b)
  91
  92end
  93
  94end Ethics
  95end IndisputableMonolith
  96