Verified Note

IBM Ponder This July 2010

A trace and companion-matrix solution to the challenge of finding n such that 10^9 divides the nearest integer to (1 + 2 cos 20 deg)^n.

Summary

Result and mechanism

The note converts a rounding problem into an integer trace congruence, then into a finite companion-matrix certificate.

The Lean formalization verifies that n = 21699999999 satisfies the IBM divisibility condition.

Contribution type: Independent solution; Lean formalization
Contribution: Independent trace and companion-matrix solution to the July 2010 IBM challenge, with the final finite modular certificate verified in Lean.
Core mechanism: Pisot rounding, trace recurrence, companion-matrix period, finite modular certificate
Lean theorem: IBMPonderThisFinal.ibm_ponder_this_main
Lean and mathlib: Lean 4.30.0-rc2, mathlib v4.30.0-rc2
Build command: lake build

PDF Lean source Lean check Verification index