Shor's algorithm — factoring capstone (ties GOOD ⟹ nontrivial factor of N)

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

This file closes the Shor classical-reduction chain by connecting the GOOD success predicate (Even (orderOf a) ∧ a ^ (orderOf a / 2) ≠ -1, in the units group (ZMod N)ˣ, the object the random-a probability bound shor_success_prob_ge_general counts) to an actual nontrivial divisor of N (the object the factoring reduction shor_factor_of_even_order / nontrivial_factor produces).

Two results:

• shor_random_a_yields_factor — pointwise: a GOOD unit a yields a proper nontrivial factor gcd(x - 1, N) of N, where x lifts a ^ (orderOf a / 2). Bridges the units-group ≠ ±1 conditions of the GOOD predicate to the ZMod-coercion ≠ ±1 hypotheses of shor_factor_of_even_order.
• shor_factor_prob_ge — probability capstone: a uniformly random unit a mod N (odd, with ≥ 2 distinct prime factors) yields a proper nontrivial factor with probability ≥ 1/2. The GOOD filter is contained in the factor-yielding filter (shor_random_a_yields_factor), so the ≥ 1/2 bound on the GOOD frequency (shor_success_prob_ge_general) transports to the factor frequency by Finset cardinality monotonicity and ℚ division monotonicity.

Both are foundational-triple-only (no busch_effect_gleason, no measure axioms): the content is elementary finite number theory composed on top of the already-verified S6 reduction and the S7 counting bound.

theorem CSD.Empirical.QM.Shor.shor_random_a_yields_factor (N : ℕ) (hN : 1 < N) (a : (ZMod N)ˣ) (hgood : Even (orderOf a) ∧ 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

Pointwise: a GOOD unit yields a nontrivial factor. For a : (ZMod N)ˣ satisfying the Shor GOOD predicate (Even (orderOf a) and a ^ (orderOf a / 2) ≠ -1 in the units group) and any integer x lifting a ^ (orderOf a / 2), the natural number gcd(x - 1, N) is a proper nontrivial divisor of N.

Bridges the units-group ≠ -1 condition (and the derived ≠ 1) to the ZMod-coercion hypotheses of shor_factor_of_even_order (S6). The ≠ 1 side is derived from 0 < orderOf a / 2 < orderOf a (so orderOf a ∤ orderOf a / 2, hence a ^ (orderOf a / 2) ≠ 1 by orderOf_dvd_iff_pow_eq_one); both ±1 units conditions are pushed to the coercion via Units.val_inj (Units.val_eq_one for 1, Units.val_neg/Units.val_one for -1).

theorem CSD.Empirical.QM.Shor.shor_factor_prob_ge (N : ℕ) [NeZero N] (hodd : Odd N) (hN : 2 ≤ N.primeFactors.card) : 1 / 2 ≤ ↑{a : (ZMod N)ˣ | 1 < (↑(↑(a ^ (orderOf a / 2))).val - 1).gcd ↑N ∧ (↑(↑(a ^ (orderOf a / 2))).val - 1).gcd ↑N < N}.card / ↑(Fintype.card (ZMod N)ˣ)

Probability capstone: a random unit yields a nontrivial factor with probability ≥ 1/2. For odd N with at least two distinct prime factors, the fraction of units a : (ZMod N)ˣ for which the canonical integer representative of a ^ (orderOf a / 2) yields a proper nontrivial divisor gcd(· - 1, N) of N is at least 1/2.

The canonical representative is xrep a := (((a ^ (orderOf a / 2) : (ZMod N)ˣ) : ZMod N).val : ℤ), which lifts a ^ (orderOf a / 2) (hxrep below, via Int.cast_natCast + ZMod.natCast_val + ZMod.cast_id). By shor_random_a_yields_factor every GOOD unit lands in the factor-yielding filter, so the GOOD filter is ⊆ the factor filter; cardinality monotonicity (Finset.card_le_card) and ℚ division monotonicity (gcongr) then transport the ≥ 1/2 GOOD frequency bound (shor_success_prob_ge_general) to the factor frequency.