Empirical/CSD: Grover's search as a flow on Σ

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

Empirical/QM/Algorithms/Grover.lean proves the search algorithm on the QM side: after k Grover steps from the uniform superposition the marked item w is measured with probability sin²((2k+1)θ) (grover_success). This file is the same algorithm on the CSD side. The Grover step is a unitary matrix on the n-qubit register (the oracle and the diffusion operator are reflections, 1 − 2|v⟩⟨v|), so it is a Circuit and hence a flow on the register's sector Σ = ℂℙ^{2ⁿ − 1} (CircuitFlow.lean); k runs are the flow iterated k times; and the readout is the record basin of the outcome w. The headline reads the algorithm's success probability off the basin's Born weight at the flowed ready point.

• reflectionMatrix v = 1 − 2|v⟩⟨v| — the reflection through a unit vector, with reflectionMatrix_conjTranspose_mul (unitary) and toEuclideanLin_reflectionMatrix (ψ ↦ ψ − 2⟪v, ψ⟫ v);
• oracleMatrix w, diffusionMatrix n, groverMatrix w — Grover's operators as matrices, with toEuclideanLin_groverMatrix : they act as groverStep w;
• groverCircuit w : Circuit (Fin n → Fin 2) — the search as a circuit, hence (groverCircuit w).flow is the search as a Σ-flow;
• groverReady — the uniform superposition as a point of the sector;
• ★★ grover_flow_born — Grover on Σ: at the point reached from the ready point by k runs of the flow, the record basin of the marked item has Born weight sin²((2k+1)θ); and ★ grover_flow_certain, certainty at the optimal count.

⚠️ Honest scope. The QM-side theorem carries the mathematics; this file adds the ontic reading (a flow on Σ, a basin as readout) and no new analysis of the algorithm. What the RegisterFlow.lean note says applies: the flow is the time-one map of the projective action, no Hamiltonian generating the step is modelled (R-015). The oracle is a reflection given as a matrix; no query model is claimed, as in the QM file.

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

Reflections as matrices

noncomputable def CSD.Empirical.CSDBridge.Algorithms.reflectionMatrix {ι : Type u_1} [DecidableEq ι] (v : EuclideanSpace ℂ ι) : Matrix ι ι ℂ

The reflection through a unit vector v, as a matrix: 1 − 2|v⟩⟨v|.

Equations

• CSD.Empirical.CSDBridge.Algorithms.reflectionMatrix v = 1 - 2 • CSD.LF2.outerProduct v

theorem CSD.Empirical.CSDBridge.Algorithms.reflectionMatrix_conjTranspose {ι : Type u_1} [Fintype ι] [DecidableEq ι] (v : EuclideanSpace ℂ ι) : (reflectionMatrix v).conjTranspose = reflectionMatrix v

A reflection is Hermitian.

theorem CSD.Empirical.CSDBridge.Algorithms.reflectionMatrix_mul_self {ι : Type u_1} [Fintype ι] [DecidableEq ι] (v : EuclideanSpace ℂ ι) (hv : ‖v‖ = 1) : reflectionMatrix v * reflectionMatrix v = 1

A reflection through a unit vector is an involution.

theorem CSD.Empirical.CSDBridge.Algorithms.reflectionMatrix_conjTranspose_mul {ι : Type u_1} [Fintype ι] [DecidableEq ι] (v : EuclideanSpace ℂ ι) (hv : ‖v‖ = 1) : (reflectionMatrix v).conjTranspose * reflectionMatrix v = 1

A reflection through a unit vector is unitary.

theorem CSD.Empirical.CSDBridge.Algorithms.toEuclideanLin_outerProduct {ι : Type u_1} [Fintype ι] [DecidableEq ι] (v ψ : EuclideanSpace ℂ ι) : (Matrix.toEuclideanLin (LF2.outerProduct v)) ψ = inner ℂ v ψ • v

|v⟩⟨v| acts as ψ ↦ ⟪v, ψ⟫ v.

theorem CSD.Empirical.CSDBridge.Algorithms.toEuclideanLin_reflectionMatrix {ι : Type u_1} [Fintype ι] [DecidableEq ι] (v ψ : EuclideanSpace ℂ ι) : (Matrix.toEuclideanLin (reflectionMatrix v)) ψ = ψ - (2 * inner ℂ v ψ) • v

A reflection acts as ψ ↦ ψ − 2⟪v, ψ⟫ v.

Grover's operators as matrices

noncomputable def CSD.Empirical.CSDBridge.Algorithms.oracleMatrix {n : ℕ} (w : Fin n → Fin 2) : Matrix (Fin n → Fin 2) (Fin n → Fin 2) ℂ

The oracle 1 − 2|w⟩⟨w|, the reflection through the marked basis state.

Equations

• CSD.Empirical.CSDBridge.Algorithms.oracleMatrix w = CSD.Empirical.CSDBridge.Algorithms.reflectionMatrix (QuantumInfo.basisState w)

noncomputable def CSD.Empirical.CSDBridge.Algorithms.diffusionMatrix (n : ℕ) : Matrix (Fin n → Fin 2) (Fin n → Fin 2) ℂ

The diffusion operator 2|s⟩⟨s| − 1, minus the reflection through the uniform superposition.

Equations

• CSD.Empirical.CSDBridge.Algorithms.diffusionMatrix n = -CSD.Empirical.CSDBridge.Algorithms.reflectionMatrix CSD.Empirical.QM.Grover.uniformState

noncomputable def CSD.Empirical.CSDBridge.Algorithms.groverMatrix {n : ℕ} (w : Fin n → Fin 2) : Matrix (Fin n → Fin 2) (Fin n → Fin 2) ℂ

One Grover step as a matrix: diffusion after the oracle.

Equations

• CSD.Empirical.CSDBridge.Algorithms.groverMatrix w = CSD.Empirical.CSDBridge.Algorithms.diffusionMatrix n * CSD.Empirical.CSDBridge.Algorithms.oracleMatrix w

theorem CSD.Empirical.CSDBridge.Algorithms.toEuclideanLin_oracleMatrix {n : ℕ} (w : Fin n → Fin 2) (ψ : QuantumInfo.QReg n) : (Matrix.toEuclideanLin (oracleMatrix w)) ψ = QM.Grover.oracle w ψ

theorem CSD.Empirical.CSDBridge.Algorithms.toEuclideanLin_diffusionMatrix {n : ℕ} (ψ : QuantumInfo.QReg n) : (Matrix.toEuclideanLin (diffusionMatrix n)) ψ = QM.Grover.diffusion ψ

theorem CSD.Empirical.CSDBridge.Algorithms.toEuclideanLin_groverMatrix {n : ℕ} (w : Fin n → Fin 2) : ⇑(Matrix.toEuclideanLin (groverMatrix w)) = QM.Grover.groverStep w

The Grover matrix acts as the Grover step.

theorem CSD.Empirical.CSDBridge.Algorithms.groverMatrix_conjTranspose_mul {n : ℕ} (w : Fin n → Fin 2) : (groverMatrix w).conjTranspose * groverMatrix w = 1

The Grover matrix is unitary.

The search as a circuit and as a flow

noncomputable def CSD.Empirical.CSDBridge.Algorithms.groverCircuit {n : ℕ} (w : Fin n → Fin 2) : Circuit (Fin n → Fin 2)

Grover's search as a circuit on the n-qubit register.

Equations

• CSD.Empirical.CSDBridge.Algorithms.groverCircuit w = { U := CSD.Empirical.CSDBridge.Algorithms.groverMatrix w, conjTranspose_mul := ⋯ }

theorem CSD.Empirical.CSDBridge.Algorithms.groverCircuit_U {n : ℕ} (w : Fin n → Fin 2) : (groverCircuit w).U = groverMatrix w

noncomputable def CSD.Empirical.CSDBridge.Algorithms.uniformReady (n : ℕ) : EuclideanSpace ℂ (Fin (Fintype.card (Fin n → Fin 2)))

The uniform superposition, enumerated.

Equations

• CSD.Empirical.CSDBridge.Algorithms.uniformReady n = (LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ (CSD.Empirical.CSDBridge.Algorithms.idx (Fin n → Fin 2))) CSD.Empirical.QM.Grover.uniformState

theorem CSD.Empirical.CSDBridge.Algorithms.uniformReady_norm {n : ℕ} : ‖uniformReady n‖ = 1

theorem CSD.Empirical.CSDBridge.Algorithms.uniformReady_ne_zero {n : ℕ} : uniformReady n ≠ 0

noncomputable def CSD.Empirical.CSDBridge.Algorithms.groverReady (n : ℕ) : RegisterSector (Fin n → Fin 2)

The ready point: the uniform superposition as a point of the register's sector.

Equations

• CSD.Empirical.CSDBridge.Algorithms.groverReady n = Projectivization.mk ℂ (CSD.Empirical.CSDBridge.Algorithms.uniformReady n) ⋯

theorem CSD.Empirical.CSDBridge.Algorithms.grover_flow_born {n : ℕ} (hn : 1 ≤ n) (w : Fin n → Fin 2) (k : ℕ) (θ : ℝ) (hsin : Real.sin θ = (√(2 ^ n))⁻¹) (hcos : Real.cos θ = √(2 ^ n - 1) / √(2 ^ n)) : (RecordLayer.epistemicMeasure ((groverCircuit w).flow^[k] (groverReady n))) (RecordLayer.globalBasin (RecordLayer.momentContext (Fintype.card (Fin n → Fin 2))) ((idx (Fin n → Fin 2)) w)) = ENNReal.ofReal (Real.sin ((2 * ↑k + 1) * θ) ^ 2)

★★ Grover on Σ. At the point reached from the ready point by k runs of the search flow, the record basin of the marked item w has Born weight sin²((2k+1)θ), sin θ = 1/√2ⁿ: the algorithm's success probability, read as the ontic typicality volume of the outcome's basin at the flowed point.

theorem CSD.Empirical.CSDBridge.Algorithms.grover_flow_certain {n : ℕ} (hn : 1 ≤ n) (w : Fin n → Fin 2) (k : ℕ) (θ : ℝ) (hsin : Real.sin θ = (√(2 ^ n))⁻¹) (hcos : Real.cos θ = √(2 ^ n - 1) / √(2 ^ n)) (hopt : (2 * ↑k + 1) * θ = Real.pi / 2) : (RecordLayer.epistemicMeasure ((groverCircuit w).flow^[k] (groverReady n))) (RecordLayer.globalBasin (RecordLayer.momentContext (Fintype.card (Fin n → Fin 2))) ((idx (Fin n → Fin 2)) w)) = 1

★ Certainty at the optimal count, on Σ: when (2k+1)θ = π/2 the marked item's basin has full weight at the flowed ready point.