fix: ManifoldShortcut GoldenSpiral — ASCII doc comments, API fixes

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

@@ -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

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