Core automorphisms on the closed genus-five orthant #
CoreSymmetry transports positive subdivisions of a fixed ordered core.
The Atanasov--Ranganathan row obligation ClosedSubdivisionDharConstruction
is stated on the whole closed orthant, where zero slots have already
identified core vertices, so a row proof needs the closed-face counterpart:
a core automorphism must also act on the canonical forest contraction
faceSpec.
That is what this module supplies. The proofs deliberately use reachability
rather than the literal output of compFold: canonical union-find
representatives need not commute definitionally with a vertex permutation,
but their fibres do. Everything below is the public restatement, at
faceSpec, of the shared transport Utilities.Certificate.ClosedCoreSymmetry.
The payoff for a row author is closedConstruction_of_chamber: prove the row
on any chamber P of length space, exhibit for each nonloopy forest face one
symmetry moving it into P, and the whole closed orthant follows. Neither
the forest hypothesis nor the looplessness hypothesis has to be re-proved at
the moved face -- isForest_iff and isLoopy_iff transport them.
The length vector obtained by moving length along the symmetry's slot
permutation. A row proof works at targetLength and concludes at
length.
Equations
- AtanasovRanganathan.ClosedOrbit.targetLength symmetry length = symmetry.reindexLength length
Instances For
The zero set moves along the slot permutation #
Adjacency and reachability in the contracted core #
The fibre statement. Canonical union-find representatives do not
commute definitionally with a vertex permutation, but their fibres do: two
core vertices are identified at length exactly when their images are
identified at targetLength.
The induced bijection of contracted classes. It is built from the fibre
statement by Equiv.ofBijective, never by claiming that compFold commutes
with vertexPerm.
Equations
- AtanasovRanganathan.ClosedOrbit.classEquiv symmetry length = Utilities.Certificate.ClosedCoreSymmetry.classEquiv symmetry length
Instances For
The two face hypotheses transport #
Genus preservation is a symmetry-invariant property of a face.
Surviving loops are a symmetry-invariant property of a face.
The transported forest hypothesis.
The transported looplessness hypothesis.
Existence transports across the closed face #
The closed-face relabeling induced by a core symmetry.
bnExists_iff used to build this datum inline. Naming it is what lets a
per-vertex statement — StrongSeparator.Reaches at one contracted core
class — be transported as well as a whole-graph one; see
AtanasovRanganathan.Guarding.faceGuard_map. The shared closed-core transport
supplies the relabeling and its vertex action.
Equations
- AtanasovRanganathan.ClosedOrbit.relabeling symmetry length core_nonempty forest not_loopy = Utilities.Certificate.ClosedCoreSymmetry.relabeling symmetry length core_nonempty forest not_loopy
Instances For
The relabeling sends a contracted core class to the class of its image under the symmetry's vertex permutation.
The closed-face transport. The canonical forest contraction at
targetLength and the one at length carry exactly the same Brill--Noether
existence statements.
The AR pencil form of the transport: a pencil at the moved face gives a pencil at the original face.
The row-authoring interface #
The consumer corollary. A row is closed on the whole nonloopy forest orthant as soon as
chamber: it is proved on some chamberPof length space, andcovers: every nonloopy forest face is carried intoPby some core symmetry.
Both face hypotheses at the moved length vector are supplied by this lemma,
so chamber may assume them freely; and covers may pick a different
symmetry for each face, typically by by_cases on the chamber inequalities
with CoreSymmetry.refl and CoreSymmetry.trans composites as the
witnesses.
The same statement with the symmetries supplied as an explicit list, the shape generated orbit tables use.
Smoke test: a nontrivial symmetry of the row-11 cube core #
row11Core is the three-cube Q₃ (outer square 0,1,3,2, inner square
4,5,7,6, four rungs). The antipodal map exchanging the two squares is a
core automorphism reversing exactly the four rung slots; both endpoint laws
are kernel-checked. This is the shape a row author writes.
The antipodal automorphism of the cube row11Core: v ↦ v + 4. It
exchanges the two squares slotwise and reverses the four rungs.
Equations
- One or more equations did not get rendered due to their size.