Orbit reduction at the bare core: the generic transport

The repository certifies "only a fundamental domain of the core's automorphism group" at several different packagings of the same core data. This module states the transport once at the common denominator, which is a bare ExplicitPotential.Core n p together with a positive length vector. No row structure, no catalog metadata and no marked data enter the statement. A CoreSymmetry is an occurrence-sensitive automorphism of the ordered core: it permutes core vertices and edge slots, and may independently reverse the reading direction of each slot. Given any two positive length vectors matched along the slot permutation, such a symmetry produces a SubdivisionGraph.Spec.Relabeling, hence a LaplacianEquiv and a CFGraphIso, and therefore transports BNExists in both directions.

The declarations use the established Utilities.Certificate.CoreOrbitReduction namespace for API compatibility.

The general symmetry datum

structure Utilities.Certificate.CoreOrbitReduction.CoreSymmetry {n p : ℕ} (core : ExplicitPotential.Core n p) : Type

An occurrence-sensitive automorphism of a bare ordered core.

slotPerm acts on edge occurrences, so parallel core edges are never identified. reversed edge = true records that the image slot is read from the image of the head to the image of the tail; the two endpoint equations certify exactly that reading.

• vertexPerm : Equiv.Perm (Fin n)

  Permutation of core vertices.

• slotPerm : Equiv.Perm (Fin p)

  Permutation of edge slots (occurrences, not endpoint pairs).

• reversed : Fin p → Bool

  Per-slot orientation reversal flag.

• tail_eq (edge : Fin p) : core.tail (self.slotPerm edge) = if self.reversed edge = true then self.vertexPerm (core.head edge) else self.vertexPerm (core.tail edge)
• head_eq (edge : Fin p) : core.head (self.slotPerm edge) = if self.reversed edge = true then self.vertexPerm (core.tail edge) else self.vertexPerm (core.head edge)

def Utilities.Certificate.CoreOrbitReduction.CoreSymmetry.refl {n p : ℕ} (core : ExplicitPotential.Core n p) : CoreSymmetry core

The identity symmetry.

Equations

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

def Utilities.Certificate.CoreOrbitReduction.CoreSymmetry.ofSlotPerm {n p : ℕ} (core : ExplicitPotential.Core n p) (σ : Equiv.Perm (Fin p)) (hTail : ∀ (edge : Fin p), core.tail (σ edge) = core.tail edge) (hHead : ∀ (edge : Fin p), core.head (σ edge) = core.head edge) : CoreSymmetry core

A pure slot permutation of a core, i.e. a permutation of edge occurrences fixing every endpoint. This is the shape used by the genus-four catalog rows to sort parallel slot pairs.

Equations

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

noncomputable def Utilities.Certificate.CoreOrbitReduction.CoreSymmetry.ofMaps {n p : ℕ} (core : ExplicitPotential.Core n p) (vertexMap : Fin n → Fin n) (slotMap : Fin p → Fin p) (reversed : Fin p → Bool) (hVertex : ∀ (i j : Fin n), vertexMap i = vertexMap j → i = j) (hSlot : ∀ (i j : Fin p), slotMap i = slotMap j → i = j) (hTail : ∀ (edge : Fin p), core.tail (slotMap edge) = if reversed edge = true then vertexMap (core.head edge) else vertexMap (core.tail edge)) (hHead : ∀ (edge : Fin p), core.head (slotMap edge) = if reversed edge = true then vertexMap (core.tail edge) else vertexMap (core.head edge)) : CoreSymmetry core

The smart constructor for hand-written or generated automorphisms. Build a CoreSymmetry from raw vertex- and slot-permutation functions together with a reversal flag, checking bijectivity by injectivity (a finite endofunction is bijective iff it is injective) rather than carrying an inverse function by hand. At a concrete core all four hypotheses are by decide.

This is the public successor of the retired Certificate/CoreAutomorphismOrbit.lean's mkCoreSymmetry, which was specialized to eight-vertex, twelve-slot cores.

Equations

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

@[simp]

theorem Utilities.Certificate.CoreOrbitReduction.CoreSymmetry.ofMaps_slotPerm {n p : ℕ} (core : ExplicitPotential.Core n p) (vertexMap : Fin n → Fin n) (slotMap : Fin p → Fin p) (reversed : Fin p → Bool) (hVertex : ∀ (i j : Fin n), vertexMap i = vertexMap j → i = j) (hSlot : ∀ (i j : Fin p), slotMap i = slotMap j → i = j) (hTail : ∀ (edge : Fin p), core.tail (slotMap edge) = if reversed edge = true then vertexMap (core.head edge) else vertexMap (core.tail edge)) (hHead : ∀ (edge : Fin p), core.head (slotMap edge) = if reversed edge = true then vertexMap (core.tail edge) else vertexMap (core.head edge)) (edge : Fin p) : (ofMaps core vertexMap slotMap reversed hVertex hSlot hTail hHead).slotPerm edge = slotMap edge

@[simp]

theorem Utilities.Certificate.CoreOrbitReduction.CoreSymmetry.ofMaps_vertexPerm {n p : ℕ} (core : ExplicitPotential.Core n p) (vertexMap : Fin n → Fin n) (slotMap : Fin p → Fin p) (reversed : Fin p → Bool) (hVertex : ∀ (i j : Fin n), vertexMap i = vertexMap j → i = j) (hSlot : ∀ (i j : Fin p), slotMap i = slotMap j → i = j) (hTail : ∀ (edge : Fin p), core.tail (slotMap edge) = if reversed edge = true then vertexMap (core.head edge) else vertexMap (core.tail edge)) (hHead : ∀ (edge : Fin p), core.head (slotMap edge) = if reversed edge = true then vertexMap (core.tail edge) else vertexMap (core.head edge)) (vertex : Fin n) : (ofMaps core vertexMap slotMap reversed hVertex hSlot hTail hHead).vertexPerm vertex = vertexMap vertex

def Utilities.Certificate.CoreOrbitReduction.CoreSymmetry.ofInverses {n p : ℕ} (core : ExplicitPotential.Core n p) (vertexMap vertexInv : Fin n → Fin n) (slotMap slotInv : Fin p → Fin p) (reversed : Fin p → Bool) (hVertexLeft : ∀ (x : Fin n), vertexInv (vertexMap x) = x) (hVertexRight : ∀ (x : Fin n), vertexMap (vertexInv x) = x) (hSlotLeft : ∀ (e : Fin p), slotInv (slotMap e) = e) (hSlotRight : ∀ (e : Fin p), slotMap (slotInv e) = e) (hTail : ∀ (edge : Fin p), core.tail (slotMap edge) = if reversed edge = true then vertexMap (core.head edge) else vertexMap (core.tail edge)) (hHead : ∀ (edge : Fin p), core.head (slotMap edge) = if reversed edge = true then vertexMap (core.tail edge) else vertexMap (core.head edge)) : CoreSymmetry core

The kernel-transparent constructor.

ofMaps is the convenient one — it checks bijectivity by injectivity — but it builds its permutations with Equiv.ofBijective, and Equiv.symm of such a permutation does not reduce in the kernel. Forward application still reduces (ofMaps_vertexPerm and ofMaps_slotPerm above are both rfl), so a decide about vertexPerm cannot tell the two constructions apart. What breaks is reindexLength, which is fun edge => length (slotPerm.symm edge), and with it every consumer of it — ClosedCoreSymmetry.targetLength and the closed-orthant orbit and chamber arguments.

ofInverses takes the two inverse functions explicitly, so every projection, forward and backward, reduces. Use it whenever the symmetry will be fed to reindexLength; reindexLength_ofInverses below is the one-line regression test that the reduction is really there.

Equations

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

@[simp]

theorem Utilities.Certificate.CoreOrbitReduction.CoreSymmetry.ofInverses_vertexPerm {n p : ℕ} (core : ExplicitPotential.Core n p) (vertexMap vertexInv : Fin n → Fin n) (slotMap slotInv : Fin p → Fin p) (reversed : Fin p → Bool) (hVL : ∀ (x : Fin n), vertexInv (vertexMap x) = x) (hVR : ∀ (x : Fin n), vertexMap (vertexInv x) = x) (hSL : ∀ (e : Fin p), slotInv (slotMap e) = e) (hSR : ∀ (e : Fin p), slotMap (slotInv e) = e) (hTail : ∀ (edge : Fin p), core.tail (slotMap edge) = if reversed edge = true then vertexMap (core.head edge) else vertexMap (core.tail edge)) (hHead : ∀ (edge : Fin p), core.head (slotMap edge) = if reversed edge = true then vertexMap (core.tail edge) else vertexMap (core.head edge)) (vertex : Fin n) : (ofInverses core vertexMap vertexInv slotMap slotInv reversed hVL hVR hSL hSR hTail hHead).vertexPerm vertex = vertexMap vertex

@[simp]

theorem Utilities.Certificate.CoreOrbitReduction.CoreSymmetry.ofInverses_slotPerm {n p : ℕ} (core : ExplicitPotential.Core n p) (vertexMap vertexInv : Fin n → Fin n) (slotMap slotInv : Fin p → Fin p) (reversed : Fin p → Bool) (hVL : ∀ (x : Fin n), vertexInv (vertexMap x) = x) (hVR : ∀ (x : Fin n), vertexMap (vertexInv x) = x) (hSL : ∀ (e : Fin p), slotInv (slotMap e) = e) (hSR : ∀ (e : Fin p), slotMap (slotInv e) = e) (hTail : ∀ (edge : Fin p), core.tail (slotMap edge) = if reversed edge = true then vertexMap (core.head edge) else vertexMap (core.tail edge)) (hHead : ∀ (edge : Fin p), core.head (slotMap edge) = if reversed edge = true then vertexMap (core.tail edge) else vertexMap (core.head edge)) (edge : Fin p) : (ofInverses core vertexMap vertexInv slotMap slotInv reversed hVL hVR hSL hSR hTail hHead).slotPerm edge = slotMap edge

@[simp]

theorem Utilities.Certificate.CoreOrbitReduction.CoreSymmetry.ofInverses_slotPerm_symm {n p : ℕ} (core : ExplicitPotential.Core n p) (vertexMap vertexInv : Fin n → Fin n) (slotMap slotInv : Fin p → Fin p) (reversed : Fin p → Bool) (hVL : ∀ (x : Fin n), vertexInv (vertexMap x) = x) (hVR : ∀ (x : Fin n), vertexMap (vertexInv x) = x) (hSL : ∀ (e : Fin p), slotInv (slotMap e) = e) (hSR : ∀ (e : Fin p), slotMap (slotInv e) = e) (hTail : ∀ (edge : Fin p), core.tail (slotMap edge) = if reversed edge = true then vertexMap (core.head edge) else vertexMap (core.tail edge)) (hHead : ∀ (edge : Fin p), core.head (slotMap edge) = if reversed edge = true then vertexMap (core.tail edge) else vertexMap (core.head edge)) (edge : Fin p) : (Equiv.symm (ofInverses core vertexMap vertexInv slotMap slotInv reversed hVL hVR hSL hSR hTail hHead).slotPerm) edge = slotInv edge

def Utilities.Certificate.CoreOrbitReduction.CoreSymmetry.trans {n p : ℕ} {core : ExplicitPotential.Core n p} (first second : CoreSymmetry core) : CoreSymmetry core

The composite of two core symmetries: apply first, then second.

Equations

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

Reindexing a length vector

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

Transport a length vector along the slot permutation.

Equations

• symmetry.reindexLength length edge = length ((Equiv.symm symmetry.slotPerm) edge)

@[simp]

theorem Utilities.Certificate.CoreOrbitReduction.CoreSymmetry.reindexLength_ofInverses {n p : ℕ} (core : ExplicitPotential.Core n p) (vertexMap vertexInv : Fin n → Fin n) (slotMap slotInv : Fin p → Fin p) (reversed : Fin p → Bool) (hVL : ∀ (x : Fin n), vertexInv (vertexMap x) = x) (hVR : ∀ (x : Fin n), vertexMap (vertexInv x) = x) (hSL : ∀ (e : Fin p), slotInv (slotMap e) = e) (hSR : ∀ (e : Fin p), slotMap (slotInv e) = e) (hTail : ∀ (edge : Fin p), core.tail (slotMap edge) = if reversed edge = true then vertexMap (core.head edge) else vertexMap (core.tail edge)) (hHead : ∀ (edge : Fin p), core.head (slotMap edge) = if reversed edge = true then vertexMap (core.tail edge) else vertexMap (core.head edge)) (length : Fin p → ℕ) (edge : Fin p) : (ofInverses core vertexMap vertexInv slotMap slotInv reversed hVL hVR hSL hSR hTail hHead).reindexLength length edge = length (slotInv edge)

The regression test for the kernel-reduction hazard. For a symmetry built by ofInverses, reindexing a length vector is definitionally the composite with the supplied slot inverse — the rfl is the whole point. The same statement for ofMaps is not provable by rfl, because Equiv.ofBijective's inverse is opaque; that is the difference the two constructors exist to record.

theorem Utilities.Certificate.CoreOrbitReduction.CoreSymmetry.reindexLength_pos {n p : ℕ} {core : ExplicitPotential.Core n p} (symmetry : CoreSymmetry core) (length : Fin p → ℕ) (hLength : ∀ (edge : Fin p), 0 < length edge) (edge : Fin p) : 0 < symmetry.reindexLength length edge

@[simp]

theorem Utilities.Certificate.CoreOrbitReduction.CoreSymmetry.reindexLength_slotPerm {n p : ℕ} {core : ExplicitPotential.Core n p} (symmetry : CoreSymmetry core) (length : Fin p → ℕ) (edge : Fin p) : symmetry.reindexLength length (symmetry.slotPerm edge) = length edge

theorem Utilities.Certificate.CoreOrbitReduction.CoreSymmetry.reindexLength_compat {n p : ℕ} {core : ExplicitPotential.Core n p} (symmetry : CoreSymmetry core) (length : Fin p → ℕ) (edge : Fin p) : length edge = symmetry.reindexLength length (symmetry.slotPerm edge)

The compatibility hypothesis required by relabeling, in the canonical reindexLength case.

@[simp]

theorem Utilities.Certificate.CoreOrbitReduction.CoreSymmetry.reindexLength_refl {n p : ℕ} {core : ExplicitPotential.Core n p} (length : Fin p → ℕ) : (refl core).reindexLength length = length

theorem Utilities.Certificate.CoreOrbitReduction.CoreSymmetry.reindexLength_trans {n p : ℕ} {core : ExplicitPotential.Core n p} (first second : CoreSymmetry core) (length : Fin p → ℕ) : (first.trans second).reindexLength length = second.reindexLength (first.reindexLength length)

The general relabeling

@[reducible, inline]

abbrev Utilities.Certificate.CoreOrbitReduction.CoreSymmetry.spec {n p : ℕ} (core : ExplicitPotential.Core n p) (core_nonempty : 0 < n) (core_loopless : ∀ (edge : Fin p), core.tail edge ≠ core.head edge) (length : Fin p → ℕ) (hLength : ∀ (edge : Fin p), 0 < length edge) : SubdivisionGraph.Spec n p

The subdivision of core at a positive length vector.

Equations

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

def Utilities.Certificate.CoreOrbitReduction.CoreSymmetry.relabeling {n p : ℕ} {core : ExplicitPotential.Core n p} (core_nonempty : 0 < n) (core_loopless : ∀ (edge : Fin p), core.tail edge ≠ core.head edge) (symmetry : CoreSymmetry core) (length length' : Fin p → ℕ) (hLength : ∀ (edge : Fin p), 0 < length edge) (hLength' : ∀ (edge : Fin p), 0 < length' edge) (hCompat : ∀ (edge : Fin p), length edge = length' (symmetry.slotPerm edge)) : (spec core core_nonempty core_loopless length hLength).Relabeling (spec core core_nonempty core_loopless length' hLength')

The general transport datum. A core symmetry, together with any two positive length vectors matched along its slot permutation, is a checked slotwise relabeling from the subdivision at length to the subdivision at length'.

Stating the two length vectors independently (rather than forcing length' = reindexLength length) is what lets the same lemma serve both the row packaging, which reindexes, and the catalog rows, which sort a chosen pair of parallel slots.

Equations

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

def Utilities.Certificate.CoreOrbitReduction.CoreSymmetry.laplacianEquiv {n p : ℕ} {core : ExplicitPotential.Core n p} (core_nonempty : 0 < n) (core_loopless : ∀ (edge : Fin p), core.tail edge ≠ core.head edge) (symmetry : CoreSymmetry core) (length length' : Fin p → ℕ) (hLength : ∀ (edge : Fin p), 0 < length edge) (hLength' : ∀ (edge : Fin p), 0 < length' edge) (hCompat : ∀ (edge : Fin p), length edge = length' (symmetry.slotPerm edge)) : LaplacianEquiv (spec core core_nonempty core_loopless length hLength).graph (spec core core_nonempty core_loopless length' hLength').graph

The Laplacian equivalence carried by a core symmetry.

Equations

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

def Utilities.Certificate.CoreOrbitReduction.CoreSymmetry.graphIso {n p : ℕ} {core : ExplicitPotential.Core n p} (core_nonempty : 0 < n) (core_loopless : ∀ (edge : Fin p), core.tail edge ≠ core.head edge) (symmetry : CoreSymmetry core) (length length' : Fin p → ℕ) (hLength : ∀ (edge : Fin p), 0 < length edge) (hLength' : ∀ (edge : Fin p), 0 < length' edge) (hCompat : ∀ (edge : Fin p), length edge = length' (symmetry.slotPerm edge)) : CFGraphIso (spec core core_nonempty core_loopless length hLength).graph (spec core core_nonempty core_loopless length' hLength').graph

The graph isomorphism carried by a core symmetry.

Equations

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

def Utilities.Certificate.CoreOrbitReduction.CoreSymmetry.vertexEquiv {n p : ℕ} {core : ExplicitPotential.Core n p} (core_nonempty : 0 < n) (core_loopless : ∀ (edge : Fin p), core.tail edge ≠ core.head edge) (symmetry : CoreSymmetry core) (length length' : Fin p → ℕ) (hLength : ∀ (edge : Fin p), 0 < length edge) (hLength' : ∀ (edge : Fin p), 0 < length' edge) (hCompat : ∀ (edge : Fin p), length edge = length' (symmetry.slotPerm edge)) : (spec core core_nonempty core_loopless length hLength).Vertex ≃ (spec core core_nonempty core_loopless length' hLength').Vertex

The vertex bijection carried by a core symmetry.

Equations

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

@[simp]

theorem Utilities.Certificate.CoreOrbitReduction.CoreSymmetry.vertexEquiv_coreVertex {n p : ℕ} {core : ExplicitPotential.Core n p} (core_nonempty : 0 < n) (core_loopless : ∀ (edge : Fin p), core.tail edge ≠ core.head edge) (symmetry : CoreSymmetry core) (length length' : Fin p → ℕ) (hLength : ∀ (edge : Fin p), 0 < length edge) (hLength' : ∀ (edge : Fin p), 0 < length' edge) (hCompat : ∀ (edge : Fin p), length edge = length' (symmetry.slotPerm edge)) (vertex : Fin n) : (vertexEquiv core_nonempty core_loopless symmetry length length' hLength hLength' hCompat) ((spec core core_nonempty core_loopless length hLength).coreVertex vertex) = (spec core core_nonempty core_loopless length' hLength').coreVertex (symmetry.vertexPerm vertex)

The transport corollary

theorem Utilities.Certificate.CoreOrbitReduction.CoreSymmetry.bnExists_iff {n p : ℕ} {core : ExplicitPotential.Core n p} (core_nonempty : 0 < n) (core_loopless : ∀ (edge : Fin p), core.tail edge ≠ core.head edge) (symmetry : CoreSymmetry core) (length length' : Fin p → ℕ) (hLength : ∀ (edge : Fin p), 0 < length edge) (hLength' : ∀ (edge : Fin p), 0 < length' edge) (hCompat : ∀ (edge : Fin p), length edge = length' (symmetry.slotPerm edge)) (r d : ℤ) : BNExists (spec core core_nonempty core_loopless length' hLength').graph r d ↔ BNExists (spec core core_nonempty core_loopless length hLength).graph r d

Transport of Brill--Noether existence, in both directions. A core symmetry makes the subdivisions at two matched length vectors carry exactly the same existence statements.

theorem Utilities.Certificate.CoreOrbitReduction.CoreSymmetry.bnExists_of_bnExists {n p : ℕ} {core : ExplicitPotential.Core n p} (core_nonempty : 0 < n) (core_loopless : ∀ (edge : Fin p), core.tail edge ≠ core.head edge) (symmetry : CoreSymmetry core) (length length' : Fin p → ℕ) (hLength : ∀ (edge : Fin p), 0 < length edge) (hLength' : ∀ (edge : Fin p), 0 < length' edge) (hCompat : ∀ (edge : Fin p), length edge = length' (symmetry.slotPerm edge)) (r d : ℤ) (hBN : BNExists (spec core core_nonempty core_loopless length hLength).graph r d) : BNExists (spec core core_nonempty core_loopless length' hLength').graph r d

Forward direction of bnExists_iff, spelled out.

theorem Utilities.Certificate.CoreOrbitReduction.CoreSymmetry.bnExists_of_bnExists' {n p : ℕ} {core : ExplicitPotential.Core n p} (core_nonempty : 0 < n) (core_loopless : ∀ (edge : Fin p), core.tail edge ≠ core.head edge) (symmetry : CoreSymmetry core) (length length' : Fin p → ℕ) (hLength : ∀ (edge : Fin p), 0 < length edge) (hLength' : ∀ (edge : Fin p), 0 < length' edge) (hCompat : ∀ (edge : Fin p), length edge = length' (symmetry.slotPerm edge)) (r d : ℤ) (hBN : BNExists (spec core core_nonempty core_loopless length' hLength').graph r d) : BNExists (spec core core_nonempty core_loopless length hLength).graph r d

Backward direction of bnExists_iff, spelled out. This is the direction the catalog rows use: solve the sorted chamber, conclude at arbitrary lengths.

theorem Utilities.Certificate.CoreOrbitReduction.CoreSymmetry.bnExists_of_reindexed {n p : ℕ} {core : ExplicitPotential.Core n p} (core_nonempty : 0 < n) (core_loopless : ∀ (edge : Fin p), core.tail edge ≠ core.head edge) (symmetry : CoreSymmetry core) (length : Fin p → ℕ) (hLength : ∀ (edge : Fin p), 0 < length edge) (r d : ℤ) (hBN : BNExists (spec core core_nonempty core_loopless (symmetry.reindexLength length) ⋯).graph r d) : BNExists (spec core core_nonempty core_loopless length hLength).graph r d

The reindexing shape used by the genus-four catalog rows that sort a parallel slot pair by permuting the length vector (GenusFourCore034): solve at the reindexed lengths, conclude at the original lengths. Here the compatibility hypothesis is discharged automatically.

The genus-four slot-permutation transport, re-derived

The statement below was MarkedGraphs.Certificate.GenusFourCore066.bnExists_of_slotPerm, copied verbatim (only the name is primed); that row's cover has since been retired, and this is now the only copy. It is proved as a corollary of CoreSymmetry.bnExists_iff rather than by building a Spec.Relabeling by hand, which is the evidence that the abstraction of this file really does subsume that instance.

theorem Utilities.Certificate.CoreOrbitReduction.bnExists_of_slotPerm' {n p : ℕ} (core : ExplicitPotential.Core n p) (core_nonempty : 0 < n) (core_loopless : ∀ (edge : Fin p), core.tail edge ≠ core.head edge) (σ : Equiv.Perm (Fin p)) (hTail : ∀ (edge : Fin p), core.tail (σ edge) = core.tail edge) (hHead : ∀ (edge : Fin p), core.head (σ edge) = core.head edge) (length : Fin p → ℕ) (hLength : ∀ (edge : Fin p), 0 < length edge) (hLength' : ∀ (edge : Fin p), 0 < length (σ edge)) (hBN : BNExists (SubdivisionGraph.Spec.ofCore core core_nonempty core_loopless (fun (edge : Fin p) => length (σ edge)) hLength').graph 1 3) : BNExists (SubdivisionGraph.Spec.ofCore core core_nonempty core_loopless length hLength).graph 1 3

Existence transports along a tail- and head-preserving permutation of the edge slots of a fixed core: the subdivision at lengths length ∘ σ is isomorphic to the subdivision at length. This is the special case of SubdivisionIso with the identity vertex relabeling and no reversed slots; it is what discharges a parallel-slot ordering row.

theorem Utilities.Certificate.CoreOrbitReduction.bnExists_of_pairSort {n p : ℕ} (core : ExplicitPotential.Core n p) (core_nonempty : 0 < n) (core_loopless : ∀ (edge : Fin p), core.tail edge ≠ core.head edge) (a b : Fin p) (hTail : ∀ (edge : Fin p), core.tail ((Equiv.swap a b) edge) = core.tail edge) (hHead : ∀ (edge : Fin p), core.head ((Equiv.swap a b) edge) = core.head edge) (C : (Fin p → ℕ) → Prop) (hCswap : ∀ (length : Fin p → ℕ), C length → C fun (edge : Fin p) => length ((Equiv.swap a b) edge)) (H : ∀ (length : Fin p → ℕ) (hLength : ∀ (edge : Fin p), 0 < length edge), C length → length a ≤ length b → BNExists (SubdivisionGraph.Spec.ofCore core core_nonempty core_loopless length hLength).graph 1 3) (length : Fin p → ℕ) (hLength : ∀ (edge : Fin p), 0 < length edge) (hC : C length) : BNExists (SubdivisionGraph.Spec.ofCore core core_nonempty core_loopless length hLength).graph 1 3

One sorting step. If existence is known on the half-space L a ≤ L b under a side condition C that the transposition of the parallel slot pair {a, b} preserves, then it holds everywhere C does: an unsorted length vector is sorted by the transposition, and existence transports back along it by bnExists_of_slotPerm'.

This is what discharges the parallel-slot ordering rows a mixed cover's advertised base chamber may retain, one pair at a time, instead of by a 2 ^ (number of pairs) case split. It came from GenusFourCore066.lean, whose cover was retired on 2026-08-18 in favour of the corresponding closed-row proof module; the lemma is general and outlives that row.