Documentation

LeanPool.BrillNoetherGraphs.LowGenus.GenusFiveRow12Tripod

The tripod part of the Atanasov--Ranganathan construction on row 12 #

Put one chip on each of {3, 4, 5, 6}. At either tripod center 0 or 1, 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.

The calculation itself is core generic and lives in LowGenus/ConfigurationTwo.lean. All this file does is name the row's lookup tables, check the incidence facts that file asks for, and re-export the reach statement in the shape row 12 consumes.

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

The two configuration-2 centers, as a decidable table.

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

    The three displayed arms at each tripod center.

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

      Second tripod arm, using slot 4 at centre 0 and slot 5 at centre 1; other inputs use zero.

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

        Third tripod arm, using slot 9 at centre 0 and slot 10 at centre 1; other inputs use zero.

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

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

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

            Chip at the end of the second tripod arm, vertex 3 for centre 0 and vertex 4 for centre 1.

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

              Chip at the end of the third tripod arm, vertex 5 for centre 0 and vertex 6 for centre 1.

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

                The one chip a tripod center does not touch.

                Equations
                Instances For
                  source
                  def AtanasovRanganathan.GenusFiveRow12Tripod.row12TripodConfig :
                  ConfigurationTwo.ConfigTwo

                  The two tripod centres of row 12, read as AR configuration-2 pictures.

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

                    The shape row 12 consumes #

                    source
                    def AtanasovRanganathan.GenusFiveRow12Tripod.IsTripodCenter (v : Fin 8) :
                    Prop

                    The two configuration-2 centers.

                    Equations
                    Instances For
                      source
                      @[instance_reducible]
                      instance AtanasovRanganathan.GenusFiveRow12Tripod.instDecidableIsTripodCenter (v : Fin 8) :
                      Decidable (IsTripodCenter v)
                      Equations
                      source
                      theorem AtanasovRanganathan.GenusFiveRow12Tripod.isCenter_of_isTripodCenter {v : Fin 8} (h : IsTripodCenter v) :
                      isCenter v = true
                      source
                      def AtanasovRanganathan.GenusFiveRow12Tripod.rowDivisor (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) :
                      CFDiv d.graph

                      One chip on the selected bipartition class.

                      Equations
                      Instances For
                        source
                        theorem AtanasovRanganathan.GenusFiveRow12Tripod.rowDivisor_eq_config (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) :
                        rowDivisor d = row12TripodConfig.divisor d
                        source
                        theorem AtanasovRanganathan.GenusFiveRow12Tripod.rowDivisor_reaches_tripodCenter (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (hCore : d.core = GenusFiveCoreAtlas.row12Core) (F : Finset (Fin 12)) (hRepReach : ∀ (x y : Fin 8), d.rep x = d.rep y ↔ Utilities.Certificate.ContractionForestCensusGeneral.ReachIn GenusFiveCoreAtlas.row12Core F x y) (center : Fin 8) (hCenter : IsTripodCenter center) :
                        Utilities.Certificate.StrongSeparator.Reaches d.graph (rowDivisor d) (d.coreVertex center)

                        Configuration 2 at either tripod centre of row 12.