Occurrence relabeling on closed subdivision faces

An occurrence-sensitive relabeling of ordered cores transports the canonical union-find face attached to any closed length vector. Literal representatives need not commute with the vertex equivalence, so the proof works with the reachability relation generated by zero slots and then builds the induced equivalence of quotient classes.

theorem Utilities.Certificate.ExplicitPotential.Core.Relabeling.adj_map {n p : ℕ} {source target : Core n p} (r : source.Relabeling target) (length : Fin p → ℕ) {u v : Fin n} : ContractionForestCensusGeneral.AdjInList source (ContractionForestCensusGeneral.edgeList (AtanasovRanganathan.Configurations.zeroSlots length)) u v → ContractionForestCensusGeneral.AdjInList target (ContractionForestCensusGeneral.edgeList (AtanasovRanganathan.Configurations.zeroSlots (r.reindexedLength length))) (r.coreEquiv u) (r.coreEquiv v)

theorem Utilities.Certificate.ExplicitPotential.Core.Relabeling.adj_map_iff {n p : ℕ} {source target : Core n p} (r : source.Relabeling target) (length : Fin p → ℕ) {u v : Fin n} : ContractionForestCensusGeneral.AdjInList target (ContractionForestCensusGeneral.edgeList (AtanasovRanganathan.Configurations.zeroSlots (r.reindexedLength length))) (r.coreEquiv u) (r.coreEquiv v) ↔ ContractionForestCensusGeneral.AdjInList source (ContractionForestCensusGeneral.edgeList (AtanasovRanganathan.Configurations.zeroSlots length)) u v

theorem Utilities.Certificate.ExplicitPotential.Core.Relabeling.reach_map_iff {n p : ℕ} {source target : Core n p} (r : source.Relabeling target) (length : Fin p → ℕ) (u v : Fin n) : ContractionForestCensusGeneral.ReachIn target (AtanasovRanganathan.Configurations.zeroSlots (r.reindexedLength length)) (r.coreEquiv u) (r.coreEquiv v) ↔ ContractionForestCensusGeneral.ReachIn source (AtanasovRanganathan.Configurations.zeroSlots length) u v

theorem Utilities.Certificate.ExplicitPotential.Core.Relabeling.rep_eq_iff {n p : ℕ} {source target : Core n p} (r : source.Relabeling target) (length : Fin p → ℕ) (u v : Fin n) : ContractionForestCensusGeneral.compFold target (AtanasovRanganathan.Configurations.zeroSlots (r.reindexedLength length)) (r.coreEquiv u) = ContractionForestCensusGeneral.compFold target (AtanasovRanganathan.Configurations.zeroSlots (r.reindexedLength length)) (r.coreEquiv v) ↔ ContractionForestCensusGeneral.compFold source (AtanasovRanganathan.Configurations.zeroSlots length) u = ContractionForestCensusGeneral.compFold source (AtanasovRanganathan.Configurations.zeroSlots length) v

noncomputable def Utilities.Certificate.ExplicitPotential.Core.Relabeling.classEquiv {n p : ℕ} {source target : Core n p} (r : source.Relabeling target) (length : Fin p → ℕ) : { v : Fin n // ContractionForestCensusGeneral.compFold source (AtanasovRanganathan.Configurations.zeroSlots length) v = v } ≃ { v : Fin n // ContractionForestCensusGeneral.compFold target (AtanasovRanganathan.Configurations.zeroSlots (r.reindexedLength length)) v = v }

Relabeling transports canonical representatives of zero-edge connected components.

Equations

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

theorem Utilities.Certificate.ExplicitPotential.Core.Relabeling.isForest_iff {n p : ℕ} {source target : Core n p} (r : source.Relabeling target) (length : Fin p → ℕ) : ContractionForestCensusGeneral.IsForest target (AtanasovRanganathan.Configurations.zeroSlots (r.reindexedLength length)) ↔ ContractionForestCensusGeneral.IsForest source (AtanasovRanganathan.Configurations.zeroSlots length)

theorem Utilities.Certificate.ExplicitPotential.Core.Relabeling.isLoopy_iff {n p : ℕ} {source target : Core n p} (r : source.Relabeling target) (length : Fin p → ℕ) : ContractionForestCensusGeneral.IsLoopy target (AtanasovRanganathan.Configurations.zeroSlots (r.reindexedLength length)) ↔ ContractionForestCensusGeneral.IsLoopy source (AtanasovRanganathan.Configurations.zeroSlots length)

noncomputable def Utilities.Certificate.ExplicitPotential.Core.Relabeling.faceClassEquiv {n p : ℕ} {source target : Core n p} (r : source.Relabeling target) (length : Fin p → ℕ) (source_nonempty : 0 < n) (hForest : ContractionForestCensusGeneral.IsForest source (AtanasovRanganathan.Configurations.zeroSlots length)) (hNotLoopy : ¬ContractionForestCensusGeneral.IsLoopy source (AtanasovRanganathan.Configurations.zeroSlots length)) : (AtanasovRanganathan.Configurations.faceSpec source source_nonempty length hForest hNotLoopy).Class ≃ (AtanasovRanganathan.Configurations.faceSpec target source_nonempty (r.reindexedLength length) ⋯ ⋯).Class

The induced equivalence of contracted vertex classes in the corresponding closed faces.

Equations

• r.faceClassEquiv length source_nonempty hForest hNotLoopy = r.classEquiv length

noncomputable def Utilities.Certificate.ExplicitPotential.Core.Relabeling.faceRelabeling {n p : ℕ} {source target : Core n p} (r : source.Relabeling target) (length : Fin p → ℕ) (source_nonempty : 0 < n) (hForest : ContractionForestCensusGeneral.IsForest source (AtanasovRanganathan.Configurations.zeroSlots length)) (hNotLoopy : ¬ContractionForestCensusGeneral.IsLoopy source (AtanasovRanganathan.Configurations.zeroSlots length)) : (AtanasovRanganathan.Configurations.faceSpec source source_nonempty length hForest hNotLoopy).Relabeling (AtanasovRanganathan.Configurations.faceSpec target source_nonempty (r.reindexedLength length) ⋯ ⋯)

The closed faces attached to occurrence-relabelled cores are themselves occurrence-relabelled.

Equations

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

theorem Utilities.Certificate.ExplicitPotential.Core.Relabeling.closedPencil_of_target {n p : ℕ} {source target : Core n p} (relabeling : source.Relabeling target) (source_nonempty : 0 < n) {r degree : ℤ} (targetClosed : ∀ (targetLength : Fin p → ℕ) (targetForest : ContractionForestCensusGeneral.IsForest target (AtanasovRanganathan.Configurations.zeroSlots targetLength)) (targetNotLoopy : ¬ContractionForestCensusGeneral.IsLoopy target (AtanasovRanganathan.Configurations.zeroSlots targetLength)), BNExists (AtanasovRanganathan.Configurations.faceSpec target source_nonempty targetLength targetForest targetNotLoopy).graph r degree) (sourceLength : Fin p → ℕ) (sourceForest : ContractionForestCensusGeneral.IsForest source (AtanasovRanganathan.Configurations.zeroSlots sourceLength)) (sourceNotLoopy : ¬ContractionForestCensusGeneral.IsLoopy source (AtanasovRanganathan.Configurations.zeroSlots sourceLength)) : BNExists (AtanasovRanganathan.Configurations.faceSpec source source_nonempty sourceLength sourceForest sourceNotLoopy).graph r degree

A closed-orthant Brill--Noether existence theorem transports backward along an occurrence-sensitive core relabeling, at arbitrary rank and degree.

theorem Utilities.Certificate.ExplicitPotential.Core.Relabeling.closedConstruction_of_target {n p : ℕ} {source target : Core n p} (relabeling : source.Relabeling target) (source_nonempty : 0 < n) : AtanasovRanganathan.Configurations.ClosedSubdivisionDharConstruction target source_nonempty → AtanasovRanganathan.Configurations.ClosedSubdivisionDharConstruction source source_nonempty

A closed construction transports backward along an occurrence-sensitive core relabeling.