OAI/Combinatorics/UniformKServer/Basic.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

A concrete bit-machine model for the main conclusion. There is a fixed finite number of work tapes and finite control states, independent of the instance. The input tape is read-only. One transition reads one fresh unbiased bit and can output at most one bit. Halting/yielding stutters, allowing exact finite uniform averages without rejection sampling. A request installs only its own binary input word; it does not reveal either the horizon or the clock.

  1. structure OAI.UniformKServer.RationalMetric line 15

    Also declared: ComparatorChallenges/UniformKServer.lean:12 (same declaration text).

  2. abbrev OAI.UniformKServer.Configuration line 22

    Also declared: ComparatorChallenges/UniformKServer.lean:19 (same declaration text).

  3. abbrev OAI.UniformKServer.History line 23

    Also declared: ComparatorChallenges/UniformKServer.lean:20 (same declaration text).

  4. def OAI.UniformKServer.serve line 25

    Also declared: ComparatorChallenges/UniformKServer.lean:22 (same declaration text).

  5. def OAI.UniformKServer.costAlong line 28

    Also declared: ComparatorChallenges/UniformKServer.lean:25 (same declaration text).

  6. def OAI.UniformKServer.offlineCost line 34

    Source documentation

    All finite serving-label choices, knowing the entire request word.

    Also declared: ComparatorChallenges/UniformKServer.lean:31 (same declaration text).

    noncomputable def offlineCost {n k : ℕ} (d : RationalMetric n) (s : Configuration n k)
    (w : List (Fin n)) : ℝ :=
…

    Mentions: OAI.UniformKServer.RationalMetric, OAI.UniformKServer.Configuration

  7. structure OAI.UniformKServer.Policy line 40

    Source documentation

    A single online policy: its row depends on prior requests and choices and the current request, never on future requests or the horizon.

    structure Policy (n k : ℕ) where
…
  8. def OAI.UniformKServer.expectedCostFrom line 45
  9. inductive OAI.UniformKServer.HeadMove line 60

    Also declared: ComparatorChallenges/UniformKServer.lean:35 (same declaration text).

  10. structure OAI.UniformKServer.BitTape line 64

    Also declared: ComparatorChallenges/UniformKServer.lean:39 (same declaration text).

  11. def OAI.UniformKServer.BitTape.blank line 71

    Also declared: ComparatorChallenges/UniformKServer.lean:46 (same declaration text).

  12. def OAI.UniformKServer.BitTape.ofWord line 73

    Also declared: ComparatorChallenges/UniformKServer.lean:48 (same declaration text).

  13. def OAI.UniformKServer.BitTape.shift line 78

    Also declared: ComparatorChallenges/UniformKServer.lean:53 (same declaration text).

  14. structure OAI.UniformKServer.BitAction line 89

    Also declared: ComparatorChallenges/UniformKServer.lean:64 (same declaration text).

  15. structure OAI.UniformKServer.BitMachine line 97

    Also declared: ComparatorChallenges/UniformKServer.lean:72 (same declaration text).

  16. structure OAI.UniformKServer.MachineState line 104

    Also declared: ComparatorChallenges/UniformKServer.lean:79 (same declaration text).

  17. def OAI.UniformKServer.BitMachine.initial line 113

    Also declared: ComparatorChallenges/UniformKServer.lean:88 (same declaration text).

  18. def OAI.UniformKServer.BitMachine.step line 116

    Also declared: ComparatorChallenges/UniformKServer.lean:91 (same declaration text).

  19. def OAI.UniformKServer.BitMachine.run line 127

    Also declared: ComparatorChallenges/UniformKServer.lean:102 (same declaration text).

  20. def OAI.UniformKServer.BitMachine.install line 132

    Source documentation

    At a request boundary only the input/output interface is refreshed. Work tapes and control retain the complete internal state.

    Also declared: ComparatorChallenges/UniformKServer.lean:107 (same declaration text).

    def install (M : BitMachine) (s : MachineState M) (input : List Bool) : MachineState M :=
…

    Mentions: OAI.UniformKServer.BitMachine, OAI.UniformKServer.MachineState

  21. def OAI.UniformKServer.natCode line 140

    Source documentation

    Self-delimiting binary code: ℓ ones, a zero, then ℓ low-to-high bits. This fixes one standard binary encoding rather than allowing a nonuniform advice string to be included in the input.

    Also declared: ComparatorChallenges/UniformKServer.lean:115 (same declaration text).

    def natCode (a : ℕ) : List Bool :=
…
  22. def OAI.UniformKServer.rationalCode line 143

    Also declared: ComparatorChallenges/UniformKServer.lean:118 (same declaration text).

  23. def OAI.UniformKServer.instanceCode line 146

    Also declared: ComparatorChallenges/UniformKServer.lean:121 (same declaration text).

  24. def OAI.UniformKServer.bitValue line 152

    Also declared: ComparatorChallenges/UniformKServer.lean:127 (same declaration text).

  25. def OAI.UniformKServer.outputValue line 156

    Also declared: ComparatorChallenges/UniformKServer.lean:131 (same declaration text).

  26. def OAI.UniformKServer.polynomialBudget line 161

    Source documentation

    A dominating polynomial; every fixed polynomial nonnegative on natural inputs is bounded by one of this form after increasing c and e.

    Also declared: ComparatorChallenges/UniformKServer.lean:136 (same declaration text).

    def polynomialBudget (c e x : ℕ) : ℕ := c * (x + 1)^e
  27. def OAI.UniformKServer.requestBudget line 163

    Also declared: ComparatorChallenges/UniformKServer.lean:138 (same declaration text).

  28. def OAI.UniformKServer.boot line 166

    Also declared: ComparatorChallenges/UniformKServer.lean:141 (same declaration text).

  29. def OAI.UniformKServer.requestStep line 171

    Also declared: ComparatorChallenges/UniformKServer.lean:146 (same declaration text).

  30. inductive OAI.UniformKServer.Reachable line 178

    Source documentation

    Reachability includes every binary choice, not merely an almost-sure set. The index counts requests already served.

    Also declared: ComparatorChallenges/UniformKServer.lean:153 (same declaration text).

    inductive Reachable {n k : ℕ} (M : BitMachine) (c e : ℕ)
    (d : RationalMetric n) (s : Configuration n k) : ℕ → MachineState M → Prop
  | boot : Reachable M c e d s 0 (boot M c e d s)
  | next {t z} : Reachable M c e d s t z → (r : Fin n) →
      (bits : Fin (requestBudget c e (instanceCode d s).length (t+1)) → Bool) →
      Reachable M c e d s (t+1)
        (requestStep M c e (instanceCode d s).length (t+1) z r bits)

/-- Modulo makes the semantic recursion total even for unsuccessful machines.
    The main statement separately requires the output to be < k at *every*
    reachable outcome, so no invalid output is accepted or silently repaired. -/

    Mentions: OAI.UniformKServer.BitMachine, OAI.UniformKServer.RationalMetric, OAI.UniformKServer.Configuration, OAI.UniformKServer.MachineState, OAI.UniformKServer.boot, OAI.UniformKServer.requestBudget, OAI.UniformKServer.instanceCode, OAI.UniformKServer.requestStep

  31. def OAI.UniformKServer.selectedLabel line 189

    Source documentation

    Modulo makes the semantic recursion total even for unsuccessful machines. The main statement separately requires the output to be < k at every reachable outcome, so no invalid output is accepted or silently repaired.

    Also declared: ComparatorChallenges/UniformKServer.lean:164 (same declaration text).

    def selectedLabel {M : BitMachine} {k : ℕ} (hk : 0 < k) (s : MachineState M) : Fin k :=
…

    Mentions: OAI.UniformKServer.BitMachine, OAI.UniformKServer.MachineState

  32. def OAI.UniformKServer.machineExpectedCost line 192

    Also declared: ComparatorChallenges/UniformKServer.lean:167 (same declaration text).

  33. def OAI.UniformKServer.UniformAlgorithmClaim line 209

    Source documentation

    Full uniform main objective in the explicit bit model, not a theorem or assumption. Machine transition steps are bit operations. Installing the standard input and reading/erasing the output adds only O(L + budget) charged bit operations, hence is absorbed by a single larger polynomial. A single deterministic boot is sufficient for the source construction.

    Also declared: ComparatorChallenges/UniformKServer.lean:184 (same declaration text).

    def UniformAlgorithmClaim : Prop :=
…