NumberTheory 35 declarations in 6 modules

FormalRV.NumberTheory.GoodElements

FormalRV/NumberTheory/GoodElements.lean

FormalRV.NumberTheory.GoodElements — the ≥1/2 success-probability bound for Shor's algorithm on a SEMIPRIME N = p·q (the RSA case), the standard textbook counting (Nielsen–Chuang A4.13). GOAL: a uniformly random `a ∈ (ℤ/N)ˣ` is "good" (even order `r`, `a^(r/2) ≢ −1 mod N`) with probability ≥ 1/2 — so the order→factoring reduction (`NumberTheory.ShorReduction`) succeeds after O(1) expected tries. STATUS — the two reusable KERNELS of the textbook counting are PROVEN here (axiom-clean): `diag_card_le` — PURE COMBINATORICS: if every fiber `{b : g b = k}` has ≤ c elements, the "diagonal" `{(a,b) : f a = g b}` has ≤ |A|·c elements. This is the `|bad| = ∑_v aᵥ·bᵥ ≤ (max atom)·|A|` step, instantiated with `A = (ℤ/p)ˣ`, `c = |（ℤ/q)ˣ|/2`. `card_sqrt_one_eq_two` — in a finite cyclic group of even order there are exactly two square roots of 1. `card_squares_eq_half` — exactly half the elements are squares (the squaring map is 2-to-1: each fiber is a coset of the 2-element kernel). [= R1] `card_atom_le_half` [R2] — every `v₂(ord)`-atom `{a : v₂(ord a)=v}` ≤ |G|/2 (each atom lands in `{ord ∣ |G|/2}` or its complement, both of size |G|/2; `{ord ∣ |G|/2}` counted via `∑φ = |G|/2`). `card_diag_v2_le_half` [R4 core] — for `G × H` both even cyclic, the diagonal `{(x,y) : v₂(ord x) = v₂(ord y)}` ≤ |G×H|/2. THE textbook Shor/Miller ≥1/2 counting. `orderOf_prod_mk` / `factorization_lcm_two` — `ord(a,b) = lcm`, `v₂(lcm) = max`. `prodBad_iff_diag` [R3] — `(x,y)` bad (`Odd(ord(x,y)) ∨ (x^(r/2)≠1 ∧ y^(r/2)≠1)`) ⟺ `v₂(ord x) = v₂(ord y)`. (The `≠ 1` form needs no order-2 element; the `= −1` identification is done at the field level in `ShorBadSet`.) Hence `card_prodBad_le_half` — bad set ≤ |G×H|/2. The transport to the actual Shor bad set on `(ℤ/N)ˣ` (`N = p·q`) — `card_bad_le_half` / `card_good_ge_half` — is in `FormalRV.NumberTheory.ShorBadSet` (CRT iso + field square roots). No `sorry`, no `native_decide`, no axioms beyond the prelude.

theoremdiag_card_le

theorem diag_card_le {A B : Type*} [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B]
    (f : A → ℕ) (g : B → ℕ) (c : ℕ)
    (hfib : ∀ k, (univ.filter (fun b : B => g b = k)).card ≤ c) :
    (univ.filter (fun p : A × B => f p.1 = g p.2)).card ≤ Fintype.card A * c

*Diagonal counting bound (pure combinatorics).** If for every `k` the fiber `{b : g b = k}` has at most `c` elements, then the diagonal `{(a,b) : f a = g b}` has at most `|A|·c` elements. This is the `∑_v Pr[d₁=v]·Pr[d₂=v] ≤ (max_v Pr[d₂=v])·1` step of the Shor counting, with `c = max atom`.

theoremcard_sqrt_one_eq_two

theorem card_sqrt_one_eq_two (G : Type*) [Group G] [Fintype G] [DecidableEq G] [IsCyclic G]
    (hev : 2 ∣ Fintype.card G) :
    (univ.filter (fun a : G => a ^ 2 = 1)).card = 2

*Square roots of 1 in a finite cyclic group of even order: exactly two** (`1` and the unique order-2 element). Via `IsCyclic.card_orderOf_eq_totient`: `a²=1 ⟺ orderOf a ∈ {1,2}`, and the order-1/order-2 classes have `φ(1)=φ(2)=1` elements each.

theoremcard_squares_eq_half

theorem card_squares_eq_half (G : Type*) [CommGroup G] [Fintype G] [DecidableEq G] [IsCyclic G]
    (hev : 2 ∣ Fintype.card G) :
    (univ.filter (fun a : G => IsSquare a)).card * 2 = Fintype.card G

*Exactly half the elements of a finite cyclic group of even order are squares.** The squaring map is 2-to-1 (each fiber is a coset of the 2-element kernel `{z : z²=1}`), so `|squares|·2 = |G|`.

theoremdvd_half_iff_factorization

private theorem dvd_half_iff_factorization (r n : ℕ) (hr : r ∣ n) (hn0 : 0 < n) (hev : 2 ∣ n) :
    r ∣ n / 2 ↔ r.factorization 2 < n.factorization 2

Nat arithmetic: with `r ∣ n` and `2 ∣ n`, `r ∣ n/2 ↔ v₂(r) < v₂(n)`.

theoremcard_orderOf_dvd_half

theorem card_orderOf_dvd_half (G : Type*) [Group G] [Fintype G] [DecidableEq G] [IsCyclic G]
    (hev : 2 ∣ Fintype.card G) :
    (univ.filter (fun a : G => orderOf a ∣ Fintype.card G / 2)).card = Fintype.card G / 2

In a finite cyclic group of even order, the elements whose order divides `|G|/2` are exactly half: `|{a : ord a ∣ |G|/2}| = |G|/2` (via `∑_{d ∣ |G|/2} φ(d) = |G|/2`).

theoremcard_atom_le_half

theorem card_atom_le_half (G : Type*) [Group G] [Fintype G] [DecidableEq G] [IsCyclic G]
    (hev : 2 ∣ Fintype.card G) (v : ℕ) :
    (univ.filter (fun a : G => (orderOf a).factorization 2 = v)).card ≤ Fintype.card G / 2

*★ (R2) Atom bound. ★** In a finite cyclic group of even order, for every `v` the set of elements whose order has 2-adic valuation `= v` has at most `|G|/2` elements: each atom lies entirely inside `{a : ord a ∣ |G|/2}` (if `v < v₂|G|`) or its complement (if `v = v₂|G|`), both of size `|G|/2`.

theoremcard_diag_v2_le_half

theorem card_diag_v2_le_half (G H : Type*) [Group G] [Group H] [Fintype G] [Fintype H]
    [DecidableEq G] [DecidableEq H] [IsCyclic G] [IsCyclic H]
    (hG : 2 ∣ Fintype.card G) (hH : 2 ∣ Fintype.card H) :
    (univ.filter (fun p : G × H =>
        (orderOf p.1).factorization 2 = (orderOf p.2).factorization 2)).card
      ≤ Fintype.card (G × H) / 2

*★ The diagonal `2`-adic-valuation set is at most half. ★** For `G × H` with both `G`, `H` finite cyclic of even order, the set of `(x,y)` with `v₂(ord x) = v₂(ord y)` has at most `|G×H|/2` elements. This is the textbook Shor/Miller counting: it bounds the "bad" set (which, through the CRT iso `(ℤ/N)ˣ ≅ (ℤ/p)ˣ×(ℤ/q)ˣ`, is exactly this diagonal — see `ShorReduction`). Proof: `diag_card_le` with `c = |H|/2` (every atom of `H` is ≤ `|H|/2`, `card_atom_le_half`).

theoremorderOf_prod_mk

theorem orderOf_prod_mk {G H : Type*} [Group G] [Group H] [Fintype G] [Fintype H]
    (a : G) (b : H) : orderOf (a, b) = Nat.lcm (orderOf a) (orderOf b)

`orderOf` in a product group is the `lcm` of the component orders.

theoremfactorization_lcm_two

theorem factorization_lcm_two (a b : ℕ) (ha : a ≠ 0) (hb : b ≠ 0) :
    (Nat.lcm a b).factorization 2 = max (a.factorization 2) (b.factorization 2)

`v₂(lcm a b) = max (v₂ a) (v₂ b)`.

theoremprodBad_iff_diag

theorem prodBad_iff_diag {G H : Type*} [Group G] [Group H] [Fintype G] [Fintype H]
    [DecidableEq G] [DecidableEq H] [IsCyclic G] [IsCyclic H]
    (x : G) (y : H) :
    (Odd (orderOf (x, y)) ∨
        (x ^ (orderOf (x, y) / 2) ≠ 1 ∧ y ^ (orderOf (x, y) / 2) ≠ 1))
      ↔ (orderOf x).factorization 2 = (orderOf y).factorization 2

*★ (R3) The bad set is exactly the `v₂`-diagonal. ★** In `G × H` (both finite cyclic of even order), an element `(x,y)` is "bad" — its order `r` is odd, OR both half-power components `x^(r/2)`, `y^(r/2)` are `≠ 1` (i.e. `(x,y)^(r/2)` is the order-2 element `(z₁,z₂)`, which for `(ℤ/p)ˣ` is `−1`) — **iff** `v₂(ord x) = v₂(ord y)`. This is the group-theoretic core of Shor's `≥ 1/2`: combined with `card_diag_v2_le_half`, the bad set has at most half the elements.

theoremcard_prodBad_le_half

theorem card_prodBad_le_half (G H : Type*) [Group G] [Group H] [Fintype G] [Fintype H]
    [DecidableEq G] [DecidableEq H] [IsCyclic G] [IsCyclic H]
    (hG : 2 ∣ Fintype.card G) (hH : 2 ∣ Fintype.card H) :
    (univ.filter (fun p : G × H => Odd (orderOf p) ∨
        (p.1 ^ (orderOf p / 2) ≠ 1 ∧ p.2 ^ (orderOf p / 2) ≠ 1))).card
      ≤ Fintype.card (G × H) / 2

*★ The bad set is at most half (abstract product form). ★** In `G × H` both finite cyclic of even order, the set of "bad" `(x,y)` (order odd, or both half-powers `≠ 1`) has at most `|G×H|/2` elements — the full Shor/Miller `≥ 1/2`, transported to `(ℤ/N)ˣ` in R4.

FormalRV.NumberTheory.NontrivialSqrt

FormalRV/NumberTheory/NontrivialSqrt.lean

FormalRV.NumberTheory.NontrivialSqrt — the deterministic heart of Shor's classical order→factoring reduction: a NONTRIVIAL square root of 1 mod N yields a NONTRIVIAL factor. ## Why this is THE necessary number theory Shor's quantum subroutine finds the multiplicative order `r` of `a` mod `N` (`FormalRV.SQIRPort.Shor_correct_var` : `probability_of_success ≥ κ/(log₂N)⁴`). By itself that does NOT factor `N` — the bridge from "order found" to "factor found" is purely classical number theory, and in this repo it was previously absent (`Framework.L1_Algorithm.rsa_correct` is literally `: True := trivial`). This file (and `OrderToFactor`, `ShorReduction`) supplies it. The crux: if `x² ≡ 1 (mod N)` but `x ≢ ±1 (mod N)`, then `N ∣ (x−1)(x+1)` while `N ∤ (x−1)` and `N ∤ (x+1)`, so `gcd(x−1, N)` is a PROPER, NONTRIVIAL divisor of `N` (`1 < gcd < N`). Taking `x = a^(r/2)` for an even order `r` with `a^(r/2) ≢ −1` gives Shor's factor. No `sorry`, no `native_decide`, no axioms beyond the prelude.

theoremnontrivialSqrt_factor

theorem nontrivialSqrt_factor (N : ℕ) (hN : 1 < N) (x : ℤ)
    (hsq : x ^ 2 ≡ 1 [ZMOD (N : ℤ)])
    (hne1 : ¬ x ≡ 1 [ZMOD (N : ℤ)])
    (hneg1 : ¬ x ≡ -1 [ZMOD (N : ℤ)]) :
    (Int.gcd (x - 1) (N : ℤ)) ∣ N
      ∧ 1 < Int.gcd (x - 1) (N : ℤ)
      ∧ Int.gcd (x - 1) (N : ℤ) < N

*★ A nontrivial square root of 1 gives a nontrivial factor. ★** If `x² ≡ 1 (mod N)` with `x ≢ 1` and `x ≢ −1 (mod N)` (and `N > 1`), then `gcd(x−1, N)` is a proper nontrivial divisor of `N`: it divides `N`, exceeds `1`, and is `< N`. This is the classical core of Shor's factoring reduction — no quantum content.

FormalRV.NumberTheory.OrderToFactor

FormalRV/NumberTheory/OrderToFactor.lean

FormalRV.NumberTheory.OrderToFactor — from a multiplicative ORDER to a nontrivial FACTOR. The classical step of Shor's algorithm: once the quantum subroutine has produced the order `r` of `a` mod `N`, IF `r` is even and `a^(r/2) ≢ −1 (mod N)`, then `x := a^(r/2)` is a nontrivial square root of 1 (`x² = a^r ≡ 1`, `x ≢ ±1`), so `gcd(x−1, N)` is a nontrivial factor of `N` (`NontrivialSqrt.nontrivialSqrt_factor`). When `r` is the EXACT order, `a^(r/2) ≢ 1` is automatic (minimality), so the only nondegeneracy hypothesis is `a^(r/2) ≢ −1` — the standard "good `a`" condition whose probability is bounded in `GoodElements`. No `sorry`, no `native_decide`, no axioms beyond the prelude.

theoremevenPow_factor

theorem evenPow_factor (N : ℕ) (hN : 1 < N) (a : ℤ) (r : ℕ)
    (hr_even : Even r)
    (hr1 : a ^ r ≡ 1 [ZMOD (N : ℤ)])
    (hhalf1 : ¬ a ^ (r / 2) ≡ 1 [ZMOD (N : ℤ)])
    (hhalf2 : ¬ a ^ (r / 2) ≡ -1 [ZMOD (N : ℤ)]) :
    ∃ d : ℕ, d ∣ N ∧ 1 < d ∧ d < N

*Even power giving a nontrivial factor.** If `r` is even, `a^r ≡ 1 (mod N)`, and `a^(r/2) ≢ ±1 (mod N)`, then `N` has a nontrivial factor (`gcd(a^(r/2)−1, N)`).

theoremorder_even_factor

theorem order_even_factor (N : ℕ) (hN : 1 < N) (a : ℤ) (r : ℕ)
    (hr_even : Even r) (hr_pos : 0 < r)
    (hr1 : a ^ r ≡ 1 [ZMOD (N : ℤ)])
    (hmin : ∀ k, 0 < k → k < r → ¬ a ^ k ≡ 1 [ZMOD (N : ℤ)])
    (hhalf2 : ¬ a ^ (r / 2) ≡ -1 [ZMOD (N : ℤ)]) :
    ∃ d : ℕ, d ∣ N ∧ 1 < d ∧ d < N

*★ Order → factor (the exact-order form). ★** If `r` is the EXACT multiplicative order of `a` mod `N` (i.e. `a^r ≡ 1` and `r` is minimal positive with this property), `r` is even, and `a^(r/2) ≢ −1 (mod N)`, then `N` has a nontrivial factor. The `a^(r/2) ≢ 1` clause is FREE here (it would contradict minimality), so the only "luck" needed of `a` is even order and `a^(r/2) ≢ −1`.

theoremcommon_factor

theorem common_factor (N : ℕ) (a : ℕ) (h1 : 1 < Nat.gcd a N) (h2 : Nat.gcd a N < N) :
    ∃ d : ℕ, d ∣ N ∧ 1 < d ∧ d < N

*The easy case: a common factor with `N`.** If `1 < gcd(a, N) < N` (i.e. `a` is NOT coprime to `N` and not a multiple), the gcd is itself a nontrivial factor — no order needed. (Shor's classical preprocessing: try `gcd(a,N)` first.)

FormalRV.NumberTheory.ShorBadSet

FormalRV/NumberTheory/ShorBadSet.lean

FormalRV.NumberTheory.ShorBadSet — (R4) the ≥1/2 good-element bound on `(ℤ/N)ˣ`, `N = p·q`. The abstract counting (`GoodElements.card_prodBad_le_half`) says: in a product of two finite cyclic groups of even order, the "bad" set (order odd, or both half-powers `≠ 1`) is at most half. Here we TRANSPORT that to the actual Shor bad set on `(ℤ/N)ˣ` for a semiprime `N = p·q` (distinct odd primes) via the CRT iso `(ℤ/N)ˣ ≅ (ℤ/p)ˣ × (ℤ/q)ˣ`, using that each `(ℤ/p)ˣ` is a field's unit group so the square roots of `1` are exactly `±1` — hence `s^(r/2) = −1 ↔ s^(r/2) ≠ 1`. Result: `card_bad_le_half` — `|{a ∈ (ℤ/N)ˣ : ord a odd ∨ a^(ord a/2) = −1}| ≤ φ(N)/2`. Combined with `ShorReduction.shor_classical_step_correct`, a uniformly random unit is "good" (yields a factor via Shor) with probability ≥ 1/2. No `sorry`, no `native_decide`, no axioms beyond the prelude.

theoremunits_sq_eq_one

theorem units_sq_eq_one {p : ℕ} [Fact p.Prime] (x : (ZMod p)ˣ) (h : x ^ 2 = 1) :
    x = 1 ∨ x = -1

In `(ℤ/p)ˣ` (a field's unit group) the only square roots of `1` are `±1`.

theoremunits_neg_one_ne_one

theorem units_neg_one_ne_one {p : ℕ} [Fact p.Prime] (hp : 2 < p) : (-1 : (ZMod p)ˣ) ≠ 1

For odd `p`, `−1 ≠ 1` in `(ℤ/p)ˣ`.

theoremunits_eq_neg_one_iff_ne_one

theorem units_eq_neg_one_iff_ne_one {p : ℕ} [Fact p.Prime] (hp : 2 < p) (s : (ZMod p)ˣ)
    (hs : s ^ 2 = 1) : s = -1 ↔ s ≠ 1

A square root of `1` in `(ℤ/p)ˣ` (`p` odd) is `−1` exactly when it is `≠ 1`.

theoremtwo_dvd_card_units

theorem two_dvd_card_units {p : ℕ} [Fact p.Prime] (hp : 2 < p) :
    2 ∣ Fintype.card (ZMod p)ˣ

`(ℤ/p)ˣ` has even order for odd primes `p`.

defunitsCRT

noncomputable def unitsCRT {p q : ℕ} (hcop : Nat.Coprime p q) :
    (ZMod (p * q))ˣ ≃* (ZMod p)ˣ × (ZMod q)ˣ

`(ℤ/(p·q))ˣ ≃* (ℤ/p)ˣ × (ℤ/q)ˣ` for coprime `p, q`.

theoremunitsCRT_neg_one

theorem unitsCRT_neg_one {p q : ℕ} (hcop : Nat.Coprime p q) :
    unitsCRT hcop (-1) = (-1, -1)

The CRT units iso sends `−1` to `(−1, −1)`.

theoremcard_bad_le_half

theorem card_bad_le_half {p q : ℕ} [Fact p.Prime] [Fact q.Prime]
    (hp : 2 < p) (hq : 2 < q) (hpq : p ≠ q) :
    (univ.filter (fun a : (ZMod (p * q))ˣ =>
        Odd (orderOf a) ∨ a ^ (orderOf a / 2) = -1)).card
      ≤ Fintype.card (ZMod (p * q))ˣ / 2

*★ (R4) The Shor bad set has at most half the units. ★** For `N = p·q` (distinct odd primes), `|{a ∈ (ℤ/N)ˣ : ord a odd ∨ a^(ord a/2) = −1}| ≤ φ(N)/2`. So a uniformly random unit is "good" (even order, `a^(r/2) ≢ −1` — yielding a factor via `shor_classical_step_correct`) with probability `≥ 1/2`. Transports `card_prodBad_le_half` along the CRT iso, converting the component `= −1` conditions to `≠ 1` via the field square-root dichotomy.

theoremcard_good_ge_half

theorem card_good_ge_half {p q : ℕ} [Fact p.Prime] [Fact q.Prime]
    (hp : 2 < p) (hq : 2 < q) (hpq : p ≠ q) :
    Fintype.card (ZMod (p * q))ˣ / 2
      ≤ (univ.filter (fun a : (ZMod (p * q))ˣ =>
          ¬ (Odd (orderOf a) ∨ a ^ (orderOf a / 2) = -1))).card

*★ At least half the units are "good". ★** For `N = p·q` (distinct odd primes), at least `φ(N)/2` units `a` have even order with `a^(ord a/2) ≢ −1` — i.e. Shor's classical step (`shor_classical_step_correct`) extracts a nontrivial factor from `a`. So picking `a` uniformly at random succeeds with probability `≥ 1/2`. Immediate complement of `card_bad_le_half`.

FormalRV.NumberTheory.ShorFactoringEndToEnd

FormalRV/NumberTheory/ShorFactoringEndToEnd.lean

FormalRV.NumberTheory.ShorFactoringEndToEnd — the END-TO-END Shor factoring success theorem. ════════════════════════════════════════════════════════════════════════════════════════════ GAP ④ CLOSED — axiom-clean, NO literature conjecture, NO Ekerå–Håstad heuristic. This composes the two already-axiom-clean halves of Shor's factoring algorithm into ONE factoring-success-probability bound on the actual measurement distribution: • QUANTUM order-finding (`Shor_correct_var_relaxed`, axiom-clean): with probability `≥ κ/(log₂N)⁴` the QPE measurement + continued-fraction post-processing `OF_post` recovers the true multiplicative order `r` of `a` mod `N`. • CLASSICAL reduction (`shor_classical_step_correct`, axiom-clean): for a GOOD base `a` (even order, `a^(r/2) ≢ −1`), the recovered order DETERMINISTICALLY yields a NONTRIVIAL FACTOR of `N` via the gcd step. • COUNTING (`card_good_ge_half`, axiom-clean): for `N = p·q` (distinct odd primes), at least half the bases are good. HEADLINE `shor_factoring_succeeds_good_base`: for a good base, `factoringSuccessProb a N m n anc u ≥ κ/(log₂N)⁴` ∧ `∃ d, d ∣ N ∧ 1 < d ∧ d < N`, where `factoringSuccessProb` is the measure of measurement outcomes whose post-processed order yields a nontrivial factor — i.e. the probability the algorithm outputs a FACTOR of `N`, not merely the order. WHY NO EKERÅ–HÅSTAD / ASSUMPTION 1: this is VANILLA order-finding (continued fractions on a full `m`-bit phase register, `Shor_correct_var_relaxed`). Ekerå–Håstad (short-exponent discrete log) is a qubit-COUNT optimisation that lets the phase register be shorter; it is NOT required for factoring CORRECTNESS, and its success heuristic ("Assumption 1") is therefore NOT invoked anywhere in this closure. No `sorry`, no `native_decide`, no axioms beyond the prelude.

deffactorWitnessed

def factorWitnessed (a N o : Nat) : Prop

A recovered order `o` WITNESSES a factor of `N`: it is the true even multiplicative order of `a` mod `N` (positive, `a^o ≡ 1`, minimal) with `a^(o/2) ≢ −1` — exactly Shor's good condition. By minimality this holds iff `o = ord_N(a)` and `a` is a good base.

theoremfactorWitnessed_yields_factor

theorem factorWitnessed_yields_factor {a N o : Nat} (hN : 1 < N)
    (h : factorWitnessed a N o) : ∃ d : ℕ, d ∣ N ∧ 1 < d ∧ d < N

A witnessed order deterministically yields a nontrivial factor (Shor's classical gcd step).

theorempow_modEq_one_int

theorem pow_modEq_one_int {a r N : Nat} (hN : 1 < N) (h : a ^ r % N = 1) :
    (a : ℤ) ^ r ≡ 1 [ZMOD (N : ℤ)]

`a^r % N = 1` ⇒ `(a:ℤ)^r ≡ 1 [ZMOD N]` (for `1 < N`).

theorempow_ne_one_int

theorem pow_ne_one_int {a r N : Nat} (hN : 1 < N)
    (hmin : ∀ s, 0 < s → s < r → a ^ s % N ≠ 1) :
    ∀ k, 0 < k → k < r → ¬ (a : ℤ) ^ k ≡ 1 [ZMOD (N : ℤ)]

minimality transfer: `∀ s, a^s % N ≠ 1` ⇒ `∀ k, ¬ (a:ℤ)^k ≡ 1 [ZMOD N]` (for `1 < N`).

deffactorIndicator

noncomputable def factorIndicator (a N o : Nat) : ℝ

0/1 indicator: the post-processed order `o` from a measurement outcome yields a factor.

deffactoringSuccessProb

noncomputable def factoringSuccessProb (a N m n anc : Nat)
    (u : Nat → BaseUCom (n + anc)) : ℝ

*The factoring-success probability** — the measure of measurement outcomes `x` whose continued-fraction-recovered order `OF_post a N x m` yields a nontrivial factor of `N`. This is the probability the WHOLE algorithm (QPE + post-processing + classical gcd) outputs a FACTOR of `N`, not merely the order.

theoremr_found_le_factorIndicator

theorem r_found_le_factorIndicator {a r N : Nat} (hN : 1 < N)
    (h_ord : Order a r N) (hr_even : Even r)
    (hgood : ¬ (a : ℤ) ^ (r / 2) ≡ -1 [ZMOD (N : ℤ)])
    (x m : Nat) :
    r_found x m r a N ≤ factorIndicator a N (OF_post a N x m)

For a good base, every outcome that recovers the true order is also a factor-yielding outcome: `r_found x m r a N ≤ factorIndicator a N (OF_post a N x m)`.

theoremshor_factoring_succeeds_good_base

theorem shor_factoring_succeeds_good_base
    {a r N m n anc : Nat} {u : Nat → BaseUCom (n + anc)}
    (h_setting : BasicSettingRelaxed a r N m n)
    (h_modmul : ModMulImpl a N n anc u)
    (h_wt : ∀ i, i < m → uc_well_typed (u i))
    (hN : 1 < N)
    (hr_even : Even r)
    (hgood : ¬ (a : ℤ) ^ (r / 2) ≡ -1 [ZMOD (N : ℤ)]) :
    factoringSuccessProb a N m n anc u ≥ κ / (Nat.log2 N : ℝ) ^ 4
    ∧ ∃ d : ℕ, d ∣ N ∧ 1 < d ∧ d < N

*★ GAP ④ CLOSED — end-to-end Shor factoring success for a good base ★.** For a base `a` with (even) multiplicative order `r` mod `N` and `a^(r/2) ≢ −1` (a "good" base), running Shor's algorithm with ANY correct modular-multiplier family `u`: 1. outputs a nontrivial factor of `N` with probability `≥ κ/(log₂N)⁴` (`factoringSuccessProb`), and 2. the factor concretely exists (`∃ d, d ∣ N ∧ 1 < d ∧ d < N`). Both halves are axiom-clean: (1) composes the quantum order-finding bound (`Shor_correct_var_relaxed`) with the deterministic classical reduction, since recovering the order entails recovering a factor for a good base; (2) is `shor_classical_step_correct`. This is VANILLA order-finding — no Ekerå–Håstad, no Assumption 1.

theoremgood_base_fraction_ge_half

theorem good_base_fraction_ge_half {p q : ℕ} [Fact p.Prime] [Fact q.Prime]
    (hp : 2 < p) (hq : 2 < q) (hpq : p ≠ q) :
    Fintype.card (ZMod (p * q))ˣ / 2 ≤
      (Finset.univ.filter (fun a : (ZMod (p * q))ˣ =>
        ¬ (Odd (orderOf a) ∨ a ^ (orderOf a / 2) = -1))).card

*The good-base fraction is `≥ ½`.** For `N = p·q` (distinct odd primes) at least half the units `a ∈ (ℤ/N)ˣ` are good (even order, `a^(ord/2) ≠ −1`) — so a uniformly random base feeds `shor_factoring_succeeds_good_base` with probability `≥ 1/2`, giving the standard `O((log N)⁴)`-expected-shot factoring algorithm. Re-exported from `card_good_ge_half`.

FormalRV.NumberTheory.ShorReduction

FormalRV/NumberTheory/ShorReduction.lean

FormalRV.NumberTheory.ShorReduction — Shor's classical order→factoring reduction, assembled. This is the number theory that turns the quantum order-finding output into a FACTOR of N — the link that `Framework.L1_Algorithm.rsa_correct` (`: True := trivial`) was missing. PROVEN here (axiom-clean): `shor_classical_step_correct` — if order-finding returns an even order `r` of `a` mod `N` with `a^(r/2) ≢ −1`, the classical gcd step yields a NONTRIVIAL factor (the deterministic reduction). `nontrivialSqrt_exists` — for `N = m·n` coprime with `m,n > 2` (every non-prime-power odd N has such a split), a nontrivial square root of 1 EXISTS — so the reduction is non-vacuous: a factor-yielding `a` is always present. REMAINING (the heavy, standard counting — stated, not faked): the success-probability bound `goodElementFraction N ≥ 1/2` (a uniformly random coprime `a` has even order with `a^(r/2) ≢ −1` with probability ≥ 1/2), which needs the CRT decomposition of `(ℤ/N)ˣ`, the cyclic structure of `(ℤ/pᵏ)ˣ`, and the 2-adic-valuation "all-equal" counting (Shor/Miller). See `GoodElements`. No `sorry`, no `native_decide`, no axioms beyond the prelude.

theoremshor_classical_step_correct

theorem shor_classical_step_correct (N : ℕ) (hN : 1 < N) (a : ℤ) (r : ℕ)
    (hr_even : Even r) (hr_pos : 0 < r)
    (hr_ord : a ^ r ≡ 1 [ZMOD (N : ℤ)])
    (hr_min : ∀ k, 0 < k → k < r → ¬ a ^ k ≡ 1 [ZMOD (N : ℤ)])
    (hgood : ¬ a ^ (r / 2) ≡ -1 [ZMOD (N : ℤ)]) :
    ∃ d : ℕ, d ∣ N ∧ 1 < d ∧ d < N

*★ Shor's classical step is correct. ★** The number-theoretic content of "order-finding ⇒ factoring": given the (true, even) multiplicative order `r` of `a` mod `N` with `a^(r/2) ≢ −1`, the classical post-processing returns a nontrivial factor of `N`. `r` minimal (the exact order) makes the `a^(r/2) ≢ 1` clause automatic.

theoremnontrivialSqrt_exists

theorem nontrivialSqrt_exists (m n : ℕ) (hm : 2 < m) (hn : 2 < n) (hcop : Nat.Coprime m n) :
    ∃ x : ℤ, x ^ 2 ≡ 1 [ZMOD ((m * n : ℕ) : ℤ)]
      ∧ ¬ x ≡ 1 [ZMOD ((m * n : ℕ) : ℤ)]
      ∧ ¬ x ≡ -1 [ZMOD ((m * n : ℕ) : ℤ)]

*Non-vacuity via CRT: a nontrivial square root of 1 always exists** when `N = m·n` with `m, n` coprime and both `> 2`. (Every odd `N` that is not a prime power admits such a split, e.g. `m = pᵏ`, `n = N/pᵏ`.) So Shor's reduction always has a factor-yielding witness.

theoremfactor_of_coprime_split

theorem factor_of_coprime_split (m n : ℕ) (hm : 2 < m) (hn : 2 < n) (hcop : Nat.Coprime m n) :
    ∃ d : ℕ, d ∣ (m * n) ∧ 1 < d ∧ d < m * n

*Putting it together: a coprime non-prime-power split always yields a nontrivial factor of `N = m·n` via a nontrivial square root.** (The efficient route to such a square root is Shor's quantum order-finding + `shor_classical_step_correct`; this records that the target exists and is extractable by `gcd`.)