This definition gives the library's named construction or computation for “grid point”. Left-inclusive, right-exclusive grid on '[-πL,πL)' when 'L>0'.
def gridPoint (n : ℕ) (L : ℝ) (j : Fin (gridSize n)) : ℝ :=
-Real.pi * L + (j.val : ℝ) * (2 * Real.pi * L / (gridSize n : ℝ))
/-- The physical sample, without changing the polynomial on the splice interval. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “sampled amplitude”. The physical sample, without changing the polynomial on the splice interval.
def sampledAmplitude (k n : ℕ) (L : ℝ) (j : Fin (gridSize n)) : ℝ :=
smoothInitial k (gridPoint n L j)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “sampled amplitude pos”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem sampledAmplitude_pos (k n : ℕ) (L : ℝ) (j : Fin (gridSize n)) :
0 < sampledAmplitude k n L j := smoothInitial_pos _ _
/-- The true Euclidean normalizer of the complete finite sample table. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “sample norm”. The true Euclidean normalizer of the complete finite sample table.
def sampleNorm (k n : ℕ) (L : ℝ) : ℝ :=
Real.sqrt (∑ j, sampledAmplitude k n L j ^ 2)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “sample norm pos”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem sampleNorm_pos (k n : ℕ) (L : ℝ) : 0 < sampleNorm k n L := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “normalized amplitude”.
def normalizedAmplitude (k n : ℕ) (L : ℝ) (j : Fin (gridSize n)) : ℂ :=
((sampledAmplitude k n L j / sampleNorm k n L : ℝ) : ℂ)
/-- An actual list of primitive instructions on precisely `n` wires. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “hermite circuit”. An actual list of primitive instructions on precisely 'n' wires.
def hermiteCircuit (k n : ℕ) (L : ℝ) : PrimitiveCircuit n :=
prepareCircuit n (fun b => sampledAmplitude k n L (primitiveBasisLEEquiv n b))
/-- The exact primitive denotation, reindexed by little-endian integers. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “hermite unitary”. The exact primitive denotation, reindexed by little-endian integers.
def hermiteUnitary (k n : ℕ) (L : ℝ) :
_root_.Matrix (Fin (gridSize n)) (Fin (gridSize n)) ℂ :=
prepareMatrixLE (sampledAmplitude k n L)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “hermite unitary eq circuit”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem hermiteUnitary_eq_circuit (k n : ℕ) (L : ℝ) :
hermiteUnitary k n L =
_root_.Matrix.reindexAlgEquiv ℂ ℂ (primitiveBasisLEEquiv n)
(evalPrimitiveCircuit (hermiteCircuit k n L)) := rfl
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “hermite unitary unitary”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem hermiteUnitary_unitary (k n : ℕ) (L : ℝ) :
hermiteUnitary k n L ∈ _root_.Matrix.unitaryGroup (Fin (gridSize n)) ℂ :=
prepareMatrixLE_unitary _
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “hermite first column”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem hermite_firstColumn (k n : ℕ) (L : ℝ) (j : Fin (gridSize n)) :
hermiteUnitary k n L j (zeroBasisIndex n) = normalizedAmplitude k n L j :=
prepareMatrixLE_firstColumn _ (sampledAmplitude_pos k n L) j
/-- Every squared norm is included, including both exponential tails and the splice. -/
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “hermite normalized”; the hypotheses and conclusion in the code panel fix its exact scope. Every squared norm is included, including both exponential tails and the splice.
theorem hermite_normalized (k n : ℕ) (L : ℝ) :
(∑ j, Complex.normSq (normalizedAmplitude k n L j)) = 1 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “hermite state action”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem hermite_stateAction (k n : ℕ) (L : ℝ) :
applyVec (hermiteUnitary k n L) (zeroKet n) = normalizedAmplitude k n L := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “hermite ry count”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem hermite_ryCount (k n : ℕ) (L : ℝ) :
(hermiteCircuit k n L).ryCount = 2 ^ n - 1 := prepareCircuit_ryCount _
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “hermite cx count”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem hermite_cxCount (k n : ℕ) (L : ℝ) :
(hermiteCircuit k n L).cxCount = 2 * (2 ^ n - 1 - n) := prepareCircuit_cxCount _
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “hermite oracle calls”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem hermite_oracleCalls (k n : ℕ) (L : ℝ) :
(hermiteCircuit k n L).resource.oracleCalls = 0 := prepareCircuit_oracleCalls _
/-- The circuit has exactly the data register and no allocated ancillary wire. -/
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “hermite no ancilla”; the hypotheses and conclusion in the code panel fix its exact scope. The circuit has exactly the data register and no allocated ancillary wire.
theorem hermite_noAncilla (k n : ℕ) (L : ℝ) :
(hermiteCircuit k n L).resource.pureAncilla = 0 := rfl
/-- The closed symbolic root: normalization, genuine unitarity, primitive
state action and exact reference compiler resources are proved together. -/
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “hermite state preparation complete”; the hypotheses and conclusion in the code panel fix its exact scope. The closed symbolic root: normalization, genuine unitarity, primitive state action and exact reference compiler resources are proved together.
theorem hermiteStatePreparation_complete (k n : ℕ) (L : ℝ) :
0 < sampleNorm k n L ∧
(∑ j, Complex.normSq (normalizedAmplitude k n L j)) = 1 ∧
hermiteUnitary k n L ∈ _root_.Matrix.unitaryGroup (Fin (gridSize n)) ℂ ∧
applyVec (hermiteUnitary k n L) (zeroKet n) = normalizedAmplitude k n L ∧
(hermiteCircuit k n L).ryCount = 2 ^ n - 1 ∧
(hermiteCircuit k n L).cxCount = 2 * (2 ^ n - 1 - n) ∧
(hermiteCircuit k n L).resource.oracleCalls = 0 :=
⟨sampleNorm_pos k n L, hermite_normalized k n L, hermiteUnitary_unitary k n L,
hermite_stateAction k n L, hermite_ryCount k n L, hermite_cxCount k n L,
hermite_oracleCalls k n L⟩
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “hermite certificate”. Integration into the existing concrete state-preparation certificate API.
def hermiteCertificate (k n : ℕ) (L : ℝ) : ComplexStatePreparationCertificate n where
target := {
amplitudes := normalizedAmplitude k n L
normalization := (∑ j, Complex.normSq (normalizedAmplitude k n L j)) = 1
source := "Exact exponential–Hermite–exponential initial datum on a little-endian grid"
}
gate := {
matrix := hermiteUnitary k n L
unitary := hermiteUnitary_unitary k n L
}
normalizationProof := hermite_normalized k n L
commit-pinned source · Verso Blueprint panel