CyclicColoring.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

def OAI.QuantitativeVanDerWaerden.CyclicColoring.finiteImageKey line 18
theorem OAI.QuantitativeVanDerWaerden.CyclicColoring.finiteImageKey_val line 21
theorem OAI.QuantitativeVanDerWaerden.CyclicColoring.finiteImageKey_eq_iff line 24
def OAI.QuantitativeVanDerWaerden.CyclicColoring.ambientSignature line 29
Source documentation
Coercion keeps literal key identities and is injective on signature words.
```
def ambientSignature {k : ℕ} (key : X → Ambient)
    (σ : Signature (Set.range key) k) : Signature Ambient k :=
…
```
theorem OAI.QuantitativeVanDerWaerden.CyclicColoring.ambientSignature_injective line 33

theorem OAI.QuantitativeVanDerWaerden.CyclicColoring.cyclic_signature_image_card line 44

Source documentation

Passing to the finite image does not rename or merge geometric signatures.

theorem cyclic_signature_image_card {N k : ℕ} [NeZero N] [DecidableEq Ambient]
    (c₀ : ZMod N → Bool) (key : ZMod N → Ambient)
    (A : Finset (ZMod N × ZMod N)) :
    (A.image (cyclicSignature (k := k) c₀ (finiteImageKey key))).card =
…

Mentions: OAI.QuantitativeVanDerWaerden.CyclicColoring.finiteImageKey

theorem OAI.QuantitativeVanDerWaerden.CyclicColoring.exists_cyclicAvoids_of_ambient_keys line 60

Source documentation

The finite Bernoulli construction also applies to an infinite ambient key type: only the actual image is used as the probability-space coordinate type.

theorem exists_cyclicAvoids_of_ambient_keys {N k : ℕ} [NeZero N]
    [DecidableEq Ambient] (c₀ : ZMod N → Bool) (key : ZMod N → Ambient)
    (A : Finset (ZMod N × ZMod N)) (hA : A ⊆ nonzeroProgressions N)
    {p : ℝ} (hp : 0 ≤ p) (hp2 : p ≤ 1 / 2)
    (hmult : ∀ ad ∈ nonzeroProgressions N, ∀ a,
      (Finset.univ.filter (fun j : Fin k => (cyclicSignature (k := k) c₀ key ad j).2 = a)).card ≤ 4)
…

theorem OAI.QuantitativeVanDerWaerden.CyclicColoring.exists_cyclicAvoids_of_geometric_data line 106