Research-Stack/0-Core-Formalism/lean/Semantics/Semantics/BraidBitwiseODE.lean

/- Copyright (c) 2026 Sovereign Research Stack. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Research Stack Team

BraidBitwiseODE.lean — Bitwise ODE integration for braid crossings

Replaces continuous O(1) integration with XOR-based bitwise operations
on Q16.16 fixed-point values.  Pattern derived from PistBridge's BlitterState
discrete Picard integral.

Hierarchy: PistBridge BlitterState → BraidBitwiseODE crossing + integration

Per AGENTS.md §0: Lean is the source of truth.
-/

import Semantics.FixedPoint
import Semantics.BraidStrand

namespace Semantics.BraidBitwiseODE

open Semantics
open Semantics.FixedPoint
open Semantics.BraidStrand

-- ════════════════════════════════════════════════════════════
-- §1  Bitwise Crossing Operation
-- ════════════════════════════════════════════════════════════

/-- XOR-based braid crossing step.

    Models a crossing between two strands as a bitwise operation
    on their Q16.16 payloads.  Parity of each strand determines
    the crossing sign (over/under).

    Pattern: M_{k+1} = M_k ⊕ F(a,b,ε) from PistBridge §3. -/
def bitwiseCrossStep (a b : BraidStrand) : BraidStrand :=
  let pa := a.phaseAcc
  let pb := b.phaseAcc
  -- XOR the phase accumulations' bit patterns
  let newX := Q16_16.ofBits (pa.x.toBits ^^^ pb.x.toBits)
  let newY := Q16_16.ofBits (pa.y.toBits ^^^ pb.y.toBits)
  -- Swap parity to indicate crossing
  let newParity := !a.parity
  -- Accumulate residue: XOR with crossing signal
  let crossSignal := Q16_16.ofBits (a.residue.toBits ^^^ b.residue.toBits)
  { phaseAcc := { x := newX, y := newY }
  , parity := newParity
  , slot := a.slot
  , residue := crossSignal
  , jitter := a.jitter
  , bracket := a.bracket }


-- ════════════════════════════════════════════════════════════
-- §2  O(1) ODE Integration Step
-- ════════════════════════════════════════════════════════════

/-- Discrete Picard integral: O(1) bitwise ODE integration.

    Replaces continuous ODE solver with a single bitwise accumulation.
    From PistBridge: M_{k+1} = M_k ⊕ (state + input) >> 16

    This is the Blitter operation: accumulate state and input via
    XOR with right-shift, giving a single-step ODE approximation. -/
def bitwiseODEIntegrate (state : Q16_16) (input : Q16_16) : Q16_16 :=
  -- Combine state and input via addition, then XOR-accumulate
  let combined := Q16_16.ofNat ((state.toBits.toNat + input.toBits.toNat) % (2^32))
  -- Right-shift by 16 to extract the integer portion effect
  let shifted := Q16_16.ofBits ((combined.toBits.toNat >>> 16).toUInt32)
  -- XOR with original state for the Blitter accumulation
  Q16_16.ofBits (state.toBits ^^^ shifted.toBits)


/-- Multi-step bitwise ODE integration.

    Applies the bitwise ODE integrator iteratively over a sequence
    of input values, accumulating into the state. -/
def bitwiseODEIntegrateSeq (state : Q16_16) (inputs : List Q16_16) : Q16_16 :=
  inputs.foldl bitwiseODEIntegrate state


-- ════════════════════════════════════════════════════════════
-- §3  Braid Strand ODE Integration
-- ════════════════════════════════════════════════════════════

/-- Integrate a braid strand's phase accumulation via bitwise ODE.

    Applies the discrete Picard integral to both x and y components
    of the strand's phase vector. -/
def integrateStrand (strand : BraidStrand) (input : Q16_16) : BraidStrand :=
  let newX := bitwiseODEIntegrate strand.phaseAcc.x input
  let newY := bitwiseODEIntegrate strand.phaseAcc.y input
  { strand with phaseAcc := { x := newX, y := newY } }


/-- Two-strand crossing with integrated ODE step.

    Combines bitwiseCrossStep with ODE integration in a single
    atomic operation: cross, then integrate the result. -/
def crossingODEStep (a b : BraidStrand) : BraidStrand × BraidStrand :=
  let crossed := bitwiseCrossStep a b
  let integrated := integrateStrand crossed a.residue
  (integrated, crossed)


-- ════════════════════════════════════════════════════════════
-- §4  Fixed-Point Invariants
-- ════════════════════════════════════════════════════════════

/-- The bitwise ODE integrator preserves Q16.16 range.

    Since all operations (XOR, shift, ofBits) produce valid Q16_16
    values, the output is always in the representable range. -/
theorem bitwise_ode_preserves_range (state input : Q16_16) :
    q16MinRaw ≤ (bitwiseODEIntegrate state input).toInt ∧
    (bitwiseODEIntegrate state input).toInt ≤ q16MaxRaw := by
  unfold bitwiseODEIntegrate
  exact ⟨(Q16_16.ofBits _).property.left, (Q16_16.ofBits _).property.right⟩


/-- Bitwise cross step preserves strand slot identity.

    The slot field is carried through from the first strand. -/
theorem cross_step_preserves_slot (a b : BraidStrand) :
    (bitwiseCrossStep a b).slot = a.slot := by
  unfold bitwiseCrossStep
  rfl


-- ════════════════════════════════════════════════════════════
-- §5  Convergence (Placeholder)
-- ════════════════════════════════════════════════════════════

/-- TODO(lean-port): Prove that bitwise ODE integration converges
    for bounded inputs.  This requires showing that repeated application
    of `bitwiseODEIntegrate` reaches a fixed point (absorbing state).

    Conjecture: for any state s and bounded input sequence,
    bitwiseODEIntegrateSeq reaches a fixed point after at most
    32 steps (the bit width of Q16.16). -/
theorem bitwise_ode_correct (state : Q16_16) (h : state.toInt = 0) :
    bitwiseODEIntegrate state state = state := by
  -- state.toInt = 0 means state is the zero Q16.16 value
  rw [Q16_16.toInt_eq_zero_iff] at h
  subst h
  -- Goal: bitwiseODEIntegrate zero zero = zero
  -- All intermediate values (toBits 0, ofNat 0, ofBits 0, XOR 0 0) reduce to zero
  native_decide


-- ════════════════════════════════════════════════════════════
-- §6  Verification Examples
-- ════════════════════════════════════════════════════════════

#eval bitwiseODEIntegrate (Q16_16.ofInt 2) (Q16_16.ofInt 3)
#eval bitwiseODEIntegrate (Q16_16.ofInt 0) (Q16_16.ofInt 0)

end Semantics.BraidBitwiseODE