TerminalFiniteBudget.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.TerminalAssembly.terminalCoefficient line 10
Source documentation
The fixed coefficient in the constructive terminal length estimate.
```
def terminalCoefficient (D α : ℝ) : ℝ :=
…
```
Mentions: OAI.Problem337.D
theorem OAI.Problem337.TerminalAssembly.terminalCoefficient_pos line 13

theorem OAI.Problem337.TerminalAssembly.ceiling_length_add_depth line 23

Source documentation

Rounding the terminal budget costs at most one extra logarithmic unit.

theorem ceiling_length_add_depth {B K S : ℝ} {d : ℕ}
    (hB : 0 ≤ B) (hlog : 1 ≤ Real.log S)
    (hd : (d : ℝ) ≤ K * Real.log S) :
    ((⌈B * Real.log S⌉₊ + d : ℕ) : ℝ) ≤ (B + K + 1) * Real.log S := by
…

theorem OAI.Problem337.TerminalAssembly.terminal_finite_expansions line 34

Source documentation

Direct finite-tuple terminal data for a real cutoff. The residue hypothesis is the genuine arithmetic input; no intermediate expansions are assumed.

theorem terminal_finite_expansions
    (M : ℕ) (X D α S : ℝ) (hX : 0 ≤ X)
    (hXM : X < (M : ℝ)) (hXS : X ≤ Real.exp S)
    (hD : 1 ≤ D) (hα : 0 < α) (hα1 : α < 1)
    (hS : 1 ≤ S) (hlogS : 1 ≤ Real.log S)
    (hdiv : 2 ^ TerminalDepth.binaryExponent D S ∣ M)
    (hstep : ∀ u : ℕ, (u : ℝ) ≤ X → S ^ D < (u : ℝ) →
      ∃ t z h : ℕ, 0 < t ∧ 0 < z ∧ t ∣ M ∧
        (h : ℝ) ≤ (u : ℝ) ^ α ∧ t + h = u * z) :
    ∀ u ∈ Finset.Icc 1 ⌊X⌋₊,
      Descent.UnitListAtMost ((u : ℚ) / M)
        ⌈terminalCoefficient D α * Real.log S⌉₊ := by
…

Mentions: OAI.Problem337.D, OAI.Problem337.TerminalDepth.binaryExponent, OAI.Problem337.Descent.UnitListAtMost, OAI.Problem337.TerminalAssembly.terminalCoefficient

theorem OAI.Problem337.TerminalAssembly.terminal_finite_total_budget line 65

Source documentation

The terminal tuple budget together with all backward levels remains logarithmic, with one explicit coefficient independent of the cutoff.

theorem terminal_finite_total_budget {D α K S : ℝ} {d : ℕ}
    (hD : 1 ≤ D) (hα : 0 < α) (hα1 : α < 1)
    (hlogS : 1 ≤ Real.log S) (hd : (d : ℝ) ≤ K * Real.log S) :
    ((⌈terminalCoefficient D α * Real.log S⌉₊ + d : ℕ) : ℝ) ≤
      (terminalCoefficient D α + K + 1) * Real.log S :=
…

Mentions: OAI.Problem337.D, OAI.Problem337.TerminalAssembly.terminalCoefficient