/-
PhiDNALayout.lean — Ring 3: 30-base layout type with window invariants

phi.embed.encode_phi builds a 30-base hachimoji DNA sequence in four layers:

  bases  0-7  : F(E)  — byte-class histogram    (first 8 of 12 classes)
  bases  8-15 : τ(E)  — AST node-type histogram  (first 8 of 18 NODE_TYPES)
  bases 16-23 : δ(E)  — child-ordering histogram  (first 8 δ values)
  bases 24-29 : 6 consistency rules              (G = pass, T = fail ONLY)

Source (phi.embed.py lines 135-143):
  F_dna           = _vec_to_bases(F[:8])
  tau_dna         = _vec_to_bases(tau[:8] ...)
  delta_dna       = _vec_to_bases((delta + [0.5]*8)[:8] ...)
  consistency_dna = "".join("G" if ... else "T" for r in RULE_ORDER)
  full_sequence   = F_dna + tau_dna + delta_dna + consistency_dna  -- len 30

The key structural invariant: bases 24-29 are BINARY (only G or T).
Layers 1-3 are unrestricted (any of the 8 HachimojiBase constructors).

Anti-drift role: Ring 3 wire in the outward dependency spiral.
Any change to the 8+8+8+6 partition, or to Layer 4's binary encoding,
breaks this bridge before Ring 4 (the 6 consistency rules).
-/

import SilverSight.HachimojiCharClass
import Mathlib.Tactic

namespace SilverSight.PhiDNALayout

open HachimojiBase
open SilverSight.HachimojiCharClass

-- ============================================================
-- §1  LAYOUT CONSTANTS
-- ============================================================

/-- Total bases in a Φ-encoded DNA sequence. -/
def DNA_LEN : ℕ := 30

/-- Each of layers 1-3 has 8 bases. -/
def LAYER_WIDTH : ℕ := 8

/-- Layer 4 has exactly 6 bases (one per consistency rule). -/
def CONSISTENCY_WIDTH : ℕ := 6

theorem layout_sum : 3 * LAYER_WIDTH + CONSISTENCY_WIDTH = DNA_LEN := by decide

-- ============================================================
-- §2  LAYOUT TYPE
-- ============================================================

/-- A valid Φ-encoded DNA sequence.
    The only structural invariant is Layer 4: bases 24-29 are binary
    (G = rule passed, T = rule failed).  Layers 1-3 are unrestricted. -/
structure PhiLayout where
  seq      : Fin 30 → HachimojiBase
  h_layer4 : ∀ i : Fin 6,
      seq ⟨24 + i.val, by omega⟩ = G ∨
      seq ⟨24 + i.val, by omega⟩ = T

-- ============================================================
-- §3  WINDOW SELECTORS
-- ============================================================

/-- Layer 1: F(E) byte-class frequencies (bases 0-7). -/
def PhiLayout.layer1 (d : PhiLayout) : Fin 8 → HachimojiBase :=
  fun i => d.seq ⟨i.val, by omega⟩

/-- Layer 2: τ(E) AST node-type frequencies (bases 8-15). -/
def PhiLayout.layer2 (d : PhiLayout) : Fin 8 → HachimojiBase :=
  fun i => d.seq ⟨8 + i.val, by omega⟩

/-- Layer 3: δ(E) child-ordering frequencies (bases 16-23). -/
def PhiLayout.layer3 (d : PhiLayout) : Fin 8 → HachimojiBase :=
  fun i => d.seq ⟨16 + i.val, by omega⟩

/-- Layer 4: consistency rule pass/fail (bases 24-29). -/
def PhiLayout.layer4 (d : PhiLayout) : Fin 6 → HachimojiBase :=
  fun i => d.seq ⟨24 + i.val, by omega⟩

-- ============================================================
-- §4  PARTITION LEMMAS
-- ============================================================

/-- Every DNA position belongs to exactly one layer. -/
theorem layer_partition (i : Fin 30) :
    i.val < 8 ∨ (8 ≤ i.val ∧ i.val < 16) ∨
    (16 ≤ i.val ∧ i.val < 24) ∨ (24 ≤ i.val) := by omega

/-- Layer selectors correspond to the right slice of seq. -/
@[simp] theorem layer1_val (d : PhiLayout) (i : Fin 8) :
    d.layer1 i = d.seq ⟨i.val, by omega⟩ := rfl

@[simp] theorem layer2_val (d : PhiLayout) (i : Fin 8) :
    d.layer2 i = d.seq ⟨8 + i.val, by omega⟩ := rfl

@[simp] theorem layer3_val (d : PhiLayout) (i : Fin 8) :
    d.layer3 i = d.seq ⟨16 + i.val, by omega⟩ := rfl

@[simp] theorem layer4_val (d : PhiLayout) (i : Fin 6) :
    d.layer4 i = d.seq ⟨24 + i.val, by omega⟩ := rfl

-- ============================================================
-- §5  LAYER 4 BINARY CONSTRAINT
-- ============================================================

/-- Layer 4 bases are binary: only G (pass) or T (fail). -/
theorem layer4_binary (d : PhiLayout) (i : Fin 6) :
    d.layer4 i = G ∨ d.layer4 i = T := d.h_layer4 i

/-- Layer 4 never contains A, B, C, P, S, or Z. -/
theorem layer4_not_ABCPSZ (d : PhiLayout) (i : Fin 6) :
    d.layer4 i ≠ A ∧ d.layer4 i ≠ B ∧ d.layer4 i ≠ C ∧
    d.layer4 i ≠ P ∧ d.layer4 i ≠ S ∧ d.layer4 i ≠ Z := by
  obtain (h | h) := layer4_binary d i <;> rw [h] <;> decide

-- ============================================================
-- §6  CONNECTION TO RING 2 (CharClass)
-- ============================================================

/-- The char class encoded at Layer 1 slot i. -/
def layer1CharClass (d : PhiLayout) (i : Fin 8) : PhiCharClass :=
  baseToCharClass (d.layer1 i)

/-- Roundtrip: the HachimojiBase at slot i is the base for char class i. -/
theorem layer1_charclass_roundtrip (d : PhiLayout) (i : Fin 8) :
    charClassToBase (layer1CharClass d i) = d.layer1 i :=
  base_charclass_roundtrip (d.layer1 i)

-- ============================================================
-- §7  SIMPLE CONSTRUCTOR (for witnesses)
-- ============================================================

/-- Build a PhiLayout from four function arguments.
    Layer 4: con i = true → G (pass), false → T (fail). -/
def mkPhiLayout
    (f   : Fin 8 → HachimojiBase)
    (tau : Fin 8 → HachimojiBase)
    (del : Fin 8 → HachimojiBase)
    (con : Fin 6 → Bool) : PhiLayout where
  seq := fun ⟨n, hn⟩ =>
    if h1 : n < 8  then f   ⟨n, h1⟩
    else if h2 : n < 16 then tau ⟨n - 8,  by omega⟩
    else if h3 : n < 24 then del ⟨n - 16, by omega⟩
    else if con ⟨n - 24, by omega⟩ then G else T
  h_layer4 := by
    intro ⟨j, hj⟩
    have h1 : ¬(24 + j < 8)  := by omega
    have h2 : ¬(24 + j < 16) := by omega
    have h3 : ¬(24 + j < 24) := by omega
    simp only [dif_neg h1, dif_neg h2, dif_neg h3]
    split_ifs with _h
    · exact Or.inl rfl
    · exact Or.inr rfl

end SilverSight.PhiDNALayout
