WorkforcePlanning.lean

import Std

namespace WorkforcePlanning

/- Actual physical workforce model, finite causal policies and Bellman
   certificate. Four dates, two observed regimes, two skill pools. The
   general theorem itself is horizon-parametric. Concrete tables below will
   instantiate the frozen finite cases after preregistered execution. -/

inductive Skill where | A | B deriving DecidableEq, Repr
inductive Status where | absent | pending | active deriving DecidableEq, Repr
structure State where
  regime : Bool
  a : Status
  b : Status
  deriving DecidableEq, Repr
abbrev Action := Fin 192

def statuses : List Status := [.absent,.pending,.active]
def states : List State := [false,true].flatMap (fun z =>
  statuses.flatMap (fun a => statuses.map (fun b => ⟨z,a,b⟩)))

def statusIndex : Status → Nat | .absent => 0 | .pending => 1 | .active => 2
def stateIndex (s : State) : Nat := 9*s.regime.toNat + 3*statusIndex s.a + statusIndex s.b

theorem state_enumeration_complete (s : State) : s ∈ states := by
  cases s with
  | mk z a b => cases z <;> cases a <;> cases b <;> decide +kernel

def actions : List Action := [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110,111,112,113,114,115,116,117,118,119,120,121,122,123,124,125,126,127,128,129,130,131,132,133,134,135,136,137,138,139,140,141,142,143,144,145,146,147,148,149,150,151,152,153,154,155,156,157,158,159,160,161,162,163,164,165,166,167,168,169,170,171,172,173,174,175,176,177,178,179,180,181,182,183,184,185,186,187,188,189,190,191]

theorem action_enumeration_complete : ∀ a : Action, a ∈ actions := by decide +kernel

def change (a : Action) : Skill → Bool
  | .A => decide (96 ≤ a.val)
  | .B => decide ((a.val / 48) % 2 = 1)
def borrowedSkill (a : Action) : Skill → Bool
  | .A => decide ((a.val / 16) % 3 = 1)
  | .B => decide ((a.val / 16) % 3 = 2)
def own (a : Action) : Skill → Bool
  | .A => a.val.testBit 3
  | .B => a.val.testBit 2
def temporary (a : Action) : Skill → Bool
  | .A => a.val.testBit 1
  | .B => a.val.testBit 0
def status (s : State) : Skill → Status | .A => s.a | .B => s.b

theorem at_most_one_borrowed_skill : ∀ a : Action,
    ¬ (borrowedSkill a .A = true ∧ borrowedSkill a .B = true) := by decide +kernel

structure Model where
  longLead : Skill → Bool
  value : Skill → Rat
  outside : Skill → Rat
  wage : Skill → Rat
  hireCost : Skill → Rat
  exitCost : Skill → Rat
  cancelCost : Skill → Rat
  borrowCost : Skill → Rat
  demand : Nat → Bool → Skill → Nat
  available : Nat → Bool → Skill → Bool
  high : Nat → Bool → Rat

structure Valid (m : Model) (H : Nat) : Prop where
  high_nonneg : ∀ t, t < H → ∀ z, 0 ≤ m.high t z
  high_le_one : ∀ t, t < H → ∀ z, m.high t z ≤ 1
  hire_nonneg : ∀ k, 0 ≤ m.hireCost k
  exit_nonneg : ∀ k, 0 ≤ m.exitCost k
  cancel_nonneg : ∀ k, 0 ≤ m.cancelCost k
  cancel_le_exit : ∀ k, m.cancelCost k ≤ m.exitCost k

abbrev SkillFeasible (m : Model) (t : Nat) (s : State) (a : Action) (k : Skill) : Prop :=
  (own a k).toNat ≤ (if status s k = .active then 1 else 0) ∧
  (temporary a k).toNat ≤ (borrowedSkill a k).toNat ∧
  (own a k).toNat + (temporary a k).toNat ≤ m.demand t s.regime k ∧
  (borrowedSkill a k = true → m.available t s.regime k = true)
abbrev FeasibleAction (m : Model) (t : Nat) (s : State) (a : Action) : Prop :=
  SkillFeasible m t s a .A ∧ SkillFeasible m t s a .B

def allowed (m : Model) (t : Nat) (s : State) (a : Action) : Bool :=
  decide (FeasibleAction m t s a)

def nextStatus (longLead : Bool) : Status → Bool → Status
  | .absent, false => .absent
  | .absent, true => if longLead then .pending else .active
  | .pending, false => .active
  | .pending, true => .absent
  | .active, false => .active
  | .active, true => .absent

def next (m : Model) (s : State) (a : Action) (z : Bool) : State :=
  ⟨z,nextStatus (m.longLead .A) s.a (change a .A),
     nextStatus (m.longLead .B) s.b (change a .B)⟩

def bit (b : Bool) : Rat := if b then 1 else 0

def managementCost (m : Model) (s : Status) (change : Bool) (k : Skill) : Rat :=
  if change then match s with
    | .absent => m.hireCost k
    | .pending => m.cancelCost k
    | .active => m.exitCost k
  else 0

def skillStage (m : Model) (s : State) (a : Action) (k : Skill) : Rat :=
  (bit (own a k) + bit (temporary a k)) * (m.value k - m.outside k) -
  (if status s k = .active then m.wage k else 0) -
  managementCost m (status s k) (change a k) k -
  bit (borrowedSkill a k) * m.borrowCost k

def stage (m : Model) (s : State) (a : Action) : Rat :=
  skillStage m s a .A + skillStage m s a .B

def settlement (m : Model) (k : Skill) : Status → Rat
  | .absent => 0
  | .pending => -m.cancelCost k
  | .active => -m.exitCost k

def terminal (m : Model) (s : State) : Rat :=
  settlement m .A s.a + settlement m .B s.b

def expected (m : Model) (t : Nat) (s : State) (f : Bool → Rat) : Rat :=
  (1-m.high t s.regime)*f false + m.high t s.regime*f true

inductive Policy : Nat → Type where
  | done : Policy 0
  | step {n : Nat} (action : Action) (continuation : Bool → Policy n) : Policy (n+1)

def evaluate (m : Model) : (n : Nat) → Nat → State → Policy n → Rat
  | 0, _, s, .done => terminal m s
  | n+1, t, s, .step a k => stage m s a +
      expected m t s (fun z => evaluate m n (t+1) (next m s a z) (k z))

def Physical (m : Model) : (n : Nat) → Nat → State → Policy n → Prop
  | 0, _, _, .done => True
  | n+1, t, s, .step a k => allowed m t s a = true ∧
      ∀ z, Physical m n (t+1) (next m s a z) (k z)

def UpperCertificate (m : Model) (H : Nat) (U : Nat → State → Rat) : Prop :=
  (∀ s, terminal m s ≤ U H s) ∧
  ∀ t, t < H → ∀ s a, allowed m t s a = true →
    stage m s a + expected m t s (fun z => U (t+1) (next m s a z)) ≤ U t s

theorem expected_mono (m : Model) (H : Nat) (hv : Valid m H)
    (t : Nat) (ht : t < H) (s : State) (f g : Bool → Rat)
    (h : ∀ z, f z ≤ g z) : expected m t s f ≤ expected m t s g := by
  have hp := hv.high_nonneg t ht s.regime
  have hq := hv.high_le_one t ht s.regime
  have hc : 0 ≤ 1-m.high t s.regime := by grind
  have h0 := Rat.mul_le_mul_of_nonneg_left (h false) hc
  have h1 := Rat.mul_le_mul_of_nonneg_left (h true) hp
  simp only [expected]
  grind

/-- Arbitrary deterministic-action policies may use the entire past regime
    history. No action can depend on the next observed regime before it occurs. -/
theorem certificate_bounds_every_history_policy (m : Model) (H : Nat)
    (hv : Valid m H) (U : Nat → State → Rat) (hc : UpperCertificate m H U)
    (n t : Nat) (horizon : t+n=H) (s : State) (pi : Policy n)
    (hp : Physical m n t s pi) : evaluate m n t s pi ≤ U t s := by
  induction n generalizing t s with
  | zero =>
    have he : t=H := by omega
    cases pi
    simpa [evaluate,he] using hc.1 s
  | succ n ih =>
    cases pi with
    | step a k =>
      obtain ⟨ha,hk⟩ := hp
      have ht : t < H := by omega
      have hfuture := expected_mono m H hv t ht s
        (fun z => evaluate m n (t+1) (next m s a z) (k z))
        (fun z => U (t+1) (next m s a z))
        (fun z => ih (t+1) (by omega) (next m s a z) (k z) (hk z))
      have hu := hc.2 t ht s a ha
      simp only [evaluate]
      grind

def checkCertificate (m : Model) (H : Nat) (U : Nat → State → Rat) : Bool :=
  states.all (fun s => decide (terminal m s ≤ U H s)) &&
  (List.range H).all (fun t => states.all (fun s => actions.all (fun a =>
    !allowed m t s a || decide
      (stage m s a + expected m t s (fun z => U (t+1) (next m s a z)) ≤ U t s))))

theorem checked_certificate_is_upper (m : Model) (H : Nat) (U : Nat → State → Rat)
    (h : checkCertificate m H U = true) : UpperCertificate m H U := by
  obtain ⟨hz,hs⟩ := Bool.and_eq_true_iff.mp h
  constructor
  · intro s
    exact of_decide_eq_true (List.all_eq_true.mp hz s (state_enumeration_complete s))
  · intro t ht s a ha
    have hh := List.all_eq_true.mp hs t (List.mem_range.mpr ht)
    have hh' := List.all_eq_true.mp hh s (state_enumeration_complete s)
    have hh'' := List.all_eq_true.mp hh' a (action_enumeration_complete a)
    simpa [ha] using hh''

def recommend (m : Model) (sigma : Nat → State → Action) : (n : Nat) → Nat → State → Policy n
  | 0, _, _ => .done
  | n+1, t, s => .step (sigma t s)
      (fun z => recommend m sigma n (t+1) (next m s (sigma t s) z))

theorem recommend_feasible (m : Model) (H : Nat) (sigma : Nat → State → Action)
    (hf : ∀ t, t < H → ∀ s, allowed m t s (sigma t s) = true)
    (n t : Nat) (horizon : t+n=H) (s : State) :
    Physical m n t s (recommend m sigma n t s) := by
  induction n generalizing t s with
  | zero => trivial
  | succ n ih =>
    exact ⟨hf t (by omega) s, fun z => ih (t+1) (by omega) _⟩

def checkPolicy (m : Model) (H : Nat) (sigma : Nat → State → Action) : Bool :=
  (List.range H).all (fun t => states.all (fun s => allowed m t s (sigma t s)))

theorem checked_policy_is_feasible (m : Model) (H : Nat) (sigma : Nat → State → Action)
    (h : checkPolicy m H sigma = true) (t : Nat) (ht : t < H) (s : State) :
    allowed m t s (sigma t s) = true := by
  exact List.all_eq_true.mp (List.all_eq_true.mp h t (List.mem_range.mpr ht)) s
    (state_enumeration_complete s)

theorem attaining_certificate_is_globally_optimal (m : Model) (H : Nat)
    (hv : Valid m H) (U : Nat → State → Rat) (hc : UpperCertificate m H U)
    (s : State) (witness : Policy H) (hw : Physical m H 0 s witness)
    (he : evaluate m H 0 s witness = U 0 s) :
    Physical m H 0 s witness ∧ ∀ pi, Physical m H 0 s pi →
      evaluate m H 0 s pi ≤ evaluate m H 0 s witness := by
  refine ⟨hw, ?_⟩
  intro pi hp
  rw [he]
  exact certificate_bounds_every_history_policy m H hv U hc H 0 (by omega) s pi hp

/-- Current capacity is determined before recruitment and before arrival. -/
theorem absent_or_pending_cannot_serve (m : Model) (t : Nat) (s : State) (a : Action)
    (ha : allowed m t s a = true) (k : Skill) (hk : status s k ≠ .active) :
    (own a k).toNat = 0 := by
  have hf : FeasibleAction m t s a := of_decide_eq_true ha
  have hs : SkillFeasible m t s a k := by cases k; exact hf.1; exact hf.2
  have hcap := hs.1
  simp only [if_neg hk] at hcap
  omega

/-- Pending at a decision epoch always means exactly one remaining transition.
    Lead2 begun now becomes pending next epoch, then active one epoch later. -/
theorem lead_two_pipeline :
    nextStatus true .absent true = .pending ∧
    nextStatus true .pending false = .active := by decide +kernel

theorem terminal_pending_cannot_gain_by_maturing (m : Model) (H : Nat)
    (hv : Valid m H) (k : Skill) :
    settlement m k (nextStatus (m.longLead k) .pending false) ≤
      -m.cancelCost k + settlement m k (nextStatus (m.longLead k) .pending true) := by
  have hc := hv.cancel_le_exit k
  simp only [nextStatus,settlement]
  grind

/-- Erasing only A's management-change bit preserves all current service and
    temporary reservations, and leaves B's management choice unchanged. -/
def eraseA (a : Action) : Action :=
  ⟨a.val % 96, Nat.lt_trans (Nat.mod_lt _ (by decide)) (by decide)⟩

theorem eraseA_physical_identity : ∀ a : Action,
    change (eraseA a) .A = false ∧
    change (eraseA a) .B = change a .B ∧
    own (eraseA a) .A = own a .A ∧ own (eraseA a) .B = own a .B ∧
    temporary (eraseA a) .A = temporary a .A ∧
    temporary (eraseA a) .B = temporary a .B ∧
    borrowedSkill (eraseA a) .A = borrowedSkill a .A ∧
    borrowedSkill (eraseA a) .B = borrowedSkill a .B := by decide +kernel

theorem eraseA_preserves_current_feasibility (m : Model) (t : Nat)
    (s : State) (a : Action) (h : allowed m t s a = true) :
    allowed m t s (eraseA a) = true := by
  obtain ⟨_,_,hoA,hoB,htA,htB,hbA,hbB⟩ := eraseA_physical_identity a
  simpa only [allowed,FeasibleAction,SkillFeasible,hoA,hoB,htA,htB,hbA,hbB] using h

def lastValue (m : Model) (s : State) (a : Action) : Rat :=
  stage m s a + terminal m (next m s a false)

/-- A joint action cannot improve its last-date value by starting an A hire:
    deleting that recruitment preserves current feasibility and removes both
    its recruitment expense and its terminal liability. B's decision is held
    fixed. This is a conditional dominance result, not a steady-state rule. -/
theorem last_date_hiring_A_is_weakly_dominated (m : Model) (H : Nat)
    (hv : Valid m H) (t : Nat) (s : State) (a : Action)
    (hs : s.a = .absent) (hc : change a .A = true)
    (hf : allowed m t s a = true) :
    allowed m t s (eraseA a) = true ∧ lastValue m s a ≤ lastValue m s (eraseA a) := by
  refine ⟨eraseA_preserves_current_feasibility m t s a hf, ?_⟩
  obtain ⟨hmA,hmB,hoA,hoB,htA,htB,hbA,hbB⟩ := eraseA_physical_identity a
  have hk := hv.hire_nonneg .A
  have he := hv.exit_nonneg .A
  have hcancel := hv.cancel_nonneg .A
  simp only [lastValue,stage,skillStage,status,hs,hc,hmA,hmB,hoA,hoB,htA,htB,hbA,hbB,
    managementCost,next,terminal,nextStatus,settlement]
  split <;> grind

/- The concrete costs and demand laws are the frozen JavaScript primitives.
   At the unused last transition high=0: settlement is regime-independent. -/
def base : Model where
  longLead := fun _ => false
  value := fun _ => 10
  outside := fun _ => 2
  wage := fun _ => 2
  hireCost := fun _ => 3
  exitCost := fun _ => 1
  cancelCost := fun _ => 1
  borrowCost := fun _ => 5
  demand := fun _ _ _ => 0
  available := fun _ _ _ => true
  high := fun _ _ => 0

def W2 : Model := {base with demand := fun t _ k =>
  if (t=1 ∨ t=2) ∧ k=.A then 1 else 0}
def W9b : Model := {base with
  demand := fun t z k => if (t=1 ∨ t=2) ∧ z=true ∧ k=.A then 1 else 0
  high := fun t z => if t=0 then 3/4 else if t=1 then (if z then 1 else 0) else 0}
def initial : State := ⟨false,.absent,.absent⟩

theorem W2_valid : Valid W2 3 := by
  constructor
  · intro t _ z; change (0:Rat) ≤ 0; exact Rat.le_refl
  · intro t _ z; change (0:Rat) ≤ 1; decide +kernel
  · intro k; cases k <;> decide +kernel
  · intro k; cases k <;> decide +kernel
  · intro k; cases k <;> decide +kernel
  · intro k; cases k <;> decide +kernel

theorem W9b_valid : Valid W9b 3 := by
  constructor
  · intro t ht z
    have h : t=0 ∨ t=1 ∨ t=2 := by omega
    rcases h with rfl|rfl|rfl <;> cases z <;> decide +kernel
  · intro t ht z
    have h : t=0 ∨ t=1 ∨ t=2 := by omega
    rcases h with rfl|rfl|rfl <;> cases z <;> decide +kernel
  · intro k; cases k <;> decide +kernel
  · intro k; cases k <;> decide +kernel
  · intro k; cases k <;> decide +kernel
  · intro k; cases k <;> decide +kernel

/- These small tables are proposed certificates, not trusted oracle axioms.
   Kernel reduction checks the actual action admission, workforce transitions,
   stage payoffs and stochastic law for every state and every joint action. -/
def tableValue (rows : List (List Rat)) (t : Nat) (s : State) : Rat :=
  (rows.getD t []).getD (stateIndex s) 0

def tableAction (rows : List (List Action)) (t : Nat) (s : State) : Action :=
  (rows.getD t []).getD (stateIndex s) 0

def W2Values : List (List Rat) := [
  [8,7,5,11,10,8,9,8,6,8,7,5,11,10,8,9,8,6],
  [6,5,3,8,7,5,11,10,8,6,5,3,8,7,5,11,10,8],
  [3,2,0,2,1,-1,5,4,2,3,2,0,2,1,-1,5,4,2],
  [0,-1,-1,-1,-2,-2,-1,-2,-2,0,-1,-1,-1,-2,-2,-1,-2,-2]]

def W2Actions : List (List Action) := [
  [96,144,144,0,48,48,0,48,48,96,144,144,0,48,48,0,48,48],
  [18,66,66,18,66,66,8,56,56,18,66,66,18,66,66,8,56,56],
  [18,18,18,18,18,18,8,8,8,18,18,18,18,18,18,8,8,8]]

def W2Upper : Nat → State → Rat := tableValue W2Values
def W2Choice : Nat → State → Action := tableAction W2Actions

theorem W2_certificate_checked : checkCertificate W2 3 W2Upper = true := by
  decide +kernel

theorem W2_policy_checked : checkPolicy W2 3 W2Choice = true := by
  decide +kernel

def W2Witness : Policy 3 := recommend W2 W2Choice 3 0 initial

theorem W2_witness_physical : Physical W2 3 0 initial W2Witness := by
  exact recommend_feasible W2 3 W2Choice
    (checked_policy_is_feasible W2 3 W2Choice W2_policy_checked) 3 0 (by decide) initial

theorem W2_witness_attains : evaluate W2 3 0 initial W2Witness = W2Upper 0 initial := by
  decide +kernel

theorem W2_globally_optimal : Physical W2 3 0 initial W2Witness ∧
    ∀ pi, Physical W2 3 0 initial pi →
      evaluate W2 3 0 initial pi ≤ evaluate W2 3 0 initial W2Witness := by
  exact attaining_certificate_is_globally_optimal W2 3 W2_valid W2Upper
    (checked_certificate_is_upper W2 3 W2Upper W2_certificate_checked)
    initial W2Witness W2_witness_physical W2_witness_attains

def W9bValues : List (List Rat) := [
  [(9/2),(7/2),(3/2),(15/2),(13/2),(9/2),(11/2),(9/2),(5/2),(9/2),(7/2),(3/2),(15/2),(13/2),(9/2),(11/2),(9/2),(5/2)],
  [0,-1,-3,-1,-2,-4,-3,-4,-6,6,5,3,8,7,5,11,10,8],
  [0,-1,-3,-1,-2,-4,-3,-4,-6,3,2,0,2,1,-1,5,4,2],
  [0,-1,-1,-1,-2,-2,-1,-2,-2,0,-1,-1,-1,-2,-2,-1,-2,-2]]

def W9bActions : List (List Action) := [
  [0,48,48,0,48,48,0,48,48,0,48,48,0,48,48,0,48,48],
  [0,48,48,96,144,144,96,144,144,18,66,66,18,66,66,8,56,56],
  [0,0,0,0,0,0,0,0,0,18,18,18,18,18,18,8,8,8]]

def W9bUpper : Nat → State → Rat := tableValue W9bValues
def W9bChoice : Nat → State → Action := tableAction W9bActions

theorem W9b_certificate_checked : checkCertificate W9b 3 W9bUpper = true := by
  decide +kernel

theorem W9b_policy_checked : checkPolicy W9b 3 W9bChoice = true := by
  decide +kernel

def W9bWitness : Policy 3 := recommend W9b W9bChoice 3 0 initial

theorem W9b_witness_physical : Physical W9b 3 0 initial W9bWitness := by
  exact recommend_feasible W9b 3 W9bChoice
    (checked_policy_is_feasible W9b 3 W9bChoice W9b_policy_checked) 3 0 (by decide) initial

theorem W9b_witness_attains : evaluate W9b 3 0 initial W9bWitness = W9bUpper 0 initial := by
  decide +kernel

theorem W9b_globally_optimal : Physical W9b 3 0 initial W9bWitness ∧
    ∀ pi, Physical W9b 3 0 initial pi →
      evaluate W9b 3 0 initial pi ≤ evaluate W9b 3 0 initial W9bWitness := by
  exact attaining_certificate_is_globally_optimal W9b 3 W9b_valid W9bUpper
    (checked_certificate_is_upper W9b 3 W9bUpper W9b_certificate_checked)
    initial W9bWitness W9b_witness_physical W9b_witness_attains

theorem W2_value : evaluate W2 3 0 initial W2Witness = 8 := by decide +kernel

theorem W9b_value : evaluate W9b 3 0 initial W9bWitness = 9/2 := by decide +kernel

/-- The threshold supports a second optimal physical policy. Its first action
    hires A; the table representative waits. Both remain causal thereafter. -/
def W9bHireChoice (t : Nat) (s : State) : Action :=
  if t=0 ∧ s=initial then 96 else W9bChoice t s

theorem W9b_hire_policy_checked : checkPolicy W9b 3 W9bHireChoice = true := by
  decide +kernel

def W9bHireWitness : Policy 3 := recommend W9b W9bHireChoice 3 0 initial

theorem W9b_hire_witness_physical : Physical W9b 3 0 initial W9bHireWitness := by
  exact recommend_feasible W9b 3 W9bHireChoice
    (checked_policy_is_feasible W9b 3 W9bHireChoice W9b_hire_policy_checked)
    3 0 (by decide) initial

theorem W9b_hire_witness_attains :
    evaluate W9b 3 0 initial W9bHireWitness = W9bUpper 0 initial := by decide +kernel

theorem W9b_hire_globally_optimal : Physical W9b 3 0 initial W9bHireWitness ∧
    ∀ pi, Physical W9b 3 0 initial pi →
      evaluate W9b 3 0 initial pi ≤ evaluate W9b 3 0 initial W9bHireWitness := by
  exact attaining_certificate_is_globally_optimal W9b 3 W9b_valid W9bUpper
    (checked_certificate_is_upper W9b 3 W9bUpper W9b_certificate_checked)
    initial W9bHireWitness W9b_hire_witness_physical W9b_hire_witness_attains

theorem W9b_distinct_optimal_root_choices :
    W9bChoice 0 initial = 0 ∧ W9bHireChoice 0 initial = 96 := by decide +kernel

theorem W9b_hire_value : evaluate W9b 3 0 initial W9bHireWitness = 9/2 := by
  decide +kernel

end WorkforcePlanning