AssessmentLearning.lean

import Std

/- Finite diagnostic-memory benchmark. Pinned Lean 4.24.0.
   Conditional mathematical results; no empirical learning guarantee. -/
namespace AssessmentLearning

/-- Observable signatures. Names reflect the hidden world labelling only;
    the assessor does not receive `truth` as an input to its decision. -/
inductive Signature where
  | aH | bH | aL | bL
  deriving DecidableEq

def truth : Signature → Bool
  | .aH | .bH => true
  | .aL | .bL => false

def Memory := Signature → Option Bool

def emptyMemory : Memory := fun _ => none

inductive Source where
  | reviewedPitch | failedExperiment
  deriving DecidableEq

structure Evidence where
  signature : Signature
  label : Option Bool
  source : Source
  reviewed : Bool
  validated : Bool
  diagnosed : Bool

/-- Operational admission, not a proof that the label generalizes. A diagnosed
    failed experiment may produce either label, including `some true`. -/
def admitted (e : Evidence) : Bool :=
  e.reviewed && e.validated &&
    (e.source == .reviewedPitch || e.diagnosed)

def update (m : Memory) (e : Evidence) : Memory :=
  if admitted e then
    match e.label with
    | none => m
    | some b => fun s => if s = e.signature then some b else m s
  else m

def learn (m : Memory) : List Evidence → Memory
  | [] => m
  | e :: es => learn (update m e) es

/-- Access is decided before folding the chronological record history, so an
    inaccessible newer record cannot overwrite an accessible older record. -/
def learnAccessible (m : Memory) (access : Evidence → Bool) (es : List Evidence) : Memory :=
  learn m (es.filter access)

theorem inaccessible_record_ignored (m : Memory) (access : Evidence → Bool)
    (e : Evidence) (es : List Evidence) (h : access e = false) :
    learnAccessible m access (e :: es) = learnAccessible m access es := by
  simp [learnAccessible, h]

/-- Availability is retrieval-time currency/retention and context eligibility.
    Record access and paid transfer permission belong to learnAccessible. -/
def available (m : Memory) (usable : Signature → Bool) : Memory :=
  fun s => if usable s then m s else none

def bit : Bool → Rat
  | false => 0
  | true => 1

def score (base : Rat) (m : Memory) (s : Signature) : Rat :=
  match m s with
  | none => base
  | some b => bit b

def coverage (m : Memory) (s : Signature) : Rat :=
  match m s with
  | none => 0
  | some _ => 1

/-- Strong held-out stability/realizability assumption. Operational validation
    alone does not establish this condition for future transferred cases. -/
def SoundMemory (m : Memory) : Prop :=
  ∀ s b, m s = some b → b = truth s

theorem no_label_no_update (m : Memory) (e : Evidence)
    (h : e.label = none) : update m e = m := by
  simp [update, h]

theorem unreviewed_no_update (m : Memory) (e : Evidence)
    (h : e.reviewed = false) : update m e = m := by
  simp [update, admitted, h]

theorem unvalidated_no_update (m : Memory) (e : Evidence)
    (h : e.validated = false) : update m e = m := by
  simp [update, admitted, h]

theorem undiagnosed_failure_no_update (m : Memory) (e : Evidence)
    (hs : e.source = .failedExperiment) (hd : e.diagnosed = false) :
    update m e = m := by
  simp [update, admitted, hs, hd]

theorem repeated_case_idempotent (m : Memory) (e : Evidence) :
    update (update m e) e = update m e := by
  funext s
  by_cases ha : admitted e = true
  · cases hl : e.label with
    | none => simp [update, ha, hl]
    | some b => by_cases h : s = e.signature <;> simp [update, ha, hl, h]
  · simp [update, ha]

theorem update_other_signature (m : Memory) (e : Evidence) (s : Signature)
    (h : s ≠ e.signature) : update m e s = m s := by
  by_cases ha : admitted e = true
  · cases hl : e.label <;> simp [update, ha, hl, h]
  · simp [update, ha]

/-- No observations at a signature means no learned record there. In the
    high-only entry regime this applies to low-type signatures unless another
    paid feedback source supplies them. -/
theorem unseen_signature_unchanged (m : Memory) (es : List Evidence) (s : Signature)
    (h : ∀ e, e ∈ es → s ≠ e.signature) : learn m es s = m s := by
  induction es generalizing m with
  | nil => rfl
  | cons e rest ih =>
    have he : s ≠ e.signature := h e (by simp)
    have hr : ∀ r, r ∈ rest → s ≠ r.signature := by
      intro r hm
      exact h r (by simp [hm])
    change learn (update m e) rest s = m s
    rw [ih (update m e) hr, update_other_signature m e s he]

theorem unavailable_case_is_baseline (base : Rat) (m : Memory)
    (usable : Signature → Bool) (s : Signature) (h : usable s = false) :
    score base (available m usable) s = base := by
  simp [score, available, h]

theorem same_records_same_assessment (base : Rat) (m n : Memory)
    (h : ∀ s, m s = n s) (s : Signature) : score base m s = score base n s := by
  simp [score, h]

theorem sound_available (m : Memory) (usable : Signature → Bool)
    (hs : SoundMemory m) : SoundMemory (available m usable) := by
  intro s b hb
  cases hu : usable s with
  | false => simp [available, hu] at hb
  | true =>
    have hm : m s = some b := by simpa [available, hu] using hb
    exact hs s b hm

/-- A verified record preserves soundness only if its label matches the future
    regime's truth; the operational Boolean `validated` does not supply this. -/
theorem sound_update (m : Memory) (e : Evidence) (hs : SoundMemory m)
    (he : ∀ b, e.label = some b → b = truth e.signature) :
    SoundMemory (update m e) := by
  intro s b hb
  by_cases ha : admitted e = true
  · cases hl : e.label with
    | none =>
      have hm : m s = some b := by simpa [update, ha, hl] using hb
      exact hs s b hm
    | some v =>
      by_cases hsig : s = e.signature
      · have hv := he v hl
        have hsame : some v = some b := by simpa [update, ha, hl, hsig] using hb
        have hvb : v = b := Option.some.inj hsame
        grind
      · have hm : m s = some b := by simpa [update, ha, hl, hsig] using hb
        exact hs s b hm
  · have hm : m s = some b := by simpa [update, ha] using hb
    exact hs s b hm

/-- Exact per-signature correction under the declared stability assumption. -/
theorem sound_score_correction (base : Rat) (m : Memory) (s : Signature)
    (hs : SoundMemory m) :
    score base m s - base = coverage m s * (bit (truth s) - base) := by
  cases hm : m s with
  | none => simp [score, coverage, hm]; grind
  | some b =>
    have hb := hs s b hm
    simp [score, coverage, hm, hb]

def weightedRate (base : Rat) (m : Memory) : List (Rat × Signature) → Rat
  | [] => 0
  | (w,s) :: rest => w * score base m s + weightedRate base m rest

def weightedCorrection (base : Rat) (m : Memory) : List (Rat × Signature) → Rat
  | [] => 0
  | (w,s) :: rest =>
    w * coverage m s * (bit (truth s) - base) + weightedCorrection base m rest

/-- General finite-sum identity. Probability interpretation additionally needs
    nonnegative weights summing to one, fixed held-out weights, and soundness. -/
theorem finite_learning_gain (base : Rat) (m : Memory)
    (cells : List (Rat × Signature)) (hs : SoundMemory m) :
    weightedRate base m cells - weightedRate base emptyMemory cells =
      weightedCorrection base m cells := by
  induction cells with
  | nil => simp [weightedRate, weightedCorrection]; grind
  | cons cell rest ih =>
    rcases cell with ⟨w,s⟩
    have hc := sound_score_correction base m s hs
    simp only [weightedRate, weightedCorrection]
    have he : score base emptyMemory s = base := rfl
    rw [he]
    grind

/-- Matched comparison subtracts local learning, rather than calling it zero. -/
theorem matched_learning_gain (base : Rat) (m n : Memory)
    (cells : List (Rat × Signature)) (hm : SoundMemory m) (hn : SoundMemory n) :
    weightedRate base m cells - weightedRate base n cells =
      weightedCorrection base m cells - weightedCorrection base n cells := by
  have h1 := finite_learning_gain base m cells hm
  have h2 := finite_learning_gain base n cells hn
  grind

/-- Fixed conditional held-out masses: one half on each of two signatures. -/
def pHigh (base : Rat) (m : Memory) : Rat :=
  (score base m .aH + score base m .bH) / 2

def pLow (base : Rat) (m : Memory) : Rat :=
  (score base m .aL + score base m .bL) / 2

def highCoverage (m : Memory) : Rat := (coverage m .aH + coverage m .bH)/2
def lowCoverage (m : Memory) : Rat := (coverage m .aL + coverage m .bL)/2

theorem sensitivity_from_coverage (base : Rat) (m : Memory) (hs : SoundMemory m) :
    pHigh base m = base + (1-base)*highCoverage m := by
  have h1 := sound_score_correction base m .aH hs
  have h2 := sound_score_correction base m .bH hs
  simp only [truth, bit] at h1 h2
  unfold pHigh highCoverage
  grind

theorem false_positive_from_coverage (base : Rat) (m : Memory) (hs : SoundMemory m) :
    pLow base m = base * (1-lowCoverage m) := by
  have h1 := sound_score_correction base m .aL hs
  have h2 := sound_score_correction base m .bL hs
  simp only [truth, bit] at h1 h2
  unfold pLow lowCoverage
  grind

/-- Private signature, not merely H/L, is the entry information set. -/
structure Strategy where
  aH : Bool
  bH : Bool
  aL : Bool
  bL : Bool
  deriving DecidableEq

def enters (e : Strategy) : Signature → Bool
  | .aH => e.aH
  | .bH => e.bH
  | .aL => e.aL
  | .bL => e.bL

def mass (pi : Rat) : Signature → Rat
  | .aH | .bH => pi/2
  | .aL | .bL => (1-pi)/2

def sumSignatures (f : Signature → Rat) : Rat :=
  f .aH + f .bH + f .aL + f .bL

def entryMass (pi : Rat) (e : Strategy) : Rat :=
  sumSignatures (fun s => mass pi s * bit (enters e s))

def passMass (pi base : Rat) (m : Memory) (e : Strategy) : Rat :=
  sumSignatures (fun s => mass pi s * bit (enters e s) * score base m s)

def passValue (pi base highValue lowValue : Rat) (m : Memory) (e : Strategy) : Rat :=
  sumSignatures (fun s => mass pi s * bit (enters e s) * score base m s *
    (if truth s then highValue else lowValue))

/-- Own pass and rival fail wins; two passes split one award fairly. -/
def award (ownPass rivalPass : Rat) : Rat :=
  ownPass*(1-rivalPass) + ownPass*rivalPass/2

theorem conditional_award (ownPass rivalPass : Rat) :
    award ownPass rivalPass = ownPass*(1-rivalPass/2) := by
  unfold award
  grind

def entryUtility (pi base benefit burden : Rat) (m : Memory) (e : Strategy)
    (s : Signature) : Rat :=
  benefit*award (score base m s) (passMass pi base m e)-burden

def strictAt (enter : Bool) (u : Rat) : Prop := if enter then 0 < u else u < 0

def weakAt (enter : Bool) (u : Rat) : Prop := if enter then 0 ≤ u else u ≤ 0

def strictEquilibrium (pi base benefit burden : Rat) (m : Memory) (e : Strategy) : Prop :=
  strictAt e.aH (entryUtility pi base benefit burden m e .aH) ∧
  strictAt e.bH (entryUtility pi base benefit burden m e .bH) ∧
  strictAt e.aL (entryUtility pi base benefit burden m e .aL) ∧
  strictAt e.bL (entryUtility pi base benefit burden m e .bL)

def weakEquilibrium (pi base benefit burden : Rat) (m : Memory) (e : Strategy) : Prop :=
  weakAt e.aH (entryUtility pi base benefit burden m e .aH) ∧
  weakAt e.bH (entryUtility pi base benefit burden m e .bH) ∧
  weakAt e.aL (entryUtility pi base benefit burden m e .aL) ∧
  weakAt e.bL (entryUtility pi base benefit burden m e .bL)

/-- Four signatures give 16 symmetric pure entry candidates. Weak inequalities
    retain ties; enumeration does not search asymmetric or mixed equilibria. -/
def allStrategies : List Strategy :=
  [⟨false,false,false,false⟩, ⟨false,false,false,true⟩,
   ⟨false,false,true,false⟩, ⟨false,false,true,true⟩,
   ⟨false,true,false,false⟩, ⟨false,true,false,true⟩,
   ⟨false,true,true,false⟩, ⟨false,true,true,true⟩,
   ⟨true,false,false,false⟩, ⟨true,false,false,true⟩,
   ⟨true,false,true,false⟩, ⟨true,false,true,true⟩,
   ⟨true,true,false,false⟩, ⟨true,true,false,true⟩,
   ⟨true,true,true,false⟩, ⟨true,true,true,true⟩]

theorem all_symmetric_pure_strategies_listed (e : Strategy) : e ∈ allStrategies := by
  cases e with
  | mk a b c d => cases a <;> cases b <;> cases c <;> cases d <;> decide

/-- Enumerated first winner and second winner expectations under independent
    signature/test draws; joint pass splits value fairly. -/
def twoTeamGross (r z : Rat) : Rat :=
  2*((1-r)*z+r*z/2)

theorem two_team_gross_identity (r z : Rat) : twoTeamGross r z = (2-r)*z := by
  unfold twoTeamGross
  grind

def sponsor (pi base highValue lowValue testCost : Rat) (m : Memory) (e : Strategy) : Rat :=
  twoTeamGross (passMass pi base m e) (passValue pi base highValue lowValue m e) -
    2*entryMass pi e*testCost

def genericNetGain (newPass oldPass newValue oldValue newMass oldMass
    newTest oldTest overhead : Rat) : Rat :=
  twoTeamGross newPass newValue - twoTeamGross oldPass oldValue -
    2*(newMass*newTest-oldMass*oldTest)-overhead

theorem net_gain_threshold (newPass oldPass newValue oldValue newMass oldMass
    newTest oldTest overhead : Rat) :
    0 < genericNetGain newPass oldPass newValue oldValue newMass oldMass
      newTest oldTest overhead ↔
    overhead + 2*(newMass*newTest-oldMass*oldTest) <
      (2-newPass)*newValue-(2-oldPass)*oldValue := by
  unfold genericNetGain
  rw [two_team_gross_identity, two_team_gross_identity]
  grind

/-- Actual award outcomes, with no probability assumptions for capacity. -/
def chooseAward (a b coin : Bool) : Bool × Bool :=
  if a then
    if b then (coin, !coin) else (true,false)
  else (false,b)

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

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

def localMemory : Memory
  | .aH => some true
  | .aL => some false
  | _ => none

def sharedMemory : Memory := fun s => some (truth s)

def specificityMemory : Memory
  | .aH => some true
  | .bH => none
  | .aL | .bL => some false

/-- Two wrong applied lessons; intentionally violates SoundMemory. -/
def harmfulMemory : Memory
  | .aH | .bL => some true
  | .aL | .bH => some false

def localEntry : Strategy := ⟨true,true,false,true⟩
def highOnlyEntry : Strategy := ⟨true,true,false,false⟩
def harmfulEntry : Strategy := ⟨true,false,false,true⟩
def allEntry : Strategy := ⟨true,true,true,true⟩

theorem local_rates : pHigh (1/2) localMemory = 3/4 ∧ pLow (1/2) localMemory = 1/4 := by
  decide +kernel

theorem shared_rates : pHigh (1/2) sharedMemory = 1 ∧ pLow (1/2) sharedMemory = 0 := by
  decide +kernel

theorem specificity_rates :
    pHigh (1/2) specificityMemory = 3/4 ∧ pLow (1/2) specificityMemory = 0 := by
  decide +kernel

theorem harmful_rates : pHigh (1/2) harmfulMemory = 1/2 ∧ pLow (1/2) harmfulMemory = 1/2 := by
  decide +kernel

theorem local_signature_equilibrium :
    strictEquilibrium (1/2) (1/2) 4 1 localMemory localEntry := by
  unfold strictEquilibrium strictAt
  decide +kernel

theorem shared_signature_equilibrium :
    strictEquilibrium (1/2) (1/2) 4 1 sharedMemory highOnlyEntry := by
  unfold strictEquilibrium strictAt
  decide +kernel

theorem specificity_signature_equilibrium :
    strictEquilibrium (1/2) (1/2) 4 1 specificityMemory highOnlyEntry := by
  unfold strictEquilibrium strictAt
  decide +kernel

theorem harmful_signature_equilibrium :
    strictEquilibrium (1/2) (1/2) 4 1 harmfulMemory harmfulEntry := by
  unfold strictEquilibrium strictAt
  decide +kernel

theorem local_sponsor_value : sponsor (1/2) (1/2) 8 (-4) 1 localMemory localEntry = 9/4 := by
  decide +kernel

theorem shared_sponsor_value : sponsor (1/2) (1/2) 8 (-4) 1 sharedMemory highOnlyEntry = 5 := by
  decide +kernel

theorem specificity_sponsor_value :
    sponsor (1/2) (1/2) 8 (-4) 1 specificityMemory highOnlyEntry = 31/8 := by
  decide +kernel

theorem harmful_sponsor_value :
    sponsor (1/2) (1/2) 8 (-4) 1 harmfulMemory harmfulEntry = 1/2 := by
  decide +kernel

theorem shared_gain_after_cost :
    sponsor (1/2) (1/2) 8 (-4) 1 sharedMemory highOnlyEntry -
    sponsor (1/2) (1/2) 8 (-4) 1 localMemory localEntry - 1/2 = 9/4 := by
  decide +kernel

theorem overhead_reverses_shared_gain :
    sponsor (1/2) (1/2) 8 (-4) 1 sharedMemory highOnlyEntry -
    sponsor (1/2) (1/2) 8 (-4) 1 localMemory localEntry - 3 = -1/4 := by
  decide +kernel

theorem harmful_memory_loses :
    sponsor (1/2) (1/2) 8 (-4) 1 harmfulMemory harmfulEntry -
    sponsor (1/2) (1/2) 8 (-4) 1 localMemory localEntry - 1/2 = -9/4 := by
  decide +kernel

/-- This equality fixes high-only participation in both arms. It is NOT the
    comparison of their endogenous signature-equilibrium sponsor values. -/
theorem fixed_high_only_specificity_no_gain :
    sponsor (1/2) (1/2) 8 (-4) 1 localMemory highOnlyEntry =
    sponsor (1/2) (1/2) 8 (-4) 1 specificityMemory highOnlyEntry := by
  decide +kernel

theorem uninformative_strict_pooling :
    strictEquilibrium (1/2) (1/2) 4 1 emptyMemory allEntry := by
  unfold strictEquilibrium strictAt
  decide +kernel

/-- Shows why coarse H/L separation cannot substitute for signature best replies. -/
theorem local_low_cold_type_enters :
    entryUtility (1/2) (1/2) 4 1 localMemory localEntry .bL = 1/2 := by
  decide +kernel

theorem aggregate_separation_misses_signature_deviation :
    entryUtility (1/2) (1/2) 4 (3/2) localMemory highOnlyEntry .bL = 1/8 := by
  decide +kernel

/-- No symmetric pure candidate exists in this constructed cost regime.
    This does not rule out mixed or asymmetric equilibria. -/
theorem no_symmetric_pure_example (e : Strategy) :
    ¬ weakEquilibrium (1/2) 1 4 (14/5) emptyMemory e := by
  cases e with
  | mk a b c d =>
    cases a <;> cases b <;> cases c <;> cases d <;>
      unfold weakEquilibrium weakAt <;> decide +kernel

#print axioms repeated_case_idempotent
#print axioms unseen_signature_unchanged
#print axioms finite_learning_gain
#print axioms matched_learning_gain
#print axioms sensitivity_from_coverage
#print axioms false_positive_from_coverage
#print axioms all_symmetric_pure_strategies_listed
#print axioms net_gain_threshold
#print axioms local_signature_equilibrium
#print axioms one_award_capacity
end AssessmentLearning