The common closing step of an Atanasov--Ranganathan closed-face row #
Every completed genus-five row ends with the same four moves: the displayed
degree-four divisor reaches every contracted core class, hence has rank at
least one by the closed-face separator theorem, hence is a
DegreeFourDharPencil, hence witnesses a
ClosedSubdivisionDharConstruction.
Only the middle statement is row specific. This file packages the other three once, so that a row's closing theorem is a single application.
The closing wrapper. A family of effective degree-four divisors, one for each degenerate spec on a fixed connected core, which reaches every contracted core class, is a closed-orthant AR construction.
The reaches hypothesis is stated on an arbitrary DegSpec with the two
facts a face proof actually uses: its core is the fixed one, and its
representative map is exactly reachability through the zero-length slots.
That is the shape the row lemmas already have, so each row's tail becomes one
application of this theorem.
The face-indexed closing wrapper.
ofReachesCoreClasses instantiates its reaches hypothesis at exactly one
DegSpec — the canonical faceSpec of the face it is looking at. Asking for
reaches at an arbitrary DegSpec is therefore strictly more than the proof
uses. That extra generality is free for a row that builds its script by hand,
and expensive for one that wants to move a picture along a core symmetry: the
symmetry transport (ClosedOrbit.relabeling) is a relabeling between two
faceSpecs, and there is no corresponding datum for a bare DegSpec with an
unconstrained representative map.
This variant asks only for the face-indexed statement. It is the entry point
Guarding.OrbitGuard uses; ofReachesCoreClasses is unchanged and remains the
entry point for every row that already exists.
Combine a positive-subdivision proof with proofs only for the proper boundary faces. This lets a shared positive construction become the load-bearing interior proof while retaining an existing row's contraction arguments. Both branches produce the same closed-orthant obligation.