import RequestProject.RecursiveDepth

/-!
# The two-lattice fingerprint of a prime

For a prime `p ≥ 5`, the square grid (form `x² + y²`) and the flower lattice
(form `x² − xy + y²`) each either *split* at `p` (the form has a non-trivial zero mod `p`)
or stay *inert*. This file records the complete four-way table, decided by `p mod 12`:

| `p mod 12` | square grid | flower |
|---|---|---|
| 1  | split | split |
| 5  | split | inert |
| 7  | inert | split |
| 11 | inert | inert |

The earlier file `RecursiveDepth.lean` stated only the class-7 row as its own theorem.
-/

namespace Synthesis

open RecursiveDepth

/-- The square grid's form `x² + y²` has a non-trivial zero mod `p`. -/
def SquareSplits (p : ℕ) : Prop :=
  ∃ x y : ZMod p, (x ≠ 0 ∨ y ≠ 0) ∧ x ^ 2 + y ^ 2 = 0

/-- The flower lattice's form `x² − xy + y²` has a non-trivial zero mod `p`. -/
def HexSplits (p : ℕ) : Prop :=
  ∃ x y : ZMod p, (x ≠ 0 ∨ y ≠ 0) ∧ x ^ 2 - x * y + y ^ 2 = 0

/-- **Two-lattice fingerprint.** For a prime `p ≠ 2, 3`, the class of `p` mod 12 decides both
lattices at once, and all four combinations occur, one per class. -/
theorem two_lattice_fingerprint (p : ℕ) [Fact p.Prime] (hp2 : p ≠ 2) (hp3 : p ≠ 3) :
    (p % 12 = 1 ↔ SquareSplits p ∧ HexSplits p) ∧
    (p % 12 = 5 ↔ SquareSplits p ∧ ¬ HexSplits p) ∧
    (p % 12 = 7 ↔ ¬ SquareSplits p ∧ HexSplits p) ∧
    (p % 12 = 11 ↔ ¬ SquareSplits p ∧ ¬ HexSplits p) := by
  unfold SquareSplits HexSplits
  rw [(square_form_splits_iff p hp2).1, (hex_form_splits_iff p hp3).1]
  have h2 : ¬ 2 ∣ p := fun h =>
    hp2 ((Nat.prime_dvd_prime_iff_eq Nat.prime_two Fact.out).mp h).symm
  have h3 : ¬ 3 ∣ p := fun h =>
    hp3 ((Nat.prime_dvd_prime_iff_eq Nat.prime_three Fact.out).mp h).symm
  omega

/-! ## Design optimality of the counting bases

Each classical counting base is the *least* number with its divisibility property: a number has
the property exactly when it is a multiple of the base. -/

/-- 12 is the least counting base divisible by 1, 2, 3, 4. -/
theorem twelve_design (n : ℕ) : (∀ k ∈ Finset.Icc 1 4, k ∣ n) ↔ 12 ∣ n := by
  constructor
  · intro h
    have h3 := h 3 (by decide); have h4 := h 4 (by decide)
    omega
  · intro h k hk
    exact (show k ∣ 12 by fin_cases hk <;> decide).trans h

/-- 60 is the least counting base divisible by every number from 1 to 6. -/
theorem sixty_design (n : ℕ) : (∀ k ∈ Finset.Icc 1 6, k ∣ n) ↔ 60 ∣ n := by
  constructor
  · intro h
    have h3 := h 3 (by decide); have h4 := h 4 (by decide); have h5 := h 5 (by decide)
    omega
  · intro h k hk
    exact (show k ∣ 60 by fin_cases hk <;> decide).trans h

/-- 360 is the least dial divisible by every number from 1 to 10 except 7 (the one prime it
leaves out, which is exactly the step that walks the whole dial). -/
theorem three_sixty_design (n : ℕ) :
    (∀ k ∈ Finset.Icc 1 10, k ≠ 7 → k ∣ n) ↔ 360 ∣ n := by
  constructor
  · intro h
    have h5 := h 5 (by decide) (by decide); have h8 := h 8 (by decide) (by decide)
    have h9 := h 9 (by decide) (by decide)
    omega
  · intro h k hk h7
    exact (show k ∣ 360 by fin_cases hk <;> simp_all).trans h

/-- Adding the 7-wheel: 2520 is the least number divisible by every number from 1 to 10. -/
theorem twenty_five_twenty_design (n : ℕ) : (∀ k ∈ Finset.Icc 1 10, k ∣ n) ↔ 2520 ∣ n := by
  constructor
  · intro h
    have h5 := h 5 (by decide); have h7 := h 7 (by decide); have h8 := h 8 (by decide)
    have h9 := h 9 (by decide)
    omega
  · intro h k hk
    exact (show k ∣ 2520 by fin_cases hk <;> decide).trans h

end Synthesis