StrategicPitch.lean

import Std

/- Conditional finite model, Lean 4.24.0 / Std only.
   Root is sole compiler/runner. Finite reporting game, not a repeated game.
   No economic value is treated as an auditable fact. -/
namespace StrategicReporting

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

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

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

structure Game where
  prior : Rat
  benefit : Rat
  qQualified : Rat
  qUnsupported : Rat
  fineQualified : Rat
  fineUnsupported : Rat
  claimBurden : Rat
  disclosureUtility : Rat
  auditRate : Rat
  deriving DecidableEq, Repr

/-- Flag exclusion and sanction enforcement are separate. The private fine
    is expected disutility; it is never counted as sponsor revenue. -/
def auditGame (prior benefit audit falsePositive sensitivity enforcement penalty
    claimBurden disclosureUtility : Rat) : Game :=
  { prior := prior
    benefit := benefit
    qQualified := 1-audit*falsePositive
    qUnsupported := 1-audit*sensitivity
    fineQualified := audit*falsePositive*enforcement*penalty
    fineUnsupported := audit*sensitivity*enforcement*penalty
    claimBurden := claimBurden
    disclosureUtility := disclosureUtility
    auditRate := audit }

structure Valid (g : Game) : Prop where
  prior0 : 0 ≤ g.prior
  prior1 : g.prior ≤ 1
  qualified0 : 0 ≤ g.qQualified
  qualified1 : g.qQualified ≤ 1
  unsupported0 : 0 ≤ g.qUnsupported
  unsupported1 : g.qUnsupported ≤ 1
  benefit0 : 0 ≤ g.benefit

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

def rivalMass (g : Game) (s : Strategy) : Rat :=
  g.prior * eligible g true s.qualified +
  (1-g.prior) * eligible g false s.unsupported

def claimValue (benefit q fine burden rival : Rat) : Rat :=
  benefit*q*(1-rival/2)-fine-burden

def utility (g : Game) (qualified : Bool) (a : Action) (rival : Strategy) : Rat :=
  match a with
  | .claim =>
      claimValue g.benefit (if qualified then g.qQualified else g.qUnsupported)
        (if qualified then g.fineQualified else g.fineUnsupported)
        g.claimBurden (rivalMass g rival)
  | .record => g.disclosureUtility
  | .silent => 0

/-- All three deviations are retained explicitly, permitting exact finite
    checks without claiming a preferred equilibrium selection. -/
def WeakChoice (score : Action → Rat) (chosen : Action) : Prop :=
  score .claim ≤ score chosen ∧ score .record ≤ score chosen ∧ score .silent ≤ score chosen

def StrictChoice (score : Action → Rat) (chosen : Action) : Prop :=
  ∀ other : Action, other ≠ chosen → score other < 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 : Game) (first second : Strategy) : Prop :=
  WeakChoice (fun a => utility g true a second) first.qualified ∧
  WeakChoice (fun a => utility g false a second) first.unsupported ∧
  WeakChoice (fun a => utility g true a first) second.qualified ∧
  WeakChoice (fun a => utility g false a first) second.unsupported

def StrictEquilibrium (g : Game) (first second : Strategy) : Prop :=
  StrictAt (fun a => utility g true a second) first.qualified ∧
  StrictAt (fun a => utility g false a second) first.unsupported ∧
  StrictAt (fun a => utility g true a first) second.qualified ∧
  StrictAt (fun a => utility g false a first) second.unsupported

/-- The probability comes from sole eligibility plus a fair shared tie. -/
theorem award_probability (q r : Rat) :
    q*(1-r)+q*r/2 = q*(1-r/2) := by grind

theorem eligible_bounds (g : Game) (hv : Valid g) (t : Bool) (a : Action) :
    0 ≤ eligible g t a ∧ eligible g t a ≤ 1 := by
  cases a with
  | claim =>
    cases t with
    | false => exact ⟨hv.unsupported0,hv.unsupported1⟩
    | true => exact ⟨hv.qualified0,hv.qualified1⟩
  | record => simp only [eligible]; constructor <;> decide +kernel
  | silent => simp only [eligible]; constructor <;> decide +kernel

theorem rival_mass_bounds (g : Game) (hv : Valid g) (s : Strategy) :
    0 ≤ rivalMass g s ∧ rivalMass g s ≤ 1 := by
  have ht := eligible_bounds g hv true s.qualified
  have hl := eligible_bounds g hv false s.unsupported
  have hp : 0 ≤ 1-g.prior := by have h := hv.prior1; grind
  have n1 := Rat.mul_nonneg hv.prior0 ht.1
  have n2 := Rat.mul_nonneg hp hl.1
  have u1 := Rat.mul_le_mul_of_nonneg_left ht.2 hv.prior0
  have u2 := Rat.mul_le_mul_of_nonneg_left hl.2 hp
  unfold rivalMass
  constructor <;> grind

theorem claim_lower_bound (b q fine burden r : Rat)
    (hbq : 0 ≤ b*q) (hr : r ≤ 1) :
    b*q/2-fine-burden ≤ claimValue b q fine burden r := by
  have h1 : 0 ≤ 1-r := by grind
  have hm := Rat.mul_nonneg hbq h1
  have hh : (0:Rat) ≤ 1/2 := by decide +kernel
  have hn := Rat.mul_nonneg hm hh
  have he : b*q*(1-r)*(1/2) = claimValue b q fine burden r - (b*q/2-fine-burden) := by
    unfold claimValue
    grind
  rw [he] at hn
  grind

theorem claim_upper_bound (b q fine burden r : Rat)
    (hbq : 0 ≤ b*q) (hr : 0 ≤ r) :
    claimValue b q fine burden r ≤ b*q-fine-burden := by
  have hm := Rat.mul_nonneg hbq hr
  have hh : (0:Rat) ≤ 1/2 := by decide +kernel
  have hn := Rat.mul_nonneg hm hh
  have he : b*q*r*(1/2) = (b*q-fine-burden) - claimValue b q fine burden r := by
    unfold claimValue
    grind
  rw [he] at hn
  grind

theorem strict_choice_weak (score : Action → Rat) (best : Action)
    (h : StrictChoice score best) : WeakChoice score best := by
  have hall : ∀ a : Action, score a ≤ score best := by
    intro a
    by_cases he : a = best
    · subst a; exact Rat.le_refl
    · exact Rat.le_of_lt (h a he)
  exact ⟨hall .claim,hall .record,hall .silent⟩

theorem strict_choice_unique (score : Action → Rat) (best selected : Action)
    (hstrict : StrictChoice score best) (hweak : WeakChoice score selected) :
    selected = best := by
  by_cases he : selected = best
  · exact he
  have hne := he
  exfalso
  have hl := hstrict selected hne
  have hu : score best ≤ score selected := by
    cases best with
    | claim => exact hweak.1
    | record => exact hweak.2.1
    | silent => exact hweak.2.2
  grind

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

/-- SUBSTANTIVE dominance result, uniform over every rival strategy. -/
theorem truthful_actions_strictly_dominant (g : Game) (hv : Valid g)
    (hg : 0 < g.disclosureUtility)
    (hq : g.disclosureUtility <
      g.benefit*g.qQualified/2-g.fineQualified-g.claimBurden)
    (hu : g.benefit*g.qUnsupported-g.fineUnsupported-g.claimBurden <
      g.disclosureUtility)
    (t : Bool) (rival : Strategy) :
    StrictChoice (fun a => utility g t a rival) (truth.at t) := by
  have hr := rival_mass_bounds g hv rival
  have nq := Rat.mul_nonneg hv.benefit0 hv.qualified0
  have nu := Rat.mul_nonneg hv.benefit0 hv.unsupported0
  have lq := claim_lower_bound g.benefit g.qQualified g.fineQualified
    g.claimBurden (rivalMass g rival) nq hr.2
  have uu := claim_upper_bound g.benefit g.qUnsupported g.fineUnsupported
    g.claimBurden (rivalMass g rival) nu hr.1
  intro other hne
  cases t <;> cases other <;>
    simp only [truth,Strategy.at,utility] at * <;> grind

/-- General uniqueness from strict type-contingent dominance. This quantifies
    over arbitrary asymmetric strategy pairs, not only symmetric candidates. -/
theorem unique_equilibrium_of_strict_dominance (g : Game) (target : Strategy)
    (hdom : ∀ t : Bool, ∀ rival : Strategy,
      StrictChoice (fun a => utility g t a rival) (target.at t))
    (first second : Strategy) :
    Equilibrium g first second ↔ first = target ∧ second = target := by
  constructor
  · intro he
    have h1 := strict_choice_unique (fun a => utility g true a second)
      (target.at true) first.qualified (hdom true second) he.1
    have h2 := strict_choice_unique (fun a => utility g false a second)
      (target.at false) first.unsupported (hdom false second) he.2.1
    have h3 := strict_choice_unique (fun a => utility g true a first)
      (target.at true) second.qualified (hdom true first) he.2.2.1
    have h4 := strict_choice_unique (fun a => utility g false a first)
      (target.at false) second.unsupported (hdom false first) he.2.2.2
    cases first
    cases second
    cases target
    simp_all [Strategy.at]
  · intro h
    rw [h.1,h.2]
    exact ⟨strict_choice_weak _ _ (hdom true target),
      strict_choice_weak _ _ (hdom false target),
      strict_choice_weak _ _ (hdom true target),
      strict_choice_weak _ _ (hdom false target)⟩

theorem unique_truthful_equilibrium (g : Game) (hv : Valid g)
    (hg : 0 < g.disclosureUtility)
    (hq : g.disclosureUtility <
      g.benefit*g.qQualified/2-g.fineQualified-g.claimBurden)
    (hu : g.benefit*g.qUnsupported-g.fineUnsupported-g.claimBurden <
      g.disclosureUtility)
    (first second : Strategy) :
    Equilibrium g first second ↔ first = truth ∧ second = truth := by
  exact unique_equilibrium_of_strict_dominance g truth
    (truthful_actions_strictly_dominant g hv hg hq hu) first second

/-- Adverse disclosure cannot be elicited by auditing funding claims alone
    when disclosure has negative net private utility and silence is free. -/
theorem costly_disclosure_not_best_reply (g : Game) (hg : g.disclosureUtility < 0)
    (t : Bool) (rival : Strategy) :
    ¬ WeakChoice (fun a => utility g t a rival) .record := by
  intro h
  have hs := h.2.2
  change 0 ≤ g.disclosureUtility at hs
  grind

theorem zero_credit_disclosure_not_strict (g : Game) (hg : g.disclosureUtility = 0)
    (t : Bool) (rival : Strategy) :
    ¬ StrictChoice (fun a => utility g t a rival) .record := by
  intro h
  have hs := h .silent (by decide)
  change 0 < g.disclosureUtility at hs
  grind

/-- Nondiscriminating checks cannot strictly separate otherwise identical
    private preferences. This is not an assumption that future value is known. -/
theorem nondiscriminating_no_strict_separation (g : Game)
    (hq : g.qQualified = g.qUnsupported)
    (hf : g.fineQualified = g.fineUnsupported) (rival : Strategy) :
    ¬ (StrictChoice (fun a => utility g true a rival) .claim ∧
       StrictChoice (fun a => utility g false a rival) .record) := by
  rintro ⟨hc,hd⟩
  have h1 := hc .record (by decide)
  have h2 := hd .claim (by decide)
  simp only [utility] at h1 h2
  rw [hq,hf] at h1
  grind

/-- Prior technical failure is not the misconduct variable. A failure can
    be honestly disclosed in a qualified diagnostic case. -/
structure Evidence where
  qualified : Bool
  previousRunFailed : Bool
  deriving DecidableEq, Repr

def evidenceUtility (g : Game) (e : Evidence) (a : Action) (rival : Strategy) : Rat :=
  utility g e.qualified a rival

theorem honest_failure_not_penalized_as_such (g : Game) (q : Bool)
    (a : Action) (rival : Strategy) :
    evidenceUtility g ⟨q,true⟩ a rival = evidenceUtility g ⟨q,false⟩ a rival := by rfl

def allStrategies : List Strategy :=
  [⟨.claim,.claim⟩,⟨.claim,.record⟩,⟨.claim,.silent⟩,
   ⟨.record,.claim⟩,⟨.record,.record⟩,⟨.record,.silent⟩,
   ⟨.silent,.claim⟩,⟨.silent,.record⟩,⟨.silent,.silent⟩]

def allProfiles : List (Strategy × Strategy) :=
  allStrategies.flatMap (fun first => allStrategies.map (fun second => (first,second)))

theorem every_strategy_listed (s : Strategy) : s ∈ allStrategies := by
  cases s with
  | mk a b => cases a <;> cases b <;> decide

theorem every_profile_listed (first second : Strategy) : (first,second) ∈ allProfiles := by
  simp only [allProfiles,List.mem_flatMap,List.mem_map]
  exact ⟨first,every_strategy_listed first,second,every_strategy_listed second,rfl⟩

theorem eighty_one_profiles : allProfiles.length = 81 := by decide

/-- Realized allocation. Audit flags already include whether the audit ran. -/
def admitted (a : Action) (flagged : Bool) : Bool :=
  if a = .claim then !flagged else false

def chooseAward (first second coin : Bool) : Bool × Bool :=
  if first then (if second then (coin,!coin) else (true,false)) else (false,second)

def countFunded (x : Bool × Bool) : Nat :=
  (if x.1 then 1 else 0)+(if x.2 then 1 else 0)

theorem one_slot_capacity (a b coin : Bool) : countFunded (chooseAward a b coin) ≤ 1 := by
  cases a <;> cases b <;> cases coin <;> decide

theorem record_never_claims_slot (flag : Bool) : admitted .record flag = false := by rfl
theorem silence_never_claims_slot (flag : Bool) : admitted .silent flag = false := by rfl

def actionMass (g : Game) (s : Strategy) (a : Action) : Rat :=
  g.prior*(if s.qualified=a then 1 else 0) +
  (1-g.prior)*(if s.unsupported=a then 1 else 0)

def valueMass (g : Game) (jq ju fallback : Rat) (s : Strategy) : Rat :=
  g.prior*eligible g true s.qualified*(jq-fallback) +
  (1-g.prior)*eligible g false s.unsupported*(ju-fallback)

def gross (g : Game) (jq ju fallback : Rat) (first second : Strategy) : Rat :=
  (1-rivalMass g second/2)*valueMass g jq ju fallback first +
  (1-rivalMass g first/2)*valueMass g jq ju fallback second

theorem branch_value_identity (r1 r2 z1 z2 : Rat) :
    ((1-r2)*z1+r2*z1/2) + ((1-r1)*z2+r1*z2/2) =
      (1-r2/2)*z1+(1-r1/2)*z2 := by grind

def sponsor (g : Game) (jq ju fallback auditCost claimCost recordCost fixedCost : Rat)
    (first second : Strategy) : Rat :=
  gross g jq ju fallback first second -
  (actionMass g first .claim+actionMass g second .claim)*(g.auditRate*auditCost+claimCost) -
  (actionMass g first .record+actionMass g second .record)*recordCost-fixedCost

theorem sponsor_symmetric (g : Game) (jq ju fallback auditCost claimCost recordCost fixedCost : Rat)
    (first second : Strategy) :
    sponsor g jq ju fallback auditCost claimCost recordCost fixedCost first second =
    sponsor g jq ju fallback auditCost claimCost recordCost fixedCost second first := by
  unfold sponsor gross
  grind

def baseline : Game := auditGame (1/2) 4 1 (1/4) (3/4) 1 4 0 (1/8)
def noAudit : Game := auditGame (1/2) 4 0 (1/4) (3/4) 1 4 0 (1/8)
def weakEnforcement : Game := auditGame (1/2) 4 1 (1/4) (3/4) 0 4 0 (1/8)
def falseAccusations : Game := auditGame (1/2) 4 1 (3/4) (3/4) 1 4 0 (1/8)
def noDiscrimination : Game := auditGame (1/2) 4 1 (1/4) (1/4) 1 4 0 (1/8)
def zeroCredit : Game := auditGame (1/2) 4 1 (1/4) (3/4) 1 4 0 0
def costlyRecord : Game := auditGame (1/2) 4 1 (1/4) (3/4) 1 4 0 (-1/4)
def halfAudit : Game := auditGame (1/2) 4 (1/2) (1/4) (3/4) 1 4 0 (1/8)

theorem baseline_valid : Valid baseline := by
  constructor <;> decide +kernel

theorem baseline_unique (first second : Strategy) :
    Equilibrium baseline first second ↔ first=truth ∧ second=truth := by
  exact unique_truthful_equilibrium baseline baseline_valid (by decide +kernel)
    (by decide +kernel) (by decide +kernel) first second

theorem baseline_strict : StrictEquilibrium baseline truth truth := by
  simp only [StrictEquilibrium,StrictAt,truth]
  decide +kernel

theorem baseline_private_utilities :
    utility baseline true .claim truth = 23/16 ∧
    utility baseline false .claim truth = -35/16 ∧
    utility baseline false .record truth = 1/8 := by decide +kernel

theorem baseline_gross : gross baseline 8 (-4) 2 truth truth = 117/32 := by decide +kernel

theorem baseline_net : sponsor baseline 8 (-4) 2 (1/2) 0 (1/4) 0 truth truth = 93/32 := by
  decide +kernel

theorem overhead_loss : sponsor baseline 8 (-4) 2 4 0 (1/4) 0 truth truth = -19/32 := by
  decide +kernel

/-- Complete finite checks cover all asymmetric profiles as well. -/
theorem no_audit_unique (first second : Strategy) :
    Equilibrium noAudit 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 no_audit_pooling_strict : StrictEquilibrium noAudit pooling pooling := by
  simp only [StrictEquilibrium,StrictAt,pooling]
  decide +kernel

theorem no_audit_net : sponsor noAudit 8 (-4) 2 (1/2) 0 (1/4) 0 pooling pooling = 0 := by
  decide +kernel

theorem weak_enforcement_unique (first second : Strategy) :
    Equilibrium weakEnforcement 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 weak_enforcement_still_filters :
    sponsor weakEnforcement 8 (-4) 2 (1/2) 0 (1/4) 0 pooling pooling = 5/4 := by
  decide +kernel

theorem weak_enforcement_high_cost_loses :
    sponsor weakEnforcement 8 (-4) 2 2 0 (1/4) 0 pooling pooling = -7/4 := by
  decide +kernel

theorem false_accusations_unique (first second : Strategy) :
    Equilibrium falseAccusations first second ↔ first=allRecords ∧ second=allRecords := 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 false_accusations_lose :
    sponsor falseAccusations 8 (-4) 2 (1/2) 0 (1/4) 0 allRecords allRecords = -1/2 := by
  decide +kernel

theorem nondiscriminating_unique (first second : Strategy) :
    Equilibrium noDiscrimination 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 nondiscriminating_audit_loses :
    sponsor noDiscrimination 8 (-4) 2 (1/2) 0 (1/4) 0 pooling pooling = -1 := by
  decide +kernel

/-- Exactly four pure equilibria, including two asymmetric ones. -/
theorem zero_credit_equilibria (first second : Strategy) :
    Equilibrium zeroCredit first second ↔
      (first=truth ∨ first=quiet) ∧ (second=truth ∨ second=quiet) := 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 costly_record_unique (first second : Strategy) :
    Equilibrium costlyRecord first second ↔ first=quiet ∧ second=quiet := 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 costly_record_no_records : actionMass costlyRecord quiet .record = 0 := by decide +kernel

theorem costly_record_one_shot_value :
    sponsor costlyRecord 8 (-4) 2 (1/2) 0 (1/4) 0 quiet quiet = 101/32 := by
  decide +kernel

/-- Partial auditing admits TWO strict asymmetric equilibria, not a selected
    symmetric fiction. Complete profile enumeration proves exhaustiveness. -/
theorem half_audit_equilibria (first second : Strategy) :
    Equilibrium halfAudit first second ↔
      (first=pooling ∧ second=truth) ∨ (first=truth ∧ 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 half_audit_asymmetric_strict : StrictEquilibrium halfAudit pooling truth := by
  simp only [StrictEquilibrium,StrictAt,truth,pooling]
  decide +kernel

theorem half_audit_reverse_strict : StrictEquilibrium halfAudit truth pooling := by
  simp only [StrictEquilibrium,StrictAt,truth,pooling]
  decide +kernel

theorem half_audit_no_symmetric_pure (s : Strategy) : ¬ Equilibrium halfAudit s s := by
  rw [half_audit_equilibria]
  have h : pooling ≠ truth := by decide
  grind

theorem half_audit_deviation :
    utility halfAudit false .claim truth = 29/64 ∧
    utility halfAudit false .claim pooling = 1/16 := by decide +kernel

theorem half_audit_net :
    sponsor halfAudit 8 (-4) 2 (1/2) 0 (1/4) 0 pooling truth = 221/128 := by
  decide +kernel

theorem economic_misalignment_loses :
    sponsor baseline 0 8 2 (1/2) 0 (1/4) 0 truth truth = -63/32 := by
  decide +kernel

theorem economic_misalignment_uninformed :
    sponsor noAudit 0 8 2 (1/2) 0 (1/4) 0 pooling pooling = 2 := by
  decide +kernel

end StrategicReporting