Natural-number descent for the three Rhin-Viola Lemma 3 branches

Proved

RhinViola.lemma3RecurrenceDescent

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

arithmetic-bridgelemma-3natural-arithmeticrhin-violaterminationwell-founded

Write r=k+l-nu. When all four quantities k,l,nu,r are positive, each of the three recursive branches in Rhin-Viola Lemma 3 preserves the balance nu+r=k+l and strictly decreases the total measure k+l+nu+r. This supplies a simple well-founded descent certificate for the paper's statement that repeated application terminates.

Preamble

import Mathlib.Tactic

Formal statement

theorem RhinViola.lemma3RecurrenceDescent
    (k l nu r : ℕ)
    (hk : 0 < k) (hl : 0 < l) (hnu : 0 < nu) (hr : 0 < r)
    (hbal : nu + r = k + l) :
    (((nu - 1) + (r - 1) = (k - 1) + (l - 1)) ∧
      (k - 1) + (l - 1) + (nu - 1) + (r - 1) < k + l + nu + r) ∧
    ((nu + (r - 1) = k + (l - 1)) ∧
      k + (l - 1) + nu + (r - 1) < k + l + nu + r) ∧
    ((nu + (r - 1) = (k - 1) + l) ∧
      (k - 1) + l + nu + (r - 1) < k + l + nu + r) := by sorry

Source

G. Rhin and C. Viola, On the irrationality measure of zeta(2), Annales de l'Institut Fourier 43 (1993), Lemma 3, p. 90.

View graph