feat(autoresearch): bootstrap sourced RH root

Bind the root to pinned Mathlib declarations and make ROOT_UNAVAILABLE recovery atomic, elaborated, and isolated from quarantined branches.

Co-authored-by: Cursor <cursoragent@cursor.com>

Author: 2 people

KakeyaLeanGate.lean

@@ -1 +1,2 @@
 import KakeyaLeanGate.Prelude
+import KakeyaLeanGate.RiemannHypothesisRoot

KakeyaLeanGate/Prelude.lean

@@ -4,6 +4,7 @@ import Mathlib.Analysis.Complex.JensenFormula
 import Mathlib.Analysis.Complex.LocallyUniformLimit
 import Mathlib.Analysis.Complex.Order
 import Mathlib.Analysis.Analytic.Uniqueness
+import Mathlib.NumberTheory.LSeries.RiemannZeta
 
 /-!
 Minimal import target for AutoResearch theorem-signature validation.

KakeyaLeanGate/RiemannHypothesisRoot.lean

@@ -0,0 +1,25 @@
+import Mathlib.NumberTheory.LSeries.RiemannZeta
+
+/-!
+The canonical AutoResearch root is an alias of Mathlib's pinned
+`RiemannHypothesis` declaration.  The expanded branch is retained separately
+and its relationship to the canonical branch is proved definitionally below.
+-/
+
+def KakeyaRiemannHypothesisRoot : Prop := RiemannHypothesis
+
+def KakeyaRiemannHypothesisExpanded : Prop :=
+  ∀ (s : ℂ), riemannZeta s = 0 →
+    (¬ ∃ n : ℕ, s = -2 * (n + 1)) →
+    s ≠ 1 →
+    s.re = 1 / 2
+
+theorem kakeya_rh_expanded_iff_canonical :
+    KakeyaRiemannHypothesisExpanded ↔ KakeyaRiemannHypothesisRoot := by
+  rfl
+
+#check riemannZeta
+#check completedRiemannZeta
+#check completedRiemannZeta₀
+#check riemannZeta_neg_two_mul_nat_add_one
+#check RiemannHypothesis