Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

First-window two-block boundary rows

Abstract

Two ordered physical rows constrain the joined membership labels and realize a homogeneous internal image.

Theorem 1.1 (Necessary same-stream refinement and safe homogeneous attainments).

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/FirstWindowBoundaryCodes.original_first_window_boundary_rows (✓ std3). ∎

Source. Repository-derived.

Commentary.

Fix m>=5 and k=2m-2. Each support H(v) is a Finset of the actual integer phase representatives 1,…,m in P=ZMod(2m-1). The labels A(v),B(v) are unequal separately; their coincidences across values are unrestricted. The INITIAL target depends on the saved value and support membership, with every inherited tail retained. Y may inhabit any universe and need not be finite. Initial bottom keeps its independent f(none) label and stops freely.

membership(m,H,j) is the ordered pair (supportRow(H(0),j.val), supportRow(H(1),j.val)). The internal phases are those with 2<=j.val<m, and internalImage is their finite actual membership image. Its cardinality is r in Definition 29.1. Each phase is counted once; realizing histories and inherited tails add no multiplicity. firstCharge and secondCharge are the increments of stream(0) at phase -j and stream(1) at phase -j+m. PhaseSumFirst and PhaseSumSecond in the formula sum these respective rows over the entire phase group.

For every correct original two-block GLOBAL competitor, the same literal stream and its own-archive stop function supply both rows. The witness retains correctness on every actual history in each free-value fibre. Equal first and second charges force equality of both membership coordinates: native_fiber realizes each phase, and native_two_same identifies its entire two-block execution with that of any phase having the same pair. The proof applies separately to each value using its unequal A,B labels. Cross-value label collisions cannot remove either membership coordinate.

The native execution comparison includes stopping before either word and common absorption after a rejected block. A second word scheduled for a source that already stopped is used only to define its algebraic profile: it supplies neither an acquired endpoint nor a paid suffix to that source. Every actually issued complete word, including waits and rejecting attempts, remains charged by OriginalPresetFeasible and FiberCorrect.

If H(0) is nonempty, its actual value-zero target is nonconstant, since phase zero is base-labelled. The root therefore cannot stop freely. A leading one rejects every phase with inherited tail k-1 into the same absorbing archive; root_zero consequently forces the actual first bit to be zero. The literal derivative then vanishes on R=P without {1,…,m}, including phase zero. The second moving window has zero charge throughout U={2,…,m-1}. Both full rows have even charge. Since only two first-coordinate values are available on U and the second coordinate is zero, joined refinement forces r<=2. Thus r>=3 excludes every correct two-block competitor.

For r=1, the normalized inverse rows are precisely the two homogeneous-internal constructions of (29.17). At odd widths their physical supports are Ico(1,m) and {1,m}; and their region codes on (U,R,{1},{m}) are (10,00,11,01). At even widths their supports are {1,m} and R union {1}; and their region codes are (00,01,11,10). Distinct regions have distinct codes. The internal region has one membership label and the entire exterior is base-labelled, so equal codes always imply equal membership pairs, without any condition on the two boundary labels.

homogeneousRoot is Ico(1,m) for odd m and {1,m} for even m. homogeneousSecond records ordered second-path offsets, namely {0,m} for odd m and Icc(1,m) for even m. These offset sets give the physical supports above after translating by m in P. All four sets are even in their applicable branch. homogeneousWords issues exactly their prefix-parity inverses, and homogeneousCode is the corresponding chronological pair of successful differences on every phase, including all exterior sources.

Every root begins zero, clearing all legal inherited tails. For odd m its terminal charge at m is zero, so the root ends zero before the all-one second inverse of {0,m}. For even m the second inverse begins zero. Each whole prefix is therefore safe: the second word enters from tail zero or clears the tail immediately, and every word has length m<k. The decoder chooses a phase with its own acquired difference pair and returns that phase’s membership component selected by its remembered free value. This uses one preselected literal stream for both values and both original alphabets.

The native comparison and even-charge identity use D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/GlobalPresetObstruction; actual-phase realization and the root-zero result use D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/OwnPathCharges. The sum and phase-shift identities use D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/FirstWindowBoundaryAttainment; the ordered inverse and complete-prefix safety use D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/WindowChargeInverse. Original history and own-archive feasibility use D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/DonorCorrection.

The displayed live script archive contains exactly two issued blocks and 2m bits; mapReplies and flattenWords project those actual archive components. The theorem gives necessary row refinement and the r=1 safe construction. It leaves the complete Pi3/Pi4 conditions, the other r=2 safe assignments, the four-label pivot table, unequal adaptive stopping lengths and exact worst-history prices to their further classification. A script length alone does not assert an optimal actual paid-trace price.

Theorem 1.2 (Two nonbase internal labels: normalized safe literal selection).

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/FirstWindowBoundaryCodes.original_first_window_nonbase_internal_stream (✓ std3). ∎

Source. Repository-derived.

Commentary.

Retain the full original source, supports, labels and operations above. fullImage is membership[P], of size n. Suppose n=3, the internal image has size two, and it excludes the base pair zero. The admitted condition is odd m or a nonbase membership label at phase one or m, the remaining clause of Pi3 for this branch. The integer one and phaseCast(m) in the formula denote their actual phase-group casts.

The internal labels are two distinct nonzero pairs X,Z. Every actual phase has label zero, X or Z: the exterior contributes zero, and the internal two-label image already exhausts the other two labels of fullImage. Put S={h in U: membership(h)=Z}, t=|S| modulo two and e=m modulo two. Choose an orientation flip and boundary code pairs left,right. Internal X and Z have codes (flip,0) and (1+flip,0); every exterior phase has code (0,1). At phases one and m the codes are left and right. Equal codes must represent equal labels, while one label may occupy more than one code.

The required parity equations are t+flip*e+left.first+right.first=0 and e+1+left.second+right.second=0 in ZMod(2). At odd widths, changing orientation changes the internal root parity. If both boundary labels are internal, select their canonical codes and orient to make the root even. If exactly one is base, orient the odd internal class to code (1,0), then use (1,1) for the internal boundary and (0,1) for base. If both are base, one may use the spare (1,1) to correct root parity. At even widths, at least one boundary is internal. Give that boundary its canonical code with second bit zero, and give the other second bit one. The orientation and spare code then solve the root equation. The formal selector checks these two equations and separation simultaneously.

nonbaseRoot(h) is supportRow(S,h)+flip*supportRow(U,h) plus left.first at h=1 and right.first at h=m. nonbaseSecond uses ordered offsets from m: it is one on Ico(1,m), right.second at offset zero and left.second at offset m. Its interior offsets are exactly the exterior physical phases, including phase zero and the donor m+1. The internal count m-2 has parity e, and the exterior count m-1 has parity e+1; hence both complete ordered rows sum to zero. nonbaseWords is precisely the list of their two prefix-parity inverses. nonbaseCode is their actual chronological difference pair, rather than an unrestricted query.

nonbase_even gives both ordered-row sums zero and the root charge at zero under the displayed parity equations. nonbase_charges identifies both windowCharge coordinates with nonbaseCode. Their first-row projections also supply the root calculations for the base-internal donor construction. classIndex sends base, X and Z to 0,1,2; classLabel reverses these three distinct labels, and class_restore gives the exact inverse on their full image.

The root charge at zero vanishes, so its first literal bit is zero and it clears every inherited legal tail. Its terminal tail is at most m-1. If right.second is zero, the second word starts zero. If it is one, the exterior charge at offset one toggles the prefix immediately, giving a zero at literal index one. The leading seam run is then at most m<k. The proof applies D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/InternalZeroSafety at that actual zero, and the ordered inverse and clear seam from D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/WindowChargeInverse. Thus the complete two-block prefix succeeds for every original value, phase and inherited tail; no arbitrary refining inverse assignment is asserted safe.

Conversely, suppose both boundary labels are base and a correct two-block GLOBAL competitor exists. Apply the necessary row theorem above. The two internal nonbase labels have second charge zero and unequal first charges, exhausting both first-coordinate values. If any base-labelled phase also had second charge zero, it would collide with one of those internal labels. Thus the second charge is one at every exterior phase and both boundaries, and zero on U. Its full-phase sum is m+1 modulo two. The required even charge forces m odd. This uses native_two_same through the already established necessary rows, including all stopping and rejection semantics. It introduces no additional mixed-archive transport premise.

The common selector issues this same preselected list in both value fibres. Its decoder matches the two differences in its own acquired archive, recovers the membership label, and selects the component belonging to its saved free value. Separately unequal A(v),B(v), arbitrary cross-value coincidences, arbitrary Type universes and arbitrary independently observed bottom are retained. Both original alphabets use these same length-m words. Every live script archive has two issued blocks and 2m bits. This establishes the full physical two-nonbase-internal branch of (29.18). The six base-internal cases, four-label pivot, other sharp obstructions and exact paid-trace prices are separate obligations.

References