OAI/Combinatorics/KServer/Behavior.lean

GitHub source file

112 declarations, 0 contain sorry, 0 declared as axioms

Explicit causal realization of finite hidden-state algorithms.

This discharges a policy-existence interface needed both by correlated rounding and by the fictitious-prefix episode extraction. It is not a competitiveness premise: the machine below is arbitrary and its behavioral policy is constructed.

  1. def OAI.KServer.matchSum line 14
  2. lemma OAI.KServer.exists_minimum_matching line 17
  3. def OAI.KServer.matchingPerm line 23
  4. def OAI.KServer.matching line 26
  5. lemma OAI.KServer.matching_le line 28
  6. lemma OAI.KServer.matching_nonneg line 32
  7. lemma OAI.KServer.matching_self line 36
  8. lemma OAI.KServer.matching_triangle line 40
  9. lemma OAI.KServer.matching_symmetric line 54
  10. lemma OAI.KServer.matchSum_serve line 66
  11. def OAI.KServer.lazyChoice line 83

    Source documentation

    A causal minimum-matching choice. Repeated actual and virtual positions are retained: only the permutation of occurrence labels is used.

    def lazyChoice (A C : Configuration k X) (r : X) (hc : ∃ i, C i = r) : Fin k := by
…

    Mentions: OAI.KServer.Configuration

  12. lemma OAI.KServer.lazyChoice_covered line 87
  13. lemma OAI.KServer.lazyChoice_cost line 92
  14. def OAI.KServer.continuationCost line 118

    Source documentation

    Expected continuation from a specified (possibly null) history.

    def continuationCost {k : ℕ} {X : Type u} [MetricSpace X]
    (A : Policy k X) (s : Configuration k X) (h : List (X × Fin k)) (σ : List X) : ℝ :=
…

    Mentions: OAI.KServer.Policy, OAI.KServer.Configuration

  15. lemma OAI.KServer.continuationCost_nil line 122
  16. lemma OAI.KServer.continuationCost_cons line 126
  17. def OAI.KServer.lazySimulation line 151
  18. lemma OAI.KServer.lazySimulation_strong line 155
  19. def OAI.KServer.simulatedMovement line 165

    Source documentation

    Simulated movement measured by occurrence matching, exactly Section02.

    def simulatedMovement (C : List X → Configuration k X) (pre : List X) : List X → ℝ
  | [] => 0
  | r :: σ => matching (C pre) (C (pre ++ [r])) + simulatedMovement C (pre ++ [r]) σ

    Mentions: OAI.KServer.Configuration, OAI.KServer.matching

  20. lemma OAI.KServer.lazySimulation_bound line 169
  21. theorem OAI.KServer.causal_lazy_simulation line 203

    Source documentation

    Actual policy exists, is strongly lazy, and obeys the matching potential bound for every finite horizon under one common causal rule. No distributional input or future knowledge is used. This is the deterministic/private-seed kernel of source lem:lazy-simulation.

    theorem causal_lazy_simulation :
    StronglyLazy start (lazySimulation start C hcover) ∧
      ∀ σ, expectedCost (lazySimulation start C hcover) start σ  ≤ 
        matching start (C []) + simulatedMovement C [] σ := by
…

    Mentions: OAI.KServer.StronglyLazy, OAI.KServer.lazySimulation, OAI.KServer.matching, OAI.KServer.simulatedMovement

  22. lemma OAI.KServer.optimalCost_le_service line 219
  23. lemma OAI.KServer.optimalCost_nonneg line 223
  24. lemma OAI.KServer.optimalCost_attained line 226
  25. lemma OAI.KServer.matching_serve_le line 236
  26. theorem OAI.KServer.offline_lazy_comparison line 247

    Source documentation

    Source lazy simulation applied purely pathwise, without a causality premise; this is the comparison needed for repeated initial tuples.

    theorem offline_lazy_comparison (A C : Configuration k X) (σ : List X)
    (j : Fin σ.length → Fin k) :
    ∃ w : Fin σ.length → Fin k,
      serviceCost A σ w  ≤  matching A C + serviceCost C σ j := by
…

    Mentions: OAI.KServer.Configuration, OAI.KServer.matching

  27. theorem OAI.KServer.optimalCost_change_start line 272

    Source documentation

    Exact source bound OPT_t ≤ OPT_s + M(s,t); no distinctness is used.

    theorem optimalCost_change_start (s t : Configuration k X) (σ : List X) :
    optimalCost t σ  ≤  optimalCost s σ + matching s t := by
…

    Mentions: OAI.KServer.Configuration, OAI.KServer.matching

  28. lemma OAI.KServer.optimalCost_le_expectedCost line 281
  29. def OAI.KServer.historyProbability line 291
  30. lemma OAI.KServer.historyProbability_nonneg line 296
  31. lemma OAI.KServer.historyProbability_append line 302
  32. lemma OAI.KServer.historyProbability_singleton line 312
  33. structure OAI.KServer.HiddenMachine.Data line 326
  34. def OAI.KServer.HiddenMachine.step line 338
  35. def OAI.KServer.HiddenMachine.evolve line 341
  36. def OAI.KServer.HiddenMachine.weights line 345
  37. def OAI.KServer.HiddenMachine.mass line 347
  38. def OAI.KServer.HiddenMachine.outMass line 349
  39. lemma OAI.KServer.HiddenMachine.step_nonneg line 352
  40. lemma OAI.KServer.HiddenMachine.evolve_nonneg line 359
  41. lemma OAI.KServer.HiddenMachine.weights_nonneg line 365
  42. lemma OAI.KServer.HiddenMachine.mass_nonneg line 368
  43. lemma OAI.KServer.HiddenMachine.outMass_nonneg line 371
  44. lemma OAI.KServer.HiddenMachine.evolve_append line 374
  45. lemma OAI.KServer.HiddenMachine.weights_append line 383
  46. lemma OAI.KServer.HiddenMachine.mass_append line 388
  47. lemma OAI.KServer.HiddenMachine.step_sum line 392
  48. lemma OAI.KServer.HiddenMachine.outMass_sum line 407
  49. lemma OAI.KServer.HiddenMachine.outMass_le_mass line 410
  50. def OAI.KServer.HiddenMachine.policy line 416

    Source documentation

    Null histories are filled by a fixed legal label, not by any future input.

    def policy : Policy k X := fun h r =>
…

    Mentions: OAI.KServer.Policy

  51. lemma OAI.KServer.HiddenMachine.mass_mul_policy line 424
  52. theorem OAI.KServer.HiddenMachine.history_law line 435

    Source documentation

    Exact finite-history law of the realized behavioral policy.

    theorem history_law (h : List (X × Fin k)) :
    historyProbability (policy M) [] h=mass M h := by
…

    Mentions: OAI.KServer.historyProbability, OAI.KServer.HiddenMachine.policy, OAI.KServer.HiddenMachine.mass

  53. def OAI.KServer.HiddenMachine.machineCost line 447

    Source documentation

    The machine's literal finite expected movement, prior to forgetting its private state. Physical configurations are determined by visible histories.

    def machineCost (start : Configuration k X) (h : List (X × Fin k)) (s : S) :
    List X → ℝ
  | [] => 0
  | r::σ => ∑ s', M.transition h r s s' *
      (dist (configurationAfter start h (M.output h r s s')) r +
        machineCost start (h++[(r,M.output h r s s')]) s' σ)

    Mentions: OAI.KServer.Configuration, OAI.KServer.configurationAfter

  54. lemma OAI.KServer.HiddenMachine.machineCost_nonneg line 454
  55. lemma OAI.KServer.HiddenMachine.branch_sum line 465

    Source documentation

    Weighted branch disintegration; a finite algebraic identity, including zero-likelihood branches, rather than an assumed conditional kernel.

    lemma branch_sum (h : List (X × Fin k)) (r : X) (w : S → ℝ)
    (f : Fin k → S → ℝ) :
    (∑ i : Fin k, ∑ s', step M h r i w s' * f i s') =
      ∑ s, w s * ∑ s', M.transition h r s s' * f (M.output h r s s') s' := by
…

    Mentions: OAI.KServer.HiddenMachine.step

  56. theorem OAI.KServer.HiddenMachine.realization_cost line 483

    Source documentation

    Forgetting a finite private state preserves exactly all finite expected costs. No finite-horizon policy family is identified without constructing its single behavioral continuation.

    theorem realization_cost (start : Configuration k X) (h : List (X × Fin k))
    (σ : List X) :
    mass M h * continuationCost (policy M) (configurationAfter start h) h σ =
      ∑ s, weights M h s * machineCost M start h s σ := by
…

    Mentions: OAI.KServer.Configuration, OAI.KServer.HiddenMachine.mass, OAI.KServer.continuationCost, OAI.KServer.HiddenMachine.policy, OAI.KServer.configurationAfter, OAI.KServer.HiddenMachine.weights, OAI.KServer.HiddenMachine.machineCost

  57. theorem OAI.KServer.HiddenMachine.exists_realization line 509

    Source documentation

    The requested externally visible policy, valid on every finite horizon.

    theorem exists_realization (start : Configuration k X) :
    ∃ A : Policy k X, ∀ σ : List X,
      expectedCost A start σ = ∑ s, M.initial s * machineCost M start [] s σ := by
…

    Mentions: OAI.KServer.Configuration, OAI.KServer.Policy, OAI.KServer.HiddenMachine.machineCost

  58. lemma OAI.KServer.HiddenMachine.policy_strong line 520
  59. def OAI.KServer.HiddenMachine.lazyFallback line 542

    Source documentation

    A null-history fallback that satisfies strong laziness at every history.

    def lazyFallback (start : Configuration k X) (h : List (X × Fin k)) (r : X) : Fin k := by
…

    Mentions: OAI.KServer.Configuration

  60. lemma OAI.KServer.HiddenMachine.lazyFallback_covered line 547
  61. def OAI.KServer.HiddenMachine.lazyMachine line 558

    Source documentation

    Source's matching simulation, with the entire virtual private state kept. There is no illegal conditioning of a marginal coupling on realized ancestors.

    def lazyMachine : Data k X S where
…

    Mentions: OAI.KServer.HiddenMachine.Data

  62. lemma OAI.KServer.HiddenMachine.lazyMachine_strong line 569
  63. def OAI.KServer.HiddenMachine.virtualCost line 576

    Source documentation

    Virtual movement under exactly the same finite hidden-state experiment.

    def virtualCost (h : List (X × Fin k)) (s : S) : List X → ℝ
  | [] => 0
  | r::σ => ∑ s', M.transition h r s s' *
      (matching (V (h.map Prod.fst) s) (V (h.map Prod.fst++[r]) s')+
        virtualCost (h++[(r,(lazyMachine M start V hcover).output h r s s')]) s' σ)

    Mentions: OAI.KServer.matching, OAI.KServer.HiddenMachine.lazyMachine

  64. lemma OAI.KServer.HiddenMachine.lazyMachine_bound line 582
  65. theorem OAI.KServer.HiddenMachine.causal_random_lazy_simulation line 621

    Source documentation

    Fully constructed randomized causal strong-lazy simulation with arbitrary finite correlated private states and an arbitrary initial virtual mismatch. It is uniform over all fixed finite request sequences, including all horizons.

    theorem causal_random_lazy_simulation :
    ∃ A : Policy k X, StronglyLazy start A ∧ ∀ σ : List X,
      expectedCost A start σ  ≤ 
        (∑ s, M.initial s*matching start (V [] s))+
          ∑ s, M.initial s*virtualCost M start V hcover [] s σ := by
…

    Mentions: OAI.KServer.Policy, OAI.KServer.StronglyLazy, OAI.KServer.matching, OAI.KServer.HiddenMachine.virtualCost

  66. abbrev OAI.KServer.BoundedSimulation.Memory line 655

    Source documentation

    Finite private memory, sufficient for a fixed local experiment. The final policy is extended to all requests; compactness below removes this bound.

    abbrev Memory (H k : ℕ) := Fin H → Fin k
  67. def OAI.KServer.BoundedSimulation.labelAt line 657
  68. def OAI.KServer.BoundedSimulation.history line 660
  69. lemma OAI.KServer.BoundedSimulation.history_append line 663
  70. lemma OAI.KServer.BoundedSimulation.history_length line 667
  71. def OAI.KServer.BoundedSimulation.update line 670
  72. lemma OAI.KServer.BoundedSimulation.labelAt_update line 674
  73. lemma OAI.KServer.BoundedSimulation.history_update line 679
  74. lemma OAI.KServer.BoundedSimulation.history_step line 693
  75. def OAI.KServer.BoundedSimulation.transition line 700
  76. lemma OAI.KServer.BoundedSimulation.transition_sum line 703
  77. lemma OAI.KServer.BoundedSimulation.transition_integrate line 710
  78. def OAI.KServer.BoundedSimulation.machine line 719
  79. def OAI.KServer.BoundedSimulation.virtual line 737
  80. lemma OAI.KServer.BoundedSimulation.virtual_covers line 740
  81. lemma OAI.KServer.BoundedSimulation.virtual_step line 745
  82. lemma OAI.KServer.BoundedSimulation.virtual_cost_bound line 756

    Source documentation

    Exact virtual continuation bound, honoring the entire private label history. In particular the virtual policy is not falsely conditioned only on the real server positions or on the current request.

    lemma virtual_cost_bound (h : List (X × Fin k)) (s : Memory H k) (σ : List X)
    (hb : h.length+σ.length ≤ H) :
    HiddenMachine.virtualCost (machine H A pre) start (virtual H virtualStart)
      (virtual_covers H virtualStart) h s σ  ≤ 
    continuationCost A (virtual H virtualStart (h.map Prod.fst) s)
      (pre++history (h.map Prod.fst) s) σ := by
…

    Mentions: OAI.KServer.BoundedSimulation.Memory, OAI.KServer.HiddenMachine.virtualCost, OAI.KServer.BoundedSimulation.machine, OAI.KServer.BoundedSimulation.virtual, OAI.KServer.BoundedSimulation.virtual_covers, OAI.KServer.continuationCost, OAI.KServer.BoundedSimulation.history

  83. theorem OAI.KServer.BoundedSimulation.finite_horizon_simulation line 797

    Source documentation

    Realizes a supplied behavioral policy from a different actual start, up to any prescribed finite horizon; its construction is causal on all histories. The bound is uniform in the horizon, permitting the global compactness step.

    theorem finite_horizon_simulation :
    ∃ B : Policy k X, StronglyLazy start B ∧ ∀ σ : List X, σ.length ≤ H →
      expectedCost B start σ  ≤  matching start virtualStart+
        continuationCost A virtualStart pre σ := by
…

    Mentions: OAI.KServer.Policy, OAI.KServer.StronglyLazy, OAI.KServer.matching, OAI.KServer.continuationCost

  84. theorem OAI.KServer.BoundedSimulation.global_simulation line 817

    Source documentation

    One global causal simulator on an arbitrary metric. The finite-memory constructions above incur the same initial matching, so compactness selects a single policy valid for every finite horizon. No finiteness of X is required.

    theorem global_simulation :
    ∃ B : Policy k X, ∀ σ : List X,
      expectedCost B start σ  ≤  matching start virtualStart+
        continuationCost A virtualStart pre σ := by
…

    Mentions: OAI.KServer.Policy, OAI.KServer.matching, OAI.KServer.continuationCost

  85. def OAI.KServer.mixtureLikelihood line 838
  86. lemma OAI.KServer.mixtureLikelihood_nonneg line 842
  87. lemma OAI.KServer.weightedLikelihood_le line 847
  88. lemma OAI.KServer.mixtureLikelihood_append line 852
  89. def OAI.KServer.mixturePolicy line 865

    Source documentation

    The posterior distribution over the private mixture index is normalized only at reached histories; all null histories receive the same fixed pure rule.

    def mixturePolicy : Policy k X := fun h r =>
…

    Mentions: OAI.KServer.Policy

  90. lemma OAI.KServer.mixturePolicy_recurrence line 879
  91. lemma OAI.KServer.historyProbability_mixture line 898
  92. lemma OAI.KServer.historyProbability_ofFn line 906
  93. theorem OAI.KServer.pathProbability_mixture line 919
  94. theorem OAI.KServer.expectedCost_mixture line 928
  95. lemma OAI.KServer.exists_binary_mixture line 945

    Source documentation

    One private coin implements a convex combination simultaneously for all inputs.

    lemma exists_binary_mixture (s : Configuration k X) (A B : Policy k X)
    (a b : ℝ) (ha : 0  ≤  a) (hb : 0  ≤  b) (hab : a + b = 1) :
    ∃ D : Policy k X, ∀ σ, expectedCost D s σ =
      a * expectedCost A s σ + b * expectedCost B s σ := by
…

    Mentions: OAI.KServer.Configuration, OAI.KServer.Policy

  96. theorem OAI.KServer.nonpositive_vector_of_distributional line 961

    Source documentation

    The finite convex-separation implication used in source Lemma finite-set. Its premise is an explicit distributional estimate, not an assumed online policy existence theorem. The lemma itself is an unconditional convex-geometric fact.

    theorem nonpositive_vector_of_distributional {ι : Type*} [Fintype ι]
    (S : Set (ι → ℝ)) (hne : S.Nonempty) (hcmp : IsCompact S) (hconv : Convex ℝ S)
    (hdist : ∀ w : ι → ℝ, (∀ i, 0  ≤  w i) → (∑ i, w i = 1) →
      ∃ v ∈ S, ∑ i, w i * v i  ≤  0) :
    ∃ v ∈ S, ∀ i, v i  ≤  0 := by
…
  97. theorem OAI.KServer.finite_policy_of_distributional line 1044

    Source documentation

    Source finite-set separation, directly on the compact behavioral policy space. Finite random-seed conversion proved above supplies its convexity.

    theorem finite_policy_of_distributional {ι : Type*} [Fintype ι]
    (s : Configuration k X) (σ : ι → List X) (bound : ι → ℝ)
    (hdist : ∀ w : ι → ℝ, (∀ i, 0  ≤  w i) → (∑ i, w i = 1) →
      ∃ A : Policy k X, ∑ i, w i * expectedCost A s (σ i)  ≤  ∑ i, w i * bound i) :
    ∃ A : Policy k X, ∀ i, expectedCost A s (σ i)  ≤  bound i := by
…

    Mentions: OAI.KServer.Configuration, OAI.KServer.Policy

  98. theorem OAI.KServer.global_policy_of_finite_laws line 1078

    Source documentation

    Quantifier-exact combination of finite separation and product compactness. No law-dependent or horizon-dependent policy is silently asserted: the entire quantitative distributional premise is displayed, and remains to be obtained from the new finite-law construction and amplification.

    theorem global_policy_of_finite_laws {k : ℕ} [NeZero k] {X : Type u} [MetricSpace X]
    (s : Configuration k X) (bound : List X → ℝ)
    (hdist : ∀ F : Finset (List X), ∀ w : F → ℝ,
      (∀ i, 0  ≤  w i) → (∑ i, w i = 1) →
      ∃ A : Policy k X, ∑ i : F, w i * expectedCost A s i.val  ≤ 
        ∑ i : F, w i * bound i.val) :
    ∃ A : Policy k X, ∀ σ, expectedCost A s σ  ≤  bound σ := by
…

    Mentions: OAI.KServer.Configuration, OAI.KServer.Policy

  99. def OAI.KServer.mapHistory line 1100

    Source documentation

    Relabeling requests, leaving server labels unchanged.

    def mapHistory {k : ℕ} {X : Type u} {Y : Type v} (f : X → Y)
    (h : List (X × Fin k)) : List (Y × Fin k) := h.map (fun p => (f p.1,p.2))
  100. lemma OAI.KServer.mapHistory_comp line 1103
  101. lemma OAI.KServer.mapHistory_id line 1108
  102. lemma OAI.KServer.map_serve line 1111
  103. lemma OAI.KServer.serviceCost_map line 1120

    Source documentation

    Executing an identical label string through an isometry preserves every individual path cost, without any assumption on the ambient metric.

    lemma serviceCost_map {k : ℕ} {X : Type u} {Y : Type v}
    [MetricSpace X] [MetricSpace Y] (f : X → Y) (hf : Isometry f)
    (s : Configuration k X) (σ : List X) (j : Fin σ.length → Fin k) :
    serviceCost (f ∘ s) (σ.map f) (fun i => j ⟨i.val,by simpa using i.isLt⟩) =
      serviceCost s σ j := by
…

    Mentions: OAI.KServer.Configuration

  104. def OAI.KServer.retractPolicy line 1137

    Source documentation

    Ambient extension by a retraction. The extension is deliberately arbitrary on requests outside the finite submetric, while agreeing exactly on all its histories. It is one policy, not a collection indexed by horizons.

    def retractPolicy {k : ℕ} {X : Type u} {Y : Type v}
    (f : X → Y) (A : Policy k Y) : Policy k X :=
…

    Mentions: OAI.KServer.Policy

  105. lemma OAI.KServer.pathProbability_retract line 1141
  106. lemma OAI.KServer.expectedCost_retract line 1163
  107. lemma OAI.KServer.optimalCost_map line 1180
  108. def OAI.KServer.FiniteDistinctLawBound line 1199

    Source documentation

    The exact conclusion needed from source §10's episode amplification, on finite metrics only. This definition is an open obligation, not an assumption asserted by the development, and is not the main theorem.

    def FiniteDistinctLawBound (k : ℕ) (α : ℝ) : Prop :=
…
  109. theorem OAI.KServer.distinct_policy_from_finite_submetrics line 1210

    Source documentation

    Every finite family of requests lies in an actual finite submetric. Metric restriction preserves the finite laws, movement costs and offline minima needed for product compactness.

    theorem distinct_policy_from_finite_submetrics {k : ℕ} [NeZero k]
    (α : ℝ) (hfinite : FiniteDistinctLawBound.{u} k α)
    {X : Type u} [MetricSpace X] (s : Configuration k X) (hs : Function.Injective s) :
    ∃ A : Policy k X, ∀ σ, expectedCost A s σ  ≤  α*optimalCost s σ := by
…

    Mentions: OAI.KServer.Configuration, OAI.KServer.Policy

  110. theorem OAI.KServer.repeat_start_transfer line 1267

    Source documentation

    Source §10, repeated initial positions. This is a proved transformation of policies, not a competitiveness assumption: the sole input is the virtual policy's actual bound, and the real policy is constructed by finite filtering and compactness above. Its additive constant is independent of every input.

    theorem repeat_start_transfer {k : ℕ} [NeZero k] {X : Type u} [MetricSpace X]
    (s u : Configuration k X) (α : ℝ) (hα : 0 ≤ α)
    (A : Policy k X) (hA : ∀ σ, expectedCost A u σ ≤ α*optimalCost u σ) :
    ∃ B : Policy k X, ∀ σ,
      expectedCost B s σ  ≤  α*optimalCost s σ+(α+1)*matching s u := by
…

    Mentions: OAI.KServer.Configuration, OAI.KServer.Policy, OAI.KServer.matching

  111. lemma OAI.KServer.source_log_comparison line 1279
  112. theorem OAI.KServer.main_reduction line 1289

    Source documentation

    Arbitrary-metric transfer and repeated starting positions reduce the competitive estimate to a finite amplified-law bound, with constants uniform over all request horizons.

    theorem main_reduction :
    (∃ d : ℝ, 0 ≤ d ∧ ∀ k : ℕ, 2 ≤ k →
      FiniteDistinctLawBound.{u} k (d*(1+Real.log (k+1))^2)) → ReductionStatement.{u} := by
…