/-
BraidStrand.lean - Transport Topology with Bracket Shell

Braids carry the flow. Each strand accumulates PhaseVec contributions linearly
and carries a BraidBracket shell for local admissibility.

Hierarchy: DIAT leaf → AMMR vector → braid strand → bracket shell
-/

import CoreFormalism.DynamicCanal
import CoreFormalism.BraidBracket
import CoreFormalism.FixedPoint
open SilverSight.FixedPoint.Q16_16

set_option linter.dupNamespace false

namespace SilverSight.BraidStrand

open DynamicCanal
open SilverSight.BraidBracket
open SilverSight.FixedPoint.Q16_16

/-- BraidStrand: a single transport strand in the braid topology

  zᵢ = Σₖ Φᵢₖ  (linear AMMR accumulation)
  Bᵢ = C(zᵢ, μᵢ)  (bracket from accumulated state)
-/
structure BraidStrand where
  phaseAcc : PhaseVec    -- zᵢ: accumulated phase vector
  parity   : Bool        -- strand parity for crossing orientation
  slot     : UInt32      -- μᵢ: transport slot / channel assignment
  residue  : Q16_16       -- residual from prior crossings
  jitter   : Q16_16       -- timing/phase jitter bound
  bracket  : BraidBracket  -- C(zᵢ, μᵢ): admissibility shell
  deriving Repr, DecidableEq, BEq

namespace BraidStrand

/-- Create a fresh strand from initial phase contribution

  For DIAT leaf encoding: strand starts with single AMMR contribution.
-/
def fromLeaf (Φ : PhaseVec) (slot : UInt32) (μ : Q16_16) : BraidStrand :=
  let z := Φ
  { phaseAcc := z
  , parity := true
  , slot := slot
  , residue := Q16_16.zero
  , jitter := Q16_16.zero
  , bracket := BraidBracket.fromPhaseVec z μ }

/-- Update bracket after phase accumulation changes

  Recompute C(z, μ) from current phaseAcc and slot.
  This is the correct pattern: merge linearly, then derive bracket.
-/
def updateBracket (s : BraidStrand) : BraidStrand :=
  let μ := Q16_16.ofNat s.slot.toNat
  { s with bracket := BraidBracket.fromPhaseVec s.phaseAcc μ }

/-- Add AMMR contribution to strand (linear accumulation)

  Φ is the local vector contribution from a mode/carrier.
  Bracket is NOT updated here — updateBracket must be called explicitly.
-/
def addContribution (s : BraidStrand) (Φ : PhaseVec) : BraidStrand :=
  { s with phaseAcc := PhaseVec.add s.phaseAcc Φ }

/-- Zero strand (identity element for merge) -/
def zero (slot : UInt32) : BraidStrand :=
  let z := PhaseVec.zero
  let μ := Q16_16.ofNat slot.toNat
  { phaseAcc := z
  , parity := true
  , slot := slot
  , residue := Q16_16.zero
  , jitter := Q16_16.zero
  , bracket := BraidBracket.fromPhaseVec z μ }

/-- Check if strand is admissible (bracket bounds valid) -/
def isAdmissible (s : BraidStrand) : Bool :=
  s.bracket.admissible && s.bracket.gapConserved

/-- Strand magnitude ‖zᵢ‖ (norm approximation) -/
def magnitude (s : BraidStrand) : Q16_16 :=
  s.phaseAcc.normApprox

/-- Strand phase angle (0 if zero vector) -/
def phaseAngle (s : BraidStrand) : Q16_16 :=
  s.bracket.phi

end BraidStrand


/-- Strand registry for AVMR append-only storage -/
structure StrandRegistry where
  entries : List BraidStrand
  nextSlot : UInt32
  deriving Repr, DecidableEq

namespace StrandRegistry

def empty : StrandRegistry :=
  { entries := [], nextSlot := 0 }

def register (reg : StrandRegistry) (strand : BraidStrand) : StrandRegistry :=
  { entries := strand :: reg.entries
  , nextSlot := reg.nextSlot + 1 }

def count (reg : StrandRegistry) : Nat :=
  reg.entries.length

def allAdmissible (reg : StrandRegistry) : Bool :=
  reg.entries.all (fun s => BraidStrand.isAdmissible s)

end StrandRegistry


#eval BraidStrand.isAdmissible (BraidStrand.zero 0)
#eval (StrandRegistry.empty.nextSlot)

end SilverSight.BraidStrand