Core automorphisms on closed subdivision faces

@[reducible, inline]

abbrev Utilities.Certificate.ClosedCoreSymmetry.targetLength {n p : ℕ} {core : ExplicitPotential.Core n p} (symmetry : CoreOrbitReduction.CoreSymmetry core) (length : Fin p → ℕ) : Fin p → ℕ

Slot lengths transported by the core symmetry, so a target slot reads the length of its inverse image.

Equations

• Utilities.Certificate.ClosedCoreSymmetry.targetLength symmetry length = symmetry.reindexLength length

theorem Utilities.Certificate.ClosedCoreSymmetry.adj_map {n p : ℕ} {core : ExplicitPotential.Core n p} (symmetry : CoreOrbitReduction.CoreSymmetry core) (length : Fin p → ℕ) {u v : Fin n} : ContractionForestCensusGeneral.AdjInList core (ContractionForestCensusGeneral.edgeList (ClosedFaceCensus.zeroSet length)) u v → ContractionForestCensusGeneral.AdjInList core (ContractionForestCensusGeneral.edgeList (ClosedFaceCensus.zeroSet (targetLength symmetry length))) (symmetry.vertexPerm u) (symmetry.vertexPerm v)

theorem Utilities.Certificate.ClosedCoreSymmetry.adj_map_iff {n p : ℕ} {core : ExplicitPotential.Core n p} (symmetry : CoreOrbitReduction.CoreSymmetry core) (length : Fin p → ℕ) {u v : Fin n} : ContractionForestCensusGeneral.AdjInList core (ContractionForestCensusGeneral.edgeList (ClosedFaceCensus.zeroSet (targetLength symmetry length))) (symmetry.vertexPerm u) (symmetry.vertexPerm v) ↔ ContractionForestCensusGeneral.AdjInList core (ContractionForestCensusGeneral.edgeList (ClosedFaceCensus.zeroSet length)) u v

theorem Utilities.Certificate.ClosedCoreSymmetry.reach_map_iff {n p : ℕ} {core : ExplicitPotential.Core n p} (symmetry : CoreOrbitReduction.CoreSymmetry core) (length : Fin p → ℕ) (u v : Fin n) : ContractionForestCensusGeneral.ReachIn core (ClosedFaceCensus.zeroSet (targetLength symmetry length)) (symmetry.vertexPerm u) (symmetry.vertexPerm v) ↔ ContractionForestCensusGeneral.ReachIn core (ClosedFaceCensus.zeroSet length) u v

theorem Utilities.Certificate.ClosedCoreSymmetry.rep_eq_iff {n p : ℕ} {core : ExplicitPotential.Core n p} (symmetry : CoreOrbitReduction.CoreSymmetry core) (length : Fin p → ℕ) (u v : Fin n) : ContractionForestCensusGeneral.compFold core (ClosedFaceCensus.zeroSet (targetLength symmetry length)) (symmetry.vertexPerm u) = ContractionForestCensusGeneral.compFold core (ClosedFaceCensus.zeroSet (targetLength symmetry length)) (symmetry.vertexPerm v) ↔ ContractionForestCensusGeneral.compFold core (ClosedFaceCensus.zeroSet length) u = ContractionForestCensusGeneral.compFold core (ClosedFaceCensus.zeroSet length) v

noncomputable def Utilities.Certificate.ClosedCoreSymmetry.classEquiv {n p : ℕ} {core : ExplicitPotential.Core n p} (symmetry : CoreOrbitReduction.CoreSymmetry core) (length : Fin p → ℕ) : { v : Fin n // ContractionForestCensusGeneral.compFold core (ClosedFaceCensus.zeroSet length) v = v } ≃ { v : Fin n // ContractionForestCensusGeneral.compFold core (ClosedFaceCensus.zeroSet (targetLength symmetry length)) v = v }

The core symmetry induces an equivalence of contracted vertex classes.

Equations

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

theorem Utilities.Certificate.ClosedCoreSymmetry.isForest_iff {n p : ℕ} {core : ExplicitPotential.Core n p} (symmetry : CoreOrbitReduction.CoreSymmetry core) (length : Fin p → ℕ) : ContractionForestCensusGeneral.IsForest core (ClosedFaceCensus.zeroSet (targetLength symmetry length)) ↔ ContractionForestCensusGeneral.IsForest core (ClosedFaceCensus.zeroSet length)

theorem Utilities.Certificate.ClosedCoreSymmetry.isLoopy_iff {n p : ℕ} {core : ExplicitPotential.Core n p} (symmetry : CoreOrbitReduction.CoreSymmetry core) (length : Fin p → ℕ) : ContractionForestCensusGeneral.IsLoopy core (ClosedFaceCensus.zeroSet (targetLength symmetry length)) ↔ ContractionForestCensusGeneral.IsLoopy core (ClosedFaceCensus.zeroSet length)

noncomputable def Utilities.Certificate.ClosedCoreSymmetry.relabeling {n p : ℕ} {core : ExplicitPotential.Core n p} (symmetry : CoreOrbitReduction.CoreSymmetry core) (length : Fin p → ℕ) (hn : 0 < n) (hForest : ContractionForestCensusGeneral.IsForest core (ClosedFaceCensus.zeroSet length)) (hNotLoopy : ¬ContractionForestCensusGeneral.IsLoopy core (ClosedFaceCensus.zeroSet length)) : (ClosedFaceCensus.censusSpec core hn length hForest hNotLoopy).Relabeling (ClosedFaceCensus.censusSpec core hn (targetLength symmetry length) ⋯ ⋯)

Relabel the canonical forest contraction along a core symmetry.

Equations

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

theorem Utilities.Certificate.ClosedCoreSymmetry.bnExists_iff {n p : ℕ} {core : ExplicitPotential.Core n p} (symmetry : CoreOrbitReduction.CoreSymmetry core) (length : Fin p → ℕ) (hn : 0 < n) (hForest : ContractionForestCensusGeneral.IsForest core (ClosedFaceCensus.zeroSet length)) (hNotLoopy : ¬ContractionForestCensusGeneral.IsLoopy core (ClosedFaceCensus.zeroSet length)) (rank degree : ℤ) : BNExists (ClosedFaceCensus.censusSpec core hn (targetLength symmetry length) ⋯ ⋯).graph rank degree ↔ BNExists (ClosedFaceCensus.censusSpec core hn length hForest hNotLoopy).graph rank degree