Generated data for the pruned cubic classifier at n = 6

Passive data only, deliberately separated from its proof consumer. The checker recomputes the pruned traversal; this file stores only the six atlas pair-multiplicity tables and the twenty connected canonical leaf payloads.

Generated classifier data, checked by the consuming Lean declarations.

@[reducible, inline]

abbrev AtanasovRanganathan.Generated.GenusFourCanonicalClassifierData.Payload : Type

A connected canonical leaf's atlas index and matching vertex map.

Equations

• AtanasovRanganathan.Generated.GenusFourCanonicalClassifierData.Payload = (Fin 6 × (Fin 6 → Fin 6))

def AtanasovRanganathan.Generated.GenusFourCanonicalClassifierData.atlasTable : Fin 6 → Fin 6 → Fin 6 → ℕ

Pair-multiplicity tables of the six atlas rows, in atlas order.

Equations

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

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

Base-four lookup key for a leaf row list. Payloads are independently checked entry by entry, so a key collision cannot validate a bad leaf.

Equations

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

def AtanasovRanganathan.Generated.GenusFourCanonicalClassifierData.payloadTable : List (ℕ × Payload)

Payloads of all twenty connected leaves reached by the pruned traversal.

Equations

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