The outer piece table on [20/37, 3]

The interval and coefficient data originate in gen_lean_outer.py. Each piece proves its minimum and maximum comparisons once, then reuses them in the interval-count formulas. This avoids repeated case splits and arithmetic preprocessing of earlier count equations.

theorem Zeta5Irrational.outPiece_0 (x : ℝ) (h1 : 20 / 37 ≤ x) (h2 : x < 40 / 43) : Eout x = 37 / 20 * x + -1

theorem Zeta5Irrational.outPiece_1 (x : ℝ) (h1 : 40 / 43 ≤ x) (h2 : x < 1) : Eout x = 37 / 20 * x + -1

theorem Zeta5Irrational.outPiece_2 (x : ℝ) (h1 : 1 ≤ x) (h2 : x < 40 / 37) : Eout x = 1 * x + -2

theorem Zeta5Irrational.outPiece_3 (x : ℝ) (h1 : 40 / 37 ≤ x) (h2 : x < 3 / 2) : Eout x = 42 / 5 * x + -10

theorem Zeta5Irrational.outPiece_4 (x : ℝ) (h1 : 3 / 2 ≤ x) (h2 : x < 20 / 13) : Eout x = 42 / 5 * x + -10

theorem Zeta5Irrational.outPiece_5 (x : ℝ) (h1 : 20 / 13 ≤ x) (h2 : x < 60 / 37) : Eout x = 97 / 10 * x + -12

theorem Zeta5Irrational.outPiece_6 (x : ℝ) (h1 : 60 / 37 ≤ x) (h2 : x < 80 / 43) : Eout x = 231 / 20 * x + -15

theorem Zeta5Irrational.outPiece_7 (x : ℝ) (h1 : 80 / 43 ≤ x) (h2 : x < 2) : Eout x = 51 / 10 * x + -3

theorem Zeta5Irrational.outPiece_8 (x : ℝ) (h1 : 2 ≤ x) (h2 : x < 80 / 37) : Eout x = 17 / 4 * x + -5

theorem Zeta5Irrational.outPiece_9 (x : ℝ) (h1 : 80 / 37 ≤ x) (h2 : x < 5 / 2) : Eout x = 429 / 40 * x + -19

theorem Zeta5Irrational.outPiece_10 (x : ℝ) (h1 : 5 / 2 ≤ x) (h2 : x < 100 / 37) : Eout x = 429 / 40 * x + -19

theorem Zeta5Irrational.outPiece_11 (x : ℝ) (h1 : 100 / 37 ≤ x) (h2 : x < 120 / 43) : Eout x = 503 / 40 * x + -24

theorem Zeta5Irrational.outPiece_12 (x : ℝ) (h1 : 120 / 43 ≤ x) (h2 : x < 3) : Eout x = 36 / 5 * x + -9

def Zeta5Irrational.tOutL : List ℚ

The 14 rational endpoints of the 13 outer-range linear pieces.

Equations

• Zeta5Irrational.tOutL = [20 / 37, 40 / 43, 1, 40 / 37, 3 / 2, 20 / 13, 60 / 37, 80 / 43, 2, 80 / 37, 5 / 2, 100 / 37, 120 / 43, 3]

def Zeta5Irrational.aOutL : List ℚ

Rational slopes of the 13 outer-range linear pieces.

Equations

• Zeta5Irrational.aOutL = [37 / 20, 37 / 20, 1, 42 / 5, 42 / 5, 97 / 10, 231 / 20, 51 / 10, 17 / 4, 429 / 40, 429 / 40, 503 / 40, 36 / 5]

def Zeta5Irrational.bOutL : List ℚ

Rational intercepts of the 13 outer-range linear pieces.

Equations

• Zeta5Irrational.bOutL = [-1, -1, -2, -10, -10, -12, -15, -3, -5, -19, -19, -24, -9]

noncomputable def Zeta5Irrational.tOut (i : ℕ) : ℝ

The ith outer-range endpoint as a real number; zero outside the table.

Equations

• Zeta5Irrational.tOut i = ↑(Zeta5Irrational.tOutL.getD i 0)

noncomputable def Zeta5Irrational.gOut (i : ℕ) (x : ℝ) : ℝ

The affine bound on outer piece i, with coefficients from aOutL and bOutL.

Equations

• Zeta5Irrational.gOut i x = ↑(Zeta5Irrational.aOutL.getD i 0) * x + ↑(Zeta5Irrational.bOutL.getD i 0)

theorem Zeta5Irrational.tOut_mono (i : ℕ) : i < 13 → tOut i < tOut (i + 1)

theorem Zeta5Irrational.outer_table (i : ℕ) : i < 13 → ∀ x ∈ Set.Ico (tOut i) (tOut (i + 1)), Eout x = gOut i x