Composable

formal source

  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