PreservationInvestment.lean

import Std

/- Two-team preservation investment, Lean 4.24.0 / Std only.
   A separate simultaneous game, not a stochastic organizational equilibrium.
   Every pure action/profile/deviation is represented. Primary payoff identities
   connect the closed form to original departure/apprenticeship events.
   Physical capacity, independent coins, public transferable scope and real
   cost primitives are assumptions, not inferred from organizational labels. -/
namespace PreservationInvestment

inductive Action where
  | none | library | apprentice | both
  deriving DecidableEq, Repr

def actions : List Action := [.none,.library,.apprentice,.both]
def profiles : List (Action × Action) :=
  actions.flatMap (fun a => actions.map (fun b => (a,b)))

theorem every_action_listed (a : Action) : a ∈ actions := by
  cases a <;> simp [actions]

theorem every_profile_listed (a b : Action) : (a,b) ∈ profiles := by
  cases a <;> cases b <;> simp [profiles,actions]

theorem profile_count : profiles.length = 16 := by decide +kernel

def writes : Action → Bool
  | .library | .both => true
  | _ => false

def teaches : Action → Bool
  | .apprentice | .both => true
  | _ => false

structure Economy where
  departure : Rat
  learning : Rat
  expert : Rat
  recordValue : Rat
  apprenticeValue : Rat
  bothValue : Rat
  recordCost : Rat
  apprenticeCost : Rat
  fee : Rat
  deriving DecidableEq, Repr

structure Valid (e : Economy) : Prop where
  departure0 : 0 ≤ e.departure
  departure1 : e.departure ≤ 1
  learning0 : 0 ≤ e.learning
  learning1 : e.learning ≤ 1
  record0 : 0 ≤ e.recordValue
  apprentice0 : 0 ≤ e.apprenticeValue
  recordBound : e.recordValue ≤ e.bothValue
  apprenticeBound : e.apprenticeValue ≤ e.bothValue
  expertBound : e.bothValue ≤ e.expert
  recordCost0 : 0 ≤ e.recordCost
  apprenticeCost0 : 0 ≤ e.apprenticeCost
  fee0 : 0 ≤ e.fee

/-- Two independent apprentices can improve reliability; they are not treated
    as a useless duplicate of a single training attempt. -/
def success (q : Rat) (a b : Action) : Rat :=
  if teaches a && teaches b then q+q*(1-q)
  else if teaches a || teaches b then q else 0

def gross (e : Economy) (a b : Action) : Rat :=
  let z := success e.learning a b
  e.departure * (if writes a || writes b then
    (1-z)*e.recordValue+z*e.bothValue else z*e.apprenticeValue)

def cost (e : Economy) (a : Action) : Rat :=
  (if writes a then e.recordCost else 0) +
  (if teaches a then e.apprenticeCost else 0)

def utility (e : Economy) (own rival : Action) : Rat :=
  gross e own rival-cost e own

def welfare (e : Economy) (a b : Action) : Rat :=
  utility e a b+utility e b a

structure Outcome where
  departure : Bool
  first : Bool
  second : Bool
  deriving DecidableEq, Repr

def outcomes : List Outcome :=
  [⟨false,false,false⟩,⟨false,false,true⟩,
   ⟨false,true,false⟩,⟨false,true,true⟩,
   ⟨true,false,false⟩,⟨true,false,true⟩,
   ⟨true,true,false⟩,⟨true,true,true⟩]

def sumOver {α : Type} : List α → (α → Rat) → Rat
  | [], _ => 0
  | x::xs, f => f x+sumOver xs f

def coin (p : Rat) (b : Bool) : Rat := if b then p else 1-p

def weight (e : Economy) (o : Outcome) : Rat :=
  coin e.departure o.departure * coin e.learning o.first * coin e.learning o.second

def realized (e : Economy) (a b : Action) (o : Outcome) : Rat :=
  if o.departure then
    if writes a || writes b then
      if (teaches a && o.first) || (teaches b && o.second) then
        e.bothValue else e.recordValue
    else if (teaches a && o.first) || (teaches b && o.second) then
      e.apprenticeValue else 0
  else 0

def eventGross (e : Economy) (a b : Action) : Rat :=
  sumOver outcomes (fun o => weight e o * realized e a b o)

theorem event_mass (e : Economy) :
    sumOver outcomes (weight e) = 1 := by
  simp [outcomes,sumOver,weight,coin]
  grind

theorem coin_nonnegative (p : Rat) (h0 : 0 ≤ p) (h1 : p ≤ 1) (b : Bool) :
    0 ≤ coin p b := by
  cases b <;> simp [coin] <;> grind

theorem event_nonnegative (e : Economy) (hv : Valid e) (o : Outcome) :
    0 ≤ weight e o := by
  exact Rat.mul_nonneg
    (Rat.mul_nonneg
      (coin_nonnegative e.departure hv.departure0 hv.departure1 o.departure)
      (coin_nonnegative e.learning hv.learning0 hv.learning1 o.first))
    (coin_nonnegative e.learning hv.learning0 hv.learning1 o.second)

/-- The game payoff is the expectation of the original eight realized events,
    not a payoff table declared solely to obtain the desired equilibrium. -/
theorem original_events_equal_closed_form (e : Economy) (a b : Action) :
    eventGross e a b = gross e a b := by
  cases a <;> cases b <;>
    simp [eventGross,outcomes,sumOver,weight,coin,realized,writes,teaches,gross,success] <;>
    grind

theorem gross_symmetric (e : Economy) (a b : Action) :
    gross e a b = gross e b a := by
  cases a <;> cases b <;> simp [gross,success,writes,teaches]

theorem success_bounds (q : Rat) (h0 : 0 ≤ q) (h1 : q ≤ 1) (a b : Action) :
    0 ≤ success q a b ∧ success q a b ≤ 1 := by
  have hc : 0 ≤ 1-q := by grind
  have hp := Rat.mul_nonneg h0 hc
  have hs := Rat.mul_nonneg hc hc
  have htwo : 0 ≤ q+q*(1-q) ∧ q+q*(1-q) ≤ 1 := by constructor <;> grind
  cases a <;> cases b <;> simp [success,teaches] <;> grind

theorem two_attempts_not_perfect :
    success (1/2) .apprentice .apprentice = 3/4 := by decide +kernel

theorem one_attempt_not_perfect :
    success (1/2) .library .apprentice = 1/2 := by decide +kernel

theorem backup_bounded_by_lost_expert (e : Economy) (hv : Valid e) (a b : Action) :
    gross e a b ≤ e.departure*e.expert := by
  have hz := success_bounds e.learning hv.learning0 hv.learning1 a b
  have hn : 0 ≤ 1-success e.learning a b := by grind
  have hr : e.recordValue ≤ e.expert := by have h:=hv.recordBound; have h':=hv.expertBound; grind
  have ha : e.apprenticeValue ≤ e.expert := by have h:=hv.apprenticeBound; have h':=hv.expertBound; grind
  have he : 0 ≤ e.expert := by have h:=hv.apprentice0; grind
  have hrec := Rat.mul_le_mul_of_nonneg_left hr hn
  have hboth := Rat.mul_le_mul_of_nonneg_left hv.expertBound hz.1
  have happ := Rat.mul_le_mul_of_nonneg_left ha hz.1
  have hscale := Rat.mul_le_mul_of_nonneg_right hz.2 he
  have hlibrary : (1-success e.learning a b)*e.recordValue+
      success e.learning a b*e.bothValue ≤ e.expert := by grind
  have happrentice : success e.learning a b*e.apprenticeValue ≤ e.expert := by grind
  unfold gross
  split
  · exact Rat.mul_le_mul_of_nonneg_left hlibrary hv.departure0
  · exact Rat.mul_le_mul_of_nonneg_left happrentice hv.departure0

abbrev BestReply (e : Economy) (own rival : Action) : Prop :=
  actions.all (fun alternative => decide (utility e alternative rival ≤ utility e own rival)) = true

abbrev Equilibrium (e : Economy) (first second : Action) : Prop :=
  BestReply e first second ∧ BestReply e second first

theorem best_reply_iff_all_deviations (e : Economy) (own rival : Action) :
    BestReply e own rival ↔ ∀ alternative, utility e alternative rival ≤ utility e own rival := by
  constructor
  · intro h a
    exact of_decide_eq_true ((List.all_eq_true.mp h) a (every_action_listed a))
  · intro h
    exact List.all_eq_true.mpr (fun a _ => decide_eq_true (h a))

/-- Substantive game implication: strict dominance checked against every rival
    action gives the unique pure equilibrium, not merely a no-rival incentive. -/
theorem dominance_gives_unique_equilibrium (e : Economy)
    (hd : ∀ rival other, other ≠ Action.none →
      utility e other rival < utility e .none rival) (a b : Action) :
    Equilibrium e a b ↔ a=.none ∧ b=.none := by
  constructor
  · intro he
    have ha := (best_reply_iff_all_deviations e a b).mp he.1 .none
    have hb := (best_reply_iff_all_deviations e b a).mp he.2 .none
    have ea : a=.none := by
      by_cases h : a=.none
      · exact h
      · have hh:=hd b a h
        exact False.elim (by grind)
    have eb : b=.none := by
      by_cases h : b=.none
      · exact h
      · have hh:=hd a b h
        exact False.elim (by grind)
    exact ⟨ea,eb⟩
  · rintro ⟨rfl,rfl⟩
    have hb : BestReply e .none .none := by
      apply (best_reply_iff_all_deviations e .none .none).mpr
      intro other
      by_cases h : other=.none
      · subst other; exact Rat.le_refl
      · exact Rat.le_of_lt (hd .none other h)
    exact ⟨hb,hb⟩

def base : Economy :=
  ⟨1/2,1/2,8,2,3,6,3/2,3/2,0⟩

theorem base_valid : Valid base := by
  constructor <;> decide +kernel

theorem base_none_strictly_dominates (rival other : Action) (h : other ≠ Action.none) :
    utility base other rival < utility base .none rival := by
  cases other
  · exact False.elim (h rfl)
  · cases rival <;> decide +kernel
  · cases rival <;> decide +kernel
  · cases rival <;> decide +kernel

theorem base_unique_equilibrium (a b : Action) :
    Equilibrium base a b ↔ a=.none ∧ b=.none :=
  dominance_gives_unique_equilibrium base base_none_strictly_dominates a b

theorem base_equilibrium_welfare : welfare base .none .none = 0 := by decide +kernel

theorem base_every_profile_bounded (a b : Action) :
    welfare base a b ≤ 1 := by cases a <;> cases b <;> decide +kernel

abbrev OneEach (a b : Action) : Prop :=
  (a=.none ∧ b=.both) ∨ (a=.both ∧ b=.none) ∨
  (a=.library ∧ b=.apprentice) ∨ (a=.apprentice ∧ b=.library)

theorem base_all_planner_maximizers (a b : Action) :
    welfare base a b = 1 ↔ OneEach a b := by
  cases a <;> cases b <;> decide +kernel

theorem base_planner_attains_bound : welfare base .library .apprentice = 1 := by decide +kernel
theorem base_duplicate_both_loses : welfare base .both .both = -1 := by decide +kernel
theorem base_full_baseline : 2*(1-base.departure)*base.expert = 8 := by decide +kernel
theorem base_backup_is_partial : base.bothValue < base.expert := by decide +kernel

theorem one_each_welfare (e : Economy) :
    welfare e .library .apprentice =
      2*e.departure*((1-e.learning)*e.recordValue+e.learning*e.bothValue)-
      e.recordCost-e.apprenticeCost := by
  simp [welfare,utility,gross,success,cost,writes,teaches]
  grind

theorem one_each_gain_threshold (e : Economy) :
    0 < welfare e .library .apprentice ↔
      e.recordCost+e.apprenticeCost <
      2*e.departure*((1-e.learning)*e.recordValue+e.learning*e.bothValue) := by
  rw [one_each_welfare]
  grind

def sponsored (e : Economy) (a b : Action) : Rat := welfare e a b-e.fee
def coalitionTotal (e : Economy) : Rat := welfare e .library .apprentice-e.fee
def coalitionMember (e : Economy) : Rat := coalitionTotal e / 2

theorem same_programme_coalition_parity (e : Economy) :
    coalitionTotal e = sponsored e .library .apprentice := rfl

theorem coalition_equal_split_conserves (e : Economy) :
    coalitionMember e+coalitionMember e=coalitionTotal e := by
  unfold coalitionMember
  grind

theorem base_coalition_member : coalitionMember base = 1/2 := by decide +kernel

theorem base_fee_frontier (fee : Rat) :
    sponsored {base with fee:=fee} .library .apprentice=1-fee := by
  change welfare base .library .apprentice-fee=1-fee
  rw [base_planner_attains_bound]

theorem base_fee_reversal (fee : Rat) :
    sponsored {base with fee:=fee} .library .apprentice < 0 ↔ 1 < fee := by
  rw [base_fee_frontier]
  grind

theorem base_coalition_participation (fee : Rat) :
    0 < coalitionMember {base with fee:=fee} ↔ fee < 1 := by
  have hv := base_fee_frontier fee
  unfold sponsored at hv
  unfold coalitionMember coalitionTotal
  rw [hv]
  rw [Rat.lt_div_iff (by decide +kernel : (0:Rat) < 2)]
  grind

def overhead : Economy := {base with fee:=5/4}
def noLearning : Economy := {base with learning:=0}
def noDeparture : Economy := {base with departure:=0}
def weakBoundary : Economy := {base with recordCost:=1}

theorem overhead_optimum_negative (a b : Action) :
    sponsored overhead a b ≤ -1/4 := by
  cases a <;> cases b <;> decide +kernel
theorem overhead_attainment : sponsored overhead .library .apprentice = -1/4 := by decide +kernel
theorem overhead_exact_tie : sponsored {base with fee:=1} .library .apprentice = 0 := by decide +kernel

theorem no_learning_equilibria (a b : Action) :
    Equilibrium noLearning a b ↔ a=.none ∧ b=.none := by
  cases a <;> cases b <;> decide +kernel
theorem no_learning_planner_bound (a b : Action) :
    welfare noLearning a b ≤ 1/2 := by
  cases a <;> cases b <;> decide +kernel
theorem no_learning_planner_maximizers (a b : Action) :
    welfare noLearning a b = 1/2 ↔
      (a=.none ∧ b=.library) ∨ (a=.library ∧ b=.none) := by
  cases a <;> cases b <;> decide +kernel

theorem no_departure_equilibria (a b : Action) :
    Equilibrium noDeparture a b ↔ a=.none ∧ b=.none := by
  cases a <;> cases b <;> decide +kernel
theorem no_departure_planner_bound (a b : Action) :
    welfare noDeparture a b ≤ 0 := by
  cases a <;> cases b <;> decide +kernel
theorem no_departure_planner_maximizers (a b : Action) :
    welfare noDeparture a b = 0 ↔ a=.none ∧ b=.none := by
  cases a <;> cases b <;> decide +kernel

theorem weak_boundary_exact_equilibria (a b : Action) :
    Equilibrium weakBoundary a b ↔
      (a=.none ∧ b=.none) ∨ (a=.none ∧ b=.library) ∨
      (a=.library ∧ b=.none) := by
  cases a <;> cases b <;> decide +kernel
theorem weak_boundary_planner_bound (a b : Action) :
    welfare weakBoundary a b ≤ 3/2 := by
  cases a <;> cases b <;> decide +kernel
theorem weak_boundary_planner_maximizers (a b : Action) :
    welfare weakBoundary a b = 3/2 ↔ OneEach a b := by
  cases a <;> cases b <;> decide +kernel
theorem weak_boundary_none_library_tie :
    utility weakBoundary .none .none = utility weakBoundary .library .none := by decide +kernel

end PreservationInvestment