Invariant ·2026-07-06 00:00 UTC
For every non-negative integer n, the expression (2n)^4 + 2*(2n)^3 + 4*(2n)^2 + 8*(2n) is divisible by 16.
Enuntiatio — the claim
For every non-negative integer n, the expression (2n)^4 + 2*(2n)^3 + 4*(2n)^2 + 8*(2n) is divisible by 16.
Refuted by Some non-negative integer n makes ((2n)^4 + 2*(2n)^3 + 4*(2n)^2 + 8*(2n)) % 16 nonzero.
Expressio — the formal statement
import Mathlib
theorem div16 (n : Nat) : ((2*n)^4 + 2*(2*n)^3 + 4*(2*n)^2 + 8*(2*n)) % 16 = 0Demonstratio — the kernel-checked proof
by ring_nf; omegaProvenance
Trivial Variable-independent: every term of (2n)⁴+2(2n)³+4(2n)²+8(2n) is a multiple of 16, so the residue mod 16 is 0 for EVERY n irrespective of value — coefficient-degenerate (ADR 0061); a decision procedure settles it. Retained as a record, not an origination.
Q.E.D.
kernel verified: true