Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Shared Completion and First Rejection

Abstract

The shared raw complement collision law equals the ordered six-state scalar transfer entry.

Let k be any natural number and n=k+1. A is any subset of Fin(n), B is its complementary subtype, and P,Q are any reachable profiles in Profile(k,A). The arbitrary actual assignments a,a’ on A satisfy code(A,a)=encode(P) and code(A,a’)=encode(Q). No canonical-choice restriction is imposed on them. The alphabet consists of all five complete windows 000,100,010,101,001, written from low to high; all raw assignments remain in the domain, including bad seams, terminal zero, and every suffix after rejection. Zero consumes one position.

T means the original frozen task: the earliest bad seam, then terminal zero if every seam passed, then acceptance. A Lean finite label j represents source label j+1, and top represents acceptance. A merged word uses a on A and b on B. G(a,a’)=sharedProbability is the sum of the indicators T(merge(A,a,b))=T(merge(A,a’,b)), over every b:B->Window, divided by 5^|B|. U(a,a’)=fullProbability uses the same event after fullMerge, summing over all n-coordinate raw words and dividing by 5^n. Its A coordinates are dummy draws. Gamma(P,Q)=collisionProbability is U for the frozen canonical representatives. independentCollision(k,A,a,a’) instead sums the collision indicators over two independent full dummy words u,v and divides by 5^(2n). Every B coordinate supplies the SAME whole window to both histories; distinct coordinates are independent. No independence of bits inside a window is asserted.

The six states are s00,s01,s10,s11,E,D in that order. The initial state is s00. Each live state stores the two previous high bits. On symbols c,d, step first tests the incoming seams r AND first(c), r’ AND first(d). Both failures give E; one gives D; neither installs the actual high-bit pair at a nonterminal position. At the terminal position, neither failure gives E precisely when the two current zero-window flags agree, and gives D otherwise. E and D absorb. End is the external query already folded into this terminal operator; there is no extra symbol, input position, or random draw.

Qa=actualMatrix(k,A,a,a’) is the position-dependent matrix. At i it averages, with weight 1/5, the one-hot transitions step(i=last(k),s,c,d) over the five x, where c=a(i),d=a’(i) on A and c=d=x on B. Qc=SharedMatrix(k,A,P,Q) uses the canonical representatives. K(Q)=matrixEntry(Q) is the s00,E entry of the chronological product List.ofFn(Q).prod. I is the rational equality indicator, one when its argument holds and zero otherwise. terminal(i) is the Boolean test i=last(k). terminalOrNonterminal(i) means terminalMatrix when i=last(k), and nonterminalMatrix otherwise. constantWord denotes the singleton word on Fin(1).

Theorem 1.1 (Complete Shared Collision Law).

Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/SharedCompletionCollision.result (✓ std3). ∎

Source. Repository-derived.

Commentary.

The statement below is one conjunction under all its displayed binders and representative equations. u,v range over all Word(k); c,c’ range over Side(k,A); i ranges over Fin(k+1); s,t range over the six states. Qa(c,c’) denotes actualMatrix with those assignments. In the fixed-position clause the assignments are evaluated on the subtype element (i,h), for the given h:i in A. The full-cut indicator uses extend(A,a), which equals the deterministic full word when A is all coordinates.

For the actual nonterminal prefix of m positions, search the incoming-seam tests with findIdx?. Every stored first hit r satisfies r<m. Two absent hits give the live previous-bit state; two equal finite hits give E; all other cases give D. A new first hit at m cannot equal an old r<m. At m=k this same bound separates earlier stops from the last incoming seam and terminal zero. The full test list is false followed by the original bad tests; its first hit is the injective encoding top->none, j->some(j+1) of T. Thus the run event is exactly the original task equality.

Reindexing the finite raw assignment sums yields the ordered matrix recurrence. The dummy A-coordinate fibers have multiplicity 5^|A|, which cancels from 5^n to give the B-only law. At an A position, five identical dummy summands cancel to the deterministic one-hot operator. The absorbing rows sum to one, so every raw suffix retains its full mass. The frozen response-fiber theorem transports labels for each fixed b, establishing independence of the scalar entry from representative choice. Individual factors and the full product matrix need not be independent of that choice.

The nonterminal and terminal B operators are the following exact matrices. The terminal rows from s00,s11 put mass one at E; those from s01,s10 put 3/5 at E and 2/5 at D. Both absorbers self-loop.

At n=1 and A empty, sharing the complement gives collision one; two independent completions give 17/25. Zero and middle have the same ports and nonterminal transition, but their terminal labels differ. This is a position-scheduled evaluator with externally supplied cut and representatives. It asserts neither minimal state count nor an autonomous clock, and uses no rank premise.

References