ASPBE Lean Blueprint

10.16. QuantumBlockEncoding/HermiteSampleStructure.lean🔗

4 explicit public declarations, in source order.

Definition10.16.1
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “cut sample index”. Concatenate a most-significant prefix and a least-significant suffix.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. Concatenate a most-significant prefix and a least-significant suffix. This is an index map only; it allocates no amplitude table.

Declaration kind. def.

Source: QuantumBlockEncoding/HermiteSampleStructure.lean:12. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition10.16.1●1 definition
  • defdefined in QuantumBlockEncoding/HermiteSampleStructure.lean
    complete
    def QuantumBlockEncoding.HermiteSampleStructure.cutSampleIndex
  (pWidth sWidth : ℕ) (x : Fin (QuantumBlockEncoding.gridSize pWidth))
  (y : Fin (QuantumBlockEncoding.gridSize sWidth)) :
  Fin (QuantumBlockEncoding.gridSize (pWidth + sWidth))
    def QuantumBlockEncoding.HermiteSampleStructure.cutSampleIndex
  (pWidth sWidth : ℕ)
  (x :
    Fin
      (QuantumBlockEncoding.gridSize
        pWidth))
  (y :
    Fin
      (QuantumBlockEncoding.gridSize
        sWidth)) :
  Fin
    (QuantumBlockEncoding.gridSize
      (pWidth + sWidth))
    Concatenate a most-significant prefix and a least-significant suffix.
This is an index map only; it allocates no amplitude table.
Theorem10.16.2
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “sampled cut factorization”; the hypotheses and conclusion in the code panel fix its exact scope. The rank certificate applies to the actual frozen sample API at every cut, including empty prefix/suffix cuts.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. The rank certificate applies to the actual frozen sample API at every cut, including empty prefix/suffix cuts. It is not a claim about a numerical SVD.

Declaration kind. theorem.

Source: QuantumBlockEncoding/HermiteSampleStructure.lean:27. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.16.2●1 theorem
  • theoremdefined in QuantumBlockEncoding/HermiteSampleStructure.lean
    complete
    theorem QuantumBlockEncoding.HermiteSampleStructure.sampled_cut_factorization
  (k pWidth sWidth : ℕ) (L : ℝ) (hL : 0 < L) :
  QuantumBlockEncoding.HermiteCutRank.FactorsThrough fun x y =>
    QuantumBlockEncoding.HermiteStatePreparation.sampledAmplitude k
      (pWidth + sWidth) L
      (QuantumBlockEncoding.HermiteSampleStructure.cutSampleIndex pWidth
        sWidth x y)
    theorem QuantumBlockEncoding.HermiteSampleStructure.sampled_cut_factorization
  (k pWidth sWidth : ℕ) (L : ℝ)
  (hL : 0 < L) :
  QuantumBlockEncoding.HermiteCutRank.FactorsThrough
    fun x y =>
    QuantumBlockEncoding.HermiteStatePreparation.sampledAmplitude
      k (pWidth + sWidth) L
      (QuantumBlockEncoding.HermiteSampleStructure.cutSampleIndex
        pWidth sWidth x y)
    The rank certificate applies to the actual frozen sample API at every cut,
including empty prefix/suffix cuts. It is not a claim about a numerical SVD.
Theorem10.16.3
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “sampled cut rank le”; the hypotheses and conclusion in the code panel fix its exact scope.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/HermiteSampleStructure.lean:41. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.16.3●1 theorem
  • theoremdefined in QuantumBlockEncoding/HermiteSampleStructure.lean
    complete
    theorem QuantumBlockEncoding.HermiteSampleStructure.sampled_cut_rank_le
  (k pWidth sWidth : ℕ) (L : ℝ) (hL : 0 < L) :
  (Matrix.rank fun x y =>
      QuantumBlockEncoding.HermiteStatePreparation.sampledAmplitude k
        (pWidth + sWidth) L
        (QuantumBlockEncoding.HermiteSampleStructure.cutSampleIndex
          pWidth sWidth x y)) ≤
    8 * k + 12
    theorem QuantumBlockEncoding.HermiteSampleStructure.sampled_cut_rank_le
  (k pWidth sWidth : ℕ) (L : ℝ)
  (hL : 0 < L) :
  (Matrix.rank fun x y =>
      QuantumBlockEncoding.HermiteStatePreparation.sampledAmplitude
        k (pWidth + sWidth) L
        (QuantumBlockEncoding.HermiteSampleStructure.cutSampleIndex
          pWidth sWidth x y)) ≤
    8 * k + 12
Theorem10.16.4
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “normalized cut factorization”; the hypotheses and conclusion in the code panel fix its exact scope. The real amplitudes underlying the public complex state retain the same factor width after exact normalization.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. The real amplitudes underlying the public complex state retain the same factor width after exact normalization.

Declaration kind. theorem.

Source: QuantumBlockEncoding/HermiteSampleStructure.lean:50. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.16.4●1 theorem
  • theoremdefined in QuantumBlockEncoding/HermiteSampleStructure.lean
    complete
    theorem QuantumBlockEncoding.HermiteSampleStructure.normalized_cut_factorization
  (k pWidth sWidth : ℕ) (L : ℝ) (hL : 0 < L) :
  QuantumBlockEncoding.HermiteCutRank.FactorsThrough fun x y =>
    QuantumBlockEncoding.HermiteStatePreparation.sampledAmplitude k
        (pWidth + sWidth) L
        (QuantumBlockEncoding.HermiteSampleStructure.cutSampleIndex
          pWidth sWidth x y) /
      QuantumBlockEncoding.HermiteStatePreparation.sampleNorm k
        (pWidth + sWidth) L
    theorem QuantumBlockEncoding.HermiteSampleStructure.normalized_cut_factorization
  (k pWidth sWidth : ℕ) (L : ℝ)
  (hL : 0 < L) :
  QuantumBlockEncoding.HermiteCutRank.FactorsThrough
    fun x y =>
    QuantumBlockEncoding.HermiteStatePreparation.sampledAmplitude
        k (pWidth + sWidth) L
        (QuantumBlockEncoding.HermiteSampleStructure.cutSampleIndex
          pWidth sWidth x y) /
      QuantumBlockEncoding.HermiteStatePreparation.sampleNorm
        k (pWidth + sWidth) L
    The real amplitudes underlying the public complex state retain the same
factor width after exact normalization.