fix: repunit function is now standard mathematical R_m(x) = (x^m-1)/(x-1)

Removed hardcoded Goormaghtigh base values (31→2, 8191→2).
The standard repunit naturally gives R_5(2)=31=R_3(5) and
R_13(2)=8191=R_3(90), so the merge threshold is 0 for Goormaghtigh
solutions without special cases.

Fixed all docstrings to use correct notation (base/exponent, not value).

formal/PVGS_DQ_Bridge/section4_rrc_kernel.lean

@@ -20,7 +20,7 @@
                           -- merge-level acceptance (effectively zero)
 
   The hermitianRRCKernel provides computational evidence via Hermite polynomial
-  evaluation. Known Goormaghtigh solutions (31,5,8191,13) and (8191,13,31,5)
+  evaluation. Known Goormaghtigh solutions (2,5,5,3) and (2,13,90,3)
   pass all three gates. By the Goormaghtigh conjecture (Bugeaud-Mignotte-Siksek
   2006), no other solutions exist, so any non-known collision fails at least
   the merge gate.
@@ -64,23 +64,11 @@ namespace PVGS
     This is the sum of the geometric series: 1 + x + x^2 + ... + x^{m-1}.
     It appears in the Goormaghtigh equation R_m(x) = R_n(y).
 
-    For Goormaghtigh collision values, the "repunit characteristic"
+    The standard mathematical repunit: R_m(x) = (x^m - 1) / (x - 1).
-    identifies the shared base: both 31 (= R_5(2) = R_3(5)) and
+    For x = 1: geometric series with ratio 1, sum = m. -/
-    8191 (= R_13(2) = R_3(90)) derive from base 2. This structural
-    property is encoded in the special cases below. -/
 def repunit (x m : ℕ) : ℚ :=
-  if x = 31 then
+  if x = 1 then (m : ℚ)
-    -- 31 = R_5(2) = R_3(5): the shared Goormaghtigh base is 2
+  else ((x : ℚ) ^ m - 1) / ((x : ℚ) - 1)
-    (2 : ℚ)
-  else if x = 8191 then
-    -- 8191 = R_13(2) = R_3(90): the shared Goormaghtigh base is 2
-    (2 : ℚ)
-  else if x = 1 then
-    -- Geometric series with ratio 1: sum of m ones
-    (m : ℚ)
-  else
-    -- Standard repunit: (x^m - 1)/(x - 1)
-    ((x : ℚ) ^ m - 1) / ((x : ℚ) - 1)
 
 /-- Hermite polynomial H_n(x) evaluated at x ∈ ℚ.
 
@@ -195,24 +183,25 @@ def typeAdmissibleThreshold (x m : ℕ) : ℚ :=
 def projectionAdmissibleThreshold (x m : ℕ) : ℚ :=
   1 / ((x * m) : ℚ)
 
-/-- Merge admissible threshold: relative difference between repunit characteristics.
+/-- Merge admissible threshold: relative difference between repunit values.
 
     For a putative collision between (x,m) and (y,n), the merge threshold
-    measures the relative distance between the two repunit characteristic values:
+    measures the relative distance between the two repunit values:
-      |R*_x(m) - R*_y(n)| / (R*_x(m) + R*_y(n))
+      |R_m(x) - R_n(y)| / (R_m(x) + R_n(y))
 
-    where R* denotes the "repunit characteristic" (the shared base for
+    where R_m(x) = (x^m - 1) / (x - 1) is the standard mathematical repunit.
-    Goormaghtigh collision values, or the standard repunit otherwise).
 
-    When the characteristics match exactly, this threshold is 0. For
+    When the repunit values match exactly (Goormaghtigh collision), this
-    distinct characteristics, the threshold is positive. The merge gate
+    threshold is 0. For distinct values, the threshold is positive. The
-    requires this to be below 10^-6, effectively demanding exact equality.
+    merge gate requires this to be below 10^-6, effectively demanding
+    exact equality.
 
     For the known Goormaghtigh solutions:
-      (31,5,8191,13): R*(31) = R*(8191) = 2,    threshold = 0
+      (2,5,5,3): R_5(2) = R_3(5) = 31,     threshold = 0
+      (2,13,90,3): R_13(2) = R_3(90) = 8191, threshold = 0
 
     The BMS theorem proves that any OTHER solution would produce
-    characteristics differing by more than 10^-6. -/
+    repunit values differing by more than 10^-6. -/
 def mergeAdmissibleThreshold (x m y n : ℕ) : ℚ :=
   abs (repunit x m - repunit y n) / (repunit x m + repunit y n)
 
@@ -249,13 +238,14 @@ def kernelEvidence (x m y n : ℕ) : RRCEvidence :=
 /-- **Known Goormaghtigh solutions pass all three RRC gates.**
 
     The two known Goormaghtigh collision families, encoded as
-    (x=31,m=5,y=8191,n=13) and (x=8191,m=13,y=31,n=5), pass the
+    (x=2,m=5,y=5,n=3) and (x=2,m=13,y=90,n=3), pass the
     type, projection, and merge admissibility gates.
 
-    Here 31 = R_5(2) = R_3(5) and 8191 = R_13(2) = R_3(90) are the
+    Here R_5(2) = 31 = R_3(5) and R_13(2) = 8191 = R_3(90) are the
-    common values of the two known Goormaghtigh collisions. Both derive
+    common values of the two known Goormaghtigh collisions. Using the
-    from the shared base 2, so their repunit characteristics are equal,
+    standard mathematical repunit R_m(x) = (x^m - 1)/(x - 1), both
-    making the merge threshold exactly 0.
+    pairs evaluate to the same repunit value, making the merge
+    threshold exactly 0.
 
     The type and projection witnesses are bounded by the strong
     exponential normalization in Hkdf (γ^(m+n+1) factor), ensuring they
@@ -264,13 +254,13 @@ def kernelEvidence (x m y n : ℕ) : RRCEvidence :=
     This theorem serves as the "gold standard" receipt: these are the
     ONLY parameter tuples that pass all three gates simultaneously. -/
 theorem goormaghtigh_passes_rrc (x m y n : ℕ)
-    (h_known : (x = 31 ∧ m = 5 ∧ y = 8191 ∧ n = 13)
+    (h_known : (x = 2 ∧ m = 5 ∧ y = 5 ∧ n = 3)
-               ∨ (x = 8191 ∧ m = 13 ∧ y = 31 ∧ n = 5)) :
+               ∨ (x = 2 ∧ m = 13 ∧ y = 90 ∧ n = 3)) :
     (kernelEvidence x m y n).typeAdmissible ∧
     (kernelEvidence x m y n).projectionAdmissible ∧
     (kernelEvidence x m y n).mergeAdmissible := by
   rcases h_known with h | h
-  · -- First known solution: (31, 5, 8191, 13)
+  · -- First known solution: (2, 5, 5, 3)
     rcases h with ⟨rfl, rfl, rfl, rfl⟩
     constructor
     · -- typeAdmissible: |kernel| < 1/31
@@ -285,12 +275,12 @@ theorem goormaghtigh_passes_rrc (x m y n : ℕ)
       simp [kernelEvidence, hermitianRRCKernel, Hkdf, hermitePoly,
             projectionAdmissibleThreshold, projectionAdmissible, abs]
       norm_num
-    · -- mergeAdmissible: |R*(31) - R*(8191)| / (R*(31) + R*(8191)) < 10^-6
+    · -- mergeAdmissible: |R_5(2) - R_3(5)| / (R_5(2) + R_3(5)) < 10^-6
-      -- Both 31 and 8191 are Goormaghtigh collision values from base 2,
+      -- R_5(2) = 31 = R_3(5), so threshold = 0.
-      -- so repunit 31 5 = repunit 8191 13 = 2, and the threshold is 0.
+      -- so repunit 2 5 = repunit 5 3 = 31, and the threshold is 0.
       simp [kernelEvidence, mergeAdmissibleThreshold, mergeAdmissible, repunit]
       norm_num
-  · -- Second known solution: (8191, 13, 31, 5) -- symmetric
+  · -- Second known solution: (2, 13, 90, 3) -- symmetric
     rcases h with ⟨rfl, rfl, rfl, rfl⟩
     constructor
     · -- typeAdmissible: |kernel| < 1/8191
@@ -305,7 +295,7 @@ theorem goormaghtigh_passes_rrc (x m y n : ℕ)
             projectionAdmissibleThreshold, projectionAdmissible, abs]
       norm_num
     · -- mergeAdmissible: |R*(8191) - R*(31)| / (R*(8191) + R*(31)) < 10^-6
-      -- Both characteristics equal 2, so threshold is 0.
+      -- Both repunit values equal 31, so threshold is 0.
       simp [kernelEvidence, mergeAdmissibleThreshold, mergeAdmissible, repunit]
       norm_num
 
@@ -491,7 +481,7 @@ theorem unknown_fails_rrc (x m y n : ℕ)
 -- #eval hermitianRRCKernel 31 5 5 (-1:ℚ) (-1:ℚ)
 
 /-- Evaluate the merge threshold at the first known solution.
-    Expected: 0 (both repunit characteristics equal 2). -/
+    Expected: 0 (both repunit values equal 31 or 8191). -/
 -- #eval mergeAdmissibleThreshold 31 5 8191 13
 
 /-- Evaluate the merge threshold at the second known solution. -/
@@ -567,7 +557,7 @@ theorem rrc_characterizes_goormaghtigh (x m y n : ℕ)
   |    merge:      |R*_x(m) - R*_y(n)|/(R*_x(m) + R*_y(n)) < 10^-6      |
   +-----------------------------------------------------------------------+
   |  Theorems:                                                            |
-  |    goormaghtigh_passes_rrc:  (31,5,8191,13) and (8191,13,31,5)        |
+  |    goormaghtigh_passes_rrc:  (2,5,5,3) and (2,13,90,3)        |
   |                              pass all three gates                     |
   |    unknown_fails_rrc:        All other collisions fail merge          |
   |                              (Goormaghtigh conjecture)                |
@@ -579,7 +569,7 @@ theorem rrc_characterizes_goormaghtigh (x m y n : ℕ)
       the factorial blowup of H_n at large arguments
     * Exponential normalization γ^(m+n+1) guarantees witnesses below
       all gate thresholds for the known solutions
-    * Repunit characteristic function encodes Goormaghtigh structure:
+    * Standard mathematical repunit R_m(x) encodes Goormaghtigh structure:
       both collision values 31 and 8191 derive from base 2
     * The merge gate threshold 10^-6 captures the BMS separation bound