Skip to content
AquiaAI capability management

Research · Lean source

CapabilityContinuity.lean

The file exactly as Lean, a program that checks every step of a proof, checks it: 53 theorems in 592 lines.

What is proved, and what is not

import Std

namespace CapabilityContinuity

/- Finite continuity certificate, Lean 4.24.0 / Std.
   Policies below are deterministic-action trees over the complete public
   event history. This permits even unused coin labels to be observed, an
   information relaxation containing every public-state-history policy. The
   attaining witnesses depend only on current state and date. Fresh unused
   coins convey no information about any persistent hidden state.
   Randomized actions and hidden-state inference are outside
   the theorem. State sufficiency and public assessment are model premises.
   Concrete checks use exact rational arithmetic and all sixteen states. -/

def sumOver {O : Type} : List O → (O → Rat) → Rat
  | [], _ => 0
  | o :: os, f => f o + sumOver os f

structure Model (S A O : Type) where
  outcomes : List O
  actions : S → List A
  defaultAction : S → A
  default_feasible : ∀ s, defaultAction s ∈ actions s
  current : Nat → S → A → Rat
  weight : Nat → S → A → O → Rat
  weight_nonneg : ∀ n s a o, 0 ≤ weight n s a o
  weight_mass : ∀ n s a, sumOver outcomes (weight n s a) = 1
  discount : Rat
  discount_nonneg : 0 ≤ discount
  discount_le_one : discount ≤ 1
  next : S → A → O → S
  terminal : S → Rat

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

def expected (m : Model S A O) (n : Nat) (s : S) (a : A) (f : O → Rat) : Rat :=
  sumOver m.outcomes (fun o => m.weight n s a o * f o)

theorem sumOver_mono {O : Type} (os : List O) (f g : O → Rat)
    (h : ∀ o, o ∈ os → f o ≤ g o) : sumOver os f ≤ sumOver os g := by
  induction os with
  | nil => exact Rat.le_refl
  | cons o os ih =>
    have hh := h o (by simp)
    have ht := ih (fun x hx => h x (by simp [hx]))
    simp only [sumOver]
    grind

theorem expected_mono (m : Model S A O) (n : Nat) (s : S) (a : A)
    (f g : O → Rat) (h : ∀ o, o ∈ m.outcomes → f o ≤ g o) :
    expected m n s a f ≤ expected m n s a g := by
  apply sumOver_mono
  intro o ho
  exact Rat.mul_le_mul_of_nonneg_left (h o ho) (m.weight_nonneg n s a o)

def evaluate (m : Model S A O) : (n : Nat) → S → Policy A O n → Rat
  | 0, s, .done => m.terminal s
  | n+1, s, .step a k => m.current n s a + m.discount *
      expected m n s a (fun o => evaluate m n (m.next s a o) (k o))

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

/-- n is remaining time AFTER the action. U includes terminal closure. -/
def UpperCertificate (m : Model S A O) (U : Nat → S → Rat) (H : Nat) : Prop :=
  (∀ s, m.terminal s ≤ U 0 s) ∧
  ∀ n, n < H → ∀ s a, a ∈ m.actions s →
    m.current n s a + m.discount * expected m n s a (fun o => U n (m.next s a o)) ≤
      U (n+1) s

/-- The quantifier includes every feasible history-dependent action tree,
    including histories reached only by deviations from a chosen witness. -/
theorem certificate_bounds_every_policy (m : Model S A O) (U : Nat → S → Rat)
    (H : Nat) (hc : UpperCertificate m U H) (n : Nat) (hn : n ≤ H)
    (s : S) (pi : Policy A O n) (hp : Feasible m n s pi) :
    evaluate m n s pi ≤ U n s := by
  induction n generalizing s with
  | zero => cases pi; exact hc.1 s
  | succ n ih =>
    cases pi with
    | step a k =>
      obtain ⟨ha,hk⟩ := hp
      have hn' : n ≤ H := by omega
      have hs := expected_mono m n s a
        (fun o => evaluate m n (m.next s a o) (k o))
        (fun o => U n (m.next s a o))
        (fun o ho => ih hn' (m.next s a o) (k o) (hk o ho))
      have hd := Rat.mul_le_mul_of_nonneg_left hs m.discount_nonneg
      have hu := hc.2 n (by omega) s a ha
      simp only [evaluate]
      grind

def recommend (m : Model S A O) (sigma : Nat → S → A) :
    (n : Nat) → S → Policy A O n
  | 0, _ => .done
  | n+1, s => .step (sigma n s)
      (fun o => recommend m sigma n (m.next s (sigma n s) o))

theorem recommend_feasible (m : Model S A O) (sigma : Nat → S → A)
    (H : Nat) (hf : ∀ n, n < H → ∀ s, sigma n s ∈ m.actions s)
    (n : Nat) (hn : n ≤ H) (s : S) : Feasible m n s (recommend m sigma n s) := by
  induction n generalizing s with
  | zero => trivial
  | succ n ih => exact ⟨hf n (by omega) s, fun o _ => ih (by omega) _⟩

theorem recommend_attains (m : Model S A O) (sigma : Nat → S → A)
    (U : Nat → S → Rat) (H : Nat) (hz : ∀ s, m.terminal s = U 0 s)
    (he : ∀ n, n < H → ∀ s,
      m.current n s (sigma n s) + m.discount *
        expected m n s (sigma n s) (fun o => U n (m.next s (sigma n s) o)) = U (n+1) s)
    (n : Nat) (hn : n ≤ H) (s : S) :
    evaluate m n s (recommend m sigma n s) = U n s := by
  induction n generalizing s with
  | zero => exact hz s
  | succ n ih =>
    have hi : ∀ o, evaluate m n (m.next s (sigma n s) o)
        (recommend m sigma n (m.next s (sigma n s) o)) =
        U n (m.next s (sigma n s) o) := fun o => ih (by omega) _
    simpa only [recommend, evaluate, hi] using he n (by omega) s

theorem attaining_certificate_is_optimal (m : Model S A O) (U : Nat → S → Rat)
    (H : Nat) (hc : UpperCertificate m U H) (s : S)
    (witness : Policy A O H) (hw : Feasible m H s witness)
    (he : evaluate m H s witness = U H s) :
    Feasible m H s witness ∧ ∀ pi, Feasible m H s pi →
      evaluate m H s pi ≤ evaluate m H s witness := by
  refine ⟨hw, ?_⟩
  intro pi hp
  rw [he]
  exact certificate_bounds_every_policy m U H hc H (by omega) s pi hp

structure State where
  active : Bool
  star : Bool
  record : Bool
  apprentice : Bool
  deriving DecidableEq, Repr

inductive Action where
  | off | on | library | apprentice | both
  deriving DecidableEq, Repr

structure Outcome where
  learn : Bool
  leave : Bool
  deriving DecidableEq, Repr

def actions : List Action := [.off,.on,.library,.apprentice,.both]
def outcomes : List Outcome := [⟨true,true⟩,⟨true,false⟩,⟨false,true⟩,⟨false,false⟩]
def states : List State :=
  [⟨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⟩]

def chosenOn : Action → Bool | .off => false | _ => true
def boughtLibrary : Action → Bool | .library | .both => true | _ => false
def boughtApprentice : Action → Bool | .apprentice | .both => true | _ => false

def allowed (s : State) : Action → Bool
  | .off | .on => true
  | .library => s.star && !s.record
  | .apprentice => s.star && !s.apprentice
  | .both => s.star && !s.record && !s.apprentice

def feasibleActions (s : State) : List Action := actions.filter (allowed s)

def advance (s : State) (a : Action) (o : Outcome) : State :=
  ⟨chosenOn a, s.star && !o.leave, s.record || boughtLibrary a,
    s.apprentice || (boughtApprentice a && o.learn)⟩

structure Primitives where
  expert : Rat
  recordOutput : Rat
  apprenticeOutput : Rat
  bothOutput : Rat
  operation : Rat
  opening : Rat
  closing : Rat
  libraryCost : Rat
  apprenticeCost : Rat
  maintenance : Rat
  learning : Rat
  discount : Rat
  demand : Nat → Rat
  departure : Nat → Rat

structure StochasticValid (c : Primitives) : Prop where
  learning_nonneg : 0 ≤ c.learning
  learning_le_one : c.learning ≤ 1
  departure_nonneg : ∀ n, 0 ≤ c.departure n
  departure_le_one : ∀ n, c.departure n ≤ 1
  discount_nonneg : 0 ≤ c.discount
  discount_le_one : c.discount ≤ 1

def backup (c : Primitives) (s : State) : Rat :=
  if s.record then (if s.apprentice then c.bothOutput else c.recordOutput)
  else if s.apprentice then c.apprenticeOutput else 0

/-- Production uses the pre-action state. An acquisition cannot help today. -/
def reward (c : Primitives) (n : Nat) (s : State) (a : Action) : Rat :=
  c.demand n * (if chosenOn a && s.star then c.expert else backup c s) -
  (if chosenOn a then c.operation else 0) -
  (if !s.active && chosenOn a then c.opening else 0) -
  (if s.active && !chosenOn a then c.closing else 0) -
  (if boughtLibrary a then c.libraryCost else 0) -
  (if boughtApprentice a then c.apprenticeCost else 0) -
  (if s.record then c.maintenance else 0)

def terminal (c : Primitives) (s : State) : Rat := if s.active then -c.closing else 0

def coinWeight (q p : Rat) (o : Outcome) : Rat :=
  (if o.learn then q else 1-q) * (if o.leave then p else 1-p)

theorem coin_nonnegative (q p : Rat) (hq0 : 0 ≤ q) (hq1 : q ≤ 1)
    (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (o : Outcome) : 0 ≤ coinWeight q p o := by
  have hq : 0 ≤ 1-q := by grind
  have hp : 0 ≤ 1-p := by grind
  rcases o with ⟨l,e⟩
  cases l <;> cases e <;> simp only [coinWeight, Bool.false_eq_true, ↓reduceIte]
  all_goals apply Rat.mul_nonneg <;> assumption

theorem coin_mass_one (q p : Rat) : sumOver outcomes (coinWeight q p) = 1 := by
  simp only [outcomes, sumOver, coinWeight, Bool.false_eq_true, ↓reduceIte]
  grind

def continuityModel (c : Primitives) (hv : StochasticValid c) : Model State Action Outcome where
  outcomes := outcomes
  actions := feasibleActions
  defaultAction := fun _ => .off
  default_feasible := by intro s; simp [feasibleActions,actions,allowed]
  current := reward c
  weight := fun n _ _ o => coinWeight c.learning (c.departure n) o
  weight_nonneg := fun n _ _ o => coin_nonnegative _ _ hv.learning_nonneg
    hv.learning_le_one (hv.departure_nonneg n) (hv.departure_le_one n) o
  weight_mass := fun n _ _ => coin_mass_one c.learning (c.departure n)
  discount := c.discount
  discount_nonneg := hv.discount_nonneg
  discount_le_one := hv.discount_le_one
  next := advance
  terminal := terminal c

theorem every_state_listed (s : State) : s ∈ states := by
  rcases s with ⟨a,t,r,l⟩
  cases a <;> cases t <;> cases r <;> cases l <;> simp [states]

theorem every_action_listed (a : Action) : a ∈ actions := by cases a <;> simp [actions]

theorem record_persists (s : State) (a : Action) (o : Outcome) (h : s.record = true) :
    (advance s a o).record = true := by simp [advance,h]

theorem apprentice_requires_paid_success (s : State) (a : Action) (o : Outcome)
    (h : s.apprentice = false) :
    (advance s a o).apprentice = true ↔ boughtApprentice a = true ∧ o.learn = true := by
  simp [advance,h]

theorem expert_cannot_reappear (s : State) (a : Action) (o : Outcome) (h : s.star = false) :
    (advance s a o).star = false := by simp [advance,h]

theorem absent_teacher_cannot_preserve (s : State) (h : s.star = false) :
    feasibleActions s = [.off,.on] := by simp [feasibleActions,actions,allowed,h]

theorem terminal_closure_charged (c : Primitives) (s : State) (h : s.active = true) :
    terminal c s = -c.closing := by simp [terminal,h]

theorem off_does_not_destroy_record (s : State) (o : Outcome) :
    (advance s .off o).record = s.record := by simp [advance,boughtLibrary]

theorem service_closure_does_not_fire_star (s : State) (l : Bool) :
    (advance s .off ⟨l,false⟩).star = s.star := by simp [advance]

theorem state_mode_changes_only_switch_cost (c : Primitives) (n : Nat)
    (t r l : Bool) (a : Action) :
    reward c n ⟨true,t,r,l⟩ a - reward c n ⟨false,t,r,l⟩ a =
      if chosenOn a then c.opening else -c.closing := by
  cases a <;> simp [reward,chosenOn,backup,boughtLibrary,boughtApprentice] <;> grind

theorem successor_ignores_inherited_mode (t r l : Bool) (a : Action) (o : Outcome) :
    advance ⟨true,t,r,l⟩ a o = advance ⟨false,t,r,l⟩ a o := by rfl

/-- Bit order exactly matches the independent evaluator: active/star/record/apprentice. -/
def stateIndex (s : State) : Nat :=
  (if s.active then 8 else 0) + (if s.star then 4 else 0) +
  (if s.record then 2 else 0) + (if s.apprentice then 1 else 0)

def initial : State := ⟨false,true,false,false⟩

def base (d p : Nat → Rat) : Primitives where
  expert := 8
  recordOutput := 2
  apprenticeOutput := 3
  bothOutput := 6
  operation := 1
  opening := 1
  closing := 1/2
  libraryCost := 1
  apprenticeCost := 1
  maintenance := 1/4
  learning := 1/2
  discount := 1
  demand := d
  departure := p

def c1 : Primitives := base (fun _ => 1) (fun n => if n = 1 then 1 else 0)
def c5 : Primitives := base (fun n => if n = 0 ∨ n = 2 then 1 else 0) (fun _ => 0)
def c6 : Primitives := base (fun n => if n = 0 ∨ n = 3 then 1 else 0) (fun _ => 0)

theorem c1_valid : StochasticValid c1 := by
  constructor
  · decide +kernel
  · decide +kernel
  · intro n; change 0 ≤ (if n = 1 then (1 : Rat) else 0); split <;> decide +kernel
  · intro n; change (if n = 1 then (1 : Rat) else 0) ≤ 1; split <;> decide +kernel
  · decide +kernel
  · decide +kernel

theorem c5_valid : StochasticValid c5 := by
  constructor
  · decide +kernel
  · decide +kernel
  · intro n; exact Rat.le_refl
  · intro n; change (0 : Rat) ≤ 1; decide +kernel
  · decide +kernel
  · decide +kernel

theorem c6_valid : StochasticValid c6 := by
  constructor
  · decide +kernel
  · decide +kernel
  · intro n; exact Rat.le_refl
  · intro n; change (0 : Rat) ≤ 1; decide +kernel
  · decide +kernel
  · decide +kernel

/- Concrete certificate tables follow. All entries are checked against actual
   reward and transition functions, not treated as assumptions. -/

def tableValue (c : Primitives) (rows : Nat → List Rat) : Nat → State → Rat
  | 0, s => terminal c s
  | n+1, s => (rows n).getD (stateIndex s) 0

def tableAction (rows : Nat → List Action) (n : Nat) (s : State) : Action :=
  (rows n).getD (stateIndex s) .off

def checkCertificate (m : Model State Action Outcome) (U : Nat → State → Rat)
    (sigma : Nat → State → Action) (H : Nat) : Bool :=
  (List.range H).all fun n => states.all fun s =>
    decide (sigma n s ∈ m.actions s) &&
    decide (m.current n s (sigma n s) + m.discount *
      expected m n s (sigma n s) (fun o => U n (m.next s (sigma n s) o)) = U (n+1) s) &&
    (m.actions s).all fun a => decide
      (m.current n s a + m.discount * expected m n s a (fun o => U n (m.next s a o)) ≤
        U (n+1) s)

theorem checked_local (m : Model State Action Outcome) (U : Nat → State → Rat)
    (sigma : Nat → State → Action) (H : Nat)
    (hc : checkCertificate m U sigma H = true) (n : Nat) (hn : n < H) (s : State) :
    sigma n s ∈ m.actions s ∧
    (m.current n s (sigma n s) + m.discount *
      expected m n s (sigma n s) (fun o => U n (m.next s (sigma n s) o)) = U (n+1) s) ∧
    ∀ a, a ∈ m.actions s → m.current n s a + m.discount *
      expected m n s a (fun o => U n (m.next s a o)) ≤ U (n+1) s := by
  have h1 := (List.all_eq_true.mp hc) n (List.mem_range.mpr hn)
  have h2 := (List.all_eq_true.mp h1) s (every_state_listed s)
  obtain ⟨hfa,hu⟩ := Bool.and_eq_true_iff.mp h2
  obtain ⟨hf,ha⟩ := Bool.and_eq_true_iff.mp hfa
  refine ⟨of_decide_eq_true hf,of_decide_eq_true ha,?_⟩
  intro a hmem
  exact of_decide_eq_true ((List.all_eq_true.mp hu) a hmem)

theorem checked_upper (m : Model State Action Outcome) (U : Nat → State → Rat)
    (sigma : Nat → State → Action) (H : Nat)
    (hz : ∀ s, m.terminal s = U 0 s) (hc : checkCertificate m U sigma H = true) :
    UpperCertificate m U H := by
  refine ⟨?_,?_⟩
  · intro s; rw [hz s]; exact Rat.le_refl
  · intro n hn s a ha
    exact (checked_local m U sigma H hc n hn s).2.2 a ha

theorem checked_attainment (m : Model State Action Outcome) (U : Nat → State → Rat)
    (sigma : Nat → State → Action) (H : Nat)
    (hz : ∀ s, m.terminal s = U 0 s) (hc : checkCertificate m U sigma H = true)
    (s : State) :
    Feasible m H s (recommend m sigma H s) ∧
    evaluate m H s (recommend m sigma H s) = U H s := by
  constructor
  · exact recommend_feasible m sigma H
      (fun n hn s => (checked_local m U sigma H hc n hn s).1) H (by omega) s
  · exact recommend_attains m sigma U H hz
      (fun n hn s => (checked_local m U sigma H hc n hn s).2.1) H (by omega) s

def c1Values : Nat → List Rat
  | 0 => [0,3,7/4,23/4,11/2,11/2,21/4,23/4,-1/2,5/2,5/4,21/4,13/2,13/2,25/4,25/4]
  | 1 => [0,6,7/2,23/2,29/4,41/4,8,23/2,-1/2,11/2,3,11,33/4,45/4,9,12]
  | _ => []

def c1Actions : Nat → List Action
  | 0 => [.off,.off,.off,.off,.on,.on,.on,.off,.off,.off,.off,.off,.on,.on,.on,.on]
  | 1 => [.off,.off,.off,.off,.both,.library,.apprentice,.off,.off,.off,.off,.off,.both,.library,.apprentice,.on]
  | _ => []

def c1Model := continuityModel c1 c1_valid
def c1U := tableValue c1 c1Values
def c1Sigma := tableAction c1Actions

theorem c1_all_state_checks : checkCertificate c1Model c1U c1Sigma 2 = true := by
  decide +kernel

theorem c1_certificate : UpperCertificate c1Model c1U 2 :=
  checked_upper c1Model c1U c1Sigma 2 (fun _ => rfl) c1_all_state_checks

theorem c1_exact_initial_value : c1U 2 initial = 29/4 := by decide +kernel

theorem c1_every_history_policy_bounded (pi : Policy Action Outcome 2)
    (hp : Feasible c1Model 2 initial pi) : evaluate c1Model 2 initial pi ≤ 29/4 := by
  have h := certificate_bounds_every_policy c1Model c1U 2 c1_certificate
    2 (by omega) initial pi hp
  rw [c1_exact_initial_value] at h
  exact h

theorem c1_optimal_policy_attains :
    Feasible c1Model 2 initial (recommend c1Model c1Sigma 2 initial) ∧
    evaluate c1Model 2 initial (recommend c1Model c1Sigma 2 initial) = 29/4 := by
  have h := checked_attainment c1Model c1U c1Sigma 2
    (fun _ => rfl) c1_all_state_checks initial
  rw [c1_exact_initial_value] at h
  exact h

def c5Values : Nat → List Rat
  | 0 => [0,3,7/4,23/4,11/2,11/2,21/4,23/4,-1/2,5/2,5/4,21/4,13/2,13/2,25/4,25/4]
  | 1 => [0,3,3/2,11/2,11/2,11/2,5,11/2,-1/2,5/2,1,5,11/2,11/2,5,5]
  | 2 => [0,6,13/4,45/4,23/2,23/2,43/4,45/4,-1/2,11/2,11/4,43/4,25/2,25/2,47/4,47/4]
  | _ => []

def c5Actions : Nat → List Action
  | 0 => [.off,.off,.off,.off,.on,.on,.on,.off,.off,.off,.off,.off,.on,.on,.on,.on]
  | 1 => [.off,.off,.off,.off,.off,.off,.off,.off,.off,.off,.off,.off,.on,.on,.on,.off]
  | 2 => [.off,.off,.off,.off,.on,.on,.on,.off,.off,.off,.off,.off,.on,.on,.on,.on]
  | _ => []

def c5Model := continuityModel c5 c5_valid
def c5U := tableValue c5 c5Values
def c5Sigma := tableAction c5Actions

theorem c5_all_state_checks : checkCertificate c5Model c5U c5Sigma 3 = true := by
  decide +kernel

theorem c5_certificate : UpperCertificate c5Model c5U 3 :=
  checked_upper c5Model c5U c5Sigma 3 (fun _ => rfl) c5_all_state_checks

theorem c5_exact_initial_value : c5U 3 initial = 23/2 := by decide +kernel

theorem c5_every_history_policy_bounded (pi : Policy Action Outcome 3)
    (hp : Feasible c5Model 3 initial pi) : evaluate c5Model 3 initial pi ≤ 23/2 := by
  have h := certificate_bounds_every_policy c5Model c5U 3 c5_certificate
    3 (by omega) initial pi hp
  rw [c5_exact_initial_value] at h
  exact h

theorem c5_optimal_policy_attains :
    Feasible c5Model 3 initial (recommend c5Model c5Sigma 3 initial) ∧
    evaluate c5Model 3 initial (recommend c5Model c5Sigma 3 initial) = 23/2 := by
  have h := checked_attainment c5Model c5U c5Sigma 3
    (fun _ => rfl) c5_all_state_checks initial
  rw [c5_exact_initial_value] at h
  exact h

def c6Values : Nat → List Rat
  | 0 => [0,3,7/4,23/4,11/2,11/2,21/4,23/4,-1/2,5/2,5/4,21/4,13/2,13/2,25/4,25/4]
  | 1 => [0,3,3/2,11/2,11/2,11/2,5,11/2,-1/2,5/2,1,5,11/2,11/2,5,5]
  | 2 => [0,3,5/4,21/4,11/2,11/2,19/4,21/4,-1/2,5/2,3/4,19/4,5,5,17/4,19/4]
  | 3 => [0,6,3,11,11,11,10,11,-1/2,11/2,5/2,21/2,12,12,11,23/2]
  | _ => []

def c6Actions : Nat → List Action
  | 0 => [.off,.off,.off,.off,.on,.on,.on,.off,.off,.off,.off,.off,.on,.on,.on,.on]
  | 1 => [.off,.off,.off,.off,.off,.off,.off,.off,.off,.off,.off,.off,.on,.on,.on,.off]
  | 2 => [.off,.off,.off,.off,.off,.off,.off,.off,.off,.off,.off,.off,.off,.off,.off,.off]
  | 3 => [.off,.off,.off,.off,.on,.on,.on,.off,.off,.off,.off,.off,.on,.on,.on,.on]
  | _ => []

def c6Model := continuityModel c6 c6_valid
def c6U := tableValue c6 c6Values
def c6Sigma := tableAction c6Actions

theorem c6_all_state_checks : checkCertificate c6Model c6U c6Sigma 4 = true := by
  decide +kernel

theorem c6_certificate : UpperCertificate c6Model c6U 4 :=
  checked_upper c6Model c6U c6Sigma 4 (fun _ => rfl) c6_all_state_checks

theorem c6_exact_initial_value : c6U 4 initial = 11 := by decide +kernel

theorem c6_every_history_policy_bounded (pi : Policy Action Outcome 4)
    (hp : Feasible c6Model 4 initial pi) : evaluate c6Model 4 initial pi ≤ 11 := by
  have h := certificate_bounds_every_policy c6Model c6U 4 c6_certificate
    4 (by omega) initial pi hp
  rw [c6_exact_initial_value] at h
  exact h

theorem c6_optimal_policy_attains :
    Feasible c6Model 4 initial (recommend c6Model c6Sigma 4 initial) ∧
    evaluate c6Model 4 initial (recommend c6Model c6Sigma 4 initial) = 11 := by
  have h := checked_attainment c6Model c6U c6Sigma 4
    (fun _ => rfl) c6_all_state_checks initial
  rw [c6_exact_initial_value] at h
  exact h

theorem sixteen_states_without_duplicates : states.length = 16 ∧ states.Nodup := by decide +kernel

theorem four_outcomes_without_duplicates : outcomes.length = 4 ∧ outcomes.Nodup := by decide +kernel

def actionValue (m : Model State Action Outcome) (U : Nat → State → Rat)
    (n : Nat) (s : State) (a : Action) : Rat :=
  m.current n s a + m.discount * expected m n s a (fun o => U n (m.next s a o))

/-- Complete maximizing-action sets are defined by equality, not by a
    representative tie-breaking action. Under a certificate and attainment
    this set contains exactly the feasible Bellman maximizers. -/
def maximizingActions (m : Model State Action Outcome) (U : Nat → State → Rat)
    (n : Nat) (s : State) : List Action :=
  (m.actions s).filter (fun a => decide (actionValue m U n s a = U (n+1) s))

theorem maximizing_set_preserves_every_tie (m : Model State Action Outcome)
    (U : Nat → State → Rat) (n : Nat) (s : State) (a : Action) :
    a ∈ maximizingActions m U n s ↔
      a ∈ m.actions s ∧ actionValue m U n s a = U (n+1) s := by
  simp [maximizingActions]

theorem c1_initial_action_values :
    (feasibleActions initial).map (actionValue c1Model c1U 1 initial) =
      [0,11/2,25/4,6,29/4] := by decide +kernel

theorem c1_initial_unique_maximizer : maximizingActions c1Model c1U 1 initial = [.both] := by
  decide +kernel

theorem c1_preserve_then_close (l : Bool) :
    c1Sigma 1 initial = .both ∧ c1Sigma 0 (advance initial .both ⟨l,true⟩) = .off := by
  cases l <;> decide +kernel

theorem c5_selected_standing_path :
    c5Sigma 2 initial = .on ∧
    c5Sigma 1 ⟨true,true,false,false⟩ = .on ∧
    c5Sigma 0 ⟨true,true,false,false⟩ = .on := by decide +kernel

theorem c6_selected_pop_up_path :
    c6Sigma 3 initial = .on ∧
    c6Sigma 2 ⟨true,true,false,false⟩ = .off ∧
    c6Sigma 1 initial = .off ∧ c6Sigma 0 initial = .on := by decide +kernel

/-- Locations are labels only when their states, feasible actions, public
    events, rewards and terminal closure are identical. Both quantified
    policy classes below use precisely that same model. -/
theorem same_mechanics_local_and_shared_optimum :
    (∀ pi : Policy Action Outcome 2, Feasible c1Model 2 initial pi →
      evaluate c1Model 2 initial pi ≤ 29/4) ∧
    (∃ pi : Policy Action Outcome 2, Feasible c1Model 2 initial pi ∧
      evaluate c1Model 2 initial pi = 29/4) := by
  exact ⟨c1_every_history_policy_bounded,
    ⟨recommend c1Model c1Sigma 2 initial,c1_optimal_policy_attains⟩⟩

theorem mandatory_entry_fee_one : c1U 2 initial - 1 = 25/4 := by
  rw [c1_exact_initial_value]
  decide +kernel

theorem mandatory_overhead_strictly_loses (F : Rat) :
    c1U 2 initial - F < c1U 2 initial ↔ 0 < F := by grind

def optionalRouteValue (localValue F : Rat) : Rat :=
  if localValue < localValue-F then localValue-F else localValue

theorem optional_route_can_decline (F : Rat) (hF : 0 ≤ F) :
    optionalRouteValue (c1U 2 initial) F = 29/4 := by
  rw [c1_exact_initial_value]
  unfold optionalRouteValue
  split <;> grind

theorem partial_backup_below_expert :
    backup c1 ⟨false,false,true,true⟩ = 6 ∧ c1.expert = 8 ∧
    backup c1 ⟨false,false,true,true⟩ < c1.expert := by decide +kernel

end CapabilityContinuity