SixfoldMonotonicity

Abstract

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

Theorem 1.1 (initialr 0).

$$\mathrm{initialChunk}138032=\mathrm{true}$$

Proof. Machine-checked in Lean as D5/S1/Words/EvilOdious/SixfoldMonotonicity.initialr_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.2 (initialr 1).

$$\mathrm{initialChunk}1383232=\mathrm{true}$$

Proof. Machine-checked in Lean as D5/S1/Words/EvilOdious/SixfoldMonotonicity.initialr_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.3 (tail positive).

$$\forall (\mathrm{sigma}:\mathbb{Z}),(\mathrm{sigma}=1\vee \mathrm{sigma}=-1)\to \forall (n:\mathbb{N}),(2048\le n)\to 0<((n+4).\mathrm{choose}4:\mathbb{Z})+\mathrm{errorTerm}\mathrm{sigma}n$$

Proof. Machine-checked in Lean as D5/S1/Words/EvilOdious/SixfoldMonotonicity.tail_positive (✓ 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 (claim).

$$\mathrm{claim}⟺(((\exists (N:\mathbb{N}),\forall (n:\mathbb{N}),n\ge N\to r6n<r6(n+1))\wedge (\exists (N:\mathbb{N}),\forall (n:\mathbb{N}),n\ge N\to s6n<s6(n+1)))\wedge (\forall (n:\mathbb{N}),n\ge 37\to r6n<r6(n+1))\wedge (\forall (n:\mathbb{N}),n\ge 5\to s6n<s6(n+1)))$$

Formalization. D5/S1/Words/EvilOdious/SixfoldMonotonicity.claim (✓ 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.

Conjecture 12, page 10: “(a) Both r₆(n) and s₆(n) are eventually strictly increasing. (a) r₆(n) < r₆(n + 1) for n ≥ 37. (b) s₆(n) < s₆(n + 1) for n ≥ 5.” The duplicated label (a) is printed in the source. Both eventual clauses quantify a natural threshold and all natural n beyond it. Tuple coordinates are ordered, range over the nonnegative integers, and admit repetitions.

Theorem 1.5 (result).

$$\mathrm{claim}$$

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

Resolves. Problems/allouche-shallit-2021-sixfold-evil-odious (proved) by D5/S1/Words/EvilOdious/SixfoldMonotonicity.result.

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/SixfoldMonotonicity.claim
• Truth anchor: D5/S1/Words/EvilOdious/SixfoldMonotonicity.initialr_0
• Truth anchor: D5/S1/Words/EvilOdious/SixfoldMonotonicity.initialr_1
• Truth anchor: D5/S1/Words/EvilOdious/SixfoldMonotonicity.result
• Truth anchor: D5/S1/Words/EvilOdious/SixfoldMonotonicity.tail_positive
• Dependency: D5/S1/Words/EvilOdious/CoefficientTableChecker