improves_comp_left

formal source

  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)