Fixed-label Carry-tree Execution

Abstract

Fixed one-label intervals determine ordered children and an actual bit-by-bit scan.

Definition 1.1 (Output digits).

$$(\forall m:\mathbb{N},(\forall gamma:Path,(\forall i:\mathrm{Fin}\left(m\right),(\forall d:\mathbb{N},\mathrm{labelDigit}\left(gamma,i,d\right)=\mathrm{indicator}\left(\mathrm{labelSet}\left(m,gamma,d\right),i\right)))))$$

Formalization. D5/S3/Arith/FibonacciAtomic/CarryGraphRealization.labelDigit (✓ std3).

Source. Repository-derived.

Commentary.

Membership in the selected set gives digit one; every other label has digit zero.

Definition 1.2 (Charged scan).

$$(\forall m:\mathbb{N},(\forall gamma:Path,(\forall tape:Tape,(\forall d:\mathbb{N},\mathrm{scan}\left(m,gamma,tape,d\right)\in \mathrm{Sum}\left(\mathrm{Product}\left(\mathrm{Fin}\left(m\right),\mathbb{N}\right),\mathbb{N}\right)))))$$

Formalization. D5/S3/Arith/FibonacciAtomic/CarryGraphRealization.scan (✓ std3).

Source. Repository-derived.

Commentary.

The root is active slot zero. At depth d an active slot j reads tape(d), forms z=2j+toNat(tape(d)), and returns the z-th column label with charge d+1 if z is below the label count. Otherwise it continues in slot z minus that count. A returned state stays unchanged and reads no further bits.

Definition 1.3 (First return).

$$(\forall m:\mathbb{N},(\forall gamma:Path,(\forall tape:Tape,\mathrm{sample}\left(m,gamma,tape\right)=\mathrm{firstLeft}\left(\mathrm{scan}\left(m,gamma,tape\right)\right))))$$

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

Source. Repository-derived.

Commentary.

The sample is the first left scan state, with its output label and charged length. It is absent on tapes with no finite return.

Definition 1.4 (Total charged reads).

$$(\forall m:\mathbb{N},(\forall gamma:Path,(\forall tape:Tape,\mathrm{bill}\left(m,gamma,tape\right)=\sum _{d\in \mathbb{N}}\mathrm{indicator}\left(isRight,\mathrm{scan}\left(m,gamma,tape,d\right)\right))))$$

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

Source. Repository-derived.

Commentary.

The nonnegative extended-real sum counts one read for each active scan state. It is infinite on an execution that remains active forever.

Theorem 1.5 (Every root path has its actual fair-bit tree).

$$(\forall m:\mathbb{N},(2\le m\to (\forall gamma:Path,(\mathrm{IsRootPath}\left(m,gamma\right)\to ((\forall i:\mathrm{Fin}\left(m\right),0\le \mathrm{ofDigits}\left(\mathrm{labelDigit}\left(gamma,i\right)\right))\wedge \sum _{i\in \mathrm{Fin}\left(m\right)}\mathrm{ofDigits}\left(\mathrm{labelDigit}\left(gamma,i\right)\right)=1\wedge \mathrm{ofDigits}\left(\mathrm{labelDigit}\left(gamma,0\right)\right)=\mathrm{anchorValue}\left(gamma\right)\wedge (\forall i:\mathrm{Fin}\left(m\right),\mathrm{anchorValue}\left(gamma\right)\le \mathrm{ofDigits}\left(\mathrm{labelDigit}\left(gamma,i\right)\right))\wedge (0<\mathrm{anchorValue}\left(gamma\right)\to (\forall i:\mathrm{Fin}\left(m\right),0<\mathrm{ofDigits}\left(\mathrm{labelDigit}\left(gamma,i\right)\right)))\wedge \mathrm{IsPrefixFree}\left(\{w\in \mathrm{List}\left(Bool\right)\mid (\exists d:\mathbb{N},(\exists i:\mathrm{Fin}\left(m\right),(w,i)\in \mathrm{stopping}\left(m,gamma,d\right)))\}\right)\wedge (\forall d:\mathbb{N},(\mathrm{map}\left(snd,\mathrm{stopping}\left(m,gamma,d\right)\right)=\mathrm{sort}\left(\mathrm{labelSet}\left(m,gamma,d\right)\right)\wedge (\forall w:\mathrm{Product}\left(\mathrm{List}\left(Bool\right),\mathrm{Fin}\left(m\right)\right),(w\in \mathrm{stopping}\left(m,gamma,d\right)\to \mathrm{length}\left(\mathrm{fst}\left(w\right)\right)=d+1))))\wedge (\forall tape:Tape,(\forall i:\mathrm{Fin}\left(m\right),(\forall d:\mathbb{N},\mathrm{sample}\left(m,gamma,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,gamma,tape\right)=\mathrm{some}\left((i,n)\right)\to \mathrm{bill}\left(m,gamma,tape\right)=n))))\wedge (\forall i:\mathrm{Fin}\left(m\right),(\mathrm{MeasurableSet}\left(\{tape\in Tape\mid (\exists n:\mathbb{N},\mathrm{sample}\left(m,gamma,tape\right)=\mathrm{some}\left((i,n)\right))\}\right)\wedge \mathrm{fairTape}\left(\{tape\in Tape\mid (\exists n:\mathbb{N},\mathrm{sample}\left(m,gamma,tape\right)=\mathrm{some}\left((i,n)\right))\}\right)=\mathrm{ofReal}\left(\mathrm{ofDigits}\left(\mathrm{labelDigit}\left(gamma,i\right)\right)\right)))\wedge (\forall d:\mathbb{N},(\mathrm{MeasurableSet}\left(\{tape\in Tape\mid (\mathrm{sample}\left(m,gamma,tape\right)=none\vee (\exists i:\mathrm{Fin}\left(m\right),(\exists n:\mathbb{N},(\mathrm{sample}\left(m,gamma,tape\right)=\mathrm{some}\left((i,n)\right)\wedge d<n))))\}\right)\wedge \mathrm{fairTape}\left(\{tape\in Tape\mid (\mathrm{sample}\left(m,gamma,tape\right)=none\vee (\exists i:\mathrm{Fin}\left(m\right),(\exists n:\mathbb{N},(\mathrm{sample}\left(m,gamma,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,gamma,tape\right)=\mathrm{some}\left((i,n)\right))))\wedge \mathrm{lintegral}\left(fairTape,\mathrm{bill}\left(m,gamma\right)\right)=\mathrm{ofReal}\left(\mathrm{pathCost}\left(gamma\right)\right)\wedge \mathrm{pathCost}\left(gamma\right)\le m\wedge \mathrm{cost}\left((i:\mathrm{Fin}\left(m\right)\mapsto \mathrm{ofDigits}\left(\mathrm{labelDigit}\left(gamma,i\right)\right))\right)\le \mathrm{pathCost}\left(gamma\right)\wedge (\exists delta:Path,(\mathrm{IsRootPath}\left(2,delta\right)\wedge \mathrm{cost}\left((i:\mathrm{Fin}\left(2\right)\mapsto \mathrm{ofDigits}\left(\mathrm{labelDigit}\left(delta,i\right)\right))\right)<\mathrm{pathCost}\left(delta\right))))))))$$

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

Source. Repository-derived.

Commentary.

For every m at least two and every legal root path, the fixed digits give a nonnegative normalized law. Index zero is the minimum anchor and equals its digit series; a positive anchor makes every label positive.

The constructed stopping words are prefix-free and carry exactly the selected labels at each depth. The first-return sample outputs a label and length exactly when its tape prefix is that labelled leaf. Its bill is that length, so each consumed fair bit is charged once. Under the existing independent fair-tape measure its label law is the digit law, its stopping tail is r(d)/2^d, and it returns almost surely. The expected bill equals pathCost, is at most m, and dominates the existing dyadic cost. No canonical-expansion, rationality or computability hypothesis is added.

The inequality can be strict. For two labels, take the root action (b,h,c)=(0,1,0) and then repeat (1,0,0) at state (1,1). The output digits are 0.01111… and 0.10000…, so both probabilities are one half. The path cost is two while the dyadic cost of its law is one.

References

• Truth anchor: D5/S3/Arith/FibonacciAtomic/CarryGraphRealization.bill
• Truth anchor: D5/S3/Arith/FibonacciAtomic/CarryGraphRealization.labelDigit
• Truth anchor: D5/S3/Arith/FibonacciAtomic/CarryGraphRealization.result
• Truth anchor: D5/S3/Arith/FibonacciAtomic/CarryGraphRealization.sample
• Truth anchor: D5/S3/Arith/FibonacciAtomic/CarryGraphRealization.scan
• Dependency: D5/S0/Computability/Coding/PrefixFreeCode
• Dependency: D5/S0/Tower/DBonacci/TerminalSampling
• Dependency: D5/S3/Arith/FibonacciAtomic/CarryGraphEmbedding