Shor's algorithm — period recovery (S5, uniqueness route)

Category: 3-Local (QM-validity), pure finite number theory.

Tranche S5 of specs/shor-plan.md. After phase estimation (S4) a single run yields a count c with |c/T - s/r| ≤ 1/(2T) for the true order r (s/r in lowest terms). This file proves the recovery-correctness content: that bound, together with r·r' < T, pins down s/r uniquely among lowest-terms fractions, so the order r is determined by the measurement.

The argument is the elementary "distinct fractions are far apart" estimate (abs_sub_rat_ge: distinct a/b, c/d differ by at least 1/(b·d)), not the continued-fraction machinery. Mathlib has the forward CF bound (abs_sub_convergents_le') but not the Legendre converse; this route sidesteps it.

Honest scope. This is the information-theoretic determination of r (why recovery is possible: the measurement has a unique consistent answer). It is NOT the constructive continued-fraction computation of r from c/T; the constructive Legendre-on-GenContFract extraction is a heavier, separately-scoped alternative, deferred.

Composition with S4 (QuantumInfo.phase_estimation_lower_bound, Mathlib/QuantumInfo/PhaseEstimation.lean since 2026-08-29, with the Shor corollary shor_phase_estimation_lower_bound in ShorCore.lean): S4 gives prob ≥ 4/π² for the closest-integer outcome, i.e. the event |c/T - s/r| ≤ 1/(2T); S5 shows that on that event r is determined. For Shor with T ≥ N² > r² (so r, r' < √T and r·r' < T with slack) a single run determines r with probability ≥ 4/π².

Tranche S6 (nontrivial_factor) adds the classical reduction "order-finding implies factoring": for an even order r of a unit a with a^(r/2) ≢ ±1 (mod N), the element x = a^(r/2) is a nontrivial square root of unity (N ∣ x²-1, N ∤ x±1), and gcd(x-1, N) is then a proper nontrivial divisor of N. This is the step that turns the quantum period output into an actual factor.

theorem CSD.Empirical.QM.Shor.abs_sub_rat_ge (a b c d : ℤ) (hb : 0 < b) (hd : 0 < d) (hne : ↑a / ↑b ≠ ↑c / ↑d) : 1 / (↑b * ↑d) ≤ |↑a / ↑b - ↑c / ↑d|

Distinct fractions are far apart: two unequal rationals a/b, c/d with positive denominators differ by at least 1/(b·d). The numerator a·d - c·b is a nonzero integer.

theorem CSD.Empirical.QM.Shor.approx_unique (x : ℚ) (a b c d : ℤ) (hb : 0 < b) (hd : 0 < d) (T : ℤ) (hbd : b * d < T) (h₁ : |x - ↑a / ↑b| ≤ 1 / (2 * ↑T)) (h₂ : |x - ↑c / ↑d| ≤ 1 / (2 * ↑T)) : ↑a / ↑b = ↑c / ↑d

Uniqueness of a close fraction: if a/b and c/d (positive denominators with b·d < T) are both within 1/(2T) of the same rational x, they are equal.

theorem CSD.Empirical.QM.Shor.shor_period_determined (c T s r s' r' : ℕ) (hr : 0 < r) (hr' : 0 < r') (hrr' : r * r' < T) (hcop : s.Coprime r) (hcop' : s'.Coprime r') (h : |↑c / ↑T - ↑s / ↑r| ≤ 1 / (2 * ↑T)) (h' : |↑c / ↑T - ↑s' / ↑r'| ≤ 1 / (2 * ↑T)) : s = s' ∧ r = r'

Shor period determination (headline): the measured count c determines the order r. Given the true s/r and any candidate s'/r', both in lowest terms with r·r' < T and both within 1/(2T) of c/T, the two coincide: s = s' and r = r'. So the order r is the unique denominator consistent with the measurement.

theorem CSD.Empirical.QM.Shor.nontrivial_factor (N : ℕ) (hN : 1 < N) (x : ℤ) (hsq : ↑N ∣ x ^ 2 - 1) (hne1 : ¬↑N ∣ x - 1) (hne2 : ¬↑N ∣ x + 1) : 1 < (x - 1).gcd ↑N ∧ (x - 1).gcd ↑N < N ∧ (x - 1).gcd ↑N ∣ N

S6 — factoring from a nontrivial square root of unity (the classical Shor step). If x is a nontrivial square root of 1 modulo N (so N ∣ x²-1 but N ∤ x-1 and N ∤ x+1), then g := gcd(x-1, N) is a proper nontrivial divisor of N: 1 < g, g < N, and g ∣ N. Here Int.gcd : ℤ → ℤ → ℕ, so all three conjuncts are statements about the natural number g. This is the reduction that converts the quantum order-finding output into an actual factor of N.

theorem CSD.Empirical.QM.Shor.N_has_nontrivial_factor (N : ℕ) (hN : 1 < N) (x : ℤ) (hsq : ↑N ∣ x ^ 2 - 1) (hne1 : ¬↑N ∣ x - 1) (hne2 : ¬↑N ∣ x + 1) : ∃ (d : ℕ), d ∣ N ∧ 1 < d ∧ d < N

S6 existential corollary: a nontrivial square root of unity exhibits a proper nontrivial divisor of N.

theorem CSD.Empirical.QM.Shor.even_order_sqrt_unity (N : ℕ) [NeZero N] (a : (ZMod N)ˣ) (hr : Even (orderOf a)) (hy1 : ↑(a ^ (orderOf a / 2)) ≠ 1) (hy2 : ↑(a ^ (orderOf a / 2)) ≠ -1) (x : ℤ) (hx : ↑x = ↑(a ^ (orderOf a / 2))) : ↑N ∣ x ^ 2 - 1 ∧ ¬↑N ∣ x - 1 ∧ ¬↑N ∣ x + 1

Bridge from an even-order unit to S6's nontrivial-square-root hypotheses. For a unit a of (ZMod N)ˣ of even order r = orderOf a with a^(r/2) ≢ ±1 (mod N), the integer x lifting y := a^(r/2) satisfies the three hypotheses of nontrivial_factor: N ∣ x²-1, N ∤ x-1, N ∤ x+1. The square-root content is y² = 1 (since (r/2)·2 = r and a^r = 1).

theorem CSD.Empirical.QM.Shor.shor_factor_of_even_order (N : ℕ) (hN : 1 < N) (a : (ZMod N)ˣ) (hr : Even (orderOf a)) (hy1 : ↑(a ^ (orderOf a / 2)) ≠ 1) (hy2 : ↑(a ^ (orderOf a / 2)) ≠ -1) (x : ℤ) (hx : ↑x = ↑(a ^ (orderOf a / 2))) : 1 < (x - 1).gcd ↑N ∧ (x - 1).gcd ↑N < N ∧ (x - 1).gcd ↑N ∣ N

Even order ⟹ factor (the full classical reduction order-finding ⟹ factoring). Composes even_order_sqrt_unity with nontrivial_factor: for an even order r of a unit a with a^(r/2) ≢ ±1 (mod N), the natural number gcd(a^(r/2)-1, N) (via the integer lift x) is a proper nontrivial divisor of N.