IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Factorization.PeriodFactor

   1/-
   2  PrimitiveRecognitionCalculus/Factorization/PeriodFactor.lean
   3
   4  The gcd-extraction step of period-based factoring, proved (not stored). Given
   5  a half-period element `b = a^(r/2)` with `b^2 ≡ 1 (mod N)` but `b ≢ ±1`, the
   6  gcd `gcd(b - 1, N)` is a proper nontrivial divisor of `N`. This is the content
   7  Shor's algorithm reads after period finding; here it is a δ theorem, not a
   8  device hypothesis.
   9
  10  This closes the A3 exit claim. It says nothing about the cost of producing the
  11  period `r`; that remains the open performance lane.
  12-/
  13
  14import Mathlib
  15import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Factorization.PeriodSpectrum
  16
  17namespace IndisputableMonolith
  18namespace Foundation
  19namespace PrimitiveRecognitionCalculus
  20namespace Factorization
  21
  22open DistinctionNat
  23
  24/-! ## Nat-level gcd extraction -/
  25
  26/-- The square-difference factorization holds in `ℕ` truncated subtraction for
  27`b ≥ 1`. -/
  28theorem sub_mul_add_eq_sq_sub_one {b : ℕ} (hb : 1 ≤ b) :
  29    (b - 1) * (b + 1) = b ^ 2 - 1 := by
  30  have key : (b - 1) * (b + 1) + 1 = b * b := by
  31    obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hb
  32    rw [Nat.add_sub_cancel_left]
  33    ring
  34  have hfac : (b - 1) * (b + 1) = b * b - 1 := Nat.eq_sub_of_add_eq key
  35  rw [hfac, pow_two]
  36
  37/-- Even-period factor extraction. If `b^2 ≡ 1 (mod n)` while `b ≢ 1` and
  38`b ≢ -1 (mod n)`, then `gcd(b - 1, n)` is strictly between `1` and `n`, hence a
  39proper nontrivial divisor of `n`. -/
  40theorem even_period_yields_factor
  41    {n b : ℕ} (hn : 2 ≤ n) (hb : 1 ≤ b)
  42    (hsq : n ∣ b ^ 2 - 1)
  43    (hm1 : ¬ n ∣ (b - 1))
  44    (hp1 : ¬ n ∣ (b + 1)) :
  45    1 < Nat.gcd (b - 1) n ∧ Nat.gcd (b - 1) n < n := by
  46  have hfac : (b - 1) * (b + 1) = b ^ 2 - 1 := sub_mul_add_eq_sq_sub_one hb
  47  have hdvd_prod : n ∣ (b - 1) * (b + 1) := by
  48    rw [hfac]; exact hsq
  49  have hgdvdN : Nat.gcd (b - 1) n ∣ n := Nat.gcd_dvd_right (b - 1) n
  50  have hgne_n : Nat.gcd (b - 1) n ≠ n := by
  51    intro h
  52    apply hm1
  53    have hgL : Nat.gcd (b - 1) n ∣ (b - 1) := Nat.gcd_dvd_left (b - 1) n
  54    rw [h] at hgL
  55    exact hgL
  56  have hg_lt : Nat.gcd (b - 1) n < n :=
  57    lt_of_le_of_ne (Nat.le_of_dvd (by omega) hgdvdN) hgne_n
  58  have hg_ne1 : Nat.gcd (b - 1) n ≠ 1 := by
  59    intro h
  60    have hcop : Nat.Coprime (b - 1) n := h
  61    have hn_dvd : n ∣ (b + 1) := hcop.symm.dvd_of_dvd_mul_left hdvd_prod
  62    exact hp1 hn_dvd
  63  have hg_pos : 0 < Nat.gcd (b - 1) n :=
  64    Nat.gcd_pos_iff.mpr (Or.inr (by omega))
  65  exact ⟨by omega, hg_lt⟩
  66
  67/-! ## δ-level corollary -/
  68
  69/-- δ form: an even-period gap on `N` produces a native nontrivial factorization
  70of `N`, with the extracted divisor `ofNat (gcd(b - 1, N))`. The hypotheses are
  71exactly what a certified period witness supplies through the residue display. -/
  72theorem nontrivialFactorization_of_even_period_gap
  73    {N b : DistinctionNat} (hN : N ≠ zero) (hN2 : 2 ≤ N.toNat)
  74    (hb1 : 1 ≤ b.toNat)
  75    (hsq : N.toNat ∣ b.toNat ^ 2 - 1)
  76    (hm1 : ¬ N.toNat ∣ (b.toNat - 1))
  77    (hp1 : ¬ N.toNat ∣ (b.toNat + 1)) :
  78    nontrivialFactorization N := by
  79  obtain ⟨hg1, hglt⟩ := even_period_yields_factor hN2 hb1 hsq hm1 hp1
  80  have hgdvdN : Nat.gcd (b.toNat - 1) N.toNat ∣ N.toNat :=
  81    Nat.gcd_dvd_right _ _
  82  refine nontrivialFactorization_of_proper_divisor
  83    (d := ofNat (Nat.gcd (b.toNat - 1) N.toNat)) hN ?_ ?_ ?_ ?_
  84  · intro h
  85    have hh := congrArg DistinctionNat.toNat h
  86    rw [toNat_ofNat, toNat_zero] at hh
  87    omega
  88  · rw [unit_iff_toNat_eq_one, toNat_ofNat]
  89    omega
  90  · intro h
  91    have hh := congrArg DistinctionNat.toNat h
  92    rw [toNat_ofNat] at hh
  93    omega
  94  · rw [divides_iff_toNat_dvd, toNat_ofNat]
  95    exact hgdvdN
  96
  97/-- Certificate for the period-factor extraction surface. -/
  98structure PeriodFactorCertificate : Prop where
  99  nat_even_period_extracts :
 100    ∀ {n b : ℕ}, 2 ≤ n → 1 ≤ b → n ∣ b ^ 2 - 1 →
 101      ¬ n ∣ (b - 1) → ¬ n ∣ (b + 1) →
 102        1 < Nat.gcd (b - 1) n ∧ Nat.gcd (b - 1) n < n
 103  delta_even_period_factorizes :
 104    ∀ {N b : DistinctionNat}, N ≠ zero → 2 ≤ N.toNat → 1 ≤ b.toNat →
 105      N.toNat ∣ b.toNat ^ 2 - 1 →
 106      ¬ N.toNat ∣ (b.toNat - 1) → ¬ N.toNat ∣ (b.toNat + 1) →
 107        nontrivialFactorization N
 108
 109theorem period_factor_certificate : PeriodFactorCertificate where
 110  nat_even_period_extracts := by
 111    intro n b hn hb hsq hm1 hp1
 112    exact even_period_yields_factor hn hb hsq hm1 hp1
 113  delta_even_period_factorizes := by
 114    intro N b hN hN2 hb1 hsq hm1 hp1
 115    exact nontrivialFactorization_of_even_period_gap hN hN2 hb1 hsq hm1 hp1
 116
 117end Factorization
 118end PrimitiveRecognitionCalculus
 119end Foundation
 120end IndisputableMonolith
 121