RationalRootBisection.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Fixed-depth rational bisection for the correction power of two

def OAI.ContingencyTables.RationalRootBisection.interval line 15
Source documentation
Every branch compares exact rational powers. The loop count is the explicit depth, independent of the comparison outcomes.
```
def interval (c : ℚ) (s : ℕ) : ℕ → ℚ × ℚ
  | 0 => (0,8)
  | n+1 =>
    let ab := interval c s n
…
```
def OAI.ContingencyTables.RationalRootBisection.midpoint line 22

theorem OAI.ContingencyTables.RationalRootBisection.interval_contains line 26

Source documentation

The target is used only in correctness, never by the algorithm.

theorem interval_contains (c : ℚ) (s : ℕ) (hs : 0 < s) (t : ℝ)
    (ht : 0 ≤ t) (ht8 : t ≤ 8) (hroot : t^s=(c:ℝ)) (n : ℕ) :
    0 ≤ ((interval c s n).1:ℝ) ∧ ((interval c s n).1:ℝ) ≤ t ∧
      t ≤ ((interval c s n).2:ℝ) ∧ ((interval c s n).2:ℝ) ≤ 8 := by
…

Mentions: OAI.ContingencyTables.RationalRootBisection.interval

lemma OAI.ContingencyTables.RationalRootBisection.interval_width line 60
theorem OAI.ContingencyTables.RationalRootBisection.midpoint_error line 74
Source documentation
A fixed depth yields an absolute error certificate for every rational power comparison path.
```
theorem midpoint_error (c : ℚ) (s : ℕ) (hs : 0 < s) (t : ℝ)
    (ht : 0 ≤ t) (ht8 : t ≤ 8) (hroot : t^s=(c:ℝ)) (n : ℕ) :
    |(midpoint c s n:ℝ)-t| ≤ 8/(2:ℝ)^n := by
…
```
Mentions: OAI.ContingencyTables.RationalRootBisection.midpoint