Complete Native T Deleted Edge Classification
Abstract
Every literal old T cut is absent from the complete independently indexed native T surgery edge set.
Configurations are actual permutations of Fin(m+1), with the three largest prefix reversals a, b and c. CoreDeletedEdge(m,e) enumerates the old T a/b cuts from their actual circle ports. CoreUncut(m,e) enumerates native edges in every owned circle except its own cut. TSeam(m,e) enumerates the actual c connection from each cut endpoint. All three sets are specified without choosing a cycle.
Theorem 1.1 (No Old T Cut Belongs to the Complete Surgery Edge Set).
Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/PrefixReversal/NativeCoreEdgeClassification.native_t_deleted_edge_disjoint (✓ std3). ∎
Source. Repository-derived.
Commentary.
For every m at least four and every undirected configuration edge e, CoreDeletedEdge(m,e) excludes CoreUncut(m,e) and TSeam(m,e). This proves absence from the complete output edge set, rather than inferring it from preservation of other edges.
Suppose a deleted cut were retained by some circle owner. The actual cut-start endpoint belongs to the edge, and native_circle_edge_endpoint places it in that retained circle. The earned unique native T circle ownership makes its owner exactly the cut’s original owner, contradicting that owner’s own cut exclusion. Suppose instead it were a c seam. An undirected edge generated by an involution determines its generator under either endpoint orientation. Actual prefix reversal coordinates distinguish c from both a and b, so a c seam cannot equal an old cut.
The full inventory in native_core_hamiltonian_cycle_with_full_inventory therefore gives actual absence of every old T cut on that same constructed core Hamilton cycle. Further E grafts and the six J2 marked cuts require their own complete surgery inventories and path legality proofs.