QFT 250 declarations in 17 modules
FormalRV.QFT.AQFTCompile
FormalRV/QFT/AQFTCompile.lean
FormalRV.QFT.AQFTCompile — an ACTUAL Clifford+T compiler for the
inverse-QFT phase ladder of Shor's QPE, with derived approximation
error. No existence axiom: `compileLadder` is a real circuit
transformation, proven to emit only Clifford+T gates, and its total
approximation error is the closed-form geometric tail
(`ApproxQFT.aqft_ladder_error_budget`).
## What this is
The inverse QFT (`FormalRV.Framework.BaseUCom.QFTinv`) is a ladder of
controlled rotations `controlled_Rz q t (−π/2^m)` plus Hadamards. The
`controlled_Rz` decomposition uses the half-angle `R_z(∓π/2^{m+1})`, so
a ladder rotation is exactly Clifford+T iff `m ≤ 1`
(`m=0 → S†/S = CZ`, `m=1 → T†/T = controlled-S†`). The approximate
("banded") QFT keeps `m < cutoff` and DROPS the rest; with `cutoff ≤ 2`
the output is exactly Clifford+T (`compileLadder_isCliffordT`), and the
dropped rotations contribute the derived error budget.
This compiles the QFT layer; the modular-exponentiation layer of QPE is
already exact Clifford+T, so together they compile QPE's circuit to
Clifford+T up to the stated, derived error.
structurePhaseRot
structure PhaseRot
One inverse-QFT phase-ladder rotation: control `q`, target `t`, depth
`m` (the rotation angle is `−π/2^m`).
defcompileRot
noncomputable def compileRot {dim : Nat} (c : Nat) (r : PhaseRot) : BaseUCom dim*Compile one rotation under cutoff `c`.** Keep the (Clifford+T)
`controlled_Rz` when `m < c`; otherwise DROP it (`SKIP`). This is the
approximate-QFT decision, applied gate by gate.
defcompileLadder
noncomputable def compileLadder {dim : Nat} (c : Nat) (rs : List PhaseRot) :
BaseUCom dim*The compiled approximate inverse-QFT phase ladder.** Sequences the
compiled rotations. The actual compiler output.
theoremskip_isCliffordT
theorem skip_isCliffordT {dim : Nat} : IsCliffordT (SKIP : BaseUCom dim)theoremcontrolled_Rz_isCliffordT
theorem controlled_Rz_isCliffordT {dim : Nat} (q t : Nat) (lam : ℝ)
(hpos : (U_Rz (lam / 2) = U_H ∨ U_Rz (lam / 2) = U_S ∨ U_Rz (lam / 2) = U_T
∨ U_Rz (lam / 2) = U_SDAG ∨ U_Rz (lam / 2) = U_TDAG
∨ U_Rz (lam / 2) = U_I))
(hneg : (U_Rz (-(lam / 2)) = U_H ∨ U_Rz (-(lam / 2)) = U_S
∨ U_Rz (-(lam / 2)) = U_T ∨ U_Rz (-(lam / 2)) = U_SDAG
∨ U_Rz (-(lam / 2)) = U_TDAG ∨ U_Rz (-(lam / 2)) = U_I)) :
IsCliffordT (BaseUCom.controlled_Rz q t lam : BaseUCom dim)`controlled_Rz q t lam` is Clifford+T whenever its half-angle gates
`R_z(lam/2)` and `R_z(−lam/2)` are named Clifford+T gates.
theoremcontrolled_Rz_isCliffordT_depth0
theorem controlled_Rz_isCliffordT_depth0 {dim : Nat} (q t : Nat) :
IsCliffordT (BaseUCom.controlled_Rz q t (-(Real.pi / 2 ^ 0)) : BaseUCom dim)Depth-0 ladder rotation (`−π`, i.e. CZ): half-angles are `S†, S` —
Clifford.
theoremcontrolled_Rz_isCliffordT_depth1
theorem controlled_Rz_isCliffordT_depth1 {dim : Nat} (q t : Nat) :
IsCliffordT (BaseUCom.controlled_Rz q t (-(Real.pi / 2 ^ 1)) : BaseUCom dim)Depth-1 ladder rotation (`−π/2`, controlled-`S†`): half-angles are
`T†, T` — Clifford+T.
theoremcompileLadder_isCliffordT
theorem compileLadder_isCliffordT {dim : Nat} (c : Nat) (hc : c ≤ 2)
(rs : List PhaseRot) :
IsCliffordT (compileLadder c rs : BaseUCom dim)*The compiled ladder is exactly Clifford+T** (for cutoff `c ≤ 2`).
Every kept rotation has depth `< c ≤ 2`, hence depth `0` or `1`, hence
Clifford+T; every dropped rotation is `SKIP`.
theoremcompileLadder_error_budget
theorem compileLadder_error_budget (c n : ℕ) (hcn : c ≤ n) :
∑ m ∈ Finset.Ico c n, (Real.pi / 2 ^ m) ≤ 2 * Real.pi / 2 ^ c*Compiler error budget.** The total approximation error of the
cutoff-`c` AQFT ladder — summed over every dropped depth `c ≤ m < n`
of its derived per-rotation drop cost — is at most `2π/2^c`.
FormalRV.QFT.AQFTCompileSemantics
FormalRV/QFT/AQFTCompileSemantics.lean
FormalRV.QFT.AQFTCompileSemantics — SEMANTIC correctness of the AQFT
compiler (the linear-algebra proof, not just the Clifford+T gate-set).
`compileLadder` is diagonal in the computational basis, so its action is
fully characterised by a per-basis-state scalar. We prove, by induction
on the rotation list, that `compileLadder c rs` multiplies the amplitude
of basis state `f` by the PRODUCT of the kept controlled-phase scalars
(each `e^{-iπ/2^m}` when both control and target bits are set), with
DROPPED rotations contributing `1` (because `SKIP = id`). This certifies
that the compiler actually computes the banded inverse-QFT — its
semantics, not only its gate count or gate set.
Reuses the repo's already-proven controlled-phase semantics
(`controlled_Rz_acts_on_basis_correct`) via a `rfl` bridge between the
Framework `BaseUCom.controlled_Rz` (which `compileRot` emits) and the
SQIRPort `controlled_Rz` the lemma is stated about.
## Honesty boundary
Stated on `f_to_vec` computational-basis states only (the ladder is
diagonal, so this fully characterises it); NOT lifted to a full matrix
equality, and this is the BANDED action — its deviation from the exact
QFT is the separate `compileLadder_error_budget`.
Machine-validated; kernel-clean ([propext, Classical.choice, Quot.sound]).
theoremcontrolled_Rz_bridge
theorem controlled_Rz_bridge {dim : Nat} (q t : Nat) (lam : ℝ) :
(FormalRV.Framework.BaseUCom.controlled_Rz q t lam
: FormalRV.Framework.BaseUCom dim)
= FormalRV.SQIRPort.controlled_Rz q t lamBridge: the Framework `controlled_Rz` that `compileRot` emits is defeq
to the SQIRPort `controlled_Rz` that `controlled_Rz_acts_on_basis_correct`
is stated about. Closed by `rfl`.
defrotScalar
noncomputable def rotScalar (c : Nat) (r : PhaseRot) (f : Nat → Bool) : ℂ
The per-basis-state scalar of one compiled rotation: the kept
controlled-phase `e^{-iπ/2^m}` exactly when the rotation survives the
cutoff (`m < c`) AND both control/target bits are set; otherwise `1`.
defRotWF
def RotWF (dim : Nat) (r : PhaseRot) : Prop
Well-formedness of one rotation against the register dimension.
theoremcompileRot_acts_on_basis
theorem compileRot_acts_on_basis {dim : Nat} (c : Nat) (r : PhaseRot) (f : Nat → Bool)
(hpos : 0 < dim) (hq : r.q < dim) (ht : r.t < dim) (hqt : r.q ≠ r.t) :
uc_eval (compileRot c r : BaseUCom dim) * f_to_vec dim f
= rotScalar c r f • f_to_vec dim f*One compiled rotation acts as its controlled-phase scalar** on a
basis state (kept → controlled-phase, dropped → identity).
defladderScalar
noncomputable def ladderScalar (c : Nat) (rs : List PhaseRot) (f : Nat → Bool) : ℂ
The product of the per-rotation scalars over the whole ladder.
theoremcompileLadder_acts_on_basis
theorem compileLadder_acts_on_basis {dim : Nat} (c : Nat) (rs : List PhaseRot) (f : Nat → Bool)
(hpos : 0 < dim) (hwf : ∀ r ∈ rs, RotWF dim r) :
uc_eval (compileLadder c rs : BaseUCom dim) * f_to_vec dim f
= ladderScalar c rs f • f_to_vec dim f*The compiled ladder acts as the product of its kept controlled-phases**
on every computational-basis state — the compiler's semantic correctness,
proved by induction over the rotation list.
theoremcompileLadder_two_acts_on_basis
theorem compileLadder_two_acts_on_basis {dim : Nat} (c : Nat) (r1 r2 : PhaseRot)
(f : Nat → Bool) (hpos : 0 < dim) (hwf1 : RotWF dim r1) (hwf2 : RotWF dim r2) :
uc_eval (compileLadder c [r1, r2] : BaseUCom dim) * f_to_vec dim f
= (rotScalar c r1 f * rotScalar c r2 f) • f_to_vec dim fSmoke instance: a 2-rotation banded ladder acts as the product of the
two per-rotation scalars.
FormalRV.QFT.IQFTCircuitCorrectness
FormalRV/QFT/IQFTCircuitCorrectness.lean
(no documented top-level declarations)
FormalRV.QFT.IQFTCircuitCorrectness.CircuitActionColumns
FormalRV/QFT/IQFTCircuitCorrectness/CircuitActionColumns.lean
IQFTCircuitCorrectness — Part2 (re-export shim part; same namespace, opens de-duplicated).
lemmaf_to_vec_two_eq
lemma f_to_vec_two_eq (f : Nat → Bool) :
f_to_vec 2 f = FormalRV.Framework.basis_vector 4
((if f 0 then 2 else 0) + (if f 1 then 1 else 0))`f_to_vec 2 f` in terms of `basis_vector 4` and the values of `f`
at bits 0 and 1. Recall that bit 0 is MSB (weight 2), bit 1 is LSB
(weight 1) in the framework's `funbool_to_nat` convention.
lemmasqrt_two_half_sq
lemma sqrt_two_half_sq :
(Real.sqrt 2 / 2 : ℂ) * (Real.sqrt 2 / 2 : ℂ) = (1/2 : ℂ)`(√2/2)² = 1/2` over `ℂ`.
lemmaexp_neg_pi_I
lemma exp_neg_pi_I : Complex.exp (-((Real.pi : ℂ) * Complex.I)) = -1
`exp(-(π·I)) = -1`.
lemmaexp_neg_two_pi_I
lemma exp_neg_two_pi_I : Complex.exp (-(2 * (Real.pi : ℂ) * Complex.I)) = 1
`exp(-(2π·I)) = 1`.
lemmaexp_neg_three_pi_I
lemma exp_neg_three_pi_I : Complex.exp (-(3 * (Real.pi : ℂ) * Complex.I)) = -1
`exp(-(3π·I)) = -1`.
lemmaexp_neg_three_pi_half_I
lemma exp_neg_three_pi_half_I :
Complex.exp (-(3 * (Real.pi : ℂ) / 2 * Complex.I))
= -Complex.exp (-((Real.pi : ℂ) / 2 * Complex.I))`exp(-(3π/2 · I)) = -exp(-(π/2 · I))`.
lemmaexp_neg_nine_pi_half_I
lemma exp_neg_nine_pi_half_I :
Complex.exp (-(9 * (Real.pi : ℂ) / 2 * Complex.I))
= Complex.exp (-((Real.pi : ℂ) / 2 * Complex.I))`exp(-(9π/2 · I)) = exp(-(π/2 · I))` — since `-9π/2 = -π/2 - 4π` and
`exp(-4π·I) = 1`.
lemmasqrt_two_sq_complex
lemma sqrt_two_sq_complex : ((Real.sqrt 2 : ℂ))^2 = (2 : ℂ)
`(√2 : ℂ)² = 2`.
lemmasqrt_two_half_smul_sandwich
lemma sqrt_two_half_smul_sandwich (e : ℂ) :
(Real.sqrt 2 / 2 : ℂ) * (e * (Real.sqrt 2 / 2 : ℂ)) = (1/2 : ℂ) * eConsolidate `(√2/2) * (e * (√2/2))` into `(1/2) * e`.
theoremreal_QFTinv2_candidate_on_basis_zero
theorem real_QFTinv2_candidate_on_basis_zero :
FormalRV.Framework.uc_eval real_QFTinv2_candidate *
FormalRV.Framework.basis_vector 4 0
= IQFT_matrix 2 * FormalRV.Framework.basis_vector 4 0*Column 0: candidate on `|0⟩`.** Direct chain via `f_to_vec_SWAP`,
`f_to_vec_H_uc_eval`, `controlled_Rz_acts_on_basis_correct`.
theoremreal_QFTinv2_candidate_on_basis_one
theorem real_QFTinv2_candidate_on_basis_one :
FormalRV.Framework.uc_eval real_QFTinv2_candidate *
FormalRV.Framework.basis_vector 4 1
= IQFT_matrix 2 * FormalRV.Framework.basis_vector 4 1*Column 1: candidate on `|1⟩`.**
theoremreal_QFTinv2_candidate_on_basis_two
theorem real_QFTinv2_candidate_on_basis_two :
FormalRV.Framework.uc_eval real_QFTinv2_candidate *
FormalRV.Framework.basis_vector 4 2
= IQFT_matrix 2 * FormalRV.Framework.basis_vector 4 2*Column 2: candidate on `|2⟩`.**
theoremreal_QFTinv2_candidate_on_basis_three
theorem real_QFTinv2_candidate_on_basis_three :
FormalRV.Framework.uc_eval real_QFTinv2_candidate *
FormalRV.Framework.basis_vector 4 3
= IQFT_matrix 2 * FormalRV.Framework.basis_vector 4 3*Column 3: candidate on `|3⟩`.**
theoremuc_eval_real_QFTinv2_candidate_eq_IQFT_matrix
theorem uc_eval_real_QFTinv2_candidate_eq_IQFT_matrix :
FormalRV.Framework.uc_eval real_QFTinv2_candidate = IQFT_matrix 2*HEADLINE: 2-qubit IQFT matrix equality.** Lifts the four column
lemmas to matrix equality via `matrix_eq_of_basis_action`.
theoremreal_QFTinv_on_two
theorem real_QFTinv_on_two : real_QFTinv_on 2 = real_QFTinv2_candidate
The `n = 2` case of `real_QFTinv_on` is syntactically equal to
`real_QFTinv2_candidate`.
theoremuc_eval_real_QFTinv_eq_IQFT_matrix_two
theorem uc_eval_real_QFTinv_eq_IQFT_matrix_two :
FormalRV.Framework.uc_eval (real_QFTinv_on 2 : BaseUCom 2) = IQFT_matrix 2*m=2 circuit correctness.** `uc_eval (real_QFTinv_on 2) = IQFT_matrix 2`,
the 2-qubit counterpart to `uc_eval_real_QFTinv_eq_IQFT_matrix_one`.
theoremreal_QFTinv_two_on_fourier_state
theorem real_QFTinv_two_on_fourier_state (θ : ℝ) :
FormalRV.Framework.uc_eval (real_QFTinv_on 2 : BaseUCom 2) *
(((1 : ℂ) / Real.sqrt (2^2 : ℝ)) •
∑ x : Fin (2^2),
Complex.exp (2 * Real.pi * Complex.I * (x.val : ℂ) * (θ : ℂ)) •
FormalRV.Framework.basis_vector (2^2) x.val)
= qpe_phase_state 2 θ*2-qubit semantic theorem.** Mirrors `real_QFTinv_one_on_fourier_state`:
the real 2-qubit inverse QFT applied to the Fourier-weighted superposition
yields `qpe_phase_state 2 θ`.
theoremreal_QFTinv_lifted_on_kron
theorem real_QFTinv_lifted_on_kron
{m anc : Nat}
(ψc : Matrix (Fin (2^m)) (Fin 1) ℂ)
(ψd : Matrix (Fin (2^anc)) (Fin 1) ℂ)
(h_wt : UCom.WellTyped m (real_QFTinv_on m))
(h_IQFT : FormalRV.Framework.uc_eval (real_QFTinv_on m : BaseUCom m)
= IQFT_matrix m) :
FormalRV.Framework.uc_eval
(map_qubits (fun q => q) (real_QFTinv_on m) : BaseUCom (m + anc))
* kron_vec ψc ψd
= kron_vec (IQFT_matrix m * ψc) ψd*Lifted IQFT acts on the control factor.** Given `h_IQFT`, the
`real_QFTinv_on m` lifted to `m + anc` qubits acts on `kron_vec ψc ψd`
by applying `IQFT_matrix m` to the control factor `ψc`.
theoremfourier_weighted_kron_sum_eq_kron_vec_fourier_state
theorem fourier_weighted_kron_sum_eq_kron_vec_fourier_state
{m anc : Nat} (θ : ℝ) (ψ : Matrix (Fin (2^anc)) (Fin 1) ℂ) :
(((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
(((1 : ℂ) / Real.sqrt (2^m : ℝ)) •
∑ x : Fin (2^m),
Complex.exp (2 * Real.pi * Complex.I * (x.val : ℂ) * (θ : ℂ)) •
FormalRV.Framework.basis_vector (2^m) x.val) ψ*Distribute `kron_vec` into a Fourier-weighted sum.** Algebraic helper
exposing the `kron_vec ψc ψ` factorization of the Fourier-weighted
superposition.
theoremreal_QFTinv_on_fourier_weighted_kron_state_from_matrix_correct
theorem real_QFTinv_on_fourier_weighted_kron_state_from_matrix_correct
{m anc : Nat}
(θ : ℝ)
(ψ : Matrix (Fin (2^anc)) (Fin 1) ℂ)
(h_wt : UCom.WellTyped m (real_QFTinv_on m))
(h_IQFT : FormalRV.Framework.uc_eval (real_QFTinv_on m : BaseUCom m)
= IQFT_matrix m) :
FormalRV.Framework.uc_eval
(map_qubits (fun q => q) (real_QFTinv_on m) : BaseUCom (m + anc))
*
(((1 : ℂ) / Real.sqrt (2^m : ℝ)) •
∑ x : Fin (2^m),*Post-QFT theorem from IQFT correctness.** Given `h_IQFT`, the
lifted `real_QFTinv_on m` applied to the Fourier-weighted kron
superposition yields `kron_vec (qpe_phase_state m θ) ψ`.
theoremIQFT_matrix_apply
theorem IQFT_matrix_apply (m : Nat) (y x : Fin (2^m)) :
IQFT_matrix m y x
= ((1 : ℂ) / Real.sqrt (2^m : ℝ)) *
Complex.exp (-(2 * Real.pi * Complex.I) * (x.val : ℂ) * (y.val : ℂ)
/ (2^m : ℂ))*Named entry formula for `IQFT_matrix`.** Definitional unfolding,
exposed as a reusable theorem for the recursive correctness proof.
theoremuc_eval_real_QFTinv_layer_eq_IQFT_matrix_two
theorem uc_eval_real_QFTinv_layer_eq_IQFT_matrix_two :
FormalRV.Framework.uc_eval (real_QFTinv_layer 2 : BaseUCom 2)
= IQFT_matrix 2*At `n = 2`, the recursive `real_QFTinv_layer` produces `IQFT_matrix 2`.**
This is the first nontrivial inductive-base instance of the
arbitrary-n correctness `uc_eval_real_QFTinv_layer_eq_IQFT_matrix`,
proved by chaining `real_QFTinv_layer_two_eq_candidate` with
`uc_eval_real_QFTinv2_candidate_eq_IQFT_matrix`.
theoremIQFT_index_split
theorem IQFT_index_split (n : Nat) (_hn : 1 ≤ n) (xh yh xl yl : Nat) :
((2^n * xh + xl : ℂ) * (2^n * yh + yl) / 2^(n+1) : ℂ)
= (2^(n-1) * xh * yh : ℂ)
+ ((xh * yl + xl * yh : ℂ)) / 2
+ ((xl * yl : ℂ) / 2^(n+1))*Matrix-arithmetic index decomposition.** Pure scalar identity
underlying the recursive `IQFT_matrix` decomposition: when an index
splits into a high bit + low part (`z = 2^n · z_h + z_l`), the
product `xy / 2^(n+1)` decomposes into three additive terms:
- `2^(n-1) · x_h · y_h` — integer for `n ≥ 1`, contributes `exp(±2πi·N) = 1`.
- `(x_h · y_l + x_l · y_h) / 2` — half-integer offsets (the inter-bit phases).
- `x_l · y_l / 2^(n+1)` — the lower-block phase. Note the denominator
is `2^(n+1)`, not `2^n`; the recursive lower block exponent is
`exp(-π · I · x_l y_l / 2^n)`, which is half the `IQFT_matrix n`
argument. This means the natural matrix-level recursion is not
`IQFT_matrix (n+1) y x = ... · IQFT_matrix n y_l x_l` — the
textbook QFT recursion uses a different decomposition involving
controlled-phase corrections at every recursion level.
theoremiqft_index_reconstruct
theorem iqft_index_reconstruct (n : Nat) (x : Fin (2^(n+1))) :
x.val = (iqftHighBit n x).val * 2^n + (iqftLowBits n x).val*Index reconstruction from MSB + low.** `x.val = x_h · 2^n + x_l`.
theoremexp_neg_two_pi_I_mul_nat
theorem exp_neg_two_pi_I_mul_nat (k : Nat) :
Complex.exp ((-2 * Real.pi * (k : ℝ) : ℂ) * Complex.I) = 1*`exp(-2πi · k) = 1` for natural `k`.** Consequence of
`Complex.exp_int_mul_two_pi_mul_I`.
theoremexp_neg_pi_I_mul_nat
theorem exp_neg_pi_I_mul_nat (k : Nat) :
Complex.exp (((-Real.pi * (k : ℝ) : ℝ) : ℂ) * Complex.I) = (-1 : ℂ) ^ k*`exp(-π · I · k) = (-1)^k` for natural `k`.** Drives the
half-integer cross-term phase in the IQFT decomposition.
theoreminv_sqrt_pow_two_succ_factor
theorem inv_sqrt_pow_two_succ_factor (n : Nat) :
(1 : ℂ) / Real.sqrt (2^(n+1) : ℝ)
= ((1 : ℂ) / Real.sqrt 2) * ((1 : ℂ) / Real.sqrt (2^n : ℝ))*Scalar normalization for the IQFT recursion.** Factors the
inverse square-root: `1/√(2^(n+1)) = (1/√2) · (1/√(2^n))`.
FormalRV.QFT.IQFTCircuitCorrectness.CountdownDecomposition
FormalRV/QFT/IQFTCircuitCorrectness/CountdownDecomposition.lean
IQFTCircuitCorrectness — Part3 (re-export shim part; same namespace, opens de-duplicated).
theoremcountdown_zero
theorem countdown_zero (n : Nat) :
real_QFTinv_layer.countdown n 0 = (SKIP : FormalRV.Framework.BaseUCom n)Unfolding: `countdown n 0 = SKIP`.
theoremcountdown_succ
theorem countdown_succ (n k : Nat) :
real_QFTinv_layer.countdown n (k+1)
= UCom.seq (inverse_qft_phase_ladder n k) (real_QFTinv_layer.countdown n k)Unfolding: `countdown n (k+1) = ladder n k ; countdown n k`.
By the seq semantics, applying `countdown n (k+1)` to a state `v` first
applies the ladder for target `k`, then `countdown n k` (which processes
targets `k-1, k-2, ..., 0`).
theoremreal_QFTinv_layer_decomp
theorem real_QFTinv_layer_decomp (n : Nat) :
(real_QFTinv_layer n : FormalRV.Framework.BaseUCom n)
= UCom.seq (bit_reversal_swaps n) (real_QFTinv_layer.countdown n n)*Structural decomposition of `real_QFTinv_layer`.**
theoremreal_QFTinv_layer_acts
theorem real_QFTinv_layer_acts (n : Nat) (v : Matrix (Fin (2^n)) (Fin 1) ℂ) :
FormalRV.Framework.uc_eval (real_QFTinv_layer n : FormalRV.Framework.BaseUCom n) * v
= FormalRV.Framework.uc_eval
(real_QFTinv_layer.countdown n n : FormalRV.Framework.BaseUCom n)
* (FormalRV.Framework.uc_eval
(bit_reversal_swaps n : FormalRV.Framework.BaseUCom n) * v)*State-level decomposition**: applying `real_QFTinv_layer n` to a state
equals applying `bit_reversal_swaps n` first, then `countdown n n`.
theoremcountdown_zero_acts
theorem countdown_zero_acts (n : Nat) (hn : 0 < n) (v : Matrix (Fin (2^n)) (Fin 1) ℂ) :
FormalRV.Framework.uc_eval
(real_QFTinv_layer.countdown n 0 : FormalRV.Framework.BaseUCom n) * v = v*Countdown 0 acts as identity** (for positive `n`).
theoremcountdown_succ_acts
theorem countdown_succ_acts (n k : Nat) (v : Matrix (Fin (2^n)) (Fin 1) ℂ) :
FormalRV.Framework.uc_eval
(real_QFTinv_layer.countdown n (k+1) : FormalRV.Framework.BaseUCom n) * v
= FormalRV.Framework.uc_eval
(real_QFTinv_layer.countdown n k : FormalRV.Framework.BaseUCom n)
* (FormalRV.Framework.uc_eval
(inverse_qft_phase_ladder n k : FormalRV.Framework.BaseUCom n) * v)*Structural recursion for `countdown` action**: `countdown (k+1)` applied
to `v` equals `countdown k` applied to (`ladder k` applied to `v`).
theoremuc_eval_SWAP_on_f_to_vec
theorem uc_eval_SWAP_on_f_to_vec {n : Nat} (a b : Nat)
(ha : a < n) (hb : b < n) (hab : a ≠ b) (f : Nat → Bool) :
FormalRV.Framework.uc_eval
(FormalRV.Framework.BaseUCom.SWAP a b : FormalRV.Framework.BaseUCom n)
* f_to_vec n f
= f_to_vec n (swapBits f a b)*SWAP gate action on `f_to_vec`.** Direct wrapper around
`f_to_vec_SWAP` using the framework's CNOT-CNOT-CNOT unfolding of `SWAP`.
theorembit_reversal_loop_step
theorem bit_reversal_loop_step (n i : Nat) (hi : i + i + 1 < n) :
bit_reversal_swaps.loop n i
= UCom.seq (FormalRV.Framework.BaseUCom.SWAP i (n - 1 - i))
(bit_reversal_swaps.loop n (i + 1))theorembit_reversal_loop_base
theorem bit_reversal_loop_base (n i : Nat) (hi : ¬ i + i + 1 < n) :
bit_reversal_swaps.loop n i = (SKIP : FormalRV.Framework.BaseUCom n)theoremapplySwapsFrom_step
theorem applySwapsFrom_step (n k : Nat) (f : Nat → Bool) (hk : 2 * k + 1 < n) :
applySwapsFrom n k f = applySwapsFrom n (k+1) (swapBits f k (n-1-k))theoremapplySwapsFrom_base
theorem applySwapsFrom_base (n k : Nat) (f : Nat → Bool) (hk : ¬ 2 * k + 1 < n) :
applySwapsFrom n k f = ftheorembit_reversal_loop_acts_on_f_to_vec_aux
theorem bit_reversal_loop_acts_on_f_to_vec_aux
(n : Nat) (hn : 0 < n) : ∀ (m : Nat), ∀ (k : Nat), ∀ (f : Nat → Bool),
n - 2 * k = m →
FormalRV.Framework.uc_eval
(bit_reversal_swaps.loop n k : FormalRV.Framework.BaseUCom n)
* f_to_vec n f
= f_to_vec n (applySwapsFrom n k f)*Auxiliary recursion.** Action of the inner `bit_reversal_swaps.loop n k`
on `f_to_vec n f` equals `f_to_vec n (applySwapsFrom n k f)`. Proved by
strong induction on `n - 2*k`.
theorembit_reversal_swaps_acts_on_f_to_vec
theorem bit_reversal_swaps_acts_on_f_to_vec (n : Nat) (hn : 0 < n) (f : Nat → Bool) :
FormalRV.Framework.uc_eval (bit_reversal_swaps n : FormalRV.Framework.BaseUCom n)
* f_to_vec n f
= f_to_vec n (applySwapsFrom n 0 f)*HEADLINE: Bit-reversal SWAPs basis action.** The full bit-reversal
cascade maps `f_to_vec n f` to `f_to_vec n (applySwapsFrom n 0 f)`.
theoreminverse_qft_ladder_phase_from_succ
theorem inverse_qft_ladder_phase_from_succ (n target : Nat) (f : Nat → Bool) (k : Nat)
(hk : k < n) :
inverse_qft_ladder_phase_from n target f k
= (if f k ∧ f target then
Complex.exp ((((-(Real.pi / 2 ^ (k - target))) : ℝ)) * Complex.I)
else 1)
* inverse_qft_ladder_phase_from n target f (k+1)Recursive step for `inverse_qft_ladder_phase_from`.
theoreminverse_qft_ladder_phase_from_at_top
theorem inverse_qft_ladder_phase_from_at_top (n target : Nat) (f : Nat → Bool) :
inverse_qft_ladder_phase_from n target f n = 1Base case for `inverse_qft_ladder_phase_from` at `k = n`.
theoremladder_loop_step
theorem ladder_loop_step (n target j : Nat) (hj : j < n) :
inverse_qft_phase_ladder.loop n target j
= UCom.seq (controlled_Rz j target (-(Real.pi / (2 ^ (j - target) : ℝ))))
(inverse_qft_phase_ladder.loop n target (j + 1))Step unfolding for `inverse_qft_phase_ladder.loop` at `j < n`.
theoremladder_loop_base
theorem ladder_loop_base (n target j : Nat) (hj : ¬ j < n) :
inverse_qft_phase_ladder.loop n target j
= (FormalRV.Framework.BaseUCom.H target : FormalRV.Framework.BaseUCom n)Base case unfolding: `inverse_qft_phase_ladder.loop n target n = H target`.
theoremladder_loop_acts_on_f_to_vec_aux
theorem ladder_loop_acts_on_f_to_vec_aux
(n_arg : Nat) (target : Nat) (h_target : target < n_arg)
(f : Nat → Bool) :
∀ m k, k ≤ n_arg → n_arg - k = m → target < k →
FormalRV.Framework.uc_eval
(inverse_qft_phase_ladder.loop n_arg target k :
FormalRV.Framework.BaseUCom n_arg)
* f_to_vec n_arg f
= inverse_qft_ladder_phase_from n_arg target f k
• (FormalRV.Framework.uc_eval
(FormalRV.Framework.BaseUCom.H target : FormalRV.Framework.BaseUCom n_arg)
* f_to_vec n_arg f)*Auxiliary recursion**: action of the inner `loop k` on `f_to_vec`.
For `target < k ≤ n`, applying `loop k` to a basis-state vector
produces a scalar `inverse_qft_ladder_phase_from n target f k` times
the H-applied state.
theoreminverse_qft_phase_ladder_acts_on_f_to_vec
theorem inverse_qft_phase_ladder_acts_on_f_to_vec
(n target : Nat) (h_target : target < n)
(f : Nat → Bool) :
FormalRV.Framework.uc_eval
(inverse_qft_phase_ladder n target : FormalRV.Framework.BaseUCom n)
* f_to_vec n f
= inverse_qft_ladder_phase n target f
• (FormalRV.Framework.uc_eval
(FormalRV.Framework.BaseUCom.H target : FormalRV.Framework.BaseUCom n)
* f_to_vec n f)*HEADLINE: Ladder action on basis state.** The full
`inverse_qft_phase_ladder n target` applied to a basis state
`f_to_vec n f` equals `(ladder phase) • (H_target · f_to_vec n f)`,
where the ladder phase is the product of controlled-Rz contributions
from each control bit `j ∈ [target+1, n)`.
theoremIQFT_matrix_succ_entry_decomp
theorem IQFT_matrix_succ_entry_decomp
(n : Nat) (hn : 1 ≤ n)
(y x : Fin (2^(n+1))) :
IQFT_matrix (n+1) y x
= ((1 : ℂ) / Real.sqrt (2^(n+1) : ℝ))
* ((-1 : ℂ) ^
((iqftHighBit n x).val * (iqftLowBits n y).val
+ (iqftLowBits n x).val * (iqftHighBit n y).val))
* Complex.exp (-(Real.pi : ℂ) * Complex.I
* (iqftLowBits n x).val * (iqftLowBits n y).val / (2^n : ℂ))*HEADLINE: Successor entry decomposition for `IQFT_matrix`.**
For `n ≥ 1`, the `(y, x)` entry of `IQFT_matrix (n+1)` decomposes as
(1/√(2^(n+1))) · (-1)^(x_h · y_l + x_l · y_h) · exp(-π · I · x_l · y_l / 2^n)
where `(x_h, x_l)` and `(y_h, y_l)` are the MSB/lower-bit splits of `x` and `y`.
This is the matrix-arithmetic foundation for the recursive IQFT
correctness proof.
*Note on the inner exponent**: it is `exp(-π · I · x_l y_l / 2^n)`,
which is **half** the `IQFT_matrix n y_l x_l` exponent
`exp(-2π · I · x_l y_l / 2^n)`. This means the natural IQFT recursion
is not a direct factoring `IQFT_(n+1) y x = ... · IQFT_n y_l x_l`.
The textbook QFT recursion accounts for this discrepancy via the
controlled-phase ladder that conjugates the inner IQFT_n on the
control register (not yet formalized here).
theoremreal_QPE_on_eigenstate_from_IQFT_correct
theorem real_QPE_on_eigenstate_from_IQFT_correct
{m anc : Nat} (hmanc : 0 < m + anc) (hm : 0 < m)
(f : Nat → 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 θ • ψ)
(h_wt_IQFT : UCom.WellTyped m (real_QFTinv_on m))
(h_IQFT : FormalRV.Framework.uc_eval (real_QFTinv_on m : BaseUCom m)
= IQFT_matrix m) :*HEADLINE: Full real-QPE eigenstate theorem assuming IQFT correctness.**
Given `h_IQFT : uc_eval (real_QFTinv_on m) = IQFT_matrix m`, the
real-QPE circuit applied to `|0^m⟩ ⊗ ψ` (where `ψ` is a QPE eigenstate
with phase θ) yields `kron_vec (qpe_phase_state m θ) ψ`. This is the
exact form needed to drive `QPE_MMI_correct`; the only remaining
obligation is proving `h_IQFT` for arbitrary `m`.
FormalRV.QFT.IQFTCircuitCorrectness.CountdownOutputAndBitReversal
FormalRV/QFT/IQFTCircuitCorrectness/CountdownOutputAndBitReversal.lean
IQFTCircuitCorrectness — Part4 (re-export shim part; same namespace, opens de-duplicated).
theoreminverse_qft_phase_ladder_explicit_on_f_to_vec
theorem inverse_qft_phase_ladder_explicit_on_f_to_vec
(n target : Nat) (h_target : target < n)
(f : Nat → Bool) :
FormalRV.Framework.uc_eval
(inverse_qft_phase_ladder n target : FormalRV.Framework.BaseUCom n)
* f_to_vec n f
= inverse_qft_ladder_phase n target f •
(((Real.sqrt 2 / 2 : ℂ) • f_to_vec n (update f target false))
+ ((if f target then -(Real.sqrt 2 / 2 : ℂ) else (Real.sqrt 2 / 2 : ℂ))
• f_to_vec n (update f target true)))*Explicit two-branch ladder action.** Combines
`inverse_qft_phase_ladder_acts_on_f_to_vec` with `f_to_vec_H_uc_eval`
to expose the Hadamard expansion as a sum of two `f_to_vec` terms.
theoremcountdown_output_zero
theorem countdown_output_zero (n : Nat) (f : Nat → Bool) :
countdown_output n 0 f = f_to_vec n ftheoremcountdown_output_succ
theorem countdown_output_succ (n k : Nat) (f : Nat → Bool) :
countdown_output n (k+1) f
= inverse_qft_ladder_phase n k f •
(((Real.sqrt 2 / 2 : ℂ) • countdown_output n k (update f k false))
+ ((if f k then -(Real.sqrt 2 / 2 : ℂ) else (Real.sqrt 2 / 2 : ℂ))
• countdown_output n k (update f k true)))theoremcountdown_acts_on_f_to_vec
theorem countdown_acts_on_f_to_vec (n : Nat) (hn : 0 < n) :
∀ k, k ≤ n → ∀ (f : Nat → Bool),
FormalRV.Framework.uc_eval
(real_QFTinv_layer.countdown n k : FormalRV.Framework.BaseUCom n)
* f_to_vec n f
= countdown_output n k f*HEADLINE: Countdown action on `f_to_vec`.** Applying `countdown n k`
to a basis vector `f_to_vec n f` produces `countdown_output n k f`,
the recursively-defined expected output. Proof by induction on k,
using `countdown_succ_acts` and the explicit ladder action.
theoremreal_QFTinv_layer_output_on_f_to_vec
theorem real_QFTinv_layer_output_on_f_to_vec
(n : Nat) (hn : 0 < n) (f : Nat → Bool) :
FormalRV.Framework.uc_eval (real_QFTinv_layer n : FormalRV.Framework.BaseUCom n)
* f_to_vec n f
= countdown_output n n (applySwapsFrom n 0 f)*Full `real_QFTinv_layer` action on `f_to_vec`.** Combines bit-reversal
and countdown: the layer applied to `f_to_vec n f` equals
`countdown_output n n (applySwapsFrom n 0 f)`.
theoremuc_eval_real_QFTinv_layer_eq_IQFT_matrix_one
theorem uc_eval_real_QFTinv_layer_eq_IQFT_matrix_one :
FormalRV.Framework.uc_eval (real_QFTinv_layer 1 : FormalRV.Framework.BaseUCom 1)
= IQFT_matrix 1*`n = 1`: recursive layer matches `IQFT_matrix 1`.** Trivial since
`bit_reversal_swaps 1 = SKIP`, `countdown 1 = H 0 ; SKIP`, and the
matrix theorem for `H 0` is already in place.
theoremIQFT_matrix_mul_basis_apply
theorem IQFT_matrix_mul_basis_apply (n : Nat) (x y : Fin (2^n)) :
(IQFT_matrix n * FormalRV.Framework.basis_vector (2^n) x.val) y 0
= IQFT_matrix n y x*Entry formula for IQFT_matrix · basis_vector.** Picks out the
`(y, x)` entry of `IQFT_matrix`.
theoremcountdown_output_eq_IQFT_column_one
theorem countdown_output_eq_IQFT_column_one (x : Fin (2^1)) :
countdown_output 1 1 (applySwapsFrom 1 0 (nat_to_funbool 1 x.val))
= IQFT_matrix 1 * FormalRV.Framework.basis_vector (2^1) x.val*`n = 1` column equality**: derived from the n=1 layer matrix
correctness via the `real_QFTinv_layer_output_on_f_to_vec` bridge.
theoremcountdown_output_eq_IQFT_column_two
theorem countdown_output_eq_IQFT_column_two (x : Fin (2^2)) :
countdown_output 2 2 (applySwapsFrom 2 0 (nat_to_funbool 2 x.val))
= IQFT_matrix 2 * FormalRV.Framework.basis_vector (2^2) x.val*`n = 2` column equality**: derived from the n=2 layer matrix
correctness.
theoremcountdownColumn_eq_IQFT_column_one
theorem countdownColumn_eq_IQFT_column_one (x : Fin (2^1)) :
countdownColumn 1 x = IQFT_matrix 1 * FormalRV.Framework.basis_vector (2^1) x.val*`n = 1` column equality** in `countdownColumn` form.
theoremcountdownColumn_eq_IQFT_column_two
theorem countdownColumn_eq_IQFT_column_two (x : Fin (2^2)) :
countdownColumn 2 x = IQFT_matrix 2 * FormalRV.Framework.basis_vector (2^2) x.val*`n = 2` column equality** in `countdownColumn` form.
theoremf_to_vec_dim_split
theorem f_to_vec_dim_split (n : Nat) (f : Nat → Bool) :
f_to_vec (n+1) f
= kron_vec (f_to_vec n f)
(FormalRV.Framework.basis_vector 2 (if f n then 1 else 0))*`f_to_vec` dimension split.** `f_to_vec (n+1) f` factors as the
kron product of `f_to_vec n f` (using the lower n bits) and a
1-qubit basis vector encoding `f n`.
theoreminverse_qft_ladder_phase_dim_split
theorem inverse_qft_ladder_phase_dim_split
(n target : Nat) (h_target : target < n)
(f : Nat → Bool) :
inverse_qft_ladder_phase (n+1) target f
= (if f n ∧ f target then
Complex.exp ((((-(Real.pi / 2 ^ (n - target))) : ℝ)) * Complex.I)
else 1)
* inverse_qft_ladder_phase n target f*Ladder phase dimension split.** For `target < n`, the
`(n+1)`-qubit ladder phase factors as `(extra factor from qubit n) ·
(n-qubit ladder phase)`. The extra factor is the controlled-Rz
contribution from the highest qubit `n` onto the target.
theoremembedWithExtraBit_smul
theorem embedWithExtraBit_smul (n : Nat) (extra : Bool) (c : ℂ)
(v : Matrix (Fin (2^n)) (Fin 1) ℂ) :
embedWithExtraBit n extra (c • v) = c • embedWithExtraBit n extra v`embedWithExtraBit` commutes with scalar multiplication.
theoremembedWithExtraBit_add
theorem embedWithExtraBit_add (n : Nat) (extra : Bool)
(v w : Matrix (Fin (2^n)) (Fin 1) ℂ) :
embedWithExtraBit n extra (v + w)
= embedWithExtraBit n extra v + embedWithExtraBit n extra w`embedWithExtraBit` commutes with addition.
theoremcumulative_extra_phase_zero
theorem cumulative_extra_phase_zero (n : Nat) (f : Nat → Bool) :
cumulative_extra_phase n 0 f = 1theoremcumulative_extra_phase_succ
theorem cumulative_extra_phase_succ (n k : Nat) (f : Nat → Bool) :
cumulative_extra_phase n (k+1) f
= cumulative_extra_phase n k f *
(if f n ∧ f k then
Complex.exp ((((-(Real.pi / 2 ^ (n - k))) : ℝ)) * Complex.I)
else 1)theoremextra_bit_update_lt
theorem extra_bit_update_lt (n k : Nat) (hk : k < n) (f : Nat → Bool) (b : Bool) :
update f k b n = f n*Extra-bit update lemma**: updating position `k < n` doesn't change
the value at position `n`.
theoremcumulative_extra_phase_update_branch
theorem cumulative_extra_phase_update_branch
(n k : Nat) (hk : k < n) (f : Nat → Bool) (b : Bool) :
cumulative_extra_phase n k (update f k b)
= cumulative_extra_phase n k f*Cumulative extra phase update-branch lemma**: updating position
`k < n` doesn't change the cumulative extra phase product over targets
`t ∈ [0, k)`.
theoremcountdown_output_dim_split
theorem countdown_output_dim_split (n : Nat) :
∀ k, k ≤ n → ∀ (f : Nat → Bool),
countdown_output (n+1) k f
= cumulative_extra_phase n k f •
embedWithExtraBit n (f n) (countdown_output n k f)*HEADLINE: Countdown output dimension split.** For `k ≤ n`, the
`(n+1)`-qubit countdown output factors as a cumulative-extra-phase
scalar times the n-qubit countdown output embedded with the
extra-bit `f n`. Proof by induction on k: base via
`f_to_vec_dim_split`; successor via `inverse_qft_ladder_phase_dim_split`
+ the update lemmas + bilinearity of `embedWithExtraBit`, closed by
`module`.
theoremcountdown_output_dim_split_full
theorem countdown_output_dim_split_full (n : Nat) (f : Nat → Bool) :
countdown_output (n+1) n f
= cumulative_extra_phase n n f •
embedWithExtraBit n (f n) (countdown_output n n f)*Full-k specialization** of `countdown_output_dim_split`: at `k = n`,
the (n+1)-qubit countdown output factors through the full n-qubit
countdown.
theoremiqft_index_reconstruct_highN_low1
theorem iqft_index_reconstruct_highN_low1 (n : Nat) (y : Fin (2^(n+1))) :
y.val = (iqftHighBitsN n y).val * 2 + (iqftLowBitLSB n y).val*Index reconstruction**: `y.val = high_n.val · 2 + lsb.val`.
theoremswapBits_left
theorem swapBits_left (f : Nat → Bool) (a b : Nat) :
swapBits f a b a = f b`swapBits f a b a = f b`.
theoremswapBits_right
theorem swapBits_right (f : Nat → Bool) (a b : Nat) (hab : a ≠ b) :
swapBits f a b b = f a`swapBits f a b b = f a` (when `a ≠ b`).
theoremswapBits_other
theorem swapBits_other (f : Nat → Bool) (a b i : Nat) (hia : i ≠ a) (hib : i ≠ b) :
swapBits f a b i = f i`swapBits f a b i = f i` when `i ∉ {a, b}`.
theoremapplySwapsFrom_apply_region
theorem applySwapsFrom_apply_region (n : Nat) :
∀ (m k : Nat), n - 2 * k = m → ∀ (f : Nat → Bool) (i : Nat),
applySwapsFrom n k f i =
if k ≤ i ∧ i ≤ n - 1 - k then f (n - 1 - i) else f i*Partial-reversal invariant.** Starting from index `k`,
`applySwapsFrom n k f` reverses positions in `[k, n-1-k]` (and leaves
positions outside this range unchanged). Proof by strong induction
on `n - 2*k`.
FormalRV.QFT.IQFTCircuitCorrectness.OneAndTwoQubitCorrectness
FormalRV/QFT/IQFTCircuitCorrectness/OneAndTwoQubitCorrectness.lean
IQFTCircuitCorrectness — Part1 (re-export shim part; same namespace, opens de-duplicated).
lemmafourier_weighted_state_apply
lemma fourier_weighted_state_apply (m : Nat) (θ : ℝ) (k : Fin (2^m)) :
(((1 : ℂ) / Real.sqrt (2^m : ℝ)) •
∑ x : Fin (2^m),
Complex.exp (2 * Real.pi * Complex.I * (x.val : ℂ) * (θ : ℂ)) •
FormalRV.Framework.basis_vector (2^m) x.val) k 0
= ((1 : ℂ) / Real.sqrt (2^m : ℝ)) *
Complex.exp (2 * Real.pi * Complex.I * (k.val : ℂ) * (θ : ℂ))Pointwise: the Fourier-weighted superposition evaluated at index `k`
gives the single non-zero term `(1/√2^m) · exp(2πi · k · θ)`.
lemmainv_sqrt_two_pow_sq
lemma inv_sqrt_two_pow_sq (m : Nat) :
((1 : ℂ) / Real.sqrt (2^m : ℝ)) * ((1 : ℂ) / Real.sqrt (2^m : ℝ))
= 1 / (2^m : ℂ)`(1/√2^m)² = 1/2^m` in ℂ.
theoremIQFT_matrix_on_fourier_weighted_state
theorem IQFT_matrix_on_fourier_weighted_state
(m : Nat) (θ : ℝ) :
IQFT_matrix m *
(((1 : ℂ) / Real.sqrt (2^m : ℝ)) •
∑ x : Fin (2^m),
Complex.exp (2 * Real.pi * Complex.I * (x.val : ℂ) * (θ : ℂ)) •
FormalRV.Framework.basis_vector (2^m) x.val)
= qpe_phase_state m θ*HEADLINE MATH THEOREM.** The ideal inverse-QFT matrix maps the
Fourier-weighted superposition `(1/√2^m) · ∑_x exp(+2πi · x · θ) · |x⟩`
to `qpe_phase_state m θ`. This is a pure linear-algebra fact,
independent of any specific circuit realization.
theoremreal_QFTinv_on_one
theorem real_QFTinv_on_one : real_QFTinv_on 1 = (H 0 : BaseUCom 1)
The real 1-qubit inverse QFT is `H 0`.
theoremreal_QFTinv_on_zero
theorem real_QFTinv_on_zero : real_QFTinv_on 0 = (SKIP : BaseUCom 0)
The real 0-qubit inverse QFT is `SKIP`.
theoremreal_QFTinv_layer_two_eq_candidate
theorem real_QFTinv_layer_two_eq_candidate :
FormalRV.Framework.uc_eval (real_QFTinv_layer 2)
= FormalRV.Framework.uc_eval real_QFTinv2_candidate*At `n = 2`, the recursive layer matches the hand-written candidate.**
Both circuits evaluate to `H 0 · CR(-π/2) · H 1 · SWAP` as a 4×4 matrix.
The recursive layer has a trailing `SKIP`, which collapses via
`uc_eval_ID_eq_one`.
lemmasqrt_two_div_two_eq_inv
lemma sqrt_two_div_two_eq_inv :
(Real.sqrt 2 : ℂ) / 2 = (Real.sqrt 2 : ℂ)⁻¹Helper: `√2 / 2 = (√2)⁻¹` over ℂ.
theoremuc_eval_real_QFTinv_eq_IQFT_matrix_one
theorem uc_eval_real_QFTinv_eq_IQFT_matrix_one :
FormalRV.Framework.uc_eval (real_QFTinv_on 1 : BaseUCom 1)
= IQFT_matrix 1*m=1 circuit correctness.** The 1-qubit `real_QFTinv_on 1 = H 0`
has unitary evaluation matrix equal to `IQFT_matrix 1`. Proof: case
analysis on the 2×2 entries, with normalization `√2/2 = (√2)⁻¹` and
`exp(-π·I) = -1`.
theoremreal_QFTinv_one_on_fourier_state
theorem real_QFTinv_one_on_fourier_state (θ : ℝ) :
FormalRV.Framework.uc_eval (real_QFTinv_on 1 : BaseUCom 1) *
(((1 : ℂ) / Real.sqrt (2^1 : ℝ)) •
∑ x : Fin (2^1),
Complex.exp (2 * Real.pi * Complex.I * (x.val : ℂ) * (θ : ℂ)) •
FormalRV.Framework.basis_vector (2^1) x.val)
= qpe_phase_state 1 θ*1-qubit semantic theorem.** The real 1-qubit inverse QFT applied
to the Fourier-weighted superposition `(1/√2) · ∑_x exp(2πi · x · θ) |x⟩`
yields `qpe_phase_state 1 θ`. Combines the circuit-correctness
theorem with the matrix-level `IQFT_matrix_on_fourier_weighted_state`.
theoremH_one_eq_minus
theorem H_one_eq_minus :
FormalRV.Framework.uc_eval
(FormalRV.Framework.BaseUCom.H 0 : FormalRV.Framework.BaseUCom 1) *
FormalRV.Framework.basis_vector 2 1
= ((Real.sqrt 2 / 2 : ℂ)) •
(FormalRV.Framework.basis_vector 2 0 -
FormalRV.Framework.basis_vector 2 1)*`H |1⟩ = (√2/2) · (|0⟩ − |1⟩)`** — the `|1⟩` counterpart to
`H_zero_eq_plus`. Direct 2×2 computation.
theoremuc_eval_H_zero_two_eq_pad_u
theorem uc_eval_H_zero_two_eq_pad_u :
FormalRV.Framework.uc_eval (BaseUCom.H 0 : FormalRV.Framework.BaseUCom 2)
= pad_u 2 0 hMatrix`uc_eval (H 0) = pad_u 2 0 hMatrix` at dim = 2.
theoremuc_eval_H_one_two_eq_pad_u
theorem uc_eval_H_one_two_eq_pad_u :
FormalRV.Framework.uc_eval (BaseUCom.H 1 : FormalRV.Framework.BaseUCom 2)
= pad_u 2 1 hMatrix`uc_eval (H 1) = pad_u 2 1 hMatrix` at dim = 2.
theoremIQFT_matrix_two_on_basis_zero
theorem IQFT_matrix_two_on_basis_zero :
IQFT_matrix 2 * FormalRV.Framework.basis_vector 4 0
= ((1 : ℂ) / Real.sqrt (2^2 : ℝ)) •
(FormalRV.Framework.basis_vector 4 0 +
FormalRV.Framework.basis_vector 4 1 +
FormalRV.Framework.basis_vector 4 2 +
FormalRV.Framework.basis_vector 4 3)*`IQFT_matrix 2` on `|0⟩`**: produces the uniform superposition
`(1/2) · (|0⟩ + |1⟩ + |2⟩ + |3⟩)`. All phases are 1 because
`exp(0) = 1`.
theoremIQFT_matrix_two_on_basis_one
theorem IQFT_matrix_two_on_basis_one :
IQFT_matrix 2 * FormalRV.Framework.basis_vector 4 1
= ((1 : ℂ) / Real.sqrt (2^2 : ℝ)) •
(FormalRV.Framework.basis_vector 4 0
+ Complex.exp (-(Real.pi / 2) * Complex.I) • FormalRV.Framework.basis_vector 4 1
+ Complex.exp (-Real.pi * Complex.I) • FormalRV.Framework.basis_vector 4 2
+ Complex.exp (-(3 * Real.pi / 2) * Complex.I) • FormalRV.Framework.basis_vector 4 3)*`IQFT_matrix 2` on `|1⟩`**: `(1/2) · (|0⟩ + e^(-iπ/2)|1⟩ +
e^(-iπ)|2⟩ + e^(-i3π/2)|3⟩)`.
theoremIQFT_matrix_two_on_basis_two
theorem IQFT_matrix_two_on_basis_two :
IQFT_matrix 2 * FormalRV.Framework.basis_vector 4 2
= ((1 : ℂ) / Real.sqrt (2^2 : ℝ)) •
(FormalRV.Framework.basis_vector 4 0
+ Complex.exp (-Real.pi * Complex.I) • FormalRV.Framework.basis_vector 4 1
+ Complex.exp (-2 * Real.pi * Complex.I) • FormalRV.Framework.basis_vector 4 2
+ Complex.exp (-3 * Real.pi * Complex.I) • FormalRV.Framework.basis_vector 4 3)*`IQFT_matrix 2` on `|2⟩`**: phases are `1, e^(-iπ), e^(-i2π),
e^(-i3π)` which collapse to `1, -1, 1, -1`.
theoremIQFT_matrix_two_on_basis_three
theorem IQFT_matrix_two_on_basis_three :
IQFT_matrix 2 * FormalRV.Framework.basis_vector 4 3
= ((1 : ℂ) / Real.sqrt (2^2 : ℝ)) •
(FormalRV.Framework.basis_vector 4 0
+ Complex.exp (-(3 * Real.pi / 2) * Complex.I) • FormalRV.Framework.basis_vector 4 1
+ Complex.exp (-3 * Real.pi * Complex.I) • FormalRV.Framework.basis_vector 4 2
+ Complex.exp (-(9 * Real.pi / 2) * Complex.I) • FormalRV.Framework.basis_vector 4 3)*`IQFT_matrix 2` on `|3⟩`**: phases form the conjugate
`{1, -i, -1, i}` of the `|1⟩` column.
FormalRV.QFT.IQFTCorrectness
FormalRV/QFT/IQFTCorrectness.lean
FormalRV.QFT.IQFTCorrectness
────────────────────────────
THE semantic-correctness theorem for the inverse QFT.
Imports THE definition from `IQFTDef.lean`. The single theorem to audit is
`iqft_correct`: the real `BaseUCom` inverse-QFT circuit evaluates EXACTLY to
the ideal `IQFT_matrix`, for every width `n ≥ 1`. Its proof is delegated to
the recursive column argument in `IQFTRecursiveArbitrary.lean` (base cases in
`IQFTCircuitCorrectness.lean`).
theoremiqft_correct
theorem iqft_correct (n : Nat) (hn : 0 < n) :
FormalRV.Framework.uc_eval (IQFT n) = IQFT_matrix n*Inverse QFT — circuit correctness (THE headline).**
For every `n ≥ 1`, the real inverse-QFT circuit evaluates to the ideal
inverse-QFT matrix:
`uc_eval (IQFT n) = IQFT_matrix n`.
i.e. the bit-reversal-plus-phase-ladder circuit `real_QFTinv_layer n` is, as a
unitary, exactly `(y,x) ↦ (1/√2ⁿ)·exp(-2πi·x·y/2ⁿ)`. Proved by induction on `n`
(column-by-column) — no approximation, no axiom.
theoremiqft_wellTyped
theorem iqft_wellTyped (n : Nat) (hn : 0 < n) :
UCom.WellTyped n (IQFT n)*Inverse QFT — well-typed.** `IQFT n` uses only qubits `< n`.
theoremiqft_correct_verified
theorem iqft_correct_verified (n : Nat) (hn : 0 < n) :
UCom.WellTyped n (IQFT n)
∧ FormalRV.Framework.uc_eval (IQFT n) = IQFT_matrix n*Inverse QFT — verified bundle (correctness AFTER well-typedness).** The
single circuit `IQFT n` is simultaneously `WellTyped` on `n` qubits and equal,
as a unitary, to the ideal `IQFT_matrix n`.
theoremQFTinv_correct
theorem QFTinv_correct (m : Nat) (hm : 0 < m) :
FormalRV.Framework.uc_eval (FormalRV.Framework.BaseUCom.QFTinv m : BaseUCom m)
= IQFT_matrix m*Framework bridge.** The framework-level `BaseUCom.QFTinv m` (the object the
QPE / Shor pipeline plugs into its measurement basis) also evaluates to the
ideal `IQFT_matrix m`.
FormalRV.QFT.IQFTCount
FormalRV/QFT/IQFTCount.lean
FormalRV.QFT.IQFTCount
──────────────────────
CLOSED-FORM, ANCHORED resource counts for the inverse-QFT circuit — the
independent `Resource` counters applied to THE actual `BaseUCom` syntax tree
`real_QFTinv_layer n` (= `QFTinv n` = `IQFT n`), proven equal to closed forms
by induction over the circuit's own recursion. This closes the audit gap
"no gate counter on BaseUCom / QFT resource is only a predicate + an error
budget": the IQFT now has honest TIME counts (gates) and a SPACE count
(qubits), all forced by the tree.
THE headlines (for every `n`; width needs `n ≥ 1`):
• `cnotCountU_IQFT` : CNOTs = `3·⌊n/2⌋ + n·(n−1)`
(3 per bit-reversal SWAP + 2 per controlled phase,
with `n(n−1)/2` controlled phases)
• `oneQCountU_IQFT` : 1q gates = `3·(n·(n−1)/2) + n + 2`
(3 per controlled phase + n Hadamards + 2 SKIPs)
• `gateCountU_IQFT` : total = the sum of the two
• `widthU_IQFT` : qubits = `n` — exactly n qubits, NO hidden ancilla
• `iqft_verified_with_resources` : the TRIPLE — semantics (`= IQFT_matrix n`)
AND time AND space, all about the SAME syntactic object.
The counters live in `Resource/` and import only the IR — they cannot be
influenced by anything here; these theorems merely reveal what the counters
return on this circuit. Independent cross-check: the emitted OpenQASM
(`IQFTGadget.emitQASM n`, computable) lists exactly `⌊n/2⌋` `swap`,
`n(n−1)/2` `cu1` and `n` `h` lines — countable by `#eval` with no proofs.
theoremladder_loop_eq
private theorem ladder_loop_eq {dim : Nat} (n target j : Nat) :
(inverse_qft_phase_ladder.loop n target j : BaseUCom dim)
= if j < n then
UCom.seq (controlled_Rz j target (-(Real.pi / (2 ^ (j - target) : ℝ))))
(inverse_qft_phase_ladder.loop n target (j + 1))
else H targettheoremladder_eq
private theorem ladder_eq {dim : Nat} (n target : Nat) :
(inverse_qft_phase_ladder n target : BaseUCom dim)
= inverse_qft_phase_ladder.loop n target (target + 1)theorembrs_loop_eq
private theorem brs_loop_eq {dim : Nat} (n k : Nat) :
(bit_reversal_swaps.loop n k : BaseUCom dim)
= if k + k + 1 < n then
UCom.seq (SWAP k (n - 1 - k)) (bit_reversal_swaps.loop n (k + 1))
else SKIPtheorembrs_eq
private theorem brs_eq {dim : Nat} (n : Nat) :
(bit_reversal_swaps n : BaseUCom dim) = bit_reversal_swaps.loop n 0theoremcountdown_zero_eq
private theorem countdown_zero_eq {dim : Nat} (n : Nat) :
(real_QFTinv_layer.countdown n 0 : BaseUCom dim) = SKIPtheoremcountdown_succ_eq
private theorem countdown_succ_eq {dim : Nat} (n k : Nat) :
(real_QFTinv_layer.countdown n (k + 1) : BaseUCom dim)
= UCom.seq (inverse_qft_phase_ladder n k) (real_QFTinv_layer.countdown n k)theoremlayer_eq
private theorem layer_eq {dim : Nat} (n : Nat) :
(real_QFTinv_layer n : BaseUCom dim)
= UCom.seq (bit_reversal_swaps n) (real_QFTinv_layer.countdown n n)theoremwidthU_controlled_Rz
theorem widthU_controlled_Rz {dim : Nat} (q t : Nat) (lam : ℝ) :
widthU (controlled_Rz q t lam : BaseUCom dim) = max (q + 1) (t + 1)theoremladder_loop_counts
private theorem ladder_loop_counts {dim : Nat} (n target : Nat) :
∀ (fuel j : Nat), n - j = fuel →
oneQCountU (inverse_qft_phase_ladder.loop n target j : BaseUCom dim)
= 3 * (n - j) + 1
∧ cnotCountU (inverse_qft_phase_ladder.loop n target j : BaseUCom dim)
= 2 * (n - j)theoremoneQCountU_ladder
theorem oneQCountU_ladder {dim : Nat} (n target : Nat) :
oneQCountU (inverse_qft_phase_ladder n target : BaseUCom dim)
= 3 * (n - (target + 1)) + 1One-qubit gates of one phase ladder: 3 per kept rotation, plus the `H`.
theoremcnotCountU_ladder
theorem cnotCountU_ladder {dim : Nat} (n target : Nat) :
cnotCountU (inverse_qft_phase_ladder n target : BaseUCom dim)
= 2 * (n - (target + 1))CNOTs of one phase ladder: 2 per kept rotation.
theorembrs_loop_counts
private theorem brs_loop_counts {dim : Nat} (n : Nat) :
∀ (fuel k : Nat), n - 2 * k = fuel →
oneQCountU (bit_reversal_swaps.loop n k : BaseUCom dim) = 1
∧ cnotCountU (bit_reversal_swaps.loop n k : BaseUCom dim) = 3 * (n / 2 - k)theoremcnotCountU_bit_reversal_swaps
theorem cnotCountU_bit_reversal_swaps {dim : Nat} (n : Nat) :
cnotCountU (bit_reversal_swaps n : BaseUCom dim) = 3 * (n / 2)CNOTs of the bit-reversal cascade: 3 per SWAP, `⌊n/2⌋` SWAPs.
theoremoneQCountU_bit_reversal_swaps
theorem oneQCountU_bit_reversal_swaps {dim : Nat} (n : Nat) :
oneQCountU (bit_reversal_swaps n : BaseUCom dim) = 1One-qubit gates of the bit-reversal cascade: just the terminal `SKIP`.
theoremcountdown_cnot
private theorem countdown_cnot {dim : Nat} (n : Nat) :
∀ k, k ≤ n →
cnotCountU (real_QFTinv_layer.countdown n k : BaseUCom dim)
= k * (2 * n - k - 1)theoremcountdown_oneQ_doubled
private theorem countdown_oneQ_doubled {dim : Nat} (n : Nat) :
∀ k, k ≤ n →
2 * oneQCountU (real_QFTinv_layer.countdown n k : BaseUCom dim)
= 3 * (k * (2 * n - k - 1)) + 2 * k + 2theoremcnotCountU_real_QFTinv_layer
theorem cnotCountU_real_QFTinv_layer {dim : Nat} (n : Nat) :
cnotCountU (real_QFTinv_layer n : BaseUCom dim) = 3 * (n / 2) + n * (n - 1)*IQFT CNOT count (THE headline, time).** The full n-qubit inverse QFT has
exactly `3·⌊n/2⌋ + n·(n−1)` CNOTs: 3 per bit-reversal SWAP, plus 2 per
controlled phase with `n(n−1)/2` controlled phases. Anchored: the LHS is the
independent counter walking THE verified circuit's syntax tree.
theoremoneQCountU_real_QFTinv_layer
theorem oneQCountU_real_QFTinv_layer {dim : Nat} (n : Nat) :
oneQCountU (real_QFTinv_layer n : BaseUCom dim)
= 3 * (n * (n - 1) / 2) + n + 2*IQFT one-qubit-gate count (time).** `3·(n(n−1)/2) + n + 2`: 3 rotations
per controlled phase, `n` Hadamards, and the 2 structural `SKIP`s.
theoremgateCountU_real_QFTinv_layer
theorem gateCountU_real_QFTinv_layer {dim : Nat} (n : Nat) :
gateCountU (real_QFTinv_layer n : BaseUCom dim)
= (3 * (n * (n - 1) / 2) + n + 2) + (3 * (n / 2) + n * (n - 1))*IQFT total gate count (time).** One-qubit gates + CNOTs.
theoremladder_loop_width
private theorem ladder_loop_width {dim : Nat} (n target : Nat) (ht : target < n) :
∀ (fuel j : Nat), n - j = fuel →
widthU (inverse_qft_phase_ladder.loop n target j : BaseUCom dim)
= if j < n then n else target + 1theoremwidthU_ladder
theorem widthU_ladder {dim : Nat} (n target : Nat) (ht : target < n) :
widthU (inverse_qft_phase_ladder n target : BaseUCom dim) = nOne ladder spans the whole `n`-qubit register (its controls run up to
`n−1`; for `target = n−1` the lone `H` sits on qubit `n−1`).
theorembrs_loop_width
private theorem brs_loop_width {dim : Nat} (n : Nat) :
∀ (fuel k : Nat), n - 2 * k = fuel →
widthU (bit_reversal_swaps.loop n k : BaseUCom dim)
= if k + k + 1 < n then n - k else 1theoremwidthU_bit_reversal_swaps
theorem widthU_bit_reversal_swaps {dim : Nat} (n : Nat) (hn : 0 < n) :
widthU (bit_reversal_swaps n : BaseUCom dim) = nThe bit-reversal cascade spans the register (for `n ≥ 1`).
theoremcountdown_width
private theorem countdown_width {dim : Nat} (n : Nat) :
∀ k, 0 < k → k ≤ n →
widthU (real_QFTinv_layer.countdown n k : BaseUCom dim) = ntheoremwidthU_real_QFTinv_layer
theorem widthU_real_QFTinv_layer {dim : Nat} (n : Nat) (hn : 0 < n) :
widthU (real_QFTinv_layer n : BaseUCom dim) = n*IQFT qubit count (THE headline, space).** The full n-qubit inverse QFT
touches EXACTLY `n` qubits — no hidden ancilla. Anchored: the LHS is the
independent space counter walking THE verified circuit's syntax tree.
theoremcnotCountU_QFTinv
theorem cnotCountU_QFTinv {dim : Nat} (n : Nat) :
cnotCountU (QFTinv n : BaseUCom dim) = 3 * (n / 2) + n * (n - 1)The counts transfer to `QFTinv` by definitional equality.
theoremoneQCountU_QFTinv
theorem oneQCountU_QFTinv {dim : Nat} (n : Nat) :
oneQCountU (QFTinv n : BaseUCom dim) = 3 * (n * (n - 1) / 2) + n + 2theoremwidthU_QFTinv
theorem widthU_QFTinv {dim : Nat} (n : Nat) (hn : 0 < n) :
widthU (QFTinv n : BaseUCom dim) = ntheoremcnotCountU_IQFT
theorem cnotCountU_IQFT (n : Nat) :
cnotCountU (FormalRV.SQIRPort.IQFT n) = 3 * (n / 2) + n * (n - 1)*CNOT count of `IQFT n`** (the QFT spine's headline circuit, via the
SQIRPort↔Framework bridge — the two are the SAME syntax tree).
theoremoneQCountU_IQFT
theorem oneQCountU_IQFT (n : Nat) :
oneQCountU (FormalRV.SQIRPort.IQFT n) = 3 * (n * (n - 1) / 2) + n + 2*One-qubit-gate count of `IQFT n`.**
theoremwidthU_IQFT
theorem widthU_IQFT (n : Nat) (hn : 0 < n) :
widthU (FormalRV.SQIRPort.IQFT n) = n*Qubit count of `IQFT n`** — exactly `n`, no hidden ancilla.
theoremiqft_verified_with_resources
theorem iqft_verified_with_resources (n : Nat) (hn : 0 < n) :
FormalRV.Framework.uc_eval (FormalRV.SQIRPort.IQFT n) = FormalRV.SQIRPort.IQFT_matrix n
∧ cnotCountU (FormalRV.SQIRPort.IQFT n) = 3 * (n / 2) + n * (n - 1)
∧ oneQCountU (FormalRV.SQIRPort.IQFT n) = 3 * (n * (n - 1) / 2) + n + 2
∧ widthU (FormalRV.SQIRPort.IQFT n) = n*The inverse QFT, verified with resources.** The single syntactic object
`IQFT n` is simultaneously:
1. **semantically correct** — its unitary is exactly the ideal `IQFT_matrix n`;
2. **time-counted** — the independent CNOT counter walks its tree to
`3·⌊n/2⌋ + n·(n−1)` (and the 1-qubit counter to `3·(n(n−1)/2) + n + 2`);
3. **space-counted** — the independent width counter walks its tree to `n`.
No resource number floats free of the object; nothing here can cheat, because
the counters live in `Resource/` and import only the IR.
example(example)
example : cnotCountU (FormalRV.SQIRPort.IQFT 2) = 5
example(example)
example : cnotCountU (FormalRV.SQIRPort.IQFT 3) = 9
example(example)
example : widthU (FormalRV.SQIRPort.IQFT 3) = 3
FormalRV.QFT.IQFTDef
FormalRV/QFT/IQFTDef.lean
FormalRV.QFT.IQFTDef
────────────────────
THE definition of the inverse Quantum Fourier Transform (IQFT), as a concrete
`BaseUCom` unitary circuit, together with the ideal matrix it must reproduce.
*Definitions only — no proofs.**
THE circuit is `real_QFTinv_layer n` (also exposed as the framework's
`BaseUCom.QFTinv n`): on `n` qubits it runs a bit-reversal SWAP cascade, then a
countdown of phase ladders — for each target `t = n-1 … 0`, a chain of
controlled phases `controlled_Rz j t (-π/2^(j-t))` (controls `j > t`) followed
by `H t`. THE ideal target is `IQFT_matrix n`, the matrix
`(y,x) ↦ (1/√2ⁿ)·exp(-2πi·x·y/2ⁿ)`.
(The forward `QFT` is a placeholder; the real, verified object in this folder
is the INVERSE QFT — the measurement-basis transform of QPE / Shor.)
Where to look next:
• Circuit correctness (THE main theorem) : `IQFTCorrectness.lean`
• Clifford+T compilation + error budget : `IQFTResource.lean`
• Worked example + QASM emission : `IQFTExample.lean`
• Supporting proofs : `IQFTCircuitCorrectness.lean`,
`IQFTRecursiveArbitrary.lean` (and `IQFTDefinitions.lean` for the helper
defs the proofs run on).
Refs: Nielsen–Chuang §5.1 (QFT); Coppersmith (approximate/banded QFT). The
circuit pieces also live, `{dim}`-polymorphic, in `Framework.QPE` /
`Framework.BaseUCom` (`QFTinv n := real_QFTinv_layer n`, replacing the prior
semantically-wrong `invert (npar_H n)` stub).
example(example)
example (n : Nat) : IQFT n = real_QFTinv_layer n
Smoke: the alias is definitionally the canonical circuit, and its ideal
target is `IQFT_matrix`.
FormalRV.QFT.IQFTDefinitions
FormalRV/QFT/IQFTDefinitions.lean
## §1. Ideal inverse-QFT matrix and its action on Fourier-weighted states
This section is pure linear algebra — the matrix-level target that
any honest `QFTinv` circuit must reproduce.
defIQFT_matrix
noncomputable def IQFT_matrix (m : Nat) :
Matrix (Fin (2^m)) (Fin (2^m)) ℂ*Ideal inverse-QFT matrix.** `IQFT_matrix m y x = (1/√2^m) ·
exp(-2πi · x · y / 2^m)`. This is the matrix-level target for any
correct `QFTinv m` circuit.
defreal_QFTinv_on
noncomputable def real_QFTinv_on : (n : Nat) → BaseUCom n
| 0 => SKIP
| 1 => H 0
| 2 => UCom.seq
(UCom.seq
(UCom.seq (SWAP 0 1) (H 1))
(controlled_Rz 1 0 (-(Real.pi / 2))))
(H 0)
| _+3 => SKIP -- General case: deferred to `real_QFTinv_layer` (see §4)*Real inverse-QFT circuit.** Base cases for `n ≤ 2`; the
recursive case for `n ≥ 3` is provided by `real_QFTinv_layer` below.
For `n = 2`, uses the verified `real_QFTinv2_candidate`.
defreal_QFTinv2_candidate
noncomputable def real_QFTinv2_candidate : BaseUCom 2
*2-qubit inverse-QFT candidate.** Order: `SWAP 0 1 ; H 1 ;
controlled_Rz 1 0 (-π/2) ; H 0`. Hand-verified to equal
`IQFT_matrix 2` (mechanized proof deferred).
Action analysis (each basis vector `|x_0 x_1⟩`):
- `|00⟩ → (1/2)(|00⟩ + |01⟩ + |10⟩ + |11⟩)`
- `|01⟩ → (1/2)(|00⟩ - i|01⟩ - |10⟩ + i|11⟩)`
- `|10⟩ → (1/2)(|00⟩ - |01⟩ + |10⟩ - |11⟩)`
- `|11⟩ → (1/2)(|00⟩ + i|01⟩ - |10⟩ - i|11⟩)`
matching `IQFT_matrix 2`'s columns.
definverse_qft_phase_ladder
noncomputable def inverse_qft_phase_ladder
(n target : Nat) : FormalRV.Framework.BaseUCom n*Phase ladder for inverse QFT on the `target`-th qubit.**
SQIRPort-namespaced n-qubit version. Coexists with the
`{dim}`-polymorphic `Framework.BaseUCom.inverse_qft_phase_ladder`
(moved to the framework 2026-05-26 to support `QFTinv`'s replacement).
Equivalence between the two is established by
`SQIRPort_inverse_qft_phase_ladder_eq_Framework`.
defbit_reversal_swaps
noncomputable def bit_reversal_swaps (n : Nat) : FormalRV.Framework.BaseUCom n
*Bit-reversal SWAP cascade for `n` qubits.** SQIRPort-namespaced
n-qubit version. See `inverse_qft_phase_ladder` for the framework
relationship note.
defreal_QFTinv_layer
noncomputable def real_QFTinv_layer (n : Nat) : FormalRV.Framework.BaseUCom n
*Recursive layer of the real inverse-QFT for `n` qubits.**
SQIRPort-namespaced n-qubit version. See `inverse_qft_phase_ladder`
for the framework relationship note.
defreal_QPE
noncomputable def real_QPE (m anc : Nat) (f : Nat → BaseUCom anc) :
BaseUCom (m + anc)*Real QPE circuit.** `npar_H` (prep) ; `controlled_powers` (oracle
ladder, lifted to the data register) ; `real_QFTinv_on m` (measurement
basis, lifted to the control register).
defiqftHighBit
noncomputable def iqftHighBit (n : Nat) (x : Fin (2^(n+1))) : Fin 2
*High bit of a Fin (2^(n+1)) index.** MSB-first convention: the
high bit is `x.val / 2^n`.
defiqftLowBits
noncomputable def iqftLowBits (n : Nat) (x : Fin (2^(n+1))) : Fin (2^n)
*Lower n bits of a Fin (2^(n+1)) index.** `x.val % 2^n`.
defIQFT_column
noncomputable def IQFT_column (n : Nat) (x : Fin (2^n)) :
Matrix (Fin (2^n)) (Fin 1) ℂ*Ideal IQFT column**: the column vector `IQFT_matrix n · basis_vector (2^n) x.val`.
This is the target of the `real_QFTinv_layer n` action on basis vector `x`.
defswapBits
def swapBits (f : Nat → Bool) (a b : Nat) : Nat → Bool
*Bit-swap on Boolean functions.** Swaps the values at positions
`a` and `b`.
defapplySwapsFrom
def applySwapsFrom (n : Nat) : (k : Nat) → (Nat → Bool) → (Nat → Bool)
| k, f =>
if h : 2 * k + 1 < n then
applySwapsFrom n (k+1) (swapBits f k (n-1-k))
else
f
termination_by k _ => n - 2 * k*Recursive cumulative bit-reversal function.** Result of applying
all SWAPs `(k, n-1-k), (k+1, n-2-k), ...` to `f`. Terminates when
`2k+1 ≥ n` (no more swap pairs).
definverse_qft_ladder_phase_from
noncomputable def inverse_qft_ladder_phase_from
(n target : Nat) (f : Nat → Bool) (k : Nat) : ℂ*Recursive ladder phase scalar.** Product of controlled-Rz phase
factors for controls `j ∈ [k, n)`.
definverse_qft_ladder_phase
noncomputable def inverse_qft_ladder_phase
(n target : Nat) (f : Nat → Bool) : ℂ*Full ladder phase**: the accumulated phase scalar for the
inverse-QFT ladder targeting `target`.
defcountdown_output
noncomputable def countdown_output
(n : Nat) : Nat → (Nat → Bool) → Matrix (Fin (2^n)) (Fin 1) ℂ
| 0, f => f_to_vec n f
| k+1, f =>
inverse_qft_ladder_phase n k f •
(((Real.sqrt 2 / 2 : ℂ) • countdown_output n k (update f k false))
+ ((if f k then -(Real.sqrt 2 / 2 : ℂ) else (Real.sqrt 2 / 2 : ℂ))
• countdown_output n k (update f k true)))*Recursive countdown output.** The expected output of `countdown n k`
applied to `f_to_vec n f`. Mirrors `countdown_succ_acts`: at step k+1,
ladder k is applied first (producing a phase × two-branch sum), then
`countdown_output n k` recursively to each branch.
defbasisFunOfIndex
noncomputable def basisFunOfIndex (n : Nat) (x : Fin (2^n)) : Nat → Bool
Boolean function encoding a `Fin (2^n)` index in MSB-first form.
defbitReversedBasisFun
noncomputable def bitReversedBasisFun (n : Nat) (x : Fin (2^n)) : Nat → Bool
Boolean function after applying the full bit-reversal of `basisFunOfIndex`.
defcountdownColumn
noncomputable def countdownColumn (n : Nat) (x : Fin (2^n)) :
Matrix (Fin (2^n)) (Fin 1) ℂThe countdown column: the result of `real_QFTinv_layer n` applied to
`basis_vector (2^n) x.val`, as an explicit matrix column.
defembedWithExtraBit
noncomputable def embedWithExtraBit
(n : Nat) (extra : Bool)
(v : Matrix (Fin (2^n)) (Fin 1) ℂ) :
Matrix (Fin (2^(n+1))) (Fin 1) ℂ*Embed an n-qubit state into an (n+1)-qubit state by appending
an extra LSB qubit.** Uses `kron_vec` with the n-qubit vector at the
high positions and the 1-qubit extra at the LSB.
defcumulative_extra_phase
noncomputable def cumulative_extra_phase
(n k : Nat) (f : Nat → Bool) : ℂ*Cumulative extra phase**: product over targets `t ∈ [0, k)` of the
phase factor contributed by qubit `n` controlling target `t`.
defiqftHighBitsN
noncomputable def iqftHighBitsN (n : Nat) (y : Fin (2^(n+1))) : Fin (2^n)
*High n bits of an (n+1)-qubit index.** `y.val / 2`.
defiqftLowBitLSB
noncomputable def iqftLowBitLSB (n : Nat) (y : Fin (2^(n+1))) : Fin 2
*LSB of an (n+1)-qubit index.** `y.val % 2`.
defreal_QPE_layer
noncomputable def real_QPE_layer (m anc : Nat) (f : Nat → FormalRV.Framework.BaseUCom anc) :
FormalRV.Framework.BaseUCom (m + anc)*Real QPE circuit using `real_QFTinv_layer`.** The non-stub
counterpart to `real_QPE`. Structure:
`npar_H m ; controlled_powers (lifted f) m ; lifted real_QFTinv_layer m`.
defShor_final_state_lsb
noncomputable def Shor_final_state_lsb (m n anc : Nat)
(f : Nat → FormalRV.Framework.BaseUCom (n + anc)) :
QState (2^m * 2^n * 2^anc)*LSB-compatible Shor final state** (parallel to `Shor_final_state`).
Uses `QPE_var_lsb` (the LSB-oracle-reversed wrapper) instead of `QPE_var`.
This is the state on which the LSB-chain semantic theorems apply
directly; bridging to the published `Shor_final_state` requires a
design decision per the autoresearch protocol.
FormalRV.QFT.IQFTExample
FormalRV/QFT/IQFTExample.lean
FormalRV.QFT.IQFTExample
────────────────────────
A worked example for the inverse QFT + its `UGadget` descriptor for the
uniform `BaseUCom` QASM emitter (`Codegen.UComQasm`), the quantum-side sibling
of the arithmetic `Gadget` / `emitQASM` framework.
This file contains `#eval` demos, so it is kept OFF the default build path
(not imported by the `QFT` umbrella). Build / run on demand:
lake build FormalRV.QFT.IQFTExample
The emitted readable gates are EXACTLY the verified circuit's gates:
• `h q[t]` = `H t` (= `U(π/2,0,π)`)
• `cu1(-pi/2^d) q[j],q[t]` = `controlled_Rz j t (-π/2^d)` (the qelib1 `cu1`
decomposition IS our 5-gate `controlled_Rz`)
• `swap q[i],q[k]` = `SWAP i k`
so `iqftQasmLines n` renders `IQFT n` (= `real_QFTinv_layer n`) faithfully, and
the op-level faithfulness `uprogMat n (emitUComOps (IQFT n)) = uc_eval (IQFT n)`
(from `Codegen.uprogMat_emitUComOps`) plus `iqft_correct` give the punchline
`iqft_emitted_unitary_eq_IQFT_matrix`: the EMITTED circuit's unitary is exactly
the ideal inverse-QFT matrix.
defiqftSwapLines
def iqftSwapLines (n : Nat) : List String
Bit-reversal SWAP lines: `swap q[i],q[n-1-i]` for `i` with `2i+1 < n`.
defiqftLadderLines
def iqftLadderLines (n target : Nat) : List String
Phase-ladder lines for one target: `cu1(-pi/2^(j-t)) q[j],q[t]` for controls
`j > t`, then `h q[t]`.
defiqftQasmLines
def iqftQasmLines (n : Nat) : List String
The full readable OpenQASM body of the n-qubit inverse QFT.
defIQFTGadget
def IQFTGadget : UGadget
The inverse QFT as a uniform `UGadget` descriptor (quantum-side analogue of
the arithmetic `Gadget`). `render = iqftQasmLines` is the computable OpenQASM
body for `IQFT n`; its semantic faithfulness is `iqft_emitted_unitary_eq_IQFT_matrix`.
theoremiqft_emitted_unitary_eq_IQFT_matrix
theorem iqft_emitted_unitary_eq_IQFT_matrix (n : Nat) (hn : 0 < n) :
uprogMat n (emitUComOps (IQFT n)) = IQFT_matrix n*The emitted inverse-QFT circuit's unitary is exactly the ideal
`IQFT_matrix`.** Chains the uniform emitter's faithfulness
(`uprogMat_emitUComOps`, the same `progMat = uc_eval` contract the arithmetic
emitter satisfies) with the circuit-correctness headline `iqft_correct`. So the
OpenQASM we emit denotes, as a unitary, precisely `(y,x) ↦ (1/√2ⁿ)·exp(-2πi·x·y/2ⁿ)`.
defiqft3IoJson
def iqft3IoJson : String
Per-qubit wire names + INPUT/OUTPUT legend for the 3-qubit IQFT diagram.
FormalRV.QFT.IQFTRecursiveArbitrary
FormalRV/QFT/IQFTRecursiveArbitrary.lean
theoremapplySwapsFrom_apply
theorem applySwapsFrom_apply (n : Nat) (f : Nat → Bool) (i : Nat) (hi : i < n) :
applySwapsFrom n 0 f i = f (n - 1 - i)*HEADLINE: Bit-reversal action.** For `i < n`,
`applySwapsFrom n 0 f i = f (n - 1 - i)`.
theorembitReversedBasisFun_succ_extra
theorem bitReversedBasisFun_succ_extra (n : Nat) (x : Fin (2^(n+1))) :
bitReversedBasisFun (n+1) x n = decide ((iqftHighBit n x).val = 1)*Bit-reversal successor extra-bit lemma.** The value of
`bitReversedBasisFun (n+1) x` at the extra LSB position `n` equals
`iqftHighBit n x`.
theoremf_to_vec_congr
theorem f_to_vec_congr (n : Nat) (f g : Nat → Bool)
(hfg : ∀ i, i < n → f i = g i) :
f_to_vec n f = f_to_vec n g`f_to_vec n` depends on `f` only through positions `< n`.
theoreminverse_qft_ladder_phase_from_congr
theorem inverse_qft_ladder_phase_from_congr (n target : Nat) (htarget : target < n)
(f g : Nat → Bool) (hfg : ∀ i, i < n → f i = g i) (k : Nat) :
inverse_qft_ladder_phase_from n target f k
= inverse_qft_ladder_phase_from n target g kCongruence for `inverse_qft_ladder_phase_from` when `target < n`.
theoreminverse_qft_ladder_phase_congr
theorem inverse_qft_ladder_phase_congr (n target : Nat) (htarget : target < n)
(f g : Nat → Bool) (hfg : ∀ i, i < n → f i = g i) :
inverse_qft_ladder_phase n target f
= inverse_qft_ladder_phase n target gCongruence for `inverse_qft_ladder_phase`.
theoremupdate_congr_lt
theorem update_congr_lt (n k : Nat) (f g : Nat → Bool) (b : Bool)
(hfg : ∀ i, i < n → f i = g i) :
∀ i, i < n → (update f k b) i = (update g k b) iIf `f` and `g` agree on positions `< n`, then `update f k b` and `update g k b`
do too.
theoremcountdown_output_congr_input
theorem countdown_output_congr_input (n : Nat) :
∀ k, k ≤ n → ∀ (f g : Nat → Bool), (∀ i, i < n → f i = g i) →
countdown_output n k f = countdown_output n k g*HEADLINE: countdown_output congruence on lower n bits.** If `f` and `g`
agree on positions `< n`, then `countdown_output n k f = countdown_output n k g`
for `k ≤ n`. Proof by induction on k.
theorembitReversedBasisFun_succ_restrict
theorem bitReversedBasisFun_succ_restrict (n : Nat) (x : Fin (2^(n+1))) :
∀ i, i < n →
bitReversedBasisFun (n+1) x i = bitReversedBasisFun n (iqftLowBits n x) i*Bit-reversal successor restrict lemma.** For `i < n`, the value of
`bitReversedBasisFun (n+1) x` at position `i` equals the value of
`bitReversedBasisFun n (iqftLowBits n x)` at position `i`.
theoremembedWithExtraBit_apply
theorem embedWithExtraBit_apply (n : Nat) (extra : Bool)
(v : Matrix (Fin (2^n)) (Fin 1) ℂ) (y : Fin (2^(n+1))) :
embedWithExtraBit n extra v y 0
= (if (iqftLowBitLSB n y).val = (if extra then 1 else 0)
then v (iqftHighBitsN n y) 0
else 0)*Entry formula for `embedWithExtraBit`.** The entry at row `y` is
the corresponding entry of the embedded vector at the high-n part,
gated by the LSB match condition.
theoremcumulative_extra_phase_false_extra
theorem cumulative_extra_phase_false_extra
(n k : Nat) (f : Nat → Bool) (hfn : f n = false) :
cumulative_extra_phase n k f = 1`cumulative_extra_phase` is `1` when the extra bit (`f n`) is `false`.
theoreminverse_qft_ladder_phase_top
theorem inverse_qft_ladder_phase_top (n : Nat) (f : Nat → Bool) :
inverse_qft_ladder_phase (n+1) n f = 1The `(n+1)`-th ladder (target = n) has no controls, so its phase is 1.
theoremupdate_n_lt_eq
theorem update_n_lt_eq (n : Nat) (f : Nat → Bool) (b : Bool) (i : Nat) (hi : i < n) :
(update f n b) i = f i`update f n b` agrees with `f` on positions `< n`.
theoremupdate_n_eval_self
theorem update_n_eval_self (n : Nat) (f : Nat → Bool) (b : Bool) :
(update f n b) n = b`update f n b` evaluates to `b` at position `n`.
theoremcountdownColumn_succ_entry_decomp_corrected
theorem countdownColumn_succ_entry_decomp_corrected
(n : Nat) (_hn : 0 < n)
(x y : Fin (2^(n+1))) :
countdownColumn (n+1) x y 0
= if (iqftLowBitLSB n y).val = 0 then
((Real.sqrt 2 / 2 : ℂ)) *
countdownColumn n (iqftLowBits n x) (iqftHighBitsN n y) 0
else
(if (iqftHighBit n x).val = 1
then -(Real.sqrt 2 / 2 : ℂ)
else (Real.sqrt 2 / 2 : ℂ))
**HEADLINE: Corrected countdownColumn successor entry decomposition.**
For `n ≥ 1`, the `(y, 0)` entry of `countdownColumn (n+1) x` decomposes
based on the LSB of `y`:
- If `LSB(y) = 0`: `(√2/2) * countdownColumn n (iqftLowBits n x) (iqftHighBitsN n y) 0`.
- If `LSB(y) = 1`: `(if iqftHighBit n x = 1 then -(√2/2) else (√2/2))
cumulative_extra_phase n n (update (bitReversedBasisFun (n+1) x) n true)
countdownColumn n (iqftLowBits n x) (iqftHighBitsN n y) 0`.
Note the **update to `n true`** in the cumulative phase: this captures the
"true-branch cumulative phase" (the phase product assuming the extra LSB is `true`),
which is the correct factor regardless of the original value of
`bitReversedBasisFun (n+1) x n`.
theoremcumulative_extra_phase_update_extra_true
theorem cumulative_extra_phase_update_extra_true
(n k : Nat) (hk : k ≤ n) (f : Nat → Bool) :
cumulative_extra_phase n k (update f n true)
= ∏ t ∈ Finset.range k,
(if f t then
Complex.exp ((((-(Real.pi / 2 ^ (n - t))) : ℝ)) * Complex.I)
else 1)*Helper 1**: `cumulative_extra_phase n k (update f n true)` reduces
to a clean product over positions `t < k` of the per-bit phase factor,
controlled only by `f t` (since the extra bit is `true` and `t < k ≤ n`
means the update at position `n` doesn't affect `f t`).
theorembitReversedBasisFun_eq_lsb_bit
theorem bitReversedBasisFun_eq_lsb_bit (n : Nat) (xl : Fin (2^n))
(t : Nat) (ht : t < n) :
bitReversedBasisFun n xl t = decide ((xl.val / 2^t) % 2 = 1)*Helper 2**: After bit-reversal, position `t < n` of
`bitReversedBasisFun n xl` equals the `t`-th LSB bit of `xl.val`.
theoremprod_exp_bits_eq_exp_sum_aux
theorem prod_exp_bits_eq_exp_sum_aux
(n : Nat) (b : Nat → Bool) :
∀ k, k ≤ n →
(∏ t ∈ Finset.range k,
(if b t then
Complex.exp ((((-(Real.pi / 2 ^ (n - t))) : ℝ)) * Complex.I)
else 1))
= Complex.exp
(((-Real.pi
* (((∑ t ∈ Finset.range k,
(if b t then 1 else 0) * 2^t) : Nat) : ℝ)
/ (2^n : ℝ) : ℝ) : ℂ) * Complex.I)*Helper 3** (product-of-exponentials collapse): For any boolean
function `b` and any `k ≤ n`, the product
`∏ t < k, if b t then exp(-π·I/2^(n-t)) else 1` collapses to
`exp(-π·I · S / 2^n)` where `S = ∑ t < k, b_t · 2^t` is the
bit-weighted sum. Proof by induction on `k`, using `Complex.exp_add`
and the arithmetic `1/2^(n-k) = 2^k/2^n` (valid since `k ≤ n`).
theoremcumulative_extra_phase_true_branch_eq_exp
theorem cumulative_extra_phase_true_branch_eq_exp
(n : Nat) (_hn : 0 < n) (x : Fin (2^(n+1))) :
cumulative_extra_phase n n
(update (bitReversedBasisFun (n+1) x) n true)
= Complex.exp
(((-Real.pi
* ((iqftLowBits n x).val : ℝ)
/ (2^n : ℝ) : ℝ) : ℂ) * Complex.I)*HEADLINE: Cumulative extra phase (true branch) = exp.** The
cumulative extra phase scalar in the true branch of
`countdownColumn_succ_entry_decomp_corrected` collapses to a single
complex exponential whose argument is `-π·I · (iqftLowBits n x) / 2^n`.
Combines:
- `cumulative_extra_phase_update_extra_true` (remove the update),
- `bitReversedBasisFun_succ_restrict` (restrict bit-reversal to n),
- `prod_exp_bits_eq_exp_sum_aux` (collapse product to exp of sum),
- `bitReversedBasisFun_eq_lsb_bit` + `binary_expansion_lsb`
(reassemble bit-weighted sum into `(iqftLowBits n x).val`).
theoreminv_sqrt_two_eq_sqrt_two_div_two
theorem inv_sqrt_two_eq_sqrt_two_div_two :
(1 : ℂ) / Real.sqrt 2 = (Real.sqrt 2 / 2 : ℂ)*Sqrt-2 identity**: `1/√2 = √2/2`. Needed to convert
`inv_sqrt_pow_two_succ_factor`'s leading factor into the form used
in `countdownColumn_succ_entry_decomp_corrected`.
theoremIQFT_matrix_succ_entry_decomp_mixed
theorem IQFT_matrix_succ_entry_decomp_mixed
(n : Nat) (_hn : 0 < n) (x y : Fin (2^(n+1))) :
(IQFT_matrix (n+1) * FormalRV.Framework.basis_vector (2^(n+1)) x.val) y 0
= if (iqftLowBitLSB n y).val = 0 then
((Real.sqrt 2 / 2 : ℂ)) *
(IQFT_matrix n
* FormalRV.Framework.basis_vector (2^n) (iqftLowBits n x).val)
(iqftHighBitsN n y) 0
else
(if (iqftHighBit n x).val = 1
then -(Real.sqrt 2 / 2 : ℂ)
else (Real.sqrt 2 / 2 : ℂ))*HEADLINE: IQFT_matrix mixed successor entry decomposition.**
The ideal `IQFT_matrix (n+1)` column entry at `(y, 0)` decomposes
based on the LSB of `y`, into a leading `√2/2` scalar (with possible
sign flip from `iqftHighBit n x`) times the n-bit IQFT_matrix column
entry, plus (in the LSB=1 branch) a `Complex.exp(-π·xl/2^n · I)`
factor. Mirrors `countdownColumn_succ_entry_decomp_corrected` in
shape.
Proof strategy: rewrite both matrix-vector products via
`IQFT_matrix_mul_basis_apply`; unfold `IQFT_matrix`; expand the
exponent via the index decompositions `x.val = xH · 2^n + xL` and
`y.val = yH · 2 + yL`; case-split on `yL` and on `xH ∈ Fin 2`.
The integer piece `xH·yH` collapses via `exp_neg_two_pi_I_mul_nat`;
the half-integer piece `xH` collapses via `exp_neg_pi_I_mul_nat`;
the `1/√2^(n+1)` factor splits via `inv_sqrt_pow_two_succ_factor`
combined with `inv_sqrt_two_eq_sqrt_two_div_two`.
theoremcountdownColumn_succ_entry_eq_IQFT_entry
theorem countdownColumn_succ_entry_eq_IQFT_entry
(n : Nat) (hn : 0 < n)
(x y : Fin (2^(n+1)))
(IH :
countdownColumn n (iqftLowBits n x)
=
IQFT_matrix n * FormalRV.Framework.basis_vector (2^n) (iqftLowBits n x).val) :
countdownColumn (n+1) x y 0
=
(IQFT_matrix (n+1) * FormalRV.Framework.basis_vector (2^(n+1)) x.val) y 0*HEADLINE: Induction step from countdown column to IQFT matrix entry.**
Assuming the IH that `countdownColumn n (iqftLowBits n x)` equals
`IQFT_matrix n · basis_vector (iqftLowBits n x).val`, the entry-level
column equality lifts from `n` to `n+1`. Proof: rewrite LHS via
`countdownColumn_succ_entry_decomp_corrected`, RHS via
`IQFT_matrix_succ_entry_decomp_mixed`; apply IH at the inner entry;
collapse the cumulative phase via `cumulative_extra_phase_true_branch_eq_exp`.
The two `if`-`then`-`else` decompositions match by construction.
theoremcountdownColumn_eq_IQFT_column
theorem countdownColumn_eq_IQFT_column
(n : Nat) (hn : 0 < n) (x : Fin (2^n)) :
countdownColumn n x
= IQFT_matrix n * FormalRV.Framework.basis_vector (2^n) x.val*HEADLINE: Full column theorem.** For all `n ≥ 1` and
`x : Fin (2^n)`, the recursive `countdownColumn n x` equals the
ideal IQFT column `IQFT_matrix n · basis_vector (2^n) x.val`. Proof
by induction on `n`: base case `n = 1` via
`countdownColumn_eq_IQFT_column_one`; successor case via
`countdownColumn_succ_entry_eq_IQFT_entry` applied per entry.
theoremlayer_matrix_correctness_iff_countdownColumn
theorem layer_matrix_correctness_iff_countdownColumn (n : Nat) (hn : 0 < n) :
(FormalRV.Framework.uc_eval (real_QFTinv_layer n : FormalRV.Framework.BaseUCom n)
= IQFT_matrix n)
↔ (∀ x : Fin (2^n),
countdownColumn n x
= IQFT_matrix n * FormalRV.Framework.basis_vector (2^n) x.val)*Equivalence of column equality and layer-matrix correctness.**
The column equality `countdownColumn n x = IQFT_matrix n · basis_vector x.val`
for all `x` is equivalent to `uc_eval (real_QFTinv_layer n) = IQFT_matrix n`
via `matrix_eq_of_basis_action`.
theoremuc_eval_real_QFTinv_layer_eq_IQFT_matrix
theorem uc_eval_real_QFTinv_layer_eq_IQFT_matrix
(n : Nat) (hn : 0 < n) :
FormalRV.Framework.uc_eval
(real_QFTinv_layer n : FormalRV.Framework.BaseUCom n)
= IQFT_matrix n*HEADLINE: Arbitrary-n layer matrix correctness.** For all `n ≥ 1`,
`uc_eval (real_QFTinv_layer n) = IQFT_matrix n`. Direct corollary of
`countdownColumn_eq_IQFT_column` via
`layer_matrix_correctness_iff_countdownColumn`.
theoremcontrolled_Rz_well_typed
theorem controlled_Rz_well_typed {dim : Nat} (q t : Nat) (lam : ℝ)
(hq : q < dim) (ht : t < dim) (hqt : q ≠ t) :
UCom.WellTyped dim (controlled_Rz q t lam : FormalRV.Framework.BaseUCom dim)`controlled_Rz q t λ` is `WellTyped` when both qubits are in range
and distinct. Unfolds to a 5-gate seq: Rz q ; CNOT q t ; Rz t ; CNOT q t ; Rz t.
theoreminverse_qft_phase_ladder_loop_well_typed
theorem inverse_qft_phase_ladder_loop_well_typed
(n target : Nat) (h_target : target < n) :
∀ (m j : Nat), n - j = m → target < j →
UCom.WellTyped n
(inverse_qft_phase_ladder.loop n target j
: FormalRV.Framework.BaseUCom n)The inner `inverse_qft_phase_ladder.loop n target j` recursion is
`WellTyped` for `target < n` and `target < j`. Proof by strong
induction on `n - j`. The hypothesis `target < j` is the loop
invariant (loop always starts at `target + 1`).
theoreminverse_qft_phase_ladder_well_typed
theorem inverse_qft_phase_ladder_well_typed (n target : Nat) (h_target : target < n) :
UCom.WellTyped n
(inverse_qft_phase_ladder n target : FormalRV.Framework.BaseUCom n)`inverse_qft_phase_ladder n target` is `WellTyped` when
`target < n`.
theoremreal_QFTinv_layer_countdown_well_typed
theorem real_QFTinv_layer_countdown_well_typed (n : Nat) (hn : 0 < n) :
∀ k, k ≤ n →
UCom.WellTyped n
(real_QFTinv_layer.countdown n k : FormalRV.Framework.BaseUCom n)The `real_QFTinv_layer.countdown n k` recursion is `WellTyped`
when `0 < n` and `k ≤ n`. Proof by induction on `k`.
theorembit_reversal_swaps_loop_well_typed
theorem bit_reversal_swaps_loop_well_typed (n : Nat) (hn : 0 < n) :
∀ (m k : Nat), n - 2 * k = m →
UCom.WellTyped n
(bit_reversal_swaps.loop n k : FormalRV.Framework.BaseUCom n)The inner `bit_reversal_swaps.loop n k` recursion is `WellTyped`
when `0 < n`. Proof by strong induction on `n - 2 * k`.
theorembit_reversal_swaps_well_typed
theorem bit_reversal_swaps_well_typed (n : Nat) (hn : 0 < n) :
UCom.WellTyped n (bit_reversal_swaps n : FormalRV.Framework.BaseUCom n)`bit_reversal_swaps n` is `WellTyped` when `0 < n`.
theoremwellTyped_real_QFTinv_layer
theorem wellTyped_real_QFTinv_layer (n : Nat) (hn : 0 < n) :
UCom.WellTyped n (real_QFTinv_layer n : FormalRV.Framework.BaseUCom n)*HEADLINE: `real_QFTinv_layer` is well-typed for all `n ≥ 1`.**
Combines bit-reversal well-typedness with countdown well-typedness
via `real_QFTinv_layer_decomp`.
theorembit_reversal_loop_bridge
theorem bit_reversal_loop_bridge (n : Nat) :
∀ (m k : Nat), n - 2 * k = m →
FormalRV.SQIRPort.bit_reversal_swaps.loop n k
= (@FormalRV.Framework.BaseUCom.bit_reversal_swaps.loop n n k
: FormalRV.Framework.BaseUCom n)Loop-level bridge for `bit_reversal_swaps`.
theorembit_reversal_swaps_bridge
theorem bit_reversal_swaps_bridge (n : Nat) :
(FormalRV.SQIRPort.bit_reversal_swaps n : FormalRV.Framework.BaseUCom n)
= (@FormalRV.Framework.BaseUCom.bit_reversal_swaps n n)Top-level bridge for `bit_reversal_swaps`.
theoreminverse_qft_phase_ladder_loop_bridge
theorem inverse_qft_phase_ladder_loop_bridge (n target : Nat) :
∀ (m j : Nat), n - j = m →
FormalRV.SQIRPort.inverse_qft_phase_ladder.loop n target j
= (@FormalRV.Framework.BaseUCom.inverse_qft_phase_ladder.loop n n target j
: FormalRV.Framework.BaseUCom n)Loop-level bridge for `inverse_qft_phase_ladder`.
theoreminverse_qft_phase_ladder_bridge
theorem inverse_qft_phase_ladder_bridge (n target : Nat) :
(FormalRV.SQIRPort.inverse_qft_phase_ladder n target
: FormalRV.Framework.BaseUCom n)
= (@FormalRV.Framework.BaseUCom.inverse_qft_phase_ladder n n target)Top-level bridge for `inverse_qft_phase_ladder`.
theoremreal_QFTinv_layer_countdown_bridge
theorem real_QFTinv_layer_countdown_bridge (n : Nat) :
∀ k,
FormalRV.SQIRPort.real_QFTinv_layer.countdown n k
= (@FormalRV.Framework.BaseUCom.real_QFTinv_layer.countdown n n k
: FormalRV.Framework.BaseUCom n)Countdown-level bridge for `real_QFTinv_layer.countdown`.
theoremreal_QFTinv_layer_bridge
theorem real_QFTinv_layer_bridge (n : Nat) :
(FormalRV.SQIRPort.real_QFTinv_layer n : FormalRV.Framework.BaseUCom n)
= (@FormalRV.Framework.BaseUCom.real_QFTinv_layer n n)*HEADLINE: Top-level bridge for `real_QFTinv_layer`.** Proves
`SQIRPort.real_QFTinv_layer n = Framework.BaseUCom.real_QFTinv_layer n`
as a `BaseUCom n` equality. This is the key bridge: it lets the
SQIRPort correctness theorem transfer to the framework def, which
underlies `Framework.QPE.QFTinv`.
theoremuc_eval_QFTinv_eq_IQFT_matrix
theorem uc_eval_QFTinv_eq_IQFT_matrix (m : Nat) (hm : 0 < m) :
FormalRV.Framework.uc_eval
(FormalRV.Framework.BaseUCom.QFTinv m : FormalRV.Framework.BaseUCom m)
= IQFT_matrix m*HEADLINE: Framework QFTinv matrix correctness.** For all `m ≥ 1`,
`uc_eval (QFTinv m : BaseUCom m) = IQFT_matrix m`. Direct corollary
of `real_QFTinv_layer_bridge` + `uc_eval_real_QFTinv_layer_eq_IQFT_matrix`.
theoremwellTyped_QFTinv
theorem wellTyped_QFTinv (m : Nat) (hm : 0 < m) :
UCom.WellTyped m
(FormalRV.Framework.BaseUCom.QFTinv m : FormalRV.Framework.BaseUCom m)*Framework QFTinv well-typedness wrapper at `dim = m`.** Direct
corollary of `wellTyped_real_QFTinv_layer` + the bridge.
theorembit_reversal_swaps_loop_map_id_bridge
theorem bit_reversal_swaps_loop_map_id_bridge (m anc n : Nat) :
∀ (m_meas k : Nat), n - 2 * k = m_meas →
(@FormalRV.Framework.BaseUCom.bit_reversal_swaps.loop (m + anc) n k
: FormalRV.Framework.BaseUCom (m + anc))
= map_qubits id
(@FormalRV.Framework.BaseUCom.bit_reversal_swaps.loop m n k
: FormalRV.Framework.BaseUCom m)Loop-level bridge for `bit_reversal_swaps`.
theorembit_reversal_swaps_map_id_bridge
theorem bit_reversal_swaps_map_id_bridge (m anc n : Nat) :
(@FormalRV.Framework.BaseUCom.bit_reversal_swaps (m + anc) n
: FormalRV.Framework.BaseUCom (m + anc))
= map_qubits id
(@FormalRV.Framework.BaseUCom.bit_reversal_swaps m n
: FormalRV.Framework.BaseUCom m)Top-level bridge for `bit_reversal_swaps`.
theoreminverse_qft_phase_ladder_loop_map_id_bridge
theorem inverse_qft_phase_ladder_loop_map_id_bridge (m anc n target : Nat) :
∀ (m_meas j : Nat), n - j = m_meas →
(@FormalRV.Framework.BaseUCom.inverse_qft_phase_ladder.loop (m + anc) n target j
: FormalRV.Framework.BaseUCom (m + anc))
= map_qubits id
(@FormalRV.Framework.BaseUCom.inverse_qft_phase_ladder.loop m n target j
: FormalRV.Framework.BaseUCom m)Loop-level bridge for `inverse_qft_phase_ladder`.
theoreminverse_qft_phase_ladder_map_id_bridge
theorem inverse_qft_phase_ladder_map_id_bridge (m anc n target : Nat) :
(@FormalRV.Framework.BaseUCom.inverse_qft_phase_ladder (m + anc) n target
: FormalRV.Framework.BaseUCom (m + anc))
= map_qubits id
(@FormalRV.Framework.BaseUCom.inverse_qft_phase_ladder m n target
: FormalRV.Framework.BaseUCom m)Top-level bridge for `inverse_qft_phase_ladder`.
theoremreal_QFTinv_layer_countdown_map_id_bridge
theorem real_QFTinv_layer_countdown_map_id_bridge (m anc n : Nat) :
∀ k,
(@FormalRV.Framework.BaseUCom.real_QFTinv_layer.countdown (m + anc) n k
: FormalRV.Framework.BaseUCom (m + anc))
= map_qubits id
(@FormalRV.Framework.BaseUCom.real_QFTinv_layer.countdown m n k
: FormalRV.Framework.BaseUCom m)Countdown-level bridge for `real_QFTinv_layer.countdown`.
theoremreal_QFTinv_layer_map_id_bridge
theorem real_QFTinv_layer_map_id_bridge (m anc n : Nat) :
(@FormalRV.Framework.BaseUCom.real_QFTinv_layer (m + anc) n
: FormalRV.Framework.BaseUCom (m + anc))
= map_qubits id
(@FormalRV.Framework.BaseUCom.real_QFTinv_layer m n
: FormalRV.Framework.BaseUCom m)*HEADLINE: Polymorphic-lift bridge for `real_QFTinv_layer`.**
The framework `real_QFTinv_layer n` constructed at `dim = m + anc`
equals the dim-`m` version lifted via `map_qubits id`. Proved by
structural induction over the recursive structure.
FormalRV.QFT.IQFTResource
FormalRV/QFT/IQFTResource.lean
FormalRV.QFT.IQFTResource
─────────────────────────
THE "resource" theorem for the inverse QFT.
Unlike a reversible arithmetic gadget (whose resource is an exact T-count),
the IQFT's controlled phases are continuous rotations, so its hardware cost is
governed by COMPILATION to a finite gate set. The resource story is therefore
the approximate ("banded") QFT compiler:
• `iqft_banded_isCliffordT` — the cutoff-`c` compiled ladder is EXACTLY
Clifford+T for `c ≤ 2` (every kept rotation is depth 0/1 = `S†`/`controlled-S†`,
every dropped one is `SKIP`).
• `iqft_banded_error_budget` — the TOTAL approximation error of the cutoff is
the derived geometric tail `≤ 2π/2^c` (no axiom; chord-≤-arc per drop).
• `iqft_banded_error_to_zero` — that budget is antitone in the cutoff, so it
drives below any target as `c` grows.
• `iqft_banded_semantics` — the compiled ladder's actual action on basis
states is the product of its kept controlled-phase scalars.
EXACT GATE/QUBIT COUNTS (the `Resource/` counters walking THE circuit's
syntax tree — see `IQFTCount.lean`, imported below):
• `Resource.cnotCountU_IQFT` — CNOTs = `3·⌊n/2⌋ + n·(n−1)` (TIME)
• `Resource.oneQCountU_IQFT` — 1q gates = `3·(n(n−1)/2) + n + 2` (TIME)
• `Resource.widthU_IQFT` — qubits = `n`, no hidden ancilla (SPACE)
• `Resource.iqft_verified_with_resources` — semantics + time + space,
all about the SAME syntactic object.
Imports the counts (`IQFTCount`), the compiler (`AQFTCompile`), its semantics
(`AQFTCompileSemantics`), and the elementary error bound (`Core.ApproxQFT`).
These are re-surfaced headlines; proofs live in those files.
theoremiqft_banded_isCliffordT
theorem iqft_banded_isCliffordT {dim : Nat} (c : Nat) (hc : c ≤ 2)
(rs : List PhaseRot) :
IsCliffordT (compileLadder c rs : BaseUCom dim)*Banded IQFT is exactly Clifford+T (THE gate-set resource).** For cutoff
`c ≤ 2`, the compiled phase ladder emits only Clifford+T gates.
theoremiqft_banded_error_budget
theorem iqft_banded_error_budget (c n : ℕ) (hcn : c ≤ n) :
∑ m ∈ Finset.Ico c n, (Real.pi / 2 ^ m) ≤ 2 * Real.pi / 2 ^ c*Banded IQFT error budget (THE approximation resource).** The total cost
of the cutoff-`c` compilation, summed over every dropped depth `c ≤ m < n`, is
at most `2π/2^c` — a closed-form geometric tail, derived (not assumed).
theoremiqft_banded_error_to_zero
theorem iqft_banded_error_to_zero {c c' : ℕ} (h : c ≤ c') :
(2 * Real.pi / 2 ^ c' : ℝ) ≤ 2 * Real.pi / 2 ^ c*The budget → 0 with cutoff.** Increasing the cutoff `c` cannot increase
the error bound `2π/2^c`, so it can be driven below any target.
theoremiqft_banded_semantics
theorem iqft_banded_semantics {dim : Nat} (c : Nat) (rs : List PhaseRot)
(f : Nat → Bool) (hpos : 0 < dim) (hwf : ∀ r ∈ rs, RotWF dim r) :
uc_eval (compileLadder c rs : BaseUCom dim) * f_to_vec dim f
= ladderScalar c rs f • f_to_vec dim f*Banded IQFT semantics.** On any computational-basis state, the compiled
cutoff-`c` ladder acts as the product of its kept controlled-phase scalars
(dropped rotations contribute `1`) — its action is the banded inverse-QFT, not
just its gate count.
FormalRV.QFT.TwoRegisterQFT.Basic
FormalRV/QFT/TwoRegisterQFT/Basic.lean
FormalRV.QFT.TwoRegisterQFT.Basic — a REUSABLE two-register quantum Fourier transform
measurement model, the amplitude/Born-probability layer of the Ekerå–Håstad short-DLP circuit
(and Ekerå's general-DLP circuit — both use the same two-control-register + entangled-target shape).
## The model (1702.00249 §quantum-part l.408–451; 1905.09084 §general DLP)
A run prepares a two-control-register input state with amplitudes `c x y` (`x` in register A of
`2^a` states, `y` in register B of `2^b` states), an oracle entangles a target register via a
function `f : x,y ↦ e` (the measured group element), the QFT of size `2^a` is applied to A and the
QFT of size `2^b` to B, and all three registers are measured.
Using the QFT convention `|x⟩ ↦ (1/√2^a) ∑_j e^{2πi xj/2^a} |j⟩`, the amplitude of measuring
`(j, k, e)` is `(1/√(2^a·2^b)) ∑_{(x,y): f x y = e} c x y · e^{2πi xj/2^a} · e^{2πi yk/2^b}`
(`qft2FiberAmp`), and the probability of the control outcome `(j,k)` — marginalising the target —
is `∑_e ‖qft2FiberAmp …‖²` (`qft2MeasProb`).
## What is reusable here (clear interface)
`qftKernel a x j` — the QFT phase `e^{2πi xj/2^a}`.
`qftAmp a c j` — single-register QFT output amplitude from input amplitudes `c`.
`qft2Amp a b c j k` — two-register QFT output amplitude.
`qft2Amp_factor` — **the structural law**: the two-register QFT is the TENSOR product of
two single-register QFTs (`qft2Amp = qftAmp · qftAmp` when `c` factors).
`qft2FiberAmp` / `qft2MeasProb` — the target-fibre amplitude and the Born probability of `(j,k)`.
`qft2MeasProb_nonneg` — the probability is `≥ 0`.
Instantiate with `c =` (normalised uniform) and `f = (x,y) ↦ x − y·d` to obtain the Ekerå–Håstad
measurement probability; see `EkeraHastadCircuit` and `README.md`.
No `sorry`, no `native_decide`, no axioms beyond the prelude.
defqftKernel
noncomputable def qftKernel (a x j : ℕ) : ℂ
The QFT phase kernel `e^{2πi·x·j / 2^a}`.
defqftAmp
noncomputable def qftAmp (a : ℕ) (c : ℕ → ℂ) (j : ℕ) : ℂ
Single-register QFT output amplitude at outcome `j` from input amplitudes `c : ℕ → ℂ`
(`|ψ⟩ = ∑_{x<2^a} c x |x⟩ ↦ ∑_j (qftAmp a c j) |j⟩`).
defqft2Amp
noncomputable def qft2Amp (a b : ℕ) (c : ℕ → ℕ → ℂ) (j k : ℕ) : ℂ
Two-register QFT output amplitude at `(j,k)` from input amplitudes `c : ℕ → ℕ → ℂ`.
theoremqft2Amp_factor
theorem qft2Amp_factor (a b : ℕ) (c₁ c₂ : ℕ → ℂ) (j k : ℕ) :
qft2Amp a b (fun x y => c₁ x * c₂ y) j k = qftAmp a c₁ j * qftAmp b c₂ k*★ The two-register QFT is the TENSOR of two single-register QFTs. ★** If the input amplitudes
factor as `c x y = c₁ x · c₂ y`, then `qft2Amp = qftAmp(c₁) · qftAmp(c₂)`. This is the structural
reusability law: a multi-register QFT factors over its registers.
defqft2FiberAmp
noncomputable def qft2FiberAmp (a b : ℕ) (c : ℕ → ℕ → ℂ) (f : ℕ → ℕ → ℤ) (j k : ℕ) (e : ℤ) : ℂ
The QFT amplitude of `(j,k)` restricted to the target fibre `f x y = e` (the amplitude of the
joint outcome `|j,k,e⟩`).
defqft2MeasProb
noncomputable def qft2MeasProb (a b : ℕ) (c : ℕ → ℕ → ℂ) (f : ℕ → ℕ → ℤ) (E : Finset ℤ) (j k : ℕ) : ℝ
*Born probability of the control outcome `(j,k)`**, marginalising the target register over the
value set `E` (`= ∑_e ‖amplitude of (j,k,e)‖²`).
theoremqft2MeasProb_nonneg
theorem qft2MeasProb_nonneg (a b : ℕ) (c : ℕ → ℕ → ℂ) (f : ℕ → ℕ → ℤ) (E : Finset ℤ) (j k : ℕ) :
0 ≤ qft2MeasProb a b c f E j kThe Born probability is non-negative.
FormalRV.QFT.TwoRegisterQFT.Circuit
FormalRV/QFT/TwoRegisterQFT/Circuit.lean
FormalRV.QFT.TwoRegisterQFT.Circuit — the GATE-LEVEL two-register QFT as a verified `BaseUCom`.
`Basic.lean` gives the amplitude / Born-probability MODEL of a two-control-register QFT
(`qft2Amp`, `qft2MeasProb`). This file supplies the missing half the model is *about*: an honest
*gate circuit** `twoRegQFT a b : BaseUCom (a + b)`, built by composing the project's fully-verified
single-register inverse-QFT circuit `IQFT` on the two disjoint sub-registers, together with the
*unitary semantic proof** that its `uc_eval` is exactly the tensor product of the two `IQFT_matrix`
factors. This is the structural circuit-level counterpart of `qft2Amp_factor`.
## Construction
twoRegQFT a b
= (IQFT a lifted onto qubits [0,a)) -- `map_qubits id`
; (IQFT b lifted onto qubits [a,a+b)) -- `map_qubits (·+a)`
## Headline (`uc_eval_twoRegQFT_kron`)
uc_eval (twoRegQFT a b) * kron_vec ψc ψd
= kron_vec (IQFT_matrix a * ψc) (IQFT_matrix b * ψd)
i.e. the two-register QFT circuit acts as `IQFT ⊗ IQFT` on the two registers — the same tensor law
the amplitude model `qft2Amp` postulates, now discharged on the genuine gate circuit and reusing
`iqft_correct` per register. `twoRegQFT_wellTyped` makes it pluggable into the `BaseUCom` /
`prob_partial_meas` pipeline.
## Convention note
`IQFT_matrix m y x = (1/√2^m)·e^{-2πi·xy/2^m}` is the INVERSE (measurement-basis) QFT — the transform
QPE / Shor actually apply before measuring. `Basic.qft2Amp` uses the forward kernel `e^{+2πi·xy}`;
the two agree up to `x ↦ −x` (complex conjugation), which leaves every Born probability `‖·‖²`
invariant. So this circuit realizes the EH measurement distribution; the per-fibre amplitude readout
`twoRegQFT_fiberAmp_factor` exposes the realized (inverse-kernel) amplitudes explicitly.
No `sorry`, no `native_decide`, no axioms beyond the prelude.
Layering: this file depends on `FormalRV.QPE.PhaseKickback` (the `map_qubits` kron-factorization
lemmas), which imports `Shor.MainAlgorithm`. It is therefore kept OUT of the Shor-agnostic
`FormalRV.QFT` umbrella and imported directly where the circuit is used (the Ekerå–Håstad audit).
theoremuc_eval_map_qubits_shift_kron_vec
theorem uc_eval_map_qubits_shift_kron_vec {m anc : Nat}
(c : FormalRV.Framework.BaseUCom anc) (h_wt : UCom.WellTyped anc c)
(χ : Matrix (Fin (2 ^ m)) (Fin 1) ℂ) (ψ : Matrix (Fin (2 ^ anc)) (Fin 1) ℂ) :
FormalRV.Framework.uc_eval
(map_qubits (fun q => m + q) c : FormalRV.Framework.BaseUCom (m + anc)) * kron_vec χ ψ
= kron_vec χ (FormalRV.Framework.uc_eval c * ψ)*Shifted (data-register) circuit factorization, general control factor.**
For any well-typed `c : BaseUCom anc`, the lift `map_qubits (·+m) c` onto qubits `[m, m+anc)` leaves an
arbitrary control factor `χ` untouched and applies `uc_eval c` to the data factor.
theoremwellTyped_map_qubits_id_embed
theorem wellTyped_map_qubits_id_embed {dim dim' : Nat} (hle : dim ≤ dim')
(c : FormalRV.Framework.BaseUCom dim) (h_wt : UCom.WellTyped dim c) :
UCom.WellTyped dim' (map_qubits (fun q => q) c : FormalRV.Framework.BaseUCom dim')*Identity-embed well-typedness.** A circuit well-typed on `dim` qubits, embedded by the identity
qubit map into a wider register `dim' ≥ dim`, stays well-typed (every index `< dim ≤ dim'`).
deftwoRegQFT
noncomputable def twoRegQFT (a b : Nat) : FormalRV.Framework.BaseUCom (a + b)
*The two-register QFT gate circuit.** `IQFT a` on the high register `[0,a)` followed by `IQFT b`
on the low register `[a,a+b)` — a genuine `BaseUCom (a+b)` built from the verified single-register
inverse-QFT circuit.
theoremtwoRegQFT_wellTyped
theorem twoRegQFT_wellTyped (a b : Nat) (ha : 0 < a) (hb : 0 < b) :
UCom.WellTyped (a + b) (twoRegQFT a b)*`twoRegQFT` is well-typed** — it touches only qubits `< a + b`, so it plugs into the
`BaseUCom` / `prob_partial_meas` pipeline.
theoremuc_eval_twoRegQFT_kron
theorem uc_eval_twoRegQFT_kron (a b : Nat) (ha : 0 < a) (hb : 0 < b)
(ψc : Matrix (Fin (2 ^ a)) (Fin 1) ℂ) (ψd : Matrix (Fin (2 ^ b)) (Fin 1) ℂ) :
FormalRV.Framework.uc_eval (twoRegQFT a b) * kron_vec ψc ψd
= kron_vec (IQFT_matrix a * ψc) (IQFT_matrix b * ψd)*★ The two-register QFT circuit acts as `IQFT ⊗ IQFT`. ★**
`uc_eval (twoRegQFT a b) * kron_vec ψc ψd = kron_vec (IQFT_matrix a * ψc) (IQFT_matrix b * ψd)`.
The gate-level unitary semantic proof: the circuit realizes the tensor of the two verified
single-register inverse-QFT matrices (`iqft_correct` per register).
theoremiqft_matrix_mulVec_apply
theorem iqft_matrix_mulVec_apply (a : Nat) (ψ : Matrix (Fin (2 ^ a)) (Fin 1) ℂ) (j : Fin (2 ^ a)) :
(IQFT_matrix a * ψ) j 0
= (1 / (Real.sqrt (2 ^ a : ℝ) : ℂ))
* ∑ x : Fin (2 ^ a),
Complex.exp (-(2 * Real.pi * Complex.I) * (x.val : ℂ) * (j.val : ℂ) / (2 ^ a : ℂ))
* ψ x 0*Single-register inverse-QFT amplitude readout.** The realized amplitude at output `j` is the
inverse-QFT of the input: `(1/√2^a) ∑_x e^{-2πi·xj/2^a} ψ_x`. This is the gate-level counterpart of
`Basic.qftAmp` (forward kernel `e^{+2πi·xj}`; the two are complex conjugates, equal under `‖·‖²`).
theoremtwoRegQFT_out_apply
theorem twoRegQFT_out_apply (a b : Nat) (ha : 0 < a) (hb : 0 < b)
(ψc : Matrix (Fin (2 ^ a)) (Fin 1) ℂ) (ψd : Matrix (Fin (2 ^ b)) (Fin 1) ℂ)
(j : Fin (2 ^ a)) (k : Fin (2 ^ b)) :
(FormalRV.Framework.uc_eval (twoRegQFT a b) * kron_vec ψc ψd) (kron_vec_combine j k) 0
= (IQFT_matrix a * ψc) j 0 * (IQFT_matrix b * ψd) k 0*★ Joint output-amplitude factorization (circuit-level `qft2Amp_factor`). ★**
The two-register QFT circuit's output amplitude at the joint control outcome `(j,k)` is the product of
the two single-register inverse-QFT amplitudes — the genuine gate realization of the tensor law that
`Basic.qft2Amp_factor` states for the amplitude model.
FormalRV.QFT.TwoRegisterQFT.CircuitMeasurement
FormalRV/QFT/TwoRegisterQFT/CircuitMeasurement.lean
FormalRV.QFT.TwoRegisterQFT.CircuitMeasurement — the PROJECTION half of the measured two-register
QFT run: it applies the verified QFT gate (`Circuit.lean`) to a post-oracle state and reads off the
control-register Born probability as a `prob_partial_meas` statement of the shape the Shor
measurement pipeline consumes.
## What this adds — and what it does NOT
`Circuit.lean` gives the QFT gate + its unitary semantics. This file models the measured run:
1. `twoRegOracleState a b t c tgt` — the POST-ORACLE 3-register state
`∑_{x<2^a} ∑_{y<2^b} c x y · |x⟩_A |y⟩_B |tgt x y⟩_T`.
*Scope note (honest):** the oracle here is abstracted by its OUTPUT STATE — `twoRegOracleState`
is posited directly, with arbitrary `c, tgt` and NO `BaseUCom`/`uc_eval`/unitarity hypothesis.
This is *weaker* than the single-register pipeline's `MultiplyCircuitProperty`, which pins the
full `uc_eval` action of an actual `BaseUCom` oracle (the post-oracle state is then *derived*).
Realizing `twoRegOracleState` as `entangling-oracle-gate ∘ input-prep` is the remaining open seam;
for the Ekerå–Håstad instantiation the chosen `(c, tgt)` IS the image of the standard reversible
map `|x,y,0⟩ ↦ |x,y,(x−yd)⟩` on a normalized uniform input, but that is true by construction here,
not discharged as a gate property.
2. `twoRegQFTMeasState` — apply `twoRegQFT ⊗ I_target` (the verified QFT on the two control
registers, identity on the target), via `uc_eval_control_register_circuit_kron_vec`. This half
IS gate-honest (genuine `uc_eval` of the verified `twoRegQFT`).
3. `prob_partial_meas (basis_vector (2^(a+b)) ⟨control outcome⟩) twoRegQFTMeasState` — the genuine
Born probability of measuring the two control registers at `(j,k)`, marginalising the target.
## Headline (`prob_partial_meas_twoRegQFTMeasState`)
prob_partial_meas (basis_vector (2^(a+b)) (kron_vec_combine ⟨j⟩ ⟨k⟩).val) (twoRegQFTMeasState …)
= ∑ i : Fin (2^t),
‖∑ x<2^a, ∑ y<2^b with tgt x y = i, c x y · IQFT_matrix a j x · IQFT_matrix b k y‖²
i.e. the genuine circuit Born probability is the fibre-sum over the target register — the
inverse-kernel form of `Basic.qft2MeasProb`. The Ekerå–Håstad instantiation (in the audit) reindexes
the `Fin (2^t)` target sum to the value set `E` and uses the real-input conjugation symmetry to reach
the forward-kernel `qft2MeasProb = ehProb`, after which `ehCircuit_per_run_ge_eighth` lands as a
`prob_partial_meas ≥ 1/8` statement in pipeline form.
No `sorry`, no `native_decide`, no axioms beyond the prelude.
Layering: depends on `Circuit.lean` (→ `PhaseKickback` → `Shor.MainAlgorithm`); kept OUT of the
Shor-agnostic `FormalRV.QFT` umbrella, imported from the audit where it is used.
defcontrolBasis
noncomputable def controlBasis (a b x y : ℕ) : Matrix (Fin (2 ^ (a + b))) (Fin 1) ℂ
The control-register basis state `|x⟩_A |y⟩_B` on the two control registers (`2^a · 2^b` dims).
deftwoRegOracleState
noncomputable def twoRegOracleState (a b t : ℕ) (c : ℕ → ℕ → ℂ) (tgt : ℕ → ℕ → ℕ) :
Matrix (Fin (2 ^ ((a + b) + t))) (Fin 1) ℂ*The post-oracle 3-register state** `∑_{x,y} c x y · |x⟩_A|y⟩_B|tgt x y⟩_T`. The oracle is
abstracted by the value `tgt x y : ℕ` it writes into the target register.
defliftedTwoRegQFT
noncomputable def liftedTwoRegQFT (a b t : ℕ) : FormalRV.Framework.BaseUCom ((a + b) + t)
The two-register QFT lifted over the target register (`QFT ⊗ I_target`).
deftwoRegQFTMeasState
noncomputable def twoRegQFTMeasState (a b t : ℕ) (c : ℕ → ℕ → ℂ) (tgt : ℕ → ℕ → ℕ) :
Matrix (Fin (2 ^ ((a + b) + t))) (Fin 1) ℂ*The measured output state** `(twoRegQFT ⊗ I_target) · (post-oracle state)`.
defqftCtrlAmp
noncomputable def qftCtrlAmp (a b x y : ℕ) : Matrix (Fin (2 ^ (a + b))) (Fin 1) ℂ
The post-QFT control amplitude factor `(IQFT_a |x⟩) ⊗ (IQFT_b |y⟩)` on the two control
registers.
theoremtwoRegQFTMeasState_action
theorem twoRegQFTMeasState_action (a b t : ℕ) (ha : 0 < a) (hb : 0 < b)
(c : ℕ → ℕ → ℂ) (tgt : ℕ → ℕ → ℕ) :
twoRegQFTMeasState a b t c tgt
= ∑ x ∈ Finset.range (2 ^ a), ∑ y ∈ Finset.range (2 ^ b),
c x y • kron_vec (qftCtrlAmp a b x y) (FormalRV.Framework.basis_vector (2 ^ t) (tgt x y))*★ QFT ⊗ I_target action. ★** The measured output state is the post-oracle state with each
control basis pair `|x⟩|y⟩` replaced by its two-register inverse-QFT image `(IQFT_a|x⟩)⊗(IQFT_b|y⟩)`,
the target factor untouched. Reuses `uc_eval_control_register_circuit_kron_vec` (circuit on the
control block, identity on the target) and `uc_eval_twoRegQFT_kron` (the QFT tensor law).
deffiberCtrl
noncomputable def fiberCtrl (a b t : ℕ) (c : ℕ → ℕ → ℂ) (tgt : ℕ → ℕ → ℕ) (i : Fin (2 ^ t)) :
Matrix (Fin (2 ^ (a + b))) (Fin 1) ℂThe control-register amplitude on the target fibre `tgt x y = i`: the part of the post-QFT state
that lands on target basis state `|i⟩`.
theoremtwoRegQFTMeasState_regroup
theorem twoRegQFTMeasState_regroup (a b t : ℕ) (ha : 0 < a) (hb : 0 < b)
(c : ℕ → ℕ → ℂ) (tgt : ℕ → ℕ → ℕ) :
twoRegQFTMeasState a b t c tgt
= ∑ i : Fin (2 ^ t),
kron_vec (fiberCtrl a b t c tgt i) (FormalRV.Framework.basis_vector (2 ^ t) i.val)*Regroup the measured output state by target value.** The state is `∑_{i:Fin 2^t}` of the
fibre-`i` control amplitude tensored with the (distinct, hence orthonormal) target basis state `|i⟩`.
Proven by extensionality — the target basis collapse selects, per composite index, exactly the
matching fibre.
theoremtarget_basis_orthonormal
theorem target_basis_orthonormal (t : ℕ) :
∀ i i' : Fin (2 ^ t),
(∑ y : Fin (2 ^ t),
starRingEnd ℂ (FormalRV.Framework.basis_vector (2 ^ t) i'.val y 0)
* FormalRV.Framework.basis_vector (2 ^ t) i.val y 0)
= if i = i' then (1 : ℂ) else 0Distinct target basis vectors are orthonormal — the hypothesis the orthogonal-sum measurement
lemma needs.
theoremprob_partial_meas_twoRegQFTMeasState
theorem prob_partial_meas_twoRegQFTMeasState (a b t : ℕ) (ha : 0 < a) (hb : 0 < b)
(c : ℕ → ℕ → ℂ) (tgt : ℕ → ℕ → ℕ) (j k : ℕ) (hj : j < 2 ^ a) (hk : k < 2 ^ b) :
prob_partial_meas
(FormalRV.SQIRPort.basis_vector (2 ^ (a + b))
(FormalRV.Framework.kron_vec_combine (⟨j, hj⟩ : Fin (2 ^ a)) (⟨k, hk⟩ : Fin (2 ^ b))).val)
(twoRegQFTMeasState a b t c tgt)
= ∑ i : Fin (2 ^ t),
Complex.normSq
(fiberCtrl a b t c tgt i
(FormalRV.Framework.kron_vec_combine (⟨j, hj⟩ : Fin (2 ^ a)) (⟨k, hk⟩ : Fin (2 ^ b))) 0)*★ The genuine circuit Born probability of control outcome `(j,k)`. ★** Measuring the two
control registers of `twoRegQFTMeasState` (the verified `twoRegQFT ⊗ I_target` applied to the
post-oracle state) at `(j,k)` gives the sum, over target values `i`, of the squared norm of the
fibre-`i` control amplitude — the gate-level realization of `Basic.qft2MeasProb` (inverse kernel).
theoremfiberCtrl_apply_combine
theorem fiberCtrl_apply_combine (a b t : ℕ) (c : ℕ → ℕ → ℂ) (tgt : ℕ → ℕ → ℕ)
(i : Fin (2 ^ t)) (j k : ℕ) (hj : j < 2 ^ a) (hk : k < 2 ^ b) :
fiberCtrl a b t c tgt i
(FormalRV.Framework.kron_vec_combine (⟨j, hj⟩ : Fin (2 ^ a)) (⟨k, hk⟩ : Fin (2 ^ b))) 0
= ∑ x ∈ Finset.range (2 ^ a),
∑ y ∈ (Finset.range (2 ^ b)).filter (fun y => tgt x y = i.val),
c x y * (IQFT_matrix a * FormalRV.Framework.basis_vector (2 ^ a) x)
(⟨j, hj⟩ : Fin (2 ^ a)) 0
* (IQFT_matrix b * FormalRV.Framework.basis_vector (2 ^ b) y)
(⟨k, hk⟩ : Fin (2 ^ b)) 0*Explicit fibre control amplitude.** The fibre-`i` control amplitude evaluated at control
outcome `(j,k)` is the inverse-QFT fibre sum `∑_{x} ∑_{y: tgt x y = i} c x y · IQFT_matrix a j x ·
IQFT_matrix b k y` — the inverse-kernel counterpart of `Basic.qft2FiberAmp`.