Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Complete Native Circle Cut Pieces

Abstract

A native a/b circle has complete actual cut complements, with supports exhausting its independently defined rotation-and-reversal domain.

Theorem 1.1 (Actual Rotation Preserves the Tuple Cycle).

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/PrefixReversal/NativeCircleComplement.native_configurationCycle_rotation (✓ std3). ∎

Source. Repository-derived.

Commentary.

Right multiplication by any finCycle rotation preserves the actual tuple modulo rotations.

Theorem 1.2 (Actual Full Reversal Reverses the Tuple Cycle).

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/PrefixReversal/NativeCircleComplement.native_configurationCycle_reversal (✓ std3). ∎

Source. Repository-derived.

Commentary.

Right multiplication by a reverses the actual configuration tuple cycle.

Let m be at least three and let z be a permutation of Fin(m+1). Circle(z,v) means that the actual circular tuple of v equals that of z or its whole reversal; only rotations are quotiented in the tuple. Thus Circle is specified without reference to a walk. Its coordinates are zR^r and zR^r*a for r in Fin(m+1), where R=ab rotates all positions by one.

Definition 1.3 (All Actual Native Circle Coordinates).

Formalization. D5/S3/Combinatorics/Graph/PrefixReversal/NativeCircleComplement.circleEquiv (✓ std3).

Source. Repository-derived.

Commentary.

The coordinates form a bijection onto Circle(z). Injectivity reuses the existing deletion-star coordinateEquiv at one fixed gap, rather than proving a second dihedral injection. Surjectivity comes from actual tuple rotations; the negative case applies a whole reversal first, and then uses the involution a to recover the configuration.

Theorem 1.4 (The Complete b-Cut Complement).

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/PrefixReversal/NativeCircleComplement.native_b_complement (✓ std3). ∎

Source. Repository-derived.

Commentary.

The literal H word is U_m=(ab)^ma, with length 2(m+1)-1 and product b. Its scanl is the ordered flattened list [zR^r,zR^ra] over all r in Fin(m+1). The circle-coordinate bijection makes this trace simple and exhaustive. Every step is an actual a/b edge. A simple path containing the edge between its endpoints would have length one, so the displayed long path avoids its b-cut edge and transfers to the graph with that edge deleted.

Theorem 1.5 (The Complete a-Cut Complement).

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/PrefixReversal/NativeCircleComplement.native_a_complement (✓ std3). ∎

Source. Repository-derived.

Commentary.

Start with the actual b-cut H path. Its second vertex is za. Reverse the path after its first a-edge, and prepend the actual b-edge from z to zb. The support is z followed by the reverse of the H trace’s tail. It is a permutation of the original complete simple support. Its endpoint is z*a, its length remains 2(m+1)-1, and simplicity again excludes the a-cut edge.

Theorem 1.6 (Every Other Native Edge Is Retained).

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/PrefixReversal/NativeCircleComplement.native_complement_edge_inventory (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let g be a or b, and let w be an actual a/b path from z to zg, of length 2(m+1)-1, whose support is exactly Circle(z). At every x in Circle(z), and for either h=a or h=b, the edge from x to xh occurs in w exactly when it differs from the deleted endpoint edge from z to zg. To prove this, close the actual path with that endpoint edge. Every supported vertex has two cycle neighbors, and the native a/b graph allows only xa and x*b. These are distinct, so equality of the finite neighbor cardinalities forces both actual edges into the cycle. Removing its literal first edge leaves precisely all other native edges in the complement. This earns the retained b edges required at subsequent one-contact insertion suppliers.

Theorem 1.7 (The Complete Complement Edge Set).

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/PrefixReversal/NativeCircleComplement.native_complement_full_edge_inventory (✓ std3). ∎

Source. Repository-derived.

Commentary.

For any actual undirected configuration edge e, membership in the complete native complement is equivalent to NativeCircleEdge(z,e) and inequality with the literal cut. NativeCircleEdge means that e joins x to x*h for an actual x in Circle(z) and h equal to a or b. The forward direction uses the actual walk adjacency and support to earn that form; the complete native retained-edge theorem supplies both cut exclusion and the converse. This arbitrary-edge equivalence is consumed by the full T/E graft surgery inventory, including its absence direction.

Theorem 1.8 (Both Native Edge Endpoints Remain in Their Actual Circle).

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/PrefixReversal/NativeCircleComplement.native_circle_edge_endpoint (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every m, if e is a NativeCircleEdge(z,e), each actual configuration v belonging to the undirected edge e lies in Circle(z). The native generators a and b both reverse the actual tuple cycle: b is a whole reversal followed by an oriented rotation. Circle is closed under either action. Undirected edge membership selects one of these two actual endpoints. Complete T deleted-edge classification consumes this endpoint property to identify the unique circle owner of any alleged retained old cut.

These are complete native D-circle pieces for switching constructions. Their membership equivalences cover every configuration in the independent circle domain, with no finite search. Connecting multiple circles still requires actual connecting edges, distinct circle ownership and complete coverage of the intended larger domain.

References