RepeatedGame.lean

import Std

namespace RepeatedExperiment

/- Finite repeated-game verification, pinned Lean 4.24.0 with Std only.

   General verification theorem for a finite induced unilateral decision
   process. Each player gets such a process after fixing the other players'
   public-state strategies and integrating their hidden fresh types. O must
   contain ONLY the deviator's observed event and next private type, never
   simulator-only rival types. State sufficiency is a separate modeling
   assumption, not proved by this abstract dynamic-programming theorem. -/

structure Model (S A O : Type) where
  outcomes : List O
  actions : S → List A
  current : S → A → Rat
  /-- Nonnegative transition weights; instantiate as discount * probability.
      Normalization of the undiscounted law is a separate model validation. -/
  probability : S → A → O → Rat
  probability_nonneg : ∀ s a o, 0 ≤ probability s a o
  next : S → A → O → S

/-- Explicit trees can condition later deviations on all earlier observable
    outcomes, hence are not restricted to the recommended Markov strategy. -/
inductive Policy (A O : Type) : Nat → Type where
  | done : Policy A O 0
  | step {n : Nat} (action : A) (continuation : O → Policy A O n) :
      Policy A O (n+1)

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

def expected (m : Model S A O) (s : S) (a : A) (f : O → Rat) : Rat :=
  sumOver m.outcomes (fun o => m.probability s a o * f o)

theorem sumOver_mono {α : Type} (xs : List α) (f g : α → Rat)
    (h : ∀ x, x ∈ xs → f x ≤ g x) : sumOver xs f ≤ sumOver xs g := by
  induction xs with
  | nil => exact Rat.le_refl
  | cons x xs ih =>
    have hh := h x (by simp)
    have ht := ih (fun y hy => h y (by simp [hy]))
    simp only [sumOver]
    grind

theorem expected_mono (m : Model S A O) (s : S) (a : A) (f g : O → Rat)
    (h : ∀ o, o ∈ m.outcomes → f o ≤ g o) :
    expected m s a f ≤ expected m s a g := by
  apply sumOver_mono
  intro o ho
  exact Rat.mul_le_mul_of_nonneg_left (h o ho) (m.probability_nonneg s a o)

/-- Zero-weight observations do not require a solved continuation. -/
theorem expected_mono_supported (m : Model S A O) (s : S) (a : A)
    (f g : O → Rat)
    (h : ∀ o, o ∈ m.outcomes → 0 < m.probability s a o → f o ≤ g o) :
    expected m s a f ≤ expected m s a g := by
  apply sumOver_mono
  intro o ho
  by_cases hp : 0 < m.probability s a o
  · exact Rat.mul_le_mul_of_nonneg_left (h o ho hp) (m.probability_nonneg s a o)
  · have hn := m.probability_nonneg s a o
    have hz : m.probability s a o = 0 := by grind
    simp only [hz, Rat.zero_mul]
    exact Rat.le_refl

def evaluate (m : Model S A O) : (n : Nat) → S → Policy A O n → Rat
  | 0, _, .done => 0
  | n+1, s, .step a k => m.current s a +
      expected m s a (fun o => evaluate m n (m.next s a o) (k o))

def Feasible (m : Model S A O) : (n : Nat) → S → Policy A O n → Prop
  | 0, _, .done => True
  | n+1, s, .step a k => a ∈ m.actions s ∧
      ∀ o, o ∈ m.outcomes → Feasible m n (m.next s a o) (k o)

/-- sigma n is the recommended action with n+1 rounds remaining. -/
def value (m : Model S A O) (sigma : Nat → S → A) : Nat → S → Rat
  | 0, _ => 0
  | n+1, s => m.current s (sigma n s) +
      expected m s (sigma n s) (fun o => value m sigma n (m.next s (sigma n s) o))

def recommend (m : Model S A O) (sigma : Nat → S → A) :
    (n : Nat) → S → Policy A O n
  | 0, _ => .done
  | n+1, s => .step (sigma n s)
      (fun o => recommend m sigma n (m.next s (sigma n s) o))

theorem recommend_value (m : Model S A O) (sigma : Nat → S → A)
    (n : Nat) (s : S) :
    evaluate m n s (recommend m sigma n s) = value m sigma n s := by
  induction n generalizing s with
  | zero => rfl
  | succ n ih => simp [evaluate, recommend, value, ih]

theorem recommend_feasible (m : Model S A O) (sigma : Nat → S → A)
    (h : ∀ n s, sigma n s ∈ m.actions s) (n : Nat) (s : S) :
    Feasible m n s (recommend m sigma n s) := by
  induction n generalizing s with
  | zero => trivial
  | succ n ih => exact ⟨h n s, fun o _ => ih (m.next s (sigma n s) o)⟩

def OneShot (m : Model S A O) (sigma : Nat → S → A) (n : Nat) (s : S) : Prop :=
  ∀ a, a ∈ m.actions s →
    m.current s a + expected m s a (fun o => value m sigma n (m.next s a o)) ≤
      value m sigma (n+1) s

/-- Check positive-weight children of EVERY feasible action, including
    off-equilibrium actions. This permits unresolved zero-weight branches. -/
def Sequential (m : Model S A O) (sigma : Nat → S → A) : Nat → S → Prop
  | 0, _ => True
  | n+1, s => OneShot m sigma n s ∧
      ∀ a, a ∈ m.actions s → ∀ o, o ∈ m.outcomes →
        0 < m.probability s a o → Sequential m sigma n (m.next s a o)

/-- GENERAL one-shot-deviation verification. This controls complete finite
    deviation trees, not just a selected path or an accounting identity. -/
theorem sequential_dominates_every_policy (m : Model S A O)
    (sigma : Nat → S → A) (n : Nat) (s : S)
    (hs : Sequential m sigma n s) (p : Policy A O n)
    (hp : Feasible m n s p) : evaluate m n s p ≤ value m sigma n s := by
  induction n generalizing s with
  | zero => cases p; exact Rat.le_refl
  | succ n ih =>
    cases p with
    | step a k =>
      obtain ⟨ha, hk⟩ := hp
      obtain ⟨hlocal, hchild⟩ := hs
      have hem := expected_mono_supported m s a
        (fun o => evaluate m n (m.next s a o) (k o))
        (fun o => value m sigma n (m.next s a o))
        (fun o ho hpos => ih (m.next s a o) (hchild a ha o ho hpos) (k o) (hk o ho))
      have hbest := hlocal a ha
      simp only [evaluate]
      grind

/-- A profitable one-shot deviation is itself a feasible full policy. -/
theorem all_policies_implies_oneShot (m : Model S A O)
    (sigma : Nat → S → A) (hfeas : ∀ n s, sigma n s ∈ m.actions s)
    (n : Nat) (s : S)
    (hall : ∀ p : Policy A O (n+1), Feasible m (n+1) s p →
      evaluate m (n+1) s p ≤ value m sigma (n+1) s) :
    OneShot m sigma n s := by
  intro a ha
  let p : Policy A O (n+1) := .step a
    (fun o => recommend m sigma n (m.next s a o))
  have hp : Feasible m (n+1) s p :=
    ⟨ha, fun o _ => recommend_feasible m sigma hfeas n (m.next s a o)⟩
  have h := hall p hp
  simpa [p, evaluate, recommend_value] using h

/-- Terminal incentives contain no future payoff, so future-only rewards
    cannot repair a negative current comparison in the final round. -/
theorem terminal_oneShot (m : Model S A O) (sigma : Nat → S → A)
    (s : S) : OneShot m sigma 0 s ↔
      ∀ a, a ∈ m.actions s → m.current s a ≤ m.current s (sigma 0 s) := by
  have hz : ∀ xs : List O, sumOver xs (fun _ => (0 : Rat)) = 0 := by
    intro xs
    induction xs with
    | nil => rfl
    | cons x xs ih => simp only [sumOver, ih]; decide +kernel
  simp only [OneShot, value, expected, Rat.mul_zero, hz, Rat.add_zero]

/-- CURRENT slack must be compared to a player's OWN continuation loss. -/
theorem bounded_future_preserves_incentive
    (truthNow otherNow truthLater otherLater bound : Rat)
    (hc : otherNow + bound ≤ truthNow)
    (hf : otherLater ≤ truthLater + bound) :
    otherNow + otherLater ≤ truthNow + truthLater := by grind

/-- Exact two-state incentive decomposition: action changes probability of
    expert public state, whose PRIVATE value may have either sign. -/
theorem two_state_deviation_gain
    (truthNow otherNow truthP otherP expert novice : Rat) :
    (truthNow + truthP*expert + (1-truthP)*novice) -
      (otherNow + otherP*expert + (1-otherP)*novice) =
    truthNow-otherNow + (truthP-otherP)*(expert-novice) := by grind

/-- A negative private return to expertise can reverse a positive current
    disclosure advantage. This is a sufficient strict inequality, not a
    claim that expertise always reduces private rents. -/
theorem future_rent_reverses_current_truth
    (truthNow otherNow truthP otherP expert novice : Rat)
    (hcurrent : otherNow < truthNow)
    (hfuture : truthNow-otherNow < (truthP-otherP)*(novice-expert)) :
    otherNow < truthNow ∧
    truthNow + truthP*expert + (1-truthP)*novice <
      otherNow + otherP*expert + (1-otherP)*novice := by
  exact ⟨hcurrent, by grind⟩

/- Candidate-strategy retention threshold, not an equilibrium selection. -/
theorem learning_retention_threshold (retention : Rat) :
    0 < -17/64+(9/32)*retention ↔ 17/18 < retention := by
  have hleft : (64 : Rat)*(-17/64+(9/32)*retention) = 18*retention-17 := by grind
  have hright : (18 : Rat)*(retention-17/18) = 18*retention-17 := by grind
  grind


/- Actual finite reporting-game instantiation: no fixed behavior is inserted
   into a claimed equilibrium without a separate exhaustive proof below.
   The numerical evaluator is independently tested, not extracted here. -/

inductive Action where
  | claim | record | silent
  deriving DecidableEq, Repr

structure Strategy where
  qualified : Action
  unsupported : Action
  deriving DecidableEq, Repr

def Strategy.at (p : Strategy) (q : Bool) : Action :=
  if q then p.qualified else p.unsupported

structure Stage where
  benefit : Rat
  qQualified : Rat
  qUnsupported : Rat
  fineQualified : Rat
  fineUnsupported : Rat
  recordUtility : Rat
  qualifiedValue : Rat
  unsupportedValue : Rat
  fallback : Rat
  auditRate : Rat
  auditCost : Rat
  recordCost : Rat
  deriving DecidableEq, Repr

def eligible (g : Stage) (q : Bool) (a : Action) : Rat :=
  match a with
  | .claim => if q then g.qQualified else g.qUnsupported
  | .record | .silent => 0

def rivalMass (g : Stage) (p : Strategy) : Rat :=
  (eligible g true p.qualified + eligible g false p.unsupported)/2

def currentPrivate (g : Stage) (q : Bool) (a : Action) (rival : Strategy) : Rat :=
  match a with
  | .claim => g.benefit * eligible g q a * (1-rivalMass g rival/2) -
      (if q then g.fineQualified else g.fineUnsupported)
  | .record => g.recordUtility
  | .silent => 0

/-- Public transition reads reports only: no hidden grade enters this rule.
    Record admission and useful diagnostic transfer remain stipulated here.
    In the implementation arbitrary finite probability rows replace it. -/
def nextExpert (expert learns : Bool) (first second : Action) : Bool :=
  expert || (learns && (first == .record || second == .record))

/-- Own future value integrates the rival's fresh hidden type but observes
    only the resulting public expertise state, never that hidden type. -/
def continuation (expert learns : Bool) (a : Action) (rival : Strategy)
    (future : Bool → Rat) : Rat :=
  (future (nextExpert expert learns a rival.qualified) +
   future (nextExpert expert learns a rival.unsupported))/2

def utility (g : Stage) (expert learns : Bool) (future : Bool → Rat)
    (q : Bool) (a : Action) (rival : Strategy) : Rat :=
  currentPrivate g q a rival + continuation expert learns a rival future

def WeakChoice (score : Action → Rat) (chosen : Action) : Prop :=
  score .claim ≤ score chosen ∧ score .record ≤ score chosen ∧ score .silent ≤ score chosen

def StrictAt (score : Action → Rat) : Action → Prop
  | .claim => score .record < score .claim ∧ score .silent < score .claim
  | .record => score .claim < score .record ∧ score .silent < score .record
  | .silent => score .claim < score .silent ∧ score .record < score .silent

def Equilibrium (g : Stage) (expert learns : Bool) (future : Bool → Rat)
    (first second : Strategy) : Prop :=
  WeakChoice (fun a => utility g expert learns future true a second) first.qualified ∧
  WeakChoice (fun a => utility g expert learns future false a second) first.unsupported ∧
  WeakChoice (fun a => utility g expert learns future true a first) second.qualified ∧
  WeakChoice (fun a => utility g expert learns future false a first) second.unsupported

def StrictEquilibrium (g : Stage) (expert learns : Bool) (future : Bool → Rat)
    (first second : Strategy) : Prop :=
  StrictAt (fun a => utility g expert learns future true a second) first.qualified ∧
  StrictAt (fun a => utility g expert learns future false a second) first.unsupported ∧
  StrictAt (fun a => utility g expert learns future true a first) second.qualified ∧
  StrictAt (fun a => utility g expert learns future false a first) second.unsupported

def truth : Strategy := ⟨.claim,.record⟩
def pooling : Strategy := ⟨.claim,.claim⟩
def allRecords : Strategy := ⟨.record,.record⟩

def realizedCurrent (g : Stage) (t u : Bool) (a b : Action) : Rat :=
  let qa := eligible g t a
  let qb := eligible g u b
  let va := if t then g.qualifiedValue else g.unsupportedValue
  let vb := if u then g.qualifiedValue else g.unsupportedValue
  let claims : Rat := (if a == .claim then 1 else 0) + (if b == .claim then 1 else 0)
  let records : Rat := (if a == .record then 1 else 0) + (if b == .record then 1 else 0)
  g.fallback + qa*(1-qb/2)*(va-g.fallback) + qb*(1-qa/2)*(vb-g.fallback) -
    claims*g.auditRate*g.auditCost - records*g.recordCost

def currentSponsor (g : Stage) (first second : Strategy) : Rat :=
  (realizedCurrent g true true first.qualified second.qualified +
   realizedCurrent g true false first.qualified second.unsupported +
   realizedCurrent g false true first.unsupported second.qualified +
   realizedCurrent g false false first.unsupported second.unsupported)/4

def futureSponsor (expert learns : Bool) (future : Bool → Rat)
    (first second : Strategy) : Rat :=
  (future (nextExpert expert learns first.qualified second.qualified) +
   future (nextExpert expert learns first.qualified second.unsupported) +
   future (nextExpert expert learns first.unsupported second.qualified) +
   future (nextExpert expert learns first.unsupported second.unsupported))/4

def sponsor (g : Stage) (expert learns : Bool) (future : Bool → Rat)
    (first second : Strategy) : Rat :=
  currentSponsor g first second + futureSponsor expert learns future first second

def teamValue (g : Stage) (expert learns : Bool) (future : Bool → Rat)
    (own rival : Strategy) : Rat :=
  (utility g expert learns future true own.qualified rival +
   utility g expert learns future false own.unsupported rival)/2

def safe : Stage :=
  ⟨2,1,1,0,0,1/8,3,-1,0,0,0,0⟩

def advanced (adverse expert : Bool) : Stage :=
  ⟨(if adverse then 2 else 4),(if expert then 1 else 0),0,
    (if expert then 0 else 1),1,1/8,8,-4,0,1,1/2,1/4⟩

def training (adverse : Bool) : Stage :=
  ⟨2,1,1/2,0,1/2,(if adverse then 9/32 else -1/64),6,-4,0,1,1/4,1/4⟩

def zeroFuture : Bool → Rat := fun _ => 0

/-- Last round terminal profiles are first proved, then used as continuations. -/
theorem safe_unique (expert : Bool) (first second : Strategy) :
    Equilibrium safe expert false zeroFuture first second ↔
      first=pooling ∧ second=pooling := by
  cases expert <;> rcases first with ⟨a,b⟩ <;> rcases second with ⟨c,d⟩ <;>
    cases a <;> cases b <;> cases c <;> cases d <;>
    unfold Equilibrium WeakChoice <;> decide +kernel

theorem safe_strict (expert : Bool) :
    StrictEquilibrium safe expert false zeroFuture pooling pooling := by
  cases expert <;> simp only [StrictEquilibrium, StrictAt, pooling] <;> decide +kernel

theorem advanced_unique (adverse expert : Bool) (first second : Strategy) :
    Equilibrium (advanced adverse expert) expert false zeroFuture first second ↔
      first=(if expert then truth else allRecords) ∧
      second=(if expert then truth else allRecords) := by
  cases adverse <;> cases expert <;>
    rcases first with ⟨a,b⟩ <;> rcases second with ⟨c,d⟩ <;>
    cases a <;> cases b <;> cases c <;> cases d <;>
    unfold Equilibrium WeakChoice <;> decide +kernel

theorem advanced_strict (adverse expert : Bool) :
    StrictEquilibrium (advanced adverse expert) expert false zeroFuture
      (if expert then truth else allRecords) (if expert then truth else allRecords) := by
  cases adverse <;> cases expert <;> simp only [StrictEquilibrium, StrictAt, truth, allRecords, Bool.false_eq_true, if_false, if_true] <;> decide +kernel

theorem terminal_sponsor_choice (adverse : Bool) :
    currentSponsor (advanced adverse false) allRecords allRecords <
      currentSponsor safe pooling pooling ∧
    currentSponsor safe pooling pooling <
      currentSponsor (advanced adverse true) truth truth := by
  cases adverse <;> decide +kernel

/-- These continuation functions are constructed from the actual, checked
    stage equilibria and sponsor choice, not standalone payoff constants. -/
def terminalPrivate (adverse expert : Bool) : Rat :=
  if expert then teamValue (advanced adverse true) true false zeroFuture truth truth
  else teamValue safe false false zeroFuture pooling pooling

def terminalSponsor (adverse expert : Bool) : Rat :=
  if expert then currentSponsor (advanced adverse true) truth truth
  else currentSponsor safe pooling pooling

/-- First-round safe action preserves state, so private continuation is
    action-independent. The result checks all81 profiles, not just pooling. -/
theorem first_safe_unique (adverse expert : Bool) (first second : Strategy) :
    Equilibrium safe expert false (terminalPrivate adverse) first second ↔
      first=pooling ∧ second=pooling := by
  cases adverse <;> cases expert <;>
    rcases first with ⟨a,b⟩ <;> rcases second with ⟨c,d⟩ <;>
    cases a <;> cases b <;> cases c <;> cases d <;>
    unfold Equilibrium WeakChoice <;> decide +kernel

theorem first_safe_strict (adverse expert : Bool) :
    StrictEquilibrium safe expert false (terminalPrivate adverse) pooling pooling := by
  cases adverse <;> cases expert <;> simp only [StrictEquilibrium, StrictAt, pooling] <;> decide +kernel

def trainingProfile (adverse expert : Bool) : Strategy :=
  if adverse then (if expert then truth else pooling)
  else (if expert then pooling else truth)

/-- Complete81-profile verification at both public states and both scenarios.
    In novice favorable state future learning induces D; in novice adverse
    state future information rent induces C. In expert state the expertise
    transition is already saturated, so the current incentives govern. -/
theorem training_unique (adverse expert : Bool) (first second : Strategy) :
    Equilibrium (training adverse) expert true (terminalPrivate adverse) first second ↔
      first=trainingProfile adverse expert ∧ second=trainingProfile adverse expert := by
  cases adverse <;> cases expert <;>
    rcases first with ⟨a,b⟩ <;> rcases second with ⟨c,d⟩ <;>
    cases a <;> cases b <;> cases c <;> cases d <;>
    unfold Equilibrium WeakChoice <;> decide +kernel

theorem training_strict (adverse expert : Bool) :
    StrictEquilibrium (training adverse) expert true (terminalPrivate adverse)
      (trainingProfile adverse expert) (trainingProfile adverse expert) := by
  cases adverse <;> cases expert <;> simp only [StrictEquilibrium, StrictAt, trainingProfile, truth, pooling, Bool.false_eq_true, if_false, if_true] <;> decide +kernel

/-- Sponsor choices are endogenous and use public state, including offpath
    expert state; all current experiment subgames have been checked above. -/
theorem first_sponsor_training_choice (adverse expert : Bool) :
    sponsor safe expert false (terminalSponsor adverse) pooling pooling <
      sponsor (training adverse) expert true (terminalSponsor adverse)
        (trainingProfile adverse expert) (trainingProfile adverse expert) := by
  cases adverse <;> cases expert <;> decide +kernel

theorem primary_model_value :
    sponsor (training false) false true (terminalSponsor false) truth truth = 131/16 := by
  decide +kernel

theorem adverse_model_value :
    sponsor (training true) false true (terminalSponsor true) pooling pooling = 3 := by
  decide +kernel

theorem primary_model_private_value :
    teamValue (training false) false true (terminalPrivate false) truth truth = 277/128 := by
  decide +kernel

theorem costly_record_is_dynamically_best :
    currentPrivate (training false) false .record truth <
      currentPrivate (training false) false .claim truth ∧
    utility (training false) false true (terminalPrivate false) false .claim truth <
      utility (training false) false true (terminalPrivate false) false .record truth := by
  decide +kernel

theorem current_honesty_is_dynamically_reversed :
    currentPrivate (training true) false .claim pooling <
      currentPrivate (training true) false .record pooling ∧
    utility (training true) false true (terminalPrivate true) false .record pooling <
      utility (training true) false true (terminalPrivate true) false .claim pooling := by
  decide +kernel

theorem terminal_training_unique (first second : Strategy) :
    Equilibrium (training false) false true zeroFuture first second ↔
      first=pooling ∧ second=pooling := by
  rcases first with ⟨a,b⟩
  rcases second with ⟨c,d⟩
  cases a <;> cases b <;> cases c <;> cases d <;>
    unfold Equilibrium WeakChoice <;> decide +kernel

theorem terminal_training_value : currentSponsor (training false) pooling pooling = 2 := by
  decide +kernel

theorem real_model_mandatory_cost_loss :
    sponsor (training false) false true (terminalSponsor false) truth truth - 7 <
      sponsor safe false false (terminalSponsor false) pooling pooling := by
  decide +kernel



/-- Discount belongs to the team's own continuation differential. -/
theorem discounted_two_state_deviation_gain
    (truthNow otherNow truthP otherP expert novice discount : Rat) :
    (truthNow + discount*(truthP*expert + (1-truthP)*novice)) -
      (otherNow + discount*(otherP*expert + (1-otherP)*novice)) =
    truthNow-otherNow + discount*(truthP-otherP)*(expert-novice) := by grind



/-- The actual fixture induced decision process for one deviating team.
    There are no persistent private variables. Grade is OWN current evidence.
    Public expertise plus next own grade are the observable transition. -/
structure Information where
  firstRound : Bool
  expert : Bool
  qualified : Bool
  deriving DecidableEq, Repr

def informationStage (adverse : Bool) (s : Information) : Stage :=
  if s.firstRound then training adverse
  else if s.expert then advanced adverse true else safe

def informationRival (adverse : Bool) (s : Information) : Strategy :=
  if s.firstRound then trainingProfile adverse s.expert
  else if s.expert then truth else pooling

def informationWeight (adverse : Bool) (s : Information) (a : Action)
    (observation : Bool × Bool) : Rat :=
  let r := informationRival adverse s
  let qNext := nextExpert s.expert s.firstRound a r.qualified
  let uNext := nextExpert s.expert s.firstRound a r.unsupported
  ((if qNext == observation.1 then 1 else 0) +
   (if uNext == observation.1 then 1 else 0))/4

/-- The /4 integrates a rival type of probability1/2 and a NEXT own type
    of probability1/2. No next action sees the rival's private type. -/
def inducedPlayer (adverse : Bool) : Model Information Action (Bool × Bool) where
  outcomes := [(false,false),(false,true),(true,false),(true,true)]
  actions := fun _ => [.claim,.record,.silent]
  current := fun s a => currentPrivate (informationStage adverse s) s.qualified a
    (informationRival adverse s)
  probability := informationWeight adverse
  probability_nonneg := by
    intro s a o
    rcases s with ⟨first,expert,qualified⟩
    rcases o with ⟨nextExpert,nextQualified⟩
    cases adverse <;> cases first <;> cases expert <;> cases qualified <;>
      cases a <;> cases nextExpert <;> cases nextQualified <;> decide +kernel
  next := fun _ _ o => ⟨false,o.1,o.2⟩

def recommendedPlayer (adverse : Bool) (_ : Nat) (s : Information) : Action :=
  (informationRival adverse s).at s.qualified

/-- Feasibility is separate from the Bellman dominance premise. -/
theorem recommended_action_feasible (adverse : Bool) (n : Nat) (s : Information) :
    recommendedPlayer adverse n s ∈ (inducedPlayer adverse).actions s := by
  change recommendedPlayer adverse n s ∈ [.claim,.record,.silent]
  cases recommendedPlayer adverse n s <;> simp

theorem actual_recommendation_feasible (adverse : Bool) (n : Nat) (s : Information) :
    Feasible (inducedPlayer adverse) n s
      (recommend (inducedPlayer adverse) (recommendedPlayer adverse) n s) := by
  exact recommend_feasible (inducedPlayer adverse) (recommendedPlayer adverse)
    (recommended_action_feasible adverse) n s

/-- Positive/negative grades of the NEXT round are integrated, not copied
    from the current type; this directly checks the fresh-evidence law. -/
theorem induced_weights_normalized (adverse : Bool) (s : Information) (a : Action) :
    sumOver (inducedPlayer adverse).outcomes
      (fun o => (inducedPlayer adverse).probability s a o) = 1 := by
  rcases s with ⟨first,expert,qualified⟩
  cases adverse <;> cases first <;> cases expert <;> cases qualified <;>
    cases a <;> decide +kernel

theorem actual_terminal_oneShot (adverse expert qualified : Bool) :
    OneShot (inducedPlayer adverse) (recommendedPlayer adverse) 0
      ⟨false,expert,qualified⟩ := by
  intro a _
  cases adverse <;> cases expert <;> cases qualified <;> cases a <;> decide +kernel

theorem actual_initial_oneShot (adverse expert qualified : Bool) :
    OneShot (inducedPlayer adverse) (recommendedPlayer adverse) 1
      ⟨true,expert,qualified⟩ := by
  intro a _
  cases adverse <;> cases expert <;> cases qualified <;> cases a <;> decide +kernel

theorem actual_two_round_sequential (adverse expert qualified : Bool) :
    Sequential (inducedPlayer adverse) (recommendedPlayer adverse) 2
      ⟨true,expert,qualified⟩ := by
  constructor
  · exact actual_initial_oneShot adverse expert qualified
  · intro a ha o ho hpos
    change Sequential (inducedPlayer adverse) (recommendedPlayer adverse) 1
      ⟨false,o.1,o.2⟩
    constructor
    · exact actual_terminal_oneShot adverse o.1 o.2
    · intro b hb p hp hpositive
      trivial

/-- ACTUAL FIXTURE global deviation theorem: every feasible two-round policy
    tree may change its initial report and all later expertise/own-type
    contingent reports. Other observed audit/award histories are not encoded;
    their payoff irrelevance is part of the modeling reduction. It still cannot improve upon the proved dynamic profile.
    Symmetry gives the same theorem for the other persistent team. -/
theorem actual_fixture_all_reporting_deviations
    (adverse expert qualified : Bool) (p : Policy Action (Bool × Bool) 2)
    (hp : Feasible (inducedPlayer adverse) 2 ⟨true,expert,qualified⟩ p) :
    evaluate (inducedPlayer adverse) 2 ⟨true,expert,qualified⟩ p ≤
      value (inducedPlayer adverse) (recommendedPlayer adverse) 2
        ⟨true,expert,qualified⟩ := by
  exact sequential_dominates_every_policy (inducedPlayer adverse)
    (recommendedPlayer adverse) 2 ⟨true,expert,qualified⟩
    (actual_two_round_sequential adverse expert qualified) p hp

theorem induced_value_matches_primary_profile (qualified : Bool) :
    value (inducedPlayer false) (recommendedPlayer false) 2 ⟨true,false,qualified⟩ =
      utility (training false) false true (terminalPrivate false)
        qualified (truth.at qualified) truth := by
  cases qualified <;> decide +kernel

theorem induced_value_matches_adverse_profile (qualified : Bool) :
    value (inducedPlayer true) (recommendedPlayer true) 2 ⟨true,false,qualified⟩ =
      utility (training true) false true (terminalPrivate true)
        qualified (pooling.at qualified) pooling := by
  cases qualified <;> decide +kernel


/- Genuine menu expansion: original favorable stage primitives remain fixed.
   Only a new terminal expert-state experiment is added. -/

def menuNewAdvanced : Stage :=
  { advanced true true with qualifiedValue := 9 }

def oldExpertMenu : List Stage := [safe, advanced false true]
def expandedExpertMenu : List Stage := [safe, advanced false true, menuNewAdvanced]

theorem expanded_menu_retains_every_old_option :
    ∀ g, g ∈ oldExpertMenu → g ∈ expandedExpertMenu := by
  intro g hg
  change g ∈ [safe, advanced false true] at hg
  change g ∈ [safe, advanced false true, menuNewAdvanced]
  simp only [List.mem_cons, List.not_mem_nil, or_false] at hg ⊢
  rcases hg with h | h
  · exact Or.inl h
  · exact Or.inr (Or.inl h)

theorem menu_new_advanced_unique (first second : Strategy) :
    Equilibrium menuNewAdvanced true false zeroFuture first second ↔
      first=truth ∧ second=truth := by
  rcases first with ⟨a,b⟩
  rcases second with ⟨c,d⟩
  cases a <;> cases b <;> cases c <;> cases d <;>
    unfold Equilibrium WeakChoice <;> decide +kernel

theorem menu_new_advanced_strict :
    StrictEquilibrium menuNewAdvanced true false zeroFuture truth truth := by
  simp only [StrictEquilibrium, StrictAt, truth]
  decide +kernel

theorem menu_new_terminal_sponsor_value :
    currentSponsor menuNewAdvanced truth truth = 6 := by decide +kernel

theorem menu_new_terminal_private_value :
    teamValue menuNewAdvanced true false zeroFuture truth truth = 13/16 := by
  decide +kernel

/-- The discretionary sponsor strictly chooses the added experiment in the
    expert state, even though the old advanced experiment remains available. -/
theorem menu_new_terminal_choice :
    currentSponsor safe pooling pooling < currentSponsor menuNewAdvanced truth truth ∧
    currentSponsor (advanced false true) truth truth <
      currentSponsor menuNewAdvanced truth truth := by decide +kernel

def expandedTerminalPrivate (expert : Bool) : Rat :=
  if expert then teamValue menuNewAdvanced true false zeroFuture truth truth
  else teamValue safe false false zeroFuture pooling pooling

def expandedTerminalSponsor (expert : Bool) : Rat :=
  if expert then currentSponsor menuNewAdvanced truth truth
  else currentSponsor safe pooling pooling

/-- Connect new-stage continuation to the already named low-rent private
    value. This changes neither original training credit nor old B's fields. -/
theorem expanded_private_is_low_rent (expert : Bool) :
    expandedTerminalPrivate expert = terminalPrivate true expert := by
  cases expert <;> decide +kernel

/-- Original favorable training, with its original negative record utility,
    becomes pooling under the newly preferred terminal continuation. -/
theorem menu_training_low_rent_unique (expert : Bool) (first second : Strategy) :
    Equilibrium (training false) expert true (terminalPrivate true) first second ↔
      first=pooling ∧ second=pooling := by
  cases expert <;>
    rcases first with ⟨a,b⟩ <;> rcases second with ⟨c,d⟩ <;>
    cases a <;> cases b <;> cases c <;> cases d <;>
    unfold Equilibrium WeakChoice <;> decide +kernel

theorem menu_training_low_rent_strict (expert : Bool) :
    StrictEquilibrium (training false) expert true (terminalPrivate true) pooling pooling := by
  cases expert <;> simp only [StrictEquilibrium, StrictAt, pooling] <;> decide +kernel

theorem menu_training_expanded_unique (expert : Bool) (first second : Strategy) :
    Equilibrium (training false) expert true expandedTerminalPrivate first second ↔
      first=pooling ∧ second=pooling := by
  have he : expandedTerminalPrivate = terminalPrivate true := by
    funext e
    exact expanded_private_is_low_rent e
  rw [he]
  exact menu_training_low_rent_unique expert first second

theorem menu_training_expanded_strict (expert : Bool) :
    StrictEquilibrium (training false) expert true expandedTerminalPrivate pooling pooling := by
  have he : expandedTerminalPrivate = terminalPrivate true := by
    funext e
    exact expanded_private_is_low_rent e
  rw [he]
  exact menu_training_low_rent_strict expert

theorem menu_first_safe_unique (expert : Bool) (first second : Strategy) :
    Equilibrium safe expert false expandedTerminalPrivate first second ↔
      first=pooling ∧ second=pooling := by
  have he : expandedTerminalPrivate = terminalPrivate true := by
    funext e
    exact expanded_private_is_low_rent e
  rw [he]
  exact first_safe_unique true expert first second

theorem menu_first_safe_strict (expert : Bool) :
    StrictEquilibrium safe expert false expandedTerminalPrivate pooling pooling := by
  have he : expandedTerminalPrivate = terminalPrivate true := by
    funext e
    exact expanded_private_is_low_rent e
  rw [he]
  exact first_safe_strict true expert

theorem menu_first_sponsor_training_choice (expert : Bool) :
    sponsor safe expert false expandedTerminalSponsor pooling pooling <
      sponsor (training false) expert true expandedTerminalSponsor pooling pooling := by
  cases expert <;> decide +kernel

theorem expanded_menu_initial_value :
    sponsor (training false) false true expandedTerminalSponsor pooling pooling = 3 := by
  decide +kernel

/-- More available future experiments can LOWER the sequential-equilibrium
    value because today's reports respond to tomorrow's discretionary choice.
    This does not contradict optimization over committed complete policies. -/
theorem genuine_menu_expansion_equilibrium_loss :
    (∀ g, g ∈ oldExpertMenu → g ∈ expandedExpertMenu) ∧
    sponsor (training false) false true expandedTerminalSponsor pooling pooling <
      sponsor (training false) false true (terminalSponsor false) truth truth := by
  constructor
  · exact expanded_menu_retains_every_old_option
  · decide +kernel

end RepeatedExperiment