Documentation

LeanPool.BrillNoetherGraphs.LowGenus.GenusFourCanonicalClassifier

The public genus-four cubic classifier #

Every connected loopless cubic core on six vertices is relabeled to one of the six rows in GenusFourCubicAtlas.atlas. The proof uses the generic canonical-matrix traversal and a small generated payload table, but no replay tree, native_decide, private import, or unproved hypothesis.

The emitted atlas tables are the public rows #

source
theorem AtanasovRanganathan.GenusFourCanonicalClassifier.atlasTable_row095 (a b : Fin 6) :
Generated.GenusFourCanonicalClassifierData.atlasTable 0 a b = GenusFourCubicAtlas.row095.core.pairMultiplicity a b
source
theorem AtanasovRanganathan.GenusFourCanonicalClassifier.atlasTable_row096 (a b : Fin 6) :
Generated.GenusFourCanonicalClassifierData.atlasTable 1 a b = GenusFourCubicAtlas.row096.core.pairMultiplicity a b
source
theorem AtanasovRanganathan.GenusFourCanonicalClassifier.atlasTable_row097 (a b : Fin 6) :
Generated.GenusFourCanonicalClassifierData.atlasTable 2 a b = GenusFourCubicAtlas.row097.core.pairMultiplicity a b
source
theorem AtanasovRanganathan.GenusFourCanonicalClassifier.atlasTable_row098 (a b : Fin 6) :
Generated.GenusFourCanonicalClassifierData.atlasTable 3 a b = GenusFourCubicAtlas.row098.core.pairMultiplicity a b
source
theorem AtanasovRanganathan.GenusFourCanonicalClassifier.atlasTable_row099 (a b : Fin 6) :
Generated.GenusFourCanonicalClassifierData.atlasTable 4 a b = GenusFourCubicAtlas.row099.core.pairMultiplicity a b
source
theorem AtanasovRanganathan.GenusFourCanonicalClassifier.atlasTable_row100 (a b : Fin 6) :
Generated.GenusFourCanonicalClassifierData.atlasTable 5 a b = GenusFourCubicAtlas.row100.core.pairMultiplicity a b

Leaf checking and decoding #

source
def AtanasovRanganathan.GenusFourCanonicalClassifier.payloadDecide (rows : List (List ℕ)) :
Option Generated.GenusFourCanonicalClassifierData.Payload → Bool

Decide a payload hit by checking injectivity and all table entries; a miss is accepted only when the leaf matrix is disconnected.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def AtanasovRanganathan.GenusFourCanonicalClassifier.leafDecide (rows : List (List ℕ)) :
    Bool

    Look up and check the payload belonging to a leaf's own row list.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem AtanasovRanganathan.GenusFourCanonicalClassifier.pruned_valid :
      Utilities.Certificate.CubicMatrixReplay.prunedCheck Utilities.Certificate.CubicMatrixReplay.canonicalPrefix leafDecide 7 (List.replicate 6 3) [] = true

      The entire pruned six-vertex traversal passes by kernel reduction.

      source
      theorem AtanasovRanganathan.GenusFourCanonicalClassifier.decode (rows : List (List ℕ)) (hLeaf : leafDecide rows = true) (hConnected : Utilities.Certificate.CubicMatrixReplay.MatrixConnected 6 (Utilities.Certificate.CubicMatrixReplay.entryOf rows)) :
      ∃ row ∈ GenusFourCubicAtlas.atlas, ∃ (vertexEquiv : Fin 6 ≃ Fin 6), ∀ (i j : Fin 6), Utilities.Certificate.CubicMatrixReplay.entryOf rows ↑i ↑j = row.core.pairMultiplicity (vertexEquiv i) (vertexEquiv j)

      Decode an accepted connected leaf to one of the six public atlas rows.

      Public completeness theorems #

      source
      theorem AtanasovRanganathan.GenusFourCanonicalClassifier.genusFourCubicPairMultiplicityComplete (candidate : Utilities.Certificate.ExplicitPotential.Core 6 9) (hConnected : candidate.Connected) (hLoopless : ∀ (edge : Fin 9), candidate.tail edge ≠ candidate.head edge) (hCubic : candidate.Cubic) :
      ∃ row ∈ GenusFourCubicAtlas.atlas, ∃ (vertexEquiv : Fin 6 ≃ Fin 6), ∀ (i j : Fin 6), candidate.pairMultiplicity i j = row.core.pairMultiplicity (vertexEquiv i) (vertexEquiv j)

      Every connected loopless cubic core on six vertices has the unordered multiplicity table of one of the six public atlas rows.

      source
      theorem AtanasovRanganathan.GenusFourCanonicalClassifier.genusFourCubicRelabelingComplete (candidate : Utilities.Certificate.ExplicitPotential.Core 6 9) (hConnected : candidate.Connected) (hLoopless : ∀ (edge : Fin 9), candidate.tail edge ≠ candidate.head edge) (hCubic : candidate.Cubic) :
      ∃ row ∈ GenusFourCubicAtlas.atlas, Nonempty (candidate.Relabeling row.core)

      The multiplicity match lifts to an occurrence-sensitive core relabeling, the form used by closed-face transport.