ExpertiseScarcity.lean

import Std

/- Finite conditional benchmark checked with pinned Lean 4.24.0.
   Rational finite benchmark; no real-valued stochastic or empirical theorem.
   No axiom, sorry or external mathlib dependency. -/
namespace ExpertiseScarcity

def practice (x q d : Rat) : Rat := (d*x+q)/(1+q)
def stock (x h : Rat) : Rat := (x+h)/(1+h)
def gross (a c h : Rat) : Rat := a*h/(1+h)-c*h

theorem div_nonneg {a b : Rat} (ha : 0 ≤ a) (hb : 0 < b) :
    0 ≤ a/b := by
  have hi := Rat.le_of_lt (Rat.inv_pos.mpr hb)
  have hm := Rat.mul_nonneg ha hi
  simpa only [Rat.div_def] using hm

theorem div_le {a b c : Rat} (hb : 0 < b) (ha : a ≤ c*b) :
    a/b ≤ c := by
  have hn : b ≠ 0 := by grind
  have he := Rat.div_mul_cancel (a := a) hn
  apply Rat.le_of_mul_le_mul_right (c := b) _ hb
  grind

theorem practice_bounds (x q d : Rat)
    (hx : 0 ≤ x) (hx1 : x ≤ 1) (hq : 0 ≤ q)
    (hd : 0 ≤ d) (hd1 : d ≤ 1) :
    0 ≤ practice x q d ∧ practice x q d ≤ 1 := by
  have hp : 0 < 1+q := by grind
  have hn := Rat.mul_nonneg hd hx
  have hu := Rat.mul_le_mul_of_nonneg_left hx1 hd
  constructor
  · exact div_nonneg (by grind) hp
  · exact div_le hp (by grind)

/-- Three-point finite distribution: noise -s, 0, s, probabilities
    (1-x)/2, x, (1-x)/2. -/
def finiteLoss (b s x : Rat) : Rat :=
  ((1-x)/2)*((b-s)*(b-s)/2) + x*(b*b/2) +
  ((1-x)/2)*((b+s)*(b+s)/2)

theorem finite_loss_decomposition (b s x : Rat) :
    finiteLoss b s x = (b*b+s*s*(1-x))/2 := by
  unfold finiteLoss
  grind

theorem common_local_threshold (bc bl s xc xl : Rat) :
    finiteLoss bc s xc < finiteLoss bl s xl ↔
    bc*bc-bl*bl < s*s*(xc-xl) := by
  rw [finite_loss_decomposition, finite_loss_decomposition]
  have hl := Rat.div_mul_cancel
    (a := bc*bc+s*s*(1-xc)) (b := 2) (by decide +kernel)
  have hr := Rat.div_mul_cancel
    (a := bl*bl+s*s*(1-xl)) (b := 2) (by decide +kernel)
  have hi := Rat.mul_lt_mul_right
    (a := (bc*bc+s*s*(1-xc))/2)
    (b := (bl*bl+s*s*(1-xl))/2) (c := 2) (by decide +kernel)
  grind

theorem common_mismatch_reversal :
    finiteLoss 1 1 (3/4) > finiteLoss 0 1 (1/4) := by
  unfold finiteLoss
  decide +kernel

/-- Difference before activation; F is not charged to the h=0 outside option. -/
theorem packet_marginal (a c h : Rat) (hh : 0 ≤ h) :
    gross a c (h+1)-gross a c h=a/((h+1)*(h+2))-c := by
  have h1 : h+1 ≠ 0 := by grind
  have h2 : h+2 ≠ 0 := by grind
  have hp : (h+1)*(h+2) ≠ 0 := by
    have hm := Rat.mul_pos (a := h+1) (b := h+2) (by grind) (by grind)
    grind
  unfold gross
  grind

theorem next_packet_worthwhile (a c h : Rat) (hh : 0 ≤ h) :
    gross a c h < gross a c (h+1) ↔ a > c*((h+1)*(h+2)) := by
  have hp := Rat.mul_pos (a := h+1) (b := h+2) (by grind) (by grind)
  have hm := packet_marginal a c h hh
  have hi := Rat.lt_div_iff (a := c) (b := a) hp
  grind

theorem activation_threshold (a c f h : Rat) (hh : 0 ≤ h) :
    f < gross a c h ↔ a*h > (f+c*h)*(1+h) := by
  have hp : 0 < 1+h := by grind
  have hi := Rat.lt_div_iff (a := f+c*h) (b := a*h) hp
  unfold gross
  grind

/-- This identity permits a global discrete optimum proof without calculus. -/
theorem gross_difference (a c y k : Rat) (hy : 0 ≤ y) (hk : 0 ≤ k) :
    gross a c y-gross a c k =
    (y-k)*(a-c*(1+y)*(1+k))/((1+y)*(1+k)) := by
  have h1 : 1+y ≠ 0 := by grind
  have h2 : 1+k ≠ 0 := by grind
  have hp := Rat.mul_pos (a := 1+y) (b := 1+k) (by grind) (by grind)
  have hp0 : (1+y)*(1+k) ≠ 0 := by grind
  unfold gross
  grind

theorem optimum_dominates_earlier (a c y k : Rat)
    (hc : 0 ≤ c) (hy : 0 ≤ y) (hyk : y+1 ≤ k)
    (ha : c*k*(k+1) ≤ a) : gross a c y ≤ gross a c k := by
  have hk : 0 ≤ k := by grind
  have hkp : 0 ≤ 1+k := by grind
  have hck := Rat.mul_nonneg hc hkp
  have hbound := Rat.mul_le_mul_of_nonneg_left hyk hck
  have hgap : 0 ≤ a-c*(1+y)*(1+k) := by grind
  have hky : 0 ≤ k-y := by grind
  have hnum := Rat.mul_nonneg hky hgap
  have hden := Rat.mul_pos (a := 1+y) (b := 1+k) (by grind) (by grind)
  have hdiv : (y-k)*(a-c*(1+y)*(1+k))/((1+y)*(1+k)) ≤ 0 :=
    div_le hden (by grind)
  have he := gross_difference a c y k hy hk
  grind

theorem optimum_dominates_later (a c y k : Rat)
    (hc : 0 ≤ c) (hk : 0 ≤ k) (hky : k+1 ≤ y)
    (ha : a ≤ c*(k+1)*(k+2)) : gross a c y ≤ gross a c k := by
  have hy : 0 ≤ y := by grind
  have hkp : 0 ≤ 1+k := by grind
  have hck := Rat.mul_nonneg hc hkp
  have hstep : k+2 ≤ 1+y := by grind
  have hbound := Rat.mul_le_mul_of_nonneg_left hstep hck
  have hgap : 0 ≤ c*(1+y)*(1+k)-a := by grind
  have hyk : 0 ≤ y-k := by grind
  have hnum := Rat.mul_nonneg hyk hgap
  have hden := Rat.mul_pos (a := 1+y) (b := 1+k) (by grind) (by grind)
  have hdiv : (y-k)*(a-c*(1+y)*(1+k))/((1+y)*(1+k)) ≤ 0 :=
    div_le hden (by grind)
  have he := gross_difference a c y k hy hk
  grind

/-- Sufficient adjacent threshold conditions imply GLOBAL optimality across
    all packet counts in the finite cap, including endpoint k=0 and k=H. -/
theorem finite_packet_optimum (a c : Rat) (H k : Nat)
    (hc : 0 ≤ c) (hkH : k ≤ H)
    (hleft : 0 < k → c*(k:Rat)*((k:Rat)+1) ≤ a)
    (hright : k < H → a ≤ c*((k:Rat)+1)*((k:Rat)+2)) :
    ∀ y : Nat, y ≤ H → gross a c (y:Rat) ≤ gross a c (k:Rat) := by
  intro y hyH
  have hy0 := Rat.natCast_nonneg (a := y)
  have hk0 := Rat.natCast_nonneg (a := k)
  by_cases he : y=k
  · subst y; exact Rat.le_refl
  by_cases hlt : y<k
  · have hkpos : 0<k := by omega
    have hykN : y+1 ≤ k := by omega
    have hyk := Rat.natCast_le_natCast.mpr hykN
    have hykR : (y:Rat)+1 ≤ (k:Rat) := by grind
    exact optimum_dominates_earlier a c (y:Rat) (k:Rat) hc hy0 hykR (hleft hkpos)
  · have hkH' : k<H := by omega
    have hkyN : k+1 ≤ y := by omega
    have hky := Rat.natCast_le_natCast.mpr hkyN
    have hkyR : (k:Rat)+1 ≤ (y:Rat) := by grind
    exact optimum_dominates_later a c (y:Rat) (k:Rat) hc hk0 hkyR (hright hkH')

/-- Same total 2h practice; two actually feasible downstream workloads. -/
def concentrationGain (x h w1 w2 : Rat) : Rat :=
  w1*(stock x (2*h)-x)-(w1+w2)*(stock x h-x)

theorem concentration_gap (x h w1 w2 : Rat) (hh : 0 ≤ h) :
    concentrationGain x h w1 w2 =
    (1-x)*h*(w1-(1+2*h)*w2)/((1+h)*(1+2*h)) := by
  have h1 : 1+h ≠ 0 := by grind
  have h2 : 1+2*h ≠ 0 := by grind
  have hp := Rat.mul_pos (a := 1+h) (b := 1+2*h) (by grind) (by grind)
  have hp0 : (1+h)*(1+2*h) ≠ 0 := by grind
  unfold concentrationGain stock
  grind

theorem concentration_wins_iff (x h w1 w2 : Rat)
    (hx : x<1) (hh : 0<h) :
    0 < concentrationGain x h w1 w2 ↔ (1+2*h)*w2 < w1 := by
  have h0 : 0 ≤ h := by grind
  have hp := Rat.mul_pos (a := 1+h) (b := 1+2*h) (by grind) (by grind)
  have hn := Rat.mul_pos (a := 1-x) (b := h) (by grind) hh
  have hdiv := Rat.lt_div_iff (a := 0) (b := (1-x)*h*(w1-(1+2*h)*w2)) hp
  have hmul := Rat.mul_pos_iff_of_pos_left (b := w1-(1+2*h)*w2) hn
  rw [concentration_gap x h w1 w2 h0]
  grind

theorem spread_equal_workload_wins : concentrationGain 0 1 1 1 < 0 := by
  unfold concentrationGain stock
  decide +kernel

theorem concentrate_unequal_workload_wins : 0 < concentrationGain 0 1 4 1 := by
  unfold concentrationGain stock
  decide +kernel

def positivePart (x : Rat) : Rat := if 0≤x then x else 0

theorem gross_information_value_nonnegative (sPlus sMinus : Rat) :
    positivePart (sPlus+sMinus) ≤ positivePart sPlus+positivePart sMinus := by
  unfold positivePart
  split <;> split <;> split <;> grind

theorem net_information_threshold (sPlus sMinus cost : Rat) :
    positivePart (sPlus+sMinus) < positivePart sPlus+positivePart sMinus-cost ↔
    cost < positivePart sPlus+positivePart sMinus-positivePart (sPlus+sMinus) := by
  grind

/-- One award, binary free priority, fair tie. -/
def priorityAward (own other : Bool) : Rat :=
  if own=other then 1/2 else if own then 1 else 0

def priorityUtility (b : Rat) (own other : Bool) : Rat := b*priorityAward own other

theorem high_priority_strictly_dominates (b : Rat) (hb : 0<b) (other : Bool) :
    priorityUtility b false other < priorityUtility b true other := by
  cases other with
  | false =>
    change b*(1/2) < b*1
    exact Rat.mul_lt_mul_of_pos_left (c := b) (by decide +kernel) hb
  | true =>
    change b*0 < b*(1/2)
    exact Rat.mul_lt_mul_of_pos_left (c := b) (by decide +kernel) hb

def purePriorityNash (b1 b2 : Rat) (s1 s2 : Bool) : Prop :=
  (∀ a : Bool, priorityUtility b1 a s2 ≤ priorityUtility b1 s1 s2) ∧
  (∀ a : Bool, priorityUtility b2 a s1 ≤ priorityUtility b2 s2 s1)

theorem unique_pure_priority_equilibrium (b1 b2 : Rat) (hb1 : 0<b1) (hb2 : 0<b2)
    (s1 s2 : Bool) : purePriorityNash b1 b2 s1 s2 ↔ s1=true ∧ s2=true := by
  constructor
  · intro hn
    have h1 := hn.1 true
    have h2 := hn.2 true
    have d1 := high_priority_strictly_dominates b1 hb1 s2
    have d2 := high_priority_strictly_dominates b2 hb2 s1
    cases s1 <;> cases s2 <;> simp_all <;> grind
  · intro hs
    rcases hs with ⟨rfl,rfl⟩
    constructor
    · intro a
      cases a with
      | false => exact Rat.le_of_lt (high_priority_strictly_dominates b1 hb1 true)
      | true => exact Rat.le_refl
    · intro a
      cases a with
      | false => exact Rat.le_of_lt (high_priority_strictly_dominates b2 hb2 true)
      | true => exact Rat.le_refl

/-- Independent two-type, two-team experiment; opponent H enters and L stays.
    Explicitly enumerate the opponent's no-entry/fail/pass branches. -/
def separatingAward (pi pHigh pOwn : Rat) : Rat :=
  (1-pi)*pOwn + pi*(pOwn*(1-pHigh)+pOwn*pHigh/2)

theorem separating_award_probability (pi pHigh pOwn : Rat) :
    separatingAward pi pHigh pOwn = pOwn*(1-pi*pHigh/2) := by
  unfold separatingAward
  grind

def entryUtility (pi pHigh pOwn benefit burden : Rat) : Rat :=
  benefit*separatingAward pi pHigh pOwn-burden

/-- These are exactly the two strict best-reply comparisons, one at each
    private type, against the proposed separating opponent strategy. -/
def strictSeparatingBestReplies (pi pHigh pLow benefit burden : Rat) : Prop :=
  0 < entryUtility pi pHigh pHigh benefit burden ∧
  entryUtility pi pHigh pLow benefit burden < 0

theorem strict_separating_equilibrium_threshold (pi pHigh pLow benefit burden : Rat) :
    strictSeparatingBestReplies pi pHigh pLow benefit burden ↔
    pLow*(1-pi*pHigh/2)*benefit < burden ∧
    burden < pHigh*(1-pi*pHigh/2)*benefit := by
  unfold strictSeparatingBestReplies entryUtility
  rw [separating_award_probability, separating_award_probability]
  grind

/-- An actual outcome, not just a sum of marginal award probabilities.
    The coin is fair in the expected-utility calculation; capacity holds for
    either coin outcome, with no probabilistic assumption. -/
inductive Award where
  | none
  | first
  | second
  deriving DecidableEq

def chooseAward (a b coin : Bool) : Award :=
  if a then
    if b then (if coin then .first else .second) else .first
  else if b then .second else .none

def firstFunded : Award → Nat
  | .first => 1
  | _ => 0

def secondFunded : Award → Nat
  | .second => 1
  | _ => 0

theorem one_award_capacity (a b coin : Bool) :
    firstFunded (chooseAward a b coin)+secondFunded (chooseAward a b coin) ≤ 1 := by
  cases a <;> cases b <;> cases coin <;> decide

def sponsorGain (pi pHigh value testCost : Rat) : Rat :=
  (2*(pi*pHigh)-(pi*pHigh)*(pi*pHigh))*value-2*pi*testCost

theorem at_least_one_positive (r : Rat) : 1-(1-r)*(1-r)=2*r-r*r := by grind

theorem strict_separation_example :
    strictSeparatingBestReplies (1/2) (3/4) (1/4) 4 (3/2) := by
  unfold strictSeparatingBestReplies entryUtility separatingAward
  decide +kernel

theorem high_type_enters_example :
    entryUtility (1/2) (3/4) (3/4) 4 (3/2)=15/16 := by
  unfold entryUtility separatingAward
  decide +kernel

theorem low_type_stays_example :
    entryUtility (1/2) (3/4) (1/4) 4 (3/2)= -11/16 := by
  unfold entryUtility separatingAward
  decide +kernel

theorem separating_gate_profitable_example : sponsorGain (1/2) (3/4) 8 1=31/8 := by
  unfold sponsorGain
  decide +kernel

theorem separating_gate_loses_example : sponsorGain (1/2) (3/4) 1 1= -25/64 := by
  unfold sponsorGain
  decide +kernel

#print axioms practice_bounds
#print axioms finite_loss_decomposition
#print axioms finite_packet_optimum
#print axioms concentration_wins_iff
#print axioms unique_pure_priority_equilibrium
#print axioms strict_separating_equilibrium_threshold
#print axioms one_award_capacity
end ExpertiseScarcity