Main.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

One-tape simulation in two-fifths-power space, following OpenAI's “Simulating One-Tape Time in Two-Fifths-Power Space”. The capped and unknown-time bounds include all intermediate work storage and keep the accessor and simulator fixed independently of the input and time cap.

def OAI.Fifths.Single.Access line 20
Source documentation
Ordinary capped access condition. Log is binary (Cost.Log n = log base two of (n+2)). Real constants.
Also declared: ComparatorChallenges/OneTapeSpace.lean:246 (same declaration text).
```
def Access (A : M.Sym) (p q : ℝ) (x : List X) (T : ℕ) : Prop :=
…
```
Mentions: OAI.Fifths.Single.q
theorem OAI.Fifths.Single.accessed line 27
Source documentation
Widen all promised runs of the accessor to a pointwise integer bound. Parameter is integer so tight floors immaterial.
```
theorem accessed (A : M.Sym) (p q : ℝ) (hp : 1 ≤ p) :
    ∃ d c : ℕ, ∀ (x : List X) (T : ℕ), M.Access A p q x T →
      M.Gives A x T (c*(bound d T + 1)) := by
…
```
Mentions: OAI.Fifths.Single.q, OAI.Fifths.Single.c
theorem OAI.Fifths.Single.capped line 39
Source documentation
With binary cap as a separate read-only argument. Single simulator for all promised input/cap pairs. Real pointwise space bound (in particular a soft-O bound). exponent = 2/5.
Distinct definitions of this name: ComparatorChallenges/OneTapeSpace.lean:258 (same statement text; different proof or body). Qualify references as OAI.Fifths.Single.capped@path.
```
theorem capped [Fintype X] (A : M.Sym) (p q : ℝ) (hp : 1 ≤ p) (_hq : 1 ≤ q) :
    ∃ (N : TM X Unit M.Outcome) (e : ℕ) (c : ℝ), 0 < c ∧
      ∀ (x : List X) (T : ℕ), 2 ≤ T → M.Access A p q x T →
        ∃ b : ℕ, N.Within (binaryIn x (fun _ => T)) (M.outcome x T) b ∧
          (b:ℝ) ≤ c*(T:ℝ)^exponent*(Log T)^e := by
…
```
Mentions: OAI.Fifths.Single.q, OAI.Fifths.TM, OAI.Fifths.Single.c
theorem OAI.Fifths.Single.unknown line 64
Source documentation
Simulator with no cap input, an actual time t being used only to state the bound. If already halted at t, reports that outcome; under the promises, halts within the stated space.
Distinct definitions of this name: ComparatorChallenges/OneTapeSpace.lean:265 (same statement text; different proof or body). Qualify references as OAI.Fifths.Single.unknown@path.
```
theorem unknown [Fintype X] (A : M.Sym) (p q : ℝ) (hp : 1 ≤ p) (_hq : 1 ≤ q) :
    ∃ (N : TM X Empty M.Outcome) (e : ℕ) (c : ℝ), 0 < c ∧
      ∀ (x : List X), (∀ T, 2 ≤ T → M.Access A p q x T) →
        ∀ (t : ℕ), (M.outcome x t).2 = true →
          ∃ b, N.Within (files x) (M.outcome x t) b ∧
            (b:ℝ) ≤ c*((t:ℝ)+2)^exponent*(Log t)^e := by
…
```
Mentions: OAI.Fifths.Single.q, OAI.Fifths.TM, OAI.Fifths.Single.c