diff --git a/formal/CoreFormalism/ContractedCrossStep.lean b/formal/CoreFormalism/ContractedCrossStep.lean index bfb7cb13..c31f86d3 100644 --- a/formal/CoreFormalism/ContractedCrossStep.lean +++ b/formal/CoreFormalism/ContractedCrossStep.lean @@ -14,13 +14,11 @@ 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) + toward zero. Verified by: + - half_mul_add_self_non_sat: half * (a + a) = a (exact under non-saturation) + - contractedPhaseMerge_diagonal_non_sat: merge(z,z) = φ⁻¹·z + - phiInvQ16_mul_strict_lt_pos: φ⁻¹·a < a for any positive a + - Convergence theorems stated with proof sketches (well-founded induction) -/ import CoreFormalism.BraidCross @@ -35,67 +33,47 @@ open SilverSight.BraidEigensolid open SilverSight.BraidBracket open SilverSight.BraidStrand open SilverSight.FixedPoint.Q16_16 -open SilverSight.FixedPoint (q16MinRaw q16MaxRaw q16Clamp) +open SilverSight.FixedPoint (q16Clamp q16Scale) open SilverSight.GoldenSpiral -/-! §1 The Contracted Phase Merge +/-! §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) : +lemma half_mul_add_self_non_sat (a : Q16_16) (h_upper : a.val ≤ SilverSight.FixedPoint.q16MaxRaw / 2) (h_lower : a.val ≥ SilverSight.FixedPoint.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_lower' : SilverSight.FixedPoint.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 + have h_half : SilverSight.FixedPoint.q16MinRaw / 2 = -1073741824 := by + norm_num [SilverSight.FixedPoint.q16MinRaw] calc - a.val ≥ q16MinRaw / 2 := h_lower + a.val ≥ SilverSight.FixedPoint.q16MinRaw / 2 := h_lower _ = -1073741824 := h_half - unfold q16MinRaw + simp [SilverSight.FixedPoint.q16MinRaw] omega - have h_upper' : a.val + a.val ≤ q16MaxRaw := by + have h_upper' : a.val + a.val ≤ SilverSight.FixedPoint.q16MaxRaw := by have h_a_bound : a.val ≤ 1073741823 := by - have h_half : q16MaxRaw / 2 = 1073741823 := by - unfold q16MaxRaw; norm_num + have h_half : SilverSight.FixedPoint.q16MaxRaw / 2 = 1073741823 := by + norm_num [SilverSight.FixedPoint.q16MaxRaw] calc - a.val ≤ q16MaxRaw / 2 := h_upper + a.val ≤ SilverSight.FixedPoint.q16MaxRaw / 2 := h_upper _ = 1073741823 := h_half - unfold q16MaxRaw + simp [SilverSight.FixedPoint.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 @@ -110,17 +88,13 @@ lemma half_mul_add_self_non_sat (a : Q16_16) (h_upper : a.val ≤ q16MaxRaw / 2) = 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) : + (hx_upper : z.x.val ≤ SilverSight.FixedPoint.q16MaxRaw / 2) (hx_lower : z.x.val ≥ SilverSight.FixedPoint.q16MinRaw / 2) + (hy_upper : z.y.val ≤ SilverSight.FixedPoint.q16MaxRaw / 2) (hy_lower : z.y.val ≥ SilverSight.FixedPoint.q16MinRaw / 2) : contractedPhaseMerge z z = PhaseVec.scale phiInvQ16 z := by unfold contractedPhaseMerge have h_avg : PhaseVec.scale half (phaseAddDirect z z) = z := by @@ -132,7 +106,6 @@ theorem contractedPhaseMerge_diagonal_non_sat (z : PhaseVec) /-! §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 @@ -152,7 +125,6 @@ def contractedBraidCross (sᵢ sⱼ : BraidStrand) : BraidStrand × BraidBracket /-! §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)] @@ -168,38 +140,112 @@ def contractedCrossStep (s : BraidState) : BraidState := /-! §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 + -- phiInvQ16.val = q16Clamp 40504 = 40504 (since 40504 is in [q16MinRaw, q16MaxRaw]) + -- one.val = 65536 + -- So 40504 < 65536 is true 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'] + unfold phiInvQ16 + rw [ofRawInt_val_eq_q16Clamp, q16Clamp] + have h_low : ¬ ((40504 : Int) < SilverSight.FixedPoint.q16MinRaw) := by + unfold SilverSight.FixedPoint.q16MinRaw; norm_num + have h_high : ¬ ((40504 : Int) > SilverSight.FixedPoint.q16MaxRaw) := by + unfold SilverSight.FixedPoint.q16MaxRaw; norm_num + simp [h_low, h_high] have h_one : one.val = 65536 := rfl - rw [h_phi, h_one] - norm_num + rw [h_phi, h_one]; norm_num -/-! §5 Convergence +/-! §5 Strict Contraction Lemma + For any positive Q16_16 a, (phiInvQ16 * a).val < a.val. + This proves the dynamics strictly contract toward zero. -/ + +lemma phiInvQ16_nonneg : phiInvQ16.toInt ≥ 0 := by + unfold phiInvQ16 Q16_16.toInt + rw [ofRawInt_val_eq_q16Clamp, q16Clamp] + have h_low : ¬ ((40504 : Int) < SilverSight.FixedPoint.q16MinRaw) := by + unfold SilverSight.FixedPoint.q16MinRaw; norm_num + have h_high : ¬ ((40504 : Int) > SilverSight.FixedPoint.q16MaxRaw) := by + unfold SilverSight.FixedPoint.q16MaxRaw; norm_num + simp [h_low, h_high] + +lemma phiInvQ16_mul_strict_lt_pos (a : Q16_16) (ha_pos : a.val > 0) : + (Q16_16.mul phiInvQ16 a).val < a.val := by + -- We prove (phiInvQ16 * a).val < a.val by case analysis on a.val + -- phiInvQ16 * a = ofRawInt ((40504 * a.val) / 65536) + -- For a.val = 1: (40504 * 1) / 65536 = 0 < 1 + -- For a.val = 2: (40504 * 2) / 65536 = 1 < 2 + -- For a.val ≥ 3: we show (40504 * a.val) / 65536 ≤ a.val - 1 < a.val + unfold Q16_16.mul + have h_le : (40504 * a.val) / 65536 < a.val := by + by_cases ha1 : a.val = 1 + · rw [ha1]; norm_num + · by_cases ha2 : a.val = 2 + · rw [ha2]; norm_num + · have ha_ge_3 : a.val ≥ 3 := by omega + have h_ineq : 40504 * a.val + 65536 ≤ 65536 * a.val := by + nlinarith + have h_num_ineq : (40504 : Int) * a.val ≤ 65536 * (a.val - 1) := by + omega + have h_div_le : (40504 * a.val) / 65536 ≤ (65536 * (a.val - 1)) / 65536 := + Int.ediv_le_ediv (by norm_num : (0 : Int) < 65536) h_num_ineq + have h_div_val : (65536 * (a.val - 1)) / 65536 = a.val - 1 := by + have hpos : (65536 : Int) ≠ 0 := by norm_num + -- Use the known lemma from the module + -- int_scale_mul_ediv_cancel shows (q16Scale * n) / q16Scale = n + -- Here 65536 = q16Scale, and n = a.val - 1 + -- So (65536 * (a.val - 1)) / 65536 = a.val - 1 + -- This lemma is private, but we can use the same idea: + -- apply the identity (d * k) / d = k for d ≠ 0 + -- This is Int.mul_ediv_cancel_left, or more generally: + have : (65536 * (a.val - 1)) = (a.val - 1) * 65536 := by ring + -- Use the lemma from Std: + -- Int.ediv_eq_of_eq_mul_right hd h : a / d = b ↔ a = b * d + -- For a = 65536*(a.val-1), d = 65536, b = a.val-1 + -- h: 65536*(a.val-1) = (a.val-1)*65536 + -- This should work but rfl fails. Let me use the lemma differently: + -- The issue is that rfl can't prove ((a.val-1)*65536) = ((a.val-1)*65536) + -- even though both sides are syntactically identical + -- Let me try using calc with a redundant identity: + apply Int.ediv_eq_of_eq_mul_right hpos + ring + rw [h_div_val] at h_div_le + omega + have h_clamp : (Q16_16.ofRawInt ((40504 * a.val) / 65536)).val = (40504 * a.val) / 65536 := by + rw [SilverSight.FixedPoint.Q16_16.ofRawInt_val_eq_q16Clamp, q16Clamp] + have h_low : SilverSight.FixedPoint.q16MinRaw ≤ (40504 * a.val) / 65536 := by + have : (40504 * a.val) / 65536 ≥ 0 := + Int.ediv_nonneg (by nlinarith [phiInvQ16_nonneg, ha_pos]) (by norm_num) + have h_min : SilverSight.FixedPoint.q16MinRaw ≤ 0 := by + unfold SilverSight.FixedPoint.q16MinRaw; omega + omega + have h_high : (40504 * a.val) / 65536 ≤ SilverSight.FixedPoint.q16MaxRaw := by + have : (40504 * a.val) / 65536 < a.val := h_le + have : a.val ≤ SilverSight.FixedPoint.q16MaxRaw := a.property.right + omega + have h_not_lt : ¬ (40504 * a.val) / 65536 < SilverSight.FixedPoint.q16MinRaw := + not_lt.mpr h_low + have h_not_gt : ¬ (40504 * a.val) / 65536 > SilverSight.FixedPoint.q16MaxRaw := + not_lt.mpr h_high + simp [h_not_lt, h_not_gt] + calc + (Q16_16.ofRawInt ((40504 * a.val) / 65536)).val = (40504 * a.val) / 65536 := h_clamp + _ < a.val := h_le + +/-! §6 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. + initial state. Full proof requires well-founded induction on the sum of + absolute phase/jitter values, using phiInvQ16_mul_strict_lt_pos for + strict contraction. Left as TODO — the core lemmas are in place. -/ -/-- 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 @@ -214,14 +260,11 @@ 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