Coarse.lean`

125 declarations, 0 contain sorry, 0 declared as axioms

The actual epoch/wholesale recurrence of §03. The old credit is discarded on a parent refresh, never spent twice. Empty transitions are forced by the same variation test.

structure OAI.KServer.CoarseSchedule.State line 13
def OAI.KServer.CoarseSchedule.Valid line 17
def OAI.KServer.CoarseSchedule.update line 19
def OAI.KServer.CoarseSchedule.charge line 25
def OAI.KServer.CoarseSchedule.factor line 26
def OAI.KServer.CoarseSchedule.potential line 27
lemma OAI.KServer.CoarseSchedule.factor_ge_seven line 30
lemma OAI.KServer.CoarseSchedule.update_valid line 34
lemma OAI.KServer.CoarseSchedule.charge_self line 39
lemma OAI.KServer.CoarseSchedule.charge_le line 40
lemma OAI.KServer.CoarseSchedule.update_credit line 45
lemma OAI.KServer.CoarseSchedule.potential_nonneg line 83
lemma OAI.KServer.CoarseSchedule.potential_input line 88
def OAI.KServer.CoarseSchedule.run line 97
lemma OAI.KServer.CoarseSchedule.run_valid line 101
theorem OAI.KServer.CoarseSchedule.active_size_budget line 108
Source documentation
Uniform-in-horizon amortization of the literal §03 active-size schedule. This pays genuine old-plus-new charges, not merely total variation.
```
theorem active_size_budget {c δ : ℝ} {x : ℕ → ℝ} {initial : State}
    (hc : 0 ≤ c) (hδ : 0 < δ) (hδu : δ ≤ 1/3)
    (hx : ∀ t, 0 ≤ x t) (hi : Valid initial) (N : ℕ) :
    (∑ t ∈ range N, charge (run c δ x initial t) (run c δ x initial (t+1))) ≤
      factor δ*(∑ t ∈ range N, |x (t+1)-x t|) + potential c δ (x 0) initial := by
…
```
Mentions: OAI.KServer.CoarseSchedule.State, OAI.KServer.CoarseSchedule.Valid, OAI.KServer.CoarseSchedule.charge, OAI.KServer.CoarseSchedule.run, OAI.KServer.CoarseSchedule.factor, OAI.KServer.CoarseSchedule.potential
def OAI.KServer.EpochSchedule.total line 138
def OAI.KServer.EpochSchedule.variation line 139
lemma OAI.KServer.EpochSchedule.variation_nonneg line 140
lemma OAI.KServer.EpochSchedule.total_nonneg line 141
lemma OAI.KServer.EpochSchedule.total_change line 142
lemma OAI.KServer.EpochSchedule.coordinate_change line 145
lemma OAI.KServer.EpochSchedule.variation_triangle line 147
structure OAI.KServer.EpochSchedule.State line 151
def OAI.KServer.EpochSchedule.Valid line 155
def OAI.KServer.EpochSchedule.reset line 159
instance OAI.KServer.EpochSchedule.(instance at line 162) line 162
def OAI.KServer.EpochSchedule.update line 164
lemma OAI.KServer.EpochSchedule.update_valid line 167
lemma OAI.KServer.EpochSchedule.valid_total line 177
lemma OAI.KServer.EpochSchedule.valid_coordinate line 182
lemma OAI.KServer.EpochSchedule.empty_transition line 187
def OAI.KServer.EpochSchedule.wholesale line 203
def OAI.KServer.EpochSchedule.parentCharge line 206
lemma OAI.KServer.EpochSchedule.update_budget line 212
Source documentation
Each volume-triggered wholesale consumes only its epoch's accumulated variation. The constant 203 is the literal bound used in the source.
```
lemma update_budget {x y : J → ℝ} {a b : K} {s : State J}
    (hs : Valid x s) :
    wholesale x y a b s+203*(update x y a b s).credit ≤
      203*s.credit+203*variation y x+parentCharge x y a b := by
…
```
Mentions: OAI.KServer.EpochSchedule.State, OAI.KServer.EpochSchedule.Valid, OAI.KServer.EpochSchedule.wholesale, OAI.KServer.EpochSchedule.update, OAI.KServer.EpochSchedule.variation, OAI.KServer.EpochSchedule.parentCharge
def OAI.KServer.EpochSchedule.run line 233
lemma OAI.KServer.EpochSchedule.run_valid line 237
theorem OAI.KServer.EpochSchedule.wholesale_budget line 246
Source documentation
Deterministic finite-horizon wholesale budget, with no terminal charge and no dependence on the horizon in its constants.
```
theorem wholesale_budget (x : ℕ → J → ℝ) (key : ℕ → K) (hx : ∀ t i, 0 ≤ x t i) (n : ℕ) :
    (∑ t ∈ range n, wholesale (x t) (x (t+1)) (key t) (key (t+1)) (run x key t)) ≤
      203*(∑ t ∈ range n, variation (x (t+1)) (x t))+
      ∑ t ∈ range n, parentCharge (x t) (x (t+1)) (key t) (key (t+1)) := by
…
```
Mentions: OAI.KServer.EpochSchedule.wholesale, OAI.KServer.EpochSchedule.run, OAI.KServer.EpochSchedule.variation, OAI.KServer.EpochSchedule.parentCharge
def OAI.KServer.EpochSchedule.dominant line 267
Source documentation
Exact dominant selection; the same reference, hence the same mark, is held until a wholesale event.
```
def dominant (s : State J) : Option J :=
…
```
Mentions: OAI.KServer.EpochSchedule.State
lemma OAI.KServer.EpochSchedule.dominant_large line 271
lemma OAI.KServer.EpochSchedule.regular_small line 280
lemma OAI.KServer.EpochSchedule.side_total line 304
def OAI.KServer.CoarseProcess.estimate line 332
Source documentation
Literal sum of the independently maintained size-rank references.
```
def estimate (δ : ℝ) (P : R → FilteredRanks w) (t : ℕ) (ω : Ω) : ℝ :=
…
```
def OAI.KServer.CoarseProcess.size line 334
lemma OAI.KServer.CoarseProcess.estimate_nonneg line 337
lemma OAI.KServer.CoarseProcess.size_nonneg line 339
lemma OAI.KServer.CoarseProcess.estimate_accuracy line 342
lemma OAI.KServer.CoarseProcess.estimate_bound line 355
lemma OAI.KServer.CoarseProcess.term_variation line 364
lemma OAI.KServer.CoarseProcess.estimate_variation line 381
lemma OAI.KServer.CoarseProcess.update_accuracy line 408
Source documentation
All invariants are established after actually executing the hysteretic rule.
```
lemma update_accuracy {c δ x : ℝ} {s : CoarseSchedule.State}
    (hc : 0 < c) (hδ : 0 < δ) (hx : 0 ≤ x) (hs : CoarseSchedule.Valid s) :
    let a := CoarseSchedule.update c δ x s
…
```
Mentions: OAI.KServer.CoarseSchedule.State, OAI.KServer.CoarseSchedule.Valid, OAI.KServer.CoarseSchedule.update
def OAI.KServer.CoarseProcess.active line 434
Source documentation
Trackers are not reinitialized; the active state alone is updated.
```
def active (c δ : ℝ) (P : R → FilteredRanks w) (ω : Ω) : ℕ → CoarseSchedule.State :=
…
```
Mentions: OAI.KServer.CoarseSchedule.State
lemma OAI.KServer.CoarseProcess.active_valid line 438
lemma OAI.KServer.CoarseProcess.active_accuracy line 443
lemma OAI.KServer.CoarseProcess.charge_nonneg line 480
lemma OAI.KServer.CoarseProcess.initial_potential line 487
lemma OAI.KServer.CoarseProcess.avg_range line 504

theorem OAI.KServer.CoarseProcess.active_budget line 510

Source documentation

Actual old-plus-new active refresh budget, with a fixed-star endpoint.

theorem active_budget {c δ : ℝ} (hc : 0 < c) (hδ : 0 < δ) (hδu : δ ≤ 1/1000)
    (hw : ∀ ω, 0 ≤ w ω) (hw1 : ∑ ω, w ω=1) (P : R → FilteredRanks w) (N : ℕ) :
    (∑ t ∈ range N, avg w (fun ω =>
        charge (active c δ P ω t) (active c δ P ω (t+1)))) ≤
      (factor δ*(5*(4/3:ℝ)^2/δ)) *
        (∑ a, ∑ t ∈ range N, avg w (fun ω => |(P a).p (t+1) ω-(P a).before (t+1) ω|))+
      (factor δ*(5*(4/3:ℝ)^2/δ+1))*Fintype.card R := by
…

Mentions: OAI.KServer.CoarseProcess.active

lemma OAI.KServer.CoarseProcess.estimate_adapted line 534
lemma OAI.KServer.CoarseProcess.active_adapted line 543
def OAI.KServer.CoarseProcess.relative line 560
Source documentation
The parent's scalar relative reference, and later the side-total reference, use exactly the manuscript's two-sided factor test, including zero crossings.
```
def relative (δ : ℝ) (x : ℕ → Ω → ℝ) : ℕ → Ω → ℝ := held (factorTest id δ) x
…
```
lemma OAI.KServer.CoarseProcess.relative_nonneg line 563
lemma OAI.KServer.CoarseProcess.relative_accuracy line 574
def OAI.KServer.CoarseProcess.relativeCharge line 587
lemma OAI.KServer.CoarseProcess.relative_charge_bound line 592
lemma OAI.KServer.CoarseProcess.relative_budget line 610
def OAI.KServer.CoarseEpoch.clipped line 634
def OAI.KServer.CoarseEpoch.parent line 637
lemma OAI.KServer.CoarseEpoch.clipped_nonneg line 640
lemma OAI.KServer.CoarseEpoch.clipped_variation line 643
lemma OAI.KServer.CoarseEpoch.clipped_accuracy line 648
lemma OAI.KServer.CoarseEpoch.parent_accuracy line 663
lemma OAI.KServer.CoarseEpoch.parent_nonneg line 675
lemma OAI.KServer.CoarseEpoch.parent_budget line 678
def OAI.KServer.CoarseEpoch.vector line 698
lemma OAI.KServer.CoarseEpoch.vector_nonneg line 702
lemma OAI.KServer.CoarseEpoch.value_bound line 705
lemma OAI.KServer.CoarseEpoch.total_parent line 712
lemma OAI.KServer.CoarseEpoch.value_variation line 726
lemma OAI.KServer.CoarseEpoch.vector_variation line 733
lemma OAI.KServer.CoarseEpoch.wholesale_parent line 741

lemma OAI.KServer.CoarseEpoch.wholesale_budget line 762

Source documentation

The literal epoch recurrence is paid by actual active-size and parent reference changes; the test does not assume its own amortized conclusion.

lemma wholesale_budget {c δ ε : ℝ} (hc : 0 < c) (hδ : 0 < δ) (hδu : δ ≤ 1/1000)
    (hε : 0 < ε) (hεu : ε ≤ 1/1000) (P : J → R → FilteredRanks w) (V : R → FilteredRanks w)
    (htree : ∀ t ω, (∑ i,size (P i) t ω) ≤ size V t ω) (β : ℝ → ℝ) (ω : Ω) (N : ℕ) :
    (∑ t ∈ range N, EpochSchedule.wholesale (vector c δ P ω t) (vector c δ P ω (t+1))
        (β (parent c ε V t ω)) (β (parent c ε V (t+1) ω))
        (EpochSchedule.run (vector c δ P ω) (fun t => β (parent c ε V t ω)) t)) ≤
      203*(∑ t ∈ range N, ∑ i,charge (active c δ (P i) ω t) (active c δ (P i) ω (t+1)))+
      2*(∑ t ∈ range N, relativeCharge ε (clipped c ε V) t ω) := by
…

Mentions: OAI.KServer.EpochSchedule.wholesale, OAI.KServer.CoarseEpoch.vector, OAI.KServer.CoarseEpoch.parent, OAI.KServer.EpochSchedule.run, OAI.KServer.CoarseEpoch.clipped

def OAI.KServer.CoarseSide.held line 790

Source documentation

Relative reference with genuine wholesale resets. Resetting discards, rather than spends, the unused scalar variation credit.

def held (δ : ℝ) (x : ℕ → ℝ) (reset : ℕ → Prop) : ℕ → ℝ
  | 0 => x 0
  | t+1 => if reset t ∨ factorTest id δ (x (t+1)) (held δ x reset t)
      then x (t+1) else held δ x reset t

lemma OAI.KServer.CoarseSide.held_nonneg line 795
lemma OAI.KServer.CoarseSide.held_accuracy line 801
def OAI.KServer.CoarseSide.charge line 815
def OAI.KServer.CoarseSide.stepVariation line 818
def OAI.KServer.CoarseSide.C line 821
lemma OAI.KServer.CoarseSide.C_nonneg line 823
lemma OAI.KServer.CoarseSide.update_budget line 825
lemma OAI.KServer.CoarseSide.budget line 849
def OAI.KServer.CoarseSide.side line 864
lemma OAI.KServer.CoarseSide.side_nonneg line 867
lemma OAI.KServer.CoarseSide.side_le_total line 871
lemma OAI.KServer.CoarseSide.mark_unchanged line 875
lemma OAI.KServer.CoarseSide.side_variation line 880
def OAI.KServer.CoarseSide.sideInput line 893
Source documentation
Actual side totals and reset times are derived from the epoch recurrence.
```
def sideInput (x : ℕ → J → ℝ) (key : ℕ → K) (t : ℕ) : ℝ := side (x t) (run x key t)
```
Mentions: OAI.KServer.CoarseSide.side
def OAI.KServer.CoarseSide.epochReset line 894
lemma OAI.KServer.CoarseSide.side_stepVariation line 897

lemma OAI.KServer.CoarseSide.side_budget line 906

Source documentation

Side-reference refreshes are paid independently of the number of epochs.

lemma side_budget {δ : ℝ} (hδ : 0 < δ) (x : ℕ → J → ℝ)
    (key : ℕ → K) (hx : ∀ t i, 0 ≤ x t i) (N : ℕ) :
    (∑ t ∈ range N, charge δ (sideInput x key) (epochReset x key) t) ≤
      C δ*(∑ t ∈ range N, variation (x (t+1)) (x t)) := by
…

Mentions: OAI.KServer.CoarseSide.charge, OAI.KServer.CoarseSide.sideInput, OAI.KServer.CoarseSide.epochReset, OAI.KServer.CoarseSide.C

lemma OAI.KServer.CoarseParameters.regular_log_comparison line 923
lemma OAI.KServer.CoarseParameters.dominant_log_comparison line 936

lemma OAI.KServer.CoarseParameters.size_ratio line 951

Source documentation

Quantitative size-ratio estimate from the genuine superadditive parent size, without discarding the child's own true size.

lemma size_ratio {M a : J → ℝ} {V : ℝ} (hM : ∀ i, 0 ≤ M i)
    (_ : ∀ i, 0 ≤ a i) (hupper : ∀ i, a i ≤ (11/10)*M i)
    (hV : (∑ i,M i) ≤ V) (i : J) (hMi : 0 < M i) (hai : 0 < a i)
    (hlower : (9/10)*M i ≤ a i) :
    1+(9/11)*((∑ j,a j)/a i-1) ≤ V/M i := by
…

lemma OAI.KServer.CoarseParameters.regular_gap line 968
lemma OAI.KServer.CoarseParameters.dominant_gap line 982
def OAI.KServer.CoarseParameters.beta line 1006
Source documentation
Literal true and held beta parameters. Their coefficient is chosen only once; these functions do not depend on the horizon or posterior law.
```
def beta (k c cb ell M : ℝ) : ℝ := 3+cb/ell*Real.log (k/max M c)
```
def OAI.KServer.CoarseParameters.lowerSize line 1007
def OAI.KServer.CoarseParameters.upperBeta line 1008
lemma OAI.KServer.CoarseParameters.beta_difference line 1010
lemma OAI.KServer.CoarseParameters.lowerSize_accuracy line 1018
lemma OAI.KServer.CoarseParameters.beta_upper_error line 1031
lemma OAI.KServer.CoarseScale.size_antitone line 1072
lemma OAI.KServer.CoarseScale.rank_size line 1077
def OAI.KServer.CoarseScale.noncore line 1087
lemma OAI.KServer.CoarseScale.noncore_nonneg line 1090
lemma OAI.KServer.CoarseScale.noncore_bound line 1098
lemma OAI.KServer.CoarseScale.term_variation line 1113
lemma OAI.KServer.CoarseScale.noncore_variation line 1119
lemma OAI.KServer.CoarseScale.mark_positive line 1129
def OAI.KServer.CoarseScale.scale line 1138
lemma OAI.KServer.CoarseScale.scale_nonneg line 1142
lemma OAI.KServer.CoarseScale.scale_bound line 1149
lemma OAI.KServer.CoarseScale.scale_unchanged_variation line 1175
lemma OAI.KServer.CoarseScale.scale_step line 1197

lemma OAI.KServer.CoarseScale.scale_budget line 1227

Source documentation

The change of dominant flex scale is paid by actual elementary trackers, core flips, and wholesale totals. This includes changes of dominant identity.

lemma scale_budget {c δ : ℝ} (hc : 0 < c) (hδ : 0 < δ) (hδu : δ ≤ 1/1000)
    (hw : ∀ ω, 0 ≤ w ω) (hw1 : ∑ ω,w ω=1)
    (P : J → R → FilteredRanks w) (key : Ω → ℕ → K) (N : ℕ) :
    (∑ t ∈ range N, avg w (fun ω =>
      |scale δ P (t+1) ω (EpochSchedule.run (CoarseEpoch.vector c δ P ω) (key ω) (t+1))-
       scale δ P t ω (EpochSchedule.run (CoarseEpoch.vector c δ P ω) (key ω) t)|)) ≤
      (80/δ+(CoreFlags.tolerance^2)⁻¹)*
        ((∑ i, ∑ a, ∑ t ∈ range N, avg w (fun ω => |(P i a).p (t+1) ω-(P i a).before (t+1) ω|))+
          Fintype.card J*Fintype.card R)+
      41*(∑ t ∈ range N, avg w (fun ω => EpochSchedule.wholesale
        (CoarseEpoch.vector c δ P ω t) (CoarseEpoch.vector c δ P ω (t+1))
        (key ω t) (key ω (t+1)) (EpochSchedule.run (CoarseEpoch.vector c δ P ω) (key ω) t))) := by
…

Mentions: OAI.KServer.CoarseScale.scale, OAI.KServer.EpochSchedule.run, OAI.KServer.CoarseEpoch.vector, OAI.KServer.CoreFlags.tolerance, OAI.KServer.EpochSchedule.wholesale