Shor's algorithm — random-a success, per-cyclic-factor v₂ distribution bound (S7b) #
Category: 3-Local (QM-validity), pure finite group theory.
Tranche S7b of specs/shor-plan.md §S7 — the meaty, self-contained, reusable core of the
random-a ≥ 1/2 success-probability argument. In a finite cyclic group G of even order, no
single "2-adic-valuation-of-order" class can exceed half the group:
2 · #{a ∈ G : v₂(orderOf a) = k} ≤ |G| for every k.
This is the per-factor input to the CRT counting bound (S7a/S7d): the per-prime-power factors of
(ZMod N)ˣ are cyclic of even order, and this bound on each factor drives 2·#BAD ≤ |G|.
Route (generator, not totient) #
Let n = |G|, c = v₂(n) (so c ≥ 1 since n is even). Pick a generator g
(IsCyclic.exists_generator), with orderOf g = n. The power map t : Fin n ↦ g ^ t is a
bijection Fin n ≃ G (pow_injOn_Iio_orderOf + a card count). Under it the order-valuation class
transports to a subset of a parity class of Fin n:
orderOf (g ^ t) = n / gcd n t(orderOf_pow+orderOf g = n);v₂(orderOf (g ^ t)) = c − min(c, v₂ t)(Nat.factorization_divon the divisorgcd n t- hence
v₂(orderOf (g ^ t)) = c ⟺ v₂ t = 0 ⟺ t odd, and any classk ≠ cforcesv₂ t ≥ 1, i.e.teven.
So the class k = c injects into {t : Fin n | t odd} and every class k ≠ c injects into
{t : Fin n | t even}; each parity class of Fin n has cardinality n/2 (Nat.card_multiples
for the odd residues, complement for the even). Therefore every class has cardinality ≤ n/2,
i.e. 2 · #class ≤ n.
This avoids the divisor-reindexing of the totient route (IsCyclic.card_orderOf_eq_totient +
Nat.sum_totient); the generator bijection carries the whole count.
Honest scope. S7b only. The −1-characterisation (S7c), the two-factor CRT framing (S7a), and
the assembly into 2·#GOOD ≥ |G| (S7d) are separate, not in this file.
The valuation fact. For g a generator of G with orderOf g = n and 0 < t < n,
the 2-adic valuation of orderOf (g ^ t) is v₂ n − min(v₂ n, v₂ t).
Uses orderOf_pow (orderOf (g^t) = n / gcd n t), Nat.factorization_div (on the divisor
gcd n t), and Nat.factorization_gcd.
The per-cyclic-factor 2-adic-valuation distribution bound (S7b).
In a finite cyclic group G of even order, no single "2-adic-valuation-of-order" class exceeds
half the group:
2 · #{a ∈ G : v₂(orderOf a) = k} ≤ |G| for every k.
where v₂(orderOf a) = (orderOf a).factorization 2.
Route: generator bijection t : Fin n ↦ g ^ t, the valuation fact v2_orderOf_pow, and parity
counting (card_odd_fin / card_even_fin). The class k = c := v₂ n injects into the odd
residues; every class k ≠ c injects into the even residues; each parity class has n/2 elements.
S7c — the −1 characterisation (abstract cyclic core) #
In a finite cyclic group G, the unique order-2 element z (e.g. -1 in a units group) is hit
by a ^ (R/2) exactly when the 2-adic valuation of orderOf a equals that of R. This is the
per-cyclic-factor core of Shor's "a^(r/2) = -1" success condition (S7).
ℕ valuation lemma (Step A). For m ∣ R with R even and both nonzero, m divides the
half R/2 iff its 2-adic valuation is strictly below that of R. The non-2 primes are
unconstrained by halving (m ∣ R already bounds them); the p = 2 slot drops by exactly one
(Nat.factorization_div on the divisor 2, (2).factorization = single 2 1).
Square-root-of-1 dichotomy in a finite cyclic group (Step B). If w ^ 2 = 1 and z is an
order-2 element of the cyclic group, then w is either 1 or z: the order-2 elements form a
singleton (IsCyclic.card_orderOf_eq_totient, Nat.totient 2 = 1), so w of order 2 must equal
z.
S7c — the −1 characterisation, abstract cyclic core.
In a finite cyclic group G with unique order-2 element z, and a an element whose order
divides an even R ≠ 0:
a ^ (R / 2) = z ↔ v₂(orderOf a) = v₂(R).
a ^ (R/2) is a square-root of 1 (its square is a ^ R = 1), so by the cyclic dichotomy
(sqrt_one_dichotomy) it is 1 or z. It is 1 exactly when orderOf a ∣ R/2, i.e.
v₂(orderOf a) < v₂(R) (dvd_half_iff_v2_lt). Since orderOf a ∣ R forces
v₂(orderOf a) ≤ v₂(R), the negation of the strict inequality is precisely equality, which is
therefore equivalent to hitting z. This is the per-cyclic-factor input to the Shor
a^(r/2) = -1 success condition.
S7a — two-factor CRT framing for units #
The Chinese Remainder Theorem gives a ring isomorphism ZMod (m*n) ≃+* ZMod m × ZMod n
for coprime m, n (ZMod.chineseRemainder). Restricting to units and splitting the product
gives a multiplicative isomorphism (ZMod (m*n))ˣ ≃* (ZMod m)ˣ × (ZMod n)ˣ. This is the
two-factor framing the S7d assembly needs: it transports orderOf to an lcm of per-factor
orders (unitsCRT_orderOf), sends the success witness -1 to the per-factor (-1, -1)
(unitsCRT_neg_one), and factors the group cardinality (card_units_mul).
Cyclicity-agnostic. Nothing here uses cyclicity of the factors; it holds for any coprime
m, n. Cyclicity of the per-prime-power factors enters only in S7d, where this framing is
iterated against the prime-power factorisation of N.
The CRT units isomorphism (S7a). For coprime m, n, the units of ZMod (m*n) split
as a product of the units of each factor:
(ZMod (m*n))ˣ ≃* (ZMod m)ˣ × (ZMod n)ˣ.
Built from the ring CRT iso ZMod.chineseRemainder by Units.mapEquiv (units functor on a
MulEquiv) followed by MulEquiv.prodUnits (units of a product = product of units). This is the
exact Mathlib idiom used in Mathlib.RingTheory.ZMod.UnitsCyclic.
Equations
Instances For
orderOf transport across the CRT split (S7a). The order of a unit of ZMod (m*n) is
the least common multiple of the orders of its two CRT components:
orderOf a = lcm (orderOf (unitsCRT h a).1) (orderOf (unitsCRT h a).2).
A MulEquiv preserves orderOf (MulEquiv.orderOf_eq), and orderOf of a pair is the lcm
of the component orders (Prod.orderOf). This is the lcm fact the S7d counting bound consumes.
The -1 split (S7a). The CRT units iso sends the success witness -1 to the per-factor
(-1, -1). The iso is induced from a ring isomorphism, which sends -1 ↦ -1; the units functor
and prodUnits preserve this. Proved by Units.ext/Prod.ext reduction to the underlying ring
values, where RingEquiv.map_neg_one (via map_neg, map_one) fires.
Cardinality factorisation (S7a). For coprime m, n (both nonzero), the number of units of
ZMod (m*n) is the product of the per-factor unit counts:
#(ZMod (m*n))ˣ = #(ZMod m)ˣ · #(ZMod n)ˣ.
Transport the cardinality across unitsCRT (Fintype.card_congr) and split the product
(Fintype.card_prod). (Equivalently ZMod.card_units_eq_totient + Nat.totient_mul.)
S7d-1 — the diagonal count (abstract) #
The per-factor distribution bound card_v2_orderOf_le (S7b) summed over a second finite group.
For a finite group G₁ and a finite cyclic group G₂ of even order, the "matched-v₂" diagonal
{(p₁, p₂) : v₂(orderOf p₁) = v₂(orderOf p₂)} of the product is no more than half:
2 · #{(p₁, p₂) : v₂(orderOf p₁) = v₂(orderOf p₂)} ≤ |G₁| · |G₂|.
This is the abstract counting step the S7d assembly iterates against the prime-power factorisation: only the second factor needs cyclicity / even order; the first is an arbitrary finite group the count sums over.
S7d-1 — the diagonal count (abstract). For a finite group G₁ and a finite cyclic group
G₂ of even order, the matched-2-adic-valuation diagonal of the product group is at most half:
2 · #{(p₁, p₂) : v₂(orderOf p₁) = v₂(orderOf p₂)} ≤ |G₁| · |G₂|.
Route: decompose the product-filter cardinality into a sum over the first coordinate
(Finset.card_filter + Fintype.sum_prod_type), recognise each fiber as S7b's filter at
k = v₂(orderOf a₁), apply card_v2_orderOf_le (G := G₂) per fiber, and sum
(Finset.mul_sum + Finset.sum_le_sum + Finset.sum_const). Only G₂ carries
IsCyclic / Even; G₁ is the summation index.
S7d-2a — the BAD characterisation (abstract two-factor core) #
For a product p = (p₁, p₂) of two finite cyclic groups, each carrying a distinguished order-2
element (z₁, z₂, playing the role of −1), Shor's per-pair success witness is r even and
p ^ (r/2) ≠ (z₁, z₂) (where r = orderOf p). The complementary BAD event — the failure of
that witness — is characterised purely arithmetically: it holds iff the two component orders share
the same 2-adic valuation.
This is the two-factor heart of S7d: combined with the CRT split (unitsCRT*, S7a) and the
diagonal count (two_mul_card_diag_le, S7d-1) it turns the success-probability bound into the
matched-v₂ diagonal count.
S7d-2a — the BAD characterisation (abstract). For a pair p = (p₁, p₂) of finite cyclic
groups with distinguished order-2 elements z₁, z₂, the Shor "BAD" event
¬ (Even (orderOf p) ∧ p ^ (orderOf p / 2) ≠ (z₁, z₂)) holds iff the two components share the
same 2-adic valuation of order:
¬ (Even r ∧ p ^ (r/2) ≠ (z₁, z₂)) ↔ v₂(orderOf p₁) = v₂(orderOf p₂), r := orderOf p.
Route: Prod.orderOf gives r = lcm (orderOf p₁) (orderOf p₂), so (Nat.factorization_lcm)
v₂ r = max (v₂ orderOf p₁) (v₂ orderOf p₂). Even r ↔ 1 ≤ v₂ r (even_iff_two_dvd +
Nat.Prime.dvd_iff_one_le_factorization). Splitting the product power componentwise
(Prod.pow_fst / Prod.pow_snd) and applying pow_half_eq_orderTwo_iff (S7c) per factor (with
the component-order divisibility orderOf pᵢ ∣ r from Nat.dvd_lcm_left/right) turns the
"p^(r/2) = (z₁,z₂)" condition into v₂ orderOf p₁ = v₂ r ∧ v₂ orderOf p₂ = v₂ r. A case split on
Even r plus omega (which handles Nat.max) collapses both disjuncts to v₂ p₁ = v₂ p₂.
S7d-2b-i — the abstract GOOD lower bound #
The complement of the S7d-2a BAD characterisation against the S7d-1 diagonal count. The Shor
per-pair GOOD event is Even (orderOf p) ∧ p ^ (orderOf p / 2) ≠ (z₁, z₂) (r even and the
half-power misses the joint (z₁, z₂) = (−1, −1) witness). GOOD is at least half:
|G₁| · |G₂| ≤ 2 · #GOOD.
S7d-2b-i — the abstract GOOD lower bound. For a pair of finite cyclic groups G₁, G₂
each with a distinguished order-2 element (z₁, z₂), the Shor "GOOD" event
Even (orderOf p) ∧ p ^ (orderOf p / 2) ≠ (z₁, z₂) covers at least half the product group:
|G₁| · |G₂| ≤ 2 · #{p : Even (orderOf p) ∧ p ^ (orderOf p / 2) ≠ (z₁, z₂)}.
Route (mechanical, no new math): bad_iff_v2_eq (S7d-2a) identifies the BAD filter (¬ GOOD) with
the matched-v₂ diagonal filter via Finset.filter_congr; card_filter_add_card_filter_not gives
#GOOD + #BAD = |G₁ × G₂| (Fintype.card_prod); two_mul_card_diag_le (S7d-1) gives
2 · #BAD ≤ |G₁|·|G₂|. omega on A + B = C, 2·B ≤ C ⟹ C ≤ 2·A. Even order of G₂ is
derived from hz₂ (orderOf_dvd_card).
S7d-2b-ii — the general coprime transport (S7★ closing piece) #
The abstract GOOD lower bound two_mul_card_good_ge (S7d-2b-i) is stated over a product of two
finite cyclic groups with distinguished order-2 elements. To land it on the actual units group
(ZMod N)ˣ of a composite N = m·n (coprime m, n), transport along the CRT units iso
unitsCRT (S7a): the Shor per-pair predicate Even (orderOf a) ∧ a^(orderOf a/2) ≠ -1 corresponds
across e := unitsCRT to the product predicate against (-1, -1), because e preserves orderOf
(unitsCRT_orderOf / MulEquiv.orderOf_eq) and sends -1 ↦ (-1, -1) (unitsCRT_neg_one). A
filter-card bijection (Finset.card_bij along e) plus the cardinality factorisation
card_units_mul then carries the bound onto (ZMod (m·n))ˣ.
S7d-2b-ii — the general coprime transport. For coprime m, n with cyclic unit groups
each having orderOf (-1) = 2, the Shor "GOOD" event covers at least half of (ZMod (m·n))ˣ:
|(ZMod (m·n))ˣ| ≤ 2 · #{a : Even (orderOf a) ∧ a ^ (orderOf a / 2) ≠ -1}.
Route: transport two_mul_card_good_ge (S7d-2b-i) across unitsCRT h : (ZMod (m·n))ˣ ≃* (ZMod m)ˣ × (ZMod n)ˣ (S7a). The Shor predicate corresponds across the iso (unitsCRT preserves
orderOf via MulEquiv.orderOf_eq and sends -1 ↦ (-1, -1) via unitsCRT_neg_one), giving a
filter-card bijection (Finset.card_bij); card_units_mul factors |(ZMod (m·n))ˣ|.
S7★ — the prime-power headline #
Instantiating the general coprime transport at m = p^α, n = q^β for distinct odd primes p, q
gives the Shor random-a success bound on the actual units group of a (two-prime-power) composite
modulus: a uniformly random unit is GOOD (yields a non-trivial factor via the order-finding step)
with probability at least 1/2.
The per-factor hypotheses of shor_good_transport are discharged from primality: coprimality via
Nat.Coprime.pow on Nat.coprime_primes; cyclicity via ZMod.isCyclic_units_of_prime_pow
(the odd-prime-power units group is cyclic); and orderOf (-1) = 2 via orderOf_neg_one
(= 2 since ringChar (ZMod (p^α)) = p^α ≠ 2 for p an odd prime, α ≥ 1).
S7★ — Shor random-a success, prime-power headline. For distinct odd primes p ≠ q and
exponents α, β ≥ 1, the Shor "GOOD" event covers at least half of (ZMod (p^α·q^β))ˣ:
|(ZMod (p^α·q^β))ˣ| ≤ 2 · #{a : Even (orderOf a) ∧ a ^ (orderOf a / 2) ≠ -1}.
A uniformly random unit a mod N = p^α·q^β has even multiplicative order and a^(r/2) ≢ -1
(so the order-finding step yields a non-trivial factor of N) with probability ≥ 1/2. Proof:
instantiate shor_good_transport (S7d-2b-ii) at m = p^α, n = q^β, discharging coprimality
(Nat.Coprime.pow), cyclicity (ZMod.isCyclic_units_of_prime_pow), and orderOf (-1) = 2
(orderOf_neg_one with ringChar = p^α ≠ 2).
The [Fact p.Prime] [Fact q.Prime] instance arguments are required only so the statement's
Fintype (ZMod (p^α·q^β))ˣ synthesises (via NeZero (p^α), derived from Fact p.Prime); they
carry no content beyond the explicit hp, hq.
S7★ — Shor random-a success, probability reading. The counting bound
shor_random_a_success restated as a probability: under uniform sampling of a unit
a mod N = p^α·q^β (distinct odd primes, α, β ≥ 1), the success probability
#GOOD / #units is at least 1/2:
1/2 ≤ #{a : Even (orderOf a) ∧ a^(orderOf a/2) ≠ -1} / |(ZMod N)ˣ|.
Pure ℚ-arithmetic corollary of shor_random_a_success (|units| ≤ 2·#GOOD): clear the
denominator (le_div_iff₀, with 0 < |units| from Fintype.card_pos — a units group is
nonempty via 1), push_cast, and linarith against the cast counting bound.
gen-C — the m-fold diagonal count (abstract) #
The general-m analogue of two_mul_card_diag_le (S7d-1). For a finite indexed family of finite
cyclic groups (G i) where the distinguished factor i₀ has even order, the "fully matched"
diagonal — tuples whose components ALL share the same 2-adic valuation of order — is at most half
the product group:
2 · #{f : ∀ i, v₂(orderOf (f i)) = v₂(orderOf (f i₀))} ≤ ∏ i, |G i|.
Only the distinguished factor i₀ needs even order; the remaining factors are summed over.
Route (product-of-sums): partition the diagonal by the common valuation k
(Finset.card_eq_sum_card_fiberwise along the key f ↦ v₂(orderOf (f i₀))); each fiber is a
Fintype.piFinset of per-component valuation classes, so its card is ∏ i, cₖ(i)
(Fintype.card_piFinset); factor out i₀ (Finset.mul_prod_erase) and bound 2·cₖ(i₀) ≤ |G i₀|
by card_v2_orderOf_le (S7b); the remaining erased sum ∑ₖ ∏_{i≠i₀} cₖ(i) is bounded by
∏_{i≠i₀} |G i| via a disjoint-biUnion count of the per-k piFinsets over the subtype
{i // i ≠ i₀} (disjoint because membership pins v₂(orderOf (g i)) = k for every i ≠ i₀,
so all the free components agree on k).
Spec correction (load-bearing hypothesis surfaced). The task statement omitted any free factor
besides i₀; as literally stated the theorem is FALSE when ι is a singleton {i₀}: there the
diagonal predicate ∀ i, v₂(orderOf (f i)) = v₂(orderOf (f i₀)) reduces to the tautology
v₂(orderOf (f i₀)) = v₂(orderOf (f i₀)), so the filter is all of univ and 2·|univ| ≤ |G i₀|
i.e. 2·N ≤ N fails for N > 0. The two-factor two_mul_card_diag_le is true precisely because
G₁ is an always-present free factor that the count sums over; the faithful m-fold analogue must
carry a free factor, here as (i₁ : ι) (hi₁ : i₁ ≠ i₀). This is not a weakening of the intended
content (the intended content is the genuinely-summed m-fold diagonal with m ≥ 2); it names the
hypothesis that was silently required.
gen-A — indexed-product plumbing for the general-m Shor bound #
Three reusable facts for the m-fold (ι-indexed) CRT framing, the indexed analogue of the
two-factor S7a primitives (unitsCRT*):
orderOf_pi: the order of a tuple in a finite product is thelcmof component orders (them-foldProd.orderOf);unitsPiCRT: the indexed units-CRT iso(ZMod (∏ N i))ˣ ≃* Π i, (ZMod (N i))ˣ, built from the ring CRT isoZMod.prodEquivPiby the units functor (Units.mapEquiv) and the units-of-a-product splitting (MulEquiv.piUnits) — them-fold analogue ofunitsCRT(S7a);unitsPiCRT_neg_one: that iso sends the success witness-1to the constant tuplefun _ => -1(them-foldunitsCRT_neg_one).
Cyclicity-agnostic: nothing here uses cyclicity of the factors (it enters only at the assembly,
where orderOf_pi feeds the lcm into the gen-C diagonal count two_mul_card_pi_diag_le).
orderOf in a finite indexed product = lcm of component orders (gen-A). The order of a
tuple f : Π i, G i in a finite product of finite monoids is the least common multiple of the
component orders. This is exactly Mathlib's Pi.orderOf; re-exported here under the
CSD.Empirical.QM.Shor namespace as the named m-fold analogue of Prod.orderOf (which drives
unitsCRT_orderOf, S7a).
The indexed units-CRT isomorphism (gen-A). For a finite family N : ι → ℕ that is
pairwise coprime, the units of ZMod (∏ i, N i) split as a product of the units of each factor:
(ZMod (∏ i, N i))ˣ ≃* Π i, (ZMod (N i))ˣ.
Built from the ring CRT iso ZMod.prodEquivPi by Units.mapEquiv (units functor on a MulEquiv)
followed by MulEquiv.piUnits (units of a product = product of units). This is the m-fold
analogue of the two-factor unitsCRT (S7a), mirroring its construction exactly. The coprimality
hypothesis is in ZMod.prodEquivPi's native spelling Pairwise (Function.onFun Nat.Coprime N).
Equations
- CSD.Empirical.QM.Shor.unitsPiCRT N hcop = (Units.mapEquiv (ZMod.prodEquivPi N hcop).toMulEquiv).trans MulEquiv.piUnits
Instances For
The -1 split (gen-A). The indexed units-CRT iso sends the success witness -1 to the
constant tuple fun _ => -1. The iso is induced from a ring isomorphism, which sends -1 ↦ -1;
the units functor and piUnits preserve this componentwise. Proved by funext/Units.ext
reduction to the underlying ring values at each i, where the piUnits component is defeq to the
underlying coercion of Units.mapEquiv (…) at i, and map_neg/map_one of the ring iso fire.
This is the m-fold analogue of unitsCRT_neg_one (S7a).
gen-B — the m-fold Pi characterisation + abstract GOOD bound #
The general-m analogues of the two-factor S7d-2a/S7d-2b-i pair (bad_iff_v2_eq /
two_mul_card_good_ge). For a finite indexed family of finite cyclic groups (G i) each carrying a
distinguished order-2 element z i (the per-factor −1), Shor's per-tuple success witness is
Even (orderOf f) ∧ f ^ (orderOf f / 2) ≠ z (where z = fun i => −1 after the gen-A
unitsPiCRT_neg_one transport). The complementary BAD event is characterised purely arithmetically
— it holds iff the components ALL share a common 2-adic valuation of order, equivalently each
equals that of the distinguished index i₀ — and the GOOD event then covers at least half the
product group.
Route. orderOf_pi (gen-A) gives r := orderOf f = univ.lcm (orderOf ∘ f); the sup-helper
v2_finset_lcm_eq_sup gives v₂ r = univ.sup (v₂ ∘ orderOf ∘ f) =: S. Even r ↔ 1 ≤ S
(even_iff_two_dvd + Nat.Prime.dvd_iff_one_le_factorization). The product power splits
componentwise (Pi.pow_apply + funext_iff); pow_half_eq_orderTwo_iff (S7c) per factor (with
orderOf (f i) ∣ r from Finset.dvd_lcm) turns f^(r/2) = z into ∀ i, v₂(orderOf (f i)) = S. A
case split on Even r collapses both readings to ∀ i, v₂(orderOf (f i)) = v₂(orderOf (f i₀)).
The GOOD bound is then the mechanical complement against two_mul_card_pi_diag_le (gen-C) via
Finset.filter_congr + card_filter_add_card_filter_not + omega.
v₂ of a Finset.lcm is the sup of the per-element v₂ (gen-B helper). For
g : ι → ℕ with all g i ≠ 0 on s, the 2-adic valuation of the finite lcm is the sup of the
per-element valuations. Finset.induction on the binary Nat.factorization_lcm (whose Finsupp ⊔
is max at the prime 2, Finsupp.sup_apply), with Finset.lcm_insert / Finset.sup_insert and
the GCDMonoid.lcm = Nat.lcm bridge lcm_eq_nat_lcm. The nonzero side-condition needed by
Nat.factorization_lcm is finset_lcm_ne_zero. Mathlib has no Finset-level factorization_lcm.
gen-B — the m-fold BAD characterisation (Pi form). For a finite indexed family of finite
cyclic groups (G i) with distinguished order-2 elements z i, the Shor "BAD" event
¬ (Even (orderOf f) ∧ f ^ (orderOf f / 2) ≠ z) holds iff every component's order shares the
2-adic valuation of the distinguished index i₀:
¬ (Even r ∧ f ^ (r/2) ≠ z) ↔ ∀ i, v₂(orderOf (f i)) = v₂(orderOf (f i₀)), r := orderOf f.
The m-fold analogue of bad_iff_v2_eq (S7d-2a). Route: orderOf_pi (gen-A) +
v2_finset_lcm_eq_sup give v₂ r = S := univ.sup (v₂ ∘ orderOf ∘ f); Even r ↔ 1 ≤ S; the Pi
power splits componentwise (Pi.pow_apply + funext_iff), and per factor S7c
(pow_half_eq_orderTwo_iff, fed orderOf (f i) ∣ r via Finset.dvd_lcm) gives
(f i)^(r/2) = z i ↔ v₂(orderOf (f i)) = S. A case split on Even r collapses both disjuncts to
∀ i, v₂(orderOf (f i)) = v₂(orderOf (f i₀)) (using Finset.sup_le / Finset.le_sup to identify
S with the common valuation, resp. force every valuation to 0 when ¬ Even r).
gen-B (cont.) — the abstract m-fold GOOD lower bound #
The complement of the gen-B BAD characterisation against the gen-C diagonal count
(two_mul_card_pi_diag_le). The Shor per-tuple GOOD event covers at least half the product group:
∏ i, |G i| ≤ 2 · #{f : Even (orderOf f) ∧ f ^ (orderOf f / 2) ≠ z}.
The m-fold analogue of two_mul_card_good_ge (S7d-2b-i). The free-factor hypothesis
i₁ ≠ i₀ is the load-bearing datum gen-C requires (see its docstring's spec correction): without a
second free index the diagonal bound 2·#diag ≤ ∏ is false for a singleton family.
gen-B — the abstract m-fold GOOD lower bound (Pi form). For a finite indexed family of
finite cyclic groups (G i) each with a distinguished order-2 element z i, and a free index
i₁ ≠ i₀, the Shor "GOOD" event covers at least half the product group:
∏ i, |G i| ≤ 2 · #{f : Even (orderOf f) ∧ f ^ (orderOf f / 2) ≠ z}.
Mechanical complement (no new math), mirroring two_mul_card_good_ge (S7d-2b-i): bad_iff_v2_eq_pi
(gen-B) identifies the BAD filter (¬ GOOD) with the fully-matched diagonal filter via
Finset.filter_congr; card_filter_add_card_filter_not gives #GOOD + #BAD = |Π i, G i|
(Fintype.card_pi); two_mul_card_pi_diag_le G i₀ h₀ i₁ hi (gen-C) gives 2·#BAD ≤ ∏ i, |G i|.
omega on A + B = C, 2·B ≤ C ⟹ C ≤ 2·A. The distinguished factor's even order h₀ is
derived from hz i₀ (orderOf_dvd_card).
gen-D — the m-fold coprime transport (indexed S7d-2b-ii) #
The general-m analogue of shor_good_transport (S7d-2b-ii). The abstract m-fold GOOD lower
bound two_mul_card_good_pi_ge (gen-B) is stated over an indexed product of finite cyclic groups
with distinguished order-2 elements. To land it on the actual units group (ZMod (∏ i, N i))ˣ of a
pairwise-coprime family N : ι → ℕ, transport along the indexed CRT units iso unitsPiCRT (gen-A):
the Shor per-tuple predicate Even (orderOf a) ∧ a^(orderOf a/2) ≠ -1 corresponds across
e := unitsPiCRT to the product predicate against the constant tuple fun i => -1, because e
preserves orderOf (MulEquiv.orderOf_eq) and sends -1 ↦ fun i => -1 (unitsPiCRT_neg_one,
gen-A). A filter-card bijection (Finset.card_bij along e) plus the cardinality factorisation
(Fintype.card_congr e.toEquiv + Fintype.card_pi) then carries the bound onto
(ZMod (∏ i, N i))ˣ. Exact Pi-form mirror of shor_good_transport.
The [NeZero (∏ i, N i)] binder is carried explicitly: it is derivable from [∀ i, NeZero (N i)]
(a product of nonzeros is nonzero, Finset.prod_ne_zero_iff + NeZero.ne), but Mathlib registers
no instance for it, so the body's Fintype (ZMod (∏ N))ˣ cannot synthesise from the per-factor
NeZeros alone. Unlike the two-factor card_units_mul / shor_good_transport (where
NeZero (m*n) is derived inside via Nat.mul_ne_zero), the indexed product needs the instance in
scope at the statement's Fintype, hence the binder. Callers discharge it with
haveI : NeZero (∏ i, N i) := ⟨Finset.prod_ne_zero_iff.mpr (fun i _ => NeZero.ne (N i))⟩.
gen-D — the m-fold coprime transport (indexed S7d-2b-ii). For a pairwise-coprime family
N : ι → ℕ of nonzero moduli with cyclic unit groups each having orderOf (-1) = 2, and a free
index i₁ ≠ i₀, the Shor "GOOD" event covers at least half of (ZMod (∏ i, N i))ˣ:
|(ZMod (∏ i, N i))ˣ| ≤ 2 · #{a : Even (orderOf a) ∧ a ^ (orderOf a / 2) ≠ -1}.
Route: transport two_mul_card_good_pi_ge (gen-B) across
unitsPiCRT N hcop : (ZMod (∏ i, N i))ˣ ≃* Π i, (ZMod (N i))ˣ (gen-A). The Shor predicate
corresponds across the iso (unitsPiCRT preserves orderOf via MulEquiv.orderOf_eq and sends
-1 ↦ fun i => -1 via unitsPiCRT_neg_one), giving a filter-card bijection (Finset.card_bij);
Fintype.card_congr e.toEquiv + Fintype.card_pi factor |(ZMod (∏ i, N i))ˣ|. Exact Pi-form
mirror of shor_good_transport (S7d-2b-ii).
gen-E — the general odd-composite headline (S7★-gen closing piece) #
Instantiating the m-fold coprime transport shor_random_a_success_pi (gen-D) at the prime-power
factorisation of an arbitrary odd composite N closes the Shor random-a success bound for any
odd N with at least two distinct prime factors. The indexing family is ↥N.primeFactors (the
Finset-as-subtype), with N' p = p ^ (N.factorization p). The two product facts are ready-made in
Mathlib (Nat.prod_primeFactors_coe_pow_factorization, Nat.pairwise_coprime_pow_primeFactors_factorization);
the gen-D side-conditions are discharged from primality exactly as in the two-prime-power headline
shor_random_a_success (each p ∈ N.primeFactors is an odd prime since p ∣ N and N is odd, so
its prime-power factor is cyclic with orderOf (-1) = 2). The free-index pair i₁ ≠ i₀ comes from
Finset.one_lt_card applied to 2 ≤ N.primeFactors.card.
gen-E — Shor random-a success, general odd-composite headline (S7★-gen). For an odd N
with at least two distinct prime factors, the Shor "GOOD" event covers at least half of (ZMod N)ˣ:
|(ZMod N)ˣ| ≤ 2 · #{a : Even (orderOf a) ∧ a ^ (orderOf a / 2) ≠ -1}.
A uniformly random unit a mod N has even multiplicative order and a^(r/2) ≢ -1 (so the
order-finding step yields a non-trivial factor of N) with probability ≥ 1/2. Proof: instantiate
shor_random_a_success_pi (gen-D) at ι := ↥N.primeFactors, N' p := p ^ (N.factorization p).
The product ∏ N' = N is Nat.prod_primeFactors_coe_pow_factorization; the pairwise coprimality is
Nat.pairwise_coprime_pow_primeFactors_factorization. Per-factor: each p ∈ N.primeFactors is an
odd prime (p ∣ N, N odd), so ZMod (p^α)ˣ is cyclic (ZMod.isCyclic_units_of_prime_pow) and
orderOf (-1) = 2 (orderOf_neg_one, ringChar = p^α ≠ 2). The free index pair i₁ ≠ i₀ comes
from Finset.one_lt_card.mp hN. The conclusion is transported from ∏ N' to N by prod_pow….
gen-E — Shor random-a success, general odd-composite probability reading. The counting
bound shor_random_a_success_general restated as a probability: under uniform sampling of a unit
a mod an odd N with at least two distinct prime factors, the success probability
#GOOD / #units is at least 1/2:
1/2 ≤ #{a : Even (orderOf a) ∧ a^(orderOf a/2) ≠ -1} / |(ZMod N)ˣ|.
Pure ℚ-arithmetic corollary of shor_random_a_success_general (|units| ≤ 2·#GOOD), mirroring
shor_success_prob_ge: clear the denominator (le_div_iff₀, with 0 < |units| from
Fintype.card_pos), cast, and linarith. N ≠ 0 (hence the Fintype (ZMod N)) is recovered from
the two-distinct-primes hypothesis.