SwitchTracker.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Literal hysteresis of the two allocation-rule outputs and its drop potential. This is not total-variation tracking of S: only changes of the old-rule potential after filtering enter the all-step ledger.

inductive OAI.UniformKServer.SwitchTracker.Rule line 13
def OAI.UniformKServer.SwitchTracker.update line 17
def OAI.UniformKServer.SwitchTracker.valid line 22
def OAI.UniformKServer.SwitchTracker.potential line 27
def OAI.UniformKServer.SwitchTracker.charge line 32
theorem OAI.UniformKServer.SwitchTracker.update_valid line 37
theorem OAI.UniformKServer.SwitchTracker.potential_nonneg line 41
theorem OAI.UniformKServer.SwitchTracker.charge_nonneg line 44
theorem OAI.UniformKServer.SwitchTracker.switch_drop line 48
Source documentation
The actual Rule I→II charge is D, and II→I charge is S.
```
theorem switch_drop (old : Rule) (S D : ℝ) :
    potential (update old S D) S D ≤ potential old S D-charge old S D/2 := by
…
```
Mentions: OAI.UniformKServer.SwitchTracker.Rule, OAI.UniformKServer.SwitchTracker.potential, OAI.UniformKServer.SwitchTracker.update, OAI.UniformKServer.SwitchTracker.charge
theorem OAI.UniformKServer.SwitchTracker.input_slope line 52
theorem OAI.UniformKServer.SwitchTracker.nonwholesale_step line 60
Source documentation
New S here is compared to the OLD flag sum at NEW posteriors. Thus its error is the number of flag changes, not absolute posterior variation.
```
theorem nonwholesale_step (old : Rule) (Sbar Dold Snew Dnew K : ℝ)
    (hK : |Snew-Sbar| ≤ K) :
    potential (update old Snew Dnew) Snew Dnew-potential old Sbar Dold ≤
      K+|Dnew-Dold|-charge old Snew Dnew/2 := by
…
```
Mentions: OAI.UniformKServer.SwitchTracker.Rule, OAI.UniformKServer.SwitchTracker.potential, OAI.UniformKServer.SwitchTracker.update, OAI.UniformKServer.SwitchTracker.charge
theorem OAI.UniformKServer.SwitchTracker.wholesale_step line 69
Source documentation
At wholesale resets no switch credit is claimed.
```
theorem wholesale_step (old new : Rule) {Sbar Dold Snew Dnew C : ℝ}
    (hS : 0 ≤ Sbar) (hD : 0 ≤ Dold) (hSC : Snew ≤ C) (hDC : Dnew ≤ C) :
    potential new Snew Dnew-potential old Sbar Dold ≤ C := by
…
```
Mentions: OAI.UniformKServer.SwitchTracker.Rule, OAI.UniformKServer.SwitchTracker.potential