Generated data for the pruned cubic classifier at n = 8

Passive data only, and deliberately not a replay tree. Certificate/CubicMatrixCanonical.lean re-enumerates the branching itself and prunes it by canonicalPrefix, so nothing about the shape of the search has to be stored. What remains is the leaf payload, and only for the leaves the pruned traversal actually reaches.

• atlasTable is the unordered pair-multiplicity table of each atlas row, so Core.pairMultiplicity is evaluated once per row rather than once per leaf;
• payloadBuckets maps the row list of each connected canonical leaf to an atlas index and a vertex permutation matching it, in 251 buckets keyed by rowKey % 251.

Both are read by List.getD rather than by Matrix.vecCons. That is not a stylistic choice: ![...] indexing unfolds to Fin.cases, hence to Nat.rec with a dependent motive, once per index step, and at n = 8 the resulting kernel terms dominated everything else. Bucketing the payload table and flattening the two vector layers took the peak resident set of the largest traversal chunk from 3.7 GB to 0.8 GB.

A reached leaf missing from payloadBuckets is one whose table is disconnected; the checker discharges those through the decidable MatrixConnected. Nothing here is proved; the checking is done in the corresponding Certificate/...CanonicalClassifier.lean.

Generated classifier data with --n 8 --deg 3 --layout bucket.

@[reducible, inline]

abbrev AtanasovRanganathan.Generated.GenusFiveCanonicalClassifierData.Payload : Type

Payload of a connected canonical leaf: an atlas index together with a vertex permutation matching the leaf table against that row.

Equations

• AtanasovRanganathan.Generated.GenusFiveCanonicalClassifierData.Payload = (Fin 20 × List (Fin 8))

def AtanasovRanganathan.Generated.GenusFiveCanonicalClassifierData.atlasTable : List (List (List ℕ))

The pair-multiplicity tables of the 20 atlas rows.

Equations

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

def AtanasovRanganathan.Generated.GenusFiveCanonicalClassifierData.atlasEntry (idx : Fin 20) (a b : Fin 8) : ℕ

One entry of one atlas table.

Equations

• AtanasovRanganathan.Generated.GenusFiveCanonicalClassifierData.atlasEntry idx a b = ((AtanasovRanganathan.Generated.GenusFiveCanonicalClassifierData.atlasTable.getD ↑idx []).getD ↑a []).getD (↑b) 0

def AtanasovRanganathan.Generated.GenusFiveCanonicalClassifierData.permOf (p : List (Fin 8)) (i : Fin 8) : Fin 8

A stored permutation, read as a function.

Equations

• AtanasovRanganathan.Generated.GenusFiveCanonicalClassifierData.permOf p i = p.getD (↑i) 0

def AtanasovRanganathan.Generated.GenusFiveCanonicalClassifierData.rowKey (rows : List (List ℕ)) : ℕ

Fold a leaf's row list into a single numeral, base 4 since every entry is at most 3. This is only a lookup key: the checker verifies the payload it retrieves entry by entry, so a collision would cause pruned_valid to fail rather than to prove something false.

Equations

• AtanasovRanganathan.Generated.GenusFiveCanonicalClassifierData.rowKey rows = List.foldl (fun (acc : ℕ) (row : List ℕ) => List.foldl (fun (a x : ℕ) => a * 4 + x) acc row) 0 rows

def AtanasovRanganathan.Generated.GenusFiveCanonicalClassifierData.bucketCount : ℕ

The number of payload buckets.

Equations

• AtanasovRanganathan.Generated.GenusFiveCanonicalClassifierData.bucketCount = 251

def AtanasovRanganathan.Generated.GenusFiveCanonicalClassifierData.payloadBucketPart0 : List (List (ℕ × Payload))

Buckets 0 through 19 of the canonical genus-five classifier, storing row-key and payload associations for connected canonical leaves.

Equations

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

def AtanasovRanganathan.Generated.GenusFiveCanonicalClassifierData.payloadBucketPart1 : List (List (ℕ × Payload))

Buckets 20 through 39 of the canonical genus-five classifier, storing row-key and payload associations for connected canonical leaves.

Equations

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

def AtanasovRanganathan.Generated.GenusFiveCanonicalClassifierData.payloadBucketPart2 : List (List (ℕ × Payload))

Buckets 40 through 59 of the canonical genus-five classifier, storing row-key and payload associations for connected canonical leaves.

Equations

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

def AtanasovRanganathan.Generated.GenusFiveCanonicalClassifierData.payloadBucketPart3 : List (List (ℕ × Payload))

Buckets 60 through 79 of the canonical genus-five classifier, storing row-key and payload associations for connected canonical leaves.

Equations

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

def AtanasovRanganathan.Generated.GenusFiveCanonicalClassifierData.payloadBucketPart4 : List (List (ℕ × Payload))

Buckets 80 through 99 of the canonical genus-five classifier, storing row-key and payload associations for connected canonical leaves.

Equations

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

def AtanasovRanganathan.Generated.GenusFiveCanonicalClassifierData.payloadBucketPart5 : List (List (ℕ × Payload))

Buckets 100 through 119 of the canonical genus-five classifier, storing row-key and payload associations for connected canonical leaves.

Equations

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

def AtanasovRanganathan.Generated.GenusFiveCanonicalClassifierData.payloadBucketPart6 : List (List (ℕ × Payload))

Buckets 120 through 139 of the canonical genus-five classifier, storing row-key and payload associations for connected canonical leaves.

Equations

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

def AtanasovRanganathan.Generated.GenusFiveCanonicalClassifierData.payloadBucketPart7 : List (List (ℕ × Payload))

Buckets 140 through 159 of the canonical genus-five classifier, storing row-key and payload associations for connected canonical leaves.

Equations

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

def AtanasovRanganathan.Generated.GenusFiveCanonicalClassifierData.payloadBucketPart8 : List (List (ℕ × Payload))

Buckets 160 through 179 of the canonical genus-five classifier, storing row-key and payload associations for connected canonical leaves.

Equations

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

def AtanasovRanganathan.Generated.GenusFiveCanonicalClassifierData.payloadBucketPart9 : List (List (ℕ × Payload))

Buckets 180 through 199 of the canonical genus-five classifier, storing row-key and payload associations for connected canonical leaves.

Equations

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

def AtanasovRanganathan.Generated.GenusFiveCanonicalClassifierData.payloadBucketPart10 : List (List (ℕ × Payload))

Buckets 200 through 219 of the canonical genus-five classifier, storing row-key and payload associations for connected canonical leaves.

Equations

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

def AtanasovRanganathan.Generated.GenusFiveCanonicalClassifierData.payloadBucketPart11 : List (List (ℕ × Payload))

Buckets 220 through 239 of the canonical genus-five classifier, storing row-key and payload associations for connected canonical leaves.

Equations

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

def AtanasovRanganathan.Generated.GenusFiveCanonicalClassifierData.payloadBucketPart12 : List (List (ℕ × Payload))

Buckets 240 through 250 of the canonical genus-five classifier, storing row-key and payload associations for connected canonical leaves.

Equations

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

def AtanasovRanganathan.Generated.GenusFiveCanonicalClassifierData.payloadBuckets : List (List (ℕ × Payload))

The payload of every connected leaf the pruned traversal reaches, keyed by rowKey of that leaf and split into 251 buckets. There are 777 payloads in all; the largest bucket holds 9. Disconnected leaves are absent by design.

Equations

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

def AtanasovRanganathan.Generated.GenusFiveCanonicalClassifierData.payloadLookup (key : ℕ) : Option Payload

Look a leaf key up in its bucket.

Equations

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