QPE 168 declarations in 15 modules
FormalRV.QPE.ControlledGates
FormalRV/QPE/ControlledGates.lean
FormalRV.SQIRPort.ControlledGates
Smallest-vertical-slice toward replacing the `control` stub in
`Framework/UnitaryOps.lean:972`.
Background:
- `BaseUnitary 1` has ONE constructor: `R θ φ λ` (general single-qubit
rotation). Gates like `X`, `H`, `T` are defined as specific R instances
(`U_X := R π 0 π`, `U_H := R (π/2) 0 π`, `U_T := R 0 0 (π/4)`, etc.).
- `BaseUnitary 2` has ONE constructor: `CNOT`.
- There is NO `BaseUnitary 3` constructor — `CCX` is a derived 16-gate
circuit (H, T, T†, CNOT). `UCom.app3` therefore has no real instances
in `BaseUCom` and the `control q (UCom.app3 _ _ _ _) = SKIP` clause is
vacuous.
- The actual blocker is `control q (UCom.app1 _ _) = SKIP`, which strips
every single-qubit gate from any controlled circuit. Because
`BaseUnitary 1` is entirely `R θ φ λ`, the correct replacement must
handle the full general rotation (no easy partial fix on `X` only at
the BaseUnitary level).
Modular-multiplier oracle gate-subset analysis:
- `f_modmult_circuit` in `SQIRPort/Shor.lean` is itself an `axiom`
(no concrete construction). The review chain uses an abstract
`u : Nat → BaseUCom (n + anc)` constrained by `ModMulImpl u`.
- A canonical RCIR implementation would use only `{X, CNOT, CCX}`,
where `CCX` decomposes to `{H, T, T†, CNOT}`. So even the "X-only"
intuition pulls in `H` and `T` via CCX.
- For `QPE_MMI_correct`'s proof, the oracle is universally quantified
over `BaseUCom`, so the fix must handle arbitrary `R θ φ λ`.
This file's deliverable (Step 4 of the user's plan): introduce
`controlled_X` as the simplest concrete case — it equals `CNOT` —
and prove its matrix-level correctness via the framework's existing
`pad_ctrl σx` definition. This is the BASE CASE for the future
full controlled-R port; it does not yet fix `control` globally.
The next theorems needed (sketched at the bottom of the file as
future work) are:
- `controlled_H_correct`: controlled-H = H-conjugated controlled-Z.
- `controlled_Rz_correct`: controlled-Rz(λ) via Rz(λ/2); CNOT; Rz(-λ/2); CNOT.
- `controlled_R_correct`: the full general-rotation decomposition.
Each adds a piece of the future `control` rewrite without touching
the global stub.
defcontrolled_X
noncomputable def controlled_X {dim : Nat} (q t : Nat) : BaseUCom dim*Controlled-X = CNOT** as a `BaseUCom` term.
This is the trivially-correct base case for any future fix of the
`control` stub: `control q (UCom.app1 U_X t)` should produce a
`BaseUCom` whose semantics equal `pad_ctrl dim q t σx`, and the
shortest such circuit is the framework's built-in `CNOT q t`.
The definition is intentionally `rfl`-equal to `CNOT q t` so that
downstream uses can be transparently swapped.
theoremuc_eval_controlled_X_eq_pad_ctrl
theorem uc_eval_controlled_X_eq_pad_ctrl {dim : Nat} (q t : Nat) :
uc_eval (controlled_X q t : BaseUCom dim) = pad_ctrl dim q t σx*`controlled_X`'s matrix semantics is `pad_ctrl dim q t σx`** —
the standard projector-decomposition form of a controlled-X gate.
This holds by `rfl` because `uc_eval (CNOT q t) = ueval_cnot dim q t
= pad_ctrl dim q t σx` (unfolding `uc_eval`'s app2 branch + the
definition of `ueval_cnot`).
This theorem is the **matrix-level** correctness claim for the
controlled-X gate; it is the form a future `control`-stub fix
would need to satisfy for the `app1 U_X` case.
theoremcontrolled_X_acts_on_basis
theorem controlled_X_acts_on_basis (n q t : Nat) (f : Nat → Bool)
(hq : q < n) (ht : t < n) (hqt : q ≠ t) :
uc_eval (controlled_X q t : BaseUCom n) * f_to_vec n f
= f_to_vec n (update f t (xor (f t) (f q)))*`controlled_X` acts on basis states as expected**: on input
`|f(0)...f(dim-1)⟩`, it produces the state with bit `t` XORed with
bit `q`, i.e., classical controlled-X.
Direct lift of the framework's `f_to_vec_CNOT_proved`. Together with
`uc_eval_controlled_X_eq_pad_ctrl`, this gives both the matrix-level
and operational (basis-state) characterizations of controlled-X.
defcontrolled_Rz
noncomputable def controlled_Rz {dim : Nat} (q t : Nat) (lam : ℝ) : BaseUCom dim*Controlled-Rz (controlled-phase) decomposition.** SQIRPort-namespaced
local copy; the `{dim}`-polymorphic version
`FormalRV.Framework.BaseUCom.controlled_Rz` was moved into the
framework 2026-05-26 to support `QFTinv`'s replacement. Both have
identical bodies; references inside this file go through the local
copy.
theoremcontrolled_Rz_acts_on_basis_correct
theorem controlled_Rz_acts_on_basis_correct
(dim q t : Nat) (hq : q < dim) (ht : t < dim) (hqt : q ≠ t)
(lam : ℝ) (f : Nat → Bool) :
uc_eval (controlled_Rz q t lam : BaseUCom dim) * f_to_vec dim f
= (if f q ∧ f t then Complex.exp ((lam : ℂ) * Complex.I) else 1)
• f_to_vec dim f*`controlled_Rz` basis-vector action correctness** (the
arbitrary-dimensional theorem, per the user's "best outcome" target).
For any `dim`, `q < dim`, `t < dim`, `q ≠ t`, real angle `λ`, and
Boolean function `f`, the 5-gate decomposition above acting on
`f_to_vec dim f` gives `(if f q ∧ f t then exp(iλ) else 1) • f_to_vec
dim f` — exactly the controlled-phase action.
Proof: walk the 5-gate sequence one factor at a time using
`f_to_vec_Rz_uc_eval` (single-qubit Rz on basis state) and
`f_to_vec_CNOT_proved` (CNOT on basis state). The intermediate
`update` after CNOT is reversed by the second CNOT (the double
application is the identity on Booleans), so the final state is
`f_to_vec f` again, scaled by the product of three scalars
`c1 · c2 · c3`. A by-cases analysis on `(f q, f t)` shows
`c1 · c2 · c3 = if f q ∧ f t then exp(iλ) else 1`.
Kernel-clean.
theoremmatrix_eq_of_f_to_vec_action
theorem matrix_eq_of_f_to_vec_action {dim : Nat}
(A B : Matrix (Fin (2^dim)) (Fin (2^dim)) ℂ)
(h : ∀ f : Nat → Bool, A * f_to_vec dim f = B * f_to_vec dim f) :
A = B*Matrix-equality lifting for `f_to_vec` action**: two square matrices
on `Fin (2^dim)` are equal iff they agree on every `f_to_vec dim f`
column.
Direct corollary of `Framework.matrix_eq_of_basis_action` plus the
`basis_vector ↔ f_to_vec` bridge `basis_vector_eq_f_to_vec_nat`.
theorempad_ctrl_Rz_acts_on_basis
theorem pad_ctrl_Rz_acts_on_basis
(dim q t : Nat) (hq : q < dim) (ht : t < dim)
(lam : ℝ) (f : Nat → Bool) :
pad_ctrl dim q t (rotation 0 0 lam) * f_to_vec dim f
= (if f q ∧ f t then Complex.exp ((lam : ℂ) * Complex.I) else 1)
• f_to_vec dim f*`pad_ctrl` basis-vector action for `rotation 0 0 λ`**: the
projector-decomposition form of controlled-phase matches the
controlled-Rz semantics on `f_to_vec` basis states.
pad_ctrl dim q t (rotation 0 0 λ) · f_to_vec dim f
= (if f q ∧ f t then exp(iλ) else 1) • f_to_vec dim f.
Proof: unfold `pad_ctrl = pad_u q proj0 + pad_u q proj1 · pad_u t M`,
distribute over `+` and `*`, apply
`pad_u_proj0_on_f_to_vec`, `pad_u_proj1_on_f_to_vec`,
`f_to_vec_Rz_proved`, and case-split on `(f q, f t)`.
theoremuc_eval_controlled_Rz_eq_pad_ctrl
theorem uc_eval_controlled_Rz_eq_pad_ctrl {dim : Nat}
(q t : Nat) (hq : q < dim) (ht : t < dim) (hqt : q ≠ t)
(lam : ℝ) :
uc_eval (controlled_Rz q t lam : BaseUCom dim)
= pad_ctrl dim q t (rotation 0 0 lam)*`controlled_Rz` matrix-equality correctness** (Phase 4.B's first
real building block):
uc_eval (controlled_Rz q t λ : BaseUCom dim)
= pad_ctrl dim q t (rotation 0 0 λ).
Closes the matrix-equality target by combining:
- `controlled_Rz_acts_on_basis_correct` (5-gate decomposition's action)
- `pad_ctrl_Rz_acts_on_basis` (projector form's action)
- `matrix_eq_of_f_to_vec_action` (matrix equality from basis-action).
Both sides agree pointwise on `f_to_vec`, hence are equal as matrices.
Kernel-clean.
theoremrotation_eq_exp_smul_ABXBXC
theorem rotation_eq_exp_smul_ABXBXC (θ φ lam : ℝ) :
rotation θ φ lam
= Complex.exp (((φ + lam) / 2 : ℂ) * Complex.I) •
(rotation (θ/2) φ 0 * σx * rotation (-θ/2) 0 (-(φ + lam)/2) * σx
* rotation 0 0 ((lam - φ)/2))*2×2 ABXBXC decomposition of `rotation θ φ λ`** — the pure single-
qubit matrix identity.
Proof: matrix extensionality on Fin 2 × Fin 2, then case-by-case
verification. Each of the 4 entries reduces to a product of complex
exponentials and trigonometric half-angle terms. Three helper
identities are used:
- `h_cos_half`: `cos(x/2) = cos²(x/4) - sin²(x/4)` (cos double-angle).
- `h_sin_half`: `sin(x/2) = 2 sin(x/4) cos(x/4)` (sin double-angle).
- Two complex-exp phase identities:
`exp((φ+λ)/2·I) · exp(-(λ+φ)/2·I) = 1` (cancellation)
`exp((φ+λ)/2·I) · exp((λ-φ)/2·I) = exp(λ·I)` (combination)
Plus `exp((φ+λ)·I) = exp(λ·I) · exp(φ·I)` for the (1,1) entry.
Kernel-clean. ~70 lines.
theoremproj0_mul_rotation_phase
private theorem proj0_mul_rotation_phase (α : ℝ) :
proj0 * rotation 0 0 α = proj0*Projector-phase identity** for proj0 (single-qubit 2x2).
theoremproj1_mul_rotation_phase
private theorem proj1_mul_rotation_phase (α : ℝ) :
proj1 * rotation 0 0 α = Complex.exp ((α : ℂ) * Complex.I) • proj1*Projector-phase identity** for proj1: produces a scalar `exp(iα)`.
theorempad_ctrl_mul_control_phase
theorem pad_ctrl_mul_control_phase {dim : Nat} (q t : Nat) (hqt : q ≠ t)
(α : ℝ) (M : Matrix (Fin 2) (Fin 2) ℂ) :
pad_ctrl dim q t M * pad_u dim q (rotation 0 0 α)
= pad_ctrl dim q t (Complex.exp ((α : ℂ) * Complex.I) • M)*Control-phase absorption** (Task 2 / L1 of the user's plan).
When the control-side phase `pad_u q (rotation 0 0 α) = P(α)_q` is
applied AFTER (right-multiplied by) a `pad_ctrl q t M`, it gets absorbed
as a scalar `exp(iα)` on the inner target matrix:
pad_ctrl dim q t M * pad_u dim q (rotation 0 0 α)
= pad_ctrl dim q t (exp(iα) • M).
Proof: expand `pad_ctrl = pad_u q proj0 + pad_u q proj1 · pad_u t M`,
distribute, commute the target-side `pad_u t M` past the control-side
phase via `pad_u_disjoint_comm'`, combine same-qubit projector·phase
products via `pad_u_mul_pad_u`, then apply the projector-phase identities
`proj0_mul_rotation_phase` (identity) and `proj1_mul_rotation_phase`
(scalar e^iα). Final scalar normalization via `pad_u_smul` +
`smul_mul_assoc` + `Matrix.mul_smul`.
Kernel-clean. ~12 lines after the helpers.
theorempad_branch_term
private theorem pad_branch_term (dim q t : Nat) (hqt : q ≠ t)
(Pa Pb A B : Matrix (Fin 2) (Fin 2) ℂ) :
pad_u dim q Pa * pad_u dim t A * (pad_u dim q Pb * pad_u dim t B)
= pad_u dim q (Pa * Pb) * pad_u dim t (A * B)*Per-branch term collapse.** A single `Pa_q * A_t * Pb_q * B_t`
product (with target factors `A`, `B` and control projectors `Pa`,
`Pb`) commutes the target through the control via `pad_u_disjoint_
comm'`, then combines same-qubit pad_u's via `pad_u_mul_pad_u`.
theorempad_ctrl_two_branch_collapse
private theorem pad_ctrl_two_branch_collapse (dim q t : Nat) (hqt : q ≠ t)
(A0 A1 B0 B1 : Matrix (Fin 2) (Fin 2) ℂ) :
(pad_u dim q proj0 * pad_u dim t A0 + pad_u dim q proj1 * pad_u dim t A1) *
(pad_u dim q proj0 * pad_u dim t B0 + pad_u dim q proj1 * pad_u dim t B1)
= pad_u dim q proj0 * pad_u dim t (A0 * B0)
+ pad_u dim q proj1 * pad_u dim t (A1 * B1)*Two-branch collapse.** Multiplying two control-projector-branch
sums collapses via projector orthogonality (`proj0 · proj1 = 0`)
and idempotence (`proj0 · proj0 = proj0`):
(P0·A0 + P1·A1) * (P0·B0 + P1·B1) = P0·(A0·B0) + P1·(A1·B1)
The cross terms vanish because the control projectors are orthogonal.
theorempad_ctrl_eq_branch_sum
private theorem pad_ctrl_eq_branch_sum (dim q t : Nat) (ht : t < dim)
(M : Matrix (Fin 2) (Fin 2) ℂ) :
pad_ctrl dim q t M
= pad_u dim q proj0 * pad_u dim t σi + pad_u dim q proj1 * pad_u dim t MRewrite `pad_ctrl` in standard branch-sum form. Uses `pad_u_id`
to fold the trivial proj0 branch's target into the explicit `σi_t`
form needed by `pad_ctrl_two_branch_collapse`.
theoremcnot_sandwich_collapse
private theorem cnot_sandwich_collapse (dim q t : Nat) (ht : t < dim) (hqt : q ≠ t)
(N : Matrix (Fin 2) (Fin 2) ℂ) :
pad_ctrl dim q t σx * pad_u dim t N * pad_ctrl dim q t σx
= pad_u dim q proj0 * pad_u dim t N
+ pad_u dim q proj1 * pad_u dim t (σx * N * σx)*CNOT sandwich collapse.** The composition `CNOT * pad_u t N * CNOT`
collapses to a single projector-branch sum:
pad_ctrl q t σx * pad_u t N * pad_ctrl q t σx
= pad_u q proj0 * pad_u t N + pad_u q proj1 * pad_u t (σx · N · σx).
This is the central lemma for the 5-gate circuit collapse. The
proj0 branch leaves `N` untouched; the proj1 branch conjugates `N`
by `σx`.
theoremabsorb_right_branch
private theorem absorb_right_branch (dim q t : Nat)
(A B X : Matrix (Fin 2) (Fin 2) ℂ) :
(pad_u dim q proj0 * pad_u dim t A + pad_u dim q proj1 * pad_u dim t B) *
pad_u dim t X
= pad_u dim q proj0 * pad_u dim t (A * X)
+ pad_u dim q proj1 * pad_u dim t (B * X)*Right-absorption helper.** A `pad_u t X` factor on the right of
a projector-branch sum gets absorbed into both branches' target
matrices.
theoremabsorb_left_branch
private theorem absorb_left_branch (dim q t : Nat) (hqt : q ≠ t)
(A B X : Matrix (Fin 2) (Fin 2) ℂ) :
pad_u dim t X *
(pad_u dim q proj0 * pad_u dim t A + pad_u dim q proj1 * pad_u dim t B)
= pad_u dim q proj0 * pad_u dim t (X * A)
+ pad_u dim q proj1 * pad_u dim t (X * B)*Left-absorption helper.** Symmetric to `absorb_right_branch` —
the `pad_u t X` factor must first commute through the control
projectors before absorbing into each target.
theorempad_ctrl_circuit_collapse
theorem pad_ctrl_circuit_collapse {dim : Nat}
(q t : Nat) (hq : q < dim) (ht : t < dim) (hqt : q ≠ t)
(M N K : Matrix (Fin 2) (Fin 2) ℂ) (h_abc : K * N * M = 1) :
pad_u dim t K * pad_ctrl dim q t σx * pad_u dim t N * pad_ctrl dim q t σx *
pad_u dim t M
= pad_ctrl dim q t (K * σx * N * σx * M)*5-gate circuit collapse.** Given `K · N · M = 1`, the 5-gate
sandwich `K_t · CNOT · N_t · CNOT · M_t` collapses to a single
`pad_ctrl` of the conjugated middle matrix:
pad_u t K · pad_ctrl q t σx · pad_u t N · pad_ctrl q t σx · pad_u t M
= pad_ctrl q t (K · σx · N · σx · M)
This is Task 3 / L2 of the user's plan. Proof flow: reassociate to
group the inner sandwich, apply `cnot_sandwich_collapse` for the
inner CNOT pair, then `absorb_left_branch` for the outer `K`,
`absorb_right_branch` for the outer `M`, then `h_abc` collapses the
proj0 branch to identity, leaving `pad_ctrl q t (K · σx · N · σx · M)`.
theoremrotation_ABC_eq_one
private theorem rotation_ABC_eq_one (θ φ lam : ℝ) :
rotation (θ/2) φ 0 * rotation (-θ/2) 0 (-(φ + lam)/2) * rotation 0 0 ((lam - φ)/2)
= 1*ABC = I identity** for the three rotation matrices `A`, `B`, `C`
appearing in the Nielsen-Chuang controlled-R decomposition.
Concretely: `rotation (θ/2) φ 0 · rotation (-θ/2) 0 (-(φ+λ)/2) ·
rotation 0 0 ((λ-φ)/2) = I`. The proof reduces to (0,0): `cos² +
sin² = 1`; (0,1) and (1,0): both 0; (1,1): a phase-cancellation
identity combined with Pythagoras. This is the algebraic hypothesis
fed to `pad_ctrl_circuit_collapse` in the main matrix-equality
theorem.
theoremuc_eval_controlled_R_eq_pad_ctrl
theorem uc_eval_controlled_R_eq_pad_ctrl {dim : Nat}
(q t : Nat) (hq : q < dim) (ht : t < dim) (hqt : q ≠ t) (θ φ lam : ℝ) :
uc_eval (controlled_R q t θ φ lam : BaseUCom dim)
= pad_ctrl dim q t (rotation θ φ lam)*MATRIX-EQUALITY THEOREM for `controlled_R`** (the L3 capstone
of the user's plan): the matrix semantics of the `controlled_R q t
θ φ λ` circuit equals the projector-decomposition form
`pad_ctrl dim q t (rotation θ φ λ)`.
Proof flow:
1. Unfold `uc_eval` of the 6-gate `controlled_R` circuit to a
matrix product `pad_u t A · CNOT · pad_u t B · CNOT · pad_u t C
· pad_u q P((φ+λ)/2)` (where `A`, `B`, `C` are the rotation
matrices in the decomposition).
2. Apply `pad_ctrl_circuit_collapse` to the first 5 factors, using
`rotation_ABC_eq_one` as the `K·N·M = 1` hypothesis. Result:
`pad_ctrl q t (A · σx · B · σx · C) · pad_u q P((φ+λ)/2)`.
3. Apply `pad_ctrl_mul_control_phase` to absorb the control-phase
into the inner matrix as `exp(i(φ+λ)/2) • (A · σx · B · σx · C)`.
4. Apply `rotation_eq_exp_smul_ABXBXC` (the 2×2 algebra) backwards
to identify this with `rotation θ φ λ`.
This is the structural theorem that, once `controlled_R` is wired
into the `control` stub (the global rewrite at
`Framework/UnitaryOps.lean:972`), justifies the `app1` branch's
matrix semantics — and hence unblocks `QPE_MMI_correct`.
theoremuc_eval_control_app1_R_eq_pad_ctrl
theorem uc_eval_control_app1_R_eq_pad_ctrl {dim : Nat}
(q t : Nat) (hq : q < dim) (ht : t < dim) (hqt : q ≠ t)
(θ φ lam : ℝ) :
uc_eval (control q (UCom.app1 (BaseUnitary.R θ φ lam) t : BaseUCom dim))
= pad_ctrl dim q t (rotation θ φ lam)*Framework-level wrapper**: the global `control` definition's
matrix semantics on the `app1 (R θ φ λ) t` case equals the projector
form `pad_ctrl dim q t (rotation θ φ λ)`.
This is the user-facing surface of the `control`-stub fix: any place
that uses `control q U` for a single-qubit `U = R θ φ λ` now has a
clean matrix semantics, not the previous `SKIP = 1` stub. Reduces by
definition to `controlled_R`, then chains to
`uc_eval_controlled_R_eq_pad_ctrl`.
theoremuc_eval_CCX_eq_controlled_CNOT
theorem uc_eval_CCX_eq_controlled_CNOT {dim : Nat} (q m n : Nat)
(hq : q < dim) (hm : m < dim) (hn : n < dim)
(hqm : q ≠ m) (hqn : q ≠ n) (hmn : m ≠ n) :
uc_eval (BaseUCom.CCX q m n : BaseUCom dim)
= pad_u dim q proj0
+ pad_u dim q proj1 * uc_eval (BaseUCom.CNOT m n : BaseUCom dim)*CCX as a projector-decomposed controlled-CNOT** (matrix equality).
For pairwise-distinct in-range `q, m, n`,
`uc_eval (CCX q m n) = pad_u q proj0 + pad_u q proj1 · uc_eval (CNOT m n)`.
Proof: by `matrix_eq_of_f_to_vec_action`, suffices to check the basis-
vector action. `f_to_vec_CCX_proved` rewrites the LHS to
`f_to_vec dim (update f n (xor (f n) (f q && f m)))`; the RHS unfolds
via `f_to_vec_CNOT_proved` and the projector-on-f_to_vec lemmas. The
final case split on `f q` matches the two branches.
theoremuc_eval_control_app2_CNOT_eq_proj_decomp
theorem uc_eval_control_app2_CNOT_eq_proj_decomp {dim : Nat} (q m n : Nat)
(hq : q < dim) (hm : m < dim) (hn : n < dim)
(hqm : q ≠ m) (hqn : q ≠ n) (hmn : m ≠ n) :
uc_eval (control q (UCom.app2 BaseUnitary.CNOT m n : BaseUCom dim))
= pad_u dim q proj0
+ pad_u dim q proj1 *
uc_eval (UCom.app2 BaseUnitary.CNOT m n : BaseUCom dim)*Framework-level wrapper** for the `app2 CNOT` case: the new
`control` definition routes `app2 BaseUnitary.CNOT m n` to `CCX q m n`,
so the matrix semantics of `control q (app2 CNOT m n)` equals the
projector decomposition.
theorempad_u_comm_uc_eval_of_fresh
theorem pad_u_comm_uc_eval_of_fresh {dim : Nat} (q : Nat) :
∀ (c : BaseUCom dim), is_fresh q c →
∀ (U : Matrix (Fin 2) (Fin 2) ℂ),
pad_u dim q U * uc_eval c = uc_eval c * pad_u dim q U*Freshness commutation.** If `q` is fresh in `c`, then `pad_u dim q U`
commutes with `uc_eval c` for any single-qubit matrix `U`.
Proof by induction on `c`:
- `seq`: commute through both halves via IH;
- `app1 (R θ φ λ) n`: `uc_eval = pad_u n (rotation θ φ λ)`, commutes
by `pad_u_disjoint_comm'` using `q ≠ n`;
- `app2 CNOT m n`: `uc_eval = pad_ctrl m n σx`, commutes by
`pad_u_pad_ctrl_disjoint_comm` using `q ≠ m ∧ q ≠ n`;
- `app3`: vacuous since `BaseUnitary 3` is empty.
theorempadq_proj0_mul_proj0
private theorem padq_proj0_mul_proj0 (dim q : Nat) :
pad_u dim q proj0 * pad_u dim q proj0 = pad_u dim q proj0theorempadq_proj1_mul_proj1
private theorem padq_proj1_mul_proj1 (dim q : Nat) :
pad_u dim q proj1 * pad_u dim q proj1 = pad_u dim q proj1theorempadq_proj0_mul_proj1
private theorem padq_proj0_mul_proj1 (dim q : Nat) :
pad_u dim q proj0 * pad_u dim q proj1 = 0theorempadq_proj1_mul_proj0
private theorem padq_proj1_mul_proj0 (dim q : Nat) :
pad_u dim q proj1 * pad_u dim q proj0 = 0theoremuc_eval_control_eq_proj_decomp
theorem uc_eval_control_eq_proj_decomp {dim : Nat} (q : Nat) (c : BaseUCom dim)
(hq : q < dim) (h_fresh : is_fresh q c) (h_wt : UCom.WellTyped dim c) :
uc_eval (control q c)
= pad_u dim q proj0 + pad_u dim q proj1 * uc_eval c*GENERAL CONTROLLED-CIRCUIT SEMANTIC THEOREM**.
For any well-typed `BaseUCom dim` `c` and any fresh control qubit `q`,
the matrix semantics of the controlled circuit `control q c` is the
standard projector decomposition
uc_eval (control q c) = P0_q + P1_q · uc_eval c.
Proof by induction on `c`:
- **`seq c₁ c₂`**: by IH on both halves, then projector algebra. After
`Matrix.add_mul` / `Matrix.mul_add`, the four cross-terms simplify
via `P0·P0 = P0`, `P0·P1 = P1·P0 = 0`, `P1·P1 = P1`, plus
`pad_u_comm_uc_eval_of_fresh` to commute `U₂` past `P0` / `P1`.
- **`app1 (R θ φ λ) n`**: directly `uc_eval_control_app1_R_eq_pad_ctrl`
+ unfolding `pad_ctrl`.
- **`app2 CNOT m n`**: directly `uc_eval_control_app2_CNOT_eq_proj_decomp`.
- **`app3`**: vacuous since `BaseUnitary 3` is empty.
This is the user-facing surface of the `control`-stub fix: any place
that uses `control q U` for an arbitrary well-typed circuit `U`
(modular-multiplier oracle, QFT, etc.) now has clean controlled-U
matrix semantics. Downstream, this directly enables phase-kickback
chaining for `controlled_powers` and the `QPE_var_on_eigenstate` step
of `QPE_MMI_correct`.
theoremuc_eval_control_on_projector_decomp
theorem uc_eval_control_on_projector_decomp {dim : Nat}
(q : Nat) (c : BaseUCom dim) (hq : q < dim)
(h_fresh : is_fresh q c) (h_wt : UCom.WellTyped dim c)
(ψ : Matrix (Fin (2^dim)) (Fin 1) ℂ)
(ζ : ℂ) (h_eig : uc_eval c * ψ = ζ • ψ) :
uc_eval (control q c) * ψ
= pad_u dim q proj0 * ψ + ζ • (pad_u dim q proj1 * ψ)*Single-control phase kickback (projector form).**
Given a well-typed circuit `c` with control qubit `q` fresh in `c`, and
a state `ψ` that is an eigenstate of `c` with eigenvalue `ζ`, the
matrix action of `control q c` on `ψ` is the projector decomposition
`uc_eval (control q c) * ψ = (P0_q · ψ) + ζ · (P1_q · ψ)`
where `Pi_q = pad_u dim q proj_i` (i = 0, 1).
Proof: rewrite `uc_eval (control q c)` via `uc_eval_control_eq_proj_decomp`,
distribute via `Matrix.add_mul`, then substitute `h_eig` and pull the
scalar out via `Matrix.mul_smul`. ~3 lines.
theoremuc_eval_controlled_powers_succ_step
theorem uc_eval_controlled_powers_succ_step {dim n : Nat}
(f : Nat → BaseUCom dim) (hn : n < dim)
(h_fresh : is_fresh n (f n))
(h_wt : UCom.WellTyped dim (f n))
(ψ φ : Matrix (Fin (2^dim)) (Fin 1) ℂ)
(h_prior : uc_eval (controlled_powers f n) * ψ = φ)
(ζ : ℂ) (h_eig : uc_eval (f n) * φ = ζ • φ) :
uc_eval (controlled_powers f (n + 1)) * ψ
= pad_u dim n proj0 * φ + ζ • (pad_u dim n proj1 * φ)*Single-step cascade for `controlled_powers`.**
If after applying `controlled_powers f n` to `ψ` we obtain a state `φ`
that is an eigenstate of `f n` with eigenvalue `ζ`, then the next
iteration `controlled_powers f (n+1)` gives the projector-decomposition
form of phase-kickback on `φ`. This abstracts the cascade step so
callers can supply the intermediate `φ` and its eigen-relation directly
(useful when `φ ≠ ψ` because earlier controls have already updated the
control register, yet `φ` happens to still be an eigenstate of `f n`).
Proof: unfold `controlled_powers (n+1) = seq (controlled_powers n) (control n (f n))`,
substitute `h_prior` for the intermediate state, then apply
`uc_eval_control_on_projector_decomp`. ~5 lines.
defphase_projector
noncomputable def phase_projector {dim : Nat}
(i : Nat) (ζ : ℂ) : Matrix (Fin (2^dim)) (Fin (2^dim)) ℂ*Per-qubit phase projector.** The matrix
`P0_i + ζ_i · P1_i` that the i-th controlled `f i` produces on an
eigenstate: identity on the control-0 branch, scaled by `ζ_i` on the
control-1 branch.
theoremphase_projector_apply
theorem phase_projector_apply {dim : Nat} (i : Nat) (ζ : ℂ)
(ψ : Matrix (Fin (2^dim)) (Fin 1) ℂ) :
@phase_projector dim i ζ * ψ
= pad_u dim i proj0 * ψ + ζ • (pad_u dim i proj1 * ψ)Action of `phase_projector` on a state vector.
defphase_projector_product
noncomputable def phase_projector_product {dim : Nat}
(ζ : Nat → ℂ) : Nat → Matrix (Fin (2^dim)) (Fin (2^dim)) ℂ
| 0 => 1
| n + 1 => phase_projector n (ζ n) * phase_projector_product ζ n*Recursive phase-projector product**, ordered to match
`uc_eval (controlled_powers f m)`: the latest projector is on the
LEFT (because `uc_eval (UCom.seq c₁ c₂) = uc_eval c₂ * uc_eval c₁`
and `controlled_powers f (n+1) = seq (controlled_powers f n) (control n (f n))`).
theoremphase_projector_commutes_uc_eval
theorem phase_projector_commutes_uc_eval {dim : Nat}
(i : Nat) (ζ : ℂ) (M : Matrix (Fin (2^dim)) (Fin (2^dim)) ℂ)
(h_comm0 : pad_u dim i proj0 * M = M * pad_u dim i proj0)
(h_comm1 : pad_u dim i proj1 * M = M * pad_u dim i proj1) :
@phase_projector dim i ζ * M = M * @phase_projector dim i ζA single `phase_projector` commutes with any matrix `M` that commutes
separately with both projectors `pad_u dim i proj0` and `pad_u dim i proj1`.
theoremphase_projector_product_commutes
theorem phase_projector_product_commutes {dim : Nat}
(ζ : Nat → ℂ) (M : Matrix (Fin (2^dim)) (Fin (2^dim)) ℂ) :
∀ n,
(∀ i, i < n → ∀ b : Matrix (Fin 2) (Fin 2) ℂ,
pad_u dim i b * M = M * pad_u dim i b) →
@phase_projector_product dim ζ n * M = M * @phase_projector_product dim ζ n`phase_projector_product ζ n` commutes with `M` whenever each of the
underlying single-qubit projector lifts `pad_u dim i b` (for `i < n`,
`b` either `proj0` or `proj1`, or any 2x2) commutes with `M`.
theoremuc_eval_controlled_powers_on_common_eigenstate_recursive
theorem uc_eval_controlled_powers_on_common_eigenstate_recursive
{dim : Nat} (hd : 0 < dim) (f : Nat → BaseUCom dim)
(ψ : Matrix (Fin (2^dim)) (Fin 1) ℂ) (ζ : Nat → ℂ) :
∀ m, (∀ i, i < m → i < dim) →
(∀ i, i < m → is_fresh i (f i)) →
(∀ i, i < m → UCom.WellTyped dim (f i)) →
(∀ i j, i < m → j < m →
∀ U : Matrix (Fin 2) (Fin 2) ℂ,
pad_u dim i U * uc_eval (f j) = uc_eval (f j) * pad_u dim i U) →
(∀ i, i < m → uc_eval (f i) * ψ = ζ i • ψ) →
uc_eval (controlled_powers f m) * ψ
= @phase_projector_product dim ζ m * ψ*Full controlled-powers cascade on a common eigenstate.**
Given a state `ψ` that is a common eigenstate of each `f i` (for `i < m`)
with eigenvalue `ζ i`, and given the data-only commutation hypothesis
(each `pad_u dim i U` commutes with `uc_eval (f j)` for `i, j < m` — in
QPE this is automatic because the controls live on positions `< m` and
the `f j`s are shift-lifted to positions `≥ m`), the controlled-powers
cascade applied to `ψ` produces the phase-kickback state
uc_eval (controlled_powers f m) * ψ = phase_projector_product ζ m * ψ.
Proof: induction on `m`. Base case `m = 0` uses
`uc_eval_controlled_powers_zero_eq_one`. The successor step uses
`uc_eval_controlled_powers_succ_step` with the intermediate state
`φ := phase_projector_product ζ k * ψ`; the eigen-relation on `φ`
follows from `phase_projector_product_commutes` plus the data-only
commutation hypothesis.
FormalRV.QPE.PhaseKickback
FormalRV/QPE/PhaseKickback.lean
FormalRV.SQIRPort.PhaseKickback
Block-disjoint commutation + QPE-specific phase-kickback cascade.
QPE's `QPE_var m anc f` lifts each `f i : BaseUCom anc` to
`BaseUCom (m + anc)` via `map_qubits (fun q => m + q) (f i)`,
placing the data-register action at qubit positions [m, m + anc)
and leaving the control register at [0, m). This file proves:
- `is_fresh_map_qubits_shift`: control qubits are fresh in lifted circuits.
- `wellTyped_map_qubits_shift`: lifted circuits remain well-typed on the
enlarged register.
- `uc_eval_map_qubits_shift_commutes_pad_u`: matrix-level block-disjoint
commutation — the key bridge that validates the abstract cascade's
`h_comm_all` hypothesis for QPE's layout.
- `uc_eval_controlled_powers_shifted_on_common_eigenstate`: the QPE-
specific cascade theorem, derived by discharging the abstract cascade
theorem's hypotheses with the three lemmas above.
This file imports both `ControlledGates` (for the abstract cascade) and
`Shor` (for `map_qubits`). The two have no cyclic dependency: Shor.lean
imports only `Eigenstate` + `TotientLowerBound`, neither of which uses
the control-stub fix.
(no documented top-level declarations)
FormalRV.QPE.PhaseKickback.ControlFactorization
FormalRV/QPE/PhaseKickback/ControlFactorization.lean
PhaseKickback — Part6 (re-export shim part; same namespace, opens de-duplicated).
theorempad_ctrl_control_kron_vec_factors
theorem pad_ctrl_control_kron_vec_factors {m anc a b : Nat}
(ha : a < m) (hb : b < m)
(χ : Matrix (Fin (2^m)) (Fin 1) ℂ) (ψ : Matrix (Fin (2^anc)) (Fin 1) ℂ) :
pad_ctrl (m + anc) a b σx * kron_vec χ ψ
= kron_vec (pad_ctrl m a b σx * χ) ψ*Control-register `pad_ctrl` (CNOT) factorization.** When both
the control qubit `a` and the target qubit `b` lie in the control
register (`a, b < m`), the CNOT factors through `kron_vec` and only
affects the control component `χ`.
theoremuc_eval_control_register_circuit_kron_vec
theorem uc_eval_control_register_circuit_kron_vec
{m anc : Nat}
(c : FormalRV.Framework.BaseUCom m)
(h_wt : UCom.WellTyped m c)
(χ : Matrix (Fin (2^m)) (Fin 1) ℂ)
(ψ : Matrix (Fin (2^anc)) (Fin 1) ℂ) :
FormalRV.Framework.uc_eval
(map_qubits (fun q => q) c : FormalRV.Framework.BaseUCom (m + anc))
* kron_vec χ ψ
= kron_vec (FormalRV.Framework.uc_eval c * χ) ψ*Generic control-register circuit factorization.** Any well-typed
`BaseUCom m` circuit, lifted via `map_qubits (· + 0) = id` to
`BaseUCom (m + anc)`, factors through `kron_vec` and acts only on the
control component `χ`. Structural induction on the circuit; each gate
case dispatches to the corresponding control-side factorization lemma.
FormalRV.QPE.PhaseKickback.ControlSideLinearity
FormalRV/QPE/PhaseKickback/ControlSideLinearity.lean
PhaseKickback — Part3 (re-export shim part; same namespace, opens de-duplicated).
theorempadEquiv_control_eq_kron_combine
theorem padEquiv_control_eq_kron_combine (m anc n : Nat) (hn : n < m)
(h_combined : n < m + anc)
(h_size : m + anc - n - 1 = (m - n - 1) + anc)
(xH : Fin (2^n)) (xM : Fin 2) (xL : Fin (2^(m-n-1)))
(y : Fin (2^anc)) :
(padEquiv (m + anc) n h_combined
((xH, xM), Fin.cast (by rw [h_size]) (kron_vec_combine xL y))).val
= (kron_vec_combine (padEquiv m n hn ((xH, xM), xL)) y).valtheorempad_u_control_kron_basis_factors
theorem pad_u_control_kron_basis_factors
{m anc n : Nat} (hn : n < m)
(M : Matrix (Fin 2) (Fin 2) ℂ)
(x : Fin (2^m)) (y : Fin (2^anc)) :
pad_u (m + anc) n M
* kron_vec (FormalRV.Framework.basis_vector (2^m) x.val)
(FormalRV.Framework.basis_vector (2^anc) y.val)
= kron_vec (pad_u m n M * FormalRV.Framework.basis_vector (2^m) x.val)
(FormalRV.Framework.basis_vector (2^anc) y.val)*Control-side `pad_u` / `kron_vec` factorization (basis form).**
Mirror of `pad_u_shifted_kron_basis_factors` for control-register
gates. For `pad_u (m + anc) n M` with `n < m` (i.e., the qubit lies in
the control register), the action on a tensor of two basis vectors
factors through the local control-side `pad_u m n M`:
pad_u (m + anc) n M * kron_vec (basis_x) (basis_y)
= kron_vec (pad_u m n M * basis_x) (basis_y)
Proof: structurally identical to the data-side theorem, but uses
`padEquiv_control_eq_kron_combine` as the alignment bridge instead
of the data-side bridge, and decomposes `x` and `kron_vec_high r` via
`padEquiv m n` instead of `y` and `kron_vec_low r` via `padEquiv anc n`.
theorempad_u_control_kron_basis_control_vec
theorem pad_u_control_kron_basis_control_vec {m anc n : Nat} (hn : n < m)
(M : Matrix (Fin 2) (Fin 2) ℂ)
(x : Fin (2^m)) (ψ : Matrix (Fin (2^anc)) (Fin 1) ℂ) :
pad_u (m + anc) n M
* kron_vec (FormalRV.Framework.basis_vector (2^m) x.val) ψ
= kron_vec (pad_u m n M * FormalRV.Framework.basis_vector (2^m) x.val) ψ*Linearity extension: control-side `pad_u` on basis-control,
arbitrary-data `kron_vec`.** Same linearity-over-basis-decomposition
strategy as `pad_u_shifted_kron_basis_control_vec`.
theoremkron_vec_sum_left
theorem kron_vec_sum_left {a b : Nat}
{ι : Type*} [Fintype ι] (s : ι → Matrix (Fin (2^a)) (Fin 1) ℂ)
(φ : Matrix (Fin (2^b)) (Fin 1) ℂ) :
kron_vec (∑ y, s y) φ = ∑ y, kron_vec (s y) φLinearity of `kron_vec` on the LEFT over finite sums.
Companion to `kron_vec_sum_right`.
theorempad_u_control_kron_vec_factors
theorem pad_u_control_kron_vec_factors {m anc n : Nat} (hn : n < m)
(M : Matrix (Fin 2) (Fin 2) ℂ)
(χ : Matrix (Fin (2^m)) (Fin 1) ℂ) (ψ : Matrix (Fin (2^anc)) (Fin 1) ℂ) :
pad_u (m + anc) n M * kron_vec χ ψ
= kron_vec (pad_u m n M * χ) ψ*Arbitrary control-vector `pad_u` factorization.** Extends
`pad_u_control_kron_basis_control_vec` (basis-control) to arbitrary
`χ` via linearity over the basis decomposition.
theoremuc_eval_app1_control_kron_vec
theorem uc_eval_app1_control_kron_vec {m anc n : Nat} (hn : n < m)
(u : FormalRV.Framework.BaseUnitary 1)
(χ : Matrix (Fin (2^m)) (Fin 1) ℂ) (ψ : Matrix (Fin (2^anc)) (Fin 1) ℂ) :
FormalRV.Framework.uc_eval
(UCom.app1 u n : FormalRV.Framework.BaseUCom (m + anc)) * kron_vec χ ψ
= kron_vec
(FormalRV.Framework.uc_eval (UCom.app1 u n : FormalRV.Framework.BaseUCom m) * χ) ψ*App1 control-register wrapper.** Since `BaseUnitary 1` has only
the `R` constructor, this reduces to `pad_u_control_kron_vec_factors`.
theoremuc_eval_npar_H_kron_vec_aux
theorem uc_eval_npar_H_kron_vec_aux (m anc : Nat) (hm : 0 < m)
(χ : Matrix (Fin (2^m)) (Fin 1) ℂ) (ψ : Matrix (Fin (2^anc)) (Fin 1) ℂ) :
∀ k, k ≤ m →
FormalRV.Framework.uc_eval
(npar_H k : FormalRV.Framework.BaseUCom (m + anc)) * kron_vec χ ψ
= kron_vec
(FormalRV.Framework.uc_eval (npar_H k : FormalRV.Framework.BaseUCom m) * χ) ψ*Auxiliary: `npar_H k` factorization for any `k ≤ m`.** Induction
on `k` with `m` fixed. The H at qubit `k < m` lifts to
`pad_u (m+anc) k hMatrix`, which factors through `kron_vec` via
`pad_u_control_kron_vec_factors`.
theoremuc_eval_npar_H_kron_vec
theorem uc_eval_npar_H_kron_vec (m anc : Nat) (hm : 0 < m)
(χ : Matrix (Fin (2^m)) (Fin 1) ℂ) (ψ : Matrix (Fin (2^anc)) (Fin 1) ℂ) :
FormalRV.Framework.uc_eval
(npar_H m : FormalRV.Framework.BaseUCom (m + anc)) * kron_vec χ ψ
= kron_vec
(FormalRV.Framework.uc_eval (npar_H m : FormalRV.Framework.BaseUCom m) * χ) ψ*`npar_H m` factors through `kron_vec`.** The full Hadamard column
on `m` control qubits acts on a `kron_vec χ ψ` by applying `npar_H m`
to the control component `χ` and leaving the data component `ψ`
unchanged. Specialization of the auxiliary lemma at `k = m`.
theorempad_u_one_zero_eq
theorem pad_u_one_zero_eq (M : Matrix (Fin 2) (Fin 2) ℂ) : pad_u 1 0 M = M
For `dim = 1`, `pad_u 1 0 M = M`. The reindex layer collapses
because the high and low padding factors are `Iₙ(1)`.
theoremhMatrix_mul_basis_zero
theorem hMatrix_mul_basis_zero :
hMatrix * FormalRV.Framework.basis_vector 2 0
= ((Real.sqrt 2 / 2 : ℂ)) •
(FormalRV.Framework.basis_vector 2 0 +
FormalRV.Framework.basis_vector 2 1)`hMatrix * |0⟩ = (√2/2) · (|0⟩ + |1⟩)`. The fundamental Hadamard
identity on the standard zero state. Proved by 2-entry extensionality.
theoremH_zero_eq_plus
theorem H_zero_eq_plus :
FormalRV.Framework.uc_eval
(FormalRV.Framework.BaseUCom.H 0 : FormalRV.Framework.BaseUCom 1) *
FormalRV.Framework.kron_zeros 1
= ((Real.sqrt 2 / 2 : ℂ)) •
(FormalRV.Framework.basis_vector 2 0 +
FormalRV.Framework.basis_vector 2 1)*Single-qubit H-on-zero**: `uc_eval (H 0 : BaseUCom 1) * kron_zeros 1
= (√2/2) · (basis_vector 2 0 + basis_vector 2 1)`. The base case of
the m-qubit `npar_H` induction.
FormalRV.QPE.PhaseKickback.FourierFormQPE
FormalRV/QPE/PhaseKickback/FourierFormQPE.lean
PhaseKickback — Part5 (re-export shim part; same namespace, opens de-duplicated).
defcontrolBit
noncomputable def controlBit (m i : Nat) (hi : i < m) (x : Fin (2^m)) : Bool
*Control bit at position `i`.** Boolean indicator of whether the
`i`-th qubit of `x : Fin (2^m)` (viewed via the framework's `padEquiv`
decomposition) is 1. Defined via `padEquiv m i hi` so it aligns with
`pad_u_proj{0,1}_on_basis_vector_{zero,one}`.
theoremcontrolBit_eq_digit
theorem controlBit_eq_digit (m i : Nat) (hi : i < m) (x : Fin (2^m)) :
controlBit m i hi x = ((x.val / 2^(m-i-1)) % 2 = 1)*Control bit ↔ binary digit.** The `controlBit m i hi x` Boolean is
true exactly when the `(m-i-1)`-th bit of `x.val` is set; this is the
MSB-first convention coming from `padEquiv`.
defcontrolBitNat
noncomputable def controlBitNat (m i : Nat) (hi : i < m) (x : Fin (2^m)) : Nat
*Numeric form of `controlBit`.** Returns the actual `Nat` digit
(0 or 1) of `x` at position `i` under the MSB-first convention.
theoremcontrolBitNat_eq_digit
theorem controlBitNat_eq_digit (m i : Nat) (hi : i < m) (x : Fin (2^m)) :
controlBitNat m i hi x = (x.val / 2^(m-i-1)) % 2*Numeric `controlBit` equals the binary digit.**
defphase_prefix
noncomputable def phase_prefix (ζ : Nat → ℂ) (m : Nat) (x : Fin (2^m)) :
Nat → ℂ
| 0 => 1
| k+1 =>
(if h : k < m then
(if controlBit m k h x then ζ k else 1)
else 1) * phase_prefix ζ m x k*Recursive phase prefix.** The scalar accumulated by applying the
first `k` phase projectors to the basis-control state `|x⟩`. Matches
the order of `phase_projector_product`.
theoremphase_prefix_succ
theorem phase_prefix_succ {ζ : Nat → ℂ} {m : Nat} (x : Fin (2^m)) (k : Nat)
(hk : k < m) :
phase_prefix ζ m x (k+1) =
(if controlBit m k hk x then ζ k else 1) * phase_prefix ζ m x kUnfolding equation for `phase_prefix` at the successor case when
`k < m`.
theoremphase_projector_on_kron_basis
theorem phase_projector_on_kron_basis
{m anc i : Nat} (hi : i < m)
(ζi : ℂ)
(x : Fin (2^m))
(ψ : Matrix (Fin (2^anc)) (Fin 1) ℂ) :
@phase_projector (m + anc) i ζi
* kron_vec (FormalRV.Framework.basis_vector (2^m) x.val) ψ
= (if controlBit m i hi x then ζi else 1) •
kron_vec (FormalRV.Framework.basis_vector (2^m) x.val) ψ*Single phase projector on basis-control kron.** The phase
projector `P0_i + ζ_i · P1_i` lifted to the combined `(m + anc)`-qubit
register acts on `kron_vec (basis_vector x) ψ` by leaving the data
register `ψ` unchanged and multiplying by `ζ_i` (when bit `i` of `x`
is 1) or `1` (when it is 0).
theoremphase_projector_product_prefix_on_kron_basis
theorem phase_projector_product_prefix_on_kron_basis
{m anc : Nat}
(ζ : Nat → ℂ)
(x : Fin (2^m))
(ψ : Matrix (Fin (2^anc)) (Fin 1) ℂ) :
∀ k, k ≤ m →
@phase_projector_product (m + anc) ζ k
* kron_vec (FormalRV.Framework.basis_vector (2^m) x.val) ψ
= phase_prefix ζ m x k •
kron_vec (FormalRV.Framework.basis_vector (2^m) x.val) ψ*Phase-projector-product prefix on basis-control kron.** Induction
on the inner index `k` (with `m` fixed): the prefix of `k` phase
projectors applied to `kron_vec (basis_vector x) ψ` yields the
`phase_prefix ζ m x k` scalar acting on the same kron state.
theoremphase_projector_product_on_kron_basis
theorem phase_projector_product_on_kron_basis
{m anc : Nat}
(ζ : Nat → ℂ)
(x : Fin (2^m))
(ψ : Matrix (Fin (2^anc)) (Fin 1) ℂ) :
@phase_projector_product (m + anc) ζ m
* kron_vec (FormalRV.Framework.basis_vector (2^m) x.val) ψ
= phase_prefix ζ m x m •
kron_vec (FormalRV.Framework.basis_vector (2^m) x.val) ψ*Full phase-projector product on basis-control kron**: specialization
of the prefix theorem at `k = m`.
theoremphase_projector_product_on_uniform_control_sum
theorem phase_projector_product_on_uniform_control_sum
{m anc : Nat}
(ζ : Nat → ℂ)
(ψ : Matrix (Fin (2^anc)) (Fin 1) ℂ) :
@phase_projector_product (m + anc) ζ m
* (((1 : ℂ) / Real.sqrt (2^m : ℝ)) •
∑ x : Fin (2^m),
kron_vec (FormalRV.Framework.basis_vector (2^m) x.val) ψ)
= ((1 : ℂ) / Real.sqrt (2^m : ℝ)) •
∑ x : Fin (2^m),
phase_prefix ζ m x m •
kron_vec (FormalRV.Framework.basis_vector (2^m) x.val) ψ*PHASE-WEIGHTED FORM OF THE UNIFORM CONTROL SUM.** Applying the
phase-projector product to the H-prepared uniform superposition yields
the phase-weighted sum over basis-control states. This is the state
shape that QFTinv will consume in the next pass.
Proof: `Matrix.mul_smul` pulls the prefactor through, `Matrix.mul_sum`
distributes over the sum, then `phase_projector_product_on_kron_basis`
gives the per-term phase weight.
lemmabinary_expansion_lsb
lemma binary_expansion_lsb (m n : Nat) (hn : n < 2^m) :
n = ∑ i ∈ Finset.range m, ((n / 2^i) % 2) * 2^i*LSB-first binary expansion.** Any `n < 2^m` is the sum of its
binary digits times the corresponding powers of two, with index `i`
weighted by `2^i`.
lemmabinary_expansion_msb
lemma binary_expansion_msb (m n : Nat) (hn : n < 2^m) :
n = ∑ i ∈ Finset.range m, ((n / 2^(m-i-1)) % 2) * 2^(m-i-1)*MSB-first binary expansion.** Same as `binary_expansion_lsb`
but reindexed so the `i`-th term is weighted by `2^(m-i-1)`, i.e.
the most-significant bit comes first (matching `padEquiv`'s
MSB-first decomposition).
defcontrolWeightedIndex
noncomputable def controlWeightedIndex (m : Nat) (x : Fin (2^m)) : Nat
*Weighted control index.** The integer reconstructed from the
control bits of `x` under the MSB-first weighting.
theoremcontrolWeightedIndex_eq_val
theorem controlWeightedIndex_eq_val (m : Nat) (x : Fin (2^m)) :
controlWeightedIndex m x = x.val*Weighted control index equals `x.val`.** The phase-kickback
"weighted index" is exactly the underlying natural number — the
abstract bit-by-bit accumulation reassembles the binary expansion.
defqpeEigenvalue
noncomputable def qpeEigenvalue (m i : Nat) (θ : ℝ) : ℂ
*QPE eigenvalue at qubit `i`.** The eigenvalue that the `i`-th
controlled-power gadget would impart on a phase-`θ` eigenstate, under
the MSB-first weighting `2^(m-i-1)`.
defpartialWeightedIndex
noncomputable def partialWeightedIndex (m k : Nat) (x : Fin (2^m)) : Nat
*Partial weighted index.** Sum of `controlBitNat · 2^(m-i-1)` over
the first `k` qubits. At `k = m` this equals `controlWeightedIndex` and
hence `x.val`.
theorempartialWeightedIndex_at_m
theorem partialWeightedIndex_at_m (m : Nat) (x : Fin (2^m)) :
partialWeightedIndex m m x = x.valAt `k = m`, the partial weighted index recovers `x.val`.
theorempartialWeightedIndex_succ
theorem partialWeightedIndex_succ (m k : Nat) (hk : k < m) (x : Fin (2^m)) :
partialWeightedIndex m (k+1) x
= partialWeightedIndex m k x
+ controlBitNat m k hk x * 2^(m-k-1)Successor unfolding for the partial weighted index.
theoremphase_prefix_qpe_eq_exp_partial
theorem phase_prefix_qpe_eq_exp_partial (m : Nat) (θ : ℝ) (x : Fin (2^m)) :
∀ k, k ≤ m →
phase_prefix (qpeEigenvalue m · θ) m x k
= Complex.exp (2 * Real.pi * Complex.I *
(partialWeightedIndex m k x : ℂ) * (θ : ℂ))*Phase-prefix on QPE eigenvalues equals exp of weighted partial index.**
The accumulating phase factor for the QPE-specific eigenvalues collapses
to a single complex exponential whose argument is `2πi · θ · (partial sum)`.
theoremphase_prefix_qpe_eq_exp_val
theorem phase_prefix_qpe_eq_exp_val (m : Nat) (θ : ℝ) (x : Fin (2^m)) :
phase_prefix (qpeEigenvalue m · θ) m x m
= Complex.exp (2 * Real.pi * Complex.I * (x.val : ℂ) * (θ : ℂ))*Phase-prefix at full length equals `exp(2πi · x.val · θ)`.**
Combines `phase_prefix_qpe_eq_exp_partial` at `k = m` with
`partialWeightedIndex_at_m`. This is the bridge from the abstract
phase-projector cascade to the standard QPE phase-weighted form.
theoremQPE_pre_QFT_on_eigenstate_fourier_form
theorem QPE_pre_QFT_on_eigenstate_fourier_form
{m anc : Nat} (hmanc : 0 < m + anc) (hm : 0 < m)
(f : Nat → FormalRV.Framework.BaseUCom anc)
(ψ : Matrix (Fin (2^anc)) (Fin 1) ℂ)
(θ : ℝ)
(h_wt_all : ∀ i, i < m → UCom.WellTyped anc (f i))
(h_eig_data : ∀ i, i < m →
FormalRV.Framework.uc_eval (f i) * ψ =
qpeEigenvalue m i θ • ψ) :
FormalRV.Framework.uc_eval (controlled_powers
(fun i => (map_qubits (fun q => m + q) (f i) :
FormalRV.Framework.BaseUCom (m + anc))) m)*Pre-QFT QPE eigenstate result in explicit Fourier form.**
Given a data-register `ψ` such that each oracle `f i` (`i < m`) acts on
`ψ` as the QPE eigenvalue `exp(2πi · 2^(m-i-1) · θ)` (MSB-first
weighting), the composition `H^⊗m ; controlled_powers (shifted f) m`
applied to `|0^m⟩ ⊗ |ψ⟩` produces the phase-weighted Fourier
superposition `(1/√2^m) · ∑_x exp(2πi · x · θ) · |x⟩ ⊗ |ψ⟩`.
This is the state shape that a *real* `QFTinv` would consume to produce
`qpe_phase_state m θ ⊗ ψ`. The current `QFTinv` in
`Framework/QPE.lean` is a stub (see `QFTinv_is_stub` below); closing
`QPE_MMI_correct` further requires either implementing the real QFTinv
circuit or porting a QFT semantic axiom.
FormalRV.QPE.PhaseKickback.PadEquivBridge
FormalRV/QPE/PhaseKickback/PadEquivBridge.lean
PhaseKickback — Part2 (re-export shim part; same namespace, opens de-duplicated).
theorempadEquiv_combined_eq_kron_combine
theorem padEquiv_combined_eq_kron_combine
(m anc n : Nat) (hn : n < anc)
(h_combined : m + n < m + anc)
(h_size : m + anc - (m + n) - 1 = anc - n - 1)
(x : Fin (2^m)) (yH : Fin (2^n)) (yM : Fin 2)
(yL : Fin (2^(anc-n-1))) :
(padEquiv (m + anc) (m + n) h_combined
((kron_vec_combine x yH, yM), Fin.cast (by rw [h_size]) yL)).val
= (kron_vec_combine x (padEquiv anc n hn ((yH, yM), yL))).valtheorempad_u_shifted_kron_basis_factors
theorem pad_u_shifted_kron_basis_factors
{m anc n : Nat} (hn : n < anc)
(M : Matrix (Fin 2) (Fin 2) ℂ)
(x : Fin (2^m)) (y : Fin (2^anc)) :
pad_u (m + anc) (m + n) M
* kron_vec (FormalRV.Framework.basis_vector (2^m) x.val)
(FormalRV.Framework.basis_vector (2^anc) y.val)
= kron_vec (FormalRV.Framework.basis_vector (2^m) x.val)
(pad_u anc n M *
FormalRV.Framework.basis_vector (2^anc) y.val)*`pad_u` on `kron_vec` of basis vectors: factorization theorem.**
For the QPE shift convention (control register at qubits `[0, m)`,
data register at `[m, m + anc)`), `pad_u (m + anc) (m + n) M` applied
to a tensor of two basis vectors factors as `kron_vec` of the
control-side basis with the local `pad_u anc n M` action on the
data-side basis.
Proof outline:
1. Rewrite `kron_vec (basis_vector x) (basis_vector y)` as
`basis_vector (kron_vec_combine x y)` via
`kron_vec_basis_eq_basis_combine`.
2. After `ext r`, extract column entries using `mul_basis_vector_apply`.
3. Decompose `y` and `kron_vec_low r` via `padEquiv anc n`.
4. Apply the bridge `padEquiv_combined_eq_kron_combine` to express
both `r` and the combined index in `padEquiv (m+anc) (m+n)` form.
5. Apply `pad_u_apply_reindex` to both LHS entry and RHS pad_u entry.
6. Case split (2x2x2 = 8 cases) on `kron_vec_high r = x`, `lrH = yH`,
`lrL = yL`. Each case reduces to `combine_kron`-injectivity
arithmetic + `simp`.
theoremvec_eq_sum_basis
theorem vec_eq_sum_basis (n : Nat) (ψ : Matrix (Fin n) (Fin 1) ℂ) :
ψ = ∑ y : Fin n, ψ y 0 • FormalRV.Framework.basis_vector n y.val*Vector decomposition into basis.** Any matrix column vector
equals the sum over basis vectors weighted by its entries. The
elementary linear algebra fact `ψ = ∑ y, ψ y 0 • basis_vector y`.
theoremkron_vec_sum_right
theorem kron_vec_sum_right {a b : Nat} (χ : Matrix (Fin (2^a)) (Fin 1) ℂ)
{ι : Type*} [Fintype ι] (s : ι → Matrix (Fin (2^b)) (Fin 1) ℂ) :
kron_vec χ (∑ y, s y) = ∑ y, kron_vec χ (s y)Linearity of `kron_vec` on the right over finite sums.
theorempad_u_shifted_kron_basis_control_vec
theorem pad_u_shifted_kron_basis_control_vec {m anc n : Nat} (hn : n < anc)
(M : Matrix (Fin 2) (Fin 2) ℂ)
(x : Fin (2^m)) (ψ : Matrix (Fin (2^anc)) (Fin 1) ℂ) :
pad_u (m + anc) (m + n) M
* kron_vec (FormalRV.Framework.basis_vector (2^m) x.val) ψ
= kron_vec (FormalRV.Framework.basis_vector (2^m) x.val)
(pad_u anc n M * ψ)*Single-qubit `pad_u` on basis-control, arbitrary-data kron.**
The basis-state theorem `pad_u_shifted_kron_basis_factors` extends
by linearity over the basis decomposition of `ψ`:
pad_u (m + anc) (m + n) M * kron_vec (basis_vector x) ψ
= kron_vec (basis_vector x) (pad_u anc n M * ψ).
Proof: decompose `ψ` as `∑_y ψ(y, 0) • basis_y`, distribute via
`kron_vec_sum_right` and `Matrix.mul_sum`, then apply the basis
theorem pointwise.
theorempad_ctrl_shifted_kron_basis_control_vec
theorem pad_ctrl_shifted_kron_basis_control_vec {m anc a b : Nat}
(ha : a < anc) (hb : b < anc)
(x : Fin (2^m)) (ψ : Matrix (Fin (2^anc)) (Fin 1) ℂ) :
pad_ctrl (m + anc) (m + a) (m + b) σx
* kron_vec (FormalRV.Framework.basis_vector (2^m) x.val) ψ
= kron_vec (FormalRV.Framework.basis_vector (2^m) x.val)
(pad_ctrl anc a b σx * ψ)*`pad_ctrl` (CNOT) on basis-control, arbitrary-data kron.**
The shifted CNOT factors through `kron_vec` for any data state.
Derivable from `pad_u_shifted_kron_basis_control_vec` via
`pad_ctrl`'s projector decomposition.
theoremuc_eval_map_qubits_shift_kron_basis_control_vec
theorem uc_eval_map_qubits_shift_kron_basis_control_vec {m anc : Nat}
(c : FormalRV.Framework.BaseUCom anc)
(h_wt : UCom.WellTyped anc c)
(x : Fin (2^m)) (ψ : Matrix (Fin (2^anc)) (Fin 1) ℂ) :
FormalRV.Framework.uc_eval
(map_qubits (fun q => m + q) c : FormalRV.Framework.BaseUCom (m + anc))
* kron_vec (FormalRV.Framework.basis_vector (2^m) x.val) ψ
= kron_vec (FormalRV.Framework.basis_vector (2^m) x.val)
(FormalRV.Framework.uc_eval c * ψ)*CIRCUIT-LEVEL shifted factorization.** For any well-typed
`BaseUCom anc` circuit `c`, the shifted lift `map_qubits (· + m) c`
acts on `kron_vec (basis_vector x) ψ` by leaving the control-side
basis state intact and applying the local `uc_eval c` to the data
side.
Proof: structural induction on `c`. Each gate case uses the
corresponding shifted basis-control-vec lemma; `seq` chains via IH
and matrix associativity; `app3` is vacuous.
theoremlifted_oracle_eigen_on_kron_basis_control_vec
theorem lifted_oracle_eigen_on_kron_basis_control_vec {m anc : Nat}
(f : FormalRV.Framework.BaseUCom anc)
(x : Fin (2^m)) (ψ : Matrix (Fin (2^anc)) (Fin 1) ℂ) (ζ : ℂ)
(h_wt : UCom.WellTyped anc f)
(h_eig : FormalRV.Framework.uc_eval f * ψ = ζ • ψ) :
FormalRV.Framework.uc_eval
(map_qubits (fun q => m + q) f : FormalRV.Framework.BaseUCom (m + anc))
* kron_vec (FormalRV.Framework.basis_vector (2^m) x.val) ψ
= ζ • kron_vec (FormalRV.Framework.basis_vector (2^m) x.val) ψ*Unconditional lifted-oracle eigen on basis-control kron.**
Given a data-register eigenstate `ψ` of `f` with eigenvalue `ζ`,
the shifted oracle `map_qubits (· + m) f` has `kron_vec (basis_x) ψ`
as eigenstate with the same eigenvalue.
This is the unconditional version of
`lifted_oracle_eigen_on_kron_control_conditional` for basis-control
states. The proof is a 2-line composition of the circuit-level
shifted factorization theorem above with the scalar pull-out via
`kron_vec_smul_right`.
FormalRV.QPE.PhaseKickback.ShiftedCascade
FormalRV/QPE/PhaseKickback/ShiftedCascade.lean
PhaseKickback — Part1 (re-export shim part; same namespace, opens de-duplicated).
theoremis_fresh_map_qubits_shift
theorem is_fresh_map_qubits_shift {m anc q : Nat}
(c : BaseUCom anc) (hq : q < m) :
is_fresh q (map_qubits (fun x => m + x) c : BaseUCom (m + anc))*Shifted freshness.** Any control qubit `q < m` is fresh in the
shift-lifted circuit `map_qubits (fun x => m + x) c`, because every gate's
qubit index becomes `m + n ≥ m > q`.
theoremwellTyped_map_qubits_shift
theorem wellTyped_map_qubits_shift {m anc : Nat}
(c : BaseUCom anc) (h_wt : UCom.WellTyped anc c) :
UCom.WellTyped (m + anc)
(map_qubits (fun x => m + x) c : BaseUCom (m + anc))*Shifted well-typedness.** A circuit well-typed on `anc` qubits
becomes well-typed on `m + anc` after shifting every index by `+m`.
theoremuc_eval_map_qubits_shift_commutes_pad_u
theorem uc_eval_map_qubits_shift_commutes_pad_u {m anc q : Nat}
(c : BaseUCom anc) (hq : q < m) (U : Matrix (Fin 2) (Fin 2) ℂ) :
pad_u (m + anc) q U *
FormalRV.Framework.uc_eval
(map_qubits (fun x => m + x) c : BaseUCom (m + anc))
= FormalRV.Framework.uc_eval
(map_qubits (fun x => m + x) c : BaseUCom (m + anc)) *
pad_u (m + anc) q U*Block-disjoint commutation.** For any control-register qubit
`q < m`, the matrix `pad_u (m + anc) q U` commutes with the matrix
semantics of a shift-lifted data-register circuit. This is the crucial
lemma validating the `h_comm_all` hypothesis of the abstract cascade
theorem for QPE's specific block layout.
Proof by induction on `c`:
- `seq`: by IH on both sides + reassociation;
- `app1 (R θ φ λ) n`: shifted target `m + n` satisfies `q < m ≤ m + n`,
so `pad_u_disjoint_comm'` applies;
- `app2 CNOT a b`: shifted targets `m + a`, `m + b` both `> q`, so
`pad_u_pad_ctrl_disjoint_comm` applies;
- `app3`: vacuous since `BaseUnitary 3` is empty.
theoremuc_eval_controlled_powers_shifted_on_common_eigenstate
theorem uc_eval_controlled_powers_shifted_on_common_eigenstate
{m anc : Nat} (hd : 0 < m + anc)
(f : Nat → BaseUCom anc)
(h_wt_all : ∀ i, i < m → UCom.WellTyped anc (f i))
(ψ : Matrix (Fin (2^(m + anc))) (Fin 1) ℂ) (ζ : Nat → ℂ)
(h_eig : ∀ i, i < m →
FormalRV.Framework.uc_eval
(map_qubits (fun x => m + x) (f i) : BaseUCom (m + anc)) * ψ
= ζ i • ψ) :
FormalRV.Framework.uc_eval (controlled_powers
(fun i => (map_qubits (fun x => m + x) (f i) : BaseUCom (m + anc))) m) * ψ
= @phase_projector_product (m + anc) ζ m * ψ*QPE-SHIFTED CASCADE THEOREM.** The full controlled-powers
phase-kickback identity, specialized to QPE's shift-lifted oracle
family `i ↦ map_qubits (fun x => m + x) (f i)`. All commutation,
freshness, and well-typedness hypotheses of the abstract cascade
theorem are discharged automatically using the three lemmas above;
the caller need only supply the per-oracle well-typedness and the
common eigenstate relation.
abbrevKronVecShiftHyp
abbrev KronVecShiftHyp (m anc : Nat) (f : FormalRV.Framework.BaseUCom anc)
(χ : Matrix (Fin (2^m)) (Fin 1) ℂ)
(ψ : Matrix (Fin (2^anc)) (Fin 1) ℂ) : Prop*The shifted-oracle / kron-vec interaction hypothesis.**
`pad_u`/`pad_ctrl` on the data-register block `[m, m + anc)` should
act on a `kron_vec` state by leaving the control component `χ`
unchanged and applying the unshifted oracle to the data component `ψ`.
This abbreviation packages the statement so the conditional
theorems below can require it as an explicit hypothesis. Proving it
unconditionally (i.e., for every `f : BaseUCom anc`) requires the
`pad_u`-on-`kron_vec` interaction infrastructure (a known
multi-file gap in the framework).
theoremlifted_oracle_eigen_on_kron_control_conditional
theorem lifted_oracle_eigen_on_kron_control_conditional
{m anc : Nat}
(f : FormalRV.Framework.BaseUCom anc)
(χ : Matrix (Fin (2^m)) (Fin 1) ℂ)
(ψ : Matrix (Fin (2^anc)) (Fin 1) ℂ)
(ζ : ℂ)
(h_eig : FormalRV.Framework.uc_eval f * ψ = ζ • ψ)
(h_shift_kron : KronVecShiftHyp m anc f χ ψ) :
FormalRV.Framework.uc_eval
(map_qubits (fun q => m + q) f : FormalRV.Framework.BaseUCom (m + anc))
* kron_vec χ ψ
= ζ • kron_vec χ ψ*Conditional eigen-on-kron-control.** Given the kron-vec
interaction hypothesis and the data-register eigen-relation, the
combined `χ ⊗ᵥ ψ` is an eigenstate of the shifted oracle with the
same eigenvalue. The proof is one rewrite + a scalar pull-out
(`kron_vec_smul_right`).
abbrevNparHKronZerosUniformHyp
abbrev NparHKronZerosUniformHyp (m anc : Nat)
(ψ : Matrix (Fin (2^anc)) (Fin 1) ℂ) : Prop*The H-on-zeros / uniform-superposition hypothesis.** The
column of Hadamards `npar_H m` applied to `kron_vec (kron_zeros m) ψ`
produces the uniform superposition `(1/√2^m) · ∑_x |x⟩ ⊗ ψ` on
the control register, leaving the data register `ψ` untouched.
theoremQPE_pre_QFT_on_eigenstate_conditional
theorem QPE_pre_QFT_on_eigenstate_conditional
{m anc : Nat} (hmanc : 0 < m + anc)
(f : Nat → FormalRV.Framework.BaseUCom anc)
(ψ : Matrix (Fin (2^anc)) (Fin 1) ℂ) (ζ : Nat → ℂ)
(h_wt_all : ∀ i, i < m → UCom.WellTyped anc (f i))
(h_shift_kron_eig_uniform : ∀ i, i < m →
FormalRV.Framework.uc_eval
(map_qubits (fun q => m + q) (f i) :
FormalRV.Framework.BaseUCom (m + anc))
* (((1 : ℂ) / Real.sqrt (2 ^ m)) •
∑ x : Fin (2^m),
kron_vec (FormalRV.Framework.basis_vector (2^m) x.val) ψ)*CONDITIONAL pre-QFT QPE composition on a common eigenstate.**
Composes `npar_H m` (Hadamard layer on control register) with the
shifted controlled-powers cascade. The eigenvalue carries to the
phase-projector-product form on the uniform-superposition state.
This is the pre-QFT half of QPE; combining it with `QFTinv k` on the
phase-projector-product form yields the `qpe_phase_state k θ ⊗ ψ`
that QPE measurement projects against.
The conditional version takes two explicit hypotheses for the missing
`pad_u`/`kron_vec` infrastructure:
- `h_npar_H : NparHKronZerosUniformHyp m anc ψ` — the H-on-zeros step;
- `h_shift_kron_eig_uniform` — the shifted-oracle eigen-relation on
the uniform-superposition state. (The latter would follow from
`h_eig_data` + a `KronVecShiftHyp` lemma for the uniform sum;
exposed here as a single hypothesis for the conditional form.)
Once the `pad_u`-on-`kron_vec` infrastructure lands, both hypotheses
become provable and the conditional becomes unconditional.
theoremkron_vec_basis_eq_basis_combine
theorem kron_vec_basis_eq_basis_combine (a b : Nat) (x : Fin (2^a)) (y : Fin (2^b)) :
kron_vec (FormalRV.Framework.basis_vector (2^a) x.val)
(FormalRV.Framework.basis_vector (2^b) y.val)
= FormalRV.Framework.basis_vector (2^(a+b)) (kron_vec_combine x y).val*Kron of two basis vectors = basis of combined index.** The
elementary fact that `|x⟩ ⊗ |y⟩` (on `m + anc` qubits) is the standard
basis vector for the combined index `kron_vec_combine x y`. Used
downstream when the QPE proof reduces actions on `kron_vec` to actions
on individual basis states.
FormalRV.QPE.PhaseKickback.UniformSuperpositionEigenstate
FormalRV/QPE/PhaseKickback/UniformSuperpositionEigenstate.lean
PhaseKickback — Part4 (re-export shim part; same namespace, opens de-duplicated).
theorempad_u_shifted_kron_vec_factors
theorem pad_u_shifted_kron_vec_factors {m anc n : Nat} (hn : n < anc)
(M : Matrix (Fin 2) (Fin 2) ℂ)
(χ : Matrix (Fin (2^m)) (Fin 1) ℂ) (ψ : Matrix (Fin (2^anc)) (Fin 1) ℂ) :
pad_u (m + anc) (m + n) M * kron_vec χ ψ
= kron_vec χ (pad_u anc n M * ψ)*Arbitrary-control + arbitrary-data data-side factorization.**
The full generality of `pad_u_shifted_kron_basis_control_vec` — by
linearity over the basis decomposition of χ.
theoremkron_zeros_succ
theorem kron_zeros_succ (m : Nat) :
FormalRV.Framework.kron_zeros (m + 1)
= kron_vec (FormalRV.Framework.kron_zeros m)
(FormalRV.Framework.kron_zeros 1)*`kron_zeros (m+1) = kron_vec (kron_zeros m) (kron_zeros 1)`.**
Both sides reduce to `basis_vector (2^(m+1)) 0`.
theoreminv_sqrt_pow_two_succ
theorem inv_sqrt_pow_two_succ (m : Nat) :
((1 : ℂ) / Real.sqrt (2^m : ℝ)) * ((Real.sqrt 2 / 2 : ℂ))
= (1 : ℂ) / Real.sqrt (2^(m+1) : ℝ)*Scalar recurrence:** `(1/√2^m) · (√2/2) = 1/√2^(m+1)`.
theoremuniform_sum_succ_split
theorem uniform_sum_succ_split (m : Nat) :
∑ z : Fin (2^(m+1)), FormalRV.Framework.basis_vector (2^(m+1)) z.val
= ∑ x : Fin (2^m),
(kron_vec (FormalRV.Framework.basis_vector (2^m) x.val)
(FormalRV.Framework.basis_vector (2^1) 0)
+ kron_vec (FormalRV.Framework.basis_vector (2^m) x.val)
(FormalRV.Framework.basis_vector (2^1) 1))*Sum split over the last bit:** the uniform basis sum on `m+1`
qubits splits into pairs along the highest-bit / lowest-bit alternative.
theoreminv_sqrt_two_pow_one
private theorem inv_sqrt_two_pow_one :
((1 : ℂ) / Real.sqrt ((2:ℝ)^1)) = (Real.sqrt 2 / 2 : ℂ)Single-qubit `m=1` scalar special case.
theoremnpar_H_kron_zeros_pure_eq_uniform_sum
theorem npar_H_kron_zeros_pure_eq_uniform_sum :
∀ (m : Nat), 0 < m →
FormalRV.Framework.uc_eval
(npar_H m : FormalRV.Framework.BaseUCom m) *
FormalRV.Framework.kron_zeros m
= ((1 : ℂ) / Real.sqrt (2^m : ℝ)) •
∑ x : Fin (2^m), FormalRV.Framework.basis_vector (2^m) x.val*PURE H-ON-ZEROS UNIFORM SUPERPOSITION.** The Hadamard column
on `m` qubits applied to the all-zeros state produces the uniform
superposition `(1/√2^m) · ∑_x |x⟩`. Requires `0 < m` because at
`m = 0` the framework's `pad_u 0 0` returns zero. Inducts on `m`:
- m=1 base: `H_zero_eq_plus` + scalar special case.
- m+1 step: split via `kron_zeros_succ`, IH for prefix m H-gates via
`uc_eval_npar_H_kron_vec`, then the final H gate at position m via
`pad_u_shifted_kron_vec_factors` + `pad_u_one_zero_eq` +
`hMatrix_mul_basis_zero`; reassemble with kron-vec linearity and
`uniform_sum_succ_split`.
theoremnpar_H_kron_zeros_eq_uniform_sum
theorem npar_H_kron_zeros_eq_uniform_sum {m anc : Nat} (hm : 0 < m)
(ψ : Matrix (Fin (2^anc)) (Fin 1) ℂ) :
FormalRV.Framework.uc_eval (npar_H m : FormalRV.Framework.BaseUCom (m + anc))
* kron_vec (FormalRV.Framework.kron_zeros m) ψ
= ((1 : ℂ) / Real.sqrt (2^m : ℝ)) •
∑ x : Fin (2^m),
kron_vec (FormalRV.Framework.basis_vector (2^m) x.val) ψ*TENSORED H-ON-ZEROS UNIFORM SUPERPOSITION.** The H column on
`m` control qubits applied to `kron_vec (kron_zeros m) ψ` produces
the uniform-superposition state on the control register tensored with
the unchanged data state `ψ`. Combines the pure theorem with
`uc_eval_npar_H_kron_vec` (the m-qubit H factorization across kron).
theoremshifted_oracle_eigen_on_uniform_control_sum
theorem shifted_oracle_eigen_on_uniform_control_sum
{m anc : Nat}
(f : FormalRV.Framework.BaseUCom anc)
(ψ : Matrix (Fin (2^anc)) (Fin 1) ℂ)
(ζ : ℂ)
(h_wt : UCom.WellTyped anc f)
(h_eig_data : FormalRV.Framework.uc_eval f * ψ = ζ • ψ) :
FormalRV.Framework.uc_eval
(map_qubits (fun q => m + q) f : FormalRV.Framework.BaseUCom (m + anc))
*
(((1 : ℂ) / Real.sqrt (2^m : ℝ)) •
∑ x : Fin (2^m),*Shifted oracle eigen on the H-prepared uniform-superposition
state.** For each oracle `f` with data-register eigenstate `ψ` of
eigenvalue `ζ`, the lifted (shifted) oracle has the H-prepared
uniform sum `(1/√2^m) · ∑_x |x⟩ ⊗ ψ` as an eigenstate with the
same eigenvalue. Proved by distributing the matrix-vector
product over the scalar and the sum, applying
`lifted_oracle_eigen_on_kron_basis_control_vec` pointwise, then
reassembling via `smul_comm`.
theoremQPE_pre_QFT_on_eigenstate
theorem QPE_pre_QFT_on_eigenstate
{m anc : Nat} (hmanc : 0 < m + anc) (hm : 0 < m)
(f : Nat → FormalRV.Framework.BaseUCom anc)
(ψ : Matrix (Fin (2^anc)) (Fin 1) ℂ) (ζ : Nat → ℂ)
(h_wt_all : ∀ i, i < m → UCom.WellTyped anc (f i))
(h_eig_data : ∀ i, i < m → FormalRV.Framework.uc_eval (f i) * ψ = ζ i • ψ) :
FormalRV.Framework.uc_eval (controlled_powers
(fun i => (map_qubits (fun q => m + q) (f i) :
FormalRV.Framework.BaseUCom (m + anc))) m)
* (FormalRV.Framework.uc_eval
(npar_H m : FormalRV.Framework.BaseUCom (m + anc))
* kron_vec (FormalRV.Framework.kron_zeros m) ψ)*UNCONDITIONAL PRE-QFT QPE EIGENSTATE THEOREM.**
The full pre-QFT QPE composition on a data-register eigenstate `ψ`:
applying `npar_H m` then `controlled_powers` to `|0^m⟩ ⊗ ψ` produces
the phase-projector-product form acting on the uniform-superposition
state `(1/√2^m) · ∑_x |x⟩ ⊗ ψ`.
Composition of:
1. `npar_H_kron_zeros_eq_uniform_sum` — H prepares the uniform sum.
2. `shifted_oracle_eigen_on_uniform_control_sum` — establishes the
common-eigenstate hypothesis for each lifted oracle on the
uniform sum.
3. `uc_eval_controlled_powers_shifted_on_common_eigenstate` —
the QPE-shifted cascade theorem, which now applies because (2)
discharges its eigen hypothesis.
This is the cap of the pre-QFT half of QPE. The conditional
theorem `QPE_pre_QFT_on_eigenstate_conditional` from earlier
sessions is now subsumed by this unconditional version.
FormalRV.QPE.QPE
FormalRV/QPE/QPE.lean
FormalRV.Framework.QPE — Quantum Phase Estimation circuit.
Lean translation skeleton of `SQIR/examples/QPEGeneral.v`.
QPE applied to a unitary U with eigenstate |ψ⟩ (eigenvalue e^(2πi·θ))
outputs an n-bit approximation of θ.
Status: SCAFFOLDING. The circuit is defined; the correctness theorem
(success probability ≥ 4/π² for n-bit precision) is sorried — it requires
significant analysis of the inverse QFT applied to the right input state.
defQFT
noncomputable def QFT {dim : Nat} (n : Nat) : BaseUCom dimQuantum Fourier Transform on `n` qubits. SQIR's `QFT n` is a
well-known circuit; this is a stub.
defcontrolled_Rz
noncomputable def controlled_Rz {dim : Nat} (q t : Nat) (lam : ℝ) : BaseUCom dim*Controlled-Rz (controlled-phase) decomposition.** Five-gate
sequence implementing controlled-Rz via Rz, CNOT, Rz, CNOT, Rz.
definverse_qft_phase_ladder
noncomputable def inverse_qft_phase_ladder
{dim : Nat} (n target : Nat) : BaseUCom dim*Inverse-QFT phase ladder for one target.** Sequence of
controlled-Rz gates targeting qubit `target` from controls
`target+1, target+2, ..., n-1`, followed by `H target`.
defbit_reversal_swaps
noncomputable def bit_reversal_swaps {dim : Nat} (n : Nat) : BaseUCom dim*Bit-reversal SWAP cascade for `n` qubits.** Swaps qubit `i`
with qubit `n-1-i` for `i < n/2`. Required at the end of the
inverse-QFT to undo the QFT's natural reverse-bit ordering.
defreal_QFTinv_layer
noncomputable def real_QFTinv_layer {dim : Nat} (n : Nat) : BaseUCom dim*Recursive layer of the real inverse-QFT for `n` qubits.**
1. Bit-reversal SWAP cascade `bit_reversal_swaps n`.
2. For `target = n-1` down to `0`: `inverse_qft_phase_ladder n target`.
defQFTinv
noncomputable def QFTinv {dim : Nat} (n : Nat) : BaseUCom dim*Inverse QFT (QFT†)**: the real recursive inverse-QFT layer.
Previously a stub `invert (QFT n) = invert (npar_H n)` (semantically
wrong — see `FormalRV.SQIRPort.QFTinv_is_stub`). Replaced
2026-05-26 with the real recursive layer
`real_QFTinv_layer n`, whose matrix correctness is established by
`FormalRV.SQIRPort.uc_eval_real_QFTinv_layer_eq_IQFT_matrix`.
This replacement breaks the prior `QFT_QFTinv_id`-style cancellation
theorems (which only held because both QFT and QFTinv were `npar_H`
stubs). Those theorems are removed; the corresponding correct
behavior is captured in
`SQIRPort.uc_eval_real_QFTinv_layer_eq_IQFT_matrix`.
theoremQFT_eq_npar_H
theorem QFT_eq_npar_H {dim : Nat} (n : Nat) :
(QFT n : BaseUCom dim) = npar_H nThe current QFT stub equals npar_H — useful as a bridge to the
UnitaryOps lemmas about npar_H. When the real QFT is implemented,
this lemma will go away.
theoremuc_eval_QFT_succ
theorem uc_eval_QFT_succ {dim : Nat} (n : Nat) :
uc_eval (QFT (n + 1) : BaseUCom dim)
= pad_u dim n hMatrix * uc_eval (QFT n)Matrix form of QFT's succ: `uc_eval (QFT (n+1)) = pad_u dim n hMatrix
uc_eval (QFT n)`. Direct lift of `uc_eval_npar_H_succ` via QFT = npar_H.
theoremuc_eval_QFT_zero_eq_one
theorem uc_eval_QFT_zero_eq_one {dim : Nat} (h : 0 < dim) :
uc_eval (QFT 0 : BaseUCom dim) = (1 : Square dim)Matrix form of QFT's zero base case: `uc_eval (QFT 0) = 1` when 0 < dim.
theoremQFT_well_typed
theorem QFT_well_typed {dim : Nat} (n : Nat) (h : n ≤ dim) (hd : 0 < dim) :
UCom.WellTyped dim (QFT n : BaseUCom dim)The QFT stub is WellTyped on `dim` qubits when `n ≤ dim` (so all the
H gates fit) and `0 < dim` (so the SKIP base case is valid).
1-line corollary of `npar_H_well_typed` since QFT = npar_H definitionally.
theoremQFTinv_zero_unfold
theorem QFTinv_zero_unfold {dim : Nat} :
(QFTinv 0 : BaseUCom dim) = UCom.seq SKIP SKIP`QFTinv 0 = real_QFTinv_layer 0 = bit_reversal_swaps 0 ; SKIP =
SKIP ; SKIP` (a definitional simplification). Distinct from the
prior stub which gave `QFTinv 0 = SKIP` directly. Use
`uc_eval_QFTinv_zero_eq_one` for the matrix-level identity.
theoremuc_eval_QFTinv_zero_eq_one
theorem uc_eval_QFTinv_zero_eq_one {dim : Nat} (h : 0 < dim) :
uc_eval (QFTinv 0 : BaseUCom dim) = (1 : Square dim)Matrix form of QFTinv's zero base case: `uc_eval (QFTinv 0) = 1`
when `0 < dim`. The new `real_QFTinv_layer 0` is `SKIP ; SKIP`,
whose `uc_eval` is `1 * 1 = 1`.
theoremQFTinv_well_typed_of_layer_well_typed
theorem QFTinv_well_typed_of_layer_well_typed {dim : Nat} (n : Nat)
(h_layer_wt : UCom.WellTyped dim (real_QFTinv_layer n : BaseUCom dim)) :
UCom.WellTyped dim (QFTinv n : BaseUCom dim)The inverse QFT is WellTyped on `dim` qubits when `n ≤ dim` (so
all gates fit) and `0 < dim` (so the SKIP base cases are valid).
Proven via well-typedness of `real_QFTinv_layer`, which is
established in `FormalRV.SQIRPort.PostQFT.lean` as
`wellTyped_real_QFTinv_layer`. To avoid an import cycle, this
theorem's proof is parameterized: the calling site supplies
well-typedness of the inner layer (typically via the SQIRPort
theorem).
defcontrolled_powers
noncomputable def controlled_powers {dim : Nat} (f : Nat → BaseUCom dim) (n : Nat) : BaseUCom dimApply `f i` controlled on qubit `i` for i in [0, n).
theoremuc_eval_controlled_powers_zero
theorem uc_eval_controlled_powers_zero {dim : Nat} (f : Nat → BaseUCom dim) :
uc_eval (controlled_powers f 0) = uc_eval (SKIP : BaseUCom dim)Matrix form of controlled_powers' zero base case: equals SKIP.
theoremuc_eval_controlled_powers_zero_eq_one
theorem uc_eval_controlled_powers_zero_eq_one {dim : Nat}
(f : Nat → BaseUCom dim) (hd : 0 < dim) :
uc_eval (controlled_powers f 0) = (1 : Square dim)Well-typed matrix form for the empty controlled-powers chain:
`uc_eval (controlled_powers f 0) = 1` when 0 < dim.
theoremuc_eval_controlled_powers_succ
theorem uc_eval_controlled_powers_succ {dim : Nat} (f : Nat → BaseUCom dim) (n : Nat) :
uc_eval (controlled_powers f (n + 1))
= uc_eval (control n (f n)) * uc_eval (controlled_powers f n)Matrix form of controlled_powers' succ unfold: appending `control n (f n)`
left-multiplies by its uc_eval.
defQPE
noncomputable def QPE (k n : Nat) (c : Nat → BaseUCom (k + n)) : BaseUCom (k + n)
The QPE circuit on k+n qubits (matches SQIR `QPE k n c`).
The first k qubits are the measurement register, the next n are the
data register where c acts.
theoremQPE_def_unfold
theorem QPE_def_unfold {k n : Nat} (c : Nat → BaseUCom (k + n)) :
QPE k n c
= UCom.seq (npar_H k) (UCom.seq (controlled_powers c k) (QFTinv k))Definitional unfolding of QPE: exposes the 3-piece composition.
theoremuc_eval_QPE
theorem uc_eval_QPE {k n : Nat} (c : Nat → BaseUCom (k + n)) :
uc_eval (QPE k n c)
= uc_eval (QFTinv k) * uc_eval (controlled_powers c k) * uc_eval (npar_H k)Matrix form of QPE: the right-to-left chain
`uc_eval (QFTinv k) * uc_eval (controlled_powers c k) * uc_eval (npar_H k)`.
FormalRV.QPE.QPEAmplitude
FormalRV/QPE/QPEAmplitude.lean
FormalRV.Framework.QPEAmplitude — pure-math QPE amplitude/probability.
Standalone analytic development of the ideal Quantum Phase Estimation
amplitude/probability expressions. No circuit semantics, no SQIR, no
Hilbert-space tensor infrastructure — just the Dirichlet-kernel
arithmetic the QPE Born-rule analysis ultimately reduces to.
The single ideal amplitude at output `y` for phase `θ` on an
`m`-bit precision register is
qpe_amp m y θ
= (1 / 2^m) · ∑_{x : Fin (2^m)} exp(2πi · x · (θ - y/2^m))
and the Born probability of outcome `y` is
qpe_prob m y θ = ‖qpe_amp m y θ‖².
This file establishes the basic definitions and the easy
"exact-phase" lemma (`θ = y/2^m → qpe_amp = 1`). The geometric-
series closed form and the 4/π² Dirichlet peak bound are future
ticks; this is the foundation they will build on.
Standalone in scope: imports only Mathlib, exports a namespaced
collection of defs/lemmas. No dependency on `FormalRV.SQIRPort.Shor`
or `FormalRV.Framework.QPE` (the circuit-level file).
defqpe_amp
noncomputable def qpe_amp (m y : Nat) (θ : ℝ) : ℂ
*Ideal QPE amplitude** at measurement outcome `y` on an `m`-bit
precision register for true phase `θ ∈ [0, 1)`:
`qpe_amp m y θ = (1 / 2^m) · ∑_{x : Fin (2^m)} exp(2πi · x · (θ - y/2^m))`.
This is the amplitude that would arise from the textbook QPE circuit
applied to a single eigenstate with eigenvalue `exp(2πi · θ)` (after
the inverse-QFT step on the precision register). The full Born-rule
analysis of `QPE_MMI_correct` ultimately bounds `‖qpe_amp m y θ‖²`
below by `4/π²` for the closest output `y` and `|θ - y/2^m| ≤ 1/2^(m+1)`.
defqpe_prob
noncomputable def qpe_prob (m y : Nat) (θ : ℝ) : ℝ
*Ideal QPE outcome probability** `‖qpe_amp m y θ‖²`.
theoremqpe_prob_nonneg
theorem qpe_prob_nonneg (m y : Nat) (θ : ℝ) : 0 ≤ qpe_prob m y θ
The QPE outcome probability is non-negative — trivial since it
is the squared norm of a complex number.
theoremqpe_amp_eq_one_of_exact
theorem qpe_amp_eq_one_of_exact (m y : Nat) (θ : ℝ)
(h : θ = (y : ℝ) / (2^m : ℝ)) :
qpe_amp m y θ = 1*Exact-phase amplitude is 1**: if `θ = y/2^m` exactly (the
measurement outcome `y` corresponds to the true phase exactly), every
exponent in the sum is zero, so the sum is `2^m` complex `1`s and
the prefactor gives `1`.
theoremqpe_prob_eq_one_of_exact
theorem qpe_prob_eq_one_of_exact (m y : Nat) (θ : ℝ)
(h : θ = (y : ℝ) / (2^m : ℝ)) :
qpe_prob m y θ = 1*Exact-phase probability is 1**: direct corollary of the
amplitude lemma.
defqpe_sum
noncomputable def qpe_sum (m y : Nat) (θ : ℝ) : ℂ
*The QPE sum is the inner sum factor (no prefactor)**. Convenient
form for the geometric-series closed form (future work).
theoremqpe_amp_eq_inv_pow_two_mul_sum
theorem qpe_amp_eq_inv_pow_two_mul_sum (m y : Nat) (θ : ℝ) :
qpe_amp m y θ = (1 / (2^m : ℂ)) * qpe_sum m y θRelation between `qpe_amp` and the prefactor-stripped `qpe_sum`.
theoremqpe_sum_eq_sum_phase_diff
theorem qpe_sum_eq_sum_phase_diff (m y : Nat) (θ : ℝ) :
qpe_sum m y θ
= ∑ x : Fin (2^m),
Complex.exp (2 * Real.pi * Complex.I * (x.val : ℂ) *
(((2^m : ℝ) * θ - (y : ℝ)) / (2^m : ℝ) : ℂ))*Phase-difference encapsulation**: the natural variable of the
ideal QPE expression is `φ = 2^m · θ - y` (the un-normalised phase
discrepancy). Each summand exponent factors as `2πi · x · φ / 2^m`.
theoremqpe_sum_summand_eq_pow
theorem qpe_sum_summand_eq_pow (m y : Nat) (θ : ℝ) (x : Fin (2^m)) :
Complex.exp (2 * Real.pi * Complex.I * (x.val : ℂ) *
((θ : ℂ) - (y : ℂ) / (2^m : ℂ)))
= (Complex.exp (2 * Real.pi * Complex.I *
((θ : ℂ) - (y : ℂ) / (2^m : ℂ))))^x.val*The qpe_sum summand factored as `z^x.val`**: rewrites each
exponential `exp(2πi · x · (θ - y/2^m))` as `z^x.val` where
`z = exp(2πi · (θ - y/2^m))`. Foundational step for the geometric-
series closed form.
theoremqpe_sum_eq_sum_pow
theorem qpe_sum_eq_sum_pow (m y : Nat) (θ : ℝ) :
qpe_sum m y θ
= ∑ k ∈ Finset.range (2^m),
(Complex.exp (2 * Real.pi * Complex.I *
((θ : ℂ) - (y : ℂ) / (2^m : ℂ))))^k*qpe_sum as a sum of powers**: combines `qpe_sum_summand_eq_pow`
over all `x : Fin (2^m)` and converts `Fin`-indexed sum to
`Finset.range`-indexed sum. Convenient form to apply mathlib's
`geom_sum_eq` / "sum of 1's" lemmas.
theoremqpe_sum_geom_eq
theorem qpe_sum_geom_eq (m y : Nat) (θ : ℝ)
(hz : Complex.exp (2 * Real.pi * Complex.I *
((θ : ℂ) - (y : ℂ) / (2^m : ℂ))) ≠ 1) :
qpe_sum m y θ
= ((Complex.exp (2 * Real.pi * Complex.I *
((θ : ℂ) - (y : ℂ) / (2^m : ℂ))))^(2^m) - 1) /
((Complex.exp (2 * Real.pi * Complex.I *
((θ : ℂ) - (y : ℂ) / (2^m : ℂ)))) - 1)*Geometric-series closed form for qpe_sum (non-degenerate case)**:
when the per-step phase factor `z = exp(2πi · (θ - y/2^m))` is not 1,
the qpe_sum equals `(z^(2^m) - 1)/(z - 1)` — the standard finite
geometric series.
theoremqpe_sum_eq_card_of_exp_eq_one
theorem qpe_sum_eq_card_of_exp_eq_one (m y : Nat) (θ : ℝ)
(hz : Complex.exp (2 * Real.pi * Complex.I *
((θ : ℂ) - (y : ℂ) / (2^m : ℂ))) = 1) :
qpe_sum m y θ = (2^m : ℂ)*qpe_sum in the degenerate `z = 1` case**: when every summand is
`1`, the sum is simply `2^m`.
defqpe_phase_discrepancy
noncomputable def qpe_phase_discrepancy (m y : Nat) (θ : ℝ) : ℝ
*Phase discrepancy**: the natural variable for the QPE peak bound.
For exact phase (`θ = y/2^m`), `φ = 0` and the QPE outcome is
deterministic; for `|φ| ≤ 1/2`, the analytic peak bound gives
`qpe_prob ≥ 4/π²`.
theoremqpe_denom_norm
theorem qpe_denom_norm (m y : Nat) (θ : ℝ) :
‖Complex.exp (2 * Real.pi * Complex.I *
((θ : ℂ) - (y : ℂ) / (2^m : ℂ))) - 1‖
= 2 * |Real.sin (Real.pi * (θ - (y : ℝ) / (2^m : ℝ)))|*Modulus of the denominator** `|z - 1|`, where
`z = exp(2πi · (θ - y/2^m))`: equals `2 |sin(π · (θ - y/2^m))|`.
Equivalently `= 2 |sin(π · φ / 2^m)|` (see
`qpe_denom_norm_eq_sin_phase_diff`).
theoremqpe_num_norm
theorem qpe_num_norm (m y : Nat) (θ : ℝ) :
‖(Complex.exp (2 * Real.pi * Complex.I *
((θ : ℂ) - (y : ℂ) / (2^m : ℂ))))^(2^m) - 1‖
= 2 * |Real.sin (Real.pi * qpe_phase_discrepancy m y θ)|*Modulus of the numerator** `|z^(2^m) - 1|`, where
`z = exp(2πi · (θ - y/2^m))`: equals `2 |sin(π · φ)|` with
`φ = 2^m · θ - y`. Via `Complex.exp_nat_mul` to absorb the power into
the exponent, then the same identity used in `qpe_denom_norm`.
theoremqpe_denom_norm_eq_sin_phase_diff
theorem qpe_denom_norm_eq_sin_phase_diff (m y : Nat) (θ : ℝ) :
‖Complex.exp (2 * Real.pi * Complex.I *
((θ : ℂ) - (y : ℂ) / (2^m : ℂ))) - 1‖
= 2 * |Real.sin (Real.pi * qpe_phase_discrepancy m y θ / (2^m : ℝ))|*Denominator modulus in phase-discrepancy form**: the same value
expressed via `φ / 2^m` instead of `θ - y/2^m`. Useful for the
`|qpe_sum| = |sin(πφ)| / |sin(πφ/2^m)|` rewrite.
theoremqpe_sum_norm
theorem qpe_sum_norm (m y : Nat) (θ : ℝ)
(hz : Complex.exp (2 * Real.pi * Complex.I *
((θ : ℂ) - (y : ℂ) / (2^m : ℂ))) ≠ 1) :
‖qpe_sum m y θ‖
= |Real.sin (Real.pi * qpe_phase_discrepancy m y θ)| /
|Real.sin (Real.pi * qpe_phase_discrepancy m y θ / (2^m : ℝ))|*Modulus / sine formula for `qpe_sum`**: the headline result of
this section. In the non-degenerate case `z ≠ 1`, the geometric
closed form `qpe_sum = (z^(2^m) - 1)/(z - 1)` has modulus
|qpe_sum m y θ| = |sin(π · φ)| / |sin(π · φ / 2^m)|.
This is the entry point to the standard QPE peak-bound argument: when
`|φ| ≤ 1/2`, the right-hand side is bounded below by `2 · 2^m / π`
(via `|sin x| ≥ 2|x|/π` for `|x| ≤ π/2` in the numerator combined
with `|sin x| ≤ |x|` in the denominator), which after dividing by
the prefactor `1/2^m` and squaring gives `qpe_prob ≥ 4/π²`.
theoremqpe_prob_peak_bound
theorem qpe_prob_peak_bound
(m y : Nat) (θ : ℝ)
(hφ : |qpe_phase_discrepancy m y θ| ≤ 1 / 2) :
qpe_prob m y θ ≥ 4 / Real.pi^2*QPE peak bound** (the headline analytic result of this module):
when the phase discrepancy `φ = 2^m · θ - y` satisfies `|φ| ≤ 1/2`,
the QPE outcome probability at `y` is at least `4/π²`.
defqpe_phase_state
noncomputable def qpe_phase_state (m : Nat) (θ : ℝ) :
Matrix (Fin (2^m)) (Fin 1) ℂ*Ideal QPE phase-register output state**: the `y`-th amplitude is
the ideal QPE amplitude `qpe_amp m y θ`.
theoremqpe_phase_state_apply
theorem qpe_phase_state_apply (m : Nat) (θ : ℝ) (y : Fin (2^m)) :
qpe_phase_state m θ y 0 = qpe_amp m y.val θPer-index evaluation of `qpe_phase_state`.
theoremnormSq_qpe_phase_state_apply
theorem normSq_qpe_phase_state_apply (m : Nat) (θ : ℝ) (y : Fin (2^m)) :
Complex.normSq (qpe_phase_state m θ y 0) = qpe_prob m y.val θThe squared amplitude of `qpe_phase_state m θ` at index `y` is
the ideal QPE outcome probability `qpe_prob m y θ`. Direct consequence
of the definition: `‖qpe_amp m y θ‖² = Complex.normSq (qpe_amp m y θ)
= qpe_prob m y θ`.
theoremnormSq_sum_apply_orth
theorem normSq_sum_apply_orth {n r : Nat}
(β : Fin r → Matrix (Fin n) (Fin 1) ℂ)
(h_orth : ∀ j j' : Fin r,
∑ y : Fin n, starRingEnd ℂ (β j' y 0) * β j y 0
= if j = j' then (1 : ℂ) else 0)
(a : Fin r → ℂ) :
∑ y : Fin n, Complex.normSq (∑ j : Fin r, a j * β j y 0)
= ∑ j : Fin r, Complex.normSq (a j)*Parseval identity for finite orthonormal families**:
Σ_y ‖Σ_j a_j (β_j)_y‖² = Σ_j ‖a_j‖²
when the `β_j` are orthonormal (i.e., `⟨β_j' | β_j⟩ = δ_{j,j'}`).
Used downstream to compute the partial-measurement probability of a
linear combination of eigenstate-tensor terms: cross-terms vanish by
orthonormality, leaving only the diagonal `‖a_j‖²` contribution per
eigenstate.
FormalRV.QPE.QPECorrectness
FormalRV/QPE/QPECorrectness.lean
FormalRV.QPE.QPECorrectness
───────────────────────────
THE semantic-correctness theorems for Quantum Phase Estimation, on an
ABSTRACT (black-box) oracle family `f : Nat → BaseUCom anc`. These are the
QPE-generic results — they make NO reference to modular exponentiation (that
instantiation is Shor's job: `Shor/PostQFT/QPEModmultEigenstate.lean`).
Relocated here (2026-06-10) out of `QFT/IQFTRecursiveArbitrary.lean`, where
they had been developed alongside the inverse-QFT correctness but did not
belong: they are QPE's semantics, not the QFT's. The QFT file now holds only
the inverse-QFT correctness + the SQIRPort↔Framework bridges they depend on,
which this file imports.
THE headline:
• `QPE_var_on_eigenstate_from_real_QFTinv` — MSB-first: for an eigenstate
`ψ` of each oracle `f i` with eigenvalue `qpeEigenvalue m i θ`, running
`QPE_var m anc f` on `|0^m⟩ ⊗ ψ` yields `qpe_phase_state m θ ⊗ ψ`.
• `QPE_var_lsb_on_eigenstate_from_real_QFTinv` — the LSB-first analogue
(eigenvalue `exp(2πi · 2^i · θ)`), the convention Shor uses.
Both are UNCONDITIONAL (no `h_IQFT` hypothesis) — the inverse-QFT matrix
correctness is now proven for arbitrary `n`. The measurement peak bound
`qpe_prob_peak_bound` (≥ 4/π²) lives in `QPEAmplitude.lean`.
theoremreal_QFTinv_layer_lifted_on_kron
theorem real_QFTinv_layer_lifted_on_kron
{m anc : Nat} (hm : 0 < m)
(ψc : Matrix (Fin (2^m)) (Fin 1) ℂ)
(ψd : Matrix (Fin (2^anc)) (Fin 1) ℂ) :
FormalRV.Framework.uc_eval
(map_qubits (fun q => q) (real_QFTinv_layer m)
: FormalRV.Framework.BaseUCom (m + anc))
* kron_vec ψc ψd
= kron_vec (IQFT_matrix m * ψc) ψd*Lifted real-IQFT-layer factors through `kron_vec`.** The
`real_QFTinv_layer m` lifted to `m + anc` qubits acts on `kron_vec ψc ψd`
by applying `IQFT_matrix m` to the control factor `ψc`. Combines
`uc_eval_control_register_circuit_kron_vec` with the arbitrary-n
layer matrix correctness.
theoremreal_QFTinv_layer_on_fourier_weighted_kron_state
theorem real_QFTinv_layer_on_fourier_weighted_kron_state
{m anc : Nat} (hm : 0 < m) (θ : ℝ)
(ψ : Matrix (Fin (2^anc)) (Fin 1) ℂ) :
FormalRV.Framework.uc_eval
(map_qubits (fun q => q) (real_QFTinv_layer m)
: FormalRV.Framework.BaseUCom (m + anc))
*
(((1 : ℂ) / Real.sqrt (2^m : ℝ)) •
∑ x : Fin (2^m),
Complex.exp (2 * Real.pi * Complex.I * (x.val : ℂ) * (θ : ℂ)) •
kron_vec (FormalRV.Framework.basis_vector (2^m) x.val) ψ)
= kron_vec (qpe_phase_state m θ) ψ*HEADLINE: Lifted real-IQFT-layer on Fourier-weighted state.**
The arbitrary-n analogue of `real_QFTinv_on_fourier_weighted_kron_state_from_matrix_correct`,
NOW UNCONDITIONAL: the `h_IQFT` hypothesis is discharged by
`uc_eval_real_QFTinv_layer_eq_IQFT_matrix`.
theoremreal_QPE_layer_on_eigenstate
theorem real_QPE_layer_on_eigenstate
{m anc : Nat} (hmanc : 0 < m + anc) (hm : 0 < m)
(f : Nat → FormalRV.Framework.BaseUCom anc)
(ψ : Matrix (Fin (2^anc)) (Fin 1) ℂ) (θ : ℝ)
(h_wt_all : ∀ i, i < m → UCom.WellTyped anc (f i))
(h_eig_data : ∀ i, i < m →
FormalRV.Framework.uc_eval (f i) * ψ =
qpeEigenvalue m i θ • ψ) :
FormalRV.Framework.uc_eval (real_QPE_layer m anc f)
* kron_vec (FormalRV.Framework.kron_zeros m) ψ
= kron_vec (qpe_phase_state m θ) ψ*HEADLINE: Unconditional real-QPE-layer single-eigenstate theorem.**
Given a data-register `ψ` that is a QPE eigenstate (i.e., each oracle
`f i` acts on `ψ` as `qpeEigenvalue m i θ`), the `real_QPE_layer m anc f`
applied to `|0^m⟩ ⊗ ψ` produces `kron_vec (qpe_phase_state m θ) ψ`.
UNLIKE `real_QPE_on_eigenstate_from_IQFT_correct`, this theorem has
NO `h_IQFT` hypothesis — the matrix correctness is now built into
`real_QFTinv_layer`'s definition via
`uc_eval_real_QFTinv_layer_eq_IQFT_matrix`.
theoremQFTinv_on_fourier_weighted_kron_state
theorem QFTinv_on_fourier_weighted_kron_state
{m anc : Nat} (hm : 0 < m) (θ : ℝ)
(ψ : Matrix (Fin (2^anc)) (Fin 1) ℂ) :
FormalRV.Framework.uc_eval
(FormalRV.Framework.BaseUCom.QFTinv m
: FormalRV.Framework.BaseUCom (m + anc))
*
(((1 : ℂ) / Real.sqrt (2^m : ℝ)) •
∑ x : Fin (2^m),
Complex.exp (2 * Real.pi * Complex.I * (x.val : ℂ) * (θ : ℂ)) •
kron_vec (FormalRV.Framework.basis_vector (2^m) x.val) ψ)
= kron_vec (qpe_phase_state m θ) ψ*HEADLINE: Framework `QFTinv` (lifted) on Fourier-weighted kron state.**
Direct analogue of `real_QFTinv_layer_on_fourier_weighted_kron_state`,
stated for the framework `QFTinv m : BaseUCom (m + anc)` (rather than
the SQIRPort-lifted version). Proof: unfold `QFTinv`; apply the
polymorphic-lift bridge to convert to the dim-`m` version via
`map_qubits id`; apply the SQIRPort bridge to convert to
`SQIRPort.real_QFTinv_layer`; apply the existing fourier-weighted theorem.
theoremQPE_var_on_eigenstate_from_real_QFTinv
theorem QPE_var_on_eigenstate_from_real_QFTinv
{m anc : Nat} (hmanc : 0 < m + anc) (hm : 0 < m)
(f : Nat → FormalRV.Framework.BaseUCom anc)
(ψ : Matrix (Fin (2^anc)) (Fin 1) ℂ) (θ : ℝ)
(h_wt_all : ∀ i, i < m → UCom.WellTyped anc (f i))
(h_eig_data : ∀ i, i < m →
FormalRV.Framework.uc_eval (f i) * ψ =
qpeEigenvalue m i θ • ψ) :
FormalRV.Framework.uc_eval (FormalRV.SQIRPort.QPE_var m anc f)
* kron_vec (FormalRV.Framework.kron_zeros m) ψ
= kron_vec (qpe_phase_state m θ) ψ*HEADLINE: `QPE_var` on QPE eigenstate (real IQFT).** The first
fully-unconditional QPE eigenstate theorem for the framework
`QPE_var` (which underlies `Shor_final_state`). Given a data-register
eigenstate `ψ` with the standard QPE eigenvalue data on each oracle,
`QPE_var m anc f` applied to `|0^m⟩ ⊗ ψ` yields `qpe_phase_state m θ ⊗ ψ`.
Proof: unfold `QPE_var` and `BaseUCom.QPE`; chain through
`QPE_pre_QFT_on_eigenstate_fourier_form` (existing); finish with
`QFTinv_on_fourier_weighted_kron_state`.
theoremqpeEigenvalue_reverse_index_eq_lsb
theorem qpeEigenvalue_reverse_index_eq_lsb
(m i : Nat) (_hi : i < m) (θ : ℝ) :
qpeEigenvalue m (m - 1 - i) θ
= Complex.exp (((2 * Real.pi * ((2^i : Nat) : ℝ) * θ : ℝ) : ℂ) * Complex.I)*Eigenvalue bridge**: the framework's MSB-first `qpeEigenvalue m j θ`
at reversed index `j = m - 1 - i` equals the natural LSB-first eigenvalue
`exp(2π·I · 2^i · θ)`. Substitutes `m - (m-1-i) - 1 = i` to reduce the
weight in qpeEigenvalue from `2^(m-(m-1-i)-1) = 2^i`.
theoremQPE_var_lsb_on_eigenstate_from_real_QFTinv
theorem QPE_var_lsb_on_eigenstate_from_real_QFTinv
{m anc : Nat} (hmanc : 0 < m + anc) (hm : 0 < m)
(f : Nat → FormalRV.Framework.BaseUCom anc)
(ψ : Matrix (Fin (2^anc)) (Fin 1) ℂ) (θ : ℝ)
(h_wt_all : ∀ i, i < m → UCom.WellTyped anc (f i))
(h_eig_lsb : ∀ i, i < m →
FormalRV.Framework.uc_eval (f i) * ψ =
Complex.exp (((2 * Real.pi * ((2^i : Nat) : ℝ) * θ : ℝ) : ℂ) * Complex.I) • ψ) :
FormalRV.Framework.uc_eval (QPE_var_lsb m anc f)
* kron_vec (FormalRV.Framework.kron_zeros m) ψ
= kron_vec (qpe_phase_state m θ) ψ*HEADLINE: LSB-compatible QPE eigenstate theorem.** The natural
LSB-first analogue of `QPE_var_on_eigenstate_from_real_QFTinv`. Given a
data-register eigenstate `ψ` with LSB-first eigenvalue weights
(`uc_eval (f i) * ψ = exp(2π·I · 2^i · θ) • ψ` for each oracle index `i`),
the `QPE_var_lsb m anc f` circuit applied to `|0^m⟩ ⊗ ψ` produces
`kron_vec (qpe_phase_state m θ) ψ`.
Proof: unfold `QPE_var_lsb`; apply `QPE_var_on_eigenstate_from_real_QFTinv`
to the reversed family `fun j => f (revIndex m j)`; discharge the
well-typedness obligation via `revIndex_lt` + `h_wt_all`; discharge the
eigenvalue obligation by chaining `h_eig_lsb` at index `revIndex m j`
with the index-arithmetic identity `m - 1 - (m-1-j) = j` (equivalently
`m - (m-1-j) - 1 = j`, so the qpeEigenvalue weight `2^(m-(m-1-j)-1) = 2^j`
matches the LSB-first weight at the reversed index).
theoremqpe_on_eigenstate_correct
theorem qpe_on_eigenstate_correct
{m anc : Nat} (hmanc : 0 < m + anc) (hm : 0 < m)
(f : Nat → FormalRV.Framework.BaseUCom anc)
(ψ : Matrix (Fin (2^anc)) (Fin 1) ℂ) (θ : ℝ)
(h_wt_all : ∀ i, i < m → UCom.WellTyped anc (f i))
(h_eig_lsb : ∀ i, i < m →
FormalRV.Framework.uc_eval (f i) * ψ =
Complex.exp (((2 * Real.pi * ((2^i : Nat) : ℝ) * θ : ℝ) : ℂ) * Complex.I) • ψ) :
FormalRV.Framework.uc_eval (QPE_var_lsb m anc f)
* kron_vec (FormalRV.Framework.kron_zeros m) ψ
= kron_vec (qpe_phase_state m θ) ψ*QPE — eigenstate correctness (THE headline, LSB-first).** Running the
QPE circuit `QPE_var_lsb m anc f` on `|0^m⟩ ⊗ ψ`, where `ψ` is a common
eigenstate of the abstract oracle family with LSB-first eigenvalues
`exp(2πi · 2^i · θ)`, produces exactly `qpe_phase_state m θ ⊗ ψ` — the ideal
phase-register state. The oracle `f` is a BLACK BOX (any `WellTyped` family
with the eigenvalue property); modular exponentiation is just one instance.
FormalRV.QPE.QPECount
FormalRV/QPE/QPECount.lean
FormalRV.QPE.QPECount
─────────────────────
CLOSED-FORM, ANCHORED resource counts for the QPE circuit, with the oracle as
a BLACK BOX: the independent `Resource` counters applied to THE actual
`BaseUCom` syntax tree `QPE k n c`, proven equal to a closed form that is
parametric in the oracle family's own counts. QPE adds NOTHING hidden on top
of its oracle calls: the count theorem exhibits exactly
CNOTs(QPE k n c) = Σᵢ (2·1q(cᵢ) + 6·CNOT(cᵢ)) [the controlled oracle calls]
+ 3·⌊k/2⌋ + k·(k−1) [the inverse-QFT basis]
(a controlled 1-qubit gate costs 2 CNOTs + 4 one-qubit gates; a controlled
CNOT is a Toffoli = 6 CNOTs + 9 one-qubit gates — `Resource.UComCombinators`).
The modular-exponentiation instantiation's cost is the INSTANTIATION's
business; it enters only through `oneQCountU (f i)` / `cnotCountU (f i)`.
Headlines:
• `cnotCountU_QPE` / `oneQCountU_QPE` — the framework `QPE k n c`
• `cnotCountU_QPE_var_lsb` — the Shor-facing wrapper (counts
invariant under the `map_qubits` lift and the LSB index reversal)
• `widthU_QPE_decomp` + `widthU_QFTinv` — the space decomposition
• `qpe_verified_with_resources` — THE TRIPLE: black-box semantic
correctness AND the CNOT count, about the SAME syntactic object.
theoremoneQCountU_map_qubits
theorem oneQCountU_map_qubits {dim dim' : Nat} (g : Nat → Nat) (c : BaseUCom dim) :
oneQCountU (FormalRV.SQIRPort.map_qubits g c : BaseUCom dim') = oneQCountU ctheoremcnotCountU_map_qubits
theorem cnotCountU_map_qubits {dim dim' : Nat} (g : Nat → Nat) (c : BaseUCom dim) :
cnotCountU (FormalRV.SQIRPort.map_qubits g c : BaseUCom dim') = cnotCountU ctheoremcnotCountU_controlled_powers
theorem cnotCountU_controlled_powers {dim : Nat} (c : Nat → BaseUCom dim) (k : Nat) :
cnotCountU (controlled_powers c k)
= ∑ i ∈ Finset.range k, (2 * oneQCountU (c i) + 6 * cnotCountU (c i))CNOTs of the controlled-powers ladder: each controlled oracle call costs
`2·(its one-qubit gates) + 6·(its CNOTs)`.
theoremoneQCountU_controlled_powers
theorem oneQCountU_controlled_powers {dim : Nat} (c : Nat → BaseUCom dim) (k : Nat) :
oneQCountU (controlled_powers c k)
= (∑ i ∈ Finset.range k, (4 * oneQCountU (c i) + 9 * cnotCountU (c i))) + 1One-qubit gates of the controlled-powers ladder (`+1` for the structural
`SKIP` at the base of `npar`).
theoremcnotCountU_QPE
theorem cnotCountU_QPE {k n : Nat} (c : Nat → BaseUCom (k + n)) :
cnotCountU (QPE k n c)
= (∑ i ∈ Finset.range k, (2 * oneQCountU (c i) + 6 * cnotCountU (c i)))
+ (3 * (k / 2) + k * (k - 1))*QPE CNOT count (THE headline, time).** Exactly the controlled-oracle
calls plus the inverse-QFT measurement basis — nothing hidden.
theoremoneQCountU_QPE
theorem oneQCountU_QPE {k n : Nat} (c : Nat → BaseUCom (k + n)) :
oneQCountU (QPE k n c)
= (∑ i ∈ Finset.range k, (4 * oneQCountU (c i) + 9 * cnotCountU (c i)))
+ (3 * (k * (k - 1) / 2) + 2 * k + 4)*QPE one-qubit-gate count (time).** The `k` Hadamards, the controlled
oracle calls, the inverse-QFT rotations, and the structural `SKIP`s.
theoremwidthU_QPE_decomp
theorem widthU_QPE_decomp {k n : Nat} (c : Nat → BaseUCom (k + n)) :
widthU (QPE k n c)
= max (widthU (npar_H k : BaseUCom (k + n)))
(max (widthU (controlled_powers c k)) (widthU (QFTinv k : BaseUCom (k + n))))*QPE width decomposition (space).** The register is the max of the three
stages' footprints — with the oracle's footprint left as the black box it is.
theoremcnotCountU_QPE_var
theorem cnotCountU_QPE_var (m anc : Nat) (f : Nat → BaseUCom anc) :
cnotCountU (FormalRV.SQIRPort.QPE_var m anc f)
= (∑ i ∈ Finset.range m, (2 * oneQCountU (f i) + 6 * cnotCountU (f i)))
+ (3 * (m / 2) + m * (m - 1))CNOTs of `QPE_var`: the `map_qubits` lift does not change any count.
theoremcnotCountU_QPE_var_lsb
theorem cnotCountU_QPE_var_lsb (m anc : Nat) (f : Nat → BaseUCom anc) :
cnotCountU (FormalRV.SQIRPort.QPE_var_lsb m anc f)
= (∑ i ∈ Finset.range m, (2 * oneQCountU (f i) + 6 * cnotCountU (f i)))
+ (3 * (m / 2) + m * (m - 1))CNOTs of `QPE_var_lsb`: the LSB index reversal is a permutation of the
oracle family, so the summed count is unchanged (`Finset.sum_range_reflect`).
theoremqpe_verified_with_resources
theorem qpe_verified_with_resources
{m anc : Nat} (hmanc : 0 < m + anc) (hm : 0 < m)
(f : Nat → FormalRV.Framework.BaseUCom anc)
(ψ : Matrix (Fin (2^anc)) (Fin 1) ℂ) (θ : ℝ)
(h_wt_all : ∀ i, i < m → UCom.WellTyped anc (f i))
(h_eig_lsb : ∀ i, i < m →
FormalRV.Framework.uc_eval (f i) * ψ =
Complex.exp (((2 * Real.pi * ((2^i : Nat) : ℝ) * θ : ℝ) : ℂ) * Complex.I) • ψ) :
(FormalRV.Framework.uc_eval (QPE_var_lsb m anc f)
* kron_vec (FormalRV.Framework.kron_zeros m) ψ
= kron_vec (qpe_phase_state m θ) ψ)
∧ cnotCountU (QPE_var_lsb m anc f)*QPE, verified with resources (black-box oracle).** For ANY eigenstate-
bearing oracle family `f`, the single syntactic object `QPE_var_lsb m anc f` is
simultaneously:
1. **semantically correct** — it maps `|0^m⟩ ⊗ ψ` to `qpe_phase_state m θ ⊗ ψ`;
2. **time-counted** — the independent CNOT counter walks its tree to exactly
the controlled-oracle calls plus the inverse-QFT basis
`3·⌊m/2⌋ + m·(m−1)`, with the oracle's own counts left as the black box
they are.
The counters live in `Resource/` and import only the IR — nothing here can
influence what they return.
FormalRV.QPE.QPEDef
FormalRV/QPE/QPEDef.lean
FormalRV.QPE.QPEDef
───────────────────
THE definition of Quantum Phase Estimation (QPE), as a concrete `BaseUCom`
unitary circuit over an ABSTRACT (black-box) oracle. **Definitions only — no
proofs.**
THE circuit is `Framework.BaseUCom.QPE k n c` (QPE.lean): on `k + n` qubits,
QPE k n c = npar_H k ; controlled_powers c k ; QFTinv k
i.e. (1) Hadamards on the `k` measurement qubits, (2) the controlled-powers
ladder of the oracle, and (3) the inverse QFT on the measurement register.
## The black box
`c : Nat → BaseUCom (k+n)` is a BLACK-BOX oracle family: `c i` is "apply the
unitary `U` to the power `2^i`, controlled on measurement qubit `i`". QPE
knows `U` ONLY through this abstract family and an eigenvalue hypothesis — it
does NOT know how `U` is built. Modular exponentiation (`U = ×a mod N`) is one
instantiation, supplied by Shor; QPE itself is oracle-generic. The Shor-facing
wrappers `QPE_var m anc f` / `QPE_var_lsb m anc f` (in
`Shor/MainAlgorithm/.../QuantumPrimitives.lean`) lift a data-register family
`f : Nat → BaseUCom anc` into this shape via `map_qubits (· + m)`.
## The ideal output and the eigenvalue hypothesis
On a data-register eigenstate `ψ` of `U` with phase `θ` (`U|ψ⟩ = e^{2πiθ}|ψ⟩`),
QPE produces `qpe_phase_state m θ ⊗ ψ` (QPEAmplitude.lean), the phase-register
state peaked at the `m`-bit approximation of `θ`. The per-oracle eigenvalue
weight is `qpeEigenvalue m i θ = exp(2πi · 2^(m-i-1) · θ)` (MSB-first;
PhaseKickback.lean), or `exp(2πi · 2^i · θ)` LSB-first.
Where to look next:
• Semantic correctness (THE main theorem) : `QPECorrectness.lean`
• Resource / measurement-basis compilation : `QPEResource.lean`
• Worked example + QASM emission : `QPEExample.lean`
• Heavy machinery (phase kickback, cascade): `PhaseKickback.lean`,
`ControlledGates.lean`; amplitude/peak analysis: `QPEAmplitude.lean`.
Refs: Nielsen–Chuang §5.2 (phase estimation); SQIR `QPEGeneral.v`.
example(example)
example (k n : Nat) (c : Nat → BaseUCom (k + n)) :
QPE k n c
= UCom.seq (npar_H k) (UCom.seq (controlled_powers c k) (QFTinv k))Smoke: THE QPE circuit is exactly `npar_H k ; controlled_powers c k ; QFTinv k`.
example(example)
example (d k : Nat) (c : Nat → BaseUCom d) :
controlled_powers c (k + 1)
= UCom.seq (controlled_powers c k) (control k (c k))Smoke: the controlled-powers ladder is `control i (c i)` over `i ∈ [0,k)`
(the black-box oracle is applied once per measurement qubit).
FormalRV.QPE.QPEExample
FormalRV/QPE/QPEExample.lean
FormalRV.QPE.QPEExample
───────────────────────
A worked example for QPE + its `UGadget` descriptor for the uniform `BaseUCom`
QASM emitter (`Codegen.UComQasm`), the same framework the QFT and arithmetic
gadgets emit through.
This file contains `#eval` demos, so it is kept OFF the default build path
(not imported by the `QPE` umbrella). Build / run on demand:
lake build FormalRV.QPE.QPEExample
## The black box, made concrete
QPE's oracle is a BLACK BOX in general (`QPECorrectness.qpe_on_eigenstate_correct`
holds for any eigenstate-bearing family). To EMIT a runnable circuit we pick
the canonical concrete oracle: the single-qubit PHASE gate `U = u1(2πθ)` on one
ancilla, whose eigenstate is `|1⟩` with eigenvalue `e^{2πiθ}`. Then
`c i = control i (U^{2^i}) = cu1(2π·2^i·θ) q[i],q[ancilla]`, and the QPE circuit
on `k` measurement qubits + 1 ancilla is
h q[0..k-1] ; cu1(2π·2^i·θ) q[i],q[k] (i<k) ; inverse-QFT q[0..k-1]
estimating the `k`-bit value of `θ`. For `θ = 1/2^k` the peak is at `y = 1`.
defpiFrac
def piFrac (num : Int) (den : Nat) : String
Render `num·π/den` as OpenQASM angle text, reduced by `gcd`.
defiqftPrefixLines
def iqftPrefixLines (k : Nat) : List String
The inverse QFT on the measurement register `q[0..k-1]` (the QPE measurement
basis): bit-reversal `swap`s, then the `cu1`/`h` phase-ladder countdown. Same
gates as `IQFT k`, acting only on the first `k` qubits.
defqpeBodyLines
def qpeBodyLines (k p q : Nat) : List String
The phase-oracle QPE body on `k` measurement qubits + ancilla `q[k]`,
estimating `θ = p / 2^q`: H-layer, the `cu1(2π·2^i·θ)` controlled-power ladder,
then the inverse QFT on the measurement register.
defQPEPhaseGadget
def QPEPhaseGadget : UGadget
Phase-oracle QPE as a uniform `UGadget` (estimating `θ = 1/2^k`).
defqpe3IoJson
def qpe3IoJson : String
Wire names + INPUT/OUTPUT legend for the 3+1-qubit phase-oracle QPE.
FormalRV.QPE.QPEResource
FormalRV/QPE/QPEResource.lean
FormalRV.QPE.QPEResource
────────────────────────
THE "resource" account for Quantum Phase Estimation.
QPE adds only TWO things on top of its `k` black-box controlled-oracle calls:
1. `k` Hadamards on the measurement register (`npar_H k`), and
2. one `k`-qubit INVERSE QFT as the measurement basis (`QFTinv k`).
The oracle (`controlled_powers c k`) is a BLACK BOX — its cost belongs to the
instantiation (for Shor, the modular-exponentiation ladder, which dominates).
So the QPE-specific resource is exactly the measurement-basis cost, which is
the inverse-QFT cost: continuous controlled phases, hence governed by
Clifford+T COMPILATION (the approximate / banded QFT), not an exact T-count.
Headlines (re-surfaced from `QFT/IQFTResource.lean`, now phrased about QPE's
measurement basis):
• `qpe_measurement_basis_isCliffordT` — the banded measurement basis is
exactly Clifford+T (cutoff `c ≤ 2`).
• `qpe_measurement_basis_error_budget` — its derived `≤ 2π/2^c` error budget.
• `qpe_circuit_resource_decomp` — the QPE unitary factors as
`QFTinv k · controlled_powers c k · npar_H k` (so the only QPE overhead is
the H-layer + the inverse QFT).
EXACT GATE/QUBIT COUNTS (the `Resource/` counters walking THE circuit's
syntax tree, with the oracle a BLACK BOX — see `QPECount.lean`, imported below):
• `Resource.cnotCountU_QPE` / `oneQCountU_QPE` — QPE's counts = the
controlled-oracle calls (parametric in the oracle's own counts) + the
inverse-QFT basis `3·⌊k/2⌋ + k·(k−1)` (TIME)
• `Resource.cnotCountU_QPE_var_lsb` — same through the Shor-facing
wrapper (counts invariant under lifting + LSB reversal)
• `Resource.widthU_QPE_decomp` — the space decomposition
• `SQIRPort.qpe_verified_with_resources` — black-box semantics + count,
about the SAME syntactic object.
theoremqpe_measurement_basis_isCliffordT
theorem qpe_measurement_basis_isCliffordT {dim : Nat} (c : Nat) (hc : c ≤ 2)
(rs : List PhaseRot) :
FormalRV.Framework.CliffordTRotations.IsCliffordT
(compileLadder c rs : BaseUCom dim)*QPE measurement basis is Clifford+T (THE gate-set resource).** The QPE
measurement-basis inverse QFT, compiled at cutoff `c ≤ 2` (banded), emits only
Clifford+T gates.
theoremqpe_measurement_basis_error_budget
theorem qpe_measurement_basis_error_budget (c n : ℕ) (hcn : c ≤ n) :
∑ m ∈ Finset.Ico c n, (Real.pi / 2 ^ m) ≤ 2 * Real.pi / 2 ^ c*QPE measurement basis error budget (THE approximation resource).** The
total cost of the cutoff-`c` measurement-basis compilation is the derived
geometric tail `≤ 2π/2^c`.
theoremqpe_circuit_resource_decomp
theorem qpe_circuit_resource_decomp {k n : Nat} (c : Nat → BaseUCom (k + n)) :
uc_eval (QPE k n c)
= uc_eval (QFTinv k) * uc_eval (controlled_powers c k) * uc_eval (npar_H k)*QPE resource decomposition.** The QPE unitary is the right-to-left
product `QFTinv k · controlled_powers c k · npar_H k`: beyond the `k`
black-box controlled-oracle calls, the only overhead is the `k`-Hadamard
preparation and the `k`-qubit inverse QFT (the measurement basis).