IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Factorization.EvenPeriodGap

   1/-
   2  PrimitiveRecognitionCalculus/Factorization/EvenPeriodGap.lean
   3
   4  Capstone of the period-to-factor chain. With period existence (Euler, in
   5  `PeriodExistence`) and gcd extraction (in `PeriodFactor`) both proved, the only
   6  remaining link is the existence of a unit residue whose period is even and
   7  whose half-power avoids ±1. This file proves the conditional closure: such a
   8  witness yields a nontrivial factorization. It names the existence as the single
   9  open lane (the δ form of Shor's success condition), and does not assert it.
  10-/
  11
  12import Mathlib
  13import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Factorization.PeriodFactor
  14
  15namespace IndisputableMonolith
  16namespace Foundation
  17namespace PrimitiveRecognitionCalculus
  18namespace Factorization
  19
  20open DistinctionNat
  21
  22/-- A unit residue with an even-period gap: `base` has a full period `half + half`
  23returning to the identity, while the half-power avoids both `1` and `-1` modulo
  24`N`. This is exactly the configuration Shor's algorithm needs after period
  25finding. -/
  26structure EvenPeriodGapWitness (N : DistinctionNat) (hN : N ≠ zero) : Type where
  27  base : DistinctionNat
  28  half : DistinctionNat
  29  base_unit : unitResidue N base
  30  full_period : sameResidue N hN (orbitPow base (half + half)) one
  31  half_not_one : ¬ N.toNat ∣ ((orbitPow base half).toNat - 1)
  32  half_not_neg_one : ¬ N.toNat ∣ ((orbitPow base half).toNat + 1)
  33
  34/-- The conditional closure: an even-period-gap witness produces a native
  35nontrivial factorization of `N`. This reduces period-based factoring to a single
  36existence statement. -/
  37theorem nontrivialFactorization_of_evenPeriodGapWitness {N : DistinctionNat}
  38    {hN : N ≠ zero} (hN2 : 2 ≤ N.toNat) (w : EvenPeriodGapWitness N hN) :
  39    nontrivialFactorization N := by
  40  have hbase_pos : 1 ≤ w.base.toNat := by
  41    have hcop := (unitResidue_iff_nat_coprime N w.base).mp w.base_unit
  42    rcases Nat.eq_zero_or_pos w.base.toNat with h0 | h0
  43    · rw [h0, Nat.coprime_zero_left] at hcop
  44      omega
  45    · omega
  46  have hb1 : 1 ≤ (orbitPow w.base w.half).toNat := by
  47    rw [orbitPow_toNat]
  48    exact Nat.one_le_pow _ _ hbase_pos
  49  have hsqeq : (orbitPow w.base (w.half + w.half)).toNat
  50      = (orbitPow w.base w.half).toNat ^ 2 := by
  51    rw [orbitPow_toNat, orbitPow_toNat, toNat_add, pow_two, ← pow_add]
  52  have hmod : (orbitPow w.base (w.half + w.half)).toNat % N.toNat = 1 % N.toNat := by
  53    have hp := (sameResidue_iff_mod_eq N hN _ _).mp w.full_period
  54    rwa [one_toNat] at hp
  55  have hsq : N.toNat ∣ (orbitPow w.base w.half).toNat ^ 2 - 1 := by
  56    rw [← hsqeq]
  57    have hge : 1 ≤ (orbitPow w.base (w.half + w.half)).toNat := by
  58      rw [hsqeq]
  59      exact Nat.one_le_pow _ _ hb1
  60    rw [← Nat.modEq_iff_dvd' hge]
  61    exact hmod.symm
  62  exact nontrivialFactorization_of_even_period_gap hN hN2 hb1 hsq
  63    w.half_not_one w.half_not_neg_one
  64
  65/-- The single open lane, stated precisely: for the modulus `N`, does a unit
  66residue with an even-period gap exist? This is the δ form of Shor's success
  67condition. It is OPEN here. Proving it (the ≥ 1/2 counting bound over the unit
  68group of a composite with at least two distinct odd prime factors) would close
  69period-based factoring end to end. This definition asserts nothing; it only
  70names the residual. -/
  71def EvenPeriodGapExists (N : DistinctionNat) (hN : N ≠ zero) : Prop :=
  72  Nonempty (EvenPeriodGapWitness N hN)
  73
  74/-- If the open existence holds for `N`, then `N` has a nontrivial factorization.
  75The reduction is unconditional; only the existence input is open. -/
  76theorem nontrivialFactorization_of_evenPeriodGapExists {N : DistinctionNat}
  77    {hN : N ≠ zero} (hN2 : 2 ≤ N.toNat) (h : EvenPeriodGapExists N hN) :
  78    nontrivialFactorization N := by
  79  obtain ⟨w⟩ := h
  80  exact nontrivialFactorization_of_evenPeriodGapWitness hN2 w
  81
  82/-- Certificate for the even-period-gap reduction. It records the proved
  83conditional and is explicit that the existence input is not supplied here. -/
  84structure EvenPeriodGapCertificate : Prop where
  85  witness_factorizes :
  86    ∀ {N : DistinctionNat} {hN : N ≠ zero}, 2 ≤ N.toNat →
  87      EvenPeriodGapWitness N hN → nontrivialFactorization N
  88  existence_reduces_to_factorization :
  89    ∀ {N : DistinctionNat} {hN : N ≠ zero}, 2 ≤ N.toNat →
  90      EvenPeriodGapExists N hN → nontrivialFactorization N
  91
  92theorem even_period_gap_certificate : EvenPeriodGapCertificate where
  93  witness_factorizes := by
  94    intro N hN hN2 w
  95    exact nontrivialFactorization_of_evenPeriodGapWitness hN2 w
  96  existence_reduces_to_factorization := by
  97    intro N hN hN2 h
  98    exact nontrivialFactorization_of_evenPeriodGapExists hN2 h
  99
 100end Factorization
 101end PrimitiveRecognitionCalculus
 102end Foundation
 103end IndisputableMonolith
 104