Documentation

LeanPool.BrillNoetherGraphs.LowGenus.GenusFiveRow11

The Atanasov--Ranganathan construction on row 11 #

Row 11 is the cube. Put one chip on the bipartition class {0, 3, 5, 6}. At a chip-free vertex of the other class, interpolate the same negative height along its three incident arms, choosing that height to be the shortest arm length. Every arm consumes at most its endpoint chip and a shortest arm delivers a chip to the centre. This is configuration 2 of Atanasov--Ranganathan, Proposition 5.1.

All four chip-free cube vertices are tripod centres, so the whole closed-orthant construction comes from ConfigTwo.closedConstruction. The calculation itself is core generic and lives in LowGenus/ConfigurationTwo.lean, over the base layer in LowGenus/ConfigurationCommon.lean (which is where the ramp and endpoint lemmas this file used to carry now live). All this file does is name the row's lookup tables and check the incidence facts.

source
def AtanasovRanganathan.GenusFiveRow11.isCenter :
Fin 8 → Bool

The chip-free bipartition class of the cube, as a decidable table. Every one of its vertices is a configuration-2 tripod centre.

Equations
Instances For
    source
    def AtanasovRanganathan.GenusFiveRow11.firstArm :
    Fin 8 → Fin 12

    The three displayed arms at each chip-free cube vertex.

    Equations
    Instances For
      source
      def AtanasovRanganathan.GenusFiveRow11.secondArm :
      Fin 8 → Fin 12

      Second tripod arm at centres 1, 2, 4, and 7, respectively slots 1, 3, 7, and 6; other inputs use zero.

      Equations
      Instances For
        source
        def AtanasovRanganathan.GenusFiveRow11.thirdArm :
        Fin 8 → Fin 12

        Third tripod arm at centres 1, 2, 4, and 7, respectively slots 9, 11, 8, and 10; other inputs use zero.

        Equations
        Instances For
          source
          def AtanasovRanganathan.GenusFiveRow11.firstChip :
          Fin 8 → Fin 8

          The chip vertex at the far end of each displayed arm.

          Equations
          Instances For
            source
            def AtanasovRanganathan.GenusFiveRow11.secondChip :
            Fin 8 → Fin 8

            Chip at the end of the second tripod arm for centres 1, 2, 4, and 7, respectively vertices 3, 0, 6, and 6.

            Equations
            Instances For
              source
              def AtanasovRanganathan.GenusFiveRow11.thirdChip :
              Fin 8 → Fin 8

              Chip at the end of the third tripod arm for centres 1, 2, 4, and 7, respectively vertices 5, 6, 0, and 3.

              Equations
              Instances For
                source
                def AtanasovRanganathan.GenusFiveRow11.spareChip :
                Fin 8 → Fin 8

                The one chip a tripod centre does not touch: the cube vertex antipodal to it.

                Equations
                Instances For
                  source
                  def AtanasovRanganathan.GenusFiveRow11.row11Config :
                  ConfigurationTwo.ConfigTwo

                  The cube read as four AR configuration-2 pictures.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    def AtanasovRanganathan.GenusFiveRow11.cubeDivisor (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) :
                    CFDiv d.graph

                    One chip on the selected bipartition class.

                    Equations
                    Instances For
                      source
                      theorem AtanasovRanganathan.GenusFiveRow11.cubeDivisor_eq_config (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) :
                      cubeDivisor d = row11Config.divisor d
                      source
                      theorem AtanasovRanganathan.GenusFiveRow11.row11_closedConstruction :
                      Configurations.ClosedSubdivisionDharConstruction GenusFiveCoreAtlas.row11Core row11_closedConstruction._proof_1

                      AR configuration 2 on the cube, valid simultaneously on the open cell and every nonloopy forest face.