SilverSight/formal/SilverSight/HachimojiCharClass.lean

/-
HachimojiCharClass.lean — Ring 2: PhiCharClass ≃ HachimojiBase

phi.charclass (BioSight) defines 12 character classes. phi.embed uses only
the first 8 (indices 0-7) in DNA bases 0-7 of the 30-base layout:

  bases  0-7  : F(E) byte-class frequencies (Layer 1)
  bases  8-15 : τ(E) parse-tree node types   (Layer 2)
  bases 16-23 : δ(E) child-ordering          (Layer 3)
  bases 24-29 : consistency flags             (Layer 4)

The base at slot i is HACHIMOJI_BASES[i] where
  HACHIMOJI_BASES = list("ABCGPSTZ")   -- phi.embed.py line 37

Explicit mapping (INDEX_TO_BASE in phi.embed.py):
  digit       (0) ↔ A
  lower_alpha (1) ↔ B
  upper_alpha (2) ↔ C
  operator    (3) ↔ G
  bracket     (4) ↔ P
  punctuation (5) ↔ S
  whitespace  (6) ↔ T
  other       (7) ↔ Z

Anti-drift role: this is the Ring 2 wire in the outward dependency spiral.
Any change to BioSight's HACHIMOJI_BASES string, the first-8-class selection,
or the char-class indices breaks this bridge before reaching Ring 3 or Ring 4.
-/

import CoreFormalism.HachimojiManifoldAxiom
import Mathlib.Tactic

namespace SilverSight.HachimojiCharClass

-- ============================================================
-- §1  PHI CHARACTER CLASSES (DNA Layer 1)
-- ============================================================

/-- The 8 character classes encoding DNA Layer 1 (bases 0-7).
    Source: phi.charclass.CHAR_CLASSES indices 0-7.
    Classes 8-11 (symmetry, periodicity, continuity, meta_math) are not
    in Layer 1 — they fold into the AST-based layers 2-3. -/
inductive PhiCharClass where
  | digit        -- 0: 0-9
  | lower_alpha  -- 1: a-z
  | upper_alpha  -- 2: A-Z
  | operator_    -- 3: +-*/^%=<>!&|~
  | bracket      -- 4: ()[]{}
  | punctuation  -- 5: .,;:'"@#$\_
  | whitespace   -- 6: space, tab, newline
  | other        -- 7: Unicode, non-ASCII
  deriving DecidableEq, Repr, Fintype

/-- Exactly 8 character classes in DNA Layer 1. -/
theorem phi_charclass_card : Fintype.card PhiCharClass = 8 := by decide

-- ============================================================
-- §2  THE BIJECTION (phi.embed.INDEX_TO_BASE)
-- ============================================================

/-- Map char class to its HachimojiBase.
    Ordering: HACHIMOJI_BASES = list("ABCGPSTZ"), index = charclass index. -/
def charClassToBase : PhiCharClass → HachimojiBase
  | .digit       => .A
  | .lower_alpha => .B
  | .upper_alpha => .C
  | .operator_   => .G
  | .bracket     => .P
  | .punctuation => .S
  | .whitespace  => .T
  | .other       => .Z

/-- Inverse: the base at DNA slot i was produced by char class i. -/
def baseToCharClass : HachimojiBase → PhiCharClass
  | .A => .digit
  | .B => .lower_alpha
  | .C => .upper_alpha
  | .G => .operator_
  | .P => .bracket
  | .S => .punctuation
  | .T => .whitespace
  | .Z => .other

/-- The Layer 1 char-class ↔ HachimojiBase correspondence is a bijection. -/
def charClassEquiv : PhiCharClass ≃ HachimojiBase where
  toFun     := charClassToBase
  invFun    := baseToCharClass
  left_inv  := by intro c; cases c <;> rfl
  right_inv := by intro b; cases b <;> rfl

-- ============================================================
-- §3  DERIVED FACTS
-- ============================================================

/-- Distinct char classes produce distinct bases: layer-1 is drift-detectable. -/
theorem charClassToBase_injective : Function.Injective charClassToBase :=
  charClassEquiv.injective

/-- Every HachimojiBase appears as a Layer-1 byte-class encoding. -/
theorem charClassToBase_surjective : Function.Surjective charClassToBase :=
  charClassEquiv.surjective

/-- Composition: charClassToBase ∘ baseToCharClass = id. -/
theorem base_charclass_roundtrip : ∀ b : HachimojiBase,
    charClassToBase (baseToCharClass b) = b :=
  charClassEquiv.right_inv

/-- Composition: baseToCharClass ∘ charClassToBase = id. -/
theorem charclass_base_roundtrip : ∀ c : PhiCharClass,
    baseToCharClass (charClassToBase c) = c :=
  charClassEquiv.left_inv

-- ============================================================
-- §4  DNA SLOT POSITIONS
-- ============================================================

/-- The DNA slot (position in the 30-base sequence) for each char class. -/
def PhiCharClass.dnaSlot : PhiCharClass → Fin 30
  | .digit       => ⟨0, by omega⟩
  | .lower_alpha => ⟨1, by omega⟩
  | .upper_alpha => ⟨2, by omega⟩
  | .operator_   => ⟨3, by omega⟩
  | .bracket     => ⟨4, by omega⟩
  | .punctuation => ⟨5, by omega⟩
  | .whitespace  => ⟨6, by omega⟩
  | .other       => ⟨7, by omega⟩

/-- Layer 1 slots are strictly in the first 8 positions of the 30-base DNA. -/
theorem dna_layer1_in_first8 : ∀ c : PhiCharClass, (c.dnaSlot : ℕ) < 8 := by
  intro c; cases c <;> simp [PhiCharClass.dnaSlot]

/-- DNA slots for distinct char classes are distinct (no collision in Layer 1). -/
theorem dna_slots_injective : Function.Injective PhiCharClass.dnaSlot := by
  intro a b h
  cases a <;> cases b <;> simp_all [PhiCharClass.dnaSlot]

-- ============================================================
-- §5  WITNESSES
-- ============================================================

#eval charClassToBase .digit        -- expect: HachimojiBase.A
#eval charClassToBase .lower_alpha  -- expect: HachimojiBase.B
#eval charClassToBase .upper_alpha  -- expect: HachimojiBase.C
#eval charClassToBase .operator_    -- expect: HachimojiBase.G
#eval charClassToBase .bracket      -- expect: HachimojiBase.P
#eval charClassToBase .punctuation  -- expect: HachimojiBase.S
#eval charClassToBase .whitespace   -- expect: HachimojiBase.T
#eval charClassToBase .other        -- expect: HachimojiBase.Z

end SilverSight.HachimojiCharClass