This definition gives the library's named construction or computation for “normalized source”. Normalize the formula-derived cores using the local norm, not a full sample sum.
noncomputable def normalizedSource (k n : ℕ) (L : ℝ) : Chain (n + 1) 1 1 :=
MatrixProductChain.ofKernel (kernel k n L)
(fun a => rawInitial k n L a / localSampleNorm k n L) (terminal k) 0 n
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “normalized source eq source”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem normalizedSource_eq_source (k n : ℕ) (L : ℝ) (hL : 0 < L) :
normalizedSource k n L = sourceChain k n L :=
(sourceChain_eq_local k n L hL).symm
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “normalized source max bond”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem normalizedSource_maxBond (k n : ℕ) (L : ℝ) :
maxBond (normalizedSource k n L) ≤ 2 * k + 6 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “normalized source normalized”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem normalizedSource_normalized (k n : ℕ) (L : ℝ) (hL : 0 < L) :
(∑ x : Word (n + 1), (contract (normalizedSource k n L) x 0 0) ^ 2) = 1 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “normalized source contract”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem normalizedSource_contract (k n : ℕ) (L : ℝ) (hL : 0 < L)
(x : Word (n + 1)) :
contract (normalizedSource k n L) x 0 0 =
HermiteStatePreparation.sampledAmplitude k (n + 1) L (sampleEquiv (n + 1) x) /
HermiteStatePreparation.sampleNorm k (n + 1) L := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “prepare”. The actual finite primitive list; no circuit witness is selected.
noncomputable def prepare (k n : ℕ) (L : ℝ) : PrimitiveCircuit ((n + 1) + bondQubits k) :=
ConstructiveTensorTrainCompiler.compile (normalizedSource k n L)
((normalizedSource_maxBond k n L).trans (bond_fits k))
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “prepare gate count”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem prepare_gateCount (k n : ℕ) (L : ℝ) :
(prepare k n L).gateCount ≤ 48 * (n + 1) * (2 * k + 6) ^ 3 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “prepare depth”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem prepare_depth (k n : ℕ) (L : ℝ) :
(prepare k n L).resource.depth ≤ 48 * (n + 1) * (2 * k + 6) ^ 3 :=
(prepare k n L).resource_depth_le_gateCount.trans (prepare_gateCount k n L)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “prepare columns”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem prepare_columns (k n : ℕ) (L : ℝ) (hL : 0 < L)
(x : PrimitiveBasis (n + 1)) (b : PrimitiveBasis (bondQubits k)) :
evalPrimitiveCircuit (prepare k n L) (Fin.append x b) (fun _ => 0) =
if b = (fun _ => 0) then
HermiteStatePreparation.normalizedAmplitude k (n + 1) L
(primitiveBasisLEEquiv (n + 1) x) else 0 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “prepare spec”; the hypotheses and conclusion in the code panel fix its exact scope. Literal source semantics, all clean/non-clean output sectors, full unitary, and gate/depth bounds for this particular constructed circuit.
theorem prepare_spec (k n : ℕ) (L : ℝ) (hL : 0 < L) :
(prepare k n L).gateCount ≤ 48 * (n + 1) * (2 * k + 6) ^ 3 ∧
(prepare k n L).resource.depth ≤ 48 * (n + 1) * (2 * k + 6) ^ 3 ∧
(prepare k n L).resource.oracleCalls = 0 ∧
evalPrimitiveCircuit (prepare k n L) ∈
_root_.Matrix.unitaryGroup (PrimitiveBasis ((n + 1) + bondQubits k)) ℂ ∧
∀ (x : PrimitiveBasis (n + 1)) (b : PrimitiveBasis (bondQubits k)),
evalPrimitiveCircuit (prepare k n L) (Fin.append x b) (fun _ => 0) =
if b = (fun _ => 0) then
HermiteStatePreparation.normalizedAmplitude k (n + 1) L
(primitiveBasisLEEquiv (n + 1) x) else 0 :=
commit-pinned source · Verso Blueprint panel