From da4ea434e73c03a3735b76edc80306c8bc053d8e Mon Sep 17 00:00:00 2001 From: allaun Date: Mon, 6 Jul 2026 10:01:56 -0500 Subject: [PATCH] =?UTF-8?q?feat(lean):=20ContractedCrossStep=20=E2=80=94?= =?UTF-8?q?=20genuine=20=CF=86=E2=81=BB=C2=B9=20contraction=20for=20braid?= =?UTF-8?q?=20crossing=20dynamics?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The real crossStep uses PhaseVec.add (additive doubling: zᵢⱼ = zᵢ + zⱼ), which grows until Q16_16 saturation. ContractedCrossStep fixes this by replacing the merge with φ⁻¹ · (half · (p + q)), which contracts on the diagonal: merge(z,z) = φ⁻¹ · z (exact under non-saturation). Key results: - half_mul_add_self_non_sat: half * (a + a) = a (exact Q16_16 identity when a + a doesn't overflow) - contractedPhaseMerge_diagonal_non_sat: merge contracts by φ⁻¹ - Jitter also contracted by φ⁻¹ to prevent saturation - #eval witnesses confirm φ⁻¹ contraction and zero-state fixedness Convergence theorems stated with proof sketches; full proofs require Q16_16 inequality lemmas and well-founded induction (TODO). Build: 3309 jobs, 0 errors --- formal/CoreFormalism/ContractedCrossStep.lean | 226 ++++++++++++++++++ lakefile.lean | 1 + 2 files changed, 227 insertions(+) create mode 100644 formal/CoreFormalism/ContractedCrossStep.lean diff --git a/formal/CoreFormalism/ContractedCrossStep.lean b/formal/CoreFormalism/ContractedCrossStep.lean new file mode 100644 index 00000000..951aee11 --- /dev/null +++ b/formal/CoreFormalism/ContractedCrossStep.lean @@ -0,0 +1,226 @@ +/- + 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 Convergence Theorem + + Proof sketch: + 1. After step 1, each pair is diagonal (commutativity of contractedBraidCross). + 2. After step 2, slots are 0 (XOR of equal slots). + 3. On the diagonal, each phase contracts by φ⁻¹: + contractedPhaseMerge z z = φ⁻¹ · z (under non-saturation) + 4. Since φ⁻¹ ≈ 0.618 < 1, the phase norm decreases geometrically. + 5. The phase space is finite (Q16_16 has 2³² values), so after finitely many + steps the phase reaches the non-saturated regime. + 6. Once non-saturated, it contracts to 0 in O(log_{1/φ⁻¹}(maxPhase)) steps. + 7. With phase = 0, slot = 0, jitter = 0, the state is the zero eigensolid. + + Full proof requires: + - Q16_16 inequality lemmas (phiInvQ16.val < one.val) + - normApprox monotonicity under φ⁻¹ scaling + - IsNonSaturated preservation under contractedCrossStep + - Well-founded induction on PhaseVec.normApprox + + These are left as TODO — the core dynamical correction (contraction via + half then φ⁻¹ instead of additive doubling) is in place and verified + by the #eval witnesses below. +-/ + +/-- Contracted crossStep converges to an eigensolid for any initial state. + (Statement — full proof requires well-founded induction on phase norm.) -/ +theorem contractedCrossStep_converges (s : BraidState) : + ∃ n : Nat, IsEigensolid (contractedCrossStep^[n] s) := by + sorry + +/-- The zero state is the unique attractor of contractedCrossStep -/ +theorem zero_is_attractor : + ∀ s : BraidState, ∃ n : Nat, contractedCrossStep^[n] s = zeroState := 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 diff --git a/lakefile.lean b/lakefile.lean index de559dd1..29108441 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -33,6 +33,7 @@ lean_lib «SilverSightFormal» where `CoreFormalism.SieveLemmas, `CoreFormalism.InteractionGraphSidon, `CoreFormalism.BraidEigensolid, + `CoreFormalism.ContractedCrossStep, `CoreFormalism.BraidSpherionBridge, `CoreFormalism.E8Sidon, `CoreFormalism.EisensteinSeries,