SequenceCoefficients

Abstract

Dyadic coefficient recurrences control the sixfold evil and odious representation counts.

Definition 1.1 (r).

$$\forall (jn:\mathbb{N}),rjn=((\mathrm{Finset}.\mathrm{Nat}.\mathrm{antidiagonalTuple}jn).\mathrm{filter}(\mathrm{fun}(x:\mathrm{Fin}j\to \mathbb{N})\mapsto \forall (i:\mathrm{Fin}j),\mathrm{thueMorse}(xi)=\mathrm{false})).\mathrm{card}$$

Formalization. D5/S1/Words/EvilOdious/SequenceCoefficients.r (✓ std3).

Citation. Jean-Paul Allouche and Jeffrey Shallit (2021). Additive properties of the evil and odious numbers and similar sequences. DOI: 10.7169/facm/2108. URL: https://arxiv.org/abs/2112.13627v3.

Commentary.

Equation (2), page 2: “rⱼ(n) := |{(x₁, x₂, …, xⱼ) : n = ∑₁≤ᵢ≤ⱼ xᵢ and tₓᵢ = 0 for 1 ≤ i ≤ j}|” The carrier Fin j indexes ordered natural coordinates; false encodes zero and true encodes one. Zero is included, and repetitions are allowed.

Definition 1.2 (s).

$$\forall (jn:\mathbb{N}),sjn=((\mathrm{Finset}.\mathrm{Nat}.\mathrm{antidiagonalTuple}jn).\mathrm{filter}(\mathrm{fun}(x:\mathrm{Fin}j\to \mathbb{N})\mapsto \forall (i:\mathrm{Fin}j),\mathrm{thueMorse}(xi)=\mathrm{true})).\mathrm{card}$$

Formalization. D5/S1/Words/EvilOdious/SequenceCoefficients.s (✓ std3).

Citation. Jean-Paul Allouche and Jeffrey Shallit (2021). Additive properties of the evil and odious numbers and similar sequences. DOI: 10.7169/facm/2108. URL: https://arxiv.org/abs/2112.13627v3.

Commentary.

Equation (3), page 2: “sⱼ(n) := |{(x₁, x₂, …, xⱼ) : n = ∑₁≤ᵢ≤ⱼ xᵢ and tₓᵢ = 1 for 1 ≤ i ≤ j}|,” The carrier Fin j indexes ordered natural coordinates; false encodes zero and true encodes one. Zero is included, and repetitions are allowed.

Definition 1.3 (recur).

$$\forall (q:\mathrm{List}\mathbb{Z}),(\mathrm{recur}q0=1)\wedge (\forall (n:\mathbb{N}),\mathrm{recur}q(n+1)=\sum _{k\in \mathrm{Finset}.\mathrm{range}q.\mathrm{length}}\mathrm{if}k\le n+1\wedge 2\mid n+1-k\mathrm{then}(\mathrm{List}.\mathrm{getD}qk0)\cdot \mathrm{recur}q((n+1-k)/2)\mathrm{else}0)$$

Formalization. D5/S1/Words/EvilOdious/SequenceCoefficients.recur (✓ std3).

Source. Repository-derived.

Acknowledgement. Jean-Paul Allouche and Jeffrey Shallit (2021). Additive properties of the evil and odious numbers and similar sequences. DOI: 10.7169/facm/2108. URL: https://arxiv.org/abs/2112.13627v3.

Commentary.

The formula uses the indicated natural or integer carriers. Natural subtraction is truncated; a slash between natural numbers denotes floor division, Nat.div. Dotted operations and the displayed casts retain their Lean meanings.

Definition 1.4 (zrecur).

$$\forall (p:\mathrm{List}\mathbb{Z}),\forall (n:\mathbb{Z}),\mathrm{zrecur}pn=\mathrm{if}0\le n\mathrm{then}\mathrm{recur}pn.\mathrm{toNat}\mathrm{else}0$$

Formalization. D5/S1/Words/EvilOdious/SequenceCoefficients.zrecur (✓ std3).

Source. Repository-derived.

Acknowledgement. Jean-Paul Allouche and Jeffrey Shallit (2021). Additive properties of the evil and odious numbers and similar sequences. DOI: 10.7169/facm/2108. URL: https://arxiv.org/abs/2112.13627v3.

Commentary.

The formula uses the indicated natural or integer carriers. Natural subtraction is truncated; a slash between natural numbers denotes floor division, Nat.div. Dotted operations and the displayed casts retain their Lean meanings.

Definition 1.5 (p).

$$p1=[1,3,2,-2,-3,-1]\wedge p2=[1,1,-2,-2,1,1]\wedge p3=[1,-1,-2,2,1,-1]\wedge p4=[1,-3,2,2,-3,1]\wedge p5=[1,-5,10,-10,5,-1]\wedge (\forall (j:\mathbb{N}),(j=0\vee 6\le j)\to pj=[1,-6,15,-20,15,-6,1])$$

Formalization. D5/S1/Words/EvilOdious/SequenceCoefficients.p (✓ std3).

Source. Repository-derived.

Acknowledgement. Jean-Paul Allouche and Jeffrey Shallit (2021). Additive properties of the evil and odious numbers and similar sequences. DOI: 10.7169/facm/2108. URL: https://arxiv.org/abs/2112.13627v3.

Commentary.

The formula uses the indicated natural or integer carriers. Natural subtraction is truncated; a slash between natural numbers denotes floor division, Nat.div. Dotted operations and the displayed casts retain their Lean meanings.

Definition 1.6 (errorTerm).

$$\forall (\mathrm{sigma}:\mathbb{Z}),\forall (n:\mathbb{N}),\mathrm{errorTerm}\mathrm{sigma}n=(\sum _{j\in \mathrm{Finset}.\mathrm{Icc}15}{\mathrm{sigma}}^j\cdot (\mathrm{Nat}.\mathrm{choose}6j:\mathbb{Z})\cdot (\mathrm{recur}(pj)n))+(\mathrm{recur}(p6)n)-(\mathrm{recur}(p6)(n-1))$$

Formalization. D5/S1/Words/EvilOdious/SequenceCoefficients.errorTerm (✓ std3).

Source. Repository-derived.

Acknowledgement. Jean-Paul Allouche and Jeffrey Shallit (2021). Additive properties of the evil and odious numbers and similar sequences. DOI: 10.7169/facm/2108. URL: https://arxiv.org/abs/2112.13627v3.

Commentary.

The formula uses the indicated natural or integer carriers. Natural subtraction is truncated; a slash between natural numbers denotes floor division, Nat.div. Dotted operations and the displayed casts retain their Lean meanings.

Theorem 1.7 (r difference).

$$\forall (n:\mathbb{N}),1\le n\to 64\cdot ((r6n:\mathbb{Z})-(r6(n-1):\mathbb{Z}))=((n+4).\mathrm{choose}4:\mathbb{Z})+\mathrm{errorTerm}1n$$

Proof. Machine-checked in Lean as D5/S1/Words/EvilOdious/SequenceCoefficients.r_difference (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Jean-Paul Allouche and Jeffrey Shallit (2021). Additive properties of the evil and odious numbers and similar sequences. DOI: 10.7169/facm/2108. URL: https://arxiv.org/abs/2112.13627v3.

Commentary.

The formula uses the indicated natural or integer carriers. Natural subtraction is truncated; a slash between natural numbers denotes floor division, Nat.div. Dotted operations and the displayed casts retain their Lean meanings.

Theorem 1.8 (s difference).

$$\forall (n:\mathbb{N}),1\le n\to 64\cdot ((s6n:\mathbb{Z})-(s6(n-1):\mathbb{Z}))=((n+4).\mathrm{choose}4:\mathbb{Z})+\mathrm{errorTerm}(-1)n$$

Proof. Machine-checked in Lean as D5/S1/Words/EvilOdious/SequenceCoefficients.s_difference (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Jean-Paul Allouche and Jeffrey Shallit (2021). Additive properties of the evil and odious numbers and similar sequences. DOI: 10.7169/facm/2108. URL: https://arxiv.org/abs/2112.13627v3.

Commentary.

The formula uses the indicated natural or integer carriers. Natural subtraction is truncated; a slash between natural numbers denotes floor division, Nat.div. Dotted operations and the displayed casts retain their Lean meanings.

Definition 1.9 (matrixBound).

$$\forall (d:\mathbb{N})(A:\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{Z})(B:\mathbb{N}),\mathrm{matrixBound}AB⟺\forall (i:\mathrm{Fin}d),\sum _{j:\mathrm{Fin}d}(Aij).\mathrm{natAbs}\le B$$

Formalization. D5/S1/Words/EvilOdious/SequenceCoefficients.matrixBound (✓ std3).

Source. Repository-derived.

Acknowledgement. Jean-Paul Allouche and Jeffrey Shallit (2021). Additive properties of the evil and odious numbers and similar sequences. DOI: 10.7169/facm/2108. URL: https://arxiv.org/abs/2112.13627v3.

Commentary.

The formula uses the indicated natural or integer carriers. Natural subtraction is truncated; a slash between natural numbers denotes floor division, Nat.div. Dotted operations and the displayed casts retain their Lean meanings.

Definition 1.10 (vectorBound).

$$\forall (d:\mathbb{N})(v:\mathrm{Fin}d\to \mathbb{Z})(B:\mathbb{N}),\mathrm{vectorBound}vB⟺\forall (i:\mathrm{Fin}d),(vi).\mathrm{natAbs}\le B$$

Formalization. D5/S1/Words/EvilOdious/SequenceCoefficients.vectorBound (✓ std3).

Source. Repository-derived.

Acknowledgement. Jean-Paul Allouche and Jeffrey Shallit (2021). Additive properties of the evil and odious numbers and similar sequences. DOI: 10.7169/facm/2108. URL: https://arxiv.org/abs/2112.13627v3.

Commentary.

The formula uses the indicated natural or integer carriers. Natural subtraction is truncated; a slash between natural numbers denotes floor division, Nat.div. Dotted operations and the displayed casts retain their Lean meanings.

Theorem 1.11 (matrix apply bound).

$$\forall (d:\mathbb{N}),\forall (A:\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{Z}),\forall (v:\mathrm{Fin}d\to \mathbb{Z}),\forall (BK:\mathbb{N}),(\mathrm{matrixBound}AB)\to (\mathrm{vectorBound}vK)\to \mathrm{vectorBound}(A.\mathrm{mulVec}v)(B\cdot K)$$

Proof. Machine-checked in Lean as D5/S1/Words/EvilOdious/SequenceCoefficients.matrix_apply_bound (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Jean-Paul Allouche and Jeffrey Shallit (2021). Additive properties of the evil and odious numbers and similar sequences. DOI: 10.7169/facm/2108. URL: https://arxiv.org/abs/2112.13627v3.

Commentary.

The formula uses the indicated natural or integer carriers. Natural subtraction is truncated; a slash between natural numbers denotes floor division, Nat.div. Dotted operations and the displayed casts retain their Lean meanings.

Definition 1.12 (pz).

$$\forall (p:\mathrm{List}\mathbb{Z}),\forall (k:\mathbb{Z}),\mathrm{pz}pk=\mathrm{if}0\le k\mathrm{then}(\mathrm{List}.\mathrm{getD}pk.\mathrm{toNat}0)\mathrm{else}0$$

Formalization. D5/S1/Words/EvilOdious/SequenceCoefficients.pz (✓ std3).

Source. Repository-derived.

Acknowledgement. Jean-Paul Allouche and Jeffrey Shallit (2021). Additive properties of the evil and odious numbers and similar sequences. DOI: 10.7169/facm/2108. URL: https://arxiv.org/abs/2112.13627v3.

Commentary.

The formula uses the indicated natural or integer carriers. Natural subtraction is truncated; a slash between natural numbers denotes floor division, Nat.div. Dotted operations and the displayed casts retain their Lean meanings.

Definition 1.13 (stateMatrix).

$$\forall (d:\mathbb{N})(p:\mathrm{List}\mathbb{Z})(b:\mathrm{Bool}),\mathrm{stateMatrix}dpb=\mathrm{fun}(ia:\mathrm{Fin}d)\mapsto \mathrm{pz}p(2\cdot (a:\mathbb{Z})+(\mathrm{if}b\mathrm{then}1\mathrm{else}0)-(i:\mathbb{Z}))$$

Formalization. D5/S1/Words/EvilOdious/SequenceCoefficients.stateMatrix (✓ std3).

Source. Repository-derived.

Acknowledgement. Jean-Paul Allouche and Jeffrey Shallit (2021). Additive properties of the evil and odious numbers and similar sequences. DOI: 10.7169/facm/2108. URL: https://arxiv.org/abs/2112.13627v3.

Commentary.

The formula uses the indicated natural or integer carriers. Natural subtraction is truncated; a slash between natural numbers denotes floor division, Nat.div. Dotted operations and the displayed casts retain their Lean meanings.

Definition 1.14 (words).

$$\forall (n:\mathbb{N}),\mathrm{words}n=(\mathrm{List}.\mathrm{replicate}n[\mathrm{false},\mathrm{true}]).\mathrm{sections}$$

Formalization. D5/S1/Words/EvilOdious/SequenceCoefficients.words (✓ std3).

Source. Repository-derived.

Acknowledgement. Jean-Paul Allouche and Jeffrey Shallit (2021). Additive properties of the evil and odious numbers and similar sequences. DOI: 10.7169/facm/2108. URL: https://arxiv.org/abs/2112.13627v3.

Commentary.

The formula uses the indicated natural or integer carriers. Natural subtraction is truncated; a slash between natural numbers denotes floor division, Nat.div. Dotted operations and the displayed casts retain their Lean meanings.

Definition 1.15 (wordMatrix).

$$\forall (d:\mathbb{N})(M:\mathrm{Bool}\to \mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{Z})(w:\mathrm{List}\mathrm{Bool}),\mathrm{wordMatrix}Mw=(w.\mathrm{map}M).\mathrm{prod}$$

Formalization. D5/S1/Words/EvilOdious/SequenceCoefficients.wordMatrix (✓ std3).

Source. Repository-derived.

Acknowledgement. Jean-Paul Allouche and Jeffrey Shallit (2021). Additive properties of the evil and odious numbers and similar sequences. DOI: 10.7169/facm/2108. URL: https://arxiv.org/abs/2112.13627v3.

Commentary.

The formula uses the indicated natural or integer carriers. Natural subtraction is truncated; a slash between natural numbers denotes floor division, Nat.div. Dotted operations and the displayed casts retain their Lean meanings.

Theorem 1.16 (h matrix bound).

$$\mathrm{matrixBound}(\mathrm{stateMatrix}5(p1)\mathrm{false})6\wedge \mathrm{matrixBound}(\mathrm{stateMatrix}5(p1)\mathrm{true})6\wedge \mathrm{matrixBound}(\mathrm{stateMatrix}5(p2)\mathrm{false})4\wedge \mathrm{matrixBound}(\mathrm{stateMatrix}5(p2)\mathrm{true})4\wedge \mathrm{matrixBound}(\mathrm{stateMatrix}5(p3)\mathrm{false})4\wedge \mathrm{matrixBound}(\mathrm{stateMatrix}5(p3)\mathrm{true})4\wedge \mathrm{matrixBound}(\mathrm{stateMatrix}5(p4)\mathrm{false})6\wedge \mathrm{matrixBound}(\mathrm{stateMatrix}5(p4)\mathrm{true})6\wedge \mathrm{matrixBound}(\mathrm{stateMatrix}5(p5)\mathrm{false})16\wedge \mathrm{matrixBound}(\mathrm{stateMatrix}5(p5)\mathrm{true})16$$

Proof. Machine-checked in Lean as D5/S1/Words/EvilOdious/SequenceCoefficients.h_matrix_bound (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Jean-Paul Allouche and Jeffrey Shallit (2021). Additive properties of the evil and odious numbers and similar sequences. DOI: 10.7169/facm/2108. URL: https://arxiv.org/abs/2112.13627v3.

Commentary.

The formula uses the indicated natural or integer carriers. Natural subtraction is truncated; a slash between natural numbers denotes floor division, Nat.div. Dotted operations and the displayed casts retain their Lean meanings.

Definition 1.17 (wordsCheck).

$$\forall (\mathrm{len}\mathrm{bound}:\mathbb{N}),\mathrm{wordsCheck}\mathrm{len}\mathrm{bound}=(\mathrm{words}\mathrm{len}).\mathrm{all}(\mathrm{fun}w\mapsto \mathrm{decide}(\mathrm{matrixBound}(\mathrm{wordMatrix}(\mathrm{stateMatrix}6(p6))w)\mathrm{bound}))$$

Formalization. D5/S1/Words/EvilOdious/SequenceCoefficients.wordsCheck (✓ std3).

Source. Repository-derived.

Acknowledgement. Jean-Paul Allouche and Jeffrey Shallit (2021). Additive properties of the evil and odious numbers and similar sequences. DOI: 10.7169/facm/2108. URL: https://arxiv.org/abs/2112.13627v3.

Commentary.

The formula uses the indicated natural or integer carriers. Natural subtraction is truncated; a slash between natural numbers denotes floor division, Nat.div. Dotted operations and the displayed casts retain their Lean meanings.

Theorem 1.18 (c five checked).

$$\mathrm{wordsCheck}51019200=\mathrm{true}$$

Proof. Machine-checked in Lean as D5/S1/Words/EvilOdious/SequenceCoefficients.c_five_checked (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Jean-Paul Allouche and Jeffrey Shallit (2021). Additive properties of the evil and odious numbers and similar sequences. DOI: 10.7169/facm/2108. URL: https://arxiv.org/abs/2112.13627v3.

Commentary.

The formula uses the indicated natural or integer carriers. Natural subtraction is truncated; a slash between natural numbers denotes floor division, Nat.div. Dotted operations and the displayed casts retain their Lean meanings.

Theorem 1.19 (c word bound).

$$\forall (w:\mathrm{List}\mathrm{Bool}),\mathrm{matrixBound}(\mathrm{wordMatrix}(\mathrm{stateMatrix}6(p6))w)(2\cdot 16^{w.\mathrm{length}})$$

Proof. Machine-checked in Lean as D5/S1/Words/EvilOdious/SequenceCoefficients.c_word_bound (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Jean-Paul Allouche and Jeffrey Shallit (2021). Additive properties of the evil and odious numbers and similar sequences. DOI: 10.7169/facm/2108. URL: https://arxiv.org/abs/2112.13627v3.

Commentary.

The formula uses the indicated natural or integer carriers. Natural subtraction is truncated; a slash between natural numbers denotes floor division, Nat.div. Dotted operations and the displayed casts retain their Lean meanings.

Definition 1.20 (state).

$$\forall (d:\mathbb{N})(q:\mathrm{List}\mathbb{Z})(n:\mathbb{N}),\mathrm{state}dqn=\mathrm{fun}(i:\mathrm{Fin}d)\mapsto \mathrm{recur}q(n-(i:\mathbb{N}))$$

Formalization. D5/S1/Words/EvilOdious/SequenceCoefficients.state (✓ std3).

Source. Repository-derived.

Acknowledgement. Jean-Paul Allouche and Jeffrey Shallit (2021). Additive properties of the evil and odious numbers and similar sequences. DOI: 10.7169/facm/2108. URL: https://arxiv.org/abs/2112.13627v3.

Commentary.

The formula uses the indicated natural or integer carriers. Natural subtraction is truncated; a slash between natural numbers denotes floor division, Nat.div. Dotted operations and the displayed casts retain their Lean meanings.

Theorem 1.21 (recur pos).

$$\forall (q:\mathrm{List}\mathbb{Z}),\forall (N:\mathbb{N}),(0<N)\to \mathrm{recur}qN=\sum _{k\in \mathrm{Finset}.\mathrm{range}q.\mathrm{length}}\mathrm{if}k\le N\wedge 2\mid N-k\mathrm{then}(\mathrm{List}.\mathrm{getD}qk0)\cdot \mathrm{recur}q((N-k)/2)\mathrm{else}0$$

Proof. Machine-checked in Lean as D5/S1/Words/EvilOdious/SequenceCoefficients.recur_pos (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Jean-Paul Allouche and Jeffrey Shallit (2021). Additive properties of the evil and odious numbers and similar sequences. DOI: 10.7169/facm/2108. URL: https://arxiv.org/abs/2112.13627v3.

Commentary.

The formula uses the indicated natural or integer carriers. Natural subtraction is truncated; a slash between natural numbers denotes floor division, Nat.div. Dotted operations and the displayed casts retain their Lean meanings.

Definition 1.22 (stateZ).

$$\forall (d:\mathbb{N})(q:\mathrm{List}\mathbb{Z})(n:\mathbb{N}),\mathrm{stateZ}dqn=\mathrm{fun}(i:\mathrm{Fin}d)\mapsto \mathrm{zrecur}q((n:\mathbb{Z})-((i:\mathbb{N}):\mathbb{Z}))$$

Formalization. D5/S1/Words/EvilOdious/SequenceCoefficients.stateZ (✓ std3).

Source. Repository-derived.

Acknowledgement. Jean-Paul Allouche and Jeffrey Shallit (2021). Additive properties of the evil and odious numbers and similar sequences. DOI: 10.7169/facm/2108. URL: https://arxiv.org/abs/2112.13627v3.

Commentary.

The formula uses the indicated natural or integer carriers. Natural subtraction is truncated; a slash between natural numbers denotes floor division, Nat.div. Dotted operations and the displayed casts retain their Lean meanings.

Theorem 1.23 (stateZ eq state).

$$\forall (d:\mathbb{N}),(d\le 6)\to \forall (q:\mathrm{List}\mathbb{Z}),\forall (n:\mathbb{N}),(6\le n)\to \mathrm{stateZ}dqn=\mathrm{state}dqn$$

Proof. Machine-checked in Lean as D5/S1/Words/EvilOdious/SequenceCoefficients.stateZ_eq_state (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Jean-Paul Allouche and Jeffrey Shallit (2021). Additive properties of the evil and odious numbers and similar sequences. DOI: 10.7169/facm/2108. URL: https://arxiv.org/abs/2112.13627v3.

Commentary.

The formula uses the indicated natural or integer carriers. Natural subtraction is truncated; a slash between natural numbers denotes floor division, Nat.div. Dotted operations and the displayed casts retain their Lean meanings.

Theorem 1.24 (stateZ step 1).

$$\forall (n:\mathbb{N}),\forall (b:\mathrm{Bool}),\mathrm{stateZ}5(p1)(2\cdot n+(\mathrm{if}b\mathrm{then}1\mathrm{else}0))=(\mathrm{stateMatrix}5(p1)b).\mathrm{mulVec}(\mathrm{stateZ}5(p1)n)$$

Proof. Machine-checked in Lean as D5/S1/Words/EvilOdious/SequenceCoefficients.stateZ_step_1 (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Jean-Paul Allouche and Jeffrey Shallit (2021). Additive properties of the evil and odious numbers and similar sequences. DOI: 10.7169/facm/2108. URL: https://arxiv.org/abs/2112.13627v3.

Commentary.

The formula uses the indicated natural or integer carriers. Natural subtraction is truncated; a slash between natural numbers denotes floor division, Nat.div. Dotted operations and the displayed casts retain their Lean meanings.

Theorem 1.25 (stateZ step 2).

$$\forall (n:\mathbb{N}),\forall (b:\mathrm{Bool}),\mathrm{stateZ}5(p2)(2\cdot n+(\mathrm{if}b\mathrm{then}1\mathrm{else}0))=(\mathrm{stateMatrix}5(p2)b).\mathrm{mulVec}(\mathrm{stateZ}5(p2)n)$$

Proof. Machine-checked in Lean as D5/S1/Words/EvilOdious/SequenceCoefficients.stateZ_step_2 (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Jean-Paul Allouche and Jeffrey Shallit (2021). Additive properties of the evil and odious numbers and similar sequences. DOI: 10.7169/facm/2108. URL: https://arxiv.org/abs/2112.13627v3.

Commentary.

The formula uses the indicated natural or integer carriers. Natural subtraction is truncated; a slash between natural numbers denotes floor division, Nat.div. Dotted operations and the displayed casts retain their Lean meanings.

Theorem 1.26 (stateZ step 3).

$$\forall (n:\mathbb{N}),\forall (b:\mathrm{Bool}),\mathrm{stateZ}5(p3)(2\cdot n+(\mathrm{if}b\mathrm{then}1\mathrm{else}0))=(\mathrm{stateMatrix}5(p3)b).\mathrm{mulVec}(\mathrm{stateZ}5(p3)n)$$

Proof. Machine-checked in Lean as D5/S1/Words/EvilOdious/SequenceCoefficients.stateZ_step_3 (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Jean-Paul Allouche and Jeffrey Shallit (2021). Additive properties of the evil and odious numbers and similar sequences. DOI: 10.7169/facm/2108. URL: https://arxiv.org/abs/2112.13627v3.

Commentary.

The formula uses the indicated natural or integer carriers. Natural subtraction is truncated; a slash between natural numbers denotes floor division, Nat.div. Dotted operations and the displayed casts retain their Lean meanings.

Definition 1.27 (appendValue).

$$\forall (q:\mathbb{N})(w:\mathrm{List}\mathrm{Bool}),\mathrm{appendValue}qw=\mathrm{Nat}.\mathrm{ofDigits}2(\mathrm{List}.\mathrm{append}(\mathrm{List}.\mathrm{map}\mathrm{Bool}.\mathrm{toNat}w)[q])$$

Formalization. D5/S1/Words/EvilOdious/SequenceCoefficients.appendValue (✓ std3).

Source. Repository-derived.

Acknowledgement. Jean-Paul Allouche and Jeffrey Shallit (2021). Additive properties of the evil and odious numbers and similar sequences. DOI: 10.7169/facm/2108. URL: https://arxiv.org/abs/2112.13627v3.

Commentary.

The formula uses the indicated natural or integer carriers. Natural subtraction is truncated; a slash between natural numbers denotes floor division, Nat.div. Dotted operations and the displayed casts retain their Lean meanings.

Theorem 1.28 (state word).

$$\forall (d:\mathbb{N})(q:\mathrm{List}\mathbb{Z})(M:\mathrm{Bool}\to \mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{Z}),(\forall (n:\mathbb{N})(b:\mathrm{Bool}),\mathrm{stateZ}dq(2\cdot n+(\mathrm{if}b\mathrm{then}1\mathrm{else}0))=(Mb).\mathrm{mulVec}(\mathrm{stateZ}dqn))\to \forall (p:\mathbb{N})(w:\mathrm{List}\mathrm{Bool}),\mathrm{stateZ}dq(\mathrm{appendValue}pw)=(\mathrm{wordMatrix}Mw).\mathrm{mulVec}(\mathrm{stateZ}dqp)$$

Proof. Machine-checked in Lean as D5/S1/Words/EvilOdious/SequenceCoefficients.state_word (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Jean-Paul Allouche and Jeffrey Shallit (2021). Additive properties of the evil and odious numbers and similar sequences. DOI: 10.7169/facm/2108. URL: https://arxiv.org/abs/2112.13627v3.

Commentary.

Induction on the binary word composes each one-bit state transition into its matrix product.

Theorem 1.29 (vector prefix bound).

$$\forall (d:\mathbb{N})(q:\mathrm{List}\mathbb{Z})(M:\mathrm{Bool}\to \mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{Z}),(\forall (n:\mathbb{N})(b:\mathrm{Bool}),\mathrm{stateZ}dq(2\cdot n+(\mathrm{if}b\mathrm{then}1\mathrm{else}0))=(Mb).\mathrm{mulVec}(\mathrm{stateZ}dqn))\to \forall (K:\mathbb{N}),(\forall (w:\mathrm{List}\mathrm{Bool}),\mathrm{matrixBound}(\mathrm{wordMatrix}Mw)(K\cdot 16^{w.\mathrm{length}}))\to \forall (p:\mathbb{N})(w:\mathrm{List}\mathrm{Bool})(B:\mathbb{N}),\mathrm{vectorBound}(\mathrm{stateZ}dqp)B\to \mathrm{vectorBound}(\mathrm{stateZ}dq(\mathrm{appendValue}pw))(K\cdot 16^{w.\mathrm{length}}\cdot B)$$

Proof. Machine-checked in Lean as D5/S1/Words/EvilOdious/SequenceCoefficients.vector_prefix_bound (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Jean-Paul Allouche and Jeffrey Shallit (2021). Additive properties of the evil and odious numbers and similar sequences. DOI: 10.7169/facm/2108. URL: https://arxiv.org/abs/2112.13627v3.

Commentary.

The matrix-word bound transfers the seed bound to every word extension.

Theorem 1.30 (appendValue decompose).

$$\forall (p0:\mathbb{N}),\forall (w:\mathrm{List}\mathrm{Bool}),\mathrm{appendValue}p0w=p0\cdot 2^{w.\mathrm{length}}+\mathrm{appendValue}0w$$

Proof. Machine-checked in Lean as D5/S1/Words/EvilOdious/SequenceCoefficients.appendValue_decompose (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Jean-Paul Allouche and Jeffrey Shallit (2021). Additive properties of the evil and odious numbers and similar sequences. DOI: 10.7169/facm/2108. URL: https://arxiv.org/abs/2112.13627v3.

Commentary.

The formula uses the indicated natural or integer carriers. Natural subtraction is truncated; a slash between natural numbers denotes floor division, Nat.div. Dotted operations and the displayed casts retain their Lean meanings.

Theorem 1.31 (stateZ step 4).

$$\forall (n:\mathbb{N}),\forall (b:\mathrm{Bool}),\mathrm{stateZ}5(p4)(2\cdot n+(\mathrm{if}b\mathrm{then}1\mathrm{else}0))=(\mathrm{stateMatrix}5(p4)b).\mathrm{mulVec}(\mathrm{stateZ}5(p4)n)$$

Proof. Machine-checked in Lean as D5/S1/Words/EvilOdious/SequenceCoefficients.stateZ_step_4 (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Jean-Paul Allouche and Jeffrey Shallit (2021). Additive properties of the evil and odious numbers and similar sequences. DOI: 10.7169/facm/2108. URL: https://arxiv.org/abs/2112.13627v3.

Commentary.

The formula uses the indicated natural or integer carriers. Natural subtraction is truncated; a slash between natural numbers denotes floor division, Nat.div. Dotted operations and the displayed casts retain their Lean meanings.

Theorem 1.32 (stateZ step 5).

$$\forall (n:\mathbb{N}),\forall (b:\mathrm{Bool}),\mathrm{stateZ}5(p5)(2\cdot n+(\mathrm{if}b\mathrm{then}1\mathrm{else}0))=(\mathrm{stateMatrix}5(p5)b).\mathrm{mulVec}(\mathrm{stateZ}5(p5)n)$$

Proof. Machine-checked in Lean as D5/S1/Words/EvilOdious/SequenceCoefficients.stateZ_step_5 (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Jean-Paul Allouche and Jeffrey Shallit (2021). Additive properties of the evil and odious numbers and similar sequences. DOI: 10.7169/facm/2108. URL: https://arxiv.org/abs/2112.13627v3.

Commentary.

The formula uses the indicated natural or integer carriers. Natural subtraction is truncated; a slash between natural numbers denotes floor division, Nat.div. Dotted operations and the displayed casts retain their Lean meanings.

Theorem 1.33 (stateZ step 6).

$$\forall (n:\mathbb{N}),\forall (b:\mathrm{Bool}),\mathrm{stateZ}6(p6)(2\cdot n+(\mathrm{if}b\mathrm{then}1\mathrm{else}0))=(\mathrm{stateMatrix}6(p6)b).\mathrm{mulVec}(\mathrm{stateZ}6(p6)n)$$

Proof. Machine-checked in Lean as D5/S1/Words/EvilOdious/SequenceCoefficients.stateZ_step_6 (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Jean-Paul Allouche and Jeffrey Shallit (2021). Additive properties of the evil and odious numbers and similar sequences. DOI: 10.7169/facm/2108. URL: https://arxiv.org/abs/2112.13627v3.

Commentary.

The formula uses the indicated natural or integer carriers. Natural subtraction is truncated; a slash between natural numbers denotes floor division, Nat.div. Dotted operations and the displayed casts retain their Lean meanings.

Theorem 1.34 (lowWord bound).

$$\forall (w:\mathrm{List}\mathrm{Bool}),\mathrm{appendValue}0w<2^{w.\mathrm{length}}$$

Proof. Machine-checked in Lean as D5/S1/Words/EvilOdious/SequenceCoefficients.lowWord_bound (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Jean-Paul Allouche and Jeffrey Shallit (2021). Additive properties of the evil and odious numbers and similar sequences. DOI: 10.7169/facm/2108. URL: https://arxiv.org/abs/2112.13627v3.

Commentary.

The formula uses the indicated natural or integer carriers. Natural subtraction is truncated; a slash between natural numbers denotes floor division, Nat.div. Dotted operations and the displayed casts retain their Lean meanings.

Theorem 1.35 (word for low).

$$\forall (m\mathrm{low}:\mathbb{N}),\mathrm{low}<2^m\to \exists (w:\mathrm{List}\mathrm{Bool}),w.\mathrm{length}=m\wedge \mathrm{appendValue}0w=\mathrm{low}$$

Proof. Machine-checked in Lean as D5/S1/Words/EvilOdious/SequenceCoefficients.word_for_low (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Jean-Paul Allouche and Jeffrey Shallit (2021). Additive properties of the evil and odious numbers and similar sequences. DOI: 10.7169/facm/2108. URL: https://arxiv.org/abs/2112.13627v3.

Commentary.

Induction on the length constructs a binary word for every allowed low part, including leading zero bits.

Theorem 1.36 (state dyadic bound).

$$\forall (d:\mathbb{N})(q:\mathrm{List}\mathbb{Z})(M:\mathrm{Bool}\to \mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{Z}),(\forall (n:\mathbb{N})(b:\mathrm{Bool}),\mathrm{stateZ}dq(2\cdot n+(\mathrm{if}b\mathrm{then}1\mathrm{else}0))=(Mb).\mathrm{mulVec}(\mathrm{stateZ}dqn))\to \forall (K:\mathbb{N}),(\forall (w:\mathrm{List}\mathrm{Bool}),\mathrm{matrixBound}(\mathrm{wordMatrix}Mw)(K\cdot 16^{w.\mathrm{length}}))\to \forall (pm\mathrm{low}:\mathbb{N}),\mathrm{low}<2^m\to \mathrm{vectorBound}(\mathrm{stateZ}dq(p\cdot 2^m+\mathrm{low}))(K\cdot 16^m\cdot (\mathrm{Finset}.\mathrm{range}d).\sup (\mathrm{fun}(i:\mathbb{N})\mapsto (\mathrm{zrecur}q((p:\mathbb{Z})-(i:\mathbb{Z}))).\mathrm{natAbs}))$$

Proof. Machine-checked in Lean as D5/S1/Words/EvilOdious/SequenceCoefficients.state_dyadic_bound (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Jean-Paul Allouche and Jeffrey Shallit (2021). Additive properties of the evil and odious numbers and similar sequences. DOI: 10.7169/facm/2108. URL: https://arxiv.org/abs/2112.13627v3.

Commentary.

Binary-word construction and the matrix estimate bound every dyadic extension by the largest seed coordinate.

References

• Truth anchor: D5/S1/Words/EvilOdious/SequenceCoefficients.appendValue
• Truth anchor: D5/S1/Words/EvilOdious/SequenceCoefficients.appendValue_decompose
• Truth anchor: D5/S1/Words/EvilOdious/SequenceCoefficients.c_five_checked
• Truth anchor: D5/S1/Words/EvilOdious/SequenceCoefficients.c_word_bound
• Truth anchor: D5/S1/Words/EvilOdious/SequenceCoefficients.errorTerm
• Truth anchor: D5/S1/Words/EvilOdious/SequenceCoefficients.h_matrix_bound
• Truth anchor: D5/S1/Words/EvilOdious/SequenceCoefficients.lowWord_bound
• Truth anchor: D5/S1/Words/EvilOdious/SequenceCoefficients.matrixBound
• Truth anchor: D5/S1/Words/EvilOdious/SequenceCoefficients.matrix_apply_bound
• Truth anchor: D5/S1/Words/EvilOdious/SequenceCoefficients.p
• Truth anchor: D5/S1/Words/EvilOdious/SequenceCoefficients.pz
• Truth anchor: D5/S1/Words/EvilOdious/SequenceCoefficients.r
• Truth anchor: D5/S1/Words/EvilOdious/SequenceCoefficients.r_difference
• Truth anchor: D5/S1/Words/EvilOdious/SequenceCoefficients.recur
• Truth anchor: D5/S1/Words/EvilOdious/SequenceCoefficients.recur_pos
• Truth anchor: D5/S1/Words/EvilOdious/SequenceCoefficients.s
• Truth anchor: D5/S1/Words/EvilOdious/SequenceCoefficients.s_difference
• Truth anchor: D5/S1/Words/EvilOdious/SequenceCoefficients.state
• Truth anchor: D5/S1/Words/EvilOdious/SequenceCoefficients.stateMatrix
• Truth anchor: D5/S1/Words/EvilOdious/SequenceCoefficients.stateZ
• Truth anchor: D5/S1/Words/EvilOdious/SequenceCoefficients.stateZ_eq_state
• Truth anchor: D5/S1/Words/EvilOdious/SequenceCoefficients.stateZ_step_1
• Truth anchor: D5/S1/Words/EvilOdious/SequenceCoefficients.stateZ_step_2
• Truth anchor: D5/S1/Words/EvilOdious/SequenceCoefficients.stateZ_step_3
• Truth anchor: D5/S1/Words/EvilOdious/SequenceCoefficients.stateZ_step_4
• Truth anchor: D5/S1/Words/EvilOdious/SequenceCoefficients.stateZ_step_5
• Truth anchor: D5/S1/Words/EvilOdious/SequenceCoefficients.stateZ_step_6
• Truth anchor: D5/S1/Words/EvilOdious/SequenceCoefficients.state_dyadic_bound
• Truth anchor: D5/S1/Words/EvilOdious/SequenceCoefficients.state_word
• Truth anchor: D5/S1/Words/EvilOdious/SequenceCoefficients.vectorBound
• Truth anchor: D5/S1/Words/EvilOdious/SequenceCoefficients.vector_prefix_bound
• Truth anchor: D5/S1/Words/EvilOdious/SequenceCoefficients.wordMatrix
• Truth anchor: D5/S1/Words/EvilOdious/SequenceCoefficients.word_for_low
• Truth anchor: D5/S1/Words/EvilOdious/SequenceCoefficients.words
• Truth anchor: D5/S1/Words/EvilOdious/SequenceCoefficients.wordsCheck
• Truth anchor: D5/S1/Words/EvilOdious/SequenceCoefficients.zrecur
• Dependency: D5/S1/Words/Complexity/ThueMorseReducedAbelianOdd