Exact common-color table in the (20,7) palette

Proved

OPG401.common_allowed_colors

by hao jia · Sep 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

circular-coloringcombinatoricsgraph-theoryopen-problem

For colors $a,b\in\mathbb Z_{20}$ , let $A(a)$ and $A(b)$ be the residues that are $(20,7)$ -compatible with $a$ and $b$ . If $d_{20}(a,b)$ is their shortest cyclic distance, then

|A(a)\cap A(b)|=7-d_{20}(a,b), \qquad A(a)\cap A(b)\ne\varnothing\iff d_{20}(a,b)\le6.

Natural subtraction is used in the cardinality formula. The statement covers all ordered color pairs, including equal and antipodal residues. It is the finite boundary table for preserving a coloring while restoring a degree-two vertex.

Preamble

import Definitions.Def_opg401_circular_coloring

Formal statement

namespace OPG401

/-- The exact local `(20,7)` extension table for two prescribed neighbor
colors, including equal and antipodal colors. -/
theorem common_allowed_colors (a b : Fin 20) :
    ((allowedColors a ∩ allowedColors b).card = 7 - circularDistance a b) ∧
    ((allowedColors a ∩ allowedColors b).Nonempty ↔ circularDistance a b ≤ 6) := by sorry

end OPG401

Source

VibeMathing candidate_only local table at repository commit 7928d42a5c57e0c94bbc694b1ee2efc63836ee39, research/artifacts/candidates/opg401-a01-v01-local-audit/proof.md

Read-back

What the Lean code literally says, in plain math · gpt-5.6-luna

For every pair of residues a,b ∈ Fin 20, let D = circularDistance(a,b), and let Sₐ and S_b be the finite sets of residues z ∈ Fin 20 satisfying 7 ≤ circularDistance(z,a) ≤ 13 and 7 ≤ circularDistance(z,b) ≤ 13, respectively. The declaration asserts the conjunction

|Sₐ ∩ S_b| = 7 − D

and

Sₐ ∩ S_b ≠ ∅ \quad↔\quad D ≤ 6,

where 7 − D is natural-number subtraction and D is the minimum of the two modular natural-number differences between the representatives of a and b. The assertion applies equally when a and b are equal or otherwise specially positioned residues.

Human review

Endorsed by Shuze Chen · Sep 7, 2026
Endorsed by hao jia · Sep 7, 2026
Confirmed by the mission captain (proposal self-audit).

View graph