lean_workbook_plus_79949

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

If $n=2^u-2^v+t$ where $u>v\ge 0$ and $t<2^{v-1}$ : \n $f(n)=2^v-t-1$ and $g(n)=f(f(n))=t$ \nSo $n-g(n)=2^u-2^v$ and $f(n-g(n))=2^v-1$ and $g(n-g(n))=f(2^v-1)=0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_79949  (u v t : ℕ)
  (n : ℕ)
  (f g : ℕ → ℕ)
  (h₀ : n = 2^u - 2^v + t)
  (h₁ : u > v)
  (h₂ : v >= 0)
  (h₃ : t < 2^(v-1))
  (h₄ : f n = 2^v - t - 1)
  (h₅ : g n = f (f n))
  (h₆ : n - g n = 2^u - 2^v)
  (h₇ : f (n - g n) = 2^v - 1)
  (h₈ : g (n - g n) = f (2^v - 1))
  (h₉ : f (2^v - 1) = 0) :
  g n = t   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph