This type lists the allowed alternatives for “gate aligned”; its constructors are the cases that downstream code must handle.
inductive GateAligned {qubits : ℕ} (δ : ℝ) : PrimitiveGate qubits → PrimitiveGate qubits → Prop
| unchanged (gate : PrimitiveGate qubits) : GateAligned δ gate gate
| ry (target : Fin qubits) (a b : ExactAngle) (error : |a.eval - b.eval| ≤ δ) :
GateAligned δ (.ry target a) (.ry target b)
/-- A Forall₂ witness preserves every position, physical label and list length. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “aligned”. A Forall₂ witness preserves every position, physical label and list length.
def Aligned {qubits : ℕ} (δ : ℝ) (exact approximate : PrimitiveCircuit qubits) : Prop :=
List.Forall₂ (GateAligned δ) exact approximate
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “touched eq”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem GateAligned.touched_eq {qubits : ℕ} {δ : ℝ} {a b : PrimitiveGate qubits}
(h : GateAligned δ a b) : a.touched = b.touched := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “length eq”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem Aligned.length_eq {qubits : ℕ} {δ : ℝ} {exact approximate : PrimitiveCircuit qubits}
(h : Aligned δ exact approximate) : exact.length = approximate.length :=
List.Forall₂.length_eq h
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “refl”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem Aligned.refl {qubits : ℕ} (δ : ℝ) (circuit : PrimitiveCircuit qubits) :
Aligned δ circuit circuit := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “distance le”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem GateAligned.distance_le {qubits : ℕ} {δ : ℝ} (hδ : 0 ≤ δ)
{exact approximate : PrimitiveGate qubits} (h : GateAligned δ exact approximate) :
‖evalPrimitiveGate approximate - evalPrimitiveGate exact‖ ≤ δ / 2 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “aligned eval distance le”; the hypotheses and conclusion in the code panel fix its exact scope. No gate order is commuted: each induction step matches the actual evaluator.
theorem aligned_eval_distance_le {qubits : ℕ} {δ : ℝ} (hδ : 0 ≤ δ)
{exact approximate : PrimitiveCircuit qubits} (aligned : Aligned δ exact approximate) :
‖evalPrimitiveCircuit approximate - evalPrimitiveCircuit exact‖ ≤
(exact.length : ℝ) * δ / 2 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “aligned eval clm distance le”; the hypotheses and conclusion in the code panel fix its exact scope. Explicit Euclidean CLM formulation prevents accidental entrywise-norm use.
theorem aligned_eval_clm_distance_le {qubits : ℕ} {δ : ℝ} (hδ : 0 ≤ δ)
{exact approximate : PrimitiveCircuit qubits} (aligned : Aligned δ exact approximate) :
‖_root_.Matrix.toEuclideanCLM (𝕜 := ℂ) (n := PrimitiveBasis qubits)
(evalPrimitiveCircuit approximate - evalPrimitiveCircuit exact)‖ ≤
(exact.length : ℝ) * δ / 2 := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “hermite angle budget”. Sufficient uniform RY-angle budget for the existing actual prepare list.
noncomputable def hermiteAngleBudget (k n : ℕ) (ε : ℝ) : ℝ :=
ε / (24 * ((n + 1 : ℕ) : ℝ) * ((2 * k + 6 : ℕ) : ℝ)^3)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “hermite angle budget nonneg”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem hermiteAngleBudget_nonneg (k n : ℕ) {ε : ℝ} (hε : 0 ≤ ε) :
0 ≤ hermiteAngleBudget k n ε := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “prepare conditional distance le”; the hypotheses and conclusion in the code panel fix its exact scope. A conditional consumer of the actual constructed Hermite circuit and its existing gate-count theorem.
theorem prepare_conditional_distance_le (k n : ℕ) (L : ℝ) {ε : ℝ} (hε : 0 ≤ ε)
(approximate : PrimitiveCircuit ((n + 1) + HermiteFiniteChain.bondQubits k))
(aligned : Aligned (hermiteAngleBudget k n ε)
(ConstructiveHermitePreparation.prepare k n L) approximate) :
‖evalPrimitiveCircuit approximate -
evalPrimitiveCircuit (ConstructiveHermitePreparation.prepare k n L)‖ ≤ ε := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “prepare conditional clm distance le”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem prepare_conditional_clm_distance_le (k n : ℕ) (L : ℝ) {ε : ℝ} (hε : 0 ≤ ε)
(approximate : PrimitiveCircuit ((n + 1) + HermiteFiniteChain.bondQubits k))
(aligned : Aligned (hermiteAngleBudget k n ε)
(ConstructiveHermitePreparation.prepare k n L) approximate) :
‖_root_.Matrix.toEuclideanCLM (𝕜 := ℂ)
(n := PrimitiveBasis ((n + 1) + HermiteFiniteChain.bondQubits k))
(evalPrimitiveCircuit approximate -
evalPrimitiveCircuit (ConstructiveHermitePreparation.prepare k n L))‖ ≤ ε := by
commit-pinned source · Verso Blueprint panel