Literal Windows and Positive End

Abstract

Low-to-high three-bit windows have a terminal flag as well as a seam. Successful literal End queries correspond to independent selected positions.

Theorem 1.1 (The seam guard recognizes the flattened legal word).

$$\begin{array}{r}\forall s,E\in B,\forall w\in W^{\ast },\\ (\mathrm{run}(\mathrm{some}((s,E)),w)=\mathrm{some}((\mathrm{lastFold}(s,w),\mathrm{endFold}(E,w)))⟺\mathrm{legal}(s,\mathrm{flatten}(w)))\wedge \\ (\mathrm{run}(\mathrm{some}((s,E)),w)=none⟺\neg \mathrm{legal}(s,\mathrm{flatten}(w))).\end{array}$$

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

Source. Repository-derived.

Commentary.

Here B is the Boolean set, W is the five-letter window alphabet, W* is its finite-word set, and none is the absorbing error. The letters are 000, 100, 010, 101 and 001 in low-to-high order. The final seam and End flag are the following folds; the initial End flag survives only for the empty word.

$$\begin{array}{r}\mathrm{lastFold}(s,w)=\mathrm{foldl}(((a,b)\mapsto \mathrm{last}(b)),s,w),\\ \mathrm{endFold}(E,w)=\mathrm{foldl}(((a,b)\mapsto \mathrm{nonzero}(b)),E,w).\end{array}$$

A live transition rejects an incoming seam 1 followed by a low bit 1. Otherwise it takes the high bit as the new seam and records whether the current window is nonzero as End. Legal(s,flatten(w)) includes the incoming seam and excludes adjacent ones in the complete flattened word.

Theorem 1.2 (All successful bounded queries have an exact independent-set parametrization).

$$\begin{array}{r}\forall t\in \mathbb{N},(\exists e:\mathrm{Equiv}(S_t,I_t),\\ (\forall x\in I_t,e^{-1}(x)=\mathrm{encode}(t,x))\wedge \\ (\forall w\in S_t,\mathrm{independentBits}(t,e(w))=\mathrm{flatten}(\mathrm{pad}(t,w)))\wedge \\ (\forall w\in S_t,\forall r\in \mathbb{N},\forall u\in \mathbb{N},\forall v\in \mathbb{N},\mathrm{query}(r,u,v,w)=\mathrm{some}((r+O(t,u,v,e(w)))))\wedge \\ (\forall H\in \mathbb{N},\forall u\in \mathbb{N},\forall v\in \mathbb{N},\forall w\in S_t,\mathrm{value}([u{]}_H,[v{]}_H,\mathrm{flatten}(w))=[O(t,u,v,e(w)){]}_H))\wedge \\ |S_t|=F_{3t+1}\wedge \\ (\forall w\in W^{\ast },\forall r\in \mathbb{N},\forall u\in \mathbb{N},\forall v\in \mathbb{N},\mathrm{query}(r,u,v,w)=none⟺\neg \mathrm{Success}(w))\wedge \\ (\forall w\in W^{\ast },\forall r\in \mathbb{N},\forall u\in \mathbb{N},\forall v\in \mathbb{N},(\mathrm{Success}(w)\wedge 0<r)⟹(\exists N\in \mathbb{N},0<N\wedge \mathrm{query}(r,u,v,w)=\mathrm{some}(N)))\wedge \\ |L_t|=\sum _{n=0}^t{5}^n\wedge \\ |R_t|=\sum _{n=0}^t{5}^n-F_{3t+1}\wedge \\ (\forall H\in \mathbb{N},\forall u\in \mathrm{ZMod}(H),\forall v\in \mathrm{ZMod}(H),|\mathrm{centerImage}(t,H,u,v)|\le F_{3t+1})\wedge \\ (\forall epsilon\in B,\forall w\in W^{\ast },\forall N\in \mathbb{N},\mathrm{initialized}(epsilon,w)=\mathrm{some}(N)⟹0<N).\end{array}$$

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

Source. Repository-derived.

Commentary.

All word lengths are numbers of whole windows. S_t is the set of words of length at most t with a true End flag after running from (seam,End)=(true,true); L_t contains every such literal word, and R_t contains those in L_t without success. I_t consists of independent Boolean selections at offsets 1 through 3t-1, identified with their selected-position sets; I_0 is a singleton. The empty selection gives the empty query, which is charged and successful.

$$\begin{array}{r}\mathrm{Success}(w)⟺\mathrm{endable}(\mathrm{run}(\mathrm{some}((true,true)),w))=true,\\ S_t=\{w\in W^{\ast }\mid \mathrm{length}(w)\le t\wedge \mathrm{Success}(w)\},\\ L_t=\{w\in W^{\ast }\mid \mathrm{length}(w)\le t\},\\ R_t=\{w\in L_t\mid \neg \mathrm{Success}(w)\},\\ I_0=\{\varnothing \},\\ t>0⟹I_t=\{x\subseteq \{i\in \mathbb{N}\mid 1\le i<3t\}\mid \mathrm{noAdjacent}(x)\}.\end{array}$$

Equiv(S_t,I_t) is the type of invertible maps; e inverse is the reverse map. Encode prepends the forced zero bit, packs windows, and removes only terminal whole 000 windows. Its inverse pads a successful word to t windows and flattens it. The selected offset below uses F_0=0 and F_1=1, so position 1 contributes v.

$$O(t,u,v,x)=\sum _{i\in x}(F_{i-1}u+F_{i}v),x\in I_t.$$

The modular value equality uses the same natural u and v after reduction modulo H. ZMod(H) is the residue ring and [a]_H denotes reduction of a natural a. CenterImage(t,H,u,v) is the set of negated modular values of successful words. A nonzero terminal window 100 or 010 is retained; first-01 words are retained. A trailing whole 000 window clears End and gives the same error for every numeric input.

$$\mathrm{centerImage}(t,H,u,v)=\{-\mathrm{value}(u,v,\mathrm{flatten}(w))\mid w\in S_t\},u,v\in \mathrm{ZMod}(H).$$

Initialized(epsilon,w) uses r=epsilon, u=2, v=3 and starts with both Boolean state fields equal to epsilon. Its successful numeric answer is positive. Applying the original terminal readout to that answer gives H divided by gcd(N,H).

The existing admissible-word count gives F_(3t+1) successes. For t=3 there are 55 successes among 156 literal words, leaving 101 errors. The image of their modular translations or negated centers has at most 55 elements; different successful words may have the same modular image. This parametrization does not establish residue realization at a common returned row or the finite-center identification criterion.

$$\begin{array}{r}|S_3|=55,|L_3|=156,|R_3|=101,\\ \forall H\in \mathbb{N},\forall u\in \mathrm{ZMod}(H),\forall v\in \mathrm{ZMod}(H),|\mathrm{centerImage}(3,H,u,v)|\le 55.\end{array}$$

References

• Truth anchor: D5/S3/Arith/FibonacciAtomic/LiteralWindowEnd.execution
• Truth anchor: D5/S3/Arith/FibonacciAtomic/LiteralWindowEnd.result
• Dependency: D5/S1/Words/AdmissibleWords/AdmissibleCount
• Dependency: D5/S3/Arith/ZeckendorfFutureKernel