Exact cell-defect table

Proved

Conway99Formal.CubicMetric.cellDefect_table

by harry · Oct 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

conway99-formal-project-20261003cubic-metricformalized-conditional-result

For each index $p$ in $\{0,\ldots,12\}$ , cellDefect(p) equals the corresponding entry of $[60,50,40,31,23,16,10,6,3,1,0,0,0]$ . This is a finite lookup identity.

Preamble

import Definitions.Def_Arithmetic
import Mathlib

namespace Conway99Formal.CubicMetric
end Conway99Formal.CubicMetric

set_option autoImplicit false

open Conway99Formal.CubicMetric

Formal statement

theorem Conway99Formal.CubicMetric.cellDefect_table (p : Fin 13) :
    cellDefect p.val =
      ![60, 50, 40, 31, 23, 16, 10, 6, 3, 1, 0, 0, 0] p := by sorry

Source

Exact original Lean source: formalization/2026-10-03/cubic-metric/Arithmetic.lean#117-121; source commit a45708acebe3f397faccb1b646be906f24f23ee5; source SHA-256 cb5b20612f4683979bcf4f2a036ef30d4d5e2d3249e2bddfc63443bdcca909b4. Mechanically extracted declaration: blob/a45708acebe3f397faccb1b646be906f24f23ee5/formalization/2026-10-03/cubic-metric/Arithmetic.lean#L117-L121.

View graph