ASPBE Lean Blueprint

6.36. QuantumBlockEncoding/StoredSelectedRyTrace.lean🔗

55 explicit public declarations, in source order.

Definition6.36.1
uses 0used by 0✓L∃∀N

Plain-English reading. This abbreviation gives a shorter name to the type or expression used for “coefficients”.

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. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

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. abbrev.

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

Lean code for Definition6.36.1●1 definition
  • abbrevdefined in QuantumBlockEncoding/StoredSelectedRyTrace.lean
    complete
    abbrev QuantumBlockEncoding.StoredSelectedRyTrace.Coefficients (controls : ℕ) :
  Type
    abbrev QuantumBlockEncoding.StoredSelectedRyTrace.Coefficients
  (controls : ℕ) : Type
Definition6.36.2
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “basis index”. The first recursive control selects the high half of the stored array.

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. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

Technical source note. The first recursive control selects the high half of the stored array.

Declaration kind. def.

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

Lean code for Definition6.36.2●1 definition
  • defdefined in QuantumBlockEncoding/StoredSelectedRyTrace.lean
    complete
    def QuantumBlockEncoding.StoredSelectedRyTrace.basisIndex (controls : ℕ) :
  QuantumBlockEncoding.PrimitiveBasis controls → Fin (2 ^ controls)
    def QuantumBlockEncoding.StoredSelectedRyTrace.basisIndex
  (controls : ℕ) :
  QuantumBlockEncoding.PrimitiveBasis
      controls →
    Fin (2 ^ controls)
    The first recursive control selects the high half of the stored array.
Definition6.36.3
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “denote”.

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. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

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. def.

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

Lean code for Definition6.36.3●1 definition
  • defdefined in QuantumBlockEncoding/StoredSelectedRyTrace.lean
    complete
    def QuantumBlockEncoding.StoredSelectedRyTrace.denote {q : ℕ}
  (coefficients :
    QuantumBlockEncoding.StoredSelectedRyTrace.Coefficients q) :
  QuantumBlockEncoding.PrimitiveBasis q → ℚ
    def QuantumBlockEncoding.StoredSelectedRyTrace.denote
  {q : ℕ}
  (coefficients :
    QuantumBlockEncoding.StoredSelectedRyTrace.Coefficients
      q) :
  QuantumBlockEncoding.PrimitiveBasis q →
    ℚ
Definition6.36.4
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “denote bits”.

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. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

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. def.

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

Lean code for Definition6.36.4●1 definition
  • defdefined in QuantumBlockEncoding/StoredSelectedRyTrace.lean
    complete
    def QuantumBlockEncoding.StoredSelectedRyTrace.denoteBits {q : ℕ}
  (bits : Vector (Fin 2) q) : QuantumBlockEncoding.PrimitiveBasis q
    def QuantumBlockEncoding.StoredSelectedRyTrace.denoteBits
  {q : ℕ} (bits : Vector (Fin 2) q) :
  QuantumBlockEncoding.PrimitiveBasis q
Theorem6.36.5
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “basis index injective”; 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. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

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/StoredSelectedRyTrace.lean:47. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.36.5●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredSelectedRyTrace.lean
    complete
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.basisIndex_injective
  (q : ℕ) :
  Function.Injective
    (QuantumBlockEncoding.StoredSelectedRyTrace.basisIndex q)
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.basisIndex_injective
  (q : ℕ) :
  Function.Injective
    (QuantumBlockEncoding.StoredSelectedRyTrace.basisIndex
      q)
Definition6.36.6
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “tail”. Materialize a tail; persistent storage is not treated as a free view.

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. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

Technical source note. Materialize a tail; persistent storage is not treated as a free view.

Declaration kind. def.

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

Lean code for Definition6.36.6●1 definition
  • defdefined in QuantumBlockEncoding/StoredSelectedRyTrace.lean
    complete
    def QuantumBlockEncoding.StoredSelectedRyTrace.tail {α : Type} {q : ℕ}
  (xs : Vector α (q + 1)) :
  QuantumBlockEncoding.StoredGivens.Run (Vector α q)
    def QuantumBlockEncoding.StoredSelectedRyTrace.tail
  {α : Type} {q : ℕ}
  (xs : Vector α (q + 1)) :
  QuantumBlockEncoding.StoredGivens.Run
    (Vector α q)
    Materialize a tail; persistent storage is not treated as a free view.
Theorem6.36.7
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “tail value”; 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. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

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/StoredSelectedRyTrace.lean:74. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.36.7●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredSelectedRyTrace.lean
    complete
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.tail_value {α : Type} {q : ℕ}
  (xs : Vector α (q + 1)) (i : Fin q) :
  (QuantumBlockEncoding.StoredSelectedRyTrace.tail xs).value[↑i] =
    xs[↑i.succ]
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.tail_value
  {α : Type} {q : ℕ}
  (xs : Vector α (q + 1)) (i : Fin q) :
  (QuantumBlockEncoding.StoredSelectedRyTrace.tail
          xs).value[↑i] =
    xs[↑i.succ]
Theorem6.36.8
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “tail cost”; 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. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

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/StoredSelectedRyTrace.lean:78. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.36.8●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredSelectedRyTrace.lean
    complete
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.tail_cost {α : Type} {q : ℕ}
  (xs : Vector α (q + 1)) (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredSelectedRyTrace.tail xs).cost op =
    q *
      (3 *
          QuantumBlockEncoding.StoredGivens.tick
            QuantumBlockEncoding.StoredGivens.Op.read op +
        2 *
          QuantumBlockEncoding.StoredGivens.tick
            QuantumBlockEncoding.StoredGivens.Op.write op)
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.tail_cost
  {α : Type} {q : ℕ}
  (xs : Vector α (q + 1))
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredSelectedRyTrace.tail
          xs).cost
      op =
    q *
      (3 *
          QuantumBlockEncoding.StoredGivens.tick
            QuantumBlockEncoding.StoredGivens.Op.read
            op +
        2 *
          QuantumBlockEncoding.StoredGivens.tick
            QuantumBlockEncoding.StoredGivens.Op.write
            op)
Definition6.36.9
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “half add”.

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. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

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. def.

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

Lean code for Definition6.36.9●1 definition
  • defdefined in QuantumBlockEncoding/StoredSelectedRyTrace.lean
    complete
    def QuantumBlockEncoding.StoredSelectedRyTrace.halfAdd (a b : ℚ) :
  QuantumBlockEncoding.StoredGivens.Run ℚ
    def QuantumBlockEncoding.StoredSelectedRyTrace.halfAdd
  (a b : ℚ) :
  QuantumBlockEncoding.StoredGivens.Run ℚ
Definition6.36.10
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “half sub”.

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. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

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. def.

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

Lean code for Definition6.36.10●1 definition
  • defdefined in QuantumBlockEncoding/StoredSelectedRyTrace.lean
    complete
    def QuantumBlockEncoding.StoredSelectedRyTrace.halfSub (a b : ℚ) :
  QuantumBlockEncoding.StoredGivens.Run ℚ
    def QuantumBlockEncoding.StoredSelectedRyTrace.halfSub
  (a b : ℚ) :
  QuantumBlockEncoding.StoredGivens.Run ℚ
Theorem6.36.11
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “half add value”; 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. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

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/StoredSelectedRyTrace.lean:91. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.36.11●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredSelectedRyTrace.lean
    complete
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.halfAdd_value (a b : ℚ) :
  (QuantumBlockEncoding.StoredSelectedRyTrace.halfAdd a b).value =
    (a + b) / 2
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.halfAdd_value
  (a b : ℚ) :
  (QuantumBlockEncoding.StoredSelectedRyTrace.halfAdd
        a b).value =
    (a + b) / 2
Theorem6.36.12
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “half sub value”; 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. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

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/StoredSelectedRyTrace.lean:92. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.36.12●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredSelectedRyTrace.lean
    complete
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.halfSub_value (a b : ℚ) :
  (QuantumBlockEncoding.StoredSelectedRyTrace.halfSub a b).value =
    (a - b) / 2
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.halfSub_value
  (a b : ℚ) :
  (QuantumBlockEncoding.StoredSelectedRyTrace.halfSub
        a b).value =
    (a - b) / 2
Theorem6.36.13
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “half add cost”; 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. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

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/StoredSelectedRyTrace.lean:94. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.36.13●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredSelectedRyTrace.lean
    complete
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.halfAdd_cost (a b : ℚ)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredSelectedRyTrace.halfAdd a b).cost op =
    2 *
      QuantumBlockEncoding.StoredGivens.tick
        QuantumBlockEncoding.StoredGivens.Op.field op
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.halfAdd_cost
  (a b : ℚ)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredSelectedRyTrace.halfAdd
          a b).cost
      op =
    2 *
      QuantumBlockEncoding.StoredGivens.tick
        QuantumBlockEncoding.StoredGivens.Op.field
        op
Theorem6.36.14
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “half sub cost”; 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. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

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/StoredSelectedRyTrace.lean:98. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.36.14●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredSelectedRyTrace.lean
    complete
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.halfSub_cost (a b : ℚ)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredSelectedRyTrace.halfSub a b).cost op =
    2 *
      QuantumBlockEncoding.StoredGivens.tick
        QuantumBlockEncoding.StoredGivens.Op.field op
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.halfSub_cost
  (a b : ℚ)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredSelectedRyTrace.halfSub
          a b).cost
      op =
    2 *
      QuantumBlockEncoding.StoredGivens.tick
        QuantumBlockEncoding.StoredGivens.Op.field
        op
Definition6.36.15
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “split”. One read of each input coefficient feeds both charged half operations.

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. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

Technical source note. One read of each input coefficient feeds both charged half operations. The pair vector is stored before its two stored projections are constructed.

Declaration kind. def.

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

Lean code for Definition6.36.15●1 definition
  • defdefined in QuantumBlockEncoding/StoredSelectedRyTrace.lean
    complete
    def QuantumBlockEncoding.StoredSelectedRyTrace.split {q : ℕ}
  (xs :
    QuantumBlockEncoding.StoredSelectedRyTrace.Coefficients (q + 1)) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredSelectedRyTrace.Coefficients q ×
      QuantumBlockEncoding.StoredSelectedRyTrace.Coefficients q)
    def QuantumBlockEncoding.StoredSelectedRyTrace.split
  {q : ℕ}
  (xs :
    QuantumBlockEncoding.StoredSelectedRyTrace.Coefficients
      (q + 1)) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredSelectedRyTrace.Coefficients
        q ×
      QuantumBlockEncoding.StoredSelectedRyTrace.Coefficients
        q)
    One read of each input coefficient feeds both charged half operations.
The pair vector is stored before its two stored projections are constructed.
Theorem6.36.16
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “split value”; 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. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

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/StoredSelectedRyTrace.lean:120. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.36.16●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredSelectedRyTrace.lean
    complete
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.split_value {q : ℕ}
  (xs :
    QuantumBlockEncoding.StoredSelectedRyTrace.Coefficients (q + 1)) :
  (QuantumBlockEncoding.StoredSelectedRyTrace.denote
        (QuantumBlockEncoding.StoredSelectedRyTrace.split xs).value.1 =
      fun bits =>
      (QuantumBlockEncoding.StoredSelectedRyTrace.denote xs
            (Fin.cons 0 bits) +
          QuantumBlockEncoding.StoredSelectedRyTrace.denote xs
            (Fin.cons 1 bits)) /
        2) ∧
    QuantumBlockEncoding.StoredSelectedRyTrace.denote
        (QuantumBlockEncoding.StoredSelectedRyTrace.split xs).value.2 =
      fun bits =>
      (QuantumBlockEncoding.StoredSelectedRyTrace.denote xs
            (Fin.cons 0 bits) -
          QuantumBlockEncoding.StoredSelectedRyTrace.denote xs
            (Fin.cons 1 bits)) /
        2
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.split_value
  {q : ℕ}
  (xs :
    QuantumBlockEncoding.StoredSelectedRyTrace.Coefficients
      (q + 1)) :
  (QuantumBlockEncoding.StoredSelectedRyTrace.denote
        (QuantumBlockEncoding.StoredSelectedRyTrace.split
              xs).value.1 =
      fun bits =>
      (QuantumBlockEncoding.StoredSelectedRyTrace.denote
            xs (Fin.cons 0 bits) +
          QuantumBlockEncoding.StoredSelectedRyTrace.denote
            xs (Fin.cons 1 bits)) /
        2) ∧
    QuantumBlockEncoding.StoredSelectedRyTrace.denote
        (QuantumBlockEncoding.StoredSelectedRyTrace.split
              xs).value.2 =
      fun bits =>
      (QuantumBlockEncoding.StoredSelectedRyTrace.denote
            xs (Fin.cons 0 bits) -
          QuantumBlockEncoding.StoredSelectedRyTrace.denote
            xs (Fin.cons 1 bits)) /
        2
Theorem6.36.17
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “split cost”; 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. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

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/StoredSelectedRyTrace.lean:128. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.36.17●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredSelectedRyTrace.lean
    complete
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.split_cost {q : ℕ}
  (xs : QuantumBlockEncoding.StoredSelectedRyTrace.Coefficients (q + 1))
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredSelectedRyTrace.split xs).cost op =
    2 ^ q *
      (4 *
            QuantumBlockEncoding.StoredGivens.tick
              QuantumBlockEncoding.StoredGivens.Op.field op +
          10 *
            QuantumBlockEncoding.StoredGivens.tick
              QuantumBlockEncoding.StoredGivens.Op.read op +
        6 *
          QuantumBlockEncoding.StoredGivens.tick
            QuantumBlockEncoding.StoredGivens.Op.write op)
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.split_cost
  {q : ℕ}
  (xs :
    QuantumBlockEncoding.StoredSelectedRyTrace.Coefficients
      (q + 1))
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredSelectedRyTrace.split
          xs).cost
      op =
    2 ^ q *
      (4 *
            QuantumBlockEncoding.StoredGivens.tick
              QuantumBlockEncoding.StoredGivens.Op.field
              op +
          10 *
            QuantumBlockEncoding.StoredGivens.tick
              QuantumBlockEncoding.StoredGivens.Op.read
              op +
        6 *
          QuantumBlockEncoding.StoredGivens.tick
            QuantumBlockEncoding.StoredGivens.Op.write
            op)
Definition6.36.18
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “append”. A real recursive persistent append: inspect each node and copy each nonempty prefix node.

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. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

Technical source note. A real recursive persistent append: inspect each node and copy each nonempty prefix node. The right list is shared, never traversed here.

Declaration kind. def.

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

Lean code for Definition6.36.18●1 definition
  • defdefined in QuantumBlockEncoding/StoredSelectedRyTrace.lean
    complete
    def QuantumBlockEncoding.StoredSelectedRyTrace.append {α : Type} :
  List α → List α → QuantumBlockEncoding.StoredGivens.Run (List α)
    def QuantumBlockEncoding.StoredSelectedRyTrace.append
  {α : Type} :
  List α →
    List α →
      QuantumBlockEncoding.StoredGivens.Run
        (List α)
    A real recursive persistent append: inspect each node and copy each
nonempty prefix node. The right list is shared, never traversed here.
Theorem6.36.19
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “append value”; 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. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

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/StoredSelectedRyTrace.lean:143. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.36.19●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredSelectedRyTrace.lean
    complete
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.append_value {α : Type}
  (xs ys : List α) :
  (QuantumBlockEncoding.StoredSelectedRyTrace.append xs ys).value =
    xs ++ ys
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.append_value
  {α : Type} (xs ys : List α) :
  (QuantumBlockEncoding.StoredSelectedRyTrace.append
        xs ys).value =
    xs ++ ys
Theorem6.36.20
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “append cost”; 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. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

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/StoredSelectedRyTrace.lean:148. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.36.20●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredSelectedRyTrace.lean
    complete
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.append_cost {α : Type}
  (xs ys : List α) (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredSelectedRyTrace.append xs ys).cost op =
    (xs.length + 1) *
        QuantumBlockEncoding.StoredGivens.tick
          QuantumBlockEncoding.StoredGivens.Op.read op +
      xs.length *
        QuantumBlockEncoding.StoredGivens.tick
          QuantumBlockEncoding.StoredGivens.Op.write op
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.append_cost
  {α : Type} (xs ys : List α)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredSelectedRyTrace.append
          xs ys).cost
      op =
    (xs.length + 1) *
        QuantumBlockEncoding.StoredGivens.tick
          QuantumBlockEncoding.StoredGivens.Op.read
          op +
      xs.length *
        QuantumBlockEncoding.StoredGivens.tick
          QuantumBlockEncoding.StoredGivens.Op.write
          op
Definition6.36.21
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “emit”. Emission and the list-cell write are both charged.

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. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

Technical source note. Emission and the list-cell write are both charged.

Declaration kind. def.

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

Lean code for Definition6.36.21●1 definition
  • defdefined in QuantumBlockEncoding/StoredSelectedRyTrace.lean
    complete
    def QuantumBlockEncoding.StoredSelectedRyTrace.emit {qubits : ℕ}
  (gate : QuantumBlockEncoding.SelectedRyTrace.Gate qubits)
  (rest : List (QuantumBlockEncoding.SelectedRyTrace.Gate qubits)) :
  QuantumBlockEncoding.StoredGivens.Run
    (List (QuantumBlockEncoding.SelectedRyTrace.Gate qubits))
    def QuantumBlockEncoding.StoredSelectedRyTrace.emit
  {qubits : ℕ}
  (gate :
    QuantumBlockEncoding.SelectedRyTrace.Gate
      qubits)
  (rest :
    List
      (QuantumBlockEncoding.SelectedRyTrace.Gate
        qubits)) :
  QuantumBlockEncoding.StoredGivens.Run
    (List
      (QuantumBlockEncoding.SelectedRyTrace.Gate
        qubits))
    Emission and the list-cell write are both charged.
Theorem6.36.22
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “emit value”; 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. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

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/StoredSelectedRyTrace.lean:163. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.36.22●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredSelectedRyTrace.lean
    complete
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.emit_value {qubits : ℕ}
  (gate : QuantumBlockEncoding.SelectedRyTrace.Gate qubits)
  (rest : List (QuantumBlockEncoding.SelectedRyTrace.Gate qubits)) :
  (QuantumBlockEncoding.StoredSelectedRyTrace.emit gate rest).value =
    gate :: rest
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.emit_value
  {qubits : ℕ}
  (gate :
    QuantumBlockEncoding.SelectedRyTrace.Gate
      qubits)
  (rest :
    List
      (QuantumBlockEncoding.SelectedRyTrace.Gate
        qubits)) :
  (QuantumBlockEncoding.StoredSelectedRyTrace.emit
        gate rest).value =
    gate :: rest
Theorem6.36.23
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “emit cost”; 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. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

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/StoredSelectedRyTrace.lean:166. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.36.23●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredSelectedRyTrace.lean
    complete
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.emit_cost {qubits : ℕ}
  (gate : QuantumBlockEncoding.SelectedRyTrace.Gate qubits)
  (rest : List (QuantumBlockEncoding.SelectedRyTrace.Gate qubits))
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredSelectedRyTrace.emit gate rest).cost op =
    QuantumBlockEncoding.StoredGivens.tick
        QuantumBlockEncoding.StoredGivens.Op.emit op +
      QuantumBlockEncoding.StoredGivens.tick
        QuantumBlockEncoding.StoredGivens.Op.write op
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.emit_cost
  {qubits : ℕ}
  (gate :
    QuantumBlockEncoding.SelectedRyTrace.Gate
      qubits)
  (rest :
    List
      (QuantumBlockEncoding.SelectedRyTrace.Gate
        qubits))
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredSelectedRyTrace.emit
          gate rest).cost
      op =
    QuantumBlockEncoding.StoredGivens.tick
        QuantumBlockEncoding.StoredGivens.Op.emit
        op +
      QuantumBlockEncoding.StoredGivens.tick
        QuantumBlockEncoding.StoredGivens.Op.write
        op
Definition6.36.24
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “compile”. The actual recursive stored producer.

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. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

Technical source note. The actual recursive stored producer. The two append traversals copy only the two recursively emitted prefixes, not an already assembled trace.

Declaration kind. def.

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

Lean code for Definition6.36.24●1 definition
  • defdefined in QuantumBlockEncoding/StoredSelectedRyTrace.lean
    complete
    def QuantumBlockEncoding.StoredSelectedRyTrace.compile {qubits : ℕ} (q : ℕ)
  (wires : Vector (Fin qubits) q) (target : Fin qubits) :
  (∀ (i : Fin q), wires[↑i] ≠ target) →
    QuantumBlockEncoding.StoredSelectedRyTrace.Coefficients q →
      QuantumBlockEncoding.StoredGivens.Run
        (List (QuantumBlockEncoding.SelectedRyTrace.Gate qubits))
    def QuantumBlockEncoding.StoredSelectedRyTrace.compile
  {qubits : ℕ} (q : ℕ)
  (wires : Vector (Fin qubits) q)
  (target : Fin qubits) :
  (∀ (i : Fin q), wires[↑i] ≠ target) →
    QuantumBlockEncoding.StoredSelectedRyTrace.Coefficients
        q →
      QuantumBlockEncoding.StoredGivens.Run
        (List
          (QuantumBlockEncoding.SelectedRyTrace.Gate
            qubits))
    The actual recursive stored producer. The two append traversals copy
only the two recursively emitted prefixes, not an already assembled trace.
Theorem6.36.25
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “compile value”; 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. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

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/StoredSelectedRyTrace.lean:195. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.36.25●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredSelectedRyTrace.lean
    complete
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.compile_value {qubits q : ℕ}
  (wires : Vector (Fin qubits) q) (target : Fin qubits)
  (distinct : ∀ (i : Fin q), wires[↑i] ≠ target)
  (xs : QuantumBlockEncoding.StoredSelectedRyTrace.Coefficients q) :
  (QuantumBlockEncoding.StoredSelectedRyTrace.compile q wires target
        distinct xs).value =
    QuantumBlockEncoding.SelectedRyTrace.compile q (fun i => wires[↑i])
      target distinct
      (QuantumBlockEncoding.StoredSelectedRyTrace.denote xs)
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.compile_value
  {qubits q : ℕ}
  (wires : Vector (Fin qubits) q)
  (target : Fin qubits)
  (distinct :
    ∀ (i : Fin q), wires[↑i] ≠ target)
  (xs :
    QuantumBlockEncoding.StoredSelectedRyTrace.Coefficients
      q) :
  (QuantumBlockEncoding.StoredSelectedRyTrace.compile
        q wires target distinct
        xs).value =
    QuantumBlockEncoding.SelectedRyTrace.compile
      q (fun i => wires[↑i]) target
      distinct
      (QuantumBlockEncoding.StoredSelectedRyTrace.denote
        xs)
Theorem6.36.26
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “compile length”; 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. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

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/StoredSelectedRyTrace.lean:208. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.36.26●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredSelectedRyTrace.lean
    complete
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.compile_length {qubits q : ℕ}
  (wires : Vector (Fin qubits) q) (target : Fin qubits)
  (distinct : ∀ (i : Fin q), wires[↑i] ≠ target)
  (xs : QuantumBlockEncoding.StoredSelectedRyTrace.Coefficients q) :
  (QuantumBlockEncoding.StoredSelectedRyTrace.compile q wires target
          distinct xs).value.length =
    2 ^ q + 2 * (2 ^ q - 1)
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.compile_length
  {qubits q : ℕ}
  (wires : Vector (Fin qubits) q)
  (target : Fin qubits)
  (distinct :
    ∀ (i : Fin q), wires[↑i] ≠ target)
  (xs :
    QuantumBlockEncoding.StoredSelectedRyTrace.Coefficients
      q) :
  (QuantumBlockEncoding.StoredSelectedRyTrace.compile
          q wires target distinct
          xs).value.length =
    2 ^ q + 2 * (2 ^ q - 1)
Theorem6.36.27
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “compile refines”; 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. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

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/StoredSelectedRyTrace.lean:215. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.36.27●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredSelectedRyTrace.lean
    complete
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.compile_refines
  {qubits q : ℕ} (wires : Vector (Fin qubits) q) (target : Fin qubits)
  (distinct : ∀ (i : Fin q), wires[↑i] ≠ target)
  (xs : QuantumBlockEncoding.StoredSelectedRyTrace.Coefficients q)
  (angle : QuantumBlockEncoding.ExactAngle) :
  QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.SelectedRyTrace.instantiate angle
        (QuantumBlockEncoding.StoredSelectedRyTrace.compile q wires
            target distinct xs).value) =
    QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.compileUniformlyControlledRy q
        (fun i => wires[↑i]) target distinct fun bits =>
        QuantumBlockEncoding.ExactAngle.scale
          (QuantumBlockEncoding.StoredSelectedRyTrace.denote xs bits)
          angle)
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.compile_refines
  {qubits q : ℕ}
  (wires : Vector (Fin qubits) q)
  (target : Fin qubits)
  (distinct :
    ∀ (i : Fin q), wires[↑i] ≠ target)
  (xs :
    QuantumBlockEncoding.StoredSelectedRyTrace.Coefficients
      q)
  (angle :
    QuantumBlockEncoding.ExactAngle) :
  QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.SelectedRyTrace.instantiate
        angle
        (QuantumBlockEncoding.StoredSelectedRyTrace.compile
            q wires target distinct
            xs).value) =
    QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.compileUniformlyControlledRy
        q (fun i => wires[↑i]) target
        distinct fun bits =>
        QuantumBlockEncoding.ExactAngle.scale
          (QuantumBlockEncoding.StoredSelectedRyTrace.denote
            xs bits)
          angle)
Definition6.36.28
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “trace cost”. This recurrence describes the charged algorithm, including both append traversals and materialization of the control-wire tail at every node.

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. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

Technical source note. This recurrence describes the charged algorithm, including both append traversals and materialization of the control-wire tail at every node.

Declaration kind. def.

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

Lean code for Definition6.36.28●1 definition
  • defdefined in QuantumBlockEncoding/StoredSelectedRyTrace.lean
    complete
    def QuantumBlockEncoding.StoredSelectedRyTrace.traceCost :
  ℕ → QuantumBlockEncoding.StoredGivens.Cost
    def QuantumBlockEncoding.StoredSelectedRyTrace.traceCost :
  ℕ →
    QuantumBlockEncoding.StoredGivens.Cost
    This recurrence describes the charged algorithm, including both append
traversals and materialization of the control-wire tail at every node.
Theorem6.36.29
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “compile cost”; 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. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

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/StoredSelectedRyTrace.lean:235. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.36.29●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredSelectedRyTrace.lean
    complete
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.compile_cost {qubits q : ℕ}
  (wires : Vector (Fin qubits) q) (target : Fin qubits)
  (distinct : ∀ (i : Fin q), wires[↑i] ≠ target)
  (xs : QuantumBlockEncoding.StoredSelectedRyTrace.Coefficients q)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredSelectedRyTrace.compile q wires target
          distinct xs).cost
      op =
    QuantumBlockEncoding.StoredSelectedRyTrace.traceCost q op
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.compile_cost
  {qubits q : ℕ}
  (wires : Vector (Fin qubits) q)
  (target : Fin qubits)
  (distinct :
    ∀ (i : Fin q), wires[↑i] ≠ target)
  (xs :
    QuantumBlockEncoding.StoredSelectedRyTrace.Coefficients
      q)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredSelectedRyTrace.compile
          q wires target distinct xs).cost
      op =
    QuantumBlockEncoding.StoredSelectedRyTrace.traceCost
      q op
Theorem6.36.30
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “trace cost fields”; the hypotheses and conclusion in the code panel fix its exact scope. Exact component counts, written additively to avoid truncated subtraction.

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

Why it is in this chapter. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

Technical source note. Exact component counts, written additively to avoid truncated subtraction.

Declaration kind. theorem.

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

Lean code for Theorem6.36.30●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredSelectedRyTrace.lean
    complete
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.traceCost_fields (q : ℕ) :
  QuantumBlockEncoding.StoredSelectedRyTrace.traceCost q
        QuantumBlockEncoding.StoredGivens.Op.field =
      2 * q * 2 ^ q ∧
    QuantumBlockEncoding.StoredSelectedRyTrace.traceCost q
              QuantumBlockEncoding.StoredGivens.Op.read +
            3 * q +
          2 =
        (8 * q + 3) * 2 ^ q ∧
      QuantumBlockEncoding.StoredSelectedRyTrace.traceCost q
              QuantumBlockEncoding.StoredGivens.Op.write +
            2 * q =
          (6 * q + 1) * 2 ^ q ∧
        QuantumBlockEncoding.StoredSelectedRyTrace.traceCost q
              QuantumBlockEncoding.StoredGivens.Op.emit +
            2 =
          3 * 2 ^ q
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.traceCost_fields
  (q : ℕ) :
  QuantumBlockEncoding.StoredSelectedRyTrace.traceCost
        q
        QuantumBlockEncoding.StoredGivens.Op.field =
      2 * q * 2 ^ q ∧
    QuantumBlockEncoding.StoredSelectedRyTrace.traceCost
              q
              QuantumBlockEncoding.StoredGivens.Op.read +
            3 * q +
          2 =
        (8 * q + 3) * 2 ^ q ∧
      QuantumBlockEncoding.StoredSelectedRyTrace.traceCost
              q
              QuantumBlockEncoding.StoredGivens.Op.write +
            2 * q =
          (6 * q + 1) * 2 ^ q ∧
        QuantumBlockEncoding.StoredSelectedRyTrace.traceCost
              q
              QuantumBlockEncoding.StoredGivens.Op.emit +
            2 =
          3 * 2 ^ q
    Exact component counts, written additively to avoid truncated subtraction.
Theorem6.36.31
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “trace cost unused”; 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. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

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/StoredSelectedRyTrace.lean:267. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.36.31●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredSelectedRyTrace.lean
    complete
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.traceCost_unused (q : ℕ) :
  QuantumBlockEncoding.StoredSelectedRyTrace.traceCost q
        QuantumBlockEncoding.StoredGivens.Op.sqrt =
      0 ∧
    QuantumBlockEncoding.StoredSelectedRyTrace.traceCost q
          QuantumBlockEncoding.StoredGivens.Op.angle =
        0 ∧
      QuantumBlockEncoding.StoredSelectedRyTrace.traceCost q
            QuantumBlockEncoding.StoredGivens.Op.trig =
          0 ∧
        QuantumBlockEncoding.StoredSelectedRyTrace.traceCost q
            QuantumBlockEncoding.StoredGivens.Op.compare =
          0
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.traceCost_unused
  (q : ℕ) :
  QuantumBlockEncoding.StoredSelectedRyTrace.traceCost
        q
        QuantumBlockEncoding.StoredGivens.Op.sqrt =
      0 ∧
    QuantumBlockEncoding.StoredSelectedRyTrace.traceCost
          q
          QuantumBlockEncoding.StoredGivens.Op.angle =
        0 ∧
      QuantumBlockEncoding.StoredSelectedRyTrace.traceCost
            q
            QuantumBlockEncoding.StoredGivens.Op.trig =
          0 ∧
        QuantumBlockEncoding.StoredSelectedRyTrace.traceCost
            q
            QuantumBlockEncoding.StoredGivens.Op.compare =
          0
Theorem6.36.32
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “compile emit”; the hypotheses and conclusion in the code panel fix its exact scope. All instructions, including zero-coefficient rotations, are emitted.

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

Why it is in this chapter. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

Technical source note. All instructions, including zero-coefficient rotations, are emitted.

Declaration kind. theorem.

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

Lean code for Theorem6.36.32●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredSelectedRyTrace.lean
    complete
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.compile_emit {qubits q : ℕ}
  (wires : Vector (Fin qubits) q) (target : Fin qubits)
  (distinct : ∀ (i : Fin q), wires[↑i] ≠ target)
  (xs : QuantumBlockEncoding.StoredSelectedRyTrace.Coefficients q) :
  (QuantumBlockEncoding.StoredSelectedRyTrace.compile q wires target
          distinct xs).cost
      QuantumBlockEncoding.StoredGivens.Op.emit =
    (QuantumBlockEncoding.StoredSelectedRyTrace.compile q wires target
          distinct xs).value.length
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.compile_emit
  {qubits q : ℕ}
  (wires : Vector (Fin qubits) q)
  (target : Fin qubits)
  (distinct :
    ∀ (i : Fin q), wires[↑i] ≠ target)
  (xs :
    QuantumBlockEncoding.StoredSelectedRyTrace.Coefficients
      q) :
  (QuantumBlockEncoding.StoredSelectedRyTrace.compile
          q wires target distinct xs).cost
      QuantumBlockEncoding.StoredGivens.Op.emit =
    (QuantumBlockEncoding.StoredSelectedRyTrace.compile
          q wires target distinct
          xs).value.length
    All instructions, including zero-coefficient rotations, are emitted.
Theorem6.36.33
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “trace cost total”; 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. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

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/StoredSelectedRyTrace.lean:285. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.36.33●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredSelectedRyTrace.lean
    complete
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.traceCost_total (q : ℕ) :
  QuantumBlockEncoding.StoredRectangularGivens.total
          (QuantumBlockEncoding.StoredSelectedRyTrace.traceCost q) +
        5 * q +
      4 =
    (16 * q + 7) * 2 ^ q
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.traceCost_total
  (q : ℕ) :
  QuantumBlockEncoding.StoredRectangularGivens.total
          (QuantumBlockEncoding.StoredSelectedRyTrace.traceCost
            q) +
        5 * q +
      4 =
    (16 * q + 7) * 2 ^ q
Theorem6.36.34
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “compile total cost le”; the hypotheses and conclusion in the code panel fix its exact scope. Polynomial in the local table size 'S = 2^q' and control count 'q'.

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

Why it is in this chapter. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

Technical source note. Polynomial in the local table size 'S = 2^q' and control count 'q'.

Declaration kind. theorem.

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

Lean code for Theorem6.36.34●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredSelectedRyTrace.lean
    complete
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.compile_total_cost_le
  {qubits q : ℕ} (wires : Vector (Fin qubits) q) (target : Fin qubits)
  (distinct : ∀ (i : Fin q), wires[↑i] ≠ target)
  (xs : QuantumBlockEncoding.StoredSelectedRyTrace.Coefficients q) :
  QuantumBlockEncoding.StoredRectangularGivens.total
      (QuantumBlockEncoding.StoredSelectedRyTrace.compile q wires target
          distinct xs).cost ≤
    (16 * q + 7) * 2 ^ q
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.compile_total_cost_le
  {qubits q : ℕ}
  (wires : Vector (Fin qubits) q)
  (target : Fin qubits)
  (distinct :
    ∀ (i : Fin q), wires[↑i] ≠ target)
  (xs :
    QuantumBlockEncoding.StoredSelectedRyTrace.Coefficients
      q) :
  QuantumBlockEncoding.StoredRectangularGivens.total
      (QuantumBlockEncoding.StoredSelectedRyTrace.compile
          q wires target distinct
          xs).cost ≤
    (16 * q + 7) * 2 ^ q
    Polynomial in the local table size `S = 2^q` and control count `q`.
Definition6.36.35
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “join index”. Two explicit index-word operations, locally charged under the field tag.

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. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

Technical source note. Two explicit index-word operations, locally charged under the field tag. This helper makes no claim about the cost of integer multiplication in bits.

Declaration kind. def.

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

Lean code for Definition6.36.35●1 definition
  • defdefined in QuantumBlockEncoding/StoredSelectedRyTrace.lean
    complete
    def QuantumBlockEncoding.StoredSelectedRyTrace.joinIndex {q : ℕ}
  (bit : Fin 2) (rest : Fin (2 ^ q)) :
  QuantumBlockEncoding.StoredGivens.Run (Fin (2 ^ (q + 1)))
    def QuantumBlockEncoding.StoredSelectedRyTrace.joinIndex
  {q : ℕ} (bit : Fin 2)
  (rest : Fin (2 ^ q)) :
  QuantumBlockEncoding.StoredGivens.Run
    (Fin (2 ^ (q + 1)))
    Two explicit index-word operations, locally charged under the field tag.
This helper makes no claim about the cost of integer multiplication in bits.
Definition6.36.36
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “encode”. Convert a stored bit pattern to its array address, with charged tail copies.

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. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

Technical source note. Convert a stored bit pattern to its array address, with charged tail copies.

Declaration kind. def.

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

Lean code for Definition6.36.36●1 definition
  • defdefined in QuantumBlockEncoding/StoredSelectedRyTrace.lean
    complete
    def QuantumBlockEncoding.StoredSelectedRyTrace.encode (q : ℕ) :
  Vector (Fin 2) q → QuantumBlockEncoding.StoredGivens.Run (Fin (2 ^ q))
    def QuantumBlockEncoding.StoredSelectedRyTrace.encode
  (q : ℕ) :
  Vector (Fin 2) q →
    QuantumBlockEncoding.StoredGivens.Run
      (Fin (2 ^ q))
    Convert a stored bit pattern to its array address, with charged tail copies.
Theorem6.36.37
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “encode value”; 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. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

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/StoredSelectedRyTrace.lean:324. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.36.37●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredSelectedRyTrace.lean
    complete
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.encode_value {q : ℕ}
  (bits : Vector (Fin 2) q) :
  (QuantumBlockEncoding.StoredSelectedRyTrace.encode q bits).value =
    QuantumBlockEncoding.StoredSelectedRyTrace.basisIndex q
      (QuantumBlockEncoding.StoredSelectedRyTrace.denoteBits bits)
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.encode_value
  {q : ℕ} (bits : Vector (Fin 2) q) :
  (QuantumBlockEncoding.StoredSelectedRyTrace.encode
        q bits).value =
    QuantumBlockEncoding.StoredSelectedRyTrace.basisIndex
      q
      (QuantumBlockEncoding.StoredSelectedRyTrace.denoteBits
        bits)
Definition6.36.38
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “encoding index operations”. Independent index-operation count; these are the extra local field-tag charges and do not change any existing real/rational field-cost theorem.

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. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

Technical source note. Independent index-operation count; these are the extra local field-tag charges and do not change any existing real/rational field-cost theorem.

Declaration kind. def.

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

Lean code for Definition6.36.38●1 definition
  • defdefined in QuantumBlockEncoding/StoredSelectedRyTrace.lean
    complete
    def QuantumBlockEncoding.StoredSelectedRyTrace.encodingIndexOperations
  (q : ℕ) : ℕ
    def QuantumBlockEncoding.StoredSelectedRyTrace.encodingIndexOperations
  (q : ℕ) : ℕ
    Independent index-operation count; these are the extra local field-tag
charges and do not change any existing real/rational field-cost theorem.
Definition6.36.39
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “encoding cost”.

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. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

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. def.

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

Lean code for Definition6.36.39●1 definition
  • defdefined in QuantumBlockEncoding/StoredSelectedRyTrace.lean
    complete
    def QuantumBlockEncoding.StoredSelectedRyTrace.encodingCost :
  ℕ → QuantumBlockEncoding.StoredGivens.Cost
    def QuantumBlockEncoding.StoredSelectedRyTrace.encodingCost :
  ℕ →
    QuantumBlockEncoding.StoredGivens.Cost
Theorem6.36.40
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “encode cost”; 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. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

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/StoredSelectedRyTrace.lean:345. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.36.40●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredSelectedRyTrace.lean
    complete
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.encode_cost {q : ℕ}
  (bits : Vector (Fin 2) q)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredSelectedRyTrace.encode q bits).cost op =
    QuantumBlockEncoding.StoredSelectedRyTrace.encodingCost q op
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.encode_cost
  {q : ℕ} (bits : Vector (Fin 2) q)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredSelectedRyTrace.encode
          q bits).cost
      op =
    QuantumBlockEncoding.StoredSelectedRyTrace.encodingCost
      q op
Theorem6.36.41
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “encode index operations”; 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. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

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/StoredSelectedRyTrace.lean:353. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.36.41●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredSelectedRyTrace.lean
    complete
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.encode_index_operations
  {q : ℕ} (bits : Vector (Fin 2) q) :
  (QuantumBlockEncoding.StoredSelectedRyTrace.encode q bits).cost
      QuantumBlockEncoding.StoredGivens.Op.field =
    QuantumBlockEncoding.StoredSelectedRyTrace.encodingIndexOperations q
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.encode_index_operations
  {q : ℕ} (bits : Vector (Fin 2) q) :
  (QuantumBlockEncoding.StoredSelectedRyTrace.encode
          q bits).cost
      QuantumBlockEncoding.StoredGivens.Op.field =
    QuantumBlockEncoding.StoredSelectedRyTrace.encodingIndexOperations
      q
Theorem6.36.42
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “encoding cost bound”; 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. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

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/StoredSelectedRyTrace.lean:360. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.36.42●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredSelectedRyTrace.lean
    complete
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.encodingCost_bound (q : ℕ)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  QuantumBlockEncoding.StoredSelectedRyTrace.encodingCost q op ≤
    q *
      (2 *
            QuantumBlockEncoding.StoredGivens.tick
              QuantumBlockEncoding.StoredGivens.Op.field op +
          (3 * q + 1) *
            QuantumBlockEncoding.StoredGivens.tick
              QuantumBlockEncoding.StoredGivens.Op.read op +
        2 * q *
          QuantumBlockEncoding.StoredGivens.tick
            QuantumBlockEncoding.StoredGivens.Op.write op)
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.encodingCost_bound
  (q : ℕ)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  QuantumBlockEncoding.StoredSelectedRyTrace.encodingCost
      q op ≤
    q *
      (2 *
            QuantumBlockEncoding.StoredGivens.tick
              QuantumBlockEncoding.StoredGivens.Op.field
              op +
          (3 * q + 1) *
            QuantumBlockEncoding.StoredGivens.tick
              QuantumBlockEncoding.StoredGivens.Op.read
              op +
        2 * q *
          QuantumBlockEncoding.StoredGivens.tick
            QuantumBlockEncoding.StoredGivens.Op.write
            op)
Definition6.36.43
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “one hot”.

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. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

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. def.

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

Lean code for Definition6.36.43●1 definition
  • defdefined in QuantumBlockEncoding/StoredSelectedRyTrace.lean
    complete
    def QuantumBlockEncoding.StoredSelectedRyTrace.oneHot {q : ℕ}
  (chosen : Fin (2 ^ q)) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredSelectedRyTrace.Coefficients q)
    def QuantumBlockEncoding.StoredSelectedRyTrace.oneHot
  {q : ℕ} (chosen : Fin (2 ^ q)) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredSelectedRyTrace.Coefficients
      q)
Theorem6.36.44
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “one hot value”; 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. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

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/StoredSelectedRyTrace.lean:370. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.36.44●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredSelectedRyTrace.lean
    complete
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.oneHot_value {q : ℕ}
  (chosen : Fin (2 ^ q)) :
  QuantumBlockEncoding.StoredSelectedRyTrace.denote
      (QuantumBlockEncoding.StoredSelectedRyTrace.oneHot chosen).value =
    fun bits =>
    if
        QuantumBlockEncoding.StoredSelectedRyTrace.basisIndex q bits =
          chosen then
      1
    else 0
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.oneHot_value
  {q : ℕ} (chosen : Fin (2 ^ q)) :
  QuantumBlockEncoding.StoredSelectedRyTrace.denote
      (QuantumBlockEncoding.StoredSelectedRyTrace.oneHot
          chosen).value =
    fun bits =>
    if
        QuantumBlockEncoding.StoredSelectedRyTrace.basisIndex
            q bits =
          chosen then
      1
    else 0
Theorem6.36.45
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “one hot cost”; 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. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

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/StoredSelectedRyTrace.lean:375. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.36.45●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredSelectedRyTrace.lean
    complete
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.oneHot_cost {q : ℕ}
  (chosen : Fin (2 ^ q)) (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredSelectedRyTrace.oneHot chosen).cost op =
    2 ^ q *
      (QuantumBlockEncoding.StoredGivens.tick
            QuantumBlockEncoding.StoredGivens.Op.compare op +
          2 *
            QuantumBlockEncoding.StoredGivens.tick
              QuantumBlockEncoding.StoredGivens.Op.read op +
        2 *
          QuantumBlockEncoding.StoredGivens.tick
            QuantumBlockEncoding.StoredGivens.Op.write op)
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.oneHot_cost
  {q : ℕ} (chosen : Fin (2 ^ q))
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredSelectedRyTrace.oneHot
          chosen).cost
      op =
    2 ^ q *
      (QuantumBlockEncoding.StoredGivens.tick
            QuantumBlockEncoding.StoredGivens.Op.compare
            op +
          2 *
            QuantumBlockEncoding.StoredGivens.tick
              QuantumBlockEncoding.StoredGivens.Op.read
              op +
        2 *
          QuantumBlockEncoding.StoredGivens.tick
            QuantumBlockEncoding.StoredGivens.Op.write
            op)
Definition6.36.46
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “selected coefficients”.

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. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

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. def.

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

Lean code for Definition6.36.46●1 definition
  • defdefined in QuantumBlockEncoding/StoredSelectedRyTrace.lean
    complete
    def QuantumBlockEncoding.StoredSelectedRyTrace.selectedCoefficients {q : ℕ}
  (chosen : Vector (Fin 2) q) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredSelectedRyTrace.Coefficients q)
    def QuantumBlockEncoding.StoredSelectedRyTrace.selectedCoefficients
  {q : ℕ} (chosen : Vector (Fin 2) q) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredSelectedRyTrace.Coefficients
      q)
Theorem6.36.47
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “selected coefficients value”; 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. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

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/StoredSelectedRyTrace.lean:385. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.36.47●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredSelectedRyTrace.lean
    complete
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.selectedCoefficients_value
  {q : ℕ} (chosen : Vector (Fin 2) q) :
  QuantumBlockEncoding.StoredSelectedRyTrace.denote
      (QuantumBlockEncoding.StoredSelectedRyTrace.selectedCoefficients
          chosen).value =
    fun bits =>
    if
        bits =
          QuantumBlockEncoding.StoredSelectedRyTrace.denoteBits
            chosen then
      1
    else 0
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.selectedCoefficients_value
  {q : ℕ} (chosen : Vector (Fin 2) q) :
  QuantumBlockEncoding.StoredSelectedRyTrace.denote
      (QuantumBlockEncoding.StoredSelectedRyTrace.selectedCoefficients
          chosen).value =
    fun bits =>
    if
        bits =
          QuantumBlockEncoding.StoredSelectedRyTrace.denoteBits
            chosen then
      1
    else 0
Definition6.36.48
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “selected”.

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. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

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. def.

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

Lean code for Definition6.36.48●1 definition
  • defdefined in QuantumBlockEncoding/StoredSelectedRyTrace.lean
    complete
    def QuantumBlockEncoding.StoredSelectedRyTrace.selected {qubits q : ℕ}
  (wires : Vector (Fin qubits) q) (target : Fin qubits)
  (distinct : ∀ (i : Fin q), wires[↑i] ≠ target)
  (chosen : Vector (Fin 2) q) :
  QuantumBlockEncoding.StoredGivens.Run
    (List (QuantumBlockEncoding.SelectedRyTrace.Gate qubits))
    def QuantumBlockEncoding.StoredSelectedRyTrace.selected
  {qubits q : ℕ}
  (wires : Vector (Fin qubits) q)
  (target : Fin qubits)
  (distinct :
    ∀ (i : Fin q), wires[↑i] ≠ target)
  (chosen : Vector (Fin 2) q) :
  QuantumBlockEncoding.StoredGivens.Run
    (List
      (QuantumBlockEncoding.SelectedRyTrace.Gate
        qubits))
Theorem6.36.49
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “selected value”; 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. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

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/StoredSelectedRyTrace.lean:397. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.36.49●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredSelectedRyTrace.lean
    complete
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.selected_value {qubits q : ℕ}
  (wires : Vector (Fin qubits) q) (target : Fin qubits)
  (distinct : ∀ (i : Fin q), wires[↑i] ≠ target)
  (chosen : Vector (Fin 2) q) :
  (QuantumBlockEncoding.StoredSelectedRyTrace.selected wires target
        distinct chosen).value =
    QuantumBlockEncoding.SelectedRyTrace.selected (fun i => wires[↑i])
      target distinct
      (QuantumBlockEncoding.StoredSelectedRyTrace.denoteBits chosen)
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.selected_value
  {qubits q : ℕ}
  (wires : Vector (Fin qubits) q)
  (target : Fin qubits)
  (distinct :
    ∀ (i : Fin q), wires[↑i] ≠ target)
  (chosen : Vector (Fin 2) q) :
  (QuantumBlockEncoding.StoredSelectedRyTrace.selected
        wires target distinct
        chosen).value =
    QuantumBlockEncoding.SelectedRyTrace.selected
      (fun i => wires[↑i]) target distinct
      (QuantumBlockEncoding.StoredSelectedRyTrace.denoteBits
        chosen)
Theorem6.36.50
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “selected refines”; 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. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

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/StoredSelectedRyTrace.lean:404. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.36.50●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredSelectedRyTrace.lean
    complete
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.selected_refines
  {qubits q : ℕ} (wires : Vector (Fin qubits) q) (target : Fin qubits)
  (distinct : ∀ (i : Fin q), wires[↑i] ≠ target)
  (chosen : Vector (Fin 2) q)
  (angle : QuantumBlockEncoding.ExactAngle) :
  QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.SelectedRyTrace.instantiate angle
        (QuantumBlockEncoding.StoredSelectedRyTrace.selected wires
            target distinct chosen).value) =
    QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.compileSelectedRy (fun i => wires[↑i])
        target distinct
        (QuantumBlockEncoding.StoredSelectedRyTrace.denoteBits chosen)
        angle)
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.selected_refines
  {qubits q : ℕ}
  (wires : Vector (Fin qubits) q)
  (target : Fin qubits)
  (distinct :
    ∀ (i : Fin q), wires[↑i] ≠ target)
  (chosen : Vector (Fin 2) q)
  (angle :
    QuantumBlockEncoding.ExactAngle) :
  QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.SelectedRyTrace.instantiate
        angle
        (QuantumBlockEncoding.StoredSelectedRyTrace.selected
            wires target distinct
            chosen).value) =
    QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.compileSelectedRy
        (fun i => wires[↑i]) target
        distinct
        (QuantumBlockEncoding.StoredSelectedRyTrace.denoteBits
          chosen)
        angle)
Theorem6.36.51
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “selected cost”; 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. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

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/StoredSelectedRyTrace.lean:411. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.36.51●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredSelectedRyTrace.lean
    complete
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.selected_cost {qubits q : ℕ}
  (wires : Vector (Fin qubits) q) (target : Fin qubits)
  (distinct : ∀ (i : Fin q), wires[↑i] ≠ target)
  (chosen : Vector (Fin 2) q)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredSelectedRyTrace.selected wires target
          distinct chosen).cost
      op =
    QuantumBlockEncoding.StoredSelectedRyTrace.encodingCost q op +
        2 ^ q *
          (QuantumBlockEncoding.StoredGivens.tick
                QuantumBlockEncoding.StoredGivens.Op.compare op +
              2 *
                QuantumBlockEncoding.StoredGivens.tick
                  QuantumBlockEncoding.StoredGivens.Op.read op +
            2 *
              QuantumBlockEncoding.StoredGivens.tick
                QuantumBlockEncoding.StoredGivens.Op.write op) +
      QuantumBlockEncoding.StoredSelectedRyTrace.traceCost q op
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.selected_cost
  {qubits q : ℕ}
  (wires : Vector (Fin qubits) q)
  (target : Fin qubits)
  (distinct :
    ∀ (i : Fin q), wires[↑i] ≠ target)
  (chosen : Vector (Fin 2) q)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredSelectedRyTrace.selected
          wires target distinct
          chosen).cost
      op =
    QuantumBlockEncoding.StoredSelectedRyTrace.encodingCost
          q op +
        2 ^ q *
          (QuantumBlockEncoding.StoredGivens.tick
                QuantumBlockEncoding.StoredGivens.Op.compare
                op +
              2 *
                QuantumBlockEncoding.StoredGivens.tick
                  QuantumBlockEncoding.StoredGivens.Op.read
                  op +
            2 *
              QuantumBlockEncoding.StoredGivens.tick
                QuantumBlockEncoding.StoredGivens.Op.write
                op) +
      QuantumBlockEncoding.StoredSelectedRyTrace.traceCost
        q op
Theorem6.36.52
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “selected field tag split”; the hypotheses and conclusion in the code panel fix its exact scope. The local field-tag overcount is exposed separately from rational work.

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

Why it is in this chapter. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

Technical source note. The local field-tag overcount is exposed separately from rational work.

Declaration kind. theorem.

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

Lean code for Theorem6.36.52●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredSelectedRyTrace.lean
    complete
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.selected_field_tag_split
  {qubits q : ℕ} (wires : Vector (Fin qubits) q) (target : Fin qubits)
  (distinct : ∀ (i : Fin q), wires[↑i] ≠ target)
  (chosen : Vector (Fin 2) q) :
  (QuantumBlockEncoding.StoredSelectedRyTrace.selected wires target
          distinct chosen).cost
      QuantumBlockEncoding.StoredGivens.Op.field =
    2 * q * 2 ^ q +
      QuantumBlockEncoding.StoredSelectedRyTrace.encodingIndexOperations
        q
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.selected_field_tag_split
  {qubits q : ℕ}
  (wires : Vector (Fin qubits) q)
  (target : Fin qubits)
  (distinct :
    ∀ (i : Fin q), wires[↑i] ≠ target)
  (chosen : Vector (Fin 2) q) :
  (QuantumBlockEncoding.StoredSelectedRyTrace.selected
          wires target distinct
          chosen).cost
      QuantumBlockEncoding.StoredGivens.Op.field =
    2 * q * 2 ^ q +
      QuantumBlockEncoding.StoredSelectedRyTrace.encodingIndexOperations
        q
    The local field-tag overcount is exposed separately from rational work.
Theorem6.36.53
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “selected length”; 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. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

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/StoredSelectedRyTrace.lean:427. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.36.53●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredSelectedRyTrace.lean
    complete
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.selected_length
  {qubits q : ℕ} (wires : Vector (Fin qubits) q) (target : Fin qubits)
  (distinct : ∀ (i : Fin q), wires[↑i] ≠ target)
  (chosen : Vector (Fin 2) q) :
  (QuantumBlockEncoding.StoredSelectedRyTrace.selected wires target
          distinct chosen).value.length =
    2 ^ q + 2 * (2 ^ q - 1)
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.selected_length
  {qubits q : ℕ}
  (wires : Vector (Fin qubits) q)
  (target : Fin qubits)
  (distinct :
    ∀ (i : Fin q), wires[↑i] ≠ target)
  (chosen : Vector (Fin 2) q) :
  (QuantumBlockEncoding.StoredSelectedRyTrace.selected
          wires target distinct
          chosen).value.length =
    2 ^ q + 2 * (2 ^ q - 1)
Theorem6.36.54
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “selected emit”; 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. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

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/StoredSelectedRyTrace.lean:434. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.36.54●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredSelectedRyTrace.lean
    complete
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.selected_emit {qubits q : ℕ}
  (wires : Vector (Fin qubits) q) (target : Fin qubits)
  (distinct : ∀ (i : Fin q), wires[↑i] ≠ target)
  (chosen : Vector (Fin 2) q) :
  (QuantumBlockEncoding.StoredSelectedRyTrace.selected wires target
          distinct chosen).cost
      QuantumBlockEncoding.StoredGivens.Op.emit =
    (QuantumBlockEncoding.StoredSelectedRyTrace.selected wires target
          distinct chosen).value.length
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.selected_emit
  {qubits q : ℕ}
  (wires : Vector (Fin qubits) q)
  (target : Fin qubits)
  (distinct :
    ∀ (i : Fin q), wires[↑i] ≠ target)
  (chosen : Vector (Fin 2) q) :
  (QuantumBlockEncoding.StoredSelectedRyTrace.selected
          wires target distinct
          chosen).cost
      QuantumBlockEncoding.StoredGivens.Op.emit =
    (QuantumBlockEncoding.StoredSelectedRyTrace.selected
          wires target distinct
          chosen).value.length
Theorem6.36.55
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “selected total cost 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. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

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/StoredSelectedRyTrace.lean:445. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.36.55●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredSelectedRyTrace.lean
    complete
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.selected_total_cost_le
  {qubits q : ℕ} (wires : Vector (Fin qubits) q) (target : Fin qubits)
  (distinct : ∀ (i : Fin q), wires[↑i] ≠ target)
  (chosen : Vector (Fin 2) q) :
  QuantumBlockEncoding.StoredRectangularGivens.total
      (QuantumBlockEncoding.StoredSelectedRyTrace.selected wires target
          distinct chosen).cost ≤
    (16 * q + 12) * 2 ^ q + 5 * q ^ 2 + 3 * q
    theorem QuantumBlockEncoding.StoredSelectedRyTrace.selected_total_cost_le
  {qubits q : ℕ}
  (wires : Vector (Fin qubits) q)
  (target : Fin qubits)
  (distinct :
    ∀ (i : Fin q), wires[↑i] ≠ target)
  (chosen : Vector (Fin 2) q) :
  QuantumBlockEncoding.StoredRectangularGivens.total
      (QuantumBlockEncoding.StoredSelectedRyTrace.selected
          wires target distinct
          chosen).cost ≤
    (16 * q + 12) * 2 ^ q + 5 * q ^ 2 +
      3 * q