DigitProduct.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

The digit-product transfer

For a cyclic avoiding coloring modulo N, color an integer by the colors of its first m base-N digits. The first nonzero digit of a positive common difference supplies a nonzero cyclic step. The arithmetic proof uses finite divisibility, so it applies to composite bases as well as prime bases.

The explicit avoiding-coloring theorems are unconditional. Statements about W consume the genuine finite Ramsey witness, supplied by UpperBound at the final assembly; finiteness is not built into the definition of W.

theorem OAI.QuantitativeVanDerWaerden.exists_base_factor line 29
Source documentation
Select the last dividing base power below a positive difference bound. No primality assumption is needed.
```
theorem exists_base_factor {N d m : ℕ} (hd : 0 < d) (hbound : d < N ^ m) :
    ∃ i < m, ∃ e, d = N ^ i * e ∧ ¬ N ∣ e := by
…
```
theorem OAI.QuantitativeVanDerWaerden.div_ap_of_base_factor line 57
Source documentation
Exact quotient arithmetic at a coordinate whose base power divides the common difference. This is the entire carry argument.
```
theorem div_ap_of_base_factor {N d i e : ℕ} (hN : 0 < N)
    (hd : d = N ^ i * e) (a j : ℕ) :
    (a + j * d) / N ^ i = a / N ^ i + j * e := by
…
```
def OAI.QuantitativeVanDerWaerden.digitColor line 64
Source documentation
A digit is identified with its residue, so an extra remainder is redundant.
```
def digitColor {N : ℕ} {α : Type uAlpha} (C : ZMod N → α) (m : ℕ) :
    ℕ → (Fin m → α) :=
…
```
theorem OAI.QuantitativeVanDerWaerden.digitColor_avoids line 68
def OAI.QuantitativeVanDerWaerden.finiteColorEmbedding line 88
Source documentation
Explicit recoloring into any sufficiently large standard finite palette.
```
noncomputable def finiteColorEmbedding {α : Type uAlpha} [Fintype α] {r : ℕ}
    (h : Fintype.card α ≤ r) : α ↪ Fin r :=
…
```
theorem OAI.QuantitativeVanDerWaerden.exists_digit_product_avoiding line 92
theorem OAI.QuantitativeVanDerWaerden.digit_product_not_isRamsey line 103

theorem OAI.QuantitativeVanDerWaerden.digit_product_lt_W line 110

Source documentation

The finite witness is provided by the proved upper-bound construction.

theorem digit_product_lt_W {N k m r : ℕ} {α : Type uAlpha} [Fintype α]
    {C : ZMod N → α} (hN : 2 ≤ N) (hk : 2 ≤ k) (hC : CyclicAvoids C k)
    (hcolors : Fintype.card α ^ m ≤ r)
    (hfinite : ∃ M, 0 < M ∧ IsRamsey (Fin r) k M) : N ^ m < W r k := by
…

Mentions: OAI.QuantitativeVanDerWaerden.CyclicAvoids, OAI.QuantitativeVanDerWaerden.IsRamsey

theorem OAI.QuantitativeVanDerWaerden.binary_digit_product_lt_W line 116
theorem OAI.QuantitativeVanDerWaerden.binary_digit_product_log_lt_W line 123