Documentation

LeanPool.BrillNoetherGraphs.LowGenus.Infrastructure.TrivalentExpansionClosed

The closed centipede face #

Contracting the internal edges of the centipede expansion recovers the original subdivision. This file expresses that observation in the closed orthant language consumed by the Atanasov--Ranganathan row constructions.

source
@[reducible, inline]
abbrev Utilities.Subdivision.TrivalentExpansion.expandedVertexCount {n p : ℕ} :
ℕ

Number of vertices in the trivalent centipede expansion.

Equations
Instances For
    source
    @[reducible, inline]
    abbrev Utilities.Subdivision.TrivalentExpansion.expandedSlotCount {n p : ℕ} :
    ℕ

    Number of edge slots in the trivalent centipede expansion.

    Equations
    Instances For
      source
      noncomputable def Utilities.Subdivision.TrivalentExpansion.firstVertex {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) (w : Fin n) :
      Fin expandedVertexCount

      The distinguished first vertex of each centipede fibre.

      Equations
      Instances For
        source
        @[simp]
        theorem Utilities.Subdivision.TrivalentExpansion.data_fib_firstVertex {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) (w : Fin n) :
        (data C hDeg).fib (firstVertex C hDeg w) = w
        source
        theorem Utilities.Subdivision.TrivalentExpansion.firstVertex_injective {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) :
        Function.Injective (firstVertex C hDeg)
        source
        noncomputable def Utilities.Subdivision.TrivalentExpansion.firstRep {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) (v : Fin expandedVertexCount) :
        Fin expandedVertexCount

        The retraction choosing the first vertex in each centipede fibre.

        Equations
        Instances For
          source
          @[simp]
          theorem Utilities.Subdivision.TrivalentExpansion.firstRep_firstVertex {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) (w : Fin n) :
          firstRep C hDeg (firstVertex C hDeg w) = firstVertex C hDeg w
          source
          theorem Utilities.Subdivision.TrivalentExpansion.firstRep_idem {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) (v : Fin expandedVertexCount) :
          firstRep C hDeg (firstRep C hDeg v) = firstRep C hDeg v
          source
          theorem Utilities.Subdivision.TrivalentExpansion.firstRep_eq_iff_fib_eq {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) (a b : Fin expandedVertexCount) :
          firstRep C hDeg a = firstRep C hDeg b ↔ (data C hDeg).fib a = (data C hDeg).fib b
          source
          theorem Utilities.Subdivision.TrivalentExpansion.card_image_firstRep {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) :
          (Finset.image (firstRep C hDeg) Finset.univ).card = n
          source
          noncomputable def Utilities.Subdivision.TrivalentExpansion.closedLength {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) (small : Certificate.SubdivisionGraph.Spec n p) (e : Fin expandedSlotCount) :
          ℕ

          The closed length vector: centipede edges vanish and carrier slots retain the lengths of the original subdivision.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem Utilities.Subdivision.TrivalentExpansion.closedLength_internal {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) (x : (w : Fin n) × Fin (Certificate.PseudocorePresentation.slotValence C w - 3)) (small : Certificate.SubdivisionGraph.Spec n p) :
            closedLength C hDeg small ((eEquiv C hDeg) (Sum.inl x)) = 0
            source
            @[simp]
            theorem Utilities.Subdivision.TrivalentExpansion.closedLength_carrier {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) (j : Fin p) (small : Certificate.SubdivisionGraph.Spec n p) :
            closedLength C hDeg small ((eEquiv C hDeg) (Sum.inr j)) = small.length j
            source
            theorem Utilities.Subdivision.TrivalentExpansion.zeroSlots_closedLength {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) (small : Certificate.SubdivisionGraph.Spec n p) :
            AtanasovRanganathan.Configurations.zeroSlots (closedLength C hDeg small) = (data C hDeg).contractedSlots
            source
            theorem Utilities.Subdivision.TrivalentExpansion.card_contractedSlots {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) :
            (data C hDeg).contractedSlots.card = expandedVertexCount - n
            source
            theorem Utilities.Subdivision.TrivalentExpansion.card_image_compFold_contracted {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) (hLoop : ∀ (e : Fin p), C.tail e ≠ C.head e) :
            (Finset.image (Certificate.ContractionForestCensusGeneral.compFold (data C hDeg).bigCore (data C hDeg).contractedSlots) Finset.univ).card = n
            source
            theorem Utilities.Subdivision.TrivalentExpansion.closedLength_isForest {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) (hLoop : ∀ (e : Fin p), C.tail e ≠ C.head e) (small : Certificate.SubdivisionGraph.Spec n p) :
            Certificate.ContractionForestCensusGeneral.IsForest (data C hDeg).bigCore (AtanasovRanganathan.Configurations.zeroSlots (closedLength C hDeg small))
            source
            theorem Utilities.Subdivision.TrivalentExpansion.closedLength_not_isLoopy {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) (hLoop : ∀ (e : Fin p), C.tail e ≠ C.head e) (small : Certificate.SubdivisionGraph.Spec n p) :
            ¬Certificate.ContractionForestCensusGeneral.IsLoopy (data C hDeg).bigCore (AtanasovRanganathan.Configurations.zeroSlots (closedLength C hDeg small))
            source
            noncomputable def Utilities.Subdivision.TrivalentExpansion.closedFace {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) (small : Certificate.SubdivisionGraph.Spec n p) (hLoop : ∀ (e : Fin p), C.tail e ≠ C.head e) :
            Certificate.DegenerateSpec.DegSpec expandedVertexCount expandedSlotCount

            The canonical closed face of the centipede expansion.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[simp]
              theorem Utilities.Subdivision.TrivalentExpansion.closedFace_core {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) (small : Certificate.SubdivisionGraph.Spec n p) (hLoop : ∀ (e : Fin p), C.tail e ≠ C.head e) :
              (closedFace C hDeg small hLoop).core = (data C hDeg).bigCore
              source
              @[simp]
              theorem Utilities.Subdivision.TrivalentExpansion.closedFace_length {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) (small : Certificate.SubdivisionGraph.Spec n p) (hLoop : ∀ (e : Fin p), C.tail e ≠ C.head e) :
              (closedFace C hDeg small hLoop).length = closedLength C hDeg small
              source
              theorem Utilities.Subdivision.TrivalentExpansion.closedFace_rep {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) (small : Certificate.SubdivisionGraph.Spec n p) (hLoop : ∀ (e : Fin p), C.tail e ≠ C.head e) (v : Fin expandedVertexCount) :
              (closedFace C hDeg small hLoop).rep v = Certificate.ContractionForestCensusGeneral.compFold (data C hDeg).bigCore (data C hDeg).contractedSlots v
              source
              noncomputable def Utilities.Subdivision.TrivalentExpansion.closedContraction {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) (small : Certificate.SubdivisionGraph.Spec n p) (hCore : small.core = C) (hLoop : ∀ (e : Fin p), C.tail e ≠ C.head e) :
              (closedFace C hDeg small hLoop).Contraction small

              The contracted closed face is the original positive subdivision.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                noncomputable def Utilities.Subdivision.TrivalentExpansion.closedFaceEquiv {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) (small : Certificate.SubdivisionGraph.Spec n p) (hCore : small.core = C) (hLoop : ∀ (e : Fin p), C.tail e ≠ C.head e) :
                Certificate.LaplacianEquiv small.graph (closedFace C hDeg small hLoop).graph

                Laplacian equivalence between the canonical closed centipede face and the subdivision it collapses onto.

                Equations
                Instances For
                  source
                  theorem Utilities.Subdivision.TrivalentExpansion.bnExists_of_closedPencil {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) (small : Certificate.SubdivisionGraph.Spec n p) (hCore : small.core = C) (hLoop : ∀ (e : Fin p), C.tail e ≠ C.head e) {r degree : ℤ} (closed : ∀ (length : Fin expandedSlotCount → ℕ) (hForest : Certificate.ContractionForestCensusGeneral.IsForest (data C hDeg).bigCore (AtanasovRanganathan.Configurations.zeroSlots length)) (hNotLoopy : ¬Certificate.ContractionForestCensusGeneral.IsLoopy (data C hDeg).bigCore (AtanasovRanganathan.Configurations.zeroSlots length)), BNExists (AtanasovRanganathan.Configurations.faceSpec (data C hDeg).bigCore ⋯ length hForest hNotLoopy).graph r degree) :
                  BNExists small.graph r degree

                  A closed-orthant Brill--Noether existence theorem on the cubic centipede expansion descends to the original positive subdivision, at arbitrary rank and degree.

                  source
                  theorem Utilities.Subdivision.TrivalentExpansion.bnExists_of_closedConstruction {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) (small : Certificate.SubdivisionGraph.Spec n p) (hCore : small.core = C) (hLoop : ∀ (e : Fin p), C.tail e ≠ C.head e) (construction : AtanasovRanganathan.Configurations.ClosedSubdivisionDharConstruction (data C hDeg).bigCore ⋯) :
                  BNExists small.graph 1 4

                  A closed construction on the cubic centipede expansion supplies a degree-four pencil on the original subdivision.