CoefficientTableChecker

Abstract

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

Definition 1.1 (tableValue).

$$\forall (\mathrm{table}:\mathrm{BinaryTree}(\mathbb{N}\times \mathbb{Z}))(\mathrm{index}:\mathbb{N}),\mathrm{tableValue}\mathrm{table}\mathrm{index}=\mathrm{match}\mathrm{table}\mathrm{with}|\mathrm{BinaryTree}.\mathrm{nil}\mapsto 0|\mathrm{BinaryTree}.\mathrm{node}(\mathrm{key},\mathrm{value})\mathrm{left}\mathrm{right}\mapsto \mathrm{if}\mathrm{index}=\mathrm{key}\mathrm{then}\mathrm{value}\mathrm{else}\mathrm{if}\mathrm{index}<\mathrm{key}\mathrm{then}\mathrm{tableValue}\mathrm{left}\mathrm{index}\mathrm{else}\mathrm{tableValue}\mathrm{right}\mathrm{index}$$

Formalization. D5/S1/Words/EvilOdious/CoefficientTableChecker.tableValue (✓ 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.2 (tableStep).

$$\forall (q:\mathrm{List}\mathbb{Z}),\forall (v:\mathbb{N}\to \mathbb{Z}),\forall (n:\mathbb{N}),\mathrm{tableStep}qvn=\mathrm{if}n=0\mathrm{then}1\mathrm{else}\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 v((n-k)/2)\mathrm{else}0$$

Formalization. D5/S1/Words/EvilOdious/CoefficientTableChecker.tableStep (✓ 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.3 (tableCheck).

$$\forall (q:\mathrm{List}\mathbb{Z})(\mathrm{table}:\mathrm{BinaryTree}(\mathbb{N}\times \mathbb{Z}))(\mathrm{bound}:\mathbb{N}),\mathrm{tableCheck}q\mathrm{table}\mathrm{bound}=(\mathrm{List}.\mathrm{range}\mathrm{bound}).\mathrm{all}(\mathrm{fun}(n:\mathbb{N})\mapsto \mathrm{BEq}.\mathrm{beq}(\mathrm{tableValue}\mathrm{table}n)(\mathrm{tableStep}q(\mathrm{tableValue}\mathrm{table})n))$$

Formalization. D5/S1/Words/EvilOdious/CoefficientTableChecker.tableCheck (✓ 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.4 (tableCheck sound).

$$\forall (q:\mathrm{List}\mathbb{Z}),\forall (\mathrm{table}:\mathrm{BinaryTree}(\mathbb{N}\times \mathbb{Z})),\forall (\mathrm{bound}:\mathbb{N}),(\mathrm{tableCheck}q\mathrm{table}\mathrm{bound}=\mathrm{true})\to \forall n,n<\mathrm{bound}\to \mathrm{recur}qn=\mathrm{tableValue}\mathrm{table}n$$

Proof. Machine-checked in Lean as D5/S1/Words/EvilOdious/CoefficientTableChecker.tableCheck_sound (✓ 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 (table1).

$$table1:\mathrm{BinaryTree}(\mathbb{N}\times \mathbb{Z})$$

Formalization. D5/S1/Words/EvilOdious/CoefficientTableChecker.table1 (✓ 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 balanced binary tree stores 4096 exact integer entries for the polynomial system p 1. Its entries are checked against the recurrence by tableCheck_sound.

Theorem 1.6 (table1 checked).

$$\mathrm{tableCheck}(p1)table14096=\mathrm{true}$$

Proof. Machine-checked in Lean as D5/S1/Words/EvilOdious/CoefficientTableChecker.table1_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.7 (table1 sound).

$$\forall (n:\mathbb{N}),(n<4096)\to \mathrm{recur}(p1)n=(\mathrm{tableValue}table1)n$$

Proof. Machine-checked in Lean as D5/S1/Words/EvilOdious/CoefficientTableChecker.table1_sound (✓ 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.8 (table2).

$$table2:\mathrm{BinaryTree}(\mathbb{N}\times \mathbb{Z})$$

Formalization. D5/S1/Words/EvilOdious/CoefficientTableChecker.table2 (✓ 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 balanced binary tree stores 4096 exact integer entries for the polynomial system p 2. Its entries are checked against the recurrence by tableCheck_sound.

Theorem 1.9 (table2 sound).

$$\forall (n:\mathbb{N}),(n<4096)\to \mathrm{recur}(p2)n=(\mathrm{tableValue}table2)n$$

Proof. Machine-checked in Lean as D5/S1/Words/EvilOdious/CoefficientTableChecker.table2_sound (✓ 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 (table3).

$$table3:\mathrm{BinaryTree}(\mathbb{N}\times \mathbb{Z})$$

Formalization. D5/S1/Words/EvilOdious/CoefficientTableChecker.table3 (✓ 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 balanced binary tree stores 4096 exact integer entries for the polynomial system p 3. Its entries are checked against the recurrence by tableCheck_sound.

Theorem 1.11 (table3 sound).

$$\forall (n:\mathbb{N}),(n<4096)\to \mathrm{recur}(p3)n=(\mathrm{tableValue}table3)n$$

Proof. Machine-checked in Lean as D5/S1/Words/EvilOdious/CoefficientTableChecker.table3_sound (✓ 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 (table4).

$$table4:\mathrm{BinaryTree}(\mathbb{N}\times \mathbb{Z})$$

Formalization. D5/S1/Words/EvilOdious/CoefficientTableChecker.table4 (✓ 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 balanced binary tree stores 4096 exact integer entries for the polynomial system p 4. Its entries are checked against the recurrence by tableCheck_sound.

Theorem 1.13 (table4 sound).

$$\forall (n:\mathbb{N}),(n<4096)\to \mathrm{recur}(p4)n=(\mathrm{tableValue}table4)n$$

Proof. Machine-checked in Lean as D5/S1/Words/EvilOdious/CoefficientTableChecker.table4_sound (✓ 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 (table5).

$$table5:\mathrm{BinaryTree}(\mathbb{N}\times \mathbb{Z})$$

Formalization. D5/S1/Words/EvilOdious/CoefficientTableChecker.table5 (✓ 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 balanced binary tree stores 4096 exact integer entries for the polynomial system p 5. Its entries are checked against the recurrence by tableCheck_sound.

Theorem 1.15 (table5 sound).

$$\forall (n:\mathbb{N}),(n<4096)\to \mathrm{recur}(p5)n=(\mathrm{tableValue}table5)n$$

Proof. Machine-checked in Lean as D5/S1/Words/EvilOdious/CoefficientTableChecker.table5_sound (✓ 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.16 (table6).

$$table6:\mathrm{BinaryTree}(\mathbb{N}\times \mathbb{Z})$$

Formalization. D5/S1/Words/EvilOdious/CoefficientTableChecker.table6 (✓ 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 balanced binary tree stores 4096 exact integer entries for the polynomial system p 6. Its entries are checked against the recurrence by tableCheck_sound.

Theorem 1.17 (table6 sound).

$$\forall (n:\mathbb{N}),(n<4096)\to \mathrm{recur}(p6)n=(\mathrm{tableValue}table6)n$$

Proof. Machine-checked in Lean as D5/S1/Words/EvilOdious/CoefficientTableChecker.table6_sound (✓ 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.18 (tableH).

$$\forall (jn:\mathbb{N}),\mathrm{tableH}jn=\mathrm{if}j=1\mathrm{then}\mathrm{tableValue}table1n\mathrm{else}\mathrm{if}j=2\mathrm{then}\mathrm{tableValue}table2n\mathrm{else}\mathrm{if}j=3\mathrm{then}\mathrm{tableValue}table3n\mathrm{else}\mathrm{if}j=4\mathrm{then}\mathrm{tableValue}table4n\mathrm{else}\mathrm{tableValue}table5n$$

Formalization. D5/S1/Words/EvilOdious/CoefficientTableChecker.tableH (✓ 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.19 (tableError).

$$\forall (\mathrm{sigma}:\mathbb{Z}),\forall (n:\mathbb{N}),\mathrm{tableError}\mathrm{sigma}n=(\sum _{j\in \mathrm{Finset}.\mathrm{Icc}15}{\mathrm{sigma}}^j\cdot (\mathrm{Nat}.\mathrm{choose}6j:\mathbb{Z})\cdot \mathrm{tableH}jn)+(\mathrm{tableValue}table6)n-(\mathrm{tableValue}table6)(n-1)$$

Formalization. D5/S1/Words/EvilOdious/CoefficientTableChecker.tableError (✓ 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 (seedH).

$$\forall (jn:\mathbb{N}),\mathrm{seedH}jn=(\mathrm{Finset}.\mathrm{range}5).\sup (\mathrm{fun}i\mapsto (\mathrm{tableH}j(n-i)).\mathrm{natAbs})$$

Formalization. D5/S1/Words/EvilOdious/CoefficientTableChecker.seedH (✓ 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.21 (seedC).

$$\forall (n:\mathbb{N}),\mathrm{seedC}n=(\mathrm{Finset}.\mathrm{range}6).\sup (\mathrm{fun}i\mapsto ((\mathrm{tableValue}table6)(n-i)).\mathrm{natAbs})$$

Formalization. D5/S1/Words/EvilOdious/CoefficientTableChecker.seedC (✓ 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 (prefixB).

$$\forall (n:\mathbb{N}),\mathrm{prefixB}n=(\sum _{j\in \mathrm{Finset}.\mathrm{Icc}15}\mathrm{Nat}.\mathrm{choose}6j\cdot \mathrm{seedH}jn)+4\cdot \mathrm{seedC}n$$

Formalization. D5/S1/Words/EvilOdious/CoefficientTableChecker.prefixB (✓ 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 (tableH sound).

$$\forall (jn:\mathbb{N}),(j\in \mathrm{Finset}.\mathrm{Icc}15)\to (n<4096)\to (\mathrm{recur}(pj)n)=\mathrm{tableH}jn$$

Proof. Machine-checked in Lean as D5/S1/Words/EvilOdious/CoefficientTableChecker.tableH_sound (✓ 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 (tableError sound).

$$\forall (\mathrm{sigma}:\mathbb{Z}),\forall (n:\mathbb{N}),(n<4096)\to \mathrm{errorTerm}\mathrm{sigma}n=\mathrm{tableError}\mathrm{sigma}n$$

Proof. Machine-checked in Lean as D5/S1/Words/EvilOdious/CoefficientTableChecker.tableError_sound (✓ 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.25 (prefixChunk).

$$\forall (\mathrm{base}\mathrm{len}:\mathbb{N}),\mathrm{prefixChunk}\mathrm{base}\mathrm{len}=(\mathrm{List}.\mathrm{range}\mathrm{len}).\mathrm{all}(\mathrm{fun}k\mapsto \mathrm{decide}(24\cdot \mathrm{prefixB}(\mathrm{base}+k)<(\mathrm{base}+k{)}^4))$$

Formalization. D5/S1/Words/EvilOdious/CoefficientTableChecker.prefixChunk (✓ 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.26 (initialChunk).

$$\forall (\mathrm{sigma}:\mathbb{Z}),\forall (\mathrm{lower}\mathrm{base}\mathrm{len}:\mathbb{N}),\mathrm{initialChunk}\mathrm{sigma}\mathrm{lower}\mathrm{base}\mathrm{len}=(\mathrm{List}.\mathrm{range}\mathrm{len}).\mathrm{all}(\mathrm{fun}k\mapsto \mathrm{decide}(\mathrm{lower}\le \mathrm{base}+k\to 0<((\mathrm{Nat}.\mathrm{descFactorial}(\mathrm{base}+k+4)4/24:\mathbb{N}):\mathbb{Z})+\mathrm{tableError}\mathrm{sigma}(\mathrm{base}+k)))$$

Formalization. D5/S1/Words/EvilOdious/CoefficientTableChecker.initialChunk (✓ 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.27 (prefixcertificate 0).

$$\mathrm{prefixChunk}204832=\mathrm{true}$$

Proof. Machine-checked in Lean as D5/S1/Words/EvilOdious/CoefficientTableChecker.prefixcertificate_0 (✓ 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 (prefixcertificate checked).

$$\forall (\mathrm{block}:\mathrm{Fin}64),\mathrm{prefixChunk}(2048+32\cdot \mathrm{block}.\mathrm{val})32=\mathrm{true}$$

Proof. Machine-checked in Lean as D5/S1/Words/EvilOdious/CoefficientTableChecker.prefixcertificate_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.29 (c prefix).

$$\forall (p0:\mathbb{N}),(2048\le p0)\to (p0<4096)\to \forall (w:\mathrm{List}\mathrm{Bool}),((\mathrm{recur}(p6)(\mathrm{appendValue}p0w))).\mathrm{natAbs}\le 2\cdot 16^{w.\mathrm{length}}\cdot \mathrm{seedC}p0\wedge ((\mathrm{recur}(p6)(\mathrm{appendValue}p0w-1))).\mathrm{natAbs}\le 2\cdot 16^{w.\mathrm{length}}\cdot \mathrm{seedC}p0$$

Proof. Machine-checked in Lean as D5/S1/Words/EvilOdious/CoefficientTableChecker.c_prefix (✓ 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.30 (seedH exact).

$$\forall (jp0:\mathbb{N}),(j\in \mathrm{Finset}.\mathrm{Icc}15)\to (p0<4096)\to \mathrm{seedH}jp0=(\mathrm{Finset}.\mathrm{range}5).\sup (\mathrm{fun}i\mapsto ((\mathrm{recur}(pj)(p0-i))).\mathrm{natAbs})$$

Proof. Machine-checked in Lean as D5/S1/Words/EvilOdious/CoefficientTableChecker.seedH_exact (✓ 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 (seedC exact).

$$\forall (p0:\mathbb{N}),(p0<4096)\to \mathrm{seedC}p0=(\mathrm{Finset}.\mathrm{range}6).\sup (\mathrm{fun}i\mapsto ((\mathrm{recur}(p6)(p0-i))).\mathrm{natAbs})$$

Proof. Machine-checked in Lean as D5/S1/Words/EvilOdious/CoefficientTableChecker.seedC_exact (✓ 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 (h dyadic).

$$\forall (jp0m\mathrm{low}:\mathbb{N}),(j\in \mathrm{Finset}.\mathrm{Icc}15)\to (2048\le p0)\to (p0<4096)\to (\mathrm{low}<2^m)\to ((\mathrm{recur}(pj)(p0\cdot 2^m+\mathrm{low}))).\mathrm{natAbs}\le 16^m\cdot (\mathrm{Finset}.\mathrm{range}5).\sup (\mathrm{fun}i\mapsto ((\mathrm{recur}(pj)(p0-i))).\mathrm{natAbs})$$

Proof. Machine-checked in Lean as D5/S1/Words/EvilOdious/CoefficientTableChecker.h_dyadic (✓ 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 (c dyadic).

$$\forall (p0m\mathrm{low}:\mathbb{N}),(2048\le p0)\to (p0<4096)\to (\mathrm{low}<2^m)\to ((\mathrm{recur}(p6)(p0\cdot 2^m+\mathrm{low}))).\mathrm{natAbs}\le 2\cdot 16^m\cdot (\mathrm{Finset}.\mathrm{range}6).\sup (\mathrm{fun}i\mapsto ((\mathrm{recur}(p6)(p0-i))).\mathrm{natAbs})\wedge ((\mathrm{recur}(p6)(p0\cdot 2^m+\mathrm{low}-1))).\mathrm{natAbs}\le 2\cdot 16^m\cdot (\mathrm{Finset}.\mathrm{range}6).\sup (\mathrm{fun}i\mapsto ((\mathrm{recur}(p6)(p0-i))).\mathrm{natAbs})$$

Proof. Machine-checked in Lean as D5/S1/Words/EvilOdious/CoefficientTableChecker.c_dyadic (✓ 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.

References

• Truth anchor: D5/S1/Words/EvilOdious/CoefficientTableChecker.c_dyadic
• Truth anchor: D5/S1/Words/EvilOdious/CoefficientTableChecker.c_prefix
• Truth anchor: D5/S1/Words/EvilOdious/CoefficientTableChecker.h_dyadic
• Truth anchor: D5/S1/Words/EvilOdious/CoefficientTableChecker.initialChunk
• Truth anchor: D5/S1/Words/EvilOdious/CoefficientTableChecker.prefixB
• Truth anchor: D5/S1/Words/EvilOdious/CoefficientTableChecker.prefixChunk
• Truth anchor: D5/S1/Words/EvilOdious/CoefficientTableChecker.prefixcertificate_0
• Truth anchor: D5/S1/Words/EvilOdious/CoefficientTableChecker.prefixcertificate_checked
• Truth anchor: D5/S1/Words/EvilOdious/CoefficientTableChecker.seedC
• Truth anchor: D5/S1/Words/EvilOdious/CoefficientTableChecker.seedC_exact
• Truth anchor: D5/S1/Words/EvilOdious/CoefficientTableChecker.seedH
• Truth anchor: D5/S1/Words/EvilOdious/CoefficientTableChecker.seedH_exact
• Truth anchor: D5/S1/Words/EvilOdious/CoefficientTableChecker.table1
• Truth anchor: D5/S1/Words/EvilOdious/CoefficientTableChecker.table1_checked
• Truth anchor: D5/S1/Words/EvilOdious/CoefficientTableChecker.table1_sound
• Truth anchor: D5/S1/Words/EvilOdious/CoefficientTableChecker.table2
• Truth anchor: D5/S1/Words/EvilOdious/CoefficientTableChecker.table2_sound
• Truth anchor: D5/S1/Words/EvilOdious/CoefficientTableChecker.table3
• Truth anchor: D5/S1/Words/EvilOdious/CoefficientTableChecker.table3_sound
• Truth anchor: D5/S1/Words/EvilOdious/CoefficientTableChecker.table4
• Truth anchor: D5/S1/Words/EvilOdious/CoefficientTableChecker.table4_sound
• Truth anchor: D5/S1/Words/EvilOdious/CoefficientTableChecker.table5
• Truth anchor: D5/S1/Words/EvilOdious/CoefficientTableChecker.table5_sound
• Truth anchor: D5/S1/Words/EvilOdious/CoefficientTableChecker.table6
• Truth anchor: D5/S1/Words/EvilOdious/CoefficientTableChecker.table6_sound
• Truth anchor: D5/S1/Words/EvilOdious/CoefficientTableChecker.tableCheck
• Truth anchor: D5/S1/Words/EvilOdious/CoefficientTableChecker.tableCheck_sound
• Truth anchor: D5/S1/Words/EvilOdious/CoefficientTableChecker.tableError
• Truth anchor: D5/S1/Words/EvilOdious/CoefficientTableChecker.tableError_sound
• Truth anchor: D5/S1/Words/EvilOdious/CoefficientTableChecker.tableH
• Truth anchor: D5/S1/Words/EvilOdious/CoefficientTableChecker.tableH_sound
• Truth anchor: D5/S1/Words/EvilOdious/CoefficientTableChecker.tableStep
• Truth anchor: D5/S1/Words/EvilOdious/CoefficientTableChecker.tableValue
• Dependency: D5/S1/Words/EvilOdious/SequenceCoefficients