A row-by-row replay tree for loopless regular multiplicity matrices

A finite classifier for loopless regular cores can work with the unordered vertex-pair multiplicity table. This module supplies its generic completeness device: a compact finite witness that some displayed list of tables exhausts every table which can arise.

This module is that device, and nothing else. It defines

• boundedCompositions, the weak compositions of one remaining degree into the capacities of the still-unvisited vertices;
• Follows, the statement that a list of strict-upper-triangular rows is produced by the row-by-row branching;
• ReplayTree, a fuelled sibling-chain tree whose branches are keyed by those compositions, with a Boolean checker validCheck;
• rowsOf / entryOf, the translation between a multiplicity matrix and its row list, and matrixOf, the multiplicity matrix of an ordered core;
• MatrixConnected, the decidable cut form of ExplicitPotential.Core.Connected read off the table.

The two results that matter are validCheck_sound — a tree passing the Boolean check accepts every row list produced by the branching — and follows_capsOf_rowsOf — every symmetric, zero-diagonal, constant-row-sum matrix does follow the branching. Exhaustiveness is proved from the weak-composition membership characterization mem_boundedCompositions; there is no native_decide, no decide over endpoint functions, and no search.

Nothing here is specific to eight vertices or to degree three. The vertex count and the common degree are parameters, so one generated tree shape serves the genus-four (6/9) and genus-five (8/12) classifiers.

Disconnected tables satisfy the same row-sum conditions and therefore also reach a leaf. A generated leaf may carry no atlas target for those; the decoding hypothesis of the composed statements only fires on tables satisfying MatrixConnected.

This is the generic checker side only. Application-specific datasets, leaf decoders, and classifier handoff theorems belong in their application layer.

Weak compositions with capacities

def Utilities.Certificate.CubicMatrixReplay.boundedCompositions (total : ℕ) : List ℕ → List (List ℕ)

All ways of splitting total into capacities.length natural summands, in order, with the k-th summand bounded by the k-th capacity. This is the branch set of one vertex of the completion tree: the remaining degree of the current vertex is distributed over the vertices that come after it.

Equations

• One or more equations did not get rendered due to their size.
• Utilities.Certificate.CubicMatrixReplay.boundedCompositions total [] = if total = 0 then [[]] else []

theorem Utilities.Certificate.CubicMatrixReplay.mem_boundedCompositions {total : ℕ} {capacities parts : List ℕ} : parts ∈ boundedCompositions total capacities ↔ List.Forall₂ (fun (x1 x2 : ℕ) => x1 ≤ x2) parts capacities ∧ parts.sum = total

boundedCompositions enumerates exactly the capacity-bounded weak compositions. This is the finite combinatorial fact that makes the tree branching exhaustive.

The branching relation

inductive Utilities.Certificate.CubicMatrixReplay.Follows : List ℕ → List (List ℕ) → Prop

Follows capacities rows says that rows is the strict-upper-triangular row list of a matrix built by the row-by-row completion, starting from the residual degree vector capacities. The head capacity is the remaining degree of the current vertex; the chosen row is a capacity-bounded weak composition of it, and the tail capacities are decreased accordingly.

• nil : Follows [] []
• cons {remaining : ℕ} {capacities parts : List ℕ} {rows : List (List ℕ)} (hParts : parts ∈ boundedCompositions remaining capacities) (hRows : Follows (List.zipWith (fun (x1 x2 : ℕ) => x1 - x2) capacities parts) rows) : Follows (remaining :: capacities) (parts :: rows)

The replay tree

inductive Utilities.Certificate.CubicMatrixReplay.ReplayTree (α : Type u_1) : Type u_1

A fuelled row-by-row completion tree. branch stores the composition that keys this child together with the child itself and the next sibling, so the sibling chain at one vertex is spelled out linearly; reject terminates a sibling chain, and accept carries the payload of a completed matrix.

• accept {α : Type u_1} : α → ReplayTree α
• reject {α : Type u_1} : ReplayTree α
• branch {α : Type u_1} : List ℕ → ReplayTree α → ReplayTree α → ReplayTree α

def Utilities.Certificate.CubicMatrixReplay.chainCheck {α : Type u_1} (sub : ReplayTree α → List ℕ → List (List ℕ) → Bool) (capacities : List ℕ) (path : List (List ℕ)) : ReplayTree α → List (List ℕ) → Bool

Check one sibling chain against the list todo of compositions it must cover. The chain must list them in exactly the enumeration order of boundedCompositions; sub checks each child against the decreased capacities and the extended path.

Equations

• One or more equations did not get rendered due to their size.
• Utilities.Certificate.CubicMatrixReplay.chainCheck sub capacities path x✝ [] = true
• Utilities.Certificate.CubicMatrixReplay.chainCheck sub capacities path x✝ (head :: tail) = false

def Utilities.Certificate.CubicMatrixReplay.validCheck {α : Type u_1} (leafCheck : List (List ℕ) → α → Bool) : ℕ → ReplayTree α → List ℕ → List (List ℕ) → Bool

The Boolean replay check. fuel bounds the number of vertices still to be visited, capacities is the residual degree vector, and path records the rows chosen so far. At a completed matrix the caller-supplied leafCheck inspects the path and the stored payload; at an unfinished vertex the tree must be a sibling chain covering every capacity-bounded weak composition of the head capacity.

Equations

• One or more equations did not get rendered due to their size.
• Utilities.Certificate.CubicMatrixReplay.validCheck leafCheck 0 x✝² x✝¹ x✝ = false
• Utilities.Certificate.CubicMatrixReplay.validCheck leafCheck n.succ (Utilities.Certificate.CubicMatrixReplay.ReplayTree.accept value) [] x✝ = leafCheck x✝ value
• Utilities.Certificate.CubicMatrixReplay.validCheck leafCheck n.succ x✝¹ [] x✝ = false

theorem Utilities.Certificate.CubicMatrixReplay.chainCheck_sound {α : Type u_1} {sub : ReplayTree α → List ℕ → List (List ℕ) → Bool} {Good : List (List ℕ) → Prop} {capacities : List ℕ} {path rows : List (List ℕ)} {part : List ℕ} (hSub : ∀ (child : ReplayTree α) (caps : List ℕ) (subPath : List (List ℕ)), sub child caps subPath = true → Follows caps rows → Good (subPath ++ rows)) (hFollows : Follows (List.zipWith (fun (x1 x2 : ℕ) => x1 - x2) capacities part) rows) (tree : ReplayTree α) (todo : List (List ℕ)) : chainCheck sub capacities path tree todo = true → part ∈ todo → Good (path ++ part :: rows)

Every composition listed in todo is genuinely handled by a checked sibling chain. The argument is an induction along the chain, so no search over the tree is performed.

theorem Utilities.Certificate.CubicMatrixReplay.validCheck_sound {α : Type u_1} (leafCheck : List (List ℕ) → α → Bool) (rows : List (List ℕ)) (fuel : ℕ) (tree : ReplayTree α) (capacities : List ℕ) (path : List (List ℕ)) : validCheck leafCheck fuel tree capacities path = true → Follows capacities rows → ∃ (value : α), leafCheck (path ++ rows) value = true

Replay soundness. A tree passing validCheck accepts every row list produced by the branching, and its leaf check succeeds on the corresponding path. Nothing about the tree's shape is assumed beyond the Boolean check; in particular exhaustiveness of the branching comes entirely from mem_boundedCompositions.

Multiplicity matrices and their row lists

structure Utilities.Certificate.CubicMatrixReplay.Conditions (n deg : ℕ) (M : ℕ → ℕ → ℕ) : Prop

The finite conditions defining a loopless deg-regular multiplicity matrix on the vertex set {0, …, n-1}. Entries outside that range are ignored, so the matrix may be given as a total function.

• symm (i j : ℕ) : i < n → j < n → M i j = M j i

  The table is symmetric.

• diag (i : ℕ) : i < n → M i i = 0

  No vertex carries a loop.

• rowSum (i : ℕ) : i < n → ∑ j ∈ Finset.range n, M i j = deg

  Every vertex has degree deg.

def Utilities.Certificate.CubicMatrixReplay.rowsOf (M : ℕ → ℕ → ℕ) : ℕ → ℕ → List (List ℕ)

The strict-upper-triangular row list of M: rowsOf M i len lists the rows of vertices i, …, i + len - 1, each row recording the multiplicities to the strictly later vertices in that range.

Equations

• Utilities.Certificate.CubicMatrixReplay.rowsOf M x✝ 0 = []
• Utilities.Certificate.CubicMatrixReplay.rowsOf M x✝ len.succ = List.map (fun (j : ℕ) => M x✝ j) (List.range' (x✝ + 1) len) :: Utilities.Certificate.CubicMatrixReplay.rowsOf M (x✝ + 1) len

def Utilities.Certificate.CubicMatrixReplay.capsOf (deg : ℕ) (M : ℕ → ℕ → ℕ) (i len : ℕ) : List ℕ

The residual degree vector of vertices i, …, i + len - 1 after the rows of vertices 0, …, i - 1 have been fixed.

Equations

• Utilities.Certificate.CubicMatrixReplay.capsOf deg M i len = List.map (fun (j : ℕ) => deg - ∑ j' ∈ Finset.range i, M j' j) (List.range' i len)

theorem Utilities.Certificate.CubicMatrixReplay.capsOf_zero (deg : ℕ) (M : ℕ → ℕ → ℕ) (n : ℕ) : capsOf deg M 0 n = List.replicate n deg

At the root the residual degree vector is constant.

theorem Utilities.Certificate.CubicMatrixReplay.follows_capsOf_rowsOf {n deg : ℕ} {M : ℕ → ℕ → ℕ} (h : Conditions n deg M) (len i : ℕ) : i + len = n → Follows (capsOf deg M i len) (rowsOf M i len)

Branching completeness. Every loopless deg-regular multiplicity matrix follows the row-by-row branching, starting from any prefix position. This is the statement that the tree's branch sets miss nothing.

Reading a matrix entry back off the row list

def Utilities.Certificate.CubicMatrixReplay.entryOf (rows : List (List ℕ)) (i j : ℕ) : ℕ

The entry of a symmetric matrix recovered from its strict-upper-triangular row list.

Equations

• Utilities.Certificate.CubicMatrixReplay.entryOf rows i j = if i < j then (rows.getD i []).getD (j - i - 1) 0 else if j < i then (rows.getD j []).getD (i - j - 1) 0 else 0

theorem Utilities.Certificate.CubicMatrixReplay.entryOf_rowsOf {n deg : ℕ} {M : ℕ → ℕ → ℕ} (h : Conditions n deg M) (i j : ℕ) (hi : i < n) (hj : j < n) : entryOf (rowsOf M 0 n) i j = M i j

Round trip. On the vertex range the row list determines the matrix. A generated leaf may therefore be checked against the path alone.

Multiplicity matrix of an ordered core

def Utilities.Certificate.CubicMatrixReplay.matrixOf {n p : ℕ} (core : ExplicitPotential.Core n p) (i j : ℕ) : ℕ

The unordered vertex-pair multiplicity table of an ordered core, as a total function on ℕ.

Equations

• Utilities.Certificate.CubicMatrixReplay.matrixOf core i j = if hi : i < n then if hj : j < n then core.pairMultiplicity ⟨i, hi⟩ ⟨j, hj⟩ else 0 else 0

theorem Utilities.Certificate.CubicMatrixReplay.conditions_matrixOf {n p deg : ℕ} (core : ExplicitPotential.Core n p) (hLoopless : ∀ (edge : Fin p), core.tail edge ≠ core.head edge) (hDegree : ∀ (vertex : Fin n), core.incidenceDegree vertex = deg) : Conditions n deg (matrixOf core)

The multiplicity table of a loopless deg-regular ordered core satisfies the finite matrix conditions.

Connectedness at the level of the table

Disconnected matrices also satisfy Conditions and therefore also follow the branching, so the tree must reach them too. A generated leaf is allowed to carry no atlas target in that case; the decoding hypothesis below is only required to fire on connected tables. MatrixConnected is the cut form of ExplicitPotential.Core.Connected transported to the multiplicity table.

def Utilities.Certificate.CubicMatrixReplay.MatrixConnected (size : ℕ) (M : ℕ → ℕ → ℕ) : Prop

Cut connectedness of a multiplicity table on the vertex range. Cuts range over (Finset.range size).powerset rather than over all of Finset ℕ, so the predicate is decidable and a generated leaf record may discharge it by evaluation.

Equations

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

@[instance_reducible]

instance Utilities.Certificate.CubicMatrixReplay.decidableMatrixConnected (size : ℕ) (M : ℕ → ℕ → ℕ) : Decidable (MatrixConnected size M)

Cut connectedness of a bounded table is a finite check.

Equations

• Utilities.Certificate.CubicMatrixReplay.decidableMatrixConnected size M = id inferInstance

theorem Utilities.Certificate.CubicMatrixReplay.matrixConnected_congr {size : ℕ} {M M' : ℕ → ℕ → ℕ} (hEntries : ∀ (i j : ℕ), i < size → j < size → M i j = M' i j) (hM : MatrixConnected size M) : MatrixConnected size M'

Cut connectedness only reads entries inside the vertex range.

theorem Utilities.Certificate.CubicMatrixReplay.matrixConnected_matrixOf {n p : ℕ} (core : ExplicitPotential.Core n p) (hConnected : core.Connected) : MatrixConnected n (matrixOf core)

Core cut connectedness transports to the multiplicity table.