Documentation

LeanPool.BrillNoetherGraphs.LowGenus.GenusFiveRow16

The Atanasov--Ranganathan construction on row 16 #

Put one chip on each of 3,4,5,6. The chip-free core vertices form the two edges 0--1 and 2--7; together with their four incident chip vertices, each is configuration 3 of Atanasov--Ranganathan, Proposition 5.1.

The calculation itself is core generic and lives in LowGenus/ConfigurationThree.lean. All this file does is name the row's lookup tables and check the incidence facts that file asks for.

source
def AtanasovRanganathan.GenusFiveRow16.partner :
Fin 8 → Fin 8

The other chip-free centre in the same configuration-3 component.

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

    The first arm from each chip-free centre to a chip vertex.

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

      The second arm from each chip-free centre to a chip vertex.

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

        The chip at the far end of the first arm.

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

          The chip at the far end of the second arm.

          Equations
          Instances For
            source
            def AtanasovRanganathan.GenusFiveRow16.middleEdge :
            Fin 8 → Fin 12

            The edge joining the two chip-free centres.

            Equations
            Instances For
              source
              def AtanasovRanganathan.GenusFiveRow16.isCenter :
              Fin 8 → Bool

              The chip-free core vertices, as a decidable table.

              Equations
              Instances For
                source
                def AtanasovRanganathan.GenusFiveRow16.row16Config :
                ConfigurationThree.ConfigThree 8 12

                Row 16 read as a pair of AR configuration-3 pictures.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  theorem AtanasovRanganathan.GenusFiveRow16.row16_closedConstruction :
                  Configurations.ClosedSubdivisionDharConstruction GenusFiveCoreAtlas.row16Core row16_closedConstruction._proof_1

                  AR configuration 3 on row 16, valid simultaneously on the open cell and every nonloopy forest face.