prefer_comp_mono

formal source

  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