Architecture 9 Cursor strategy and isolated OProver residency

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.
@@ -40,3 +41,16 @@ def agreesWithSimplePoleOnPuncturedDisk
 def nonzeroComplex (z : ℂ) : Prop := z ≠ 0
 
 def positiveRadius (radius : ℝ) : Prop := 0 < radius
+
+/- General, target-independent constructors admitted by candidate
+representation analysis.  These only wrap Mathlib types and predicates. -/
+def continuousComplexMap (f : ℂ → ℂ) : Prop := Continuous f
+
+def holomorphicComplexMapOn (f : ℂ → ℂ) (domain : Set ℂ) : Prop :=
+  DifferentiableOn ℂ f domain
+
+def convergesComplexSequence (seq : ℕ → ℂ) (limit : ℂ) : Prop :=
+  Tendsto seq atTop (nhds limit)
+
+def boundedComplexMapOn (f : ℂ → ℂ) (domain : Set ℂ) : Prop :=
+  ∃ bound : ℝ, 0 ≤ bound ∧ ∀ z ∈ domain, ‖f z‖ ≤ bound

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