Shor's algorithm — quantum core (M1 + M1.5: S1 + S2 + S3, ideal case r ∣ T)

Category: 3-Local (QM-validity).

Milestone M1 of specs/shor-plan.md: the quantum heart of Shor's order-finding algorithm, the part that needs no number-theory tail. Three pieces, all finite-dimensional QM:

• S1 — the multiply-by-a oracle. On the genuine work register EuclideanSpace ℂ (ZMod N), the modular-exponentiation oracle is the permutation |y⟩ ↦ |a·y⟩ induced by a unit a : (ZMod N)ˣ (mulOracle, mulOracle_basisState). A genuine permutation unitary, not a toy cyclic shift on Fin r.

• S2 — eigenstructure of multiply-by-a. With r = orderOf a and ω = exp(2πi/r), the states u_s = (1/√r) ∑_{j<r} conj(ω)^{s j} |a^j⟩ are eigenvectors with eigenvalue ω^s = e^{2πi s/r} (mulOracle_eigU), supported on the orbit {a^j}, and they reassemble |1⟩ = (1/√r) ∑_{s<r} u_s (sum_eigU). This is the hinge turning order-finding into phase estimation: the eigenphases are exactly the multiples of 1/r.

• S3 — phase-estimation exactness. On the counting register EuclideanSpace ℂ (Fin T), the inverse QFT inverts the QFT exactly (applyQFTinv_phaseColumn), so the phase state carrying eigenvalue ω_T^{j₀} is read out as |j₀⟩ with certainty (phase_estimation_exact). (Relocated 2026-08-29: S3's generic core and S4's 4/π² bound are Cat-1 — Mathlib/QuantumInfo/PhaseEstimation.lean — and this file consumes them; the register primitives were folded into the generalised Mathlib/QuantumInfo/Register.lean.)

• Bridge S2↔S3. In the ideal case r ∣ T, the eigenphase ω_r^s = ω_T^{s·(T/r)} (qftω_div), so the counting-register phase state carrying eigenvalue ω_r^s is exactly the QFT column s·(T/r). Inverse-QFT then reads the order's phase off a single eigenvalue branch with certainty: prob = 1 at index s·(T/r) (shor_order_readout, the M1 headline).

M1.5 — the joint two-register state and the full ideal-case output distribution

M1.5 assembles the genuine two-register joint state on EuclideanSpace ℂ (Fin T × ZMod N) and proves the full ideal-case (r ∣ T) order-finding measurement distribution:

• Joint register. tensorCN φ ψ (coordinate φ c * ψ y) and the counting-register inverse QFT qftInvCount (acting on the Fin T index only), with the key reduction qftInvCount_tensorCN : qftInvCount (tensorCN φ ψ) = tensorCN (applyQFTinv T φ) ψ. The genuine Born marginal on the counting register is probCount Φ c = ∑_y ‖Φ (c, y)‖².
• The faithful state. jointModexp a is the modular-exponentiation oracle |x⟩|y⟩ ↦ |x⟩|a^x·y⟩ (a genuine permutation), and jointModexp_initial proves it sends the prepared uniformCount ⊗ |1⟩ to postModexpState = (1/√T) ∑_x |x⟩|a^x⟩. So postModexpState IS the modexp output, not a posited form.
• Eigenbasis expansion. basisState_apow_eq (roots-of-unity inversion, dual to sum_eigU) rewrites |a^x⟩ in the eigU eigenbasis; postModexp_eq_eigenbasis then expands the joint state as (1/√r) ∑_s (phase column s·T/r) ⊗ u_s, and qftInvCount_postModexp applies the inverse QFT to read each branch as |s·T/r⟩ ⊗ u_s.
• HEADLINE shor_order_distribution: for r ∣ T, measuring the counting register gives probCount = 1/r on each s·(T/r) (s < r), via eigU_norm (‖u_s‖ = 1) and the index injectivity bridgeIndex_inj; shor_order_distribution_zero gives 0 off the r multiples. This is the uniform-1/r marginal M1 flagged as deferred.

Honest scope

M1 + M1.5 deliver the genuine oracle (S1), its eigenstructure with eigenvalues e^{2πi s/r} and the |1⟩ = (1/√r) ∑_s |u_s⟩ decomposition (S2), and the full ideal-case (r ∣ T) order-finding output distribution (S3): on the genuine two-register modexp state, the counting-register measurement is uniform 1/r on the r multiples {s·T/r : s < r} and 0 elsewhere. (Status corrected 2026-08-29 — this paragraph had listed S4–S7 as remaining, which predated their landing:) S4 (the 4/π² bound, now Cat-1 in PhaseEstimation.lean with the Shor corollary below), S5 (ShorRecovery.lean), S6 (ShorCapstone.lean) and S7b (ShorRandomA.lean) are landed. What remains for full Shor: the two-register r ∤ T measurement marginal (cross-term control across the r eigen-branches; see the S4 section note below). All per specs/shor-plan.md.

Register primitives

The computational-basis primitives basisState/prob and the coordinate bridge sum_coord are the general finite-index R1 API (Mathlib/QuantumInfo/Register.lean, generalised 2026-08-29 — this file previously carried a verbatim general-index copy mirroring the then bitstring-only R1). Shor's registers are the instances ι = ZMod N (work) and ι = Fin T (counting).

S1 — the multiply-by-a oracle on EuclideanSpace ℂ (ZMod N)

noncomputable def CSD.Empirical.QM.Shor.mulOracle {N : ℕ} (a : (ZMod N)ˣ) (ψ : EuclideanSpace ℂ (ZMod N)) : EuclideanSpace ℂ (ZMod N)

The multiply-by-a oracle |y⟩ ↦ |a·y⟩: the permutation operator reindexing a register state by multiplication by the unit a. The coordinate at y is pulled back from a⁻¹·y, so a basis state |y⟩ maps to |a·y⟩.

Equations

• CSD.Empirical.QM.Shor.mulOracle a ψ = (WithLp.equiv 2 (ZMod N → ℂ)).symm fun (y : ZMod N) => ψ.ofLp (↑a⁻¹ * y)

@[simp]

theorem CSD.Empirical.QM.Shor.mulOracle_apply {N : ℕ} (a : (ZMod N)ˣ) (ψ : EuclideanSpace ℂ (ZMod N)) (y : ZMod N) : (mulOracle a ψ).ofLp y = ψ.ofLp (↑a⁻¹ * y)

theorem CSD.Empirical.QM.Shor.mulOracle_smul {N : ℕ} (a : (ZMod N)ˣ) (c : ℂ) (ψ : EuclideanSpace ℂ (ZMod N)) : mulOracle a (c • ψ) = c • mulOracle a ψ

The oracle is linear in the state.

theorem CSD.Empirical.QM.Shor.mulOracle_sum {N : ℕ} {κ : Type u_1} (a : (ZMod N)ˣ) (s : Finset κ) (f : κ → EuclideanSpace ℂ (ZMod N)) : mulOracle a (∑ k ∈ s, f k) = ∑ k ∈ s, mulOracle a (f k)

The oracle commutes with finite sums.

@[simp]

theorem CSD.Empirical.QM.Shor.mulOracle_basisState {N : ℕ} (a : (ZMod N)ˣ) (y : ZMod N) : mulOracle a (QuantumInfo.basisState y) = QuantumInfo.basisState (↑a * y)

S1 key fact: the oracle sends the basis state |y⟩ to |a·y⟩.

S2 — eigenstructure of the multiply-by-a oracle

noncomputable def CSD.Empirical.QM.Shor.ord {N : ℕ} (a : (ZMod N)ˣ) : ℕ

The order r = orderOf a of the unit a in (ZMod N)ˣ.

Equations

• CSD.Empirical.QM.Shor.ord a = orderOf a

theorem CSD.Empirical.QM.Shor.ord_pos {N : ℕ} [NeZero N] (a : (ZMod N)ˣ) : 0 < ord a

noncomputable def CSD.Empirical.QM.Shor.omega {N : ℕ} (a : (ZMod N)ˣ) : ℂ

The primitive r-th root ω = exp(2πi/r), r = orderOf a.

Equations

• CSD.Empirical.QM.Shor.omega a = QuantumInfo.qftω (CSD.Empirical.QM.Shor.ord a)

noncomputable def CSD.Empirical.QM.Shor.orbit {N : ℕ} (a : (ZMod N)ˣ) (j : Fin (ord a)) : ZMod N

The orbit map j ↦ a^j (as an element of ZMod N) along the cyclic orbit of a.

Equations

• CSD.Empirical.QM.Shor.orbit a j = ↑(a ^ ↑j)

instance CSD.Empirical.QM.Shor.instNeZeroOrd {N : ℕ} [NeZero N] (a : (ZMod N)ˣ) : NeZero (ord a)

Fin (ord a) is nonempty as an additive group: ord a > 0.

theorem CSD.Empirical.QM.Shor.orbit_zero {N : ℕ} [NeZero N] (a : (ZMod N)ˣ) : orbit a ⟨0, ⋯⟩ = 1

noncomputable def CSD.Empirical.QM.Shor.cycShift {N : ℕ} [NeZero N] (a : (ZMod N)ˣ) : Fin (ord a) ≃ Fin (ord a)

The cyclic shift j ↦ j + 1 on Fin (ord a) as a self-equivalence.

Equations

• CSD.Empirical.QM.Shor.cycShift a = Equiv.addRight 1

theorem CSD.Empirical.QM.Shor.cycShift_apply {N : ℕ} [NeZero N] (a : (ZMod N)ˣ) (j : Fin (ord a)) : (cycShift a) j = j + 1

theorem CSD.Empirical.QM.Shor.cycShift_val {N : ℕ} [NeZero N] (a : (ZMod N)ˣ) (j : Fin (ord a)) : ↑((cycShift a) j) = (↑j + 1) % ord a

The shifted index value, modulo the order.

theorem CSD.Empirical.QM.Shor.pow_mul_mod_eq {z : ℂ} {r : ℕ} (hz : z ^ r = 1) (s m : ℕ) : z ^ (s * m) = z ^ (s * (m % r))

A root-of-unity reduction: with z^r = 1, the power z^{s·m} depends only on m mod r.

theorem CSD.Empirical.QM.Shor.units_pow_mod {N : ℕ} (a : (ZMod N)ˣ) (m : ℕ) : a ^ m = a ^ (m % ord a)

A unit-power reduction: with a^r = 1 (r = ord a), a^m = a^{m mod r}.

theorem CSD.Empirical.QM.Shor.mul_orbit {N : ℕ} [NeZero N] (a : (ZMod N)ˣ) (j : Fin (ord a)) : ↑a * orbit a j = orbit a ((cycShift a) j)

Multiplication by a shifts the orbit index by one (cyclically): a · (a^j) = a^{j+1 mod r}.

noncomputable def CSD.Empirical.QM.Shor.eigU {N : ℕ} (a : (ZMod N)ˣ) (s : Fin (ord a)) : EuclideanSpace ℂ (ZMod N)

The eigenvector u_s = (1/√r) ∑_{j<r} conj(ω)^{s j} |a^j⟩, supported on the orbit.

Equations

• One or more equations did not get rendered due to their size.

theorem CSD.Empirical.QM.Shor.mulOracle_eigU {N : ℕ} [NeZero N] (a : (ZMod N)ˣ) (s : Fin (ord a)) : mulOracle a (eigU a s) = omega a ^ ↑s • eigU a s

S2 eigenvector lemma: mulOracle a (u_s) = ω^s · u_s, with ω = exp(2πi/r). The oracle shifts the orbit index by one; reindexing by the cyclic shift and using conj ω = ω⁻¹, ω^r = 1, each summand picks up the common phase ω^s.

theorem CSD.Empirical.QM.Shor.sum_pow_orbit_phase {N : ℕ} [NeZero N] (a : (ZMod N)ˣ) (j : Fin (ord a)) : ∑ s : Fin (ord a), (starRingEnd ℂ) (omega a) ^ (↑s * ↑j) = if j = ⟨0, ⋯⟩ then ↑(ord a) else 0

A geometric-series collapse: for the primitive root ω and j < r, ∑_{s<r} conj(ω)^{s·j} = r if j = 0 and 0 otherwise. (Roots-of-unity orthogonality, the same collapse as in Fourier.qft_unitary.)

theorem CSD.Empirical.QM.Shor.sum_eigU {N : ℕ} [NeZero N] (a : (ZMod N)ˣ) : (↑√↑(ord a))⁻¹ • ∑ s : Fin (ord a), eigU a s = QuantumInfo.basisState 1

S2 decomposition lemma: (1/√r) ∑_{s<r} u_s = |1⟩. Summing the eigenvectors collapses the phase sum by roots-of-unity orthogonality to the single orbit term |a^0⟩ = |1⟩.

S3 — phase estimation on the counting register EuclideanSpace ℂ (Fin T)

The S3 core — applyQFT/applyQFTinv, phaseColumn, applyQFTinv_phaseColumn, phase_estimation_exact — is the generic phase-estimation API and lives in Mathlib/QuantumInfo/PhaseEstimation.lean (Cat-1; relocated 2026-08-29). This file keeps the Shor-specific bridge below.

Bridge S2 ↔ S3 — the eigenphase reads out the order

In the ideal case r ∣ T the eigenphase ω_r^s of mulOracle a is a T-th root: precisely ω_T^{s·(T/r)}. So the counting-register phase state carrying eigenvalue ω_r^s is the QFT column s·(T/r), and inverse-QFT reads the order's phase off it with certainty.

theorem CSD.Empirical.QM.Shor.qftω_div {r T : ℕ} (hr : 0 < r) (hT : 0 < T) (hdvd : r ∣ T) : QuantumInfo.qftω r = QuantumInfo.qftω T ^ (T / r)

ω_r = ω_T^{T/r} when r ∣ T (r, T > 0): both equal exp(2πi/r).

theorem CSD.Empirical.QM.Shor.bridgeIndex_lt {r T : ℕ} (hr : 0 < r) (hT : 0 < T) (hdvd : r ∣ T) (s : Fin r) : ↑s * (T / r) < T

The bridge index s·(T/r), valid < T when s < r, r ∣ T, and T > 0.

theorem CSD.Empirical.QM.Shor.eigenPhase_eq_phaseColumn (T : ℕ) {r : ℕ} (hr : 0 < r) (hT : 0 < T) (hdvd : r ∣ T) (s : Fin r) : (↑√↑T)⁻¹ • ∑ x : Fin T, QuantumInfo.qftω r ^ (↑s * ↑x) • QuantumInfo.basisState x = QuantumInfo.phaseColumn T ⟨↑s * (T / r), ⋯⟩

Bridge: the counting-register phase state carrying eigenvalue ω_r^s is exactly the QFT column s·(T/r).

theorem CSD.Empirical.QM.Shor.shor_order_readout (T : ℕ) [NeZero T] {r : ℕ} (hr : 0 < r) (hT : 0 < T) (hdvd : r ∣ T) (s : Fin r) : QuantumInfo.prob (QuantumInfo.applyQFTinv T ((↑√↑T)⁻¹ • ∑ x : Fin T, QuantumInfo.qftω r ^ (↑s * ↑x) • QuantumInfo.basisState x)) ⟨↑s * (T / r), ⋯⟩ = 1

M1 headline (shor_order_readout): in the ideal case r ∣ T, inverse-QFT of the counting-register phase state carrying eigenvalue ω_r^s yields the basis state s·(T/r) with certainty. This is phase estimation reading the order's phase s/r exactly.

M1.5 — the joint two-register state and the ideal-case output distribution

The product-index joint register EuclideanSpace ℂ (Fin T × ZMod N), the modular-exponentiation oracle |x⟩|y⟩ ↦ |x⟩|a^x·y⟩, and the full ideal-case (r ∣ T) measurement distribution.

The joint register EuclideanSpace ℂ (Fin T × ZMod N)

Rebuilt 2026-08-29 (plan specs/amplitude-amplification-plan.md, AA-5b step 1): the joint register machinery is now the Fin T × ZMod N instance of the generic Mathlib/QuantumInfo/JointRegister.lean (tensorState/matrixLeft/probLeft) — the local names and statements are unchanged, the proofs delegate. The r ∤ T marginal this file defers additionally gains the general orthogonal-branch mixture law probLeft_sum_tensor_orthogonal to consume when it is attempted.

noncomputable def CSD.Empirical.QM.Shor.tensorCN {N : ℕ} (T : ℕ) (φ : EuclideanSpace ℂ (Fin T)) (ψ : EuclideanSpace ℂ (ZMod N)) : EuclideanSpace ℂ (Fin T × ZMod N)

The tensor product of a counting-register state and a work-register state: the tensorState instance at ι₁ = Fin T, ι₂ = ZMod N.

Equations

• CSD.Empirical.QM.Shor.tensorCN T φ ψ = QuantumInfo.tensorState φ ψ

@[simp]

theorem CSD.Empirical.QM.Shor.tensorCN_apply {N : ℕ} [NeZero N] (T : ℕ) (φ : EuclideanSpace ℂ (Fin T)) (ψ : EuclideanSpace ℂ (ZMod N)) (c : Fin T) (y : ZMod N) : (tensorCN T φ ψ).ofLp (c, y) = φ.ofLp c * ψ.ofLp y

theorem CSD.Empirical.QM.Shor.tensorCN_smul_left {N : ℕ} (T : ℕ) (k : ℂ) (φ : EuclideanSpace ℂ (Fin T)) (ψ : EuclideanSpace ℂ (ZMod N)) : tensorCN T (k • φ) ψ = k • tensorCN T φ ψ

The tensor is linear in the counting factor (tensorState_smul_left).

theorem CSD.Empirical.QM.Shor.tensorCN_sum_left {N : ℕ} (T : ℕ) {κ : Type u_1} (s : Finset κ) (f : κ → EuclideanSpace ℂ (Fin T)) (ψ : EuclideanSpace ℂ (ZMod N)) : tensorCN T (∑ k ∈ s, f k) ψ = ∑ k ∈ s, tensorCN T (f k) ψ

The tensor commutes with finite sums in the counting factor (tensorState_sum_left).

theorem CSD.Empirical.QM.Shor.tensorCN_smul_right {N : ℕ} (T : ℕ) (k : ℂ) (φ : EuclideanSpace ℂ (Fin T)) (ψ : EuclideanSpace ℂ (ZMod N)) : tensorCN T φ (k • ψ) = k • tensorCN T φ ψ

The tensor is linear in the work factor (tensorState_smul_right).

theorem CSD.Empirical.QM.Shor.tensorCN_sum_right {N : ℕ} (T : ℕ) {κ : Type u_1} (φ : EuclideanSpace ℂ (Fin T)) (s : Finset κ) (f : κ → EuclideanSpace ℂ (ZMod N)) : tensorCN T φ (∑ k ∈ s, f k) = ∑ k ∈ s, tensorCN T φ (f k)

The tensor commutes with finite sums in the work factor (tensorState_sum_right).

@[simp]

theorem CSD.Empirical.QM.Shor.tensorCN_basis {N : ℕ} (T : ℕ) (c : Fin T) (y : ZMod N) : tensorCN T (QuantumInfo.basisState c) (QuantumInfo.basisState y) = QuantumInfo.basisState (c, y)

On basis states the tensor is the joint basis state: |c⟩ ⊗ |y⟩ = |(c, y)⟩ (tensorState_basis).

noncomputable def CSD.Empirical.QM.Shor.qftInvCount {N : ℕ} (T : ℕ) (Φ : EuclideanSpace ℂ (Fin T × ZMod N)) : EuclideanSpace ℂ (Fin T × ZMod N)

The inverse QFT on the counting register only: the matrixLeft (qftMatrix T)ᴴ instance, coordinate (qftInvCount Φ) (c, y) = ∑_x (qftMatrix T)ᴴ c x · Φ (x, y).

Equations

• CSD.Empirical.QM.Shor.qftInvCount T Φ = QuantumInfo.matrixLeft (QuantumInfo.qftMatrix T).conjTranspose Φ

@[simp]

theorem CSD.Empirical.QM.Shor.qftInvCount_apply {N : ℕ} [NeZero N] (T : ℕ) (Φ : EuclideanSpace ℂ (Fin T × ZMod N)) (c : Fin T) (y : ZMod N) : (qftInvCount T Φ).ofLp (c, y) = ∑ x : Fin T, (QuantumInfo.qftMatrix T).conjTranspose c x * Φ.ofLp (x, y)

theorem CSD.Empirical.QM.Shor.qftInvCount_smul {N : ℕ} (T : ℕ) (k : ℂ) (Φ : EuclideanSpace ℂ (Fin T × ZMod N)) : qftInvCount T (k • Φ) = k • qftInvCount T Φ

The partial inverse QFT is linear (matrixLeft_smul).

theorem CSD.Empirical.QM.Shor.qftInvCount_sum {N : ℕ} (T : ℕ) {κ : Type u_1} (s : Finset κ) (f : κ → EuclideanSpace ℂ (Fin T × ZMod N)) : qftInvCount T (∑ k ∈ s, f k) = ∑ k ∈ s, qftInvCount T (f k)

The partial inverse QFT commutes with finite sums (matrixLeft_sum).

theorem CSD.Empirical.QM.Shor.qftInvCount_tensorCN {N : ℕ} [NeZero N] (T : ℕ) [NeZero T] (φ : EuclideanSpace ℂ (Fin T)) (ψ : EuclideanSpace ℂ (ZMod N)) : qftInvCount T (tensorCN T φ ψ) = tensorCN T (QuantumInfo.applyQFTinv T φ) ψ

Key reduction: the partial inverse QFT commutes with the tensor and reduces to M1's applyQFTinv on the counting factor (matrixLeft_tensorState).

noncomputable def CSD.Empirical.QM.Shor.probCount {N : ℕ} [NeZero N] (T : ℕ) (Φ : EuclideanSpace ℂ (Fin T × ZMod N)) (c : Fin T) : ℝ

The Born marginal on the counting register: probCount Φ c = ∑_y ‖Φ (c, y)‖², the probLeft instance.

Equations

• CSD.Empirical.QM.Shor.probCount T Φ c = QuantumInfo.probLeft Φ c

The faithful modular-exponentiation state

noncomputable def CSD.Empirical.QM.Shor.jointModexp {N : ℕ} (T : ℕ) (a : (ZMod N)ˣ) (Φ : EuclideanSpace ℂ (Fin T × ZMod N)) : EuclideanSpace ℂ (Fin T × ZMod N)

The modular-exponentiation oracle |x⟩|y⟩ ↦ |x⟩|a^x·y⟩ on the joint register, the genuine permutation reindexing the work register by multiplication by a^x.

Equations

• CSD.Empirical.QM.Shor.jointModexp T a Φ = (WithLp.equiv 2 (Fin T × ZMod N → ℂ)).symm fun (p : Fin T × ZMod N) => Φ.ofLp (p.1, ↑(a ^ ↑p.1)⁻¹ * p.2)

@[simp]

theorem CSD.Empirical.QM.Shor.jointModexp_apply {N : ℕ} (T : ℕ) (a : (ZMod N)ˣ) (Φ : EuclideanSpace ℂ (Fin T × ZMod N)) (c : Fin T) (y : ZMod N) : (jointModexp T a Φ).ofLp (c, y) = Φ.ofLp (c, ↑(a ^ ↑c)⁻¹ * y)

@[simp]

theorem CSD.Empirical.QM.Shor.jointModexp_basis {N : ℕ} (T : ℕ) (a : (ZMod N)ˣ) (x : Fin T) (y : ZMod N) : jointModexp T a (QuantumInfo.basisState (x, y)) = QuantumInfo.basisState (x, ↑(a ^ ↑x) * y)

The oracle sends the joint basis state |x⟩|y⟩ to |x⟩|a^x·y⟩.

theorem CSD.Empirical.QM.Shor.jointModexp_smul {N : ℕ} [NeZero N] (T : ℕ) (a : (ZMod N)ˣ) (k : ℂ) (Φ : EuclideanSpace ℂ (Fin T × ZMod N)) : jointModexp T a (k • Φ) = k • jointModexp T a Φ

The oracle is linear in the state.

theorem CSD.Empirical.QM.Shor.jointModexp_sum {N : ℕ} (T : ℕ) {κ : Type u_1} (a : (ZMod N)ˣ) (s : Finset κ) (f : κ → EuclideanSpace ℂ (Fin T × ZMod N)) : jointModexp T a (∑ k ∈ s, f k) = ∑ k ∈ s, jointModexp T a (f k)

The oracle commutes with finite sums.

noncomputable def CSD.Empirical.QM.Shor.uniformCount (T : ℕ) : EuclideanSpace ℂ (Fin T)

The uniform counting register (1/√T) ∑_x |x⟩.

Equations

• CSD.Empirical.QM.Shor.uniformCount T = (↑√↑T)⁻¹ • ∑ x : Fin T, QuantumInfo.basisState x

noncomputable def CSD.Empirical.QM.Shor.initialState {N : ℕ} (T : ℕ) : EuclideanSpace ℂ (Fin T × ZMod N)

The prepared initial state uniformCount ⊗ |1⟩.

Equations

• CSD.Empirical.QM.Shor.initialState T = CSD.Empirical.QM.Shor.tensorCN T (CSD.Empirical.QM.Shor.uniformCount T) (QuantumInfo.basisState 1)

noncomputable def CSD.Empirical.QM.Shor.postModexpState {N : ℕ} (T : ℕ) (a : (ZMod N)ˣ) : EuclideanSpace ℂ (Fin T × ZMod N)

The post-modexp state (1/√T) ∑_x |x⟩|a^x⟩: the genuine output of the oracle on the prepared input.

Equations

• CSD.Empirical.QM.Shor.postModexpState T a = (↑√↑T)⁻¹ • ∑ x : Fin T, QuantumInfo.basisState (x, ↑(a ^ ↑x))

theorem CSD.Empirical.QM.Shor.jointModexp_initial {N : ℕ} [NeZero N] (T : ℕ) [NeZero T] (a : (ZMod N)ˣ) : jointModexp T a (initialState T) = postModexpState T a

Faithfulness link: the oracle on the prepared input uniformCount ⊗ |1⟩ produces exactly postModexpState = (1/√T) ∑_x |x⟩|a^x⟩.

Two eigenstructure facts

theorem CSD.Empirical.QM.Shor.orbit_injective {N : ℕ} (a : (ZMod N)ˣ) : Function.Injective (orbit a)

The orbit map j ↦ a^j is injective on Fin (ord a) (distinct powers below the order).

theorem CSD.Empirical.QM.Shor.eigU_norm {N : ℕ} [NeZero N] (a : (ZMod N)ˣ) (s : Fin (ord a)) : ‖eigU a s‖ = 1

‖u_s‖ = 1: the eigenvector is a unit vector. The orbit basis states are orthonormal (orbit_injective), each phase coefficient is unimodular, and ‖(√r)⁻¹‖² · r = 1.

The eigenbasis expansion of the post-modexp state

theorem CSD.Empirical.QM.Shor.basisState_apow_eq {N : ℕ} [NeZero N] (a : (ZMod N)ˣ) (x : ℕ) : QuantumInfo.basisState ↑(a ^ x) = (↑√↑(ord a))⁻¹ • ∑ s : Fin (ord a), omega a ^ (↑s * x) • eigU a s

Roots-of-unity inversion (dual to sum_eigU): for any x : ℕ, |a^x⟩ = (1/√r) ∑_s ω^{s·x} u_s. The inner phase sum ∑_s ω^{s(x-j)} collapses by orthogonality to the single orbit term a^{x mod r} = a^x.

theorem CSD.Empirical.QM.Shor.eigenPhase_eq_phaseColumn' (T : ℕ) [NeZero T] {r : ℕ} (hr : 0 < r) (hT : 0 < T) (hdvd : r ∣ T) (s : Fin r) : (↑√↑T)⁻¹ • ∑ x : Fin T, QuantumInfo.qftω r ^ (↑x * ↑s) • QuantumInfo.basisState x = QuantumInfo.phaseColumn T ⟨↑s * (T / r), ⋯⟩

The eigenphase counting state (1/√T) ∑_x ω_r^{s x} |x⟩ equals the QFT column s·(T/r), re-stated with the M1 omega a = qftω r notation.

theorem CSD.Empirical.QM.Shor.postModexp_eq_eigenbasis {N : ℕ} [NeZero N] (a : (ZMod N)ˣ) (T : ℕ) [NeZero T] (hr : 0 < ord a) (hT : 0 < T) (hdvd : ord a ∣ T) : postModexpState T a = (↑√↑(ord a))⁻¹ • ∑ s : Fin (ord a), tensorCN T (QuantumInfo.phaseColumn T ⟨↑s * (T / ord a), ⋯⟩) (eigU a s)

Eigenbasis expansion of the post-modexp state: in the ideal case r ∣ T, postModexpState = (1/√r) ∑_s (phase column s·T/r) ⊗ u_s.

Apply inverse-QFT and read the distribution

theorem CSD.Empirical.QM.Shor.qftInvCount_postModexp {N : ℕ} [NeZero N] (a : (ZMod N)ˣ) (T : ℕ) [NeZero T] (hr : 0 < ord a) (hT : 0 < T) (hdvd : ord a ∣ T) : qftInvCount T (postModexpState T a) = (↑√↑(ord a))⁻¹ • ∑ s : Fin (ord a), tensorCN T (QuantumInfo.basisState ⟨↑s * (T / ord a), ⋯⟩) (eigU a s)

Inverse-QFT of the post-modexp state: qftInvCount postModexpState = (1/√r) ∑_s |s·T/r⟩ ⊗ u_s. The partial inverse QFT reduces each phase column to a basis state.

theorem CSD.Empirical.QM.Shor.bridgeIndex_inj (T : ℕ) {r : ℕ} (hr : 0 < r) (hT : 0 < T) (hdvd : r ∣ T) : Function.Injective fun (s : Fin r) => ⟨↑s * (T / r), ⋯⟩

Index injectivity: s ↦ s·(T/r) is injective on Fin r when r ∣ T, r > 0.

theorem CSD.Empirical.QM.Shor.shor_order_distribution {N : ℕ} [NeZero N] (a : (ZMod N)ˣ) (T : ℕ) [NeZero T] (hr : 0 < ord a) (hT : 0 < T) (hdvd : ord a ∣ T) (s : Fin (ord a)) : probCount T (qftInvCount T (postModexpState T a)) ⟨↑s * (T / ord a), ⋯⟩ = (↑(ord a))⁻¹

HEADLINE — the ideal-case order-finding distribution. For r ∣ T, measuring the counting register of the inverse-QFT'd modexp state gives prob = 1/r on each multiple s·(T/r). This is the uniform-1/r spread over the order's multiples that order recovery uses.

theorem CSD.Empirical.QM.Shor.shor_order_distribution_zero {N : ℕ} [NeZero N] (a : (ZMod N)ˣ) (T : ℕ) [NeZero T] (hr : 0 < ord a) (hT : 0 < T) (hdvd : ord a ∣ T) (c : Fin T) (hc : ∀ (s : Fin (ord a)), ↑c ≠ ↑s * (T / ord a)) : probCount T (qftInvCount T (postModexpState T a)) c = 0

Complement: off the r multiples {s·(T/r)}, the counting-register probability is 0.

S4 — the Shor corollary of the 4/π² phase-estimation bound

The S4 analytic core — phaseStateR, the Dirichlet amplitude (applyQFTinv_phaseStateR_apply), the closed-form probability (prob_phaseStateR_eq) and the 4/π² lower bound (phase_estimation_lower_bound, Jordan inequality against |sin t| ≤ |t|) — is generic in T and lives in Mathlib/QuantumInfo/PhaseEstimation.lean (Cat-1; relocated 2026-08-29, no statement changed). What is Shor's is the instantiation φ = s/r below.

Honest scope (unchanged). S4 is the single-eigenvector lower bound on a fixed real phase φ (the general-r analogue of M1's eigenPhase_eq_phaseColumn, which only identified the counting state with an exact QFT column in the divisible case r ∣ T). The full two-register r ∤ T measurement marginal — controlling the cross-terms across the r eigen-branches u_s to get the per-outcome probability of the joint state — is beyond S4 and not done here.

theorem CSD.Empirical.QM.Shor.shor_phase_estimation_lower_bound (T : ℕ) [NeZero T] {r : ℕ} (hr : 0 < r) (s : Fin r) (c : Fin T) (hc : |↑↑s / ↑r - ↑↑c / ↑T| ≤ 1 / (2 * ↑T)) : 4 / Real.pi ^ 2 ≤ QuantumInfo.prob (QuantumInfo.applyQFTinv T (QuantumInfo.phaseStateR T (↑↑s / ↑r))) c

S4d — the Shor corollary. Instantiating φ = s/r, the s-branch counting state's inverse-QFT readout at the closest index c to s·T/r has probability ≥ 4/π². This is the general-r (r ∤ T) analogue of the M1 exact readout shor_order_readout: in the divisible case the phase state was an exact QFT column read with certainty; here the order phase s/r is generally not a multiple of 1/T, and the best one gets is the Dirichlet-kernel constant 4/π² at the nearest index. The two-register marginal across the r branches is beyond S4 (see the section docstring). The hr : 0 < r precondition is recorded for the spec reading (r = orderOf a > 0); it is already implied by s : Fin r, so the proof does not consume it.