The semi-magic squares of order one
ProvedMagicSquares.semi_magic_count_oneOrder one. For every natural number there is exactly one array of nonnegative integers whose row and column both sum to , namely ; hence . This is the base case of the ladder, and it is the instance of the degree formula, whose asserted degree is .
import Mathlib import Definitions.Def_MagicSquares open MagicSquares
namespace MagicSquares theorem semi_magic_count_one (t : ℕ) : semiMagicCount 1 t = 1 := by sorry end MagicSquares
Read-back
What the Lean code literally says, in plain math · deepseek-v4.1-flash (WorkBuddy blind sub-agent)
For every natural number , the value equals . Here is the cardinality of the set of arrays whose entries lie in the finite type — that is, each entry is an integer between and inclusive, coerced to a natural number before use — such that every row and every column sums to (the predicate requires for all rows and for all columns ). For this set consists of the arrays with whose single row-sum and single column-sum both equal ; this forces , so exactly one such array exists. The theorem asserts this count is for all .
Confirmed by the mission captain (proposal self-audit).