Documentation

LeanPool.BrillNoetherGraphs.LowGenus.GenusFiveRow12

The Atanasov--Ranganathan construction on row 12 #

Put one chip on each of 3,4,5,6. The remaining vertices 0 and 1 are centres of configuration-2 tripods, while 2--7 and its four incident arms form configuration 3 of Atanasov--Ranganathan, Proposition 5.1.

Both local pictures are core generic and live in LowGenus/ConfigurationTwo.lean and LowGenus/ConfigurationThree.lean. Because each of those structures names its centres by an explicit isCenter table rather than "every chip-free vertex", row 12 can declare {0,1} to be tripod centres and {2,7} to be a configuration-3 pair, and this file only has to name the row's lookup tables, check the incidence facts, and observe that the two tables between them cover every chip-free vertex.

The row-12 configuration-3 lookup tables #

source
def AtanasovRanganathan.GenusFiveRow12.isPairCenter :
Fin 8 → Bool

The two centres belonging to the configuration-3 component.

Equations
Instances For
    source
    def AtanasovRanganathan.GenusFiveRow12.partner :
    Fin 8 → Fin 8

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

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

      The two arms from a pair centre to chip vertices.

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

        Second arm of the row-12 configuration, using slot 2 at centre 2 and slot 8 at centre 7, with zero as the unused default.

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

          The chip at the far end of the first arm.

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

            The chip at the far end of the second arm.

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

              The edge joining the two chip-free centres.

              Equations
              Instances For
                source
                def AtanasovRanganathan.GenusFiveRow12.row12PairConfig :
                ConfigurationThree.ConfigThree 8 12

                The pair 2--7 of row 12, read as an AR configuration-3 picture.

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

                  Combining the two local pictures #

                  The row's closing step lives in GenusFiveRow12Guarding, which feeds centers_cover straight into a Guarding.GuardingSet and lets GuardingSet.closedConstruction do the rest. The hand-written composition that used to stand here -- a rowDivisor, two rfl bridges to the two configuration divisors, a chip/centre dispatch, and a call to ofReachesCoreClasses -- was exactly the generic argument, and is retired.

                  source
                  theorem AtanasovRanganathan.GenusFiveRow12.centers_cover (v : Fin 8) :
                  ¬row12PairConfig.IsChip v → isPairCenter v = true ∨ GenusFiveRow12Tripod.isCenter v = true

                  The two isCenter tables between them name every chip-free vertex.