Table-22 graded source and support-cover certificates

Definition
SP4Table22Certificates
by ryanshin · Sep 8, 2026 · Mathlib 0df444a (Lean v4.33.1)
finite-combinatoricshomologylinear-algebrasp4-backlog-formalization
This bundle contains the exact ordered table of 140 saved source gradings, each on thirty coordinates, and two explicit bipartite support covers per grading. Each coordinate has two fixed integer filtration values and a recorded integer degree. The total allowed support consists of entries that strictly decrease the first coordinate, weakly decrease the second, and decrease degree by one. The mixed support additionally strictly decreases the second coordinate.
For each cover, the budget is the sum of the numbers of distinct selected target rows and source columns. Repeated list entries therefore do not inflate a budget. The finite validity predicate asks that every allowed entry be covered, that the degree array have length thirty, and that
\min\{R,4+H\}\le13,\qquad \min\{R,2+H\}\le11.
The certificate structure itself permits arbitrary finite arrays and cover lists; the separate theorem verifies all 140 bundled records. Array access is total, with default zero grades and an empty default certificate outside the stored bounds. The main theorem uses indices from zero through 139 and basis indices from zero through 29; the bundled lengths are checked.
These are literal data and a decidable support-checking interface, not an assumed rank bound, an enumeration-completeness theorem, a Floer invariant or a geometric realization.
Definition code
import Mathlib

set_option autoImplicit false

namespace SP4Table22

/-- A recorded source grading and two bipartite support covers. A source column
and a target row are separate cover vertices even when their numbers agree. -/
structure Certificate where
  degrees : Array ℤ
  totalRows : List (Fin 30)
  totalCols : List (Fin 30)
  mixedRows : List (Fin 30)
  mixedCols : List (Fin 30)
  deriving Inhabited

def firstCoordinates : Array ℤ := #[-2, -2, -2, -2, -1, -1, -1, -1, -1, -1, -1, -1, 0, 0, 0, 0, 0, 0, 1, 1, 1, 1, 1, 1, 1, 1, 2, 2, 2, 2]
def secondCoordinates : Array ℤ := #[0, 0, 0, 0, -1, -1, -1, -1, 1, 1, 1, 1, -1, -1, 0, 0, 1, 1, -1, -1, -1, -1, 1, 1, 1, 1, 0, 0, 0, 0]

/-- Exact ordered records from cycle12_table22_common_rank.json. -/
def records : Array Certificate := #[
  ⟨#[-3, -2, -2, -1, -2, -1, -1, 0, 0, 1, 1, 2, -1, 0, 2, 3, 1, 2, 0, 1, 1, 2, 2, 3, 3, 4, 1, 2, 2, 3], [], [8, 12, 13, 16, 17, 18, 19, 20, 22, 23, 24, 25, 26, 27, 28, 29], [14], [8, 16, 25, 26, 27, 28, 29]⟩,
  ⟨#[-3, -2, -2, -1, -2, -1, -1, 0, 0, 1, 1, 2, 0, 1, -1, 2, 2, 3, 0, 1, 1, 2, 2, 3, 3, 4, 1, 2, 2, 3], [7, 12], [8, 12, 14, 16, 17, 18, 21, 22, 23, 24, 25, 26, 27, 28, 29], [15], [8, 14, 22, 26, 27, 28, 29]⟩,
  ⟨#[-3, -2, 0, 1, -2, -1, -1, 0, 0, 1, 1, 2, -1, 0, 0, 1, 1, 2, 0, 1, 1, 2, 2, 3, 3, 4, 1, 2, 4, 5], [2, 7, 13], [11, 12, 13, 14, 16, 17, 18, 22, 23, 24, 26, 27], [2, 3, 7], [14, 22, 26, 27]⟩,
  ⟨#[-3, -2, 0, 1, -2, -1, -1, 0, 0, 1, 1, 2, -1, 0, 2, 3, 1, 2, 0, 1, 1, 2, 2, 3, 3, 4, 1, 2, 4, 5], [2, 3, 15], [12, 13, 16, 17, 18, 19, 20, 22, 23, 24, 26, 27], [2, 3, 14], [16, 25, 26, 27]⟩,
  ⟨#[-3, -2, 0, 1, -2, -1, -1, 0, 0, 1, 1, 2, 0, 1, -1, 2, 2, 3, 0, 1, 1, 2, 2, 3, 3, 4, 1, 2, 4, 5], [2, 3, 7, 12], [12, 14, 16, 17, 18, 21, 22, 23, 24, 25, 26, 27], [2, 3, 15], [14, 22, 26, 27]⟩,
  ⟨#[-4, -3, -3, -2, -2, -1, -1, 0, 0, 1, 1, 2, -3, -2, 2, 3, -1, 0, 0, 1, 1, 2, 2, 3, 3, 4, 0, 1, 1, 2], [5, 6, 7, 18], [16, 22, 23, 24, 25, 29], [14], [16, 17, 25, 26, 27, 28, 29]⟩,
  ⟨#[-4, -3, -3, -2, -2, -1, -1, 0, 0, 1, 1, 2, -3, 0, -2, 3, -1, 2, 0, 1, 1, 2, 2, 3, 3, 4, 0, 1, 1, 2], [5, 6, 7, 13, 18], [14, 16, 17, 22, 23, 24, 25, 29], [], [16, 25, 26, 27, 28, 29]⟩,
  ⟨#[-5, -4, 0, 1, -2, -1, -1, 0, 0, 1, 1, 2, -1, 0, -4, -3, 1, 2, 0, 1, 1, 2, 2, 3, 3, 4, -1, 0, 4, 5], [2, 4], [11, 13, 14, 15, 16, 17, 18, 19, 20, 22, 23, 24, 27], [2, 3], [16, 26, 27]⟩,
  ⟨#[-5, -4, 0, 1, -2, -1, -1, 0, 0, 1, 1, 2, -3, 0, -4, 1, -1, 2, 0, 1, 1, 2, 2, 3, 3, 4, -1, 0, 4, 5], [2, 4, 5, 6, 7, 13], [11, 14, 17, 22, 23, 24], [2, 3, 4], [15, 22, 27]⟩,
  ⟨#[-3, -2, 2, 3, -2, -1, 1, 2, 0, 1, 3, 4, -1, 0, 2, 3, 1, 2, 0, 1, 3, 4, 2, 3, 5, 6, 1, 2, 6, 7], [2, 7], [11, 12, 13, 14, 16, 17, 18, 19, 22, 23, 24, 26, 27], [6], [10, 11, 15, 23, 26, 27]⟩,
  ⟨#[-3, -2, 2, 3, -2, -1, 1, 2, 0, 1, 3, 4, 0, 1, -1, 2, 2, 3, 0, 1, 3, 4, 2, 3, 5, 6, 1, 2, 6, 7], [2, 5, 7], [11, 14, 15, 16, 19, 22, 23, 24, 26, 27], [6], [10, 11, 14, 17, 22, 23, 26, 27]⟩,
  ⟨#[-3, -2, 2, 3, -2, -1, 1, 2, 0, 1, 3, 4, -1, 0, 4, 5, 1, 2, 0, 1, 3, 4, 2, 3, 5, 6, 1, 2, 6, 7], [3, 15], [10, 12, 13, 16, 17, 18, 19, 20, 22, 23, 24, 26, 27], [6], [10, 11, 23, 24, 25, 26, 27]⟩,
  ⟨#[-3, -2, 2, 3, -2, -1, 1, 2, 0, 1, 3, 4, -1, 2, 0, 5, 1, 4, 0, 1, 3, 4, 2, 3, 5, 6, 1, 2, 6, 7], [15], [10, 11, 12, 13, 14, 16, 17, 18, 20, 22, 23, 24, 26, 27], [3], [10, 14, 22, 23, 25, 26, 27]⟩,
  ⟨#[-9, -8, -6, -5, -13, -12, -12, -11, -11, -10, -10, -9, -3, -2, -12, -11, -1, 0, -11, -10, -10, -9, -9, -8, -8, -7, -5, -4, -2, -1], [7], [14, 15, 18, 22, 23, 24, 25, 26, 27, 28, 29], [0], [14, 15, 25, 28, 29]⟩,
  ⟨#[-2, -1, -1, 0, -3, -2, -2, -1, -1, 0, 0, 1, -1, 0, -2, -1, 1, 2, -1, 0, 0, 1, 1, 2, 2, 3, 2, 3, 3, 4], [0, 5, 6, 7, 11, 12, 16], [9, 10, 11, 14, 16, 21, 22, 25, 26], [3], [8, 9, 10, 14, 15, 22, 26]⟩,
  ⟨#[-2, -1, -1, 0, -3, -2, -2, -1, -1, 0, 0, 1, -2, -1, -1, 2, 0, 1, -1, 0, 0, 1, 1, 2, 2, 3, 2, 3, 3, 4], [15], [8, 9, 10, 11, 12, 13, 14, 16, 17, 18, 19, 20, 22, 23, 24, 26], [3], [8, 9, 10, 14, 16, 25, 26]⟩,
  ⟨#[-3, -2, -2, -1, -3, -2, -2, -1, -1, 0, 0, 1, -1, 0, -2, -1, 1, 2, -1, 0, 0, 1, 1, 2, 2, 3, 1, 2, 2, 3], [3, 7, 11, 12, 16, 21], [8, 12, 14, 15, 16, 18, 21, 22, 25, 26], [3, 21], [8, 14, 15, 22, 26]⟩,
  ⟨#[-3, -2, -2, -1, -3, -2, -2, -1, -1, 0, 0, 1, -2, -1, -1, 2, 0, 1, -1, 0, 0, 1, 1, 2, 2, 3, 1, 2, 2, 3], [3, 15, 21], [8, 12, 13, 14, 16, 17, 18, 19, 20, 22, 23, 24, 26], [3, 21], [8, 14, 16, 25, 26]⟩,
  ⟨#[-4, -3, -3, -2, -3, -2, -2, -1, -1, 0, 0, 1, -1, 0, -2, -1, 1, 2, -1, 0, 0, 1, 1, 2, 2, 3, 0, 1, 1, 2], [3, 5, 6, 7, 11, 12, 16], [14, 16, 21, 22, 25, 26, 27, 28, 29], [], [8, 14, 15, 22, 26, 27, 28, 29]⟩,
  ⟨#[-4, -3, -3, -2, -3, -2, -2, -1, -1, 0, 0, 1, -2, -1, -1, 2, 0, 1, -1, 0, 0, 1, 1, 2, 2, 3, 0, 1, 1, 2], [], [8, 12, 13, 14, 16, 17, 18, 19, 20, 22, 23, 24, 25, 26, 27, 28, 29], [], [8, 14, 16, 25, 26, 27, 28, 29]⟩,
  ⟨#[-4, -3, -3, -2, -3, -2, -2, -1, -1, 0, 0, 1, -1, 0, 0, 1, 1, 2, -1, 0, 0, 1, 1, 2, 2, 3, 0, 1, 1, 2], [7, 12], [8, 12, 16, 17, 18, 21, 22, 23, 24, 25, 26, 27, 28, 29], [15], [8, 14, 22, 26, 27, 28, 29]⟩,
  ⟨#[-4, -3, -1, 0, -3, -2, -2, -1, -1, 0, 0, 1, -3, -2, -2, -1, -1, 0, -1, 0, 0, 1, 1, 2, 2, 3, 0, 1, 3, 4], [2, 7, 11], [11, 13, 14, 15, 16, 17, 18, 22, 26, 27], [2, 3], [14, 15, 16, 17, 26, 27]⟩,
  ⟨#[-4, -3, -1, 0, -3, -2, -2, -1, -1, 0, 0, 1, -1, 0, 0, 1, 1, 2, -1, 0, 0, 1, 1, 2, 2, 3, 0, 1, 3, 4], [2, 3, 7, 12], [12, 16, 17, 18, 21, 22, 23, 24, 25, 26, 27], [2, 3, 15], [14, 22, 26, 27]⟩,
  ⟨#[-4, -3, -1, 0, -3, -2, -2, -1, -1, 0, 0, 1, -1, 0, 2, 3, 1, 2, -1, 0, 0, 1, 1, 2, 2, 3, 0, 1, 3, 4], [2, 7, 11, 12, 16], [11, 12, 16, 18, 21, 22, 25, 26, 27, 28, 29], [2, 3], [22, 25, 26, 27]⟩,
  ⟨#[-4, -3, -1, 0, -3, -2, -2, -1, -1, 0, 0, 1, 0, 1, -1, 2, 2, 3, -1, 0, 0, 1, 1, 2, 2, 3, 0, 1, 3, 4], [2, 7, 11, 13], [11, 14, 18, 21, 22, 25, 26, 27, 28], [2, 13], [11, 14, 22, 25, 26, 27]⟩,
  ⟨#[-5, -4, -4, -3, -3, -2, -2, -1, -1, 0, 0, 1, -1, 0, -4, -3, 1, 2, -1, 0, 0, 1, 1, 2, 2, 3, -1, 0, 0, 1], [5, 6, 7, 11, 12, 16, 18], [14, 15, 16, 21, 22, 25, 29], [], [22, 26, 27, 28, 29]⟩,
  ⟨#[-5, -4, -4, -3, -3, -2, -2, -1, -1, 0, 0, 1, -3, 0, -4, 1, -1, 2, -1, 0, 0, 1, 1, 2, 2, 3, -1, 0, 0, 1], [5, 6, 7, 11, 15, 18], [14, 21, 22, 25, 29], [15], [16, 22, 26, 27, 28, 29]⟩,
  ⟨#[-9, -8, -6, -5, -3, -2, -2, -1, -1, 0, 0, 1, -1, 0, -8, -7, 1, 2, -1, 0, 0, 1, 1, 2, 2, 3, -5, -4, -2, -1], [5, 6, 7, 11, 12, 16], [14, 15, 16, 21, 22, 25, 26, 27, 28], [], [22, 28, 29]⟩,
  ⟨#[-4, -3, 1, 2, -3, -2, 0, 1, -1, 0, 2, 3, -1, 0, -2, -1, 1, 2, -1, 0, 2, 3, 1, 2, 4, 5, 0, 1, 5, 6], [2, 5, 7], [11, 14, 16, 19, 22, 23, 24, 26, 27], [2, 7], [11, 14, 15, 16, 22, 26, 27]⟩,
  ⟨#[-4, -3, 1, 2, -3, -2, 0, 1, -1, 0, 2, 3, -2, -1, -1, 2, 0, 1, -1, 0, 2, 3, 1, 2, 4, 5, 0, 1, 5, 6], [2, 5, 7], [11, 12, 16, 17, 18, 19, 22, 23, 24, 26, 27], [2, 6, 7], [11, 14, 26, 27]⟩,
  ⟨#[-4, -3, 1, 2, -3, -2, 0, 1, -1, 0, 2, 3, -1, 0, 0, 1, 1, 2, -1, 0, 2, 3, 1, 2, 4, 5, 0, 1, 5, 6], [2, 5, 7], [11, 15, 16, 19, 22, 23, 24, 26, 27], [6], [10, 11, 17, 22, 23, 26, 27]⟩,
  ⟨#[-5, -4, 0, 1, -4, -3, -1, 0, -2, -1, 1, 2, -2, -1, -3, 0, 0, 1, -2, -1, 1, 2, 0, 1, 3, 4, -1, 0, 4, 5], [2, 5, 7], [11, 14, 15, 16, 19, 22, 23, 24, 26, 27], [6], [10, 11, 14, 17, 22, 23, 26, 27]⟩,
  ⟨#[-5, -4, 0, 1, -4, -3, -1, 0, -2, -1, 1, 2, -3, -2, 0, 1, -1, 0, -2, -1, 1, 2, 0, 1, 3, 4, -1, 0, 4, 5], [2, 7], [11, 12, 13, 14, 16, 17, 18, 19, 22, 23, 24, 26, 27], [6], [10, 11, 15, 23, 26, 27]⟩,
  ⟨#[-5, -4, 0, 1, -4, -3, -1, 0, -2, -1, 1, 2, -3, -2, 2, 3, -1, 0, -2, -1, 1, 2, 0, 1, 3, 4, -1, 0, 4, 5], [3, 15], [10, 12, 13, 16, 17, 18, 19, 20, 22, 23, 24, 26, 27], [6], [10, 11, 23, 24, 25, 26, 27]⟩,
  ⟨#[-5, -4, 0, 1, -4, -3, -1, 0, -2, -1, 1, 2, -3, 0, -2, 3, -1, 2, -2, -1, 1, 2, 0, 1, 3, 4, -1, 0, 4, 5], [15], [10, 11, 12, 13, 14, 16, 17, 18, 20, 22, 23, 24, 26, 27], [3], [10, 14, 22, 23, 25, 26, 27]⟩,
  ⟨#[-2, -1, -1, 0, -4, -3, -3, -2, -2, -1, -1, 0, -3, -2, 2, 3, -1, 0, -2, -1, -1, 0, 0, 1, 1, 2, 2, 3, 3, 4], [0, 14], [11, 12, 13, 16, 17, 18, 19, 20, 22, 23, 24, 29], [0, 1, 2, 3], [16]⟩,
  ⟨#[-2, -1, -1, 0, -4, -3, -3, -2, -2, -1, -1, 0, -3, 0, -2, 3, -1, 2, -2, -1, -1, 0, 0, 1, 1, 2, 2, 3, 3, 4], [0, 7], [11, 12, 14, 16, 18, 22, 23, 24, 29], [0], [11, 14, 16, 22, 23, 24]⟩,
  ⟨#[-3, -2, -2, -1, -4, -3, -3, -2, -2, -1, -1, 0, -3, -2, -2, -1, -1, 0, -2, -1, -1, 0, 0, 1, 1, 2, 1, 2, 2, 3], [1, 2, 7, 13], [8, 11, 12, 13, 14, 16, 17, 18, 22, 23, 24, 26], [1, 2, 3, 7], [8, 14, 22, 26]⟩,
  ⟨#[-3, -2, -2, -1, -4, -3, -3, -2, -2, -1, -1, 0, -2, -1, -3, 0, 0, 1, -2, -1, -1, 0, 0, 1, 1, 2, 1, 2, 2, 3], [3, 7, 12], [8, 9, 10, 12, 14, 16, 17, 18, 21, 22, 23, 24, 25, 26], [3, 15], [8, 9, 10, 14, 22, 26]⟩,
  ⟨#[-3, -2, -2, -1, -4, -3, -3, -2, -2, -1, -1, 0, -3, -2, 0, 1, -1, 0, -2, -1, -1, 0, 0, 1, 1, 2, 1, 2, 2, 3], [3, 15], [8, 9, 10, 12, 13, 16, 17, 18, 19, 20, 22, 23, 24, 26], [3, 14], [8, 9, 10, 16, 25, 26]⟩,
  ⟨#[-4, -3, -3, -2, -4, -3, -3, -2, -2, -1, -1, 0, -2, -1, -3, 0, 0, 1, -2, -1, -1, 0, 0, 1, 1, 2, 0, 1, 1, 2], [3, 7, 11, 12, 15, 16, 21], [8, 12, 14, 16, 18, 21, 22, 25, 26], [3, 15, 21], [8, 14, 22, 26]⟩,
  ⟨#[-4, -3, -3, -2, -4, -3, -3, -2, -2, -1, -1, 0, -3, -2, 0, 1, -1, 0, -2, -1, -1, 0, 0, 1, 1, 2, 0, 1, 1, 2], [3, 15], [8, 12, 13, 16, 17, 18, 19, 20, 22, 23, 24, 26, 27, 28], [3, 14, 21], [8, 16, 25, 26]⟩,
  ⟨#[-5, -4, -2, -1, -4, -3, -3, -2, -2, -1, -1, 0, -3, -2, -2, -1, -1, 0, -2, -1, -1, 0, 0, 1, 1, 2, -1, 0, 2, 3], [2, 7, 13], [11, 12, 13, 14, 16, 17, 18, 22, 23, 24, 26, 27], [2, 3, 7], [14, 22, 26, 27]⟩,
  ⟨#[-5, -4, -2, -1, -4, -3, -3, -2, -2, -1, -1, 0, -3, -2, -4, -3, -1, 0, -2, -1, -1, 0, 0, 1, 1, 2, -1, 0, 2, 3], [2], [11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 22, 23, 24, 26, 27], [2, 3], [15, 16, 26, 27]⟩,
  ⟨#[-5, -4, -2, -1, -4, -3, -3, -2, -2, -1, -1, 0, -4, -3, -3, 0, -2, -1, -2, -1, -1, 0, 0, 1, 1, 2, -1, 0, 2, 3], [2, 3, 7], [13, 14, 16, 17, 18, 22, 23, 24, 26, 27], [2, 3, 15], [14, 16, 17, 26, 27]⟩,
  ⟨#[-5, -4, -2, -1, -4, -3, -3, -2, -2, -1, -1, 0, -1, 0, 0, 1, 1, 2, -2, -1, -1, 0, 0, 1, 1, 2, -1, 0, 2, 3], [2, 3, 7], [16, 18, 21, 22, 23, 24, 25, 26, 27, 28], [2], [11, 22, 23, 24, 25, 26, 27]⟩,
  ⟨#[-5, -4, -4, -3, -4, -3, -3, -2, -2, -1, -1, 0, -2, -1, -3, 0, 0, 1, -2, -1, -1, 0, 0, 1, 1, 2, -1, 0, 0, 1], [7, 12], [8, 12, 14, 16, 17, 18, 21, 22, 23, 24, 25, 26, 27, 28, 29], [15], [8, 14, 22, 26, 27, 28, 29]⟩,
  ⟨#[-5, -4, -4, -3, -4, -3, -3, -2, -2, -1, -1, 0, -3, -2, 0, 1, -1, 0, -2, -1, -1, 0, 0, 1, 1, 2, -1, 0, 0, 1], [], [8, 12, 13, 16, 17, 18, 19, 20, 22, 23, 24, 25, 26, 27, 28, 29], [14], [8, 16, 25, 26, 27, 28, 29]⟩,
  ⟨#[0, 1, 3, 4, -4, -3, -3, -2, -2, -1, -1, 0, -3, -2, 6, 7, -1, 0, -2, -1, -1, 0, 0, 1, 1, 2, 4, 5, 7, 8], [], [12, 13, 16, 17, 18, 19, 20, 22, 23, 24, 25, 26, 27, 28, 29], [0], [16, 25]⟩,
  ⟨#[-6, -5, -1, 0, -5, -4, -2, -1, -3, -2, 0, 1, -1, 0, -2, -1, 1, 2, -3, -2, 0, 1, -1, 0, 2, 3, -2, -1, 3, 4], [6], [10, 11, 13, 16, 17, 18, 20, 21, 22, 23, 24, 25, 26, 27], [3], [10, 15, 22, 23, 26, 27]⟩,
  ⟨#[-6, -5, -1, 0, -5, -4, -2, -1, -3, -2, 0, 1, -2, -1, -1, 2, 0, 1, -3, -2, 0, 1, -1, 0, 2, 3, -2, -1, 3, 4], [6, 15], [10, 11, 16, 17, 18, 20, 22, 23, 24, 26, 27], [3], [10, 14, 16, 22, 23, 25, 26, 27]⟩,
  ⟨#[-6, -5, -1, 0, -5, -4, -2, -1, -3, -2, 0, 1, -1, 0, -4, -3, 1, 2, -3, -2, 0, 1, -1, 0, 2, 3, -2, -1, 3, 4], [2, 5, 7, 12], [11, 12, 14, 16, 17, 21, 22, 24, 25, 26, 27], [3], [10, 14, 15, 22, 23, 26, 27]⟩,
  ⟨#[-6, -5, -1, 0, -5, -4, -2, -1, -3, -2, 0, 1, -3, 0, -4, 1, -1, 2, -3, -2, 0, 1, -1, 0, 2, 3, -2, -1, 3, 4], [3, 5, 7], [10, 14, 16, 17, 19, 21, 22, 23, 24, 25, 26, 27], [6], [10, 11, 14, 23, 24, 26, 27]⟩,
  ⟨#[-3, -2, -2, -1, -5, -4, -4, -3, -3, -2, -2, -1, -1, 0, -4, -3, 1, 2, -3, -2, -2, -1, -1, 0, 0, 1, 1, 2, 2, 3], [0, 7, 13], [11, 14, 15, 18, 22, 23, 24], [0, 13], [11, 14, 15, 22, 23, 24]⟩,
  ⟨#[-3, -2, -2, -1, -5, -4, -4, -3, -3, -2, -2, -1, -3, 0, -4, 1, -1, 2, -3, -2, -2, -1, -1, 0, 0, 1, 1, 2, 2, 3], [0, 13, 15], [11, 12, 14, 16, 18, 19, 20, 22, 23, 24], [0, 1, 2, 3, 13], [14]⟩,
  ⟨#[-4, -3, -3, -2, -5, -4, -4, -3, -3, -2, -2, -1, -3, -2, -4, -3, -1, 0, -3, -2, -2, -1, -1, 0, 0, 1, 0, 1, 1, 2], [0, 5, 6, 7, 11, 12, 16], [9, 10, 11, 14, 16, 21, 22, 25, 26], [3], [8, 9, 10, 14, 15, 22, 26]⟩,
  ⟨#[-4, -3, -3, -2, -5, -4, -4, -3, -3, -2, -2, -1, -4, -3, -3, 0, -2, -1, -3, -2, -2, -1, -1, 0, 0, 1, 0, 1, 1, 2], [15], [8, 9, 10, 11, 12, 13, 14, 16, 17, 18, 19, 20, 22, 23, 24, 26], [3], [8, 9, 10, 14, 16, 25, 26]⟩,
  ⟨#[-6, -5, -3, -2, -5, -4, -4, -3, -3, -2, -2, -1, -3, -2, -2, -1, -1, 0, -3, -2, -2, -1, -1, 0, 0, 1, -2, -1, 1, 2], [2, 3, 7, 12], [12, 16, 17, 18, 21, 22, 23, 24, 25, 26, 27], [2, 3, 15], [14, 22, 26, 27]⟩,
  ⟨#[-6, -5, -3, -2, -5, -4, -4, -3, -3, -2, -2, -1, -3, -2, -4, -3, -1, 0, -3, -2, -2, -1, -1, 0, 0, 1, -2, -1, 1, 2], [2, 5, 6, 7, 11, 12, 16], [11, 14, 16, 21, 22, 25, 26, 27], [2, 3], [14, 15, 22, 26, 27]⟩,
  ⟨#[-6, -5, -3, -2, -5, -4, -4, -3, -3, -2, -2, -1, -4, -3, -3, 0, -2, -1, -3, -2, -2, -1, -1, 0, 0, 1, -2, -1, 1, 2], [2, 15], [11, 12, 13, 14, 16, 17, 18, 19, 20, 22, 23, 24, 26, 27], [2, 3], [14, 16, 25, 26, 27]⟩,
  ⟨#[-6, -5, -1, 0, -5, -4, -4, -3, -3, -2, -2, -1, -3, -2, 2, 3, -1, 0, -3, -2, -2, -1, -1, 0, 0, 1, -2, -1, 3, 4], [7, 12], [12, 16, 17, 18, 21, 22, 23, 24, 25, 26, 27, 28, 29], [2], [22, 25, 26, 27]⟩,
  ⟨#[-6, -5, -1, 0, -5, -4, -4, -3, -3, -2, -2, -1, -3, 0, -2, 3, -1, 2, -3, -2, -2, -1, -1, 0, 0, 1, -2, -1, 3, 4], [7, 12], [12, 16, 18, 22, 23, 24, 25, 26, 27, 29], [2], [14, 22, 25, 26, 27]⟩,
  ⟨#[-7, -6, -2, -1, -6, -5, -3, -2, -4, -3, -1, 0, -3, -2, -2, -1, -1, 0, -4, -3, -1, 0, -2, -1, 1, 2, -3, -2, 2, 3], [2, 6, 7], [11, 17, 18, 20, 22, 23, 24, 26, 27], [2, 3, 7], [14, 22, 23, 26, 27]⟩,
  ⟨#[-7, -6, -2, -1, -6, -5, -3, -2, -4, -3, -1, 0, -2, -1, -3, 0, 0, 1, -4, -3, -1, 0, -2, -1, 1, 2, -3, -2, 2, 3], [2, 3, 7, 12], [12, 16, 17, 18, 21, 22, 24, 25, 26, 27], [3], [10, 22, 23, 24, 26, 27]⟩,
  ⟨#[-7, -6, -2, -1, -6, -5, -3, -2, -4, -3, -1, 0, -3, -2, 0, 1, -1, 0, -4, -3, -1, 0, -2, -1, 1, 2, -3, -2, 2, 3], [2, 3, 7, 13, 15], [13, 17, 18, 22, 24, 26, 27], [3], [10, 16, 22, 23, 24, 25, 26, 27]⟩,
  ⟨#[-7, -6, -2, -1, -6, -5, -5, -4, -4, -3, -3, -2, -1, 0, -4, -3, 1, 2, -4, -3, -3, -2, -2, -1, -1, 0, -3, -2, 2, 3], [7], [14, 18, 22, 23, 24, 25, 26, 27], [2], [14, 15, 22, 25, 26, 27]⟩,
  ⟨#[-7, -6, -2, -1, -6, -5, -5, -4, -4, -3, -3, -2, -3, 0, -4, 1, -1, 2, -4, -3, -3, -2, -2, -1, -1, 0, -3, -2, 2, 3], [2, 7, 11], [14, 18, 21, 22, 25, 26, 27, 28], [2], [14, 22, 25, 26, 27]⟩,
  ⟨#[-7, -6, -4, -3, -6, -5, -5, -4, -4, -3, -3, -2, -3, -2, -2, -1, -1, 0, -4, -3, -3, -2, -2, -1, -1, 0, -3, -2, 0, 1], [2, 3, 7], [16, 18, 21, 22, 23, 24, 25, 26, 27, 28], [2], [11, 22, 23, 24, 25, 26, 27]⟩,
  ⟨#[-7, -6, -4, -3, -6, -5, -5, -4, -4, -3, -3, -2, -3, -2, -4, -3, -1, 0, -4, -3, -3, -2, -2, -1, -1, 0, -3, -2, 0, 1], [2, 7, 11, 13], [11, 14, 18, 21, 22, 25, 26, 27], [2, 13], [11, 14, 15, 22, 26, 27]⟩,
  ⟨#[-7, -6, -4, -3, -6, -5, -5, -4, -4, -3, -3, -2, -4, -3, -3, 0, -2, -1, -4, -3, -3, -2, -2, -1, -1, 0, -3, -2, 0, 1], [2, 7, 11, 12, 16], [11, 12, 16, 18, 21, 22, 25, 26, 27, 29], [2, 3], [14, 22, 26, 27]⟩,
  ⟨#[-7, -6, -6, -5, -6, -5, -5, -4, -4, -3, -3, -2, -3, -2, -2, -1, -1, 0, -4, -3, -3, -2, -2, -1, -1, 0, -3, -2, -2, -1], [7], [8, 16, 18, 21, 22, 23, 24, 25, 26, 27, 28, 29], [], [8, 22, 23, 24, 25, 26, 27, 28, 29]⟩,
  ⟨#[-9, -8, -2, -1, -6, -5, -5, -4, -4, -3, -3, -2, -1, 0, -8, -7, 1, 2, -4, -3, -3, -2, -2, -1, -1, 0, -5, -4, 2, 3], [7], [14, 15, 18, 22, 23, 24, 25, 26, 27], [2], [25, 26, 27]⟩,
  ⟨#[-9, -8, -4, -3, -6, -5, -5, -4, -4, -3, -3, -2, -3, -2, -8, -7, -1, 0, -4, -3, -3, -2, -2, -1, -1, 0, -5, -4, 0, 1], [2, 7, 11, 13], [11, 14, 15, 18, 21, 22, 25, 26, 27], [2, 13], [11, 22, 26, 27]⟩,
  ⟨#[-8, -7, -3, -2, -7, -6, -4, -3, -5, -4, -2, -1, -3, -2, -4, -3, -1, 0, -5, -4, -2, -1, -3, -2, 0, 1, -4, -3, 1, 2], [6], [10, 11, 13, 16, 17, 18, 20, 21, 22, 23, 24, 25, 26, 27], [3], [10, 15, 22, 23, 26, 27]⟩,
  ⟨#[-8, -7, -3, -2, -7, -6, -4, -3, -5, -4, -2, -1, -4, -3, -3, 0, -2, -1, -5, -4, -2, -1, -3, -2, 0, 1, -4, -3, 1, 2], [6, 15], [10, 11, 16, 17, 18, 20, 22, 23, 24, 26, 27], [3], [10, 14, 16, 22, 23, 25, 26, 27]⟩,
  ⟨#[-8, -7, -3, -2, -7, -6, -4, -3, -5, -4, -2, -1, -3, -2, -6, -5, -1, 0, -5, -4, -2, -1, -3, -2, 0, 1, -4, -3, 1, 2], [2, 5, 7, 12], [11, 12, 14, 16, 17, 21, 22, 24, 25, 26, 27], [3], [10, 14, 15, 22, 23, 26, 27]⟩,
  ⟨#[-8, -7, -3, -2, -7, -6, -4, -3, -5, -4, -2, -1, -5, -2, -6, -1, -3, 0, -5, -4, -2, -1, -3, -2, 0, 1, -4, -3, 1, 2], [3, 5, 7], [10, 14, 16, 17, 19, 21, 22, 23, 24, 25, 26, 27], [6], [10, 11, 14, 23, 24, 26, 27]⟩,
  ⟨#[-13, -12, -10, -9, -7, -6, -6, -5, -5, -4, -4, -3, -3, -2, -12, -11, -1, 0, -5, -4, -4, -3, -3, -2, -2, -1, -9, -8, -6, -5], [7], [14, 15, 18, 22, 23, 24, 25, 26, 27, 28, 29], [12], [25, 28, 29]⟩,
  ⟨#[-6, -5, -5, -4, -7, -6, -6, -5, -5, -4, -4, -3, -3, -2, -6, -5, -1, 0, -5, -4, -4, -3, -3, -2, -2, -1, -2, -1, -1, 0], [7, 13], [8, 9, 10, 11, 14, 15, 18, 22, 23, 24, 26], [3, 12, 13], [8, 9, 10, 14, 15, 26]⟩,
  ⟨#[-6, -5, -5, -4, -7, -6, -6, -5, -5, -4, -4, -3, -5, -2, -6, -1, -3, 0, -5, -4, -4, -3, -3, -2, -2, -1, -2, -1, -1, 0], [13], [8, 9, 10, 11, 12, 14, 16, 18, 19, 20, 22, 23, 24, 26, 29], [3, 13], [8, 9, 10, 14, 26]⟩,
  ⟨#[-7, -6, -6, -5, -7, -6, -6, -5, -5, -4, -4, -3, -3, -2, -6, -5, -1, 0, -5, -4, -4, -3, -3, -2, -2, -1, -3, -2, -2, -1], [3, 7, 11, 12, 13, 21], [8, 14, 15, 18, 22, 26], [3, 12, 13, 21], [8, 14, 15, 26]⟩,
  ⟨#[-7, -6, -6, -5, -7, -6, -6, -5, -5, -4, -4, -3, -5, -2, -6, -1, -3, 0, -5, -4, -4, -3, -3, -2, -2, -1, -3, -2, -2, -1], [3, 13, 21], [8, 12, 14, 16, 18, 19, 20, 22, 23, 24, 26], [3, 13, 21], [8, 14, 26]⟩,
  ⟨#[-8, -7, -5, -4, -7, -6, -6, -5, -5, -4, -4, -3, -3, -2, -2, -1, -1, 0, -5, -4, -4, -3, -3, -2, -2, -1, -4, -3, -1, 0], [2, 7], [11, 18, 22, 23, 24, 25, 26, 27, 28, 29], [2, 3, 12], [25, 26, 27, 28]⟩,
  ⟨#[-8, -7, -5, -4, -7, -6, -6, -5, -5, -4, -4, -3, -3, -2, -4, -3, -1, 0, -5, -4, -4, -3, -3, -2, -2, -1, -4, -3, -1, 0], [2, 3, 7, 13], [18, 22, 23, 24, 26, 27], [2, 13], [11, 14, 22, 23, 24, 26, 27]⟩,
  ⟨#[-8, -7, -5, -4, -7, -6, -6, -5, -5, -4, -4, -3, -4, -3, -3, 0, -2, -1, -5, -4, -4, -3, -3, -2, -2, -1, -4, -3, -1, 0], [2, 3, 7], [16, 18, 21, 22, 23, 24, 25, 26, 27], [2], [11, 22, 23, 24, 26, 27]⟩,
  ⟨#[-8, -7, -7, -6, -7, -6, -6, -5, -5, -4, -4, -3, -3, -2, -4, -3, -1, 0, -5, -4, -4, -3, -3, -2, -2, -1, -4, -3, -3, -2], [7], [8, 18, 22, 23, 24, 25, 26, 27, 28, 29], [], [8, 14, 22, 23, 24, 25, 26, 27, 28, 29]⟩,
  ⟨#[-8, -7, -7, -6, -7, -6, -6, -5, -5, -4, -4, -3, -4, -3, -3, 0, -2, -1, -5, -4, -4, -3, -3, -2, -2, -1, -4, -3, -3, -2], [7], [8, 16, 18, 21, 22, 23, 24, 25, 26, 27, 28, 29], [], [8, 22, 23, 24, 26, 27, 28, 29]⟩,
  ⟨#[-8, -7, -7, -6, -7, -6, -6, -5, -5, -4, -4, -3, -3, -2, -6, -5, -1, 0, -5, -4, -4, -3, -3, -2, -2, -1, -4, -3, -3, -2], [7], [8, 14, 15, 18, 22, 23, 24, 25, 26, 27, 28, 29], [12], [8, 14, 15, 25, 26, 27, 28, 29]⟩,
  ⟨#[-8, -7, -7, -6, -7, -6, -6, -5, -5, -4, -4, -3, -5, -2, -6, -1, -3, 0, -5, -4, -4, -3, -3, -2, -2, -1, -4, -3, -3, -2], [], [8, 12, 14, 16, 18, 19, 20, 22, 23, 24, 25, 26, 27, 28, 29], [], [8, 14, 25, 26, 27, 28, 29]⟩,
  ⟨#[-9, -8, -8, -7, -7, -6, -6, -5, -5, -4, -4, -3, -3, -2, -8, -7, -1, 0, -5, -4, -4, -3, -3, -2, -2, -1, -5, -4, -4, -3], [7, 18], [14, 15, 18, 22, 23, 24, 25, 26, 29], [12], [25, 26, 27, 28, 29]⟩,
  ⟨#[-9, -8, -4, -3, -8, -7, -5, -4, -6, -5, -3, -2, -6, -3, -7, 0, -4, -1, -6, -5, -3, -2, -4, -3, -1, 0, -5, -4, 0, 1], [5, 7, 11], [10, 11, 14, 16, 19, 21, 22, 23, 25, 26, 27, 29], [6], [10, 11, 14, 23, 26, 27]⟩,
  ⟨#[-7, -6, -6, -5, -8, -7, -7, -6, -6, -5, -5, -4, -6, -3, -7, 0, -4, -1, -6, -5, -5, -4, -4, -3, -3, -2, -3, -2, -2, -1], [13], [8, 9, 10, 11, 12, 14, 16, 18, 19, 20, 22, 23, 24, 26], [3, 13], [8, 9, 10, 14, 26]⟩,
  ⟨#[-8, -7, -7, -6, -8, -7, -7, -6, -6, -5, -5, -4, -6, -3, -7, 0, -4, -1, -6, -5, -5, -4, -4, -3, -3, -2, -4, -3, -3, -2], [3, 13, 21], [8, 12, 14, 16, 18, 19, 20, 22, 23, 24, 26], [3, 13, 21], [8, 14, 26]⟩,
  ⟨#[-9, -8, -6, -5, -8, -7, -7, -6, -6, -5, -5, -4, -3, -2, -4, -3, -1, 0, -6, -5, -5, -4, -4, -3, -3, -2, -5, -4, -2, -1], [2, 3, 7], [18, 22, 23, 24, 25, 26, 27, 28, 29], [2, 3, 14], [25, 26, 27, 28, 29]⟩,
  ⟨#[-9, -8, -6, -5, -8, -7, -7, -6, -6, -5, -5, -4, -4, -3, -3, 0, -2, -1, -6, -5, -5, -4, -4, -3, -3, -2, -5, -4, -2, -1], [2, 7], [11, 18, 22, 23, 24, 25, 26, 27, 28], [2, 3, 12], [25, 26, 27, 28]⟩,
  ⟨#[-9, -8, -8, -7, -8, -7, -7, -6, -6, -5, -5, -4, -6, -3, -7, 0, -4, -1, -6, -5, -5, -4, -4, -3, -3, -2, -5, -4, -4, -3], [], [8, 12, 14, 16, 18, 19, 20, 22, 23, 24, 25, 26, 27, 28, 29], [], [8, 14, 25, 26, 27, 28, 29]⟩,
  ⟨#[-10, -9, -5, -4, -9, -8, -6, -5, -7, -6, -4, -3, -3, -2, -6, -5, -1, 0, -7, -6, -4, -3, -5, -4, -2, -1, -6, -5, -1, 0], [13], [10, 11, 15, 18, 20, 22, 23, 24, 26, 27], [13], [10, 11, 15, 22, 23, 24, 26, 27]⟩,
  ⟨#[-10, -9, -5, -4, -9, -8, -6, -5, -7, -6, -4, -3, -5, -2, -6, -1, -3, 0, -7, -6, -4, -3, -5, -4, -2, -1, -6, -5, -1, 0], [13], [10, 11, 12, 16, 18, 20, 22, 23, 24, 26, 27, 29], [3, 13], [10, 22, 23, 26, 27]⟩,
  ⟨#[-10, -9, -5, -4, -9, -8, -6, -5, -7, -6, -4, -3, -3, -2, -8, -7, -1, 0, -7, -6, -4, -3, -5, -4, -2, -1, -6, -5, -1, 0], [2, 5, 7, 13], [11, 14, 22, 24, 26, 27], [13], [10, 11, 14, 15, 22, 23, 24, 26, 27]⟩,
  ⟨#[-5, -4, -2, -1, -9, -8, -8, -7, -7, -6, -6, -5, -1, 0, -8, -7, 1, 2, -7, -6, -6, -5, -5, -4, -4, -3, -1, 0, 2, 3], [7], [14, 15, 18, 22, 23, 24, 25, 26, 27], [0], [14, 15, 25, 27]⟩,
  ⟨#[-7, -6, -6, -5, -9, -8, -8, -7, -7, -6, -6, -5, -3, -2, -8, -7, -1, 0, -7, -6, -6, -5, -5, -4, -4, -3, -3, -2, -2, -1], [0, 7, 12], [11, 14, 15, 18, 22, 23, 24, 29], [0, 3, 12], [11, 14, 15, 22, 29]⟩,
  ⟨#[-11, -10, -6, -5, -10, -9, -7, -6, -8, -7, -5, -4, -6, -3, -7, 0, -4, -1, -8, -7, -5, -4, -6, -5, -3, -2, -7, -6, -2, -1], [13], [10, 11, 12, 16, 18, 20, 22, 23, 24, 26, 27], [3, 13], [10, 22, 23, 26, 27]⟩,
  ⟨#[-11, -10, -6, -5, -10, -9, -9, -8, -8, -7, -7, -6, -3, -2, -8, -7, -1, 0, -8, -7, -7, -6, -6, -5, -5, -4, -7, -6, -2, -1], [7], [14, 18, 22, 23, 24, 25, 26, 27, 28, 29], [2], [14, 15, 22, 25, 26, 27, 28, 29]⟩,
  ⟨#[-13, -12, -6, -5, -10, -9, -9, -8, -8, -7, -7, -6, -3, -2, -12, -11, -1, 0, -8, -7, -7, -6, -6, -5, -5, -4, -9, -8, -2, -1], [7], [14, 15, 18, 22, 23, 24, 25, 26, 27, 28, 29], [2], [25, 26, 27, 28, 29]⟩,
  ⟨#[-2, -1, 1, 2, -1, 0, 0, 1, 1, 2, 2, 3, -1, 0, 0, 1, 1, 2, 1, 2, 2, 3, 3, 4, 4, 5, 2, 3, 5, 6], [2, 7, 11], [11, 13, 14, 15, 16, 17, 18, 22, 26, 27], [2, 3], [14, 15, 16, 17, 26, 27]⟩,
  ⟨#[-2, -1, 1, 2, -1, 0, 0, 1, 1, 2, 2, 3, -1, 0, 2, 3, 1, 2, 1, 2, 2, 3, 3, 4, 4, 5, 2, 3, 5, 6], [2, 3, 7], [13, 16, 17, 18, 22, 23, 24, 26, 27], [2, 7, 15], [11, 16, 22, 26, 27]⟩,
  ⟨#[-2, -1, 1, 2, -1, 0, 0, 1, 1, 2, 2, 3, 0, 1, -1, 2, 2, 3, 1, 2, 2, 3, 3, 4, 4, 5, 2, 3, 5, 6], [2, 7, 13], [11, 12, 13, 14, 16, 17, 18, 22, 23, 24, 26, 27], [2, 3, 7], [22, 26, 27]⟩,
  ⟨#[-2, -1, 3, 4, -1, 0, 0, 1, 1, 2, 2, 3, -1, 0, 6, 7, 1, 2, 1, 2, 2, 3, 3, 4, 4, 5, 2, 3, 7, 8], [7], [13, 16, 17, 18, 22, 23, 24, 25, 26, 27, 28, 29], [2], [16, 17, 25, 26, 27]⟩,
  ⟨#[-4, -3, 1, 2, -1, 0, 0, 1, 1, 2, 2, 3, -3, -2, 2, 3, -1, 0, 1, 2, 2, 3, 3, 4, 4, 5, 0, 1, 5, 6], [2, 3, 4, 7], [18, 22, 23, 24, 27], [2, 4, 15], [11, 14, 22, 27]⟩,
  ⟨#[-4, -3, 1, 2, -1, 0, 0, 1, 1, 2, 2, 3, -3, 0, -2, 3, -1, 2, 1, 2, 2, 3, 3, 4, 4, 5, 0, 1, 5, 6], [2, 3, 4, 7], [14, 17, 18, 22, 23, 24, 27], [2, 3, 15], [17, 26, 27]⟩,
  ⟨#[-4, -3, 3, 4, -1, 0, 0, 1, 1, 2, 2, 3, -3, -2, 6, 7, -1, 0, 1, 2, 2, 3, 3, 4, 4, 5, 0, 1, 7, 8], [4, 7], [18, 22, 23, 24, 25, 27, 28, 29], [2, 4], [25, 27]⟩,
  ⟨#[0, 1, 1, 2, -1, 0, 0, 1, 1, 2, 2, 3, -1, 0, 0, 1, 1, 2, 1, 2, 2, 3, 3, 4, 4, 5, 4, 5, 5, 6], [4, 7, 11], [8, 9, 10, 11, 15, 16, 17, 18, 22, 26], [3], [8, 9, 10, 14, 15, 16, 17, 26]⟩,
  ⟨#[-2, -1, 3, 4, -1, 0, 2, 3, 1, 2, 4, 5, 0, 3, -1, 6, 2, 5, 1, 2, 4, 5, 3, 4, 6, 7, 2, 3, 7, 8], [15], [10, 11, 12, 13, 14, 16, 17, 18, 20, 22, 23, 24, 26, 27], [3], [10, 22, 23, 25, 26, 27]⟩,
  ⟨#[-1, 0, 0, 1, 0, 1, 1, 2, 2, 3, 3, 4, -1, 0, 4, 5, 1, 2, 2, 3, 3, 4, 4, 5, 5, 6, 3, 4, 4, 5], [7], [8, 16, 17, 18, 22, 23, 24, 25, 26, 27, 28, 29], [14], [8, 16, 17, 25, 26, 27, 28, 29]⟩,
  ⟨#[-1, 0, 0, 1, 0, 1, 1, 2, 2, 3, 3, 4, -1, 2, 0, 5, 1, 4, 2, 3, 3, 4, 4, 5, 5, 6, 3, 4, 4, 5], [], [8, 13, 14, 16, 17, 18, 19, 20, 22, 23, 24, 25, 26, 27, 28, 29], [], [8, 16, 25, 26, 27, 28, 29]⟩,
  ⟨#[-1, 0, 2, 3, 0, 1, 1, 2, 2, 3, 3, 4, -1, 0, 0, 1, 1, 2, 2, 3, 3, 4, 4, 5, 5, 6, 3, 4, 6, 7], [2, 7, 11], [11, 14, 15, 16, 17, 18, 22, 26, 27], [2, 3], [15, 16, 17, 26, 27]⟩,
  ⟨#[-1, 0, 2, 3, 0, 1, 1, 2, 2, 3, 3, 4, -1, 0, 2, 3, 1, 2, 2, 3, 3, 4, 4, 5, 5, 6, 3, 4, 6, 7], [2, 5, 6, 7, 11], [11, 16, 22, 26, 27], [2], [11, 14, 15, 16, 17, 22, 26, 27]⟩,
  ⟨#[-1, 0, 2, 3, 0, 1, 1, 2, 2, 3, 3, 4, 0, 1, -1, 2, 2, 3, 2, 3, 3, 4, 4, 5, 5, 6, 3, 4, 6, 7], [2, 7, 11], [11, 13, 15, 16, 17, 18, 22, 26, 27], [2, 3], [15, 16, 17, 26, 27]⟩,
  ⟨#[0, 1, 1, 2, 0, 1, 1, 2, 2, 3, 3, 4, -1, 0, 4, 5, 1, 2, 2, 3, 3, 4, 4, 5, 5, 6, 4, 5, 5, 6], [3, 7, 11, 14, 15, 21], [8, 16, 17, 18, 22, 26], [3, 14, 21], [8, 16, 17, 25, 26]⟩,
  ⟨#[0, 1, 1, 2, 0, 1, 1, 2, 2, 3, 3, 4, -1, 2, 0, 5, 1, 4, 2, 3, 3, 4, 4, 5, 5, 6, 4, 5, 5, 6], [3, 15, 21], [8, 13, 16, 17, 18, 19, 20, 22, 23, 24, 26], [3, 21], [8, 16, 25, 26]⟩,
  ⟨#[1, 2, 2, 3, 0, 1, 1, 2, 2, 3, 3, 4, -1, 0, 2, 3, 1, 2, 2, 3, 3, 4, 4, 5, 5, 6, 5, 6, 6, 7], [0, 1, 2, 5, 6, 7, 11], [11, 16, 22, 26], [], [8, 9, 10, 11, 14, 15, 16, 17, 22, 26]⟩,
  ⟨#[1, 2, 2, 3, 0, 1, 1, 2, 2, 3, 3, 4, 0, 1, -1, 2, 2, 3, 2, 3, 3, 4, 4, 5, 5, 6, 5, 6, 6, 7], [7, 11], [8, 9, 10, 11, 13, 15, 16, 17, 18, 22, 26], [3], [8, 9, 10, 15, 16, 17, 26]⟩,
  ⟨#[1, 2, 2, 3, 0, 1, 1, 2, 2, 3, 3, 4, -1, 0, 4, 5, 1, 2, 2, 3, 3, 4, 4, 5, 5, 6, 5, 6, 6, 7], [3, 7, 15], [8, 9, 10, 16, 17, 18, 22, 23, 24, 26], [3, 14], [8, 9, 10, 16, 17, 25, 26]⟩,
  ⟨#[1, 2, 2, 3, 0, 1, 1, 2, 2, 3, 3, 4, -1, 2, 0, 5, 1, 4, 2, 3, 3, 4, 4, 5, 5, 6, 5, 6, 6, 7], [15], [8, 9, 10, 11, 13, 16, 17, 18, 19, 20, 22, 23, 24, 26], [3], [8, 9, 10, 16, 25, 26]⟩,
  ⟨#[2, 3, 3, 4, 0, 1, 1, 2, 2, 3, 3, 4, -1, 0, 6, 7, 1, 2, 2, 3, 3, 4, 4, 5, 5, 6, 6, 7, 7, 8], [0, 7, 14], [11, 16, 17, 18, 22, 23, 24, 29], [0, 3], [11, 16, 17, 22]⟩,
  ⟨#[4, 5, 7, 8, 0, 1, 1, 2, 2, 3, 3, 4, -1, 0, 10, 11, 1, 2, 2, 3, 3, 4, 4, 5, 5, 6, 8, 9, 11, 12], [7], [16, 17, 18, 22, 23, 24, 25, 26, 27, 28, 29], [0], [16, 17, 25]⟩,
  ⟨#[-1, 0, 4, 5, 0, 1, 3, 4, 2, 3, 5, 6, -1, 0, 4, 5, 1, 2, 2, 3, 5, 6, 4, 5, 7, 8, 3, 4, 8, 9], [2, 5, 7], [11, 14, 16, 22, 23, 24, 26, 27], [6], [10, 11, 15, 16, 17, 23, 26, 27]⟩,
  ⟨#[-1, 0, 4, 5, 0, 1, 3, 4, 2, 3, 5, 6, -1, 2, 0, 5, 1, 4, 2, 3, 5, 6, 4, 5, 7, 8, 3, 4, 8, 9], [2, 5, 7], [11, 14, 16, 17, 19, 22, 23, 24, 26, 27], [2, 6, 7], [11, 16, 26, 27]⟩,
  ⟨#[-1, 0, 4, 5, 0, 1, 3, 4, 2, 3, 5, 6, -1, 0, 6, 7, 1, 2, 2, 3, 5, 6, 4, 5, 7, 8, 3, 4, 8, 9], [2, 3, 5, 7, 15], [16, 22, 24, 26, 27], [], [10, 11, 16, 17, 22, 23, 24, 25, 26, 27]⟩,
  ⟨#[0, 1, 1, 2, 1, 2, 2, 3, 3, 4, 4, 5, 0, 3, -1, 6, 2, 5, 3, 4, 4, 5, 5, 6, 6, 7, 4, 5, 5, 6], [], [8, 13, 16, 17, 18, 19, 20, 22, 23, 24, 25, 26, 27, 28, 29], [], [8, 16, 25, 26, 27, 28, 29]⟩,
  ⟨#[0, 1, 3, 4, 1, 2, 2, 3, 3, 4, 4, 5, -1, 0, 2, 3, 1, 2, 3, 4, 4, 5, 5, 6, 6, 7, 4, 5, 7, 8], [2, 7, 11], [11, 14, 15, 16, 17, 18, 22, 26, 27], [2, 3], [14, 15, 16, 17, 26, 27]⟩,
  ⟨#[0, 1, 3, 4, 1, 2, 2, 3, 3, 4, 4, 5, 0, 1, -1, 2, 2, 3, 3, 4, 4, 5, 5, 6, 6, 7, 4, 5, 7, 8], [2, 7, 11], [11, 15, 16, 17, 18, 22, 26, 27], [2, 3], [15, 16, 17, 26, 27]⟩,
  ⟨#[1, 2, 2, 3, 1, 2, 2, 3, 3, 4, 4, 5, 0, 3, -1, 6, 2, 5, 3, 4, 4, 5, 5, 6, 6, 7, 5, 6, 6, 7], [3, 15, 21], [8, 13, 16, 17, 18, 19, 20, 22, 23, 24, 26], [3, 21], [8, 16, 25, 26]⟩,
  ⟨#[2, 3, 3, 4, 1, 2, 2, 3, 3, 4, 4, 5, 0, 3, -1, 6, 2, 5, 3, 4, 4, 5, 5, 6, 6, 7, 6, 7, 7, 8], [15], [8, 9, 10, 11, 13, 16, 17, 18, 19, 20, 22, 23, 24, 26], [3], [8, 9, 10, 16, 25, 26]⟩,
  ⟨#[0, 1, 5, 6, 1, 2, 4, 5, 3, 4, 6, 7, 0, 3, -1, 6, 2, 5, 3, 4, 6, 7, 5, 6, 8, 9, 4, 5, 9, 10], [2, 5, 7], [11, 16, 17, 19, 22, 23, 24, 26, 27], [2, 6, 7], [11, 16, 26, 27]⟩,
  ⟨#[-4, -3, -1, 0, 2, 3, 3, 4, 4, 5, 5, 6, -3, -2, 6, 7, -1, 0, 4, 5, 5, 6, 6, 7, 7, 8, 0, 1, 3, 4], [2, 7], [18, 22, 23, 24, 25, 27, 28, 29], [14], [17, 25, 28, 29]⟩,
  ⟨#[0, 1, 1, 2, 2, 3, 3, 4, 4, 5, 5, 6, -1, 0, 6, 7, 1, 2, 4, 5, 5, 6, 6, 7, 7, 8, 4, 5, 5, 6], [7, 18], [16, 17, 18, 22, 23, 24, 25, 26, 29], [14], [16, 17, 25, 26, 27, 28, 29]⟩,
  ⟨#[0, 1, 5, 6, 3, 4, 4, 5, 5, 6, 6, 7, -1, 0, 6, 7, 1, 2, 5, 6, 6, 7, 7, 8, 8, 9, 4, 5, 9, 10], [2, 3, 7], [16, 17, 18, 22, 23, 24, 26, 27], [2, 15], [11, 14, 16, 17, 22, 26, 27]⟩,
  ⟨#[0, 1, 7, 8, 3, 4, 4, 5, 5, 6, 6, 7, -1, 0, 10, 11, 1, 2, 5, 6, 6, 7, 7, 8, 8, 9, 4, 5, 11, 12], [7], [16, 17, 18, 22, 23, 24, 25, 26, 27, 28, 29], [2], [16, 17, 25, 26, 27]⟩,
  ⟨#[0, 1, 3, 4, 6, 7, 7, 8, 8, 9, 9, 10, -1, 0, 10, 11, 1, 2, 8, 9, 9, 10, 10, 11, 11, 12, 4, 5, 7, 8], [7], [16, 17, 18, 22, 23, 24, 25, 26, 27, 28, 29], [14], [16, 17, 25, 28, 29]⟩
]

def record (k : Fin 140) : Certificate := records[k.val]!
def first (i : Fin 30) : ℤ := firstCoordinates[i.val]!
def second (i : Fin 30) : ℤ := secondCoordinates[i.val]!
def degree (c : Certificate) (i : Fin 30) : ℤ := c.degrees[i.val]!

/-- Arguments are target row, source column: the source loses one Maslov degree. -/
def Allowed (c : Certificate) (i j : Fin 30) : Prop :=
  first i < first j ∧ second i ≤ second j ∧ degree c i = degree c j - 1

def MixedAllowed (c : Certificate) (i j : Fin 30) : Prop :=
  Allowed c i j ∧ second i < second j

instance (c : Certificate) (i j : Fin 30) : Decidable (Allowed c i j) :=
  inferInstanceAs (Decidable (_ ∧ _ ∧ _))
instance (c : Certificate) (i j : Fin 30) : Decidable (MixedAllowed c i j) :=
  inferInstanceAs (Decidable (_ ∧ _))

def totalBudget (c : Certificate) : ℕ :=
  c.totalRows.toFinset.card + c.totalCols.toFinset.card
def mixedBudget (c : Certificate) : ℕ :=
  c.mixedRows.toFinset.card + c.mixedCols.toFinset.card

/-- Finite computational assertion only; matrix rank conclusions are separate. -/
def Valid (c : Certificate) : Prop :=
  c.degrees.size = 30 ∧
  (∀ i j : Fin 30, Allowed c i j → i ∈ c.totalRows ∨ j ∈ c.totalCols) ∧
  (∀ i j : Fin 30, MixedAllowed c i j → i ∈ c.mixedRows ∨ j ∈ c.mixedCols) ∧
  min (totalBudget c) (4 + mixedBudget c) ≤ 13 ∧
  min (totalBudget c) (2 + mixedBudget c) ≤ 11

instance (c : Certificate) : Decidable (Valid c) :=
  by
    have d0 : Decidable (c.degrees.size = 30) := inferInstance
    have d1 : Decidable (∀ i j : Fin 30, Allowed c i j → i ∈ c.totalRows ∨ j ∈ c.totalCols) := inferInstance
    have d2 : Decidable (∀ i j : Fin 30, MixedAllowed c i j → i ∈ c.mixedRows ∨ j ∈ c.mixedCols) := inferInstance
    have d3 : Decidable (min (totalBudget c) (4 + mixedBudget c) ≤ 13) := inferInstance
    have d4 : Decidable (min (totalBudget c) (2 + mixedBudget c) ≤ 11) := inferInstance
    unfold Valid
    exact @instDecidableAnd _ _ d0 (@instDecidableAnd _ _ d1 (@instDecidableAnd _ _ d2 (@instDecidableAnd _ _ d3 d4)))

end SP4Table22
Source
Ryan Shin, Table 22: a common-differential rank obstruction for Ui15/B1 and Ui15/G13, cycle12_table22_common_rank.md, Sections 2–4, equations (5)–(7); note SHA-256 04202f0649254279d91bad21875b82ddbd1a8fc8812454f5e3ca54b9c65b630e. Exact ordered records from cycle12_table22_common_rank.json, SHA-256 49ae9b38334cb89ff1eee916e4d96680850e02d51b493fd282f44181bd9c31ac. This contribution checks all 140 saved records and both rank bounds, not the unbounded source-enumeration or Floer/geometric completeness argument.
View graph