Finite Carry-slot Sampling

Abstract

A stationary carry table needs only a bounded slot control to preserve every fair-tape output and charge.

Definition 1.1 (Stationary state and action orbit).

$$(\forall m:\mathbb{N},(\forall f:P\left(m\right),(\forall c:S\left(m\right),(\forall d:\mathbb{N},(\mathrm{state}\left(\mathrm{policyPath}\left(m,f,c\right),d\right)=\mathrm{iterate}\left(\mathrm{successorBy}\left(f\right),d,c\right)\wedge \mathrm{action}\left(\mathrm{policyPath}\left(m,f,c\right),d\right)=f\left(\mathrm{iterate}\left(\mathrm{successorBy}\left(f\right),d,c\right)\right))))))$$

Formalization. D5/S3/Arith/FibonacciAtomic/CarryGraphFiniteSampler.policyPath (✓ std3).

Source. Repository-derived.

Commentary.

A legal stationary table determines the successive carry states and actions. The path may begin at any legal state; the sampler uses the root.

Definition 1.2 (Bounded active controls).

$$(\forall m:\mathbb{N},\mathrm{Active}\left(m\right)=\{(s,j)\in \mathrm{Product}\left(S\left(m\right),\mathbb{N}\right)\mid j<r\left(s\right)\})$$

Formalization. D5/S3/Arith/FibonacciAtomic/CarryGraphFiniteSampler.Active (✓ std3).

Source. Repository-derived.

Commentary.

S(m) contains exactly the legal integer carry states. The slot j is a natural number below r, so an active control has positive width. The stored fields are r, e and j; no depth or history word is stored.

Definition 1.3 (Root control).

$$(\forall m:\mathbb{N},(2\le m\to \mathrm{initial}\left(m\right)=\mathrm{inl}\left((\mathrm{root}\left(m\right),0)\right)))$$

Formalization. D5/S3/Arith/FibonacciAtomic/CarryGraphFiniteSampler.initial (✓ std3).

Source. Repository-derived.

Commentary.

The root has r=1 and e=m, with its unique slot numbered zero.

Definition 1.4 (One-bit control transition).

$$(\forall m:\mathbb{N},(\forall f:P\left(m\right),(\forall u:Bool,(\forall c:\mathrm{Sum}\left(\mathrm{Active}\left(m\right),\mathrm{Fin}\left(m\right)\right),\mathrm{step}\left(m,f,u,c\right)\in \mathrm{Sum}\left(\mathrm{Active}\left(m\right),\mathrm{Fin}\left(m\right)\right)))))$$

Formalization. D5/S3/Arith/FibonacciAtomic/CarryGraphFiniteSampler.step (✓ std3).

Source. Repository-derived.

Commentary.

An output control is absorbing. At an active control (s,j), apply the legal action f(s), form the increasing list L of its fixed labels, and set z=2j+toNat(u). If z is below the length of L, output L[z]. Otherwise move to the carry successor and slot z-length(L). A slot guard totalizes the definition by retaining the old active control when the guard fails; the correspondence proves this case is never taken from the root.

Definition 1.5 (Control and separate invoice).

$$(\forall m:\mathbb{N},(\forall f:P\left(m\right),(\forall c:\mathrm{Sum}\left(\mathrm{Active}\left(m\right),\mathrm{Fin}\left(m\right)\right),(\forall tape:Tape,(\mathrm{execute}\left(m,f,c,tape,0\right)=(c,0)\wedge (\forall d:\mathbb{N},\mathrm{execute}\left(m,f,c,tape,(d+1)\right)=(\mathrm{step}\left(m,f,\mathrm{bit}\left(tape,d\right),\mathrm{fst}\left(\mathrm{execute}\left(m,f,c,tape,d\right)\right)\right),(\mathrm{snd}\left(\mathrm{execute}\left(m,f,c,tape,d\right)\right)+\mathrm{indicator}\left(isLeft,\mathrm{fst}\left(\mathrm{execute}\left(m,f,c,tape,d\right)\right)\right)))))))))$$

Formalization. D5/S3/Arith/FibonacciAtomic/CarryGraphFiniteSampler.execute (✓ std3).

Source. Repository-derived.

Commentary.

At an output control, execution returns the previous control and invoice directly. Only the active branch takes the next tape bit and increments the invoice. Only the control and that bit enter step; the invoice is an external execution observation.

Definition 1.6 (First output with its invoice).

$$(\forall m:\mathbb{N},(\forall f:P\left(m\right),(\forall c:\mathrm{Sum}\left(\mathrm{Active}\left(m\right),\mathrm{Fin}\left(m\right)\right),(\forall tape:Tape,\mathrm{sample}\left(m,f,c,tape\right)=\mathrm{firstOutput}\left(\mathrm{execute}\left(m,f,c,tape\right)\right)))))$$

Formalization. D5/S3/Arith/FibonacciAtomic/CarryGraphFiniteSampler.sample (✓ std3).

Source. Repository-derived.

Commentary.

Take the first execution index whose control is an output, and return its label and invoice. The sample is absent if no finite output occurs.

Definition 1.7 (Every active step is charged).

$$(\forall m:\mathbb{N},(\forall f:P\left(m\right),(\forall c:\mathrm{Sum}\left(\mathrm{Active}\left(m\right),\mathrm{Fin}\left(m\right)\right),(\forall tape:Tape,\mathrm{bill}\left(m,f,c,tape\right)=\sum _{d\in \mathbb{N}}\mathrm{indicator}\left(isLeft,\mathrm{fst}\left(\mathrm{execute}\left(m,f,c,tape,d\right)\right)\right)))))$$

Formalization. D5/S3/Arith/FibonacciAtomic/CarryGraphFiniteSampler.bill (✓ std3).

Source. Repository-derived.

Commentary.

The sum is nonnegative extended-real. A divergent execution has infinitely many active steps and therefore an infinite bill.

Theorem 1.8 (Every tape preserves the carry slot and invoice).

$$(\forall m:\mathbb{N},(2\le m\to (\forall f:P\left(m\right),(\forall tape:Tape,(\forall d:\mathbb{N},((\forall i:\mathrm{Fin}\left(m\right),(\forall n:\mathbb{N},(\mathrm{scan}\left(m,\mathrm{policyPath}\left(m,f,\mathrm{root}\left(m\right)\right),tape,d\right)=\mathrm{inl}\left((i,n)\right)\to \mathrm{execute}\left(m,f,\mathrm{initial}\left(m\right),tape,d\right)=(\mathrm{inr}\left(i\right),n))))\wedge (\forall j:\mathbb{N},(\mathrm{scan}\left(m,\mathrm{policyPath}\left(m,f,\mathrm{root}\left(m\right)\right),tape,d\right)=\mathrm{inr}\left(j\right)\to (\exists x:\mathrm{Active}\left(m\right),(\mathrm{execute}\left(m,f,\mathrm{initial}\left(m\right),tape,d\right)=(\mathrm{inl}\left(x\right),d)\wedge \mathrm{core}\left(x\right)=\mathrm{state}\left(\mathrm{policyPath}\left(m,f,\mathrm{root}\left(m\right)\right),d\right)\wedge \mathrm{slot}\left(x\right)=j))))))))))$$

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

Source. Repository-derived.

Commentary.

For any legal stationary table and any tape, a returned scan label and charge equal the controller output and invoice. A continuing scan slot lifts to an active control with the current orbit state and the same slot, while its invoice equals the number of bits read. The relation holds without a positive-anchor or optimality assumption.

Theorem 1.9 (Finite control attains the critical bit bill).

$$(\forall m:\mathbb{N},(2\le m\to (\forall f:P\left(m\right),(\exists gamma:Path,(\exists p:\mathrm{Fin}\left(m\right)\to \mathbb{R},(gamma=\mathrm{policyPath}\left(m,f,\mathrm{root}\left(m\right)\right)\wedge (\forall i:\mathrm{Fin}\left(m\right),p\left(i\right)=\mathrm{ofDigits}\left(\mathrm{labelDigit}\left(gamma,i\right)\right))\wedge (0<\mathrm{anchorValue}\left(gamma\right)\to (\mathrm{pathCost}\left(gamma\right)=(\mathrm{alpha}\left(m\right)\cdot \mathrm{anchorValue}\left(gamma\right))\to (\mathrm{IsRootPath}\left(m,gamma\right)\wedge \mathrm{Finite}\left(\mathrm{Active}\left(m\right)\right)\wedge \mathrm{card}\left(\mathrm{Active}\left(m\right)\right)\le \frac{(m^2\cdot (m-1))}{2}\wedge \mathrm{card}\left(\mathrm{Fin}\left(m\right)\right)=m\wedge (\forall tape:Tape,(\forall d:\mathbb{N},((\forall i:\mathrm{Fin}\left(m\right),(\forall n:\mathbb{N},(\mathrm{scan}\left(m,gamma,tape,d\right)=\mathrm{inl}\left((i,n)\right)\to \mathrm{execute}\left(m,f,\mathrm{initial}\left(m\right),tape,d\right)=(\mathrm{inr}\left(i\right),n))))\wedge (\forall j:\mathbb{N},(\mathrm{scan}\left(m,gamma,tape,d\right)=\mathrm{inr}\left(j\right)\to (\exists x:\mathrm{Active}\left(m\right),(\mathrm{execute}\left(m,f,\mathrm{initial}\left(m\right),tape,d\right)=(\mathrm{inl}\left(x\right),d)\wedge \mathrm{core}\left(x\right)=\mathrm{state}\left(gamma,d\right)\wedge \mathrm{slot}\left(x\right)=j)))))))\wedge (\forall tape:Tape,(\mathrm{sample}\left(m,f,\mathrm{initial}\left(m\right),tape\right)=\mathrm{treeSample}\left(m,gamma,tape\right)\wedge \mathrm{bill}\left(m,f,\mathrm{initial}\left(m\right),tape\right)=\mathrm{treeBill}\left(m,gamma,tape\right)))\wedge (\forall i:\mathrm{Fin}\left(m\right),0<p\left(i\right))\wedge \sum _{i\in \mathrm{Fin}\left(m\right)}p\left(i\right)=1\wedge 0<\mathrm{anchorValue}\left(gamma\right)\wedge \inf \left(\mathrm{range}\left(p\right)\right)=\mathrm{anchorValue}\left(gamma\right)\wedge (\forall i:\mathrm{Fin}\left(m\right),(\exists q:\mathbb{Q},\mathrm{real}\left(q\right)=p\left(i\right)))\wedge (\forall i:\mathrm{Fin}\left(m\right),p\left(i\right)=\sum _{d\in \mathbb{N}}\frac{\mathrm{indicator}\left(\mathrm{labelSet}\left(m,gamma,d\right),i\right)}{2^{(d+1)}})\wedge (\forall tape:Tape,(\forall i:\mathrm{Fin}\left(m\right),(\forall d:\mathbb{N},\mathrm{sample}\left(m,f,\mathrm{initial}\left(m\right),tape\right)=\mathrm{some}\left((i,(d+1))\right)⟺(\mathrm{prefix}\left(tape,(d+1)\right),i)\in \mathrm{stopping}\left(m,gamma,d\right))))\wedge (\forall tape:Tape,(\forall i:\mathrm{Fin}\left(m\right),(\forall n:\mathbb{N},(\mathrm{sample}\left(m,f,\mathrm{initial}\left(m\right),tape\right)=\mathrm{some}\left((i,n)\right)\to \mathrm{bill}\left(m,f,\mathrm{initial}\left(m\right),tape\right)=n))))\wedge (\forall i:\mathrm{Fin}\left(m\right),\mathrm{fairTape}\left(\{tape\in Tape\mid (\exists n:\mathbb{N},\mathrm{sample}\left(m,f,\mathrm{initial}\left(m\right),tape\right)=\mathrm{some}\left((i,n)\right))\}\right)=\mathrm{ofReal}\left(p\left(i\right)\right))\wedge (\forall d:\mathbb{N},\mathrm{fairTape}\left(\{tape\in Tape\mid (\mathrm{sample}\left(m,f,\mathrm{initial}\left(m\right),tape\right)=none\vee (\exists i:\mathrm{Fin}\left(m\right),(\exists n:\mathbb{N},(\mathrm{sample}\left(m,f,\mathrm{initial}\left(m\right),tape\right)=\mathrm{some}\left((i,n)\right)\wedge d<n))))\}\right)=\mathrm{ofReal}\left(\frac{r\left(\mathrm{state}\left(gamma,d\right)\right)}{2^d}\right))\wedge ({\forall }^{\mathrm{ae}\left(fairTape\right)}tape:Tape,(\exists i:\mathrm{Fin}\left(m\right),(\exists n:\mathbb{N},\mathrm{sample}\left(m,f,\mathrm{initial}\left(m\right),tape\right)=\mathrm{some}\left((i,n)\right))))\wedge \mathrm{lintegral}\left(fairTape,\mathrm{bill}\left(m,f,\mathrm{initial}\left(m\right)\right)\right)=\mathrm{ofReal}\left(\mathrm{pathCost}\left(gamma\right)\right)\wedge \mathrm{pathCost}\left(gamma\right)=\mathrm{cost}\left(p\right)\wedge \mathrm{cost}\left(p\right)=(\mathrm{alpha}\left(m\right)\cdot \mathrm{anchorValue}\left(gamma\right)))))))))))$$

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

Source. Repository-derived.

Commentary.

For every m at least two, every legal stationary table whose positive anchor and path cost satisfy C=alpha(m) times the anchor has a finite slot machine. Its policy path gamma starts at the root, and p is the law obtained from that path’s fixed label digits. At every index on every tape, a returned scan label and charge agree with the machine control and invoice; a continuing scan slot agrees with the machine’s carry state and slot. Thus their first-return samples and total bills coincide even on exceptional divergent tapes. In the display, core(x) is the stored carry state and slot(x) is its natural slot; treeSample and treeBill denote the existing fixed-label tree sample and bill.

The active-control bound is m squared times (m-1) divided by two, with m additional absorbing output labels. The output law is rational, strictly positive and normalized, its minimum is the positive anchor, its label probabilities are the digit sums, and its stopping tail is r(d)/2 raised to d. It returns almost surely and every returned invoice equals the total bill. The expected bill equals the policy-path cost, the dyadic cost of p and alpha(m) times the anchor.

The finite stationary root orbit repeats a state. Equal tail digit streams at two distinct indices, together with the finite-prefix identity for ofDigits, give a rational expression for each probability. The statement gives no minimum-state claim or uniform bound on the number of bits read.

References

• Truth anchor: D5/S3/Arith/FibonacciAtomic/CarryGraphFiniteSampler.Active
• Truth anchor: D5/S3/Arith/FibonacciAtomic/CarryGraphFiniteSampler.bill
• Truth anchor: D5/S3/Arith/FibonacciAtomic/CarryGraphFiniteSampler.coupling
• Truth anchor: D5/S3/Arith/FibonacciAtomic/CarryGraphFiniteSampler.execute
• Truth anchor: D5/S3/Arith/FibonacciAtomic/CarryGraphFiniteSampler.initial
• Truth anchor: D5/S3/Arith/FibonacciAtomic/CarryGraphFiniteSampler.policyPath
• Truth anchor: D5/S3/Arith/FibonacciAtomic/CarryGraphFiniteSampler.result
• Truth anchor: D5/S3/Arith/FibonacciAtomic/CarryGraphFiniteSampler.sample
• Truth anchor: D5/S3/Arith/FibonacciAtomic/CarryGraphFiniteSampler.step
• Dependency: D5/S3/Arith/FibonacciAtomic/CarryGraphRealization
• Dependency: D5/S3/Arith/FibonacciAtomic/OptimalLawStrictSlope