Canonical branch pruning for the cubic matrix replay

Certificate/CubicMatrixExhaustive.lean removed the generated tree, leaving the leaf payloads as the whole remaining cost. This module supplies the machinery to cut those down, and to cut the traversal down with them.

Everything here is generic in the vertex count and the degree. That is deliberate: the genus-four instance at n = 6 is a proof of concept for the genus-five instance at n = 8, where the numbers are

            connected leaves   + cut 0   + cut 0 and cut 1
n = 6                    640        46                  20
n = 8                168,840     4,470                 777

The two cuts

A node's state is really (S, residual capacity on V \ S) with S the set of processed vertices; the row-by-row scheme is the special case where S is a prefix. The freedom to choose which vertex to process next is exactly the freedom to sort by relabeling, and that gives two cuts:

• cut 0 — relabel 1 … n-1 so that row 0 is ascending;
• cut 1 — then, within each maximal block of positions sharing a row-0 value, relabel so that row 1 is ascending. Such a permutation moves vertices only inside row-0 level sets, so it preserves cut 0.

Both are witnessed by explicit permutations, so no canonical labeling happens inside Lean.

Ascending is deliberate and is worth about 25 per cent over descending: cut 1 does not move position 1, and ascending puts the smallest row-0 value there, leaving larger blocks for cut 1 to act on.

What is here and what is not

canonicalPrefix is the decidable predicate, prunedCheck is the traversal that skips non-canonical branches, and prunedCheck_sound is its soundness. Because the predicate only inspects rows 0 and 1, it is decided as soon as those are chosen, so the pruning happens at the top of the tree where it saves the most.

The remaining obligation is named CanonicalRepresentative: every candidate is isomorphic to a canonical one. It is stated here and not proved. Its empirical form was checked at n = 6, where the 20 canonical connected leaves carry all six atlas indices; see the accompanying analysis.

The canonical predicate

def Utilities.Certificate.CubicMatrixReplay.SortedAsc : List ℕ → Bool

A list of naturals is ascending.

Equations

• Utilities.Certificate.CubicMatrixReplay.SortedAsc [] = true
• Utilities.Certificate.CubicMatrixReplay.SortedAsc [head] = true
• Utilities.Certificate.CubicMatrixReplay.SortedAsc (a :: b :: rest) = (decide (a ≤ b) && Utilities.Certificate.CubicMatrixReplay.SortedAsc (b :: rest))

def Utilities.Certificate.CubicMatrixReplay.BlocksSorted : List ℕ → List ℕ → Bool

BlocksSorted keys values asks that values be ascending across every adjacent pair whose keys agree. With keys the tail of row 0 and values row 1, this is cut 1.

Equations

• One or more equations did not get rendered due to their size.
• Utilities.Certificate.CubicMatrixReplay.BlocksSorted x✝¹ x✝ = true

def Utilities.Certificate.CubicMatrixReplay.canonicalPrefix (rows : List (List ℕ)) : Bool

The canonical predicate on a row list. It inspects only rows 0 and 1, so it is decided as soon as those two are chosen.

Equations

• One or more equations did not get rendered due to their size.
• Utilities.Certificate.CubicMatrixReplay.canonicalPrefix [] = true
• Utilities.Certificate.CubicMatrixReplay.canonicalPrefix [row1] = (Utilities.Certificate.CubicMatrixReplay.SortedAsc row1 && true)

theorem Utilities.Certificate.CubicMatrixReplay.canonicalPrefix_append {rows extra : List (List ℕ)} (h : canonicalPrefix rows = true) : 2 ≤ rows.length → canonicalPrefix (rows ++ extra) = true

Only the first two rows matter, so extending a canonical row list on the right cannot break canonicality.

Accepting along a path

def Utilities.Certificate.CubicMatrixReplay.AcceptsAlong (accept : List (List ℕ) → Bool) : List (List ℕ) → List (List ℕ) → Prop

Every nonempty prefix of rows, read after path, is accepted. This is what a pruned traversal needs in order to reach a given row list.

Equations

• Utilities.Certificate.CubicMatrixReplay.AcceptsAlong accept x✝ [] = True
• Utilities.Certificate.CubicMatrixReplay.AcceptsAlong accept x✝ (row :: rest) = (accept (x✝ ++ [row]) = true ∧ Utilities.Certificate.CubicMatrixReplay.AcceptsAlong accept (x✝ ++ [row]) rest)

The pruned traversal

def Utilities.Certificate.CubicMatrixReplay.prunedCheck (accept leafDecide : List (List ℕ) → Bool) : ℕ → List ℕ → List (List ℕ) → Bool

Exhaustive check that skips branches the accept predicate rejects. A rejected branch is discharged immediately, so the subtree below it is never traversed.

Equations

• One or more equations did not get rendered due to their size.
• Utilities.Certificate.CubicMatrixReplay.prunedCheck accept leafDecide 0 x✝¹ x✝ = false
• Utilities.Certificate.CubicMatrixReplay.prunedCheck accept leafDecide n.succ [] x✝ = leafDecide x✝

theorem Utilities.Certificate.CubicMatrixReplay.prunedCheck_sound (accept leafDecide : List (List ℕ) → Bool) {capacities : List ℕ} {rows : List (List ℕ)} (hFollows : Follows capacities rows) (fuel : ℕ) (path : List (List ℕ)) : prunedCheck accept leafDecide fuel capacities path = true → AcceptsAlong accept path rows → leafDecide (path ++ rows) = true

Soundness of the pruned traversal. A row list produced by the branching whose prefixes are all accepted is accepted by leafDecide. Rows that fail accept somewhere are deliberately not covered; supplying them is the job of CanonicalRepresentative.

Canonicality reaches every prefix

theorem Utilities.Certificate.CubicMatrixReplay.acceptsAlong_of_two (row0 row1 : List ℕ) (h : canonicalPrefix [row0, row1] = true) (acc rest : List (List ℕ)) : AcceptsAlong canonicalPrefix (row0 :: row1 :: acc) rest

Once rows 0 and 1 are fixed and canonical, every longer path stays accepted, so a pruned traversal descends all the way.

theorem Utilities.Certificate.CubicMatrixReplay.acceptsAlong_canonicalPrefix (rows : List (List ℕ)) (h : canonicalPrefix rows = true) : AcceptsAlong canonicalPrefix [] rows

A canonical row list is accepted along every one of its prefixes. This is the bridge from the predicate to what prunedCheck_sound consumes.

From index-level inequalities to the Boolean predicates

theorem Utilities.Certificate.CubicMatrixReplay.sortedAsc_map_range' (f : ℕ → ℕ) (len s : ℕ) : (∀ (k : ℕ), s ≤ k → k + 1 < s + len → f k ≤ f (k + 1)) → SortedAsc (List.map f (List.range' s len)) = true

An ascending run of values over an arithmetic index range is SortedAsc.

theorem Utilities.Certificate.CubicMatrixReplay.blocksSorted_map_range' (f g : ℕ → ℕ) (len s : ℕ) : (∀ (k : ℕ), s ≤ k → k + 1 < s + len → f k = f (k + 1) → g k ≤ g (k + 1)) → BlocksSorted (List.map f (List.range' s len)) (List.map g (List.range' s len)) = true

Values that ascend across every adjacent pair of equal keys, both read off the same arithmetic index range, satisfy BlocksSorted.

theorem Utilities.Certificate.CubicMatrixReplay.canonicalPrefix_rowsOf (M : ℕ → ℕ → ℕ) (n : ℕ) (hCut0 : ∀ (k : ℕ), 1 ≤ k → k + 1 < n → M 0 k ≤ M 0 (k + 1)) (hCut1 : ∀ (k : ℕ), 2 ≤ k → k + 1 < n → M 0 k = M 0 (k + 1) → M 1 k ≤ M 1 (k + 1)) : canonicalPrefix (rowsOf M 0 n) = true

The two index-level cuts imply the Boolean canonical predicate on the whole row list. This is stated for an arbitrary matrix and vertex count, so the small cases are discharged here rather than assumed away.

A weighted key and the exchange step

def Utilities.Certificate.CubicMatrixReplay.weightKey (n : ℕ) (F : ℕ → ℕ) : ℕ

The weighted key of one row of a matrix: entry j carries weight n - j, so the weights drop by exactly one at every step inside the range. Minimizing this is the same as minimizing the row lexicographically, but it needs no lexicographic order on lists.

Equations

• Utilities.Certificate.CubicMatrixReplay.weightKey n F = ∑ j ∈ Finset.range n, (n - j) * F j

theorem Utilities.Certificate.CubicMatrixReplay.weightKey_split (n k : ℕ) (hk : k + 1 < n) (F : ℕ → ℕ) : weightKey n F = ∑ j ∈ Finset.range n \ {k, k + 1}, (n - j) * F j + ((n - (k + 1)) * (F k + F (k + 1)) + F k)

Split the weighted key into the two positions k, k + 1 and the rest.

theorem Utilities.Certificate.CubicMatrixReplay.weightKey_swap (n k : ℕ) (hk : k + 1 < n) (F G : ℕ → ℕ) (hOther : ∀ j < n, j ≠ k → j ≠ k + 1 → G j = F j) (hAt : G k = F (k + 1)) (hAt' : G (k + 1) = F k) : (F (k + 1) < F k → weightKey n G < weightKey n F) ∧ (F k = F (k + 1) → weightKey n G = weightKey n F)

The exchange step. If G is F with the entries at k and k + 1 interchanged, then the weighted key drops exactly when F descends there, and is unchanged exactly when F is flat there.

Transporting the matrix along a relabeling

theorem Utilities.Certificate.CubicMatrixReplay.matrixOf_relabel {n p : ℕ} (core : ExplicitPotential.Core n p) (σ : Equiv.Perm (Fin n)) (i j : ℕ) (hi : i < n) (hj : j < n) : matrixOf (core.relabel σ) i j = core.pairMultiplicity (σ⁻¹ ⟨i, hi⟩) (σ⁻¹ ⟨j, hj⟩)

The multiplicity table of a relabeled core, read at the original vertices. This is the only computation rule the exchange argument needs.

def Utilities.Certificate.CubicMatrixReplay.swapIdx (k i : ℕ) : ℕ

The adjacent transposition of k and k + 1, as a map on indices.

Equations

• Utilities.Certificate.CubicMatrixReplay.swapIdx k i = if i = k then k + 1 else if i = k + 1 then k else i

theorem Utilities.Certificate.CubicMatrixReplay.swapIdx_of_ne {k i : ℕ} (h : i ≠ k) (h' : i ≠ k + 1) : swapIdx k i = i

theorem Utilities.Certificate.CubicMatrixReplay.swapIdx_left (k : ℕ) : swapIdx k k = k + 1

theorem Utilities.Certificate.CubicMatrixReplay.swapIdx_right (k : ℕ) : swapIdx k (k + 1) = k

theorem Utilities.Certificate.CubicMatrixReplay.swapIdx_lt {n k i : ℕ} (hk : k + 1 < n) (hi : i < n) : swapIdx k i < n

theorem Utilities.Certificate.CubicMatrixReplay.coe_swap_mk {n k : ℕ} (hk : k + 1 < n) (j : ℕ) (hj : j < n) : ↑((Equiv.swap ⟨k, ⋯⟩ ⟨k + 1, hk⟩) ⟨j, hj⟩) = swapIdx k j

The value of the adjacent transposition, read through the Fin coercion.

theorem Utilities.Certificate.CubicMatrixReplay.matrixOf_relabel_swap {n p : ℕ} (core : ExplicitPotential.Core n p) (σ : Equiv.Perm (Fin n)) {k : ℕ} (hk : k + 1 < n) (i j : ℕ) (hi : i < n) (hj : j < n) : matrixOf (core.relabel (Equiv.swap ⟨k, ⋯⟩ ⟨k + 1, hk⟩ * σ)) i j = matrixOf (core.relabel σ) (swapIdx k i) (swapIdx k j)

Relabeling by an extra adjacent transposition interchanges the two corresponding rows and columns of the multiplicity table.

The key of a relabeling

def Utilities.Certificate.CubicMatrixReplay.relabelKey {n p : ℕ} (core : ExplicitPotential.Core n p) (row : ℕ) (σ : Equiv.Perm (Fin n)) : ℕ

The weighted key of row row of the multiplicity table of core relabeled along σ.

Equations

• One or more equations did not get rendered due to their size.

theorem Utilities.Certificate.CubicMatrixReplay.relabelKey_swap {n p : ℕ} (core : ExplicitPotential.Core n p) (σ : Equiv.Perm (Fin n)) (row k : ℕ) (hk : k + 1 < n) (hRowLt : row < n) (hRow : row ≠ k) (hRow' : row ≠ k + 1) : (matrixOf (core.relabel σ) row (k + 1) < matrixOf (core.relabel σ) row k → relabelKey core row (Equiv.swap ⟨k, ⋯⟩ ⟨k + 1, hk⟩ * σ) < relabelKey core row σ) ∧ (matrixOf (core.relabel σ) row k = matrixOf (core.relabel σ) row (k + 1) → relabelKey core row (Equiv.swap ⟨k, ⋯⟩ ⟨k + 1, hk⟩ * σ) = relabelKey core row σ)

The exchange step, for a relabeling. Composing with the adjacent transposition of k and k + 1 interchanges those two entries of any row it fixes, so it strictly lowers that row's key exactly when the row descends there, and leaves the key alone when the row is flat there.

Canonical relabeling of a bare core

theorem Utilities.Certificate.CubicMatrixReplay.exists_canonical_relabel {n p degree : ℕ} (core : ExplicitPotential.Core n p) (hConnected : core.Connected) (hDegree : ∀ (vertex : Fin n), core.incidenceDegree vertex = degree) : ∃ (sigma : Equiv.Perm (Fin n)), (core.relabel sigma).Connected ∧ (∀ (vertex : Fin n), (core.relabel sigma).incidenceDegree vertex = degree) ∧ canonicalPrefix (rowsOf (matrixOf (core.relabel sigma)) 0 n) = true ∧ ∀ (i j : Fin n), core.pairMultiplicity i j = (core.relabel sigma).pairMultiplicity (sigma i) (sigma j)

Every connected regular ordered core is vertex-relabelled to a core whose first two multiplicity rows satisfy `canonicalPrefix`.