From 808a9a8bbb6c4317fd2c48cb0de9c0e1438f437b Mon Sep 17 00:00:00 2001 From: allaun Date: Sun, 5 Jul 2026 08:28:13 -0500 Subject: [PATCH] =?UTF-8?q?fix:=20ManifoldShortcut=20GoldenSpiral=20?= =?UTF-8?q?=E2=80=94=20ASCII=20doc=20comments,=20API=20fixes?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit ManifoldShortcut: same unicode doc comment parser issue as CharPoly. GoldenSpiral: MulLeftMono ℝ missing in Mathlib 4.30 unbundled API; replaced pow_le_pow_right' with direct induction proof. Also fixed goldenContraction noncomputable, phi_inv vs phi⁻¹, Real.sqrt_lt_iff_of_pos -> sqrt_lt_sqrt, field_simp/ring issues. Build: 3300 jobs, 0 errors --- formal/SilverSight/GoldenSpiral.lean | 130 +++++++++++------- formal/SilverSight/PIST/ManifoldShortcut.lean | 22 +-- 2 files changed, 90 insertions(+), 62 deletions(-) diff --git a/formal/SilverSight/GoldenSpiral.lean b/formal/SilverSight/GoldenSpiral.lean index bf26fc60..0b28a683 100644 --- a/formal/SilverSight/GoldenSpiral.lean +++ b/formal/SilverSight/GoldenSpiral.lean @@ -57,8 +57,9 @@ noncomputable def phi_inv : ℝ := phi - 1 lemma phi_inv_lt_one : phi_inv < 1 := by unfold phi_inv phi have h_sqrt : Real.sqrt 5 < 3 := by - apply (Real.sqrt_lt_iff_of_pos (by norm_num)).mpr - norm_num + calc + Real.sqrt 5 < Real.sqrt 9 := Real.sqrt_lt_sqrt (by norm_num) (by norm_num : (5:ℝ) < 9) + _ = 3 := by norm_num linarith [Real.sq_sqrt (by norm_num : (0:ℝ) ≤ 5), h_sqrt] /-- The golden angle: θ_g = 2π/φ². Maximally irrational. -/ @@ -131,25 +132,24 @@ def goldenSpiral16 : Mat16 := The contraction rate φ⁻¹ ≈ 0.618 is SLOWER than 1/2, meaning the golden spiral takes more steps than binary halving — but it never aligns with any rational symmetry axis (maximally observerless). -/ -def goldenContraction {V : Type*} [Sub V] [SMul ℝ V] (c s : V) : V := - c + φ⁻¹ • (s - c) +noncomputable def goldenContraction (c s : ℝ) : ℝ := + c + phi_inv * (s - c) /-- The contraction is contractive: ‖S(s) - c‖ = φ⁻¹·‖s - c‖ < ‖s - c‖. PROVEN (from phi_inv_lt_one). -/ theorem golden_contraction_contractive (c s : ℝ) : goldenContraction c s - c = phi_inv * (s - c) := by - simp [goldenContraction, phi_inv] - ring + simp [goldenContraction] /-! §5 Kähler Gate (FAMM Admissibility) -/ -/-- The conformal Kähler residual: ε_CK(R, μ) = ‖RᵀJR - J‖₁. - For the golden spiral: R commutes with J by construction (complex - scalar multiplication), so the residual should be ~0 (truncation noise). -/ +-- The conformal Kahler residual: eps_CK(R, mu) = ||R^T J R - J||_1. +-- For the golden spiral: R commutes with J by construction (complex +-- scalar multiplication), so the residual should be ~0 (truncation noise). -/-- Conformal Kähler gate: admit iff ε_CK ≤ τ. - The golden spiral passes this gate because complex-scalar - multiplication commutes with J. -/ +-- Conformal Kahler gate: admit iff eps_CK <= tau. +-- The golden spiral passes this gate because complex-scalar +-- multiplication commutes with J. structure KählerGateResult where residual : Q16_16 verdict : Bool -- true = admit, false = reject @@ -169,24 +169,22 @@ theorem goldenSpiral_passes_kahler : (kahlerGate goldenSpiral16 (ofRawInt 64)).verdict = true := by decide -/-! §6 Connection to AngrySphinx (Closed System) -/ +-- ## §6 Connection to AngrySphinx (Closed System) -/-- Contraction rate: φ⁻¹ ≈ 0.618 per golden spiral step. - Cost rate: 2 per AngrySphinx step. +-- Contraction rate: phi^-1 ~= 0.618 per golden spiral step. +-- Cost rate: 2 per AngrySphinx step. +-- The golden spiral converges (phi^-1 < 1). +-- The AngrySphinx cost escalates (2 > 1). +-- Together: the search converges AND becomes exponentially expensive. +-- The system is closed: convergence + escalation = termination. - The golden spiral converges (φ⁻¹ < 1). - The AngrySphinx cost escalates (2 > 1). - Together: the search converges AND becomes exponentially expensive. - The system is closed: convergence + escalation = termination. -/ - -/-- The ratio of AngrySphinx cost to golden contraction convergence. - After k steps: - - Distance to center: φ⁻ᵏ × initial (converging to 0) - - Solve cost: 2ᵏ (escalating to ∞) - - The product: cost/distance = (2/φ)ᵏ → ∞. - The defense overwhelms the search. -/ -def costConvergenceRatio (k : Nat) : ℝ := +-- The ratio of AngrySphinx cost to golden contraction convergence. +-- After k steps: +-- - Distance to center: phi^-k * initial (converging to 0) +-- - Solve cost: 2^k (escalating to infinity) +-- The product: cost/distance = (2/phi)^k -> infinity. +-- The defense overwhelms the search. +noncomputable def costConvergenceRatio (k : Nat) : ℝ := (2 : ℝ) ^ k / phi_inv ^ k /-- Since 2 > 1/φ⁻¹ = φ ≈ 1.618, the ratio grows without bound. @@ -197,36 +195,66 @@ theorem cost_outpaces_convergence (k : Nat) (hk : k ≥ 1) : -- φ = (1+√5)/2 < 2 since √5 < 3 (since 5 < 9) unfold costConvergenceRatio phi_inv phi have h_sqrt_lt : Real.sqrt 5 < 3 := by - apply (Real.sqrt_lt_iff_of_pos (by norm_num)).mpr - norm_num + calc + Real.sqrt 5 < Real.sqrt 9 := Real.sqrt_lt_sqrt (by norm_num) (by norm_num : (5:ℝ) < 9) + _ = 3 := by norm_num + have h_sqrt_gt_1 : Real.sqrt 5 > 1 := by + calc + Real.sqrt 5 > Real.sqrt 1 := Real.sqrt_lt_sqrt (by norm_num) (by norm_num : (1:ℝ) < 5) + _ = 1 := by norm_num have h_phi_lt_2 : phi < 2 := by - unfold phi; linarith [h_sqrt_lt] + unfold phi; nlinarith have h_phi_inv_pos : 0 < phi_inv := by - unfold phi_inv phi; linarith [h_sqrt_lt] - -- costConvergenceRatio k = 2^k / phi_inv^k = (2/phi_inv)^k - -- 2/phi_inv = 2/(phi-1) = 2*phi (since phi^2 = phi+1 => 1/(phi-1) = phi) - -- 2*phi > 2 since phi > 1 + unfold phi_inv phi; nlinarith have h_phi_gt_1 : 1 < phi := by - unfold phi; linarith [h_sqrt_lt] - -- (2/phi_inv)^k ≥ 2 when 2/phi_inv ≥ 2 and k ≥ 1 - -- 2/phi_inv = 2*phi > 2 since phi > 1 + unfold phi; nlinarith + have h_sqrt_sq : (Real.sqrt 5) ^ 2 = 5 := Real.sq_sqrt (by norm_num : (0:ℝ) ≤ 5) + have h_golden_mul : phi * phi_inv = 1 := by + calc + phi * phi_inv = phi * (phi - 1) := rfl + _ = phi ^ 2 - phi := by ring + _ = 1 := by + unfold phi + nlinarith [h_sqrt_sq] have h_ratio_gt_2 : 2 / phi_inv ≥ 2 := by - have : 2 / phi_inv = 2 * phi := by - unfold phi_inv phi - field_simp - ring - rw [this] - linarith [h_phi_gt_1] - -- (2/phi_inv)^k ≥ 2 when 2/phi_inv ≥ 2 and k ≥ 1 - -- Since 0 ≤ 2/phi_inv (proven) and 1 ≤ k (by hk), monotonicity gives: - -- (2/phi_inv)^1 ≤ (2/phi_inv)^k - have h_base_nonneg : 0 ≤ (2 : ℝ) / phi_inv := by linarith [h_phi_gt_1] + have h_eq : 2 / phi_inv = 2 * phi := by + calc + 2 / phi_inv = 2 * (1 / phi_inv) := by ring + _ = 2 * phi := by + rw [show (1 : ℝ) / phi_inv = phi from by + field_simp [h_phi_inv_pos.ne.symm] + nlinarith] + rw [h_eq] + nlinarith + have ha_ge_one : 1 ≤ ((2 : ℝ) / phi_inv) := by + have h_eq : (2 : ℝ) / phi_inv = 2 * phi := by + calc + (2 : ℝ) / phi_inv = 2 * (1 / phi_inv) := by ring + _ = 2 * phi := by + rw [show (1 : ℝ) / phi_inv = phi from by + field_simp [h_phi_inv_pos.ne.symm] + nlinarith] + rw [h_eq] + nlinarith + have ha_nonneg : 0 ≤ (2 : ℝ) / phi_inv := by nlinarith have h_pow : ((2 : ℝ) / phi_inv) ^ (1 : ℕ) ≤ ((2 : ℝ) / phi_inv) ^ k := by - refine pow_le_pow_right h_base_nonneg (by omega : (1 : ℕ) ≤ k) - -- Note: pow_le_pow_right with base ≥ 0 and exponents Nat preserves order + set a := (2 : ℝ) / phi_inv with ha + have ha1 : 1 ≤ a := ha_ge_one + induction' k with m ih + · omega + · by_cases hm : (1 : ℕ) ≤ m + · have h_ih : a ^ (1 : ℕ) ≤ a ^ m := ih hm + calc + a ^ (1 : ℕ) ≤ a ^ m := h_ih + _ ≤ a ^ m * a := by + nlinarith [ha1, pow_nonneg ha_nonneg m] + _ = a ^ (m + 1) := by ring + · have hm0 : m = 0 := by omega + subst hm0; simp calc costConvergenceRatio k = ((2 : ℝ) / phi_inv) ^ k := by - unfold costConvergenceRatio; field_simp; ring + unfold costConvergenceRatio + rw [div_pow] _ ≥ ((2 : ℝ) / phi_inv) ^ (1 : ℕ) := h_pow _ = (2 : ℝ) / phi_inv := by simp _ ≥ 2 := h_ratio_gt_2 diff --git a/formal/SilverSight/PIST/ManifoldShortcut.lean b/formal/SilverSight/PIST/ManifoldShortcut.lean index e3efd769..5c80aeff 100644 --- a/formal/SilverSight/PIST/ManifoldShortcut.lean +++ b/formal/SilverSight/PIST/ManifoldShortcut.lean @@ -102,17 +102,17 @@ structure ManifoldEquation where def lagrangian (eq : ManifoldEquation) (alpha beta : Q16_16) : Q16_16 := add eq.deltaCost (add (mul alpha eq.spectralCost) (mul beta eq.programCost)) -/-- The conservation bound: L ≥ K(data) for any equation. - This is the measured law — no equation can beat it. - - PROVEN from the conservation law (8 measured branches). -/ -/-- HONESTY CLASS: CONJECTURE - The conservation law: program_size + residual_size ≥ K(data). - Measured across 8 branches (char-poly, Braille/T9, GW SNR, weird-machine, - mass-number, superposition, pi-LUT, LLM-recoverable-drop). - All 8 branches confirmed: no method beats the entropy floor. - Cannot be formally proven (K(data) is uncomputable Kolmogorov complexity). - ACKNOWLEDGED AS AN AXIOM. -/ +-- The conservation bound: L >= K(data) for any equation. +-- This is the measured law -- no equation can beat it. +-- +-- PROVEN from the conservation law (8 measured branches). +-- HONESTY CLASS: CONJECTURE +-- The conservation law: program_size + residual_size >= K(data). +-- Measured across 8 branches (char-poly, Braille/T9, GW SNR, weird-machine, +-- mass-number, superposition, pi-LUT, LLM-recoverable-drop). +-- All 8 branches confirmed: no method beats the entropy floor. +-- Cannot be formally proven (K(data) is uncomputable Kolmogorov complexity). +-- ACKNOWLEDGED AS AN AXIOM. axiom conservation_law (eq : ManifoldEquation) (alpha beta : Q16_16) : lagrangian eq alpha beta ≥ eq.kData