PeopleDevelopment.lean

import Std

/- Task-specific apprenticeship: finite public-policy verification and exact
   hidden-state witnesses. Lean 4.24.0 / Std only. Learning and observation
   kernels are premises; authorization is an organizational rule. The concrete
   witnesses evaluate fixed curricula, not a claim of general curriculum
   optimality or empirical calibration. -/
namespace PeopleDevelopment

variable {S A O D : Type}

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

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

structure Model (S A O D : Type) where
  outcomes : List O
  actions : S → A → Prop
  terminals : S → D → Prop
  payoff : S → D → Rat
  next : S → A → O → S
  charge : S → A → Rat

inductive Policy (A O D : Type) : Nat → Type where
  | stop {n : Nat} (decision : D) : Policy A O D n
  | step {n : Nat} (action : A) (next : O → Policy A O D n) : Policy A O D (n+1)

def evaluate (m : Model S A O D) : (n : Nat) → S → Policy A O D n → Rat
  | 0, s, .stop d => m.payoff s d
  | _n+1, s, .stop d => m.payoff s d
  | n+1, s, .step a k =>
      -m.charge s a + sumOver m.outcomes (fun o => evaluate m n (m.next s a o) (k o))

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

/-- A local certificate covers every public-history policy, not just the
    policy used to propose the certificate. All branch masses live in S. -/
structure UpperCertificate (m : Model S A O D) (v : Nat → S → Rat) : Prop where
  terminal : ∀ n s d, m.terminals s d → m.payoff s d ≤ v n s
  step : ∀ n s a, m.actions s a →
    -m.charge s a + sumOver m.outcomes (fun o => v n (m.next s a o)) ≤ v (n+1) s

theorem certificate_bounds_every_policy (m : Model S A O D) (v : Nat → S → Rat)
    (cert : UpperCertificate m v) (n : Nat) (s : S) (p : Policy A O D n)
    (hp : Feasible m n s p) : evaluate m n s p ≤ v n s := by
  induction n generalizing s with
  | zero =>
    cases p with
    | stop d => exact cert.terminal 0 s d hp
  | succ n ih =>
    cases p with
    | stop d => exact cert.terminal (n+1) s d hp
    | step a k =>
      obtain ⟨ha, hk⟩ := hp
      have hs := sumOver_mono m.outcomes
        (fun o => evaluate m n (m.next s a o) (k o))
        (fun o => v n (m.next s a o))
        (fun o ho => ih (m.next s a o) (k o) (hk o ho))
      have hc := cert.step n s a ha
      simp only [evaluate]
      grind

theorem attained_certificate_is_optimal (m : Model S A O D) (v : Nat → S → Rat)
    (cert : UpperCertificate m v) (n : Nat) (s : S) (recommended : Policy A O D n)
    (hf : Feasible m n s recommended) (he : evaluate m n s recommended = v n s) :
    Feasible m n s recommended ∧ ∀ p, Feasible m n s p →
      evaluate m n s p ≤ evaluate m n s recommended := by
  refine ⟨hf, ?_⟩
  intro p hp
  rw [he]
  exact certificate_bounds_every_policy m v cert n s p hp

/-- An optional route preserves a feasible local policy without claiming that
    coordination itself changes its production technology. -/
theorem optional_route_preserves_local (localValue coordinated : Rat) :
    localValue ≤ (if localValue ≤ coordinated then coordinated else localValue) := by
  split <;> grind

/- Concrete four-world process. The exact witnesses use two actions, although
   the generic policy theorem above is valid for every finite horizon. -/
inductive Activity where
  | mentor | practice | scaffold | assess
  deriving DecidableEq, Repr
inductive Observation where
  | positive | negative | missing
  deriving DecidableEq, Repr
inductive Mode where
  | idle | independent | assisted
  deriving DecidableEq, Repr

abbrev World := Bool × Bool
abbrev Weights := World → Rat
abbrev Flags := Bool × Bool
abbrev Action := Activity × Bool

def worlds : List World := [(false,false),(true,false),(false,true),(true,true)]
def observations : List Observation := [.positive,.negative,.missing]
def skill (x : World) (second : Bool) : Bool := if second then x.2 else x.1
def change (x : World) (second value : Bool) : World :=
  if second then (x.1,value) else (value,x.2)

structure Environment where
  demand : Nat
  expert : Bool
  tool : Bool
  first : Bool
  second : Bool
  deriving DecidableEq, Repr
structure Assignment where
  expert : Bool
  first : Mode
  second : Mode
  deriving DecidableEq, Repr
abbrev Decision := Environment → Assignment

structure Configuration where
  mentorLearning : Rat := 3/4
  scaffoldLearning : Rat := 1/4
  sensitivity : Rat := 3/4
  falsePositive : Rat := 1/4
  retention : Rat := 1
  gate : Bool := true
  budget : Nat := 3
  environments : List (Rat × Environment)

structure State where
  weights : Weights
  authorization : Flags
  budget : Nat

def learning (c : Configuration) : Activity → Rat
  | .mentor => c.mentorLearning
  | .practice => 1/2
  | .scaffold => c.scaffoldLearning
  | .assess => 0

def units : Activity → Nat
  | .mentor => 2
  | .assess => 1
  | _ => 0

def cost : Activity → Rat
  | .mentor => 1
  | .practice => 1/2
  | .scaffold => 1/4
  | .assess => 1/4

/-- Concrete learning retains existing skill; the JS interface additionally
    supports activity-specific negative-transfer probabilities. -/
def targetCompetence (c : Configuration) (a : Activity) (old : Bool) : Rat :=
  if old then 1 else learning c a

def transition (c : Configuration) (a : Action) (x y : World) : Rat :=
  if change x a.2 (skill y a.2) = y then
    if skill y a.2 then targetCompetence c a.1 (skill x a.2)
    else 1 - targetCompetence c a.1 (skill x a.2)
  else 0

def likelihood (c : Configuration) (a : Activity) (competent : Bool) : Observation → Rat
  | .missing => 0
  | .positive => if a = .assess then (if competent then c.sensitivity else c.falsePositive) else 1
  | .negative => if a = .assess then 1 - (if competent then c.sensitivity else c.falsePositive) else 0

def childWeights (c : Configuration) (w : Weights) (a : Action) (o : Observation) : Weights :=
  fun y => likelihood c a.1 (skill y a.2) o * sumOver worlds (fun x => w x * transition c a x y)

def childFlags (g : Flags) (a : Action) (o : Observation) : Flags :=
  change g a.2 (decide (a.1 = .assess ∧ o = .positive))

def initial (c : Configuration) : State :=
  { weights := fun x => if x = (false,false) then 1 else 0
    authorization := (false,false), budget := c.budget }

def next (c : Configuration) (s : State) (a : Action) (o : Observation) : State :=
  { weights := childWeights c s.weights a o
    authorization := childFlags s.authorization a o
    budget := s.budget - units a.1 }

def jobs (a : Assignment) : Nat :=
  (if a.expert then 1 else 0) + (if a.first = .idle then 0 else 1) + (if a.second = .idle then 0 else 1)

def learnerAllowed (c : Configuration) (authorized available tool : Bool) (m : Mode) : Prop :=
  m = .idle ∨ (available = true ∧ (m = .independent → c.gate = false ∨ authorized = true) ∧
    (m = .assisted → tool = true))
instance (c : Configuration) (authorized available tool : Bool) (m : Mode) :
    Decidable (learnerAllowed c authorized available tool m) := by unfold learnerAllowed; infer_instance

def allowed (c : Configuration) (g : Flags) (e : Environment) (a : Assignment) : Prop :=
  jobs a ≤ e.demand ∧ (a.expert = true → e.expert = true) ∧
  learnerAllowed c g.1 e.first e.tool a.first ∧ learnerAllowed c g.2 e.second e.tool a.second
instance (c : Configuration) (g : Flags) (e : Environment) (a : Assignment) :
    Decidable (allowed c g e a) := by unfold allowed; infer_instance

def learnerReward (c : Configuration) (competent : Bool) : Mode → Rat
  | .idle => 0
  | .assisted => 4
  | .independent => if competent then c.retention * 8 + (1-c.retention) * (-24) else -24

def reward (c : Configuration) (x : World) (a : Assignment) : Rat :=
  (if a.expert then 8 else 0) + learnerReward c x.1 a.first + learnerReward c x.2 a.second

def terminalValue (c : Configuration) (s : State) (d : Decision) : Rat :=
  sumOver c.environments (fun pe => pe.1 * sumOver worlds (fun x => s.weights x * reward c x (d pe.2)))

def concreteModel (c : Configuration) : Model State Action Observation Decision where
  outcomes := observations
  actions := fun s a => units a.1 ≤ s.budget
  terminals := fun s d => ∀ pe ∈ c.environments, allowed c s.authorization pe.2 (d pe.2)
  payoff := terminalValue c
  next := next c
  charge := fun s a => sumOver worlds s.weights * cost a.1

/-- These are conditional structural properties, not a claim that tests have
    no false positives. They hold independently of the learning probabilities. -/
theorem authorized_target_iff_assessment_pass (g : Flags) (a : Action) (o : Observation) :
    skill (childFlags g a o) a.2 = true ↔ a.1 = .assess ∧ o = .positive := by
  rcases a with ⟨a, second⟩
  cases second <;> simp [childFlags, change, skill]

theorem missing_revokes (g : Flags) (a : Action) :
    skill (childFlags g a .missing) a.2 = false := by
  rcases a with ⟨a, second⟩
  cases a <;> cases second <;> simp [childFlags, change, skill]

theorem capacity_of_allowed (c : Configuration) (g : Flags) (e : Environment) (a : Assignment)
    (h : allowed c g e a) : jobs a ≤ e.demand := h.1

theorem budget_conservation (c : Configuration) (s : State) (a : Action) (o : Observation)
    (h : (concreteModel c).actions s a) : units a.1 + (next c s a o).budget = s.budget := by
  change units a.1 ≤ s.budget at h
  simp only [next]
  omega

/-- No observation about the other learner is discarded: this kernel sums
    full joint-world weights, permitting correlated priors. -/
theorem uninformative_completion (c : Configuration) (w : Weights) (a : Action)
    (ha : a.1 ≠ .assess) (y : World) :
    childWeights c w a .positive y = sumOver worlds (fun x => w x * transition c a x y) := by
  simp [childWeights, likelihood, ha]


/-- Both concrete kernels have total mass one before multiplying parent mass. -/
theorem observation_rows_normalized (c : Configuration) (a : Activity) (s : Bool) :
    sumOver observations (likelihood c a s) = 1 := by
  cases a <;> cases s <;> simp [observations, sumOver, likelihood] <;> grind

theorem transition_rows_normalized (c : Configuration) (a : Action) (x : World) :
    sumOver worlds (transition c a x) = 1 := by
  rcases a with ⟨a, i⟩
  rcases x with ⟨f, s⟩
  cases a <;> cases i <;> cases f <;> cases s <;>
    simp [worlds, sumOver, transition, targetCompetence, learning, skill, change] <;> grind

/-- The complete joint transition-and-observation filter conserves mass.
    This identity does not replace the separate nonnegativity assumptions
    required when interpreting the weights as probabilities. -/
theorem joint_filter_mass_conservation (c : Configuration) (w : Weights) (a : Action) :
    sumOver observations (fun o => sumOver worlds (childWeights c w a o)) = sumOver worlds w := by
  rcases a with ⟨a, i⟩
  cases a <;> cases i <;>
    simp [observations, worlds, sumOver, childWeights, likelihood, transition,
      targetCompetence, learning, change, skill] <;> grind

def normal : Environment := ⟨2,true,false,true,true⟩
def base : Configuration := { environments := [(1,normal)] }

def dispatch (deploy : Bool) (e : Environment) : Assignment :=
  let useExpert := e.expert && decide (0 < e.demand)
  let room := decide ((if useExpert then 1 else 0) < e.demand)
  { expert := useExpert
    first := if e.first && room then (if deploy then .independent else if e.tool then .assisted else .idle) else .idle
    second := .idle }

def mentorAssessment (deploy : Bool) : Policy Action Observation Decision 2 :=
  .step (.mentor,false) (fun o => match o with
    | .positive => .step (.assess,false) (fun q =>
        .stop (dispatch (deploy && decide (q = .positive))))
    | _ => .stop (dispatch false))

def scaffoldAssessment : Policy Action Observation Decision 2 :=
  .step (.scaffold,false) (fun o => match o with
    | .positive => .step (.assess,false) (fun q => .stop (dispatch (decide (q = .positive))))
    | _ => .stop (dispatch false))

def mentorPractice : Policy Action Observation Decision 2 :=
  .step (.mentor,false) (fun o => match o with
    | .positive => .step (.practice,false) (fun q => .stop (dispatch (decide (q = .positive))))
    | _ => .stop (dispatch false))

def fixedValue (c : Configuration) (p : Policy Action Observation Decision 2) : Rat :=
  evaluate (concreteModel c) 2 (initial c) p

def stopValue (c : Configuration) : Rat := fixedValue c (.stop (dispatch false))

def passState (c : Configuration) : State :=
  next c (next c (initial c) (.mentor,false) .positive) (.assess,false) .positive

theorem favorable_true_positive_mass : (passState base).weights (true,false) = 9/16 := by decide +kernel
theorem favorable_false_positive_mass : (passState base).weights (false,false) = 1/16 := by decide +kernel
theorem favorable_pass_mass : sumOver worlds (passState base).weights = 5/8 := by decide +kernel
theorem favorable_fixed_curriculum : fixedValue base (mentorAssessment true) = 39/4 := by decide +kernel
theorem favorable_stop : stopValue base = 8 := by decide +kernel
theorem favorable_gain : stopValue base < fixedValue base (mentorAssessment true) := by decide +kernel

def oneJob : Configuration := { base with environments := [(1,{ normal with demand := 1 })] }
theorem one_job_fixed_curriculum_loss : fixedValue oneJob (mentorAssessment true) = 27/4 := by decide +kernel
theorem one_job_stop : stopValue oneJob = 8 := by decide +kernel

def independentAbsence : Configuration := { base with environments :=
  [(1/2,{normal with demand := 1}),(1/2,{normal with demand := 1, expert := false})] }
theorem independent_absence_value : fixedValue independentAbsence (mentorAssessment true) = 17/4 := by decide +kernel

def commonAbsence : Configuration := { base with environments :=
  [(1/2,{normal with demand := 1}),(1/2,⟨1,false,false,false,false⟩)] }
theorem common_absence_fixed_loss : fixedValue commonAbsence (mentorAssessment true) = 11/4 := by decide +kernel
theorem common_absence_stop : stopValue commonAbsence = 4 := by decide +kernel

def scarce : Configuration := { base with budget := 2 }
theorem mentor_then_assessment_exceeds_scarce_budget :
    ¬ (concreteModel scarce).actions (next scarce (initial scarce) (.mentor,false) .positive) (.assess,false) := by
  change ¬ (1 ≤ (0 : Nat))
  decide +kernel

def guardedScaffold : Configuration := { scarce with scaffoldLearning := 3/4 }
theorem guarded_scaffold_value : fixedValue guardedScaffold scaffoldAssessment = 21/2 := by decide +kernel

def reliableAI : Configuration := { base with environments := [(1,{normal with tool := true})] }
theorem reliable_AI_stop : stopValue reliableAI = 12 := by decide +kernel
theorem reliable_AI_curriculum_loss : fixedValue reliableAI (mentorAssessment true) = 45/4 := by decide +kernel

def AIOutages : Configuration := { base with environments := [(1/2,normal),(1/2,{normal with tool := true})] }
theorem AI_outages_curriculum : fixedValue AIOutages (mentorAssessment true) = 21/2 := by decide +kernel
theorem AI_outages_stop : stopValue AIOutages = 10 := by decide +kernel

def weakMentor : Configuration := { base with mentorLearning := 1/2 }
theorem weak_mentor_refused_deployment : fixedValue weakMentor (mentorAssessment false) = 27/4 := by decide +kernel

def forgetting : Configuration := { base with retention := 2/3 }
theorem forgetting_refused_deployment : fixedValue forgetting (mentorAssessment false) = 27/4 := by decide +kernel
theorem forgetting_frozen_policy_loss : fixedValue forgetting (mentorAssessment true) = 15/4 := by decide +kernel
theorem forgetting_stop_beats_frozen_policy : fixedValue forgetting (mentorAssessment true) < stopValue forgetting := by decide +kernel

def noisyAssessment : Configuration := { base with falsePositive := 1/2 }
theorem noisy_assessment_value : fixedValue noisyAssessment (mentorAssessment true) = 33/4 := by decide +kernel
theorem noisy_assessment_false_positive_mass : (passState noisyAssessment).weights (false,false) = 1/8 := by decide +kernel

def uninformativeAssessment : Configuration := { base with falsePositive := 3/4 }
theorem uninformative_assessment_refused_deployment : fixedValue uninformativeAssessment (mentorAssessment false) = 27/4 := by decide +kernel

def noGate : Configuration := { base with gate := false }
theorem ungated_practice_value : fixedValue noGate mentorPractice = 21/2 := by decide +kernel
theorem ungated_practice_exceeds_gated_witness : fixedValue base (mentorAssessment true) < fixedValue noGate mentorPractice := by decide +kernel

def afterMentorPractice (c : Configuration) : State :=
  next c (next c (initial c) (.mentor,false) .positive) (.practice,false) .positive

theorem ungated_bad_assignment_mass : (afterMentorPractice noGate).weights (false,false) = 1/8 := by decide +kernel

theorem identical_local_value : fixedValue base (mentorAssessment true) = 39/4 := favorable_fixed_curriculum

def mandatoryValue (c : Configuration) (fee : Rat) (p : Policy Action Observation Decision 2) : Rat := fixedValue c p - fee

theorem mandatory_fee_loss : mandatoryValue base 2 (mentorAssessment true) = 31/4 := by decide +kernel
theorem mandatory_fee_below_untrained_local : mandatoryValue base 2 (mentorAssessment true) < stopValue base := by decide +kernel


/-- The favorable numerical witness is a feasible complete policy, including
    all missing and zero-probability branches. -/
theorem favorable_policy_feasible :
    Feasible (concreteModel base) 2 (initial base) (mentorAssessment true) := by
  constructor
  · change (2 : Nat) ≤ 3
    decide +kernel
  · intro o _ho
    cases o with
    | positive =>
      constructor
      · change (1 : Nat) ≤ 1
        decide +kernel
      · intro q _hq
        cases q <;> simp [Feasible, concreteModel, base, normal, initial, next,
          childFlags, change, dispatch, allowed, learnerAllowed, jobs]
    | negative =>
      simp [Feasible, concreteModel, base, normal, initial, next,
        childFlags, change, dispatch, allowed, learnerAllowed, jobs]
    | missing =>
      simp [Feasible, concreteModel, base, normal, initial, next,
        childFlags, change, dispatch, allowed, learnerAllowed, jobs]

/-- The ungated opportunity-cost witness obeys the same physical budget. -/
theorem ungated_policy_feasible :
    Feasible (concreteModel noGate) 2 (initial noGate) mentorPractice := by
  constructor
  · change (2 : Nat) ≤ 3
    decide +kernel
  · intro o _ho
    cases o with
    | positive =>
      constructor
      · change (0 : Nat) ≤ 1
        decide +kernel
      · intro q _hq
        cases q <;> simp [Feasible, concreteModel, noGate, base, normal, initial, next,
          childFlags, change, dispatch, allowed, learnerAllowed, jobs]
    | negative =>
      simp [Feasible, concreteModel, noGate, base, normal, initial, next,
        childFlags, change, dispatch, allowed, learnerAllowed, jobs]
    | missing =>
      simp [Feasible, concreteModel, noGate, base, normal, initial, next,
        childFlags, change, dispatch, allowed, learnerAllowed, jobs]

/-- Symbolic identities are linked to the actual transition/filter/assignment
    evaluator. Valid probability inputs are required for their economic use. -/
theorem concrete_learning_value (l : Rat) :
    fixedValue {base with mentorLearning := l} (mentorAssessment true) = 3/4 + 12*l := by
  simp [fixedValue, evaluate, concreteModel, mentorAssessment, base, initial, next,
    terminalValue, sumOver, worlds, observations, childWeights, likelihood,
    transition, targetCompetence, learning, change, skill, dispatch, normal, cost, learnerReward, reward]
  <;> grind

theorem concrete_learning_threshold (l : Rat) :
    8 < fixedValue {base with mentorLearning := l} (mentorAssessment true) ↔ 29/48 < l := by
  rw [concrete_learning_value]
  have hc : (3/4 : Rat) + 12*(29/48) = 8 := by decide +kernel
  grind

theorem concrete_retention_value (r : Rat) :
    fixedValue {base with retention := r} (mentorAssessment true) = 18*r-33/4 := by
  simp [fixedValue, evaluate, concreteModel, mentorAssessment, base, initial, next,
    terminalValue, sumOver, worlds, observations, childWeights, likelihood,
    transition, targetCompetence, learning, change, skill, dispatch, normal, cost, learnerReward, reward]
  <;> grind

theorem concrete_retention_threshold (r : Rat) :
    8 < fixedValue {base with retention := r} (mentorAssessment true) ↔ 65/72 < r := by
  rw [concrete_retention_value]
  have hc : 18*(65/72 : Rat)-33/4 = 8 := by decide +kernel
  grind

end PeopleDevelopment