Core automorphisms on the closed row-proof orthant

CoreOrbitReduction transports positive subdivisions. An RPF AUTO node also acts on boundary faces, where zero slots have identified core vertices. This file supplies that missing closed-face transport. The proof deliberately uses reachability, rather than the literal output of compFold: canonical union-find representatives need not commute definitionally with a vertex permutation, but their fibres do.

Fail-closed raw automorphism data

PTree is not indexed by a core, so an auto node stores lists. The checker decodes them only after verifying two-sided inverses and the endpoint laws. The inverse lists are emitted mechanically from the row's permutations.

structure Utilities.Subdivision.ClosedRowProof.ClosedAuto.AutoData : Type

Raw vertex and slot permutation data checked before use as a graph automorphism.

• vertex : List ℕ

  Proposed images of core vertices, decoded modulo the number of vertices.

• vertexInv : List ℕ

  Proposed inverse images of core vertices; the checker verifies both inverse identities after decoding.

• slot : List ℕ

  Proposed images of slot occurrences, decoded modulo the number of slots.

• slotInv : List ℕ

  Proposed inverse images of slot occurrences; the checker verifies both inverse identities after decoding.

• reversed : List Bool

  Orientation-reversal flags indexed by source slot, with missing flags interpreted as false.

def Utilities.Subdivision.ClosedRowProof.ClosedAuto.AutoData.vertexMap {n : ℕ} (d : AutoData) (hn : 0 < n) (v : Fin n) : Fin n

Decode a proposed vertex image using zero for missing entries and reduction modulo the nonzero vertex count.

Equations

• d.vertexMap hn v = ⟨d.vertex.getD (↑v) 0 % n, ⋯⟩

def Utilities.Subdivision.ClosedRowProof.ClosedAuto.AutoData.vertexInvMap {n : ℕ} (d : AutoData) (hn : 0 < n) (v : Fin n) : Fin n

Decode a proposed inverse vertex image using zero for missing entries and reduction modulo the nonzero vertex count.

Equations

• d.vertexInvMap hn v = ⟨d.vertexInv.getD (↑v) 0 % n, ⋯⟩

def Utilities.Subdivision.ClosedRowProof.ClosedAuto.AutoData.slotMap {p : ℕ} (d : AutoData) (hp : 0 < p) (e : Fin p) : Fin p

Decode a proposed slot image using zero for missing entries and reduction modulo the nonzero slot count.

Equations

• d.slotMap hp e = ⟨d.slot.getD (↑e) 0 % p, ⋯⟩

def Utilities.Subdivision.ClosedRowProof.ClosedAuto.AutoData.slotInvMap {p : ℕ} (d : AutoData) (hp : 0 < p) (e : Fin p) : Fin p

Decode a proposed inverse slot image using zero for missing entries and reduction modulo the nonzero slot count.

Equations

• d.slotInvMap hp e = ⟨d.slotInv.getD (↑e) 0 % p, ⋯⟩

def Utilities.Subdivision.ClosedRowProof.ClosedAuto.AutoData.reverseAt {p : ℕ} (d : AutoData) (e : Fin p) : Bool

Read the reversal flag of a source slot, defaulting to false when the list has no entry.

Equations

• d.reverseAt e = d.reversed.getD (↑e) false

def Utilities.Subdivision.ClosedRowProof.ClosedAuto.AutoData.checks {n p : ℕ} (d : AutoData) (core : Certificate.ExplicitPotential.Core n p) : Bool

Check nonempty vertex and slot sets, both inverse identities, and the two endpoint laws for the decoded automorphism data.

Equations

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

def Utilities.Subdivision.ClosedRowProof.ClosedAuto.AutoData.toSymmetry {n p : ℕ} (d : AutoData) (core : Certificate.ExplicitPotential.Core n p) (hn : 0 < n) (hp : 0 < p) (hcheck : d.checks core = true) : Certificate.CoreOrbitReduction.CoreSymmetry core

Construct a core symmetry from decoded vertex and slot permutations after their inverse and endpoint checks succeed.

Equations

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

def Utilities.Subdivision.ClosedRowProof.ClosedAuto.AutoData.pullbackForm {p : ℕ} (d : AutoData) (hp : 0 < p) (g : Form) : Form

Pull a form back exactly as rpfcheck: the old coefficient at e moves to slotMap e, equivalently the new coefficient at j is read at slotInvMap j. RPF row proofs have exactly p coordinates.

Equations

• d.pullbackForm hp g = List.getD g 0 0 :: List.ofFn fun (e : Fin p) => List.getD g (↑(d.slotInvMap hp e)).succ 0

def Utilities.Subdivision.ClosedRowProof.ClosedAuto.AutoData.pullbackContext {p : ℕ} (d : AutoData) (hp : 0 < p) (Γ : Context) : Context

Pull back every inequality and equality form in the context through the decoded inverse slot map.

Equations

• d.pullbackContext hp Γ = { ge := List.map (d.pullbackForm hp) Γ.ge, eq := List.map (d.pullbackForm hp) Γ.eq }

theorem Utilities.Subdivision.ClosedRowProof.ClosedAuto.AutoData.eval_pullbackForm {n p : ℕ} (d : AutoData) (core : Certificate.ExplicitPotential.Core n p) (hn : 0 < n) (hp : 0 < p) (hcheck : d.checks core = true) (g : Form) (point : Fin p → ℤ) : eval (d.pullbackForm hp g) (List.ofFn fun (e : Fin p) => point ((Equiv.symm (d.toSymmetry core hn hp hcheck).slotPerm) e)) = eval g (List.ofFn point)

theorem Utilities.Subdivision.ClosedRowProof.ClosedAuto.AutoData.pullbackContext_holds {n p : ℕ} (d : AutoData) (core : Certificate.ExplicitPotential.Core n p) (hn : 0 < n) (hp : 0 < p) (hcheck : d.checks core = true) {Γ : Context} {point : Fin p → ℤ} (hΓ : Γ.Holds (List.ofFn point)) : (d.pullbackContext hp Γ).Holds (List.ofFn fun (e : Fin p) => point ((Equiv.symm (d.toSymmetry core hn hp hcheck).slotPerm) e))

@[reducible, inline]

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

The symmetry-reindexed length vector used to transport the zero-slot contraction and its surviving subdivision.

Equations

• Utilities.Subdivision.ClosedRowProof.ClosedAuto.targetLength symmetry length = symmetry.reindexLength length

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

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

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

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

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

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

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