Experiments.lean`

52 declarations, 0 contain sorry, 0 declared as axioms

def OAI.KServer.FiniteExperiment.optimalTrace line 18
Source documentation
A fixed minimizing labeled trajectory for each complete input.
```
def optimalTrace (s : Configuration k Y) (σ : Fin H → Y) : List (Y × Fin k) :=
…
```
Mentions: OAI.KServer.Configuration
lemma OAI.KServer.FiniteExperiment.optimalTrace_requests line 22
lemma OAI.KServer.FiniteExperiment.optimalTrace_cost line 27
lemma OAI.KServer.FiniteExperiment.optimalTrace_length line 33
def OAI.KServer.FiniteExperiment.hidden line 39
Source documentation
The genuine hidden configuration, frozen when the finite input ends.
```
def hidden (s : Configuration k Y) (σ : Fin H → Y) (t : ℕ) : Configuration k Y :=
…
```
Mentions: OAI.KServer.Configuration
lemma OAI.KServer.FiniteExperiment.hidden_zero line 43
def OAI.KServer.FiniteExperiment.mover line 47
Source documentation
Current designated occurrence in the selected optimum; it is not observed.
```
def mover (s : Configuration k Y) (σ : Fin H → Y) (t : Fin H) : Fin k :=
…
```
Mentions: OAI.KServer.Configuration
lemma OAI.KServer.FiniteExperiment.optimalTrace_get_request line 51
lemma OAI.KServer.FiniteExperiment.hidden_step line 60
lemma OAI.KServer.FiniteExperiment.hidden_covers line 69
def OAI.KServer.FiniteExperiment.requestPrefix line 75
Source documentation
A finite observation sufficient for exactly the request requestPrefix.
```
def requestPrefix (σ : Fin H → Y) (t : ℕ) : Fin H → Option Y :=
…
```
lemma OAI.KServer.FiniteExperiment.prefix_refines line 79
lemma OAI.KServer.FiniteExperiment.prefix_request line 88
def OAI.KServer.FiniteExperiment.history line 97
Source documentation
Histories include the independent partition tape from time zero. Coding a finite observation by a natural number is injective, not a loss of information.
```
def history (t : ℕ) (ω : (Fin H → Y) × T) : ℕ :=
…
```
lemma OAI.KServer.FiniteExperiment.history_eq_iff line 101
lemma OAI.KServer.FiniteExperiment.history_refines line 107
def OAI.KServer.FiniteExperiment.weight line 113
Source documentation
Literal independent product weights, before any requestPrefix is revealed.
```
def weight (law : FiniteDistribution (Fin H → Y)) (tape : FiniteDistribution T)
    (ω : (Fin H → Y) × T) : ℝ := law.val ω.1*tape.val ω.2
…
```
Mentions: OAI.KServer.FiniteDistribution
lemma OAI.KServer.FiniteExperiment.weight_nonneg line 117
lemma OAI.KServer.FiniteExperiment.weight_sum line 122
def OAI.KServer.FiniteExperiment.count line 129
Source documentation
All ranks queried by the allocation are actual conditional hidden counts. The online map may depend on the partition tape and request requestPrefix; it never changes how the old hidden quantity is filtered.
```
def count (s : Configuration k Y) {V : Type*} (map : ℕ → ((Fin H → Y) × T) → Y → V)
    (under : V → V → Bool) (v : V) (t : ℕ) (ω : (Fin H → Y) × T) : ℕ :=
…
```
Mentions: OAI.KServer.Configuration
lemma OAI.KServer.FiniteExperiment.count_le line 134

def OAI.KServer.FiniteExperiment.ranks line 142

Source documentation

This concrete process discharges the signed all-step filtering premise.

def ranks (s : Configuration k Y) (law : FiniteDistribution (Fin H → Y))
    (tape : FiniteDistribution T) {V : Type*}
    (map : ℕ → ((Fin H → Y) × T) → Y → V) (under : V → V → Bool)
    (v : V) (a : Fin k) : RankTracking.FilteredRanks (weight law tape) :=
…

Mentions: OAI.KServer.Configuration, OAI.KServer.FiniteDistribution, OAI.KServer.RankTracking.FilteredRanks, OAI.KServer.FiniteExperiment.weight

lemma OAI.KServer.FiniteExperiment.ranks_drift line 148
lemma OAI.KServer.FiniteExperiment.hidden_movement line 162
lemma OAI.KServer.FiniteExperiment.hidden_total_cost line 170
lemma OAI.KServer.FiniteExperiment.expected_hidden_cost line 193
def OAI.KServer.FiniteExperiment.requestHistory line 203
Source documentation
True request history alone, for computing the metric posterior independently of the partition tape.
```
def requestHistory (t : ℕ) (σ : Fin H → Y) : ℕ :=
…
```
lemma OAI.KServer.FiniteExperiment.requestHistory_eq_iff line 207
lemma OAI.KServer.FiniteExperiment.mass_product line 213
lemma OAI.KServer.FiniteExperiment.numerator_product line 228
lemma OAI.KServer.FiniteExperiment.posterior_tape_irrelevant line 246
Source documentation
The precise independence statement legitimately used by the manuscript. It does not assert independence of partition events after conditioning on the tape, nor does it select reset events in a martingale estimate.
```
lemma posterior_tape_irrelevant (law : FiniteDistribution (Fin H → Y))
    (tape : FiniteDistribution T) (t : ℕ) (ω : (Fin H → Y) × T)
    (ht : tape.val ω.2≠0) (f : (Fin H → Y) → ℝ) :
    posterior (weight law tape) (history t) (fun z => f z.1) ω=
      posterior law.val (requestHistory t) f ω.1 := by
…
```
Mentions: OAI.KServer.FiniteDistribution, OAI.KServer.FiniteExperiment.weight, OAI.KServer.FiniteExperiment.history, OAI.KServer.FiniteExperiment.requestHistory
def OAI.KServer.FiniteExperiment.metricCount line 255
Source documentation
Counting measure of a labeled configuration; repetitions contribute separately.
```
def metricCount (c : Configuration k Y) (y : Y) : ℝ := by
…
```
Mentions: OAI.KServer.Configuration
lemma OAI.KServer.FiniteExperiment.metricCount_nonneg line 260
lemma OAI.KServer.FiniteExperiment.metricCount_total line 265
lemma OAI.KServer.FiniteExperiment.metricCount_at line 272
def OAI.KServer.FiniteExperiment.mu line 281
Source documentation
The true-metric posterior after t requests, independent of algorithmic tapes.
```
def mu (s : Configuration k Y) (law : FiniteDistribution (Fin H → Y))
    (t : ℕ) (σ : Fin H → Y) (y : Y) : ℝ :=
…
```
Mentions: OAI.KServer.Configuration, OAI.KServer.FiniteDistribution
lemma OAI.KServer.FiniteExperiment.mu_nonneg line 285
lemma OAI.KServer.FiniteExperiment.mu_total line 289
lemma OAI.KServer.FiniteExperiment.request_of_history line 296
lemma OAI.KServer.FiniteExperiment.mu_served line 301
lemma OAI.KServer.FiniteExperiment.mu_adapted line 312
lemma OAI.KServer.FiniteExperiment.metricCount_move line 317
def OAI.KServer.FiniteExperiment.muBefore line 333
Source documentation
Old counting measure filtered through the new true request.
```
def muBefore (s : Configuration k Y) (law : FiniteDistribution (Fin H → Y))
    (t : Fin H) (σ : Fin H → Y) (y : Y) : ℝ :=
…
```
Mentions: OAI.KServer.Configuration, OAI.KServer.FiniteDistribution
def OAI.KServer.FiniteExperiment.nu line 338
Source documentation
The conditional old-location law of the single designated optimum mover.
```
def nu (s : Configuration k Y) (law : FiniteDistribution (Fin H → Y))
    (t : Fin H) (σ : Fin H → Y) (y : Y) : ℝ := by
…
```
Mentions: OAI.KServer.Configuration, OAI.KServer.FiniteDistribution
lemma OAI.KServer.FiniteExperiment.muBefore_nonneg line 344
lemma OAI.KServer.FiniteExperiment.nu_nonneg line 348
lemma OAI.KServer.FiniteExperiment.nu_total line 354
lemma OAI.KServer.FiniteExperiment.nu_le_muBefore line 363
lemma OAI.KServer.FiniteExperiment.muBefore_total line 371
lemma OAI.KServer.FiniteExperiment.mu_move line 378
Source documentation
Exact one-mover decomposition used by the pilot potential.
```
lemma mu_move (s : Configuration k Y) (law : FiniteDistribution (Fin H → Y))
    (t : Fin H) (σ : Fin H → Y) (hσ : 0<law.val σ) (y : Y) :
    mu s law (t.val+1) σ y=muBefore s law t σ y-nu s law t σ y+
      (if σ t=y then 1 else 0) := by
…
```
Mentions: OAI.KServer.Configuration, OAI.KServer.FiniteDistribution, OAI.KServer.FiniteExperiment.mu, OAI.KServer.FiniteExperiment.muBefore, OAI.KServer.FiniteExperiment.nu
lemma OAI.KServer.FiniteExperiment.conditional_moveCost line 391
lemma OAI.KServer.FiniteExperiment.expected_moveCost line 410
Source documentation
The entire physical-drift budget is the expectation of the attained optimum, not a separate assumed bound or a policy-dependent comparator.
```
lemma expected_moveCost (s : Configuration k Y) (law : FiniteDistribution (Fin H → Y)) :
    (∑ t : Fin H,∑ σ,law.val σ*(∑ y,nu s law t σ y*dist y (σ t)))=
      ∑ σ,law.val σ*optimalCost s (List.ofFn σ) := by
…
```
Mentions: OAI.KServer.Configuration, OAI.KServer.FiniteDistribution, OAI.KServer.FiniteExperiment.nu