theorem Hex.GraphIso.Nauty.cheapautom_go_cells {ptn : Array Nat} {level nn : Nat} (hps : ptn.size = nn) (hend : ptn[ptn.size - 1]! ≤ level) (fuel i k nnt : Nat) : i = 0 ∨ ptn[i - 1]! ≤ level → cheapautom.go ptn level fuel i k nnt = (k - (cells.go ptn level nn fuel i).length, nnt + List.countP (fun (p : Nat × Nat) => decide (p.fst < p.snd)) (cells.go ptn level nn fuel i))

cheapautom's scan aligned with the partition's cell list: the first component counts down once per cell and the second counts the nontrivial cells.

theorem Hex.GraphIso.Nauty.cells_go_sizes_sum {ptn : Array Nat} {level nn : Nat} (hps : ptn.size = nn) (hend : ptn[ptn.size - 1]! ≤ level) (fuel i : Nat) : nn ≤ fuel + i → (List.map (fun (p : Nat × Nat) => p.snd + 1 - p.fst) (cells.go ptn level nn fuel i)).sum = nn - i

The cell sizes of the partition sum to the vertex count.

theorem Hex.GraphIso.Nauty.cheapautom_iff {ptn : Array Nat} {level nn : Nat} (hps : ptn.size = nn) (hend : ptn[ptn.size - 1]! ≤ level) : cheapautom ptn level nn = true ↔ nn - (cells ptn level nn).length ≤ List.countP (fun (p : Nat × Nat) => decide (p.fst < p.snd)) (cells ptn level nn) + 1 ∨ nn - (cells ptn level nn).length ≤ 4

The guard characterized: cheapautom holds exactly when the defect (vertices minus cells) is at most the nontrivial cell count plus one, or at most four.

theorem Hex.GraphIso.Nauty.size_le_three_of_defect_le {ptn : Array Nat} {level nn : Nat} (hps : ptn.size = nn) (hend : ptn[ptn.size - 1]! ≤ level) (hguard : nn - (cells ptn level nn).length ≤ List.countP (fun (p : Nat × Nat) => decide (p.fst < p.snd)) (cells ptn level nn) + 1) (q : Nat × Nat) : q ∈ cells ptn level nn → q.snd + 1 - q.fst ≤ 3

In the first guard branch every cell has size at most three.

theorem Hex.GraphIso.Nauty.triple_uniq_of_defect_le {ptn : Array Nat} {level nn : Nat} (hps : ptn.size = nn) (hend : ptn[ptn.size - 1]! ≤ level) (hguard : nn - (cells ptn level nn).length ≤ List.countP (fun (p : Nat × Nat) => decide (p.fst < p.snd)) (cells ptn level nn) + 1) (q : Nat × Nat) : q ∈ cells ptn level nn → ∀ (q' : Nat × Nat), q' ∈ cells ptn level nn → q.snd + 1 - q.fst = 3 → q'.snd + 1 - q'.fst = 3 → q = q'

In the first guard branch any two size-three cells coincide.

theorem Hex.GraphIso.Nauty.cells_shape_of_defect_le {ptn : Array Nat} {level nn : Nat} (hps : ptn.size = nn) (hend : ptn[ptn.size - 1]! ≤ level) (hguard : nn - (cells ptn level nn).length ≤ List.countP (fun (p : Nat × Nat) => decide (p.fst < p.snd)) (cells ptn level nn) + 1) (q : Nat × Nat) : q ∈ cells ptn level nn → q.snd + 1 - q.fst = 1 ∨ q.snd + 1 - q.fst = 2 ∨ q.snd + 1 - q.fst = 3 ∧ ∀ (q' : Nat × Nat), q' ∈ cells ptn level nn → q'.snd + 1 - q'.fst = 3 → q' = q

The first-branch shape: every cell is a singleton, a pair, or the unique triple.

theorem Hex.GraphIso.Nauty.exc_sum_eq_defect {ptn : Array Nat} {level nn : Nat} (hps : ptn.size = nn) (hend : ptn[ptn.size - 1]! ≤ level) : (List.map (fun (p : Nat × Nat) => p.snd - p.fst) (cells ptn level nn)).sum = nn - (cells ptn level nn).length

The cells' excesses sum to the defect.