Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

All independent first-three gaps and every natural fourth-gap lift

Abstract

The physical four-gap max-plus-two cone

Theorem 1.1 (One physical word and its literal cut-zero ear).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/MaxPlusTwo/Endpoint.actualSource_max_plus_two_first_ear

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Circle/FourNegative/MaxPlusTwo/Endpoint.actualSource_max_plus_two_first_ear (✓ std3). ∎

Source. Repository-derived.

Commentary.

For all independent natural a,b,c>=2 and d>=max(max(a,b),c)+2, let k=a+b+c+d and A=1+2^a+2^(a+b)+2^(a+b+c). The theorem constructs one list sigma of Fin(k) satisfying both OriginalOrder(k,A,sigma) and OriginalOrder(k+1,2A,earWord(k,sigma,0)). The old list permutes every physical occurrence exactly once, and both totals are zero. Both predicates bound every natural take-prefix, including empty and saturated takes. No coprimality, primitivity, distinct numerical values or supplied feasibility premise is assumed.

The exact baseWord uses four positive physical blocks separated by U-minus,V-minus,W-minus,X-minus. The ascending, descending, strict-valley and strict-peak branches partition all independent gap orderings with their equality faces. ActualStrong combines the literal source shadow and charge table with the mask inventory and three reserve inequalities. The ordinary descending OR masks count coincident bits once; its c=2,a=b+1 family advances the lowest X-positive and uses the exact third reserve 5A-2e3 and remaining charge A-2Cprime.

Ascending masks reserve V and W labels using nonnegative rounded quotients, with a low U release of at most three units. The strict-valley and peak masks use their dyadic ratios, retaining adjacent ratios and a=2 or b=2 boundaries. At every proper physical prefix the final X-negative retains positive charge. The resulting Strong invariant controls the old height h and shadow r=h+Q; the enlarged height after its first ear is h+r.

For d=d0+t with d0=max(max(a,b),c)+2, physicalWord prepends labels 0 through t-1 and shifts every base label by t. The proved natural lift preserves Q and scales r by 2^t. The existing Fin-label transport supplies one old sigma, and marked_word identifies the enlarged list with the literal earWord at cut zero. This sufficient cone does not settle the unrestricted four-gap joint-order problem or the circle conjecture below this fourth-gap threshold.

References