Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Original-coordinate port cycles and avoiding words

Abstract

Original-coordinate port cycles and avoiding words

For an arbitrary original coordinate type X, originalSpan H is precisely the integer span of the coefficient-one Boolean rows of the original family H. Complete M Omega contains all nonempty proper Boolean supports whose rows belong to M; minimalFamily is its full inclusion-minimal family. neighborhood M Omega x records literal original-coordinate incidence. No saturation, quotient, field extension or cancellation of a scaled relation is used.

Geometry M Omega q records a family B of q-free minimal rows, each meeting at least two terminal rows through q. Every pair of distinct terminals has a common B-neighbour; every B row misses some terminal. Each original coordinate shared by b in B and terminal t has exactly the minimal-row neighbourhood {t,b}. Other original coordinates, including private, unused, parallel and exterior coordinates, are unrestricted. This structure is an explicit premise; it is not derived here from charge hypotheses.

Choose b0 in B and distinct terminal neighbours a,z, together with a terminal u not neighbouring b0. The rank is injective on terminals, with a least and z greatest. At b0 exactly the ports at z are red. At each other b exactly its least terminal neighbour has red ports. K supplies exterior blue coordinates, lies in Omega minus q, and is disjoint from each B row. The relation arc G Blue s t asks for a shared B row and an actual blue ORIGINAL coordinate at t. B witnesses can repeat.

Theorem 1.1 (Construct the reverse cycle using actual original blue ports).

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Sequenceability/PositiveChargePorts.exists_portCycle (✓ std3). ∎

Source. Repository-derived.

Commentary.

The explicit paths a to u to z to a and the remaining terminal routes establish strong connectivity. Semicompleteness follows from pair coverage and the actual port colouring. Apply finite_semicomplete_hamilton to the reverse relation, then choose a blue original coordinate from each actual arc. PortStep e f records f.terminal to e.terminal through e.port. The closing step uses the same first port. Distinct terminal endpoints imply distinct blue coordinate IDs, even when B witnesses repeat.

Theorem 1.2 (A literal word avoids every complete original Boolean row).

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Sequenceability/PositiveChargePorts.native_avoiding_word (✓ std3). ∎

Source. Repository-derived.

Commentary.

The cycle C is an output, with no Hamilton-cycle or PortCycle premise. The exterior mixed-colouring premise concerns every q-free minimal row outside B. The disjoint decomposition premise concerns EVERY Complete row and expresses it as the union of an independent subfamily of the actual minimalFamily. Both remain explicit. The red coordinates alpha,beta and all local B-star colour witnesses are constructed.

For P equal to the original ports in reverse cyclic order, the literal cycleWord is (Omega minus insert q Blue minus {alpha,beta}).toList, followed by alpha,beta,q, then P, then (Blue minus P.toFinset).toList. Its permutation theorem preserves every original coordinate exactly once. It does not identify parallel coordinates or discard the exterior and private coordinates.

If a selected disjoint union contains q, exactly one selected terminal d contains q. For d=a, alpha is present and beta is forbidden by beta’s exact neighbourhood {z,b0}. For any other terminal, its arrival port is present and the immediately preceding port is absent from the entire selected union. An interval joining q to that arrival port must cross the absent predecessor. If q is absent, any selected minimal row has both a red and a blue coordinate, so its interval crosses q. These arguments handle all complete rows, including larger disjoint unions. They reuse the original infix_avoid_separator proof in PrivatePairBooleanDescent.

Theorem 1.3 (Universal-neighbour rows admit a literal avoiding word).

Lean statement: D5/S3/Combinatorics/Sequenceability/PositiveChargePorts.universal_avoiding_word

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Sequenceability/PositiveChargePorts.universal_avoiding_word (✓ std3). ∎

Source. Repository-derived.

Commentary.

For arbitrary M, Omega and q, assume Blue lies in Omega minus q, l is red, rho is blue, u and v are distinct terminals, and bzero is a q-free row meeting every terminal. The exact original neighbourhoods of l and rho are {u,bzero} and {v,bzero}. A red original coordinate b belongs to v; every terminal has a blue coordinate; every q-free minimal row has both colours. Every Complete row is the disjoint union of original minimal rows. The explicit word (red minus l).toList followed by l,q,rho and (Blue minus rho).toList permutes ALL Omega and avoids EVERY Complete infix. These remain explicit hypotheses in this port theorem; the geometry module derives them on the actual positive-charge branch.

If q belongs to an infix, disjointness identifies its unique selected terminal d. For d=v, the red b forces l across the interval, but l is forbidden by its exact two suppliers. Otherwise a blue coordinate of d forces rho, forbidden by its exact two suppliers. If q is absent, mixedness forces the q separator. All residual original coordinates are retained, and either residual side may be empty.

The port constructions are conditional. PositiveChargeGeometry derives their original geometry, exterior colouring, universal frame and decomposition inputs in the actual ordinaryChargeGCD=r positive branch. Zero charge, full Good and adaptive merge are separate obligations. The longest-cycle theorem is classical; the original-coordinate composition makes no literature-priority claim.

References