Basic.lean`

24 declarations, 0 contain sorry, 0 declared as axioms

Section02's matching and strongly lazy simulation, including repeated positions and arbitrary metric spaces.

abbrev OAI.KServer.Configuration line 13
Source documentation
Labeled configurations; no injectivity condition, so repetitions are allowed.
Also declared: ComparatorChallenges/KServer.lean:13 (same declaration text).
```
abbrev Configuration (k : ℕ) (X : Type u) := Fin k → X
```
def OAI.KServer.LabelDistribution line 16
Source documentation
The finite probability simplex of the available server labels.
Distinct definitions of this name: ComparatorChallenges/KServer.lean:15 (same statement text; different proof or body). Qualify references as OAI.KServer.LabelDistribution@path.
```
def LabelDistribution (k : ℕ) :=
…
```
abbrev OAI.KServer.Policy line 22
Source documentation
A behavioral policy knows the entire past request/choice history and the new request. It is a single rule for all horizons. Pairing the past requests and choices is equivalent to the histories X^t × [k]^(t-1) in the manuscript.
Also declared: ComparatorChallenges/KServer.lean:19 (same declaration text).
```
abbrev Policy (k : ℕ) (X : Type u) :=
…
```
def OAI.KServer.serve line 26
Source documentation
Serve one request by moving exactly the indicated label to the request.
Distinct definitions of this name: ComparatorChallenges/KServer.lean:22 (different declaration text). Qualify references as OAI.KServer.serve@path.
```
def serve {k : ℕ} {X : Type u} (s : Configuration k X) (i : Fin k) (r : X) :
    Configuration k X := Function.update s i r
```
Mentions: OAI.KServer.Configuration

def OAI.KServer.serviceCost line 30

Source documentation

Deterministic movement of a label string on a fixed finite request sequence.

Distinct definitions of this name: ComparatorChallenges/KServer.lean:26 (different declaration text). Qualify references as OAI.KServer.serviceCost@path.

def serviceCost {k : ℕ} {X : Type u} [MetricSpace X] (s : Configuration k X) :
    (σ : List X) → (Fin σ.length → Fin k) → ℝ
  | [], _ => 0
  | r :: rs, j =>
      dist (s (j 0)) r + serviceCost (serve s (j 0) r) rs (fun i => j i.succ)

/-- Probability of a finite label string under the successive behavioral choices. -/

Mentions: OAI.KServer.Configuration

def OAI.KServer.pathProbability line 37

Source documentation

Probability of a finite label string under the successive behavioral choices.

Distinct definitions of this name: ComparatorChallenges/KServer.lean:33 (different declaration text). Qualify references as OAI.KServer.pathProbability@path.

def pathProbability {k : ℕ} {X : Type u} (A : Policy k X)
    (h : List (X × Fin k)) : (σ : List X) → (Fin σ.length → Fin k) → ℝ
  | [], _ => 1
  | r :: rs, j =>
      (A h r).val (j 0) * pathProbability A (h ++ [(r, j 0)]) rs (fun i => j i.succ)

/-- Exact finite expected total movement against an oblivious input. -/

Mentions: OAI.KServer.Policy

def OAI.KServer.expectedCost line 44
Source documentation
Exact finite expected total movement against an oblivious input.
Distinct definitions of this name: ComparatorChallenges/KServer.lean:42 (different declaration text). Qualify references as OAI.KServer.expectedCost@path.
```
def expectedCost {k : ℕ} {X : Type u} [MetricSpace X]
    (A : Policy k X) (s : Configuration k X) (σ : List X) : ℝ :=
…
```
Mentions: OAI.KServer.Policy, OAI.KServer.Configuration
def OAI.KServer.optimalCost line 51
Source documentation
Offline optimum over the finite set of all label strings. For k ≥ 2 this range is nonempty and finite, hence its real infimum is the attained minimum. There is no restriction on the metric itself.
Distinct definitions of this name: ComparatorChallenges/KServer.lean:47 (different declaration text). Qualify references as OAI.KServer.optimalCost@path.
```
def optimalCost {k : ℕ} {X : Type u} [MetricSpace X]
    (s : Configuration k X) (σ : List X) : ℝ :=
…
```
Mentions: OAI.KServer.Configuration
def OAI.KServer.ReductionStatement line 59
Source documentation
Literal main objective, with arbitrary universes, arbitrary metric spaces, repeated initial positions, and one policy and additive constant for all finite inputs. Real constants are finite; an embedding witnesses at least k+1 points. The final implication encodes availability of B=0 for distinct starts.
```
def ReductionStatement : Prop :=
…
```
instance OAI.KServer.(instance at line 73) line 73
instance OAI.KServer.(instance at line 77) line 77
def OAI.KServer.pureDistribution line 97
Source documentation
A pure choice, also used to fill unreachable decision histories.
```
def pureDistribution {k : ℕ} (i : Fin k) : LabelDistribution k :=
…
```
instance OAI.KServer.(instance at line 103) line 103
lemma OAI.KServer.serviceCost_nonneg line 106
lemma OAI.KServer.pathProbability_nonneg line 113

lemma OAI.KServer.sum_labelStrings line 121

Source documentation

Decompose a complete label string into its first decision and its tail.

lemma sum_labelStrings {k n : ℕ} (f : (Fin (n + 1) → Fin k) → ℝ) :
    ∑ j, f j = ∑ i : Fin k, ∑ js : Fin n → Fin k, f (Fin.cons i js) := by
…

lemma OAI.KServer.pathProbability_sum line 126
lemma OAI.KServer.expectedCost_nonneg line 138
lemma OAI.KServer.continuous_pathProbability line 144
lemma OAI.KServer.continuous_expectedCost line 158
Source documentation
Equation (cost-polynomial): a fixed finite input has continuous expected cost on the full, possibly infinite, product of decision simplexes.
```
lemma continuous_expectedCost {k : ℕ} {X : Type u} [MetricSpace X]
    (s : Configuration k X) (σ : List X) :
    Continuous fun A : Policy k X => expectedCost A s σ := by
…
```
Mentions: OAI.KServer.Configuration, OAI.KServer.Policy
theorem OAI.KServer.compact_policy_of_finite_feasibility line 167
Source documentation
The topological step of Lemma compact-policy. The finite feasibility premise is the remaining quantitative obligation, not asserted here. This lemma does not use finite/bounded/discrete assumptions on the request space.
```
theorem compact_policy_of_finite_feasibility {k : ℕ} {X : Type u} [MetricSpace X]
    (s : Configuration k X) (bound : List X → ℝ)
    (hfinite : ∀ F : Finset (List X), ∃ A : Policy k X,
      ∀ σ ∈ F, expectedCost A s σ  ≤  bound σ) :
    ∃ A : Policy k X, ∀ σ : List X, expectedCost A s σ  ≤  bound σ := by
…
```
Mentions: OAI.KServer.Configuration, OAI.KServer.Policy
def OAI.KServer.configurationAfter line 185
def OAI.KServer.StronglyLazy line 189
lemma OAI.KServer.configurationAfter_append line 193