SilverSight/formal/CoreFormalism/ContractedCrossStep.lean

/-
  ContractedCrossStep.lean — Genuine Contraction via Golden Scale

  The real crossStep dynamics (BraidCrossStepDynamics.lean, Research Stack)
  showed that PhaseVec.add is additive doubling: zᵢⱼ = zᵢ + zⱼ. This grows
  until saturation, not toward zero. The golden contraction φ⁻¹ was never
  wired into crossStep.

  This module fixes that. The contracted phase merge computes:

    half * (p + q)  then  φ⁻¹ · (half · (p + q))

  On the diagonal (p = q = z): half * (z + z) = z (exact in Q16_16 when
  z + z doesn't saturate). Then φ⁻¹ · z contracts genuinely toward zero.

  Since φ⁻¹ ≈ 0.618 < 1, repeated application drives any unsaturated phase
  toward zero geometrically. The unsaturated condition holds after finitely
  many steps (phase magnitude decreases monotonically).

  Key theorems:
    half_mul_add_self_non_sat    — half * (a + a) = a when a + a fits in Q16_16
    contractedPhaseMerge_diagonal — merge contracts by φ⁻¹ on the diagonal
    contractedCrossStep_converges — ∀ s, ∃ n, IsEigensolid (contractedCrossStep^[n] s)
-/

import CoreFormalism.BraidCross
import CoreFormalism.BraidEigensolid
import SilverSight.FixedPoint
import SilverSight.GoldenSpiral

namespace SilverSight.ContractedCrossStep

open SilverSight.BraidCross
open SilverSight.BraidEigensolid
open SilverSight.BraidBracket
open SilverSight.BraidStrand
open SilverSight.FixedPoint.Q16_16
open SilverSight.FixedPoint (q16MinRaw q16MaxRaw q16Clamp)
open SilverSight.GoldenSpiral

/-! §1 The Contracted Phase Merge

  The real crossStep uses PhaseVec.add (additive doubling: zᵢⱼ = zᵢ + zⱼ).
  The contracted merge first averages (half * (zᵢ + zⱼ)), then scales by φ⁻¹.

  On the diagonal: φ⁻¹ · (half · (z + z)) = φ⁻¹ · z (exact when z + z fits).
  Since φ⁻¹ < 1, this genuinely contracts toward zero.
-/

/-- Half in Q16_16: 0.5 = 32768 raw -/
def half : Q16_16 := ofRawInt 32768

/-- Direct componentwise addition (no zero shortcuts).
    Avoids the PhaseVec.add zero-check which breaks identities for small values. -/
def phaseAddDirect (p q : PhaseVec) : PhaseVec :=
  { x := Q16_16.add p.x q.x, y := Q16_16.add p.y q.y }

/-- Contracted phase merge: φ⁻¹ · (half · (p + q)) using direct addition -/
def contractedPhaseMerge (p q : PhaseVec) : PhaseVec :=
  PhaseVec.scale phiInvQ16 (PhaseVec.scale half (phaseAddDirect p q))

/-- half * (a + a) = a when a + a doesn't overflow Q16_16 bounds.
    Condition: a.val ≤ q16MaxRaw/2 ensures a.val + a.val ≤ q16MaxRaw (no upper overflow).
    Condition: a.val ≥ q16MinRaw/2 ensures a.val + a.val ≥ q16MinRaw (no lower overflow).
    Uses int_scale_mul_ediv_cancel and ofRawInt_toInt. -/
lemma half_mul_add_self_non_sat (a : Q16_16) (h_upper : a.val ≤ q16MaxRaw / 2) (h_lower : a.val ≥ q16MinRaw / 2) :
    Q16_16.mul half (Q16_16.add a a) = a := by
  unfold half Q16_16.mul Q16_16.add
  -- (add a a) = ofRawInt (a.val + a.val)
  -- Show that (ofRawInt (a.val + a.val)).val = a.val + a.val (no saturation)
  have h_add_val : (Q16_16.ofRawInt (a.val + a.val)).val = a.val + a.val := by
    unfold Q16_16.ofRawInt
    have h_lower' : q16MinRaw ≤ a.val + a.val := by
      have h_a_bound : a.val ≥ -1073741824 := by
        have h_half : q16MinRaw / 2 = -1073741824 := by
          unfold q16MinRaw; norm_num
        calc
          a.val ≥ q16MinRaw / 2 := h_lower
          _ = -1073741824 := h_half
      unfold q16MinRaw
      omega
    have h_upper' : a.val + a.val ≤ q16MaxRaw := by
      have h_a_bound : a.val ≤ 1073741823 := by
        have h_half : q16MaxRaw / 2 = 1073741823 := by
          unfold q16MaxRaw; norm_num
        calc
          a.val ≤ q16MaxRaw / 2 := h_upper
          _ = 1073741823 := h_half
      unfold q16MaxRaw
      omega
    split <;> rename_i h
    · exfalso; omega
    · split <;> rename_i h'
      · exfalso; omega
      · rfl
  -- ofRawInt ((32768 * (ofRawInt (a.val + a.val)).toInt) / 65536) = a
  -- Use h_add_val to replace the inner ofRawInt(a.val+a.val).toInt with a.val+a.val
  -- Simplify: (ofRawInt (a.val + a.val)).toInt = a.val + a.val, then simplify the division
  have h_toInt_eq : (Q16_16.ofRawInt (a.val + a.val)).toInt = a.val + a.val := by
    simpa [toInt] using h_add_val
  have h_simp : (32768 * (a.val + a.val)) / 65536 = a.val := by
    calc
      (32768 * (a.val + a.val)) / 65536 = (32768 * 2 * a.val) / 65536 := by omega
      _ = (65536 * a.val) / 65536 := by ring
      _ = a.val := by
        have hpos : (65536 : Int) ≠ 0 := by norm_num
        exact Int.ediv_eq_of_eq_mul_right hpos (by ring)
  calc
    Q16_16.ofRawInt ((32768 * (Q16_16.ofRawInt (a.val + a.val)).toInt) / 65536)
        = Q16_16.ofRawInt ((32768 * (a.val + a.val)) / 65536) := by rw [h_toInt_eq]
    _ = Q16_16.ofRawInt (a.val) := by rw [h_simp]
    _ = a := by
      -- ofRawInt_toInt uses .toInt, but we have .val; dsimp to match
      have h : Q16_16.ofRawInt a.val = a := by
        simpa [toInt] using (ofRawInt_toInt a)
      exact h

/-- On the diagonal under non-saturation, contractedPhaseMerge contracts: merge(z,z) = φ⁻¹ · z.
    The phase a is unsaturated if a.a.val ≤ max/2 and a.a.val ≥ min/2, etc.
    For full details see half_mul_add_self_non_sat. -/
theorem contractedPhaseMerge_diagonal_non_sat (z : PhaseVec)
    (hx_upper : z.x.val ≤ q16MaxRaw / 2) (hx_lower : z.x.val ≥ q16MinRaw / 2)
    (hy_upper : z.y.val ≤ q16MaxRaw / 2) (hy_lower : z.y.val ≥ q16MinRaw / 2) :
    contractedPhaseMerge z z = PhaseVec.scale phiInvQ16 z := by
  unfold contractedPhaseMerge
  have h_avg : PhaseVec.scale half (phaseAddDirect z z) = z := by
    cases z; rename_i x y
    unfold phaseAddDirect PhaseVec.scale
    simp [half_mul_add_self_non_sat x hx_upper hx_lower,
          half_mul_add_self_non_sat y hy_upper hy_lower]
  simp [h_avg]

/-! §2 Contracted Braid Cross -/

/-- Contracted braid crossing: merge with golden contraction on phase and jitter -/
def contractedBraidCross (sᵢ sⱼ : BraidStrand) : BraidStrand × BraidBracket :=
  let zᵢⱼ := contractedPhaseMerge sᵢ.phaseAcc sⱼ.phaseAcc
  let μᵢ := Q16_16.ofNat sᵢ.slot.toNat
  let μⱼ := Q16_16.ofNat sⱼ.slot.toNat
  let μᵢⱼ := crossSlot μᵢ μⱼ
  let Bᵢⱼ := BraidBracket.fromPhaseVec zᵢⱼ μᵢⱼ
  let Rᵢⱼ := BraidBracket.crossingResidual Bᵢⱼ sᵢ.bracket sⱼ.bracket
  let contractedJitter := Q16_16.mul phiInvQ16 (Q16_16.add sᵢ.jitter sⱼ.jitter)
  let mergedStrand : BraidStrand :=
    { phaseAcc := zᵢⱼ
    , parity := sᵢ.parity && sⱼ.parity
    , slot := sᵢ.slot.xor sⱼ.slot
    , residue := Rᵢⱼ.kappa
    , jitter := contractedJitter
    , bracket := Bᵢⱼ }
  (mergedStrand, Rᵢⱼ)

/-! §3 Contracted Cross Step -/

/-- Contracted cross step: apply contractedBraidCross to all 4 pairs -/
def contractedCrossStep (s : BraidState) : BraidState :=
  let pairs : List (Fin 8 × Fin 8) :=
    [(0, 1), (2, 3), (4, 5), (6, 7)]
  let newStrands := pairs.map fun (i, j) =>
    let si := s.strands i
    let sj := s.strands j
    let (merged, _) := contractedBraidCross si sj
    (i, merged)
  { s with strands := fun k =>
    match newStrands.find? fun (i, _) => i = k with
    | some (_, strand) => strand
    | none => s.strands k }

/-! §4 Zero State and Contraction Factor -/

/-- The all-zero state: every strand has phase, jitter, residue = 0 and slot = 0.
    This is the true fixed point of contractedCrossStep (unlike BraidEigensolid.zeroState
    which uses distinct slots per strand). -/
def allZeroState : BraidState :=
  { strands := fun _ => BraidStrand.zero 0, step_count := 0 }

/-- phiInvQ16 < one in Q16_16: 40504 < 65536. -/
lemma phiInvQ16_lt_one : phiInvQ16.val < one.val := by
  have h_phi : phiInvQ16.val = 40504 := by
    unfold phiInvQ16 Q16_16.ofRawInt
    have h : ¬ (40504 : Int) < q16MinRaw := by
      unfold q16MinRaw; omega
    have h' : ¬ (40504 : Int) > q16MaxRaw := by
      unfold q16MaxRaw; omega
    simp [h, h']
  have h_one : one.val = 65536 := rfl
  rw [h_phi, h_one]
  norm_num

/-! §5 Convergence

  The contracted crossStep dynamics converge to the all-zero state for any
  initial state. Full proof requires Q16_16 inequality lemmas and
  well-founded induction on PhaseVec.normApprox. Left as TODO.
-/

/-- Contracted crossStep converges to an eigensolid for any initial state. -/
theorem contractedCrossStep_converges (s : BraidState) :
    ∃ n : Nat, IsEigensolid (contractedCrossStep^[n] s) := by
  sorry

/-- The zero state (allZeroState) is the unique attractor of contractedCrossStep. -/
theorem zero_is_attractor (s : BraidState) : ∃ n : Nat, contractedCrossStep^[n] s = allZeroState := by
  sorry

end SilverSight.ContractedCrossStep

/-! §5 Numerical Witnesses -/

open SilverSight.ContractedCrossStep
open SilverSight.BraidBracket
open SilverSight.BraidStrand
open SilverSight.BraidEigensolid
open SilverSight.FixedPoint
open SilverSight.FixedPoint.Q16_16

-- Witness: contractedPhaseMerge on the diagonal contracts
#eval
  let z : PhaseVec := { x := ofNat 10, y := ofNat 20 }
  let merged := contractedPhaseMerge z z
  -- φ⁻¹ · z ≈ (6.18, 12.36) in Q16_16 raw: (405040, 810080)
  (merged.x.val, merged.y.val)

-- Witness: contractedCrossStep on zero state is fixed
#eval
  let s : BraidState := { strands := fun _ => BraidStrand.zero 0, step_count := 0 }
  let s1 := contractedCrossStep s
  s1.strands 0 == BraidStrand.zero 0