WorkforceDevelopment.lean

import Std

namespace WorkforceDevelopment

/- Concrete finite delivery/development semantics.
   The actions are the complete physical product, not a preferred policy list.
   Concrete certificate tables were proposed after independent numerical checks.
   Public histories branch on qualification, employment retention and regime;
   no current action can inspect the outcome which follows it. -/

inductive Role where | A | B deriving DecidableEq, Repr
inductive Learner where | onlyA | training | qualified | departed deriving DecidableEq, Repr
inductive Hire where | absent | pending | active deriving DecidableEq, Repr
structure State where
  regime : Bool
  learner : Learner
  hire : Hire
  deriving DecidableEq, Repr
structure Outcome where
  passed : Bool
  retained : Bool
  high : Bool
  deriving DecidableEq, Repr

abbrev Action := Fin 288
def actions : List Action := List.finRange 288
def learners : List Learner := [.onlyA,.training,.qualified,.departed]
def hires : List Hire := [.absent,.pending,.active]
def states : List State := [false,true].flatMap (fun z =>
  learners.flatMap (fun l => hires.map (fun h => ⟨z,l,h⟩)))
def learnerIndex : Learner → Nat | .onlyA => 0 | .training => 1 | .qualified => 2 | .departed => 3
def hireIndex : Hire → Nat | .absent => 0 | .pending => 1 | .active => 2
def stateIndex (s : State) : Nat := 12*s.regime.toNat+3*learnerIndex s.learner+hireIndex s.hire

theorem state_enumeration_complete (s : State) : s ∈ states := by
  cases s with
  | mk z l h => cases z <;> cases l <;> cases h <;> decide +kernel
theorem action_enumeration_complete (a : Action) : a ∈ actions := by
  change a ∈ List.ofFn (fun i : Fin 288 => i)
  exact List.mem_ofFn.mpr ⟨a,rfl⟩

/- Exactly the JavaScript raw product order: training, management, borrow,
   mentor service, learner service, hired service, borrowed service.
   For qualified/departed learners the upper half is infeasible. -/
def session (a : Action) : Bool := decide (144 ≤ a.val)
def change (a : Action) : Bool := decide ((a.val / 72) % 2 = 1)
def borrow (a : Action) : Nat := (a.val / 24) % 3
def mentor (a : Action) : Bool := decide ((a.val / 12) % 2 = 1)
def learnerJob (a : Action) : Nat := (a.val / 4) % 3
def hired (a : Action) : Bool := decide ((a.val / 2) % 2 = 1)
def temporary (a : Action) : Bool := decide (a.val % 2 = 1)
def bit (b : Bool) : Rat := if b then 1 else 0
def served (a : Action) : Role → Nat
  | .A => (if learnerJob a = 1 then 1 else 0) +
      (if borrow a = 1 then (temporary a).toNat else 0)
  | .B => (mentor a).toNat+(hired a).toNat+
      (if learnerJob a = 2 then 1 else 0) +
      (if borrow a = 2 then (temporary a).toNat else 0)

structure Model where
  longTraining : Bool
  success : Rat
  fee : Rat
  longHire : Bool
  wage : Rat
  hireCost : Rat
  exitCost : Rat
  cancelCost : Rat
  value : Role → Rat
  outside : Role → Rat
  borrowCost : Role → Rat
  demand : Nat → Bool → Role → Nat
  mentorAvailable : Nat → Bool → Bool
  borrowAvailable : Nat → Bool → Role → Bool
  retention : Nat → Bool → Rat
  high : Nat → Bool → Rat

abbrev TrainFeasible (m : Model) (t : Nat) (s : State) (a : Action) : Prop :=
  session a = true →
    (s.learner = .onlyA ∨ s.learner = .training) ∧ m.mentorAvailable t s.regime = true
abbrev LearnerFeasible (s : State) (a : Action) : Prop :=
  (if learnerJob a = 0 then 0 else 1) ≤
    (if s.learner ≠ .departed ∧ session a = false then 1 else 0) ∧
  (learnerJob a = 2 → s.learner = .qualified)
abbrev BorrowFeasible (m : Model) (t : Nat) (s : State) (a : Action) : Prop :=
  (temporary a).toNat ≤ (if borrow a = 0 then 0 else 1) ∧
  (borrow a = 1 → m.borrowAvailable t s.regime .A = true) ∧
  (borrow a = 2 → m.borrowAvailable t s.regime .B = true)
abbrev FeasibleAction (m : Model) (t : Nat) (s : State) (a : Action) : Prop :=
  TrainFeasible m t s a ∧
  (mentor a).toNat ≤ (m.mentorAvailable t s.regime && !session a).toNat ∧
  LearnerFeasible s a ∧
  (hired a).toNat ≤ (if s.hire = .active then 1 else 0) ∧
  BorrowFeasible m t s a ∧
  served a .A ≤ m.demand t s.regime .A ∧ served a .B ≤ m.demand t s.regime .B
def allowed (m : Model) (t : Nat) (s : State) (a : Action) : Bool :=
  decide (FeasibleAction m t s a)

def complete (m : Model) (s : State) (a : Action) : Bool :=
  session a && (decide (s.learner = .training) || !m.longTraining)
def nextLearner (m : Model) (s : State) (a : Action) (o : Outcome) : Learner :=
  if s.learner = .departed ∨ o.retained = false then .departed
  else if session a then
    if complete m s a then (if o.passed then .qualified else .onlyA) else .training
  else if s.learner = .training then .onlyA else s.learner
def nextHire (m : Model) (s : State) (a : Action) : Hire :=
  match s.hire with
  | .absent => if change a then (if m.longHire then .pending else .active) else .absent
  | .pending => if change a then .absent else .active
  | .active => if change a then .absent else .active
def next (m : Model) (H t : Nat) (s : State) (a : Action) (o : Outcome) : State :=
  ⟨if t+1 < H then o.high else s.regime, nextLearner m s a o, nextHire m s a⟩

def managementCost (m : Model) (s : State) (a : Action) : Rat :=
  if change a then match s.hire with
    | .absent => m.hireCost
    | .pending => m.cancelCost
    | .active => m.exitCost
  else 0
def stage (m : Model) (s : State) (a : Action) : Rat :=
  (served a .A : Rat)*(m.value .A-m.outside .A) +
  (served a .B : Rat)*(m.value .B-m.outside .B) -
  bit (session a)*m.fee - (if s.hire = .active then m.wage else 0) -
  managementCost m s a -
  (if borrow a = 1 then m.borrowCost .A else if borrow a = 2 then m.borrowCost .B else 0)
def terminal (m : Model) (s : State) : Rat :=
  match s.hire with | .absent => 0 | .pending => -m.cancelCost | .active => -m.exitCost

def BernoulliValid (p : Rat) : Prop := 0 ≤ p ∧ p ≤ 1
structure Valid (m : Model) (H : Nat) : Prop where
  success : BernoulliValid m.success
  retention : ∀ t, t < H → ∀ z, BernoulliValid (m.retention t z)
  high : ∀ t, t < H → ∀ z, BernoulliValid (m.high t z)

def effectiveSuccess (m : Model) (s : State) (a : Action) : Rat :=
  if complete m s a then m.success else 0
def effectiveRetention (m : Model) (t : Nat) (s : State) : Rat :=
  if s.learner = .departed then 0 else m.retention t s.regime
def effectiveHigh (m : Model) (H t : Nat) (s : State) : Rat :=
  if t+1 < H then m.high t s.regime else bit s.regime
def coinExpected (p : Rat) (f : Bool → Rat) : Rat := (1-p)*f false+p*f true
def expected (m : Model) (H t : Nat) (s : State) (a : Action) (f : Outcome → Rat) : Rat :=
  coinExpected (effectiveSuccess m s a) (fun passed =>
  coinExpected (effectiveRetention m t s) (fun retained =>
  coinExpected (effectiveHigh m H t s) (fun high => f ⟨passed,retained,high⟩)))

/- The proof uses eight Boolean outcome labels with zero mass for an unused
   qualification/retention coin. JavaScript suppresses structurally inapplicable
   labels (`none`/null) and retains all zero-probability applicable outcomes.
   This is the same value law, not a proof of JavaScript event-count ledgers. -/

theorem effectiveSuccess_valid (m : Model) (H : Nat) (hv : Valid m H) (s : State) (a : Action) :
    BernoulliValid (effectiveSuccess m s a) := by
  unfold effectiveSuccess
  split
  · exact hv.success
  · constructor <;> decide
theorem effectiveRetention_valid (m : Model) (H : Nat) (hv : Valid m H)
    (t : Nat) (ht : t < H) (s : State) : BernoulliValid (effectiveRetention m t s) := by
  unfold effectiveRetention
  split
  · constructor <;> decide
  · exact hv.retention t ht s.regime
theorem effectiveHigh_valid (m : Model) (H : Nat) (hv : Valid m H)
    (t : Nat) (ht : t < H) (s : State) : BernoulliValid (effectiveHigh m H t s) := by
  unfold effectiveHigh
  split
  · exact hv.high t ht s.regime
  · cases s.regime <;> constructor <;> decide

theorem coinExpected_constant (p c : Rat) : coinExpected p (fun _ => c) = c := by
  simp [coinExpected]
  grind
theorem expected_normalized (m : Model) (H t : Nat) (s : State) (a : Action) :
    expected m H t s a (fun _ => 1) = 1 := by
  simp [expected, coinExpected_constant]
theorem coinExpected_mono (p : Rat) (hp : BernoulliValid p) (f g : Bool → Rat)
    (h : ∀ b, f b ≤ g b) : coinExpected p f ≤ coinExpected p g := by
  have hc : 0 ≤ 1-p := by obtain ⟨_,h⟩ := hp; 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.1
  simp only [coinExpected]
  grind
theorem expected_mono (m : Model) (H : Nat) (hv : Valid m H)
    (t : Nat) (ht : t < H) (s : State) (a : Action) (f g : Outcome → Rat)
    (h : ∀ o, f o ≤ g o) : expected m H t s a f ≤ expected m H t s a g := by
  apply coinExpected_mono _ (effectiveSuccess_valid m H hv s a)
  intro passed
  apply coinExpected_mono _ (effectiveRetention_valid m H hv t ht s)
  intro retained
  apply coinExpected_mono _ (effectiveHigh_valid m H hv t ht s)
  intro high
  exact h ⟨passed,retained,high⟩

inductive Policy : Nat → Type where
  | done : Policy 0
  | step {n : Nat} (action : Action) (continuation : Outcome → Policy n) : Policy (n+1)
def evaluate (m : Model) (H : Nat) : (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 H t s a (fun o => evaluate m H n (t+1) (next m H t s a o) (k o))
def Physical (m : Model) (H : Nat) : (n : Nat) → Nat → State → Policy n → Prop
  | 0, _, _, .done => True
  | n+1, t, s, .step a k => allowed m t s a = true ∧
      ∀ o, Physical m H n (t+1) (next m H t s a o) (k o)
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 H t s a (fun o => U (t+1) (next m H t s a o)) ≤ U t s

/-- This quantifies over history trees, not just the Markov table the solver stores. -/
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 H n t s pi) : evaluate m H 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 a
        (fun o => evaluate m H n (t+1) (next m H t s a o) (k o))
        (fun o => U (t+1) (next m H t s a o))
        (fun o => ih (t+1) (by omega) (next m H t s a o) (k o) (hk o))
      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 H t s a (fun o => U (t+1) (next m H t s a o)) ≤ 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) (H : Nat) (sigma : Nat → State → Action) : (n : Nat) → Nat → State → Policy n
  | 0, _, _ => .done
  | n+1, t, s => .step (sigma t s)
      (fun o => recommend m H sigma n (t+1) (next m H t s (sigma t s) o))
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 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 H n t s (recommend m H sigma n t s) := by
  induction n generalizing t s with
  | zero => trivial
  | succ n ih => exact ⟨hf t (by omega) s, fun o => ih (t+1) (by omega) _⟩
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 H 0 s witness)
    (he : evaluate m H H 0 s witness = U 0 s) :
    Physical m H H 0 s witness ∧ ∀ pi, Physical m H H 0 s pi →
      evaluate m H H 0 s pi ≤ evaluate m H 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

theorem training_excludes_mentor_delivery (m : Model) (t : Nat) (s : State) (a : Action)
    (ha : allowed m t s a = true) (hs : session a = true) : (mentor a).toNat = 0 := by
  have h : FeasibleAction m t s a := of_decide_eq_true ha
  have hm : (mentor a).toNat ≤ 0 := by simpa [hs] using h.2.1
  omega
theorem training_excludes_learner_delivery (m : Model) (t : Nat) (s : State) (a : Action)
    (ha : allowed m t s a = true) (hs : session a = true) : learnerJob a = 0 := by
  have h : FeasibleAction m t s a := of_decide_eq_true ha
  have hl : (if learnerJob a = 0 then 0 else 1) ≤ 0 := by
    simpa [hs] using h.2.2.1.1
  by_cases hz : learnerJob a = 0
  · exact hz
  · simp [hz] at hl
theorem learner_B_requires_preexisting_qualification (m : Model) (t : Nat) (s : State) (a : Action)
    (ha : allowed m t s a = true) (hb : learnerJob a = 2) : s.learner = .qualified := by
  have h : FeasibleAction m t s a := of_decide_eq_true ha
  exact h.2.2.1.2 hb
theorem service_respects_demand (m : Model) (t : Nat) (s : State) (a : Action)
    (ha : allowed m t s a = true) :
    served a .A ≤ m.demand t s.regime .A ∧ served a .B ≤ m.demand t s.regime .B := by
  have h : FeasibleAction m t s a := of_decide_eq_true ha
  exact h.2.2.2.2.2

theorem dual_skill_is_one_person : ∀ a : Action,
    (if learnerJob a = 1 then 1 else 0) + (if learnerJob a = 2 then 1 else 0) ≤ 1 := by
  decide +kernel
theorem only_one_external_contractor : ∀ a : Action,
    (if borrow a = 1 then 1 else 0) + (if borrow a = 2 then 1 else 0) ≤ 1 := by
  decide +kernel

/-- Remove only the training decision, keeping every current service,
    contractor reservation and external-position decision unchanged. -/
def eraseTraining (a : Action) : Action := ⟨a.val % 144, by
  have h := Nat.mod_lt a.val (by decide : 0 < 144)
  omega⟩

theorem eraseTraining_decoding : ∀ a : Action,
    session (eraseTraining a) = false ∧
    change (eraseTraining a) = change a ∧
    borrow (eraseTraining a) = borrow a ∧
    mentor (eraseTraining a) = mentor a ∧
    learnerJob (eraseTraining a) = learnerJob a ∧
    hired (eraseTraining a) = hired a ∧
    temporary (eraseTraining a) = temporary a := by
  decide +kernel

theorem eraseTraining_service (a : Action) (k : Role) :
    served (eraseTraining a) k = served a k := by
  obtain ⟨_,_,hb,hm,hl,hh,ht⟩ := eraseTraining_decoding a
  cases k <;> simp [served,hb,hm,hl,hh,ht]

theorem eraseTraining_preserves_feasibility (m : Model) (t : Nat) (s : State) (a : Action)
    (ha : allowed m t s a = true) : allowed m t s (eraseTraining a) = true := by
  have h : FeasibleAction m t s a := of_decide_eq_true ha
  obtain ⟨hs,hc,hb,hm,hl,hh,ht⟩ := eraseTraining_decoding a
  apply decide_eq_true
  change FeasibleAction m t s (eraseTraining a)
  refine ⟨?_,?_,?_,?_,?_,?_,?_⟩
  · intro bad
    simp [hs] at bad
  · rw [hm,hs]
    simp only [Bool.not_false, Bool.and_true]
    cases hsession : session a with
    | false => simpa [hsession] using h.2.1
    | true =>
      rw [training_excludes_mentor_delivery m t s a ha hsession]
      exact Nat.zero_le _
  · constructor
    · have old := h.2.2.1.1
      rw [hl,hs]
      by_cases hp : s.learner ≠ .departed
      · by_cases hj : learnerJob a = 0 <;> simp [hp,hj]
      · simpa [hp] using old
    · simpa [hl] using h.2.2.1.2
  · simpa [hh] using h.2.2.2.1
  · simpa [BorrowFeasible,hb,ht] using h.2.2.2.2.1
  · simpa [eraseTraining_service] using h.2.2.2.2.2.1
  · simpa [eraseTraining_service] using h.2.2.2.2.2.2

def finish (a : Action) : Policy 1 := .step a (fun _ => .done)
def nextSettlement (m : Model) (s : State) (a : Action) : Rat :=
  match nextHire m s a with | .absent => 0 | .pending => -m.cancelCost | .active => -m.exitCost

theorem finish_value (m : Model) (t : Nat) (s : State) (a : Action) :
    evaluate m (t+1) 1 t s (finish a) = stage m s a + nextSettlement m s a := by
  simp [evaluate,finish,terminal,next,nextSettlement,expected,coinExpected_constant]

theorem eraseTraining_nextSettlement (m : Model) (s : State) (a : Action) :
    nextSettlement m s (eraseTraining a) = nextSettlement m s a := by
  have hc := (eraseTraining_decoding a).2.1
  simp [nextSettlement,nextHire,hc]

theorem eraseTraining_stage (m : Model) (s : State) (a : Action) :
    stage m s (eraseTraining a) = stage m s a + bit (session a)*m.fee := by
  obtain ⟨hs,hc,hb,_,_,_,_⟩ := eraseTraining_decoding a
  simp [stage,eraseTraining_service,hs,bit,managementCost,hc,hb]
  grind

/-- With no terminal skill bonus, the last training session can only consume
    current slots and its nonnegative fee. External commitments are unchanged.
    Feasibility does not depend on the sign of job values: the erased action
    keeps exactly the same service allocation, allowing recovered slots idle. -/
theorem last_date_training_weakly_dominated (m : Model) (t : Nat) (s : State) (a : Action)
    (ha : allowed m t s a = true) (fee_nonnegative : 0 ≤ m.fee) :
    allowed m t s (eraseTraining a) = true ∧
    evaluate m (t+1) 1 t s (finish a) ≤
      evaluate m (t+1) 1 t s (finish (eraseTraining a)) := by
  refine ⟨eraseTraining_preserves_feasibility m t s a ha, ?_⟩
  rw [finish_value,finish_value,eraseTraining_stage,eraseTraining_nextSettlement]
  cases session a <;> simp [bit] <;> grind

def base : Model where
  longTraining := false
  success := 1
  fee := 1
  longHire := false
  wage := 2
  hireCost := 9
  exitCost := 1
  cancelCost := 1
  value := fun k => match k with | .A => 4 | .B => 8
  outside := fun _ => 0
  borrowCost := fun k => match k with | .A => 3 | .B => 7
  demand := fun t _ k => match k with | .A => if t=0 then 1 else 0 | .B => if t=0 then 1 else 2
  mentorAvailable := fun _ _ => true
  borrowAvailable := fun t _ _ => decide (t≠0)
  retention := fun _ _ => 1
  high := fun _ _ => 0
def J1 : Model := base
def J11 : Model := {base with success := 13/14}
def initial : State := ⟨false,.onlyA,.absent⟩
theorem J1_valid : Valid J1 3 := by
  constructor
  · change BernoulliValid (1 : Rat)
    constructor <;> decide +kernel
  · intro t ht z
    change BernoulliValid (1 : Rat)
    constructor <;> decide +kernel
  · intro t ht z
    change BernoulliValid (0 : Rat)
    constructor <;> decide +kernel
theorem J11_valid : Valid J11 3 := by
  constructor
  · change BernoulliValid (13/14 : Rat)
    constructor <;> decide +kernel
  · intro t ht z
    change BernoulliValid (1 : Rat)
    constructor <;> decide +kernel
  · intro t ht z
    change BernoulliValid (0 : Rat)
    constructor <;> decide +kernel

/- Tables proposed by the independently checked evaluator, exported by root
   after preregistration merge. They are not trusted axioms: kernel reduction
   must verify every admitted action in all24 states/date and each witness.
   Last-date dominance separately assumes nonnegative fee. -/
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 J1Values : List (List Rat) := [
  [31,39,37,31,39,37,44,43,41,26,35,33,31,39,37,31,39,37,44,43,41,26,35,33],
  [18,22,27,18,22,27,32,31,29,18,22,27,18,22,27,18,22,27,32,31,29,18,22,27],
  [9,8,13,9,8,13,16,15,13,9,8,13,9,8,13,9,8,13,16,15,13,9,8,13],
  [0,-1,-1,0,-1,-1,0,-1,-1,0,-1,-1,0,-1,-1,0,-1,-1,0,-1,-1,0,-1,-1]]
def J1Actions : List (List Action) := [
  [144,16,6,144,16,6,16,88,78,12,12,2,144,16,6,144,16,6,16,88,78,12,12,2],
  [61,61,14,61,61,14,20,92,82,61,61,14,61,61,14,61,61,14,20,92,82,61,61,14],
  [61,61,14,61,61,14,20,20,10,61,61,14,61,61,14,61,61,14,20,20,10,61,61,14]]
def J1Upper : Nat → State → Rat := tableValue J1Values
def J1Choice : Nat → State → Action := tableAction J1Actions
theorem J1_certificate_checked : checkCertificate J1 3 J1Upper = true := by decide +kernel
theorem J1_policy_checked : checkPolicy J1 3 J1Choice = true := by decide +kernel
def J1Witness : Policy 3 := recommend J1 3 J1Choice 3 0 initial
theorem J1_witness_physical : Physical J1 3 3 0 initial J1Witness := by
  exact recommend_feasible J1 3 J1Choice
    (checked_policy_is_feasible J1 3 J1Choice J1_policy_checked) 3 0 (by decide) initial
theorem J1_witness_attains : evaluate J1 3 3 0 initial J1Witness = J1Upper 0 initial := by
  decide +kernel
theorem J1_value : evaluate J1 3 3 0 initial J1Witness = 31 := by decide +kernel
theorem J1_globally_optimal : Physical J1 3 3 0 initial J1Witness ∧
    ∀ pi, Physical J1 3 3 0 initial pi →
      evaluate J1 3 3 0 initial pi ≤ evaluate J1 3 3 0 initial J1Witness := by
  exact attaining_certificate_is_globally_optimal J1 3 J1_valid J1Upper
    (checked_certificate_is_upper J1 3 J1Upper J1_certificate_checked)
    initial J1Witness J1_witness_physical J1_witness_attains

def J11Values : List (List Rat) := [
  [30,39,37,30,39,37,44,43,41,26,35,33,30,39,37,30,39,37,44,43,41,26,35,33],
  [18,22,27,18,22,27,32,31,29,18,22,27,18,22,27,18,22,27,32,31,29,18,22,27],
  [9,8,13,9,8,13,16,15,13,9,8,13,9,8,13,9,8,13,16,15,13,9,8,13],
  [0,-1,-1,0,-1,-1,0,-1,-1,0,-1,-1,0,-1,-1,0,-1,-1,0,-1,-1,0,-1,-1]]
def J11Actions : List (List Action) := [
  [16,16,6,16,16,6,16,88,78,12,12,2,16,16,6,16,16,6,16,88,78,12,12,2],
  [61,61,14,61,61,14,20,92,82,61,61,14,61,61,14,61,61,14,20,92,82,61,61,14],
  [61,61,14,61,61,14,20,20,10,61,61,14,61,61,14,61,61,14,20,20,10,61,61,14]]
def J11Upper : Nat → State → Rat := tableValue J11Values
def J11Choice : Nat → State → Action := tableAction J11Actions
def J11TrainChoice (t : Nat) (s : State) : Action :=
  if t=0 ∧ s=initial then 144 else J11Choice t s
def J11HireChoice (t : Nat) (s : State) : Action :=
  if t=0 ∧ s=initial then 88 else J11Choice t s
theorem J11_certificate_checked : checkCertificate J11 3 J11Upper = true := by decide +kernel
theorem J11_policy_checked : checkPolicy J11 3 J11Choice = true := by decide +kernel
theorem J11_train_policy_checked : checkPolicy J11 3 J11TrainChoice = true := by decide +kernel
theorem J11_hire_policy_checked : checkPolicy J11 3 J11HireChoice = true := by decide +kernel
def J11Witness : Policy 3 := recommend J11 3 J11Choice 3 0 initial
def J11TrainWitness : Policy 3 := recommend J11 3 J11TrainChoice 3 0 initial
def J11HireWitness : Policy 3 := recommend J11 3 J11HireChoice 3 0 initial
theorem J11_witness_physical : Physical J11 3 3 0 initial J11Witness := by
  exact recommend_feasible J11 3 J11Choice
    (checked_policy_is_feasible J11 3 J11Choice J11_policy_checked) 3 0 (by decide) initial
theorem J11_train_witness_physical : Physical J11 3 3 0 initial J11TrainWitness := by
  exact recommend_feasible J11 3 J11TrainChoice
    (checked_policy_is_feasible J11 3 J11TrainChoice J11_train_policy_checked) 3 0 (by decide) initial
theorem J11_hire_witness_physical : Physical J11 3 3 0 initial J11HireWitness := by
  exact recommend_feasible J11 3 J11HireChoice
    (checked_policy_is_feasible J11 3 J11HireChoice J11_hire_policy_checked) 3 0 (by decide) initial
theorem J11_witness_attains : evaluate J11 3 3 0 initial J11Witness = J11Upper 0 initial := by
  decide +kernel
theorem J11_train_witness_attains : evaluate J11 3 3 0 initial J11TrainWitness = J11Upper 0 initial := by
  decide +kernel
theorem J11_hire_witness_attains : evaluate J11 3 3 0 initial J11HireWitness = J11Upper 0 initial := by
  decide +kernel
theorem J11_three_equal_values :
    evaluate J11 3 3 0 initial J11Witness = 30 ∧
    evaluate J11 3 3 0 initial J11TrainWitness = 30 ∧
    evaluate J11 3 3 0 initial J11HireWitness = 30 := by decide +kernel
theorem J11_distinct_root_decisions :
    J11Choice 0 initial = 16 ∧ J11TrainChoice 0 initial = 144 ∧ J11HireChoice 0 initial = 88 := by
  decide +kernel
theorem J11_globally_optimal : Physical J11 3 3 0 initial J11Witness ∧
    ∀ pi, Physical J11 3 3 0 initial pi →
      evaluate J11 3 3 0 initial pi ≤ evaluate J11 3 3 0 initial J11Witness := by
  exact attaining_certificate_is_globally_optimal J11 3 J11_valid J11Upper
    (checked_certificate_is_upper J11 3 J11Upper J11_certificate_checked)
    initial J11Witness J11_witness_physical J11_witness_attains
theorem J11_train_globally_optimal : Physical J11 3 3 0 initial J11TrainWitness ∧
    ∀ pi, Physical J11 3 3 0 initial pi →
      evaluate J11 3 3 0 initial pi ≤ evaluate J11 3 3 0 initial J11TrainWitness := by
  exact attaining_certificate_is_globally_optimal J11 3 J11_valid J11Upper
    (checked_certificate_is_upper J11 3 J11Upper J11_certificate_checked)
    initial J11TrainWitness J11_train_witness_physical J11_train_witness_attains
theorem J11_hire_globally_optimal : Physical J11 3 3 0 initial J11HireWitness ∧
    ∀ pi, Physical J11 3 3 0 initial pi →
      evaluate J11 3 3 0 initial pi ≤ evaluate J11 3 3 0 initial J11HireWitness := by
  exact attaining_certificate_is_globally_optimal J11 3 J11_valid J11Upper
    (checked_certificate_is_upper J11 3 J11Upper J11_certificate_checked)
    initial J11HireWitness J11_hire_witness_physical J11_hire_witness_attains

end WorkforceDevelopment