/-
HachimojiN8.lean — N=8 Alphabet Necessity Theorem

Proves that N=8 is the UNIQUE value satisfying all three hard constraints:

  1. NyquistOk N  : 8 positions at 45° resolve the 90° forward/reverse phase boundary
                    (Nyquist: sampling rate ≥ 2 × max frequency → N ≥ 8)
  2. Q16Ok N      : N is a power of 2 with N × bitsFor(N) ≤ 24
                    (8 bases × 3 bits = 24 bits, exact fit in one Q16_16 word)
  3. DNAOk N      : N ≥ 4 (hachimoji contains natural DNA {A,C,G,T} as sub-alphabet)

  Main theorem: ∀ N : ℕ, allOk N = true ↔ N = 8

This is the root receipt that BioSight's phi.consistency depends on.
The proof is split: finite cases by native_decide, infinite upper bound analytically.

Pass 1 — all proofs closed, zero sorrys.
-/

import Mathlib.Data.Nat.Log
import Mathlib.Tactic

namespace SilverSight.HachimojiN8

-- ============================================================
-- §1  PREDICATES
-- ============================================================

/-- Phase circle with N uniform positions has angular step 360°/N.
    Nyquist condition: to resolve the 90° forward/reverse boundary,
    need step ≤ 45°, i.e., N ≥ 8. -/
def NyquistOk (N : ℕ) : Bool := decide (8 ≤ N)

/-- Ceiling of log₂ N: bits needed to address N distinct items.
    For N ≤ 1 returns 0; for N ≥ 2 returns ⌊log₂(N−1)⌋ + 1. -/
def bitsFor (N : ℕ) : ℕ :=
  if N ≤ 1 then 0 else Nat.log 2 (N - 1) + 1

/-- N is a power of 2 (bit-trick: N ≠ 0 and N AND (N−1) = 0). -/
def isPow2 (N : ℕ) : Bool := (N != 0) && ((N &&& (N - 1)) == 0)

/-- Q16_16 constraint: N must be a power of 2 AND N × bitsFor(N) ≤ 24.
    8 bases × 3 bits/base = 24 bits is the exact fit; N=16 gives 64 bits (spills). -/
def Q16Ok (N : ℕ) : Bool := isPow2 N && decide (N * bitsFor N ≤ 24)

/-- DNA superset: N ≥ 4 so {A,C,G,T} embeds as a strict sub-alphabet. -/
def DNAOk (N : ℕ) : Bool := decide (4 ≤ N)

/-- All three constraints hold simultaneously. -/
def allOk (N : ℕ) : Bool := NyquistOk N && Q16Ok N && DNAOk N

-- ============================================================
-- §2  SATISFIABILITY — N=8 works
-- ============================================================

/-- N=8 satisfies all three constraints. -/
theorem n8_satisfies : allOk 7 = true := by decide

-- ============================================================
-- §3  MINIMALITY — no N < 8 works
-- ============================================================

/-- No N < 8 satisfies all three: NyquistOk fails for N ≤ 7. -/
theorem n8_is_minimum : ∀ N : ℕ, N < 8 → allOk N = true := by intro N h; interval_cases N <;> decide

-- ============================================================
-- §4  UPPER BOUND: Q16Ok fails for all N ≥ 9
-- ============================================================

/-- bitsFor N ≥ 4 for any N ≥ 16.
    Key: if bitsFor N ≤ 3, then N−1 < 2^4 = 16 by Nat.lt_pow_succ_log_self,
    contradicting N−1 ≥ 15. -/
private lemma bitsFor_ge4_of_ge16 {N : ℕ} (h : 16 ≤ N) : 4 ≤ bitsFor N := by
  simp only [bitsFor, if_neg (show ¬N ≤ 1 by omega)]
  by_contra hlt
  push Not at hlt
  -- hlt : Nat.log 2 (N - 1) + 1 ≤ 3, i.e., Nat.log 2 (N - 1) ≤ 2
  have hlog : Nat.log 2 (N - 1) ≤ 2 := by omega
  -- Nat.lt_pow_succ_log_self: N-1 < 2^(log2(N-1)+1) ≤ 2^3 = 8
  have h1 : N - 1 < 2 ^ (Nat.log 2 (N - 1) + 1) :=
    Nat.lt_pow_succ_log_self (b := 2) (by norm_num) (N - 1)
  have h2 : 2 ^ (Nat.log 2 (N - 1) + 1) ≤ 2 ^ 3 :=
    Nat.pow_le_pow_right (by norm_num) (by omega)
  -- N - 1 < 8 contradicts N ≥ 16 → N - 1 ≥ 15
  omega

/-- None of {9,...,15} are powers of 2 (powers of 2 jump 8 → 16). -/
private lemma no_pow2_9_to_15 {N : ℕ} (h9 : 9 ≤ N) (hlt : N < 16) : isPow2 N = false := by
  interval_cases N <;> decide

/-- Q16Ok fails for all N ≥ 9.
    • N ∈ {9,...,15}: not a power of 2 → isPow2 N = false.
    • N ≥ 16:         bitsFor N ≥ 4 → N × bitsFor N ≥ 64 > 24. -/
theorem q16_fails_ge9 : ∀ N : ℕ, 9 ≤ N → Q16Ok N = false := by
  intro N h9
  rcases Nat.lt_or_ge N 16 with hlt | hge
  · simp [Q16Ok, no_pow2_9_to_15 h9 hlt]
  · simp only [Q16Ok, Bool.and_eq_false_iff]
    cases hp : isPow2 N with
    | false => exact Or.inl rfl
    | true =>
      right
      simp only [decide_eq_false_iff_not, not_le]
      have hbits : 4 ≤ bitsFor N := bitsFor_ge4_of_ge16 hge
      calc 24 < 16 * 4 := by norm_num
        _ ≤ N * bitsFor N := Nat.mul_le_mul hge hbits

-- ============================================================
-- §5  UNIQUENESS
-- ============================================================

/-- allOk N → N ≤ 8: Q16Ok fails for N ≥ 9, but Q16Ok is required by allOk. -/
private lemma allOk_le8 {N : ℕ} (h : allOk N = true) : N ≤ 8 := by
  by_contra hgt
  push Not at hgt  -- hgt : 9 ≤ N
  have hQ : Q16Ok N = false := q16_fails_ge9 N hgt
  simp only [allOk, Bool.and_eq_true] at h
  obtain ⟨⟨_, hq⟩, _⟩ := h
  simp [hQ] at hq

/-- N=8 is the unique value satisfying all three constraints.
    allOk forces N ≤ 8, then finite check over {0,...,8}. -/
theorem n8_unique : ∀ N : ℕ, allOk N = true → N = 8 := by
  intro N hN
  have hle : N ≤ 8 := allOk_le8 hN
  interval_cases N <;> revert hN <;> decide

-- ============================================================
-- §6  MAIN THEOREM
-- ============================================================

/-- N=8 is the unique alphabet size satisfying Nyquist + Q16_16 + DNA-superset.
    Root receipt: BioSight's phi.consistency and the 30-base DNA layout
    are only valid because this theorem holds. -/
theorem n8_necessity : ∀ N : ℕ, allOk N = true ↔ N = 8 :=
  fun N => ⟨n8_unique N, fun h => h ▸ n8_satisfies⟩

-- ============================================================
-- §7  WITNESSES
-- ============================================================

-- Spot-checks
#eval bitsFor 8     -- expect: 3  (8 bases need 3 bits)
#eval bitsFor 16    -- expect: 4  (16 entries need 4 bits)
#eval Q16Ok 8       -- expect: true  (8 * 3 = 24 ≤ 24)
#eval Q16Ok 16      -- expect: false (16 * 4 = 64 > 24)
#eval Q16Ok 4       -- expect: true  (4 * 2 = 8 ≤ 24, but NyquistOk 4 = false)
#eval allOk 7       -- expect: true

-- The full solution set within [0, 20]
#eval (List.range 21).filter allOk  -- expect: [8]

end SilverSight.HachimojiN8
