Empirical/CSD: Shor's period finding as a flow on Σ

Category: 3-Local (CSD-side twin of Empirical/QM/Algorithms/ShorCore.lean).

ShorCore.lean proves the order-finding circuit on the QM side: on the joint register Fin T × ZMod N, the modular-exponentiation oracle followed by the inverse Fourier transform on the counting register sends the prepared state uniformCount ⊗ |1⟩ to a state whose counting register reads each multiple s·(T/r) of the order's phase with probability 1/r, and nothing else (shor_order_distribution, shor_order_distribution_zero, the ideal case r ∣ T). This file is the same circuit on the CSD side: the oracle is the permutation matrix of (c, y) ↦ (c, (a^c)⁻¹ y), the inverse Fourier transform is the Kronecker factor (qftMatrix T)ᴴ ⊗ 1, their product is a Circuit and hence a flow on the joint register's sector, and the readout of the counting register is the union of the record basins of the joint outcomes (c, y) over the work register.

• modexpPerm a, modexpMatrix a — the oracle as a permutation and its matrix, with toEuclideanLin_modexpMatrix (it acts as jointModexp) and permMatrix_conjTranspose_mul (a permutation matrix is unitary);
• qftInvJoint — the inverse Fourier transform on the counting register as a matrix on the joint register, with toEuclideanLin_qftInvJoint (it acts as qftInvCount) and qftInvJoint_conjTranspose_mul;
• shorCircuit a : Circuit (Fin T × ZMod N) — period finding as a circuit, hence (shorCircuit a).flow is period finding as a Σ-flow; shorReady, the prepared state as a point of the sector (initialState_norm);
• ★★ shor_flow_born_count — Shor on Σ: at the point reached from the ready point by the flow, the counting-register readout s·(T/r) — the union over the work register of the record basins of the joint outcomes — has Born weight 1/r; and ★ shor_flow_born_count_zero, the other counting outcomes have weight 0.

⚠️ Honest scope. The QM-side theorems carry the mathematics, in the ideal case r ∣ T; this file adds the ontic reading and no new analysis. The circuit is one unitary; no gate decomposition of the modular exponentiation and no Hamiltonian generating it is modelled (R-015). The classical post-processing (continued fractions, the random base) is ShorRecovery.lean / ShorCapstone.lean on the QM side and is not restated here.

References: Empirical/QM/Algorithms/ShorCore.lean; Empirical/CSD/Algorithms/CircuitFlow.lean; specs/BACKLOG.md #34; specs/future-work.md.

Permutation matrices are unitary

theorem CSD.Empirical.CSDBridge.Algorithms.permMatrix_conjTranspose {κ : Type u_1} [DecidableEq κ] (σ : Equiv.Perm κ) : (Equiv.Perm.permMatrix ℂ σ).conjTranspose = (Equiv.Perm.permMatrix ℂ σ).transpose

The conjugate transpose of a permutation matrix is its transpose (its entries are 0 and 1).

theorem CSD.Empirical.CSDBridge.Algorithms.permMatrix_transpose {κ : Type u_1} [DecidableEq κ] (σ : Equiv.Perm κ) : (Equiv.Perm.permMatrix ℂ σ).transpose = Equiv.Perm.permMatrix ℂ σ⁻¹

The transpose of a permutation matrix is the matrix of the inverse permutation.

theorem CSD.Empirical.CSDBridge.Algorithms.permMatrix_conjTranspose_mul {κ : Type u_1} [Fintype κ] [DecidableEq κ] (σ : Equiv.Perm κ) : (Equiv.Perm.permMatrix ℂ σ).conjTranspose * Equiv.Perm.permMatrix ℂ σ = 1

A permutation matrix is unitary.

The oracle and the inverse Fourier transform as matrices

noncomputable def CSD.Empirical.CSDBridge.Algorithms.modexpPerm {N : ℕ} (T : ℕ) (a : (ZMod N)ˣ) : Equiv.Perm (Fin T × ZMod N)

The permutation (c, y) ↦ (c, (a^c)⁻¹ · y) whose pullback is the modular-exponentiation oracle jointModexp.

Equations

• CSD.Empirical.CSDBridge.Algorithms.modexpPerm T a = (Equiv.refl (Fin T)).prodShear fun (c : Fin T) => (a ^ ↑c)⁻¹.mulLeft

theorem CSD.Empirical.CSDBridge.Algorithms.modexpPerm_apply {N : ℕ} (T : ℕ) (a : (ZMod N)ˣ) (p : Fin T × ZMod N) : (modexpPerm T a) p = (p.1, ↑(a ^ ↑p.1)⁻¹ * p.2)

noncomputable def CSD.Empirical.CSDBridge.Algorithms.modexpMatrix {N : ℕ} (T : ℕ) (a : (ZMod N)ˣ) : Matrix (Fin T × ZMod N) (Fin T × ZMod N) ℂ

The oracle as a matrix: the permutation matrix of modexpPerm.

Equations

• CSD.Empirical.CSDBridge.Algorithms.modexpMatrix T a = Equiv.Perm.permMatrix ℂ (CSD.Empirical.CSDBridge.Algorithms.modexpPerm T a)

theorem CSD.Empirical.CSDBridge.Algorithms.toEuclideanLin_modexpMatrix {N : ℕ} [NeZero N] (T : ℕ) (a : (ZMod N)ˣ) (Φ : EuclideanSpace ℂ (Fin T × ZMod N)) : (Matrix.toEuclideanLin (modexpMatrix T a)) Φ = QM.Shor.jointModexp T a Φ

The oracle matrix acts as jointModexp.

noncomputable def CSD.Empirical.CSDBridge.Algorithms.qftInvJoint {N : ℕ} (T : ℕ) : Matrix (Fin T × ZMod N) (Fin T × ZMod N) ℂ

The inverse Fourier transform on the counting register as a matrix on the joint register: (qftMatrix T)ᴴ ⊗ 1.

Equations

• CSD.Empirical.CSDBridge.Algorithms.qftInvJoint T = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (QuantumInfo.qftMatrix T).conjTranspose 1

theorem CSD.Empirical.CSDBridge.Algorithms.toEuclideanLin_qftInvJoint {N : ℕ} [NeZero N] (T : ℕ) (Φ : EuclideanSpace ℂ (Fin T × ZMod N)) : (Matrix.toEuclideanLin (qftInvJoint T)) Φ = QM.Shor.qftInvCount T Φ

The joint inverse-Fourier matrix acts as qftInvCount.

theorem CSD.Empirical.CSDBridge.Algorithms.qftInvJoint_conjTranspose_mul {N : ℕ} [NeZero N] (T : ℕ) [NeZero T] : (qftInvJoint T).conjTranspose * qftInvJoint T = 1

The joint inverse-Fourier matrix is unitary.

Period finding as a circuit and as a flow

noncomputable def CSD.Empirical.CSDBridge.Algorithms.shorMatrix {N : ℕ} [NeZero N] (T : ℕ) (a : (ZMod N)ˣ) : Matrix (Fin T × ZMod N) (Fin T × ZMod N) ℂ

Shor's period-finding circuit as a matrix: the oracle, then the inverse Fourier transform on the counting register.

Equations

• CSD.Empirical.CSDBridge.Algorithms.shorMatrix T a = CSD.Empirical.CSDBridge.Algorithms.qftInvJoint T * CSD.Empirical.CSDBridge.Algorithms.modexpMatrix T a

theorem CSD.Empirical.CSDBridge.Algorithms.toEuclideanLin_shorMatrix {N : ℕ} [NeZero N] (T : ℕ) (a : (ZMod N)ˣ) (Φ : EuclideanSpace ℂ (Fin T × ZMod N)) : (Matrix.toEuclideanLin (shorMatrix T a)) Φ = QM.Shor.qftInvCount T (QM.Shor.jointModexp T a Φ)

The circuit matrix acts as the circuit.

theorem CSD.Empirical.CSDBridge.Algorithms.shorMatrix_conjTranspose_mul {N : ℕ} [NeZero N] (T : ℕ) [NeZero T] (a : (ZMod N)ˣ) : (shorMatrix T a).conjTranspose * shorMatrix T a = 1

The circuit matrix is unitary.

noncomputable def CSD.Empirical.CSDBridge.Algorithms.shorCircuit {N : ℕ} [NeZero N] (T : ℕ) [NeZero T] (a : (ZMod N)ˣ) : Circuit (Fin T × ZMod N)

Period finding as a circuit on the joint register.

Equations

• CSD.Empirical.CSDBridge.Algorithms.shorCircuit T a = { U := CSD.Empirical.CSDBridge.Algorithms.shorMatrix T a, conjTranspose_mul := ⋯ }

theorem CSD.Empirical.CSDBridge.Algorithms.shorCircuit_U {N : ℕ} [NeZero N] (T : ℕ) [NeZero T] (a : (ZMod N)ˣ) : (shorCircuit T a).U = shorMatrix T a

theorem CSD.Empirical.CSDBridge.Algorithms.initialState_norm {N : ℕ} [NeZero N] (T : ℕ) [NeZero T] : ‖QM.Shor.initialState T‖ = 1

The prepared state uniformCount ⊗ |1⟩ is a unit vector.

theorem CSD.Empirical.CSDBridge.Algorithms.initialState_ne_zero {N : ℕ} [NeZero N] (T : ℕ) [NeZero T] : QM.Shor.initialState T ≠ 0

noncomputable def CSD.Empirical.CSDBridge.Algorithms.shorReadyVec {N : ℕ} [NeZero N] (T : ℕ) : EuclideanSpace ℂ (Fin (Fintype.card (Fin T × ZMod N)))

The prepared state, enumerated.

Equations

• CSD.Empirical.CSDBridge.Algorithms.shorReadyVec T = (LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ (CSD.Empirical.CSDBridge.Algorithms.idx (Fin T × ZMod N))) (CSD.Empirical.QM.Shor.initialState T)

theorem CSD.Empirical.CSDBridge.Algorithms.shorReadyVec_norm {N : ℕ} [NeZero N] (T : ℕ) [NeZero T] : ‖shorReadyVec T‖ = 1

theorem CSD.Empirical.CSDBridge.Algorithms.shorReadyVec_ne_zero {N : ℕ} [NeZero N] (T : ℕ) [NeZero T] : shorReadyVec T ≠ 0

noncomputable def CSD.Empirical.CSDBridge.Algorithms.shorReady {N : ℕ} [NeZero N] (T : ℕ) [NeZero T] : RegisterSector (Fin T × ZMod N)

The ready point: the prepared state uniformCount ⊗ |1⟩ as a point of the sector.

Equations

• CSD.Empirical.CSDBridge.Algorithms.shorReady T = Projectivization.mk ℂ (CSD.Empirical.CSDBridge.Algorithms.shorReadyVec T) ⋯

theorem CSD.Empirical.CSDBridge.Algorithms.shor_flow_born {N : ℕ} [NeZero N] (T : ℕ) [NeZero T] (a : (ZMod N)ˣ) (c : Fin T) (y : ZMod N) : (RecordLayer.epistemicMeasure ((shorCircuit T a).flow (shorReady T))) (RecordLayer.globalBasin (RecordLayer.momentContext (Fintype.card (Fin T × ZMod N))) ((idx (Fin T × ZMod N)) (c, y))) = ENNReal.ofReal (‖(QM.Shor.qftInvCount T (QM.Shor.postModexpState T a)).ofLp (c, y)‖ ^ 2)

The Born weight of the joint outcome (c, y)'s basin at the flowed ready point is the circuit's output amplitude squared.

theorem CSD.Empirical.CSDBridge.Algorithms.shor_flow_born_count {N : ℕ} [NeZero N] (T : ℕ) [NeZero T] (a : (ZMod N)ˣ) (hr : 0 < QM.Shor.ord a) (hT : 0 < T) (hdvd : QM.Shor.ord a ∣ T) (s : Fin (QM.Shor.ord a)) : ∑ y : ZMod N, (RecordLayer.epistemicMeasure ((shorCircuit T a).flow (shorReady T))) (RecordLayer.globalBasin (RecordLayer.momentContext (Fintype.card (Fin T × ZMod N))) ((idx (Fin T × ZMod N)) (⟨↑s * (T / QM.Shor.ord a), ⋯⟩, y))) = ENNReal.ofReal (↑(QM.Shor.ord a))⁻¹

★★ Shor on Σ. In the ideal case r ∣ T, at the point reached from the ready point by the flow, the counting-register outcome s·(T/r) — the union over the work register of the record basins of the joint outcomes (s·(T/r), y) — has Born weight 1/r.

theorem CSD.Empirical.CSDBridge.Algorithms.shor_flow_born_count_zero {N : ℕ} [NeZero N] (T : ℕ) [NeZero T] (a : (ZMod N)ˣ) (hr : 0 < QM.Shor.ord a) (hT : 0 < T) (hdvd : QM.Shor.ord a ∣ T) (c : Fin T) (hc : ∀ (s : Fin (QM.Shor.ord a)), ↑c ≠ ↑s * (T / QM.Shor.ord a)) : ∑ y : ZMod N, (RecordLayer.epistemicMeasure ((shorCircuit T a).flow (shorReady T))) (RecordLayer.globalBasin (RecordLayer.momentContext (Fintype.card (Fin T × ZMod N))) ((idx (Fin T × ZMod N)) (c, y))) = 0

★ The other counting outcomes have weight zero on Σ.