SilverSight/formal/CoreFormalism/BraidStateN.lean

/-
Copyright (c) 2026 SilverSight Contributors. All rights reserved.
Released under Apache 2.0 license.

Generic n-strand braid state, crossStep, and receipt encoding.
Unlike BraidEigensolid.lean (which fixes n=8), this version is
parameterized by strand count (n : Nat).

The crossing pattern is adjacent pairing: (0,1), (2,3), ..., (n-2, n-1).
If n is odd, the last strand (n-1) does not participate in crossing.
-/

import CoreFormalism.BraidCross
import CoreFormalism.BraidStrand
import CoreFormalism.BraidBracket

namespace SilverSight.BraidStateN

open SilverSight.BraidCross
open SilverSight.BraidStrand
open SilverSight.BraidBracket
open SilverSight.FixedPoint.Q16_16

-- ── n-strand receipt ───────────────────────────────────────────────────

structure BraidReceiptN (n : Nat) where
  crossing_matrix : BraidBracket
  sidon_slack     : UInt32
  step_count      : Nat
  residuals       : List Q16_16
  write_time      : UInt64
  scar_absent     : Bool
  deriving Repr, DecidableEq, BEq

-- ── n-strand braid state ───────────────────────────────────────────────

structure BraidStateN (n : Nat) where
  strands    : Fin n → BraidStrand
  step_count : Nat
  deriving Repr

-- ── Cross partner (adjacent pairing) ───────────────────────────────────

def crossPartner {n : Nat} (i : Fin n) : Fin n :=
  let iv := i.val
  if h : iv % 2 = 0 then
    if h' : iv + 1 < n then ⟨iv + 1, h'⟩
    else i
  else
    have hpos : iv > 0 := by
      by_contra! hle
      have hzero : iv = 0 := Nat.le_antisymm hle (Nat.zero_le iv)
      have hmod : iv % 2 = 0 := by
        simpa [hzero]
      exact h hmod
    have h_one : 0 < 1 := by norm_num
    have hsub1 : iv - 1 < iv := Nat.sub_lt hpos h_one
    have hsub : iv - 1 < n := Nat.lt_trans hsub1 i.2
    ⟨iv - 1, hsub⟩

lemma crossPartner_involutive {n : Nat} (i : Fin n) (hEven : n % 2 = 0) :
    crossPartner (crossPartner i) = i := by
  apply Fin.ext
  have hpar := Nat.mod_two_eq_zero_or_one i.val
  rcases hpar with (h_even | h_odd)
  · -- i.val is even
    have h_add_lt : i.val + 1 < n := by
      by_contra! hge
      have h_n_odd : (n - 1) % 2 = 1 := by
        -- n is even (hEven), so n-1 is odd
        omega
      have h_even_val : i.val % 2 = 0 := h_even
      -- i.val is even AND i.val ≥ n-1 (since ¬(i.val+1 < n) means i.val+1 ≥ n → i.val ≥ n-1)
      -- But i.val < n, so i.val = n-1
      -- Then i.val is even but n-1 is odd → contradiction
      omega
    have h_new_odd : (i.val + 1) % 2 = 1 := by omega
    have h_sub_lt : i.val + 1 - 1 < n := by
      have : i.val + 1 - 1 = i.val := by omega
      rw [this]
      exact i.2
    simp [crossPartner, h_even, h_add_lt, h_new_odd, h_sub_lt]
  · -- i.val is odd
    have h_pos : i.val > 0 := by
      by_contra! hle
      have : i.val = 0 := by omega
      omega
    have h_sub_lt : i.val - 1 < n :=
      Nat.lt_trans (Nat.sub_lt h_pos (by norm_num : 0 < 1)) i.2
    have h_sub_even : (i.val - 1) % 2 = 0 := by
      -- i.val is odd → (i.val - 1) is even
      have h_odd_val : i.val % 2 = 1 := h_odd
      omega
    have h_add_lt : (i.val - 1) + 1 < n := by
      have : (i.val - 1) + 1 = i.val := by omega
      rw [this]
      exact i.2
    simp [crossPartner, h_odd, h_pos, h_sub_lt, h_sub_even, h_add_lt,
      show (i.val - 1) + 1 - 1 = i.val - 1 by omega]
    omega

-- ── Cross step ─────────────────────────────────────────────────────────

def crossStep {n : Nat} (s : BraidStateN n) : BraidStateN n :=
  let cross2 (i j : Fin n) : BraidStrand :=
    (braidCross (s.strands i) (s.strands j)).1
  let newStrands : Fin n → BraidStrand := fun k =>
    let kv := k.val
    if hpar : kv % 2 = 0 then
      if h : kv + 1 < n then
        cross2 ⟨kv, k.2⟩ ⟨kv + 1, h⟩
      else
        s.strands k
    else
      have hpos : kv > 0 := by
        by_contra! hle
        have hzero : kv = 0 := by
          apply Nat.le_antisymm hle
          exact Nat.zero_le kv
        have hmod : kv % 2 = 0 := by
          simpa [hzero]
        exact hpar hmod
      have hsub : kv - 1 < n :=
        have h_one : 0 < 1 := by norm_num
        have hsub1 : kv - 1 < kv := Nat.sub_lt hpos h_one
        Nat.lt_trans hsub1 k.2
      cross2 k ⟨kv - 1, hsub⟩
  { strands := newStrands
  , step_count := s.step_count + 1 }

-- ── Receipt encoding ───────────────────────────────────────────────────

def encodeReceipt {n : Nat} (hn : 0 < n) (s : BraidStateN n) : BraidReceiptN n :=
  let rs : List Q16_16 :=
    (List.range n).map (fun i =>
      if h : i < n then (s.strands ⟨i, h⟩).residue
      else Q16_16.zero)
  let allAdmissible : Bool :=
    (List.range n).all (fun i =>
      if h : i < n then (s.strands ⟨i, h⟩).bracket.admissible
      else true)
  { crossing_matrix := (s.strands ⟨0, hn⟩).bracket
  , sidon_slack :=
      let lastSlot := (s.strands ⟨n - 1, Nat.sub_lt hn (by norm_num : 0 < 1)⟩).slot
      128 - lastSlot
  , step_count := s.step_count
  , residuals := rs
  , write_time := 0
  , scar_absent := allAdmissible }

lemma encodeReceipt_residuals_length {n : Nat} (hn : 0 < n) (s : BraidStateN n) :
    (encodeReceipt hn s).residuals.length = n := by
  simp [encodeReceipt]

lemma encodeReceipt_step_count {n : Nat} (hn : 0 < n) (s : BraidStateN n) :
    (encodeReceipt hn s).step_count = s.step_count := by
  rfl

-- ── Eigensolid ─────────────────────────────────────────────────────────

def IsEigensolid {n : Nat} (s : BraidStateN n) : Prop :=
  ∀ i : Fin n, (crossStep s).strands i = s.strands i

theorem eigensolid_convergence {n : Nat} (s : BraidStateN n)
    (h_eig : IsEigensolid (crossStep s)) :
    ∀ i : Fin n, (crossStep (crossStep s)).strands i = (crossStep s).strands i := by
  intro i
  exact h_eig i

-- ── n=8 specialization ─────────────────────────────────────────────────

abbrev BraidState8 : Type := BraidStateN 8

def crossStep8 : BraidState8 → BraidState8 := crossStep

def encodeReceipt8 (s : BraidState8) : BraidReceiptN 8 := encodeReceipt (by norm_num) s

def IsEigensolid8 (s : BraidState8) : Prop := IsEigensolid s

end SilverSight.BraidStateN