The genus-five cubic classifier, without a replay tree #
This module classifies every connected loopless cubic core on eight vertices
against GenusFiveCubicAtlas.atlas, unconditionally and by kernel reduction
alone: no replay tree, no
native_decide, and no unproved hypothesis. It is the n = 8
instance of the machinery that
Certificate/GenusFourCanonicalClassifier.lean runs at n = 6.
Why the traversal is chunked #
The single decide that works at n = 6 does not work at n = 8:
the pruned traversal reaches 934 leaves, and reducing all of them
inside one kernel reduction was measured at over ten gigabytes of
resident set. So the traversal is cut two rows deep.
prunedCheck accept leaf (fuel + 1) (c :: cs) path is definitionally
a List.all over boundedCompositions c cs, which is
prunedCheck_cons below. Unfolding it twice leaves 22 independent
subgoals, the largest of them 130 leaves; those are the chunk lemmas.
The branches that unfolding exposes but canonicalPrefix rejects are
discharged wholesale by the branches lemmas, each a single cheap
decide over an explicit branch list.
Everything in this file is generated by the generated classifier data.
The emitted atlas tables are the real ones #
atlasEntry idx is generated data; these 20 lemmas are what ties it
to the actual atlas rows. The index has to be a literal, since
(atlas.get idx).n does not reduce for a symbolic idx.
The leaf decision #
The check applied to a leaf, given the result of looking its row
list up in payloadBuckets. A hit must exhibit an injective vertex
map matching the table against the indexed atlas row; a miss must
certify that the table is disconnected.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The leaf check of the pruned traversal. It receives no payload argument: the payload is fetched from the generated buckets by the leaf's own row list.
Equations
- One or more equations did not get rendered due to their size.
Instances For
One step of the traversal #
The defining equation of prunedCheck at a branching node. This
is the only thing the assembly below needs to know about it.
The chunks #
Each is the whole traversal below one canonical choice of rows 0
and 1, and each is a single kernel decide.
The branch lists #
Unfolding prunedCheck once exposes every capacity-bounded
composition, most of which canonicalPrefix rejects. Rather than
discharge those one at a time, each lemma here names the canonical
survivors of one branch list and is proved by one cheap decide.
Assembling the chunks #
The pruned traversal passes. Pure kernel reduction: no
native_decide, no generated tree, and no single reduction larger
than one chunk.
Decoding an accepted leaf #
Decoding an accepted leaf. The lookup-miss branch is discharged
against the connectedness hypothesis, and the hit branch turns the
checked injection into the required equivalence. The index must be
made concrete before the equivalence typechecks, since row.n only
reduces to 8 for a literal row.
The classifier #
Every connected loopless cubic core on eight vertices has the unordered multiplicity table of one of the twenty public atlas rows.
The multiplicity match lifts to an occurrence-sensitive public core relabeling, which is the form consumed by closed-face transport.