AdaptiveSupport.lean

import Std

namespace AdaptiveSupport

/- Adaptive support: deterministic J1/J2 specialization, Lean4.24.0 Std only.
   The generic theorem below permits every deterministic strategy depending
   on the entire observed state/action history. The concrete game has perfect
   public readiness assessment, deterministic learning and record transfer,
   no drift, and zero local learning. Stochastic JS fixtures are NOT certified
   by these concrete theorems. Sponsor and team utilities remain separate.
   A weak completion at the unreachable rent-case ready/no-memory tie is
   explicitly chosen; no all-state uniqueness claim follows. -/

structure DecisionProblem (S A : Type) where
  actions : S → List A
  current : Nat → S → A → Rat
  next : Nat → S → A → S

abbrev HistoryStrategy (S A : Type) := List (S × A) → S → A

def recommendedValue (m : DecisionProblem S A) (sigma : Nat → S → A) :
    Nat → S → Rat
  | 0, _ => 0
  | n+1, s => m.current n s (sigma n s) +
      recommendedValue m sigma n (m.next n s (sigma n s))

/-- A strategy may use the entire recorded past, not just the current state.
    In this deterministic specialization opponent responses are fixed known
    functions, so they can be reconstructed from this observed history. -/
def historyValue (m : DecisionProblem S A) (pi : HistoryStrategy S A) :
    Nat → List (S × A) → S → Rat
  | 0, _, _ => 0
  | n+1, past, s => m.current n s (pi past s) +
      historyValue m pi n ((s,pi past s)::past) (m.next n s (pi past s))

def HistoryFeasible (m : DecisionProblem S A) (pi : HistoryStrategy S A) :
    Nat → List (S × A) → S → Prop
  | 0, _, _ => True
  | n+1, past, s => pi past s ∈ m.actions s ∧
      HistoryFeasible m pi n ((s,pi past s)::past) (m.next n s (pi past s))

def OneStep (m : DecisionProblem S A) (sigma : Nat → S → A)
    (n : Nat) (s : S) : Prop :=
  ∀ a, a ∈ m.actions s →
    m.current n s a + recommendedValue m sigma n (m.next n s a) ≤
      recommendedValue m sigma (n+1) s

/-- Verification for every complete feasible history-dependent unilateral
    deviation. Conditions hold after every feasible deviation, not only the
    recommended path. The invariant permits irrelevant states to be omitted. -/
theorem all_history_deviations_bounded
    (m : DecisionProblem S A) (sigma : Nat → S → A) (valid : S → Prop)
    (limit : Nat)
    (checks : ∀ n, n < limit → ∀ s, valid s → OneStep m sigma n s)
    (closed : ∀ n s a, valid s → a ∈ m.actions s → valid (m.next n s a))
    (n : Nat) (hn : n ≤ limit) (past : List (S × A)) (s : S) (hs : valid s)
    (pi : HistoryStrategy S A) (hp : HistoryFeasible m pi n past s) :
    historyValue m pi n past s ≤ recommendedValue m sigma n s := by
  induction n generalizing past s with
  | zero => exact Rat.le_refl
  | succ n ih =>
    obtain ⟨ha,hchild⟩ := hp
    have hn' : n < limit := by omega
    have hsmall : n ≤ limit := by omega
    have hnext := closed n s (pi past s) hs ha
    have hf := ih hsmall ((s,pi past s)::past) (m.next n s (pi past s)) hnext hchild
    have hc := checks n hn' s hs (pi past s) ha
    simp only [historyValue]
    grind

inductive State where
  | n0 | n1 | d0 | d1 | r0 | r1
  deriving DecidableEq, Repr
inductive Mode where
  | teach | advise | local
  deriving DecidableEq, Repr
inductive Action where
  | coast | effort | record | both
  deriving DecidableEq, Repr

def states : List State := [.n0,.n1,.d0,.d1,.r0,.r1]
def actions : List Action := [.coast,.effort,.record,.both]
def modes : State → List Mode
  | .d1 | .r1 => [.teach,.advise,.local]
  | _ => [.teach,.local]

def readiness : State → Nat
  | .n0 | .n1 => 0
  | .d0 | .d1 => 1
  | .r0 | .r1 => 2
def memory : State → Bool
  | .n1 | .d1 | .r1 => true
  | _ => false
def exert : Action → Bool
  | .effort | .both => true
  | _ => false
def disclose : Action → Bool
  | .record | .both => true
  | _ => false
def makeState (k : Nat) (b : Bool) : State :=
  if k=0 then (if b then .n1 else .n0)
  else if k=1 then (if b then .d1 else .d0)
  else (if b then .r1 else .r0)

/-- Independent effort and record decisions: effort moves readiness only,
    delivery moves memory only, with perfect public observation stipulated. -/
def advance (s : State) (m : Mode) (a : Action) : State :=
  let k := readiness s
  let improves := exert a && ((m == .teach && k == 0) || (m == .advise && k == 1))
  makeState (if improves then k+1 else k) (memory s || disclose a)

def effortCost (a : Action) : Rat := if exert a then 1/2 else 0
def recordCost (m : Mode) (a : Action) : Rat :=
  if disclose a then (if m == .local then 1/2 else 1/4) else 0
def gross (s : State) (m : Mode) : Rat :=
  match m with
  | .teach | .advise => 6
  | .local => if readiness s=0 then 0 else if readiness s=1 then 3 else 6
def supportCost : Mode → Rat
  | .teach => 2
  | .advise => 1
  | .local => 0
def teamBase (s : State) (m : Mode) : Rat :=
  match m with
  | .teach => 2
  | .advise => 3
  | .local => if readiness s=0 then 0 else if readiness s=1 then 1 else 5
def welfare (s : State) (m : Mode) (a : Action) : Rat :=
  gross s m - supportCost m - effortCost a - recordCost m a
def teamStage (s : State) (m : Mode) (a : Action) : Rat :=
  teamBase s m - effortCost a - recordCost m a
def sponsorStage (rent : Bool) (s : State) (m : Mode) (a : Action) : Rat :=
  welfare s m a + (if rent && m != .local then 2 else 0)

/-- Candidate sponsor strategy. Rent-case r0 is an explicitly weak completion:
    local and teach have the same sponsor payoff, and r0 is unreachable from
    n0 under every feasible base action. It is not declared uniquely solved. -/
def sponsorMode (rent : Bool) : State → Mode
  | .n0 | .n1 | .d0 => .teach
  | .d1 => .advise
  | .r0 => .local
  | .r1 => if rent then .advise else .local

/-- n is the number of periods AFTER the current decision. The response is
    specified after every feasible sponsor mode, including declined modes. -/
def teamAction (rent : Bool) (n : Nat) (s : State) (m : Mode) : Action :=
  if n=0 then .coast else
  match m,s with
  | .teach,.n0 => .both
  | .teach,.n1 => .effort
  | .teach,.d0 => .record
  | .advise,.d1 => if rent then .coast else .effort
  | .local,.d0 => .record
  | _,_ => .coast

def sponsorProblem (rent : Bool) : DecisionProblem State Mode where
  actions := modes
  current := fun n s m => sponsorStage rent s m (teamAction rent n s m)
  next := fun n s m => advance s m (teamAction rent n s m)
def sponsorSigma (rent : Bool) (_n : Nat) (s : State) : Mode := sponsorMode rent s

/-- The team observes the selected mode before acting. Its public state must
    therefore include that mode, including a deviating sponsor's alternative. -/
def teamProblem (rent : Bool) : DecisionProblem (State × Mode) Action where
  actions := fun _ => actions
  current := fun _ p a => teamStage p.1 p.2 a
  next := fun _ p a =>
    let s := advance p.1 p.2 a
    (s,sponsorMode rent s)
def teamSigma (rent : Bool) (n : Nat) (p : State × Mode) : Action :=
  teamAction rent n p.1 p.2
def validTeam (p : State × Mode) : Prop := p.2 ∈ modes p.1

def checkSponsor (rent : Bool) : Bool :=
  [0,1,2].all fun n => states.all fun s => (modes s).all fun m =>
    decide ((sponsorProblem rent).current n s m +
      recommendedValue (sponsorProblem rent) (sponsorSigma rent) n ((sponsorProblem rent).next n s m) ≤
      recommendedValue (sponsorProblem rent) (sponsorSigma rent) (n+1) s)

def checkTeam (rent : Bool) : Bool :=
  [0,1,2].all fun n => states.all fun s => (modes s).all fun m => actions.all fun a =>
    decide ((teamProblem rent).current n (s,m) a +
      recommendedValue (teamProblem rent) (teamSigma rent) n ((teamProblem rent).next n (s,m) a) ≤
      recommendedValue (teamProblem rent) (teamSigma rent) (n+1) (s,m))

theorem aligned_sponsor_checks : checkSponsor false = true := by decide +kernel
theorem retention_sponsor_checks : checkSponsor true = true := by decide +kernel
theorem aligned_team_checks : checkTeam false = true := by decide +kernel
theorem retention_team_checks : checkTeam true = true := by decide +kernel

theorem every_state_listed (s : State) : s ∈ states := by cases s <;> simp [states]
theorem sponsor_choice_feasible (rent : Bool) (s : State) : sponsorMode rent s ∈ modes s := by
  cases rent <;> cases s <;> simp [sponsorMode,modes]
theorem team_choice_feasible (rent : Bool) (n : Nat) (s : State) (m : Mode) :
    teamAction rent n s m ∈ actions := by
  have h : ∀ a : Action, a ∈ actions := by intro a; cases a <;> simp [actions]
  exact h _

theorem sponsor_local_checks (rent : Bool) (n : Nat) (hn : n < 3) (s : State) :
    OneStep (sponsorProblem rent) (sponsorSigma rent) n s := by
  have h : checkSponsor rent = true := by cases rent; exact aligned_sponsor_checks; exact retention_sponsor_checks
  have hm : n ∈ [0,1,2] := by simp; omega
  have h1 := (List.all_eq_true.mp h) n hm
  have h2 := (List.all_eq_true.mp h1) s (every_state_listed s)
  intro a ha
  exact of_decide_eq_true ((List.all_eq_true.mp h2) a ha)

theorem team_local_checks (rent : Bool) (n : Nat) (hn : n < 3)
    (p : State × Mode) (hp : validTeam p) :
    OneStep (teamProblem rent) (teamSigma rent) n p := by
  have h : checkTeam rent = true := by cases rent; exact aligned_team_checks; exact retention_team_checks
  have hm : n ∈ [0,1,2] := by simp; omega
  have h1 := (List.all_eq_true.mp h) n hm
  have h2 := (List.all_eq_true.mp h1) p.1 (every_state_listed p.1)
  have h3 := (List.all_eq_true.mp h2) p.2 hp
  intro a ha
  exact of_decide_eq_true ((List.all_eq_true.mp h3) a ha)

/-- Concrete sponsor history-deviation theorem, for both rent specifications.
    Opponent responses at every feasible alternative mode are checked above. -/
theorem concrete_sponsor_history_deviations (rent : Bool) (n : Nat) (hn : n ≤ 3)
    (past : List (State × Mode)) (s : State) (pi : HistoryStrategy State Mode)
    (hp : HistoryFeasible (sponsorProblem rent) pi n past s) :
    historyValue (sponsorProblem rent) pi n past s ≤
      recommendedValue (sponsorProblem rent) (sponsorSigma rent) n s := by
  exact all_history_deviations_bounded (sponsorProblem rent) (sponsorSigma rent)
    (fun _ => True) 3 (fun k hk x _ => sponsor_local_checks rent k hk x)
    (fun _ _ _ _ _ => trivial) n hn past s trivial pi hp

/-- Concrete team history-deviation theorem after ANY feasible current mode.
    All later sponsor modes respond to the readiness/memory resulting from the
    team's actual deviation, rather than using the equilibrium-path state. -/
theorem concrete_team_history_deviations (rent : Bool) (n : Nat) (hn : n ≤ 3)
    (past : List ((State × Mode) × Action)) (p : State × Mode) (hv : validTeam p)
    (pi : HistoryStrategy (State × Mode) Action)
    (hp : HistoryFeasible (teamProblem rent) pi n past p) :
    historyValue (teamProblem rent) pi n past p ≤
      recommendedValue (teamProblem rent) (teamSigma rent) n p := by
  apply all_history_deviations_bounded (teamProblem rent) (teamSigma rent) validTeam 3
    (fun k hk x hx => team_local_checks rent k hk x hx)
    (fun _ x a _ _ => sponsor_choice_feasible rent (advance x.1 x.2 a))
    n hn past p hv pi hp

def organizationValue (rent : Bool) : Nat → State → Rat
  | 0, _ => 0
  | n+1, s =>
    let m := sponsorMode rent s
    let a := teamAction rent n s m
    welfare s m a + organizationValue rent n (advance s m a)

theorem development_welfare : organizationValue false 3 .n0 = 55/4 := by decide +kernel
theorem development_team :
    recommendedValue (teamProblem false) (teamSigma false) 3 (.n0,.teach) = 35/4 := by decide +kernel
theorem development_sponsor :
    recommendedValue (sponsorProblem false) (sponsorSigma false) 3 .n0 = 55/4 := by decide +kernel
theorem retention_welfare : organizationValue true 3 .n0 = 53/4 := by decide +kernel
theorem retention_team :
    recommendedValue (teamProblem true) (teamSigma true) 3 (.n0,.teach) = 29/4 := by decide +kernel
theorem retention_sponsor :
    recommendedValue (sponsorProblem true) (sponsorSigma true) 3 .n0 = 77/4 := by decide +kernel
theorem retention_reduces_welfare : organizationValue true 3 .n0 < organizationValue false 3 .n0 := by decide +kernel
theorem existing_memory_welfare : organizationValue false 3 .n1 = 14 := by decide +kernel
theorem existing_memory_team :
    recommendedValue (teamProblem false) (teamSigma false) 3 (.n1,.teach) = 9 := by decide +kernel

theorem initial_development_choices :
    sponsorMode false .n0 = .teach ∧ teamAction false 2 .n0 .teach = .both ∧
    advance .n0 .teach .both = .d1 ∧ sponsorMode false .d1 = .advise ∧
    teamAction false 1 .d1 .advise = .effort ∧ advance .d1 .advise .effort = .r1 ∧
    sponsorMode false .r1 = .local := by decide +kernel
theorem retention_stops_second_learning :
    teamAction true 1 .d1 .advise = .coast ∧ advance .d1 .advise .coast = .d1 := by decide +kernel
theorem learning_without_disclosure :
    advance .n0 .teach .effort = .d0 := by decide +kernel
theorem disclosure_without_learning :
    advance .n0 .teach .record = .n1 := by decide +kernel
theorem diagnosis_repair_without_skill_change :
    advance .d0 .teach .record = .d1 ∧ readiness .d0 = readiness .d1 := by decide +kernel
theorem assistance_without_effort_does_not_teach :
    advance .n0 .teach .coast = .n0 := by decide +kernel
theorem unsupported_local_effort_cannot_manufacture_learning :
    advance .n0 .local .effort = .n0 := by decide +kernel
theorem terminal_team_chooses_no_investment (rent : Bool) (s : State) (m : Mode) :
    teamAction rent 0 s m = .coast := by simp [teamAction]

theorem ready_state_release_gap (rho : Rat) :
    welfare .r1 .local .coast - (welfare .r1 .advise .coast + rho) = 1-rho := by
  have hl : welfare .r1 .local .coast = 6 := by decide +kernel
  have ha : welfare .r1 .advise .coast = 5 := by decide +kernel
  rw [hl,ha]
  grind
theorem ready_state_sponsor_tie :
    welfare .r1 .local .coast = welfare .r1 .advise .coast + 1 ∧
    welfare .r1 .advise .coast < welfare .r1 .local .coast := by decide +kernel
theorem unreachable_retention_completion_is_weak :
    sponsorStage true .r0 .teach .coast = sponsorStage true .r0 .local .coast := by decide +kernel

/-- A release-only rule forces local after readiness2 but leaves the sponsor
    free to withhold the developmental mode at readiness1. These are the actual
    two-stage sponsor payoffs, with each action's own next readiness. -/
def obstructValue : Rat :=
  sponsorStage true .d1 .teach .coast + sponsorStage true (advance .d1 .teach .coast) .advise .coast
def developThenReleaseValue : Rat :=
  sponsorStage true .d1 .advise .effort + sponsorStage true (advance .d1 .advise .effort) .local .coast
theorem release_only_obstruction_value : obstructValue = 13 := by decide +kernel
theorem release_only_development_value : developThenReleaseValue = 25/2 := by decide +kernel
theorem release_only_promise_does_not_prevent_obstruction : developThenReleaseValue < obstructValue := by decide +kernel

/-- A complete enforced mode contract uses the aligned strategy while paying
    the rent sponsor on its two supported periods. Voluntary adoption is a
    different question: the sponsor strictly prefers discretion in J2. -/
def contractedSponsorValue : Nat → State → Rat
  | 0, _ => 0
  | n+1, s =>
    let m := sponsorMode false s
    let a := teamAction false n s m
    sponsorStage true s m a + contractedSponsorValue n (advance s m a)
theorem full_contract_sponsor_value : contractedSponsorValue 3 .n0 = 71/4 := by decide +kernel
theorem voluntary_contract_participation_loss :
    recommendedValue (sponsorProblem true) (sponsorSigma true) 3 .n0 - contractedSponsorValue 3 .n0 = 3/2 := by decide +kernel

end AdaptiveSupport