/-
BraidSpherionBridge.lean — SpherionState ↔ BraidState Equivalence

Shows the correspondence between:
  - SpherionState (MMR + Mountains + RG flow via betaStep)
  - BraidState    (8 strands + crossStep)

Two formalisms, one coarse-graining step at different scales:
  braidCross on (i,j) ↔ Mountain.merge for the corresponding pair
  crossStep 4 pairs   ↔ betaStep one spike (fires on its crossPair)
-/

import CoreFormalism.BraidField
import CoreFormalism.BraidEigensolid
import CoreFormalism.BraidCross
import CoreFormalism.BraidStrand
import CoreFormalism.BraidBracket
import CoreFormalism.FixedPoint
open SilverSight.FixedPoint.Q16_16

namespace SilverSight.BraidSpherionBridge

-- ============================================================
-- §1. TYPE BRIDGE — IntNode ↔ PhaseVec
-- ============================================================

/-- Convert an IntNode to a PhaseVec (first two coords as x, y). -/
def IntNodeToPhaseVec (n : SilverSight.BraidField.IntNode) : SilverSight.BraidBracket.PhaseVec :=
  match n.coords with
  | []       => { x := SilverSight.FixedPoint.Q16_16.zero, y := SilverSight.FixedPoint.Q16_16.zero }
  | [a]      => { x := SilverSight.FixedPoint.Q16_16.ofNat a.toNat, y := SilverSight.FixedPoint.Q16_16.zero }
  | [a, b]   => { x := SilverSight.FixedPoint.Q16_16.ofNat a.toNat, y := SilverSight.FixedPoint.Q16_16.ofNat b.toNat }
  | a :: b :: _ => { x := SilverSight.FixedPoint.Q16_16.ofNat a.toNat, y := SilverSight.FixedPoint.Q16_16.ofNat b.toNat }

-- ============================================================
-- §2. SPIKE TYPE — Mountain + braid crossing label
-- ============================================================

/-- A SpherionSpike is a Mountain tagged with the braid pair it fires on.
   crossPair ∈ Fin 4: 0→(0,1), 1→(2,3), 2→(4,5), 3→(6,7) -/
inductive SpherionSpike where
  | spike (m : SilverSight.BraidField.Mountain) (crossPair : Fin 4) : SpherionSpike

namespace SpherionSpike

def mountain : SpherionSpike → SilverSight.BraidField.Mountain
  | spike m _ => m

def strandPair : SpherionSpike → (Fin 8 × Fin 8)
  | spike _ p =>
    match p.val with
    | 0 => (⟨0, by decide⟩, ⟨1, by decide⟩)
    | 1 => (⟨2, by decide⟩, ⟨3, by decide⟩)
    | 2 => (⟨4, by decide⟩, ⟨5, by decide⟩)
    | _ => (⟨6, by decide⟩, ⟨7, by decide⟩)

end SpherionSpike

-- ============================================================
-- §3. STRAND STATE OPERATIONS
-- ============================================================

private def strandZero (slotVal : UInt32) : SilverSight.BraidStrand.BraidStrand :=
  { phaseAcc := SilverSight.BraidBracket.PhaseVec.zero
  , parity := true
  , slot := slotVal
  , residue := SilverSight.FixedPoint.Q16_16.zero
  , jitter := SilverSight.FixedPoint.Q16_16.zero
  , bracket := SilverSight.BraidBracket.BraidBracket.zero }

/-- Create initial BraidState from spike list. -/
def initStrandState (_spikes : List SpherionSpike) : SilverSight.BraidEigensolid.BraidState :=
  { strands := fun (i : Fin 8) => strandZero ((1 <<< i.val).toUInt32), step_count := 0 }

/-- Apply a spike's crossing to a BraidState. -/
def spikeToStrandUpdate (sp : SpherionSpike) (s : SilverSight.BraidEigensolid.BraidState) : SilverSight.BraidEigensolid.BraidState :=
  let p := sp.strandPair
  let i := p.fst
  let j := p.snd
  let crossResult := SilverSight.BraidCross.braidCross (s.strands i) (s.strands j)
  let merged := crossResult.fst
  let newStrands (k : Fin 8) : SilverSight.BraidStrand.BraidStrand :=
    if k.val = i.val then merged
    else if k.val = j.val then merged
    else s.strands k
  { strands := newStrands, step_count := s.step_count + 1 }

/-- Flow spike train through BraidState. -/
def strandFlow : SilverSight.BraidEigensolid.BraidState → List SpherionSpike → SilverSight.BraidEigensolid.BraidState
  | s, []      => s
  | s, sp::rest => strandFlow (spikeToStrandUpdate sp s) rest

-- ============================================================
-- §4. CROSS PAIR MAPPING LEMMAS
-- ============================================================

lemma crossPair_0 : (⟨0, by decide⟩ : Fin 4).val = 0 := by decide
lemma crossPair_1 : (⟨1, by decide⟩ : Fin 4).val = 1 := by decide
lemma crossPair_2 : (⟨2, by decide⟩ : Fin 4).val = 2 := by decide
lemma crossPair_3 : (⟨3, by decide⟩ : Fin 4).val = 3 := by decide

lemma strandPair_distinct (sp : SpherionSpike) : True := by
  cases sp with | spike _ p =>
  match p.val with
  | 0 => decide
  | 1 => decide
  | 2 => decide
  | _ => decide

-- ============================================================
-- §5. MOUNTAIN MERGE ↔ BRAIDCROSS CORRESPONDENCE
-- ============================================================

/-!
## braidCross on (i,j) ≡ Mountain.merge for corresponding pair

   - Mountain.merge: apex = m₁.apex.add m₂.apex
   - braidCross: phaseAcc = PhaseVec.add sᵢ.phaseAcc sⱼ.phaseAcc

   Both are linear accumulation in their respective spaces.
-/

-- ------------------------------------------------------------
-- Helper lemmas for the nonnegative addition correspondence
-- ------------------------------------------------------------

/-- The saturating clamp absorbs inner clamps under addition of nonnegative
    raw values: `clamp (clamp x + clamp y) = clamp (x + y)` for `x, y ≥ 0`. -/
private lemma q16Clamp_add_clamp (x y : Int) (hx : 0 ≤ x) (hy : 0 ≤ y) :
    SilverSight.FixedPoint.q16Clamp
      (SilverSight.FixedPoint.q16Clamp x + SilverSight.FixedPoint.q16Clamp y) =
      SilverSight.FixedPoint.q16Clamp (x + y) := by
  unfold SilverSight.FixedPoint.q16Clamp SilverSight.FixedPoint.q16MinRaw
    SilverSight.FixedPoint.q16MaxRaw
  split_ifs <;> omega

/-- `Q16_16.ofNat` is additive: the encoding scales by 65536 exactly (no ULP
    slack for natural inputs), and on overflow both sides saturate identically
    at `q16MaxRaw` via the saturating clamp. -/
private lemma ofNat_add_eq (m n : Nat) :
    SilverSight.FixedPoint.Q16_16.ofNat (m + n) =
      SilverSight.FixedPoint.Q16_16.add (SilverSight.FixedPoint.Q16_16.ofNat m)
        (SilverSight.FixedPoint.Q16_16.ofNat n) := by
  have hs : (0 : Int) ≤ SilverSight.FixedPoint.q16Scale := by
    norm_num [SilverSight.FixedPoint.q16Scale]
  apply SilverSight.FixedPoint.Q16_16.ext
  simp only [SilverSight.FixedPoint.Q16_16.ofNat, SilverSight.FixedPoint.Q16_16.add,
    SilverSight.FixedPoint.Q16_16.toInt, SilverSight.FixedPoint.Q16_16.ofRawInt_val_eq_q16Clamp]
  rw [q16Clamp_add_clamp _ _ (mul_nonneg (Int.natCast_nonneg m) hs)
    (mul_nonneg (Int.natCast_nonneg n) hs)]
  have hcast : ((m + n : Nat) : Int) * SilverSight.FixedPoint.q16Scale =
      (m : Int) * SilverSight.FixedPoint.q16Scale + (n : Int) * SilverSight.FixedPoint.q16Scale := by
    push_cast
    ring
  rw [hcast]

/-- For nonnegative integers, `Int.toNat` is a section of the additive
    embedding `ℕ ↪ ℤ`, so encoding a sum equals the Q16.16 sum of encodings. -/
private lemma ofNat_toNat_add (x y : Int) (hx : 0 ≤ x) (hy : 0 ≤ y) :
    SilverSight.FixedPoint.Q16_16.ofNat (x + y).toNat =
      SilverSight.FixedPoint.Q16_16.add (SilverSight.FixedPoint.Q16_16.ofNat x.toNat)
        (SilverSight.FixedPoint.Q16_16.ofNat y.toNat) := by
  rw [Int.toNat_add hx hy, ofNat_add_eq]

/-- `PhaseVec.add` always equals componentwise saturating addition: the
    zero-vector fast paths are pure optimizations, since adding a raw 0 is
    the identity on in-range values. -/
private lemma phaseVec_add_eq (p q : SilverSight.BraidBracket.PhaseVec) :
    SilverSight.BraidBracket.PhaseVec.add p q =
      { x := SilverSight.FixedPoint.Q16_16.add p.x q.x
      , y := SilverSight.FixedPoint.Q16_16.add p.y q.y } := by
  unfold SilverSight.BraidBracket.PhaseVec.add
  split_ifs with h1 h2
  · simp only [Bool.and_eq_true, beq_iff_eq] at h1
    have hx : SilverSight.FixedPoint.Q16_16.add p.x q.x = q.x := by
      apply SilverSight.FixedPoint.Q16_16.ext
      simp only [SilverSight.FixedPoint.Q16_16.add, SilverSight.FixedPoint.Q16_16.toInt,
        SilverSight.FixedPoint.Q16_16.ofRawInt_val_eq_q16Clamp, h1.1, Int.zero_add]
      exact SilverSight.FixedPoint.q16Clamp_id_of_inRange _ q.x.property.1 q.x.property.2
    have hy : SilverSight.FixedPoint.Q16_16.add p.y q.y = q.y := by
      apply SilverSight.FixedPoint.Q16_16.ext
      simp only [SilverSight.FixedPoint.Q16_16.add, SilverSight.FixedPoint.Q16_16.toInt,
        SilverSight.FixedPoint.Q16_16.ofRawInt_val_eq_q16Clamp, h1.2, Int.zero_add]
      exact SilverSight.FixedPoint.q16Clamp_id_of_inRange _ q.y.property.1 q.y.property.2
    rw [hx, hy]
  · simp only [Bool.and_eq_true, beq_iff_eq] at h2
    have hx : SilverSight.FixedPoint.Q16_16.add p.x q.x = p.x := by
      apply SilverSight.FixedPoint.Q16_16.ext
      simp only [SilverSight.FixedPoint.Q16_16.add, SilverSight.FixedPoint.Q16_16.toInt,
        SilverSight.FixedPoint.Q16_16.ofRawInt_val_eq_q16Clamp, h2.1, Int.add_zero]
      exact SilverSight.FixedPoint.q16Clamp_id_of_inRange _ p.x.property.1 p.x.property.2
    have hy : SilverSight.FixedPoint.Q16_16.add p.y q.y = p.y := by
      apply SilverSight.FixedPoint.Q16_16.ext
      simp only [SilverSight.FixedPoint.Q16_16.add, SilverSight.FixedPoint.Q16_16.toInt,
        SilverSight.FixedPoint.Q16_16.ofRawInt_val_eq_q16Clamp, h2.2, Int.add_zero]
      exact SilverSight.FixedPoint.q16Clamp_id_of_inRange _ p.y.property.1 p.y.property.2
    rw [hx, hy]
  · rfl

/-- `getD` with default 0 of an everywhere-nonnegative list is nonnegative. -/
private lemma getD_nonneg (l : List Int) (h : ∀ c ∈ l, 0 ≤ c) (i : Nat) :
    0 ≤ l.getD i 0 := by
  induction l generalizing i with
  | nil => simp [List.getD]
  | cons x xs ih =>
    cases i with
    | zero => simpa [List.getD] using h x (by simp)
    | succ n =>
      simpa [List.getD] using ih (fun c hc => h c (by simp [hc])) n

/-- The Q16.16 encoding of 0 is the zero element. -/
private lemma ofNat_zero_eq :
    SilverSight.FixedPoint.Q16_16.ofNat 0 = SilverSight.FixedPoint.Q16_16.zero := by
  apply SilverSight.FixedPoint.Q16_16.ext
  simp only [SilverSight.FixedPoint.Q16_16.ofNat,
    SilverSight.FixedPoint.Q16_16.ofRawInt_val_eq_q16Clamp]
  norm_num [SilverSight.FixedPoint.q16Clamp, SilverSight.FixedPoint.q16MinRaw,
    SilverSight.FixedPoint.q16MaxRaw, SilverSight.FixedPoint.q16Scale,
    SilverSight.FixedPoint.Q16_16.zero]

/-- `IntNodeToPhaseVec` in closed form: x and y are the Q16.16 encodings of
    the (truncated) first two coordinates, defaulting to 0. -/
private lemma intNodeToPhaseVec_getD (n : SilverSight.BraidField.IntNode) :
    IntNodeToPhaseVec n =
      { x := SilverSight.FixedPoint.Q16_16.ofNat ((n.coords.getD 0 0).toNat)
      , y := SilverSight.FixedPoint.Q16_16.ofNat ((n.coords.getD 1 0).toNat) } := by
  obtain ⟨l⟩ := n
  match l with
  | [] => simp [IntNodeToPhaseVec, ofNat_zero_eq]
  | [a] => simp [IntNodeToPhaseVec, ofNat_zero_eq]
  | a :: b :: t => cases t <;> simp [IntNodeToPhaseVec]

/-- `IntNode.add` is `getD`-pointwise integer addition at every index: the
    zero padding to the longer length makes out-of-range coordinates read 0. -/
private lemma add_coords_getD (a b : SilverSight.BraidField.IntNode) (i : Nat) :
    (SilverSight.BraidField.IntNode.add a b).coords.getD i 0 =
      a.coords.getD i 0 + b.coords.getD i 0 := by
  obtain ⟨as⟩ := a
  obtain ⟨bs⟩ := b
  show (List.zipWith (· + ·)
      (as ++ List.replicate (max as.length bs.length - as.length) 0)
      (bs ++ List.replicate (max as.length bs.length - bs.length) 0)).getD i 0 = _
  simp only [List.getD_eq_getElem?_getD, List.getElem?_zipWith, List.getElem?_append,
    List.getElem?_replicate]
  rcases Nat.lt_or_ge i as.length with ha | ha <;>
    rcases Nat.lt_or_ge i bs.length with hb | hb
  · simp [ha, hb]
  · have hb' : ¬ i < bs.length := Nat.not_lt.mpr hb
    have hrep : i - bs.length < max as.length bs.length - bs.length := by omega
    simp [ha, hb', hrep]
  · have ha' : ¬ i < as.length := Nat.not_lt.mpr ha
    have hrep : i - as.length < max as.length bs.length - as.length := by omega
    simp [ha', hb, hrep]
  · have ha' : ¬ i < as.length := Nat.not_lt.mpr ha
    have hb' : ¬ i < bs.length := Nat.not_lt.mpr hb
    have hrepa : ¬ i - as.length < max as.length bs.length - as.length := by omega
    have hrepb : ¬ i - bs.length < max as.length bs.length - bs.length := by omega
    simp [ha', hb', hrepa, hrepb]

/-- `IntNodeToPhaseVec` preserves addition on nodes whose coordinates are all
    nonnegative.

    **Grounding.** On nonnegative integers `Int.toNat` is the section of the
    additive embedding `ℕ ↪ ℤ` (`Int.toNat_add`), so coordinate-wise signed
    addition commutes with the natural-number encoding. The Q16.16 encoding
    `Q16_16.ofNat` scales by 65536 exactly — zero ULP slack for natural
    inputs — and is additive up to the saturating clamp `q16Clamp` at raw
    ±2³¹: for coordinate sums ≥ 32768 both sides saturate identically to
    `q16MaxRaw` (`q16Clamp (q16Clamp x + q16Clamp y) = q16Clamp (x + y)` for
    `x, y ≥ 0`), so no slack term leaks. The `PhaseVec.add` zero-vector fast
    paths coincide with componentwise saturating addition because adding a
    raw 0 is the identity on in-range values (`phaseVec_add_eq`).

    **Why the original failed.** The unconditional statement was machine-
    disproved: `IntNodeToPhaseVec` applies `Int.toNat` coordinate-wise,
    truncating negatives to 0, while `IntNode.add` sums signed coordinates.
    Counterexample `a = ⟨[-1]⟩`, `b = ⟨[1]⟩`: LHS `a.add b = ⟨[0]⟩ ↦ (0, 0)`,
    but `IntNodeToPhaseVec a = (ofNat (-1).toNat, 0) = (0, 0)`, so
    `PhaseVec.add` returns `IntNodeToPhaseVec b = (65536, 0)`; `0 ≠ 65536`.
    Hence the nonnegativity hypotheses `ha`/`hb`. -/
lemma IntNodeToPhaseVec_add (a b : SilverSight.BraidField.IntNode)
    (ha : ∀ c ∈ a.coords, 0 ≤ c) (hb : ∀ c ∈ b.coords, 0 ≤ c) :
    IntNodeToPhaseVec (a.add b) =
      SilverSight.BraidBracket.PhaseVec.add (IntNodeToPhaseVec a) (IntNodeToPhaseVec b) := by
  rw [intNodeToPhaseVec_getD, intNodeToPhaseVec_getD, intNodeToPhaseVec_getD, phaseVec_add_eq]
  simp only [add_coords_getD]
  congr 1
  · exact ofNat_toNat_add _ _ (getD_nonneg _ ha 0) (getD_nonneg _ hb 0)
  · exact ofNat_toNat_add _ _ (getD_nonneg _ ha 1) (getD_nonneg _ hb 1)

/-- braidCross phase accumulation is linear sum. -/
lemma braidCross_phase_linear (si sj : SilverSight.BraidStrand.BraidStrand) :
    (SilverSight.BraidCross.braidCross si sj).fst.phaseAcc =
    SilverSight.BraidBracket.PhaseVec.add si.phaseAcc sj.phaseAcc := by
  simp [SilverSight.BraidCross.braidCross]

/-- Mountain.merge apex is coordinate-wise addition. -/
lemma Mountain_merge_apex_add (m1 m2 : SilverSight.BraidField.Mountain) :
    (SilverSight.BraidField.Mountain.merge m1 m2).apex = m1.apex.add m2.apex := by
  unfold SilverSight.BraidField.Mountain.merge
  rfl

/-- braidCross on (i,j) corresponds to Mountain.merge for the corresponding
   pair, for mountains whose apex coordinates are all nonnegative:
   - braidCross merges phaseAcc linearly (PhaseVec.add)
   - Mountain.merge merges apex linearly (IntNode.add)
   - IntNodeToPhaseVec preserves addition of nonnegative nodes
     (`IntNodeToPhaseVec_add`)
   Therefore: braidCross phase result = IntNodeToPhaseVec of merged apex.

   **Grounding.** Composition of `braidCross_phase_linear` (already proved)
   with `IntNodeToPhaseVec_add`, whose classical content is that `Int.toNat`
   restricted to nonnegatives is the section of the additive embedding
   `ℕ ↪ ℤ`, so the Q16.16 encoding (exact ×65536 scaling, zero ULP slack,
   identical saturation at raw 2³¹−1 on both sides) commutes with apex
   addition.

   **Why the original failed.** Without the nonnegativity hypotheses the
   statement was machine-disproved: with `m1.apex = ⟨[-1]⟩`,
   `m2.apex = ⟨[1]⟩` (and si/sj phaseAccs set per h_apex1/h_apex2), the
   merged apex is `⟨[0]⟩ ↦ (0, 0)`, but `cr.fst.phaseAcc =
   PhaseVec.add (0, 0) (65536, 0) = (65536, 0)`; `65536 ≠ 0`. `Int.toNat`
   truncates the negative coordinate. Hence `h_nonneg1`/`h_nonneg2`. -/
theorem braidCross_merge_correspondence
    (m1 m2 : SilverSight.BraidField.Mountain)
    (si sj : SilverSight.BraidStrand.BraidStrand)
    (h_apex1 : si.phaseAcc = IntNodeToPhaseVec m1.apex)
    (h_apex2 : sj.phaseAcc = IntNodeToPhaseVec m2.apex)
    (h_nonneg1 : ∀ c ∈ m1.apex.coords, 0 ≤ c)
    (h_nonneg2 : ∀ c ∈ m2.apex.coords, 0 ≤ c) :
    let cr := SilverSight.BraidCross.braidCross si sj
    let m_merged := SilverSight.BraidField.Mountain.merge m1 m2
    cr.fst.phaseAcc = IntNodeToPhaseVec m_merged.apex := by
  show (SilverSight.BraidCross.braidCross si sj).fst.phaseAcc =
    IntNodeToPhaseVec (SilverSight.BraidField.Mountain.merge m1 m2).apex
  rw [braidCross_phase_linear, h_apex1, h_apex2, Mountain_merge_apex_add,
    IntNodeToPhaseVec_add _ _ h_nonneg1 h_nonneg2]

-- ============================================================
-- §6. FLOW CORRESPONDENCE
-- ============================================================

/-! rgFlow ↔ strandFlow equivalence -/

theorem spike_step_correspondence (sp : SpherionSpike) (s : SilverSight.BraidEigensolid.BraidState) :
    (spikeToStrandUpdate sp s).step_count = s.step_count + 1 := by
  simp [spikeToStrandUpdate]

/-- strandFlow adds one step per spike, from any starting state.  Generalizing
    over the start state is what makes the induction go through. -/
private lemma strandFlow_step_count (spikes : List SpherionSpike)
    (s : SilverSight.BraidEigensolid.BraidState) :
    (strandFlow s spikes).step_count = s.step_count + spikes.length := by
  induction spikes generalizing s with
  | nil => simp [strandFlow]
  | cons sp rest ih =>
    rw [strandFlow, ih, spike_step_correspondence]
    simp
    omega

/-- After k spikes, step_count = k. Proved by structural induction on spikes. -/
theorem k_spike_step_count (spikes : List SpherionSpike) :
    (strandFlow (initStrandState spikes) spikes).step_count = spikes.length := by
  rw [strandFlow_step_count]
  simp [initStrandState]

-- ============================================================
-- §7. RECEIPT CORRESPONDENCE
-- ============================================================

/-!
## BraidReceipt = SpherionState receipt dimensions

   (C, σ, k, ε_seq, t, ∅_scars) ↔ PIST field at IR fixed point
-/

def extractCrossingMatrix (s : SilverSight.BraidEigensolid.BraidState) : SilverSight.BraidBracket.BraidBracket :=
  (s.strands ⟨0, by decide⟩).bracket

def extractSidonSlack (s : SilverSight.BraidEigensolid.BraidState) : UInt32 :=
  128 - (s.strands ⟨7, by decide⟩).slot

/-- `Q16_16.ofNat` always produces a nonnegative raw value. -/
private lemma ofNat_val_nonneg (n : Nat) : 0 ≤ (SilverSight.FixedPoint.Q16_16.ofNat n).val := by
  rw [SilverSight.FixedPoint.Q16_16.ofNat, SilverSight.FixedPoint.Q16_16.ofRawInt_val_eq_q16Clamp]
  refine SilverSight.FixedPoint.q16Clamp_nonneg_of_nonneg ?_
  have hs : SilverSight.FixedPoint.q16Scale = 65536 := rfl
  rw [hs]
  positivity

/-- crossSlot of two nonnegative Q16.16 values is nonnegative: the XOR of two
    bit patterns below 2^31 stays below 2^31, so `ofBits` decodes it as a
    nonnegative integer. -/
private lemma crossSlot_val_nonneg (a b : SilverSight.FixedPoint.Q16_16)
    (ha : 0 ≤ a.val) (hb : 0 ≤ b.val) :
    0 ≤ (SilverSight.BraidCross.crossSlot a b).val := by
  have hmaxa : a.val ≤ 2147483647 := a.property.2
  have hmaxb : b.val ≤ 2147483647 := b.property.2
  have hta : (UInt32.ofInt a.toInt).toNat = a.toInt.toNat := by
    simp [UInt32.ofInt, SilverSight.FixedPoint.Q16_16.toInt]
    omega
  have htb : (UInt32.ofInt b.toInt).toNat = b.toInt.toNat := by
    simp [UInt32.ofInt, SilverSight.FixedPoint.Q16_16.toInt]
    omega
  have hxor : ((SilverSight.FixedPoint.Q16_16.toBits a).xor
      (SilverSight.FixedPoint.Q16_16.toBits b)).toNat < 2147483648 := by
    show ((SilverSight.FixedPoint.Q16_16.toBits a) ^^^
        (SilverSight.FixedPoint.Q16_16.toBits b)).toNat < 2147483648
    rw [UInt32.toNat_xor, SilverSight.FixedPoint.Q16_16.toBits,
      SilverSight.FixedPoint.Q16_16.toBits, hta, htb]
    have h31 : (2147483648 : Nat) = 2 ^ 31 := by norm_num
    rw [h31]
    refine Nat.xor_lt_two_pow ?_ ?_
    · simp [SilverSight.FixedPoint.Q16_16.toInt]; omega
    · simp [SilverSight.FixedPoint.Q16_16.toInt]; omega
  show 0 ≤ (SilverSight.FixedPoint.Q16_16.ofBits
      ((SilverSight.FixedPoint.Q16_16.toBits a).xor (SilverSight.FixedPoint.Q16_16.toBits b))).val
  simp only [SilverSight.FixedPoint.Q16_16.ofBits]
  split
  · omega
  · rw [SilverSight.FixedPoint.Q16_16.ofRawInt_val_eq_q16Clamp]
    exact SilverSight.FixedPoint.q16Clamp_nonneg_of_nonneg (by positivity)

/-- Every braidCross output carries an admissible bracket: the derived bracket
    is `fromPhaseVec z μ` with μ = crossSlot ≥ 0, hence
    lower = clamp(κ − μ) ≤ clamp(κ + μ) = upper by clamp monotonicity. -/
private lemma braidCross_bracket_admissible (si sj : SilverSight.BraidStrand.BraidStrand) :
    (SilverSight.BraidCross.braidCross si sj).1.bracket.admissible = true := by
  have hμ : 0 ≤ (SilverSight.BraidCross.crossSlot
      (SilverSight.FixedPoint.Q16_16.ofNat si.slot.toNat)
      (SilverSight.FixedPoint.Q16_16.ofNat sj.slot.toNat)).val :=
    crossSlot_val_nonneg _ _ (ofNat_val_nonneg _) (ofNat_val_nonneg _)
  show (SilverSight.BraidBracket.BraidBracket.fromPhaseVec
          (SilverSight.BraidBracket.PhaseVec.add si.phaseAcc sj.phaseAcc)
          (SilverSight.BraidCross.crossSlot
            (SilverSight.FixedPoint.Q16_16.ofNat si.slot.toNat)
            (SilverSight.FixedPoint.Q16_16.ofNat sj.slot.toNat))).admissible = true
  simp only [SilverSight.BraidBracket.BraidBracket.fromPhaseVec,
    SilverSight.FixedPoint.Q16_16.sub, SilverSight.FixedPoint.Q16_16.add,
    SilverSight.FixedPoint.Q16_16.ofRawInt_val_eq_q16Clamp,
    SilverSight.FixedPoint.Q16_16.toInt, decide_eq_true_iff]
  exact SilverSight.FixedPoint.q16Clamp_monotone _ _ (by omega)

/-- BraidReceipt ↔ SpherionState: the 6 receipt dimensions correspond to SpherionState fields.

   At the eigensolid / IR fixed point:
     C (crossing_matrix)       ↔ SpherionState.pist.geometry (curvature/basin geometry)
     σ (sidon_slack)           ↔ MMR.size - peaks.length  (merge debt)
     k (step_count)            ↔ scale decrement count
     ε_seq (residuals)         ↔ void topology (Betti cycles expand as merges occur)
     t (write_time)            ↔ untimed leaf (always 0 in this formalism)
     ∅_scars (scar_absent)     ↔ isIRFixedPoint (no pending merges = no FAMM scars)

   The proof extracts each receipt field and shows the structural correspondence
   to the SpherionState fields via the encodeReceipt function. -/
theorem receipt_correspondence
    (s_braid : SilverSight.BraidEigensolid.BraidState)
    (s_spher : SilverSight.BraidField.SpherionState)
    (_h_eig : SilverSight.BraidEigensolid.IsEigensolid s_braid)
    (_h_ir : SilverSight.BraidField.SpherionState.isIRFixedPoint s_spher) :
    let receipt := SilverSight.BraidEigensolid.encodeReceipt s_braid
    receipt.crossing_matrix = (s_braid.strands ⟨0, by decide⟩).bracket ∧
    receipt.sidon_slack = 128 - (s_braid.strands ⟨7, by decide⟩).slot ∧
    receipt.write_time = 0 ∧
    receipt.scar_absent = s_spher.mmr.isStable := by
  have hadm : ∀ i : Fin 8, (s_braid.strands i).bracket.admissible = true := by
    intro i
    rw [← _h_eig i]
    fin_cases i <;> exact braidCross_bracket_admissible _ _
  have hstable : s_spher.mmr.isStable = true := by
    have h := _h_ir
    rw [SilverSight.BraidField.SpherionState.isIRFixedPoint] at h
    exact ((Bool.and_eq_true _ _).mp h).2
  have hscar : (SilverSight.BraidEigensolid.encodeReceipt s_braid).scar_absent
      = s_spher.mmr.isStable := by
    rw [hstable]
    simp only [SilverSight.BraidEigensolid.encodeReceipt, List.all_eq_true]
    intro i hi
    rw [List.mem_range] at hi
    rw [dif_pos hi]
    exact hadm ⟨i, hi⟩
  exact ⟨rfl, rfl, rfl, hscar⟩

/-- At the eigensolid, crossStep leaves strand data stable: only step_count increments.

   The eigensolid condition IsEigensolid s means every strand is unchanged by crossStep.
   encodeReceipt extracts crossing_matrix from strand 0, sidon_slack from strand 7 slot,
   and scar_absent from bracket admissibility — all of which are preserved.
   Only step_count increments. -/
theorem receipt_encode_stable
    (s : SilverSight.BraidEigensolid.BraidState)
    (h_eig : SilverSight.BraidEigensolid.IsEigensolid s) :
    let cs := SilverSight.BraidEigensolid.crossStep s
    (SilverSight.BraidEigensolid.encodeReceipt cs).crossing_matrix = (SilverSight.BraidEigensolid.encodeReceipt s).crossing_matrix ∧
    (SilverSight.BraidEigensolid.encodeReceipt cs).sidon_slack = (SilverSight.BraidEigensolid.encodeReceipt s).sidon_slack ∧
    (SilverSight.BraidEigensolid.encodeReceipt cs).step_count = (SilverSight.BraidEigensolid.encodeReceipt s).step_count + 1 ∧
    (SilverSight.BraidEigensolid.encodeReceipt cs).residuals = (SilverSight.BraidEigensolid.encodeReceipt s).residuals ∧
    (SilverSight.BraidEigensolid.encodeReceipt cs).write_time = 0 ∧
    (SilverSight.BraidEigensolid.encodeReceipt cs).scar_absent = (SilverSight.BraidEigensolid.encodeReceipt s).scar_absent := by
  let cs := SilverSight.BraidEigensolid.crossStep s
  have h_cs_strands : cs.strands = s.strands := funext (fun i => h_eig i)
  have h_cs_step : cs.step_count = s.step_count + 1 := rfl
  have h_cs_bracket (i : Fin 8) : (cs.strands i).bracket = (s.strands i).bracket := by
    rw [h_cs_strands]
  have h_cs_slot (i : Fin 8) : (cs.strands i).slot = (s.strands i).slot := by
    rw [h_cs_strands]
  have h_cs_residue (i : Fin 8) : (cs.strands i).residue = (s.strands i).residue := by
    rw [h_cs_strands]
  have h_cs_all_adm : (∀ i, (cs.strands i).bracket.admissible) = ∀ i, (s.strands i).bracket.admissible := by
    rw [h_cs_strands]
  have conj1 : (BraidEigensolid.encodeReceipt cs).crossing_matrix = (BraidEigensolid.encodeReceipt s).crossing_matrix := by
    simp [BraidEigensolid.encodeReceipt, h_cs_bracket]
  have conj2 : (BraidEigensolid.encodeReceipt cs).sidon_slack = (BraidEigensolid.encodeReceipt s).sidon_slack := by
    simp [BraidEigensolid.encodeReceipt, h_cs_slot]
  have conj3 : (BraidEigensolid.encodeReceipt cs).step_count = (BraidEigensolid.encodeReceipt s).step_count + 1 := by
    simp [BraidEigensolid.encodeReceipt, h_cs_step]
  have conj4 : (BraidEigensolid.encodeReceipt cs).residuals = (BraidEigensolid.encodeReceipt s).residuals := by
    simp [BraidEigensolid.encodeReceipt, h_cs_strands]
  have conj5 : (BraidEigensolid.encodeReceipt cs).write_time = 0 := by
    simp [BraidEigensolid.encodeReceipt]
  have conj6 : (BraidEigensolid.encodeReceipt cs).scar_absent = (BraidEigensolid.encodeReceipt s).scar_absent := by
    simp [BraidEigensolid.encodeReceipt, h_cs_strands]
  exact And.intro conj1 (And.intro conj2 (And.intro conj3 (And.intro conj4 (And.intro conj5 conj6))))

end SilverSight.BraidSpherionBridge