Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Energy before SMALL count: the physical mixed-suffix exchange

Abstract

Mixed suffix exchange: a native even expanding unused path can replace a consumed label and its mixed suffix, with full physical bookkeeping and strict (G,H,U) descent when the suffix has at most m-1 LARGE labels.

Theorem 1.1 (The explicit exchange and both descent cases).

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Circle/MixedSuffixEnergy.mixed_suffix_energy_exchange (✓ std3). ∎

Source. Repository-derived.

Commentary.

All labels live in the original Fin(k), and s is SourceWidth.actualSource. W=A++[x]++B is a legal distinct-label word. The literal modulo-k successor path of even length m>=2 consists of unused LARGE labels and enters x. The sole expanding condition is d=3*|s(p)|-N>0; sign orientation is selected inside the proof. LARGE means |s|>=Q, SMALL means |s|<=Q-1, where Q=2^(k-2), N=4Q-1, C=N/2. There is no append-blocking, suffix-repair, endpoint, minimizer, or replacement-energy hypothesis.

G is the sum of LARGE indicators over the actual unused physical complement. U is its cardinality, expressed as a sum of ones. H is the sum of 3^|s| over consumed LARGE occurrences. smallUsed(B) and largeUsed(B) partition the literal suffix labels, rather than a quotient by numerical values. Their sum is B.length. J is the standard natural lexicographic triple (G,H,U), using mathlib’s nested Lex product.

The new word is exactly V=A++path. If m>=k, the earlier index m mod k reaches the consumed terminal physical label, contradicting unusedness. Thus m<k; modular cancellation proves path.Nodup, and unusedness proves disjointness from all of W. The proof derives both used and unused partitions and the disjointness of both displayed unions. Equal source values, nonunits, and short numerical orbits never merge labels or energy multiplicities.

ExpandingSourcePath supplies 0<=F_j<=r for every natural take and sum_path 3^|s| < 3^r. If x is positive, old legality bounds a between 0 and C-r. If x is negative, it bounds a between r and C. Every inserted height therefore lies between the original departure and arrival heights of x. The unchanged prefix A is then appended to this proved path. Empty and overlength takes are included through InStrip and min(n,m), with no endpoint-only shortcut.

The exact natural balances are G(V)+m=G(W)+1+largeUsed(B) and U(V)+m=U(W)+1+B.length. H(A) cancels, and the inserted energy is strictly below the returned contribution of x alone; all returned LARGE terms of B are nonnegative. For largeUsed(B)=m-1, this gives G(V)=G(W), H(V)<H(W), U(V)=U(W)+smallUsed(B). If largeUsed(B)<=m-2, the same explicit V strictly lowers G. The suffix SMALL labels may have any signs and positions and may all be returned. Moving H before U is what makes their returned count compatible with strict descent.

The new complement sum is minus the new endpoint, using the existing physical zero-total theorem ZeroSumSubsets.source_cycle and the new literal complement, not an assumed inventory partition. The proof never invokes SMALL ORDERING on a LARGE batch. It uses no minimizer wrapper, no assumption of completion, no new axiom or proof placeholder.

The universal availability gap remains: no theorem here forces such an eligible even expanding path or such a short LARGE suffix at every hypothetical incomplete global minimizer. The case with two later opposite-sign LARGE labels still needs an actual SMALL-subset gate, and deeper suffixes or isolated/SMALL source boundaries need further constructions. E_keep_one is optional and is not included in this candidate. d=0 and k<3 are outside this exchange theorem. An all-zero source cannot satisfy d>0; this theorem supplies no separate zero-source completion claim. Seam crossings, ties, short numerical periods, and nonunits carry no extra hypotheses. Full C3.1 remains OPEN.

References