6.12. QuantumBlockEncoding/TextbookStatePreparation.lean🔗

29 explicit public declarations, in source order.

Definition6.12.1

uses 0used by 0✓L∃∀N

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

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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Definition6.12.1●1 definition

defdefined in QuantumBlockEncoding/TextbookStatePreparation.lean

complete

def QuantumBlockEncoding.TextbookStatePreparation.zeroIndex :
  Fin (QuantumBlockEncoding.gridSize 1)

def QuantumBlockEncoding.TextbookStatePreparation.zeroIndex :
  Fin (QuantumBlockEncoding.gridSize 1)

Definition6.12.2

uses 0used by 0✓L∃∀N

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

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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Definition6.12.2●1 definition

defdefined in QuantumBlockEncoding/TextbookStatePreparation.lean

complete

def QuantumBlockEncoding.TextbookStatePreparation.oneIndex :
  Fin (QuantumBlockEncoding.gridSize 1)

def QuantumBlockEncoding.TextbookStatePreparation.oneIndex :
  Fin (QuantumBlockEncoding.gridSize 1)

Definition6.12.3

uses 0used by 0✓L∃∀N

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

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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Definition6.12.3●1 definition

defdefined in QuantumBlockEncoding/TextbookStatePreparation.lean

complete

def QuantumBlockEncoding.TextbookStatePreparation.pauliX :
  QuantumBlockEncoding.ConcreteSemantics.FiniteMatrix
    (QuantumBlockEncoding.gridSize 1) (QuantumBlockEncoding.gridSize 1)
    ℂ

def QuantumBlockEncoding.TextbookStatePreparation.pauliX :
  QuantumBlockEncoding.ConcreteSemantics.FiniteMatrix
    (QuantumBlockEncoding.gridSize 1)
    (QuantumBlockEncoding.gridSize 1) ℂ

Theorem6.12.4

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “pauli x unitary”; the hypotheses and conclusion in the code panel fix its exact scope. The Pauli X matrix is unitary in Mathlib's standard unitary group.

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

Why it is in this chapter. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

Technical source note. The Pauli X matrix is unitary in Mathlib's standard unitary group.

Declaration kind. theorem.

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

Lean code for Theorem6.12.4●1 theorem

theoremdefined in QuantumBlockEncoding/TextbookStatePreparation.lean

complete

theorem QuantumBlockEncoding.TextbookStatePreparation.pauliX_unitary :
  QuantumBlockEncoding.TextbookStatePreparation.pauliX ∈
    Matrix.unitaryGroup (Fin (QuantumBlockEncoding.gridSize 1)) ℂ

theorem QuantumBlockEncoding.TextbookStatePreparation.pauliX_unitary :
  QuantumBlockEncoding.TextbookStatePreparation.pauliX ∈
    Matrix.unitaryGroup
      (Fin
        (QuantumBlockEncoding.gridSize 1))
      ℂ

The Pauli X matrix is unitary in Mathlib's standard unitary group.

Definition6.12.5

uses 0used by 0✓L∃∀N

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

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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Definition6.12.5●1 definition

defdefined in QuantumBlockEncoding/TextbookStatePreparation.lean

complete

def QuantumBlockEncoding.TextbookStatePreparation.oneState :
  QuantumBlockEncoding.ConcreteSemantics.StateVector
    (QuantumBlockEncoding.gridSize 1) ℂ

def QuantumBlockEncoding.TextbookStatePreparation.oneState :
  QuantumBlockEncoding.ConcreteSemantics.StateVector
    (QuantumBlockEncoding.gridSize 1) ℂ

Definition6.12.6

uses 0used by 0✓L∃∀N

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

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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Definition6.12.6●1 definition

defdefined in QuantumBlockEncoding/TextbookStatePreparation.lean

complete

def QuantumBlockEncoding.TextbookStatePreparation.oneTarget :
  QuantumBlockEncoding.StatePreparationTarget ℂ 1

def QuantumBlockEncoding.TextbookStatePreparation.oneTarget :
  QuantumBlockEncoding.StatePreparationTarget
    ℂ 1

Theorem6.12.7

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “one target normalized”; 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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Theorem6.12.7●1 theorem

theoremdefined in QuantumBlockEncoding/TextbookStatePreparation.lean

complete

theorem QuantumBlockEncoding.TextbookStatePreparation.oneTarget_normalized :
  QuantumBlockEncoding.TextbookStatePreparation.oneTarget.normalization

theorem QuantumBlockEncoding.TextbookStatePreparation.oneTarget_normalized :
  QuantumBlockEncoding.TextbookStatePreparation.oneTarget.normalization

Theorem6.12.8

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “pauli x prepares one”; 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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Theorem6.12.8●1 theorem

theoremdefined in QuantumBlockEncoding/TextbookStatePreparation.lean

complete

theorem QuantumBlockEncoding.TextbookStatePreparation.pauliX_prepares_one :
  QuantumBlockEncoding.ConcreteSemantics.applyVec
      QuantumBlockEncoding.TextbookStatePreparation.pauliX
      (QuantumBlockEncoding.ConcreteSemantics.zeroKet 1) =
    QuantumBlockEncoding.TextbookStatePreparation.oneTarget.amplitudes

theorem QuantumBlockEncoding.TextbookStatePreparation.pauliX_prepares_one :
  QuantumBlockEncoding.ConcreteSemantics.applyVec
      QuantumBlockEncoding.TextbookStatePreparation.pauliX
      (QuantumBlockEncoding.ConcreteSemantics.zeroKet
        1) =
    QuantumBlockEncoding.TextbookStatePreparation.oneTarget.amplitudes

Definition6.12.9

uses 0used by 0✓L∃∀N

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

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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Definition6.12.9●1 definition

defdefined in QuantumBlockEncoding/TextbookStatePreparation.lean

complete

def QuantumBlockEncoding.TextbookStatePreparation.pauliXGate :
  QuantumBlockEncoding.ConcreteSemantics.ComplexUnitaryGate 1

def QuantumBlockEncoding.TextbookStatePreparation.pauliXGate :
  QuantumBlockEncoding.ConcreteSemantics.ComplexUnitaryGate
    1

Definition6.12.10

uses 0used by 0✓L∃∀N

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

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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Definition6.12.10●1 definition

defdefined in QuantumBlockEncoding/TextbookStatePreparation.lean

complete

def QuantumBlockEncoding.TextbookStatePreparation.pauliXCertificate :
  QuantumBlockEncoding.ConcreteSemantics.ComplexStatePreparationCertificate
    1

def QuantumBlockEncoding.TextbookStatePreparation.pauliXCertificate :
  QuantumBlockEncoding.ConcreteSemantics.ComplexStatePreparationCertificate
    1

Definition6.12.11

uses 0used by 0✓L∃∀N

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

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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Definition6.12.11●1 definition

defdefined in QuantumBlockEncoding/TextbookStatePreparation.lean

complete

def QuantumBlockEncoding.TextbookStatePreparation.pauliXCircuit :
  QuantumBlockEncoding.Circuit

def QuantumBlockEncoding.TextbookStatePreparation.pauliXCircuit :
  QuantumBlockEncoding.Circuit

Definition6.12.12

uses 0used by 0✓L∃∀N

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

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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Definition6.12.12●1 definition

defdefined in QuantumBlockEncoding/TextbookStatePreparation.lean

complete

def QuantumBlockEncoding.TextbookStatePreparation.pauliXVerified :
  QuantumBlockEncoding.VerifiedStatePreparation ℂ 1

def QuantumBlockEncoding.TextbookStatePreparation.pauliXVerified :
  QuantumBlockEncoding.VerifiedStatePreparation
    ℂ 1

Theorem6.12.13

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “pauli x verified 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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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/TextbookStatePreparation.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.12.13●1 theorem

theoremdefined in QuantumBlockEncoding/TextbookStatePreparation.lean

complete

theorem QuantumBlockEncoding.TextbookStatePreparation.pauliXVerified_cost :
  QuantumBlockEncoding.TextbookStatePreparation.pauliXVerified.candidate.cost =
    { auxiliaryQubits := 0, gateCount := 1, depth := 1,
      oracleCalls := 0 }

theorem QuantumBlockEncoding.TextbookStatePreparation.pauliXVerified_cost :
  QuantumBlockEncoding.TextbookStatePreparation.pauliXVerified.candidate.cost =
    { auxiliaryQubits := 0,
      gateCount := 1, depth := 1,
      oracleCalls := 0 }

Definition6.12.14

uses 0used by 0✓L∃∀N

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

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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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/TextbookStatePreparation.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.12.14●1 definition

defdefined in QuantumBlockEncoding/TextbookStatePreparation.lean

complete

def QuantumBlockEncoding.TextbookStatePreparation.invSqrtTwo : ℂ

def QuantumBlockEncoding.TextbookStatePreparation.invSqrtTwo :
  ℂ

Theorem6.12.15

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “inv sqrt two mul self”; 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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Theorem6.12.15●1 theorem

theoremdefined in QuantumBlockEncoding/TextbookStatePreparation.lean

complete

theorem QuantumBlockEncoding.TextbookStatePreparation.invSqrtTwo_mul_self :
  QuantumBlockEncoding.TextbookStatePreparation.invSqrtTwo *
      QuantumBlockEncoding.TextbookStatePreparation.invSqrtTwo =
    1 / 2

theorem QuantumBlockEncoding.TextbookStatePreparation.invSqrtTwo_mul_self :
  QuantumBlockEncoding.TextbookStatePreparation.invSqrtTwo *
      QuantumBlockEncoding.TextbookStatePreparation.invSqrtTwo =
    1 / 2

Definition6.12.16

uses 0used by 0✓L∃∀N

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

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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Definition6.12.16●1 definition

defdefined in QuantumBlockEncoding/TextbookStatePreparation.lean

complete

def QuantumBlockEncoding.TextbookStatePreparation.hadamard :
  QuantumBlockEncoding.ConcreteSemantics.FiniteMatrix
    (QuantumBlockEncoding.gridSize 1) (QuantumBlockEncoding.gridSize 1)
    ℂ

def QuantumBlockEncoding.TextbookStatePreparation.hadamard :
  QuantumBlockEncoding.ConcreteSemantics.FiniteMatrix
    (QuantumBlockEncoding.gridSize 1)
    (QuantumBlockEncoding.gridSize 1) ℂ

Theorem6.12.17

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “star hadamard”; 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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Theorem6.12.17●1 theorem

theoremdefined in QuantumBlockEncoding/TextbookStatePreparation.lean

complete

theorem QuantumBlockEncoding.TextbookStatePreparation.star_hadamard :
  star QuantumBlockEncoding.TextbookStatePreparation.hadamard =
    QuantumBlockEncoding.TextbookStatePreparation.hadamard

theorem QuantumBlockEncoding.TextbookStatePreparation.star_hadamard :
  star
      QuantumBlockEncoding.TextbookStatePreparation.hadamard =
    QuantumBlockEncoding.TextbookStatePreparation.hadamard

Theorem6.12.18

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “hadamard unitary”; 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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Theorem6.12.18●1 theorem

theoremdefined in QuantumBlockEncoding/TextbookStatePreparation.lean

complete

theorem QuantumBlockEncoding.TextbookStatePreparation.hadamard_unitary :
  QuantumBlockEncoding.TextbookStatePreparation.hadamard ∈
    Matrix.unitaryGroup (Fin (QuantumBlockEncoding.gridSize 1)) ℂ

theorem QuantumBlockEncoding.TextbookStatePreparation.hadamard_unitary :
  QuantumBlockEncoding.TextbookStatePreparation.hadamard ∈
    Matrix.unitaryGroup
      (Fin
        (QuantumBlockEncoding.gridSize 1))
      ℂ

Definition6.12.19

uses 0used by 0✓L∃∀N

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

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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Definition6.12.19●1 definition

defdefined in QuantumBlockEncoding/TextbookStatePreparation.lean

complete

def QuantumBlockEncoding.TextbookStatePreparation.plusState :
  QuantumBlockEncoding.ConcreteSemantics.StateVector
    (QuantumBlockEncoding.gridSize 1) ℂ

def QuantumBlockEncoding.TextbookStatePreparation.plusState :
  QuantumBlockEncoding.ConcreteSemantics.StateVector
    (QuantumBlockEncoding.gridSize 1) ℂ

Definition6.12.20

uses 0used by 0✓L∃∀N

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

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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Definition6.12.20●1 definition

defdefined in QuantumBlockEncoding/TextbookStatePreparation.lean

complete

def QuantumBlockEncoding.TextbookStatePreparation.plusTarget :
  QuantumBlockEncoding.StatePreparationTarget ℂ 1

def QuantumBlockEncoding.TextbookStatePreparation.plusTarget :
  QuantumBlockEncoding.StatePreparationTarget
    ℂ 1

Theorem6.12.21

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “plus target normalized”; 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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Theorem6.12.21●1 theorem

theoremdefined in QuantumBlockEncoding/TextbookStatePreparation.lean

complete

theorem QuantumBlockEncoding.TextbookStatePreparation.plusTarget_normalized :
  QuantumBlockEncoding.TextbookStatePreparation.plusTarget.normalization

theorem QuantumBlockEncoding.TextbookStatePreparation.plusTarget_normalized :
  QuantumBlockEncoding.TextbookStatePreparation.plusTarget.normalization

Theorem6.12.22

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “hadamard prepares plus”; 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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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/TextbookStatePreparation.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.12.22●1 theorem

theoremdefined in QuantumBlockEncoding/TextbookStatePreparation.lean

complete

theorem QuantumBlockEncoding.TextbookStatePreparation.hadamard_prepares_plus :
  QuantumBlockEncoding.ConcreteSemantics.applyVec
      QuantumBlockEncoding.TextbookStatePreparation.hadamard
      (QuantumBlockEncoding.ConcreteSemantics.zeroKet 1) =
    QuantumBlockEncoding.TextbookStatePreparation.plusTarget.amplitudes

theorem QuantumBlockEncoding.TextbookStatePreparation.hadamard_prepares_plus :
  QuantumBlockEncoding.ConcreteSemantics.applyVec
      QuantumBlockEncoding.TextbookStatePreparation.hadamard
      (QuantumBlockEncoding.ConcreteSemantics.zeroKet
        1) =
    QuantumBlockEncoding.TextbookStatePreparation.plusTarget.amplitudes

Definition6.12.23

uses 0used by 0✓L∃∀N

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

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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Definition6.12.23●1 definition

defdefined in QuantumBlockEncoding/TextbookStatePreparation.lean

complete

def QuantumBlockEncoding.TextbookStatePreparation.hadamardGate :
  QuantumBlockEncoding.ConcreteSemantics.ComplexUnitaryGate 1

def QuantumBlockEncoding.TextbookStatePreparation.hadamardGate :
  QuantumBlockEncoding.ConcreteSemantics.ComplexUnitaryGate
    1

Definition6.12.24

uses 0used by 0✓L∃∀N

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

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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Definition6.12.24●1 definition

defdefined in QuantumBlockEncoding/TextbookStatePreparation.lean

complete

def QuantumBlockEncoding.TextbookStatePreparation.hadamardCertificate :
  QuantumBlockEncoding.ConcreteSemantics.ComplexStatePreparationCertificate
    1

def QuantumBlockEncoding.TextbookStatePreparation.hadamardCertificate :
  QuantumBlockEncoding.ConcreteSemantics.ComplexStatePreparationCertificate
    1

Definition6.12.25

uses 0used by 0✓L∃∀N

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

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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Definition6.12.25●1 definition

defdefined in QuantumBlockEncoding/TextbookStatePreparation.lean

complete

def QuantumBlockEncoding.TextbookStatePreparation.hadamardCircuit :
  QuantumBlockEncoding.Circuit

def QuantumBlockEncoding.TextbookStatePreparation.hadamardCircuit :
  QuantumBlockEncoding.Circuit

Definition6.12.26

uses 0used by 0✓L∃∀N

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

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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Definition6.12.26●1 definition

defdefined in QuantumBlockEncoding/TextbookStatePreparation.lean

complete

def QuantumBlockEncoding.TextbookStatePreparation.hadamardVerified :
  QuantumBlockEncoding.VerifiedStatePreparation ℂ 1

def QuantumBlockEncoding.TextbookStatePreparation.hadamardVerified :
  QuantumBlockEncoding.VerifiedStatePreparation
    ℂ 1

Theorem6.12.27

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “hadamard verified 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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Theorem6.12.27●1 theorem

theoremdefined in QuantumBlockEncoding/TextbookStatePreparation.lean

complete

theorem QuantumBlockEncoding.TextbookStatePreparation.hadamardVerified_cost :
  QuantumBlockEncoding.TextbookStatePreparation.hadamardVerified.candidate.cost =
    { auxiliaryQubits := 0, gateCount := 1, depth := 1,
      oracleCalls := 0 }

theorem QuantumBlockEncoding.TextbookStatePreparation.hadamardVerified_cost :
  QuantumBlockEncoding.TextbookStatePreparation.hadamardVerified.candidate.cost =
    { auxiliaryQubits := 0,
      gateCount := 1, depth := 1,
      oracleCalls := 0 }

Theorem6.12.28

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “pauli x certificate prepares one”; the hypotheses and conclusion in the code panel fix its exact scope. The certified Pauli X example states the familiar textbook equation.

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

Why it is in this chapter. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

Technical source note. The certified Pauli X example states the familiar textbook equation.

Declaration kind. theorem.

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

Lean code for Theorem6.12.28●1 theorem

theoremdefined in QuantumBlockEncoding/TextbookStatePreparation.lean

complete

theorem QuantumBlockEncoding.TextbookStatePreparation.pauliXCertificate_prepares_one :
  QuantumBlockEncoding.ConcreteSemantics.applyVec
      QuantumBlockEncoding.TextbookStatePreparation.pauliXCertificate.gate.matrix
      (QuantumBlockEncoding.ConcreteSemantics.zeroKet 1) =
    QuantumBlockEncoding.TextbookStatePreparation.pauliXCertificate.target.amplitudes

theorem QuantumBlockEncoding.TextbookStatePreparation.pauliXCertificate_prepares_one :
  QuantumBlockEncoding.ConcreteSemantics.applyVec
      QuantumBlockEncoding.TextbookStatePreparation.pauliXCertificate.gate.matrix
      (QuantumBlockEncoding.ConcreteSemantics.zeroKet
        1) =
    QuantumBlockEncoding.TextbookStatePreparation.pauliXCertificate.target.amplitudes

The certified Pauli X example states the familiar textbook equation.

Theorem6.12.29

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “hadamard certificate prepares plus”; the hypotheses and conclusion in the code panel fix its exact scope. The certified Hadamard example prepares the equal superposition.

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

Why it is in this chapter. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

Technical source note. The certified Hadamard example prepares the equal superposition.

Declaration kind. theorem.

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

Lean code for Theorem6.12.29●1 theorem

theoremdefined in QuantumBlockEncoding/TextbookStatePreparation.lean

complete

theorem QuantumBlockEncoding.TextbookStatePreparation.hadamardCertificate_prepares_plus :
  QuantumBlockEncoding.ConcreteSemantics.applyVec
      QuantumBlockEncoding.TextbookStatePreparation.hadamardCertificate.gate.matrix
      (QuantumBlockEncoding.ConcreteSemantics.zeroKet 1) =
    QuantumBlockEncoding.TextbookStatePreparation.hadamardCertificate.target.amplitudes

theorem QuantumBlockEncoding.TextbookStatePreparation.hadamardCertificate_prepares_plus :
  QuantumBlockEncoding.ConcreteSemantics.applyVec
      QuantumBlockEncoding.TextbookStatePreparation.hadamardCertificate.gate.matrix
      (QuantumBlockEncoding.ConcreteSemantics.zeroKet
        1) =
    QuantumBlockEncoding.TextbookStatePreparation.hadamardCertificate.target.amplitudes

The certified Hadamard example prepares the equal superposition.