Base-case classification for the Rhin-Viola Lemma 3 descent

Proved

RhinViola.lemma3BaseCaseClassification

by WillR · Oct 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

arithmetic-bridgebase-caseslemma-3natural-arithmeticrhin-violawell-founded

Under the balance nu+r=k+l, if at least one of k,l,nu,r vanishes then the Lemma 3 recursion is in one of the paper's base configurations: nu=0 (Lemma 1); l=0 with nu≤k (J1); k=0 with nu≤l (J1 after swapping variables); or r=0 with positive k,l, where nu=k+l and both k,l are strictly smaller than nu (J2).

Preamble

import Mathlib.Tactic

Formal statement

theorem RhinViola.lemma3BaseCaseClassification
    (k l nu r : ℕ) (hbal : nu + r = k + l)
    (hzero : k = 0 ∨ l = 0 ∨ nu = 0 ∨ r = 0) :
    nu = 0 ∨
      (l = 0 ∧ nu ≤ k) ∨
      (k = 0 ∧ nu ≤ l) ∨
      (r = 0 ∧ 0 < k ∧ 0 < l ∧ nu = k + l ∧ k < nu ∧ l < nu) := by sorry

Source

G. Rhin and C. Viola, On the irrationality measure of zeta(2), Annales de l'Institut Fourier 43 (1993), Lemmas 1-3, pp. 87-90.

View graph