What does a referee have to check by hand?
🟢 2 formal · 🟡 2 formal in part · 🔵 2 computation
To check by hand, in order
Each statement comes after what it uses. 🟡: only the part not formalized; 🔵: the argument, not its computations.
- even n ≥ 14: middle rows strictly ordered, no sign change — 🟡 the rest is to be checked by hand
- odd n ≥ 15: row ⌊w/2⌋, no zero, exactly two sign changes — 🟡 the rest is to be checked by hand
- exhaustive search, w ≤ 12: 14 and 15 are the smallest n — 🔵 written proof; its computations are checked by a program
- zeros deleted: examples already in widths 6–8 — 🔵 written proof; its computations are checked by a program
Every statement
| statement | status | relations |
|---|---|---|
| thm:A even n ≥ 14: middle rows strictly ordered, no sign change formal: the base pair n = 14 only (kernel computation, decide); the family for every n is in Isabelle | 🟡 formal in part | uses Lemma 1 |
| Lemma 1 antipodal ear insertion keeps the old diameters, adds one | 🟢 formal | — |
| thm:B odd n ≥ 15: row ⌊w/2⌋, no zero, exactly two sign changes formal: the pair n = 15 only (kernel computation, decide); the family for every n is in Isabelle | 🟡 formal in part | — |
| cor:all four sign changes fail for every n ≥ 14 (k ≤ ⌈w/2⌉), for odd n inside k ≤ ⌊w/2⌋ | 🟢 formal | uses even n ≥ 14: middle rows strictly ordered, no sign change; uses odd n ≥ 15: row ⌊w/2⌋, no zero, exactly two sign changes |
| prop:min exhaustive search, w ≤ 12: 14 and 15 are the smallest n | 🔵 computation | — |
| rem:zeros zeros deleted: examples already in widths 6–8 | 🔵 computation | — |
🟢 formal: the whole statement is machine-checked · 🟡 formal in part: the rest is to be checked by hand · 🔵 computation: written proof; its computations are checked by a program · 🔴 by hand: written proof only · ⚪ cited / no proof here: a result of others, or a question