6.10. QuantumBlockEncoding/ReversibleClassical.lean🔗

7 explicit public declarations, in source order.

Definition6.10.1

uses 0used by 0✓L∃∀N

Plain-English reading. This type lists the allowed alternatives for “reversible gate”; its constructors are the cases that downstream code must handle.

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

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

Lean code for Definition6.10.1●1 definition

inductive(3 constructors, 1 parameter)defined in QuantumBlockEncoding/ReversibleClassical.lean

complete

inductive QuantumBlockEncoding.ReversibleGate (qubits : ℕ) : Type

inductive QuantumBlockEncoding.ReversibleGate
  (qubits : ℕ) : Type

Constructors

x {qubits : ℕ} (target : Fin qubits) :
  QuantumBlockEncoding.ReversibleGate qubits

cx {qubits : ℕ} (control target : Fin qubits)
  (distinct : control ≠ target) :
  QuantumBlockEncoding.ReversibleGate qubits

ccx {qubits : ℕ} (control0 control1 target : Fin qubits)
  (c0_ne_c1 : control0 ≠ control1)
  (c0_ne_target : control0 ≠ target)
  (c1_ne_target : control1 ≠ target) :
  QuantumBlockEncoding.ReversibleGate qubits

Definition6.10.2

uses 0used by 0✓L∃∀N

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

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

Source: QuantumBlockEncoding/ReversibleClassical.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.10.2●1 definition

abbrevdefined in QuantumBlockEncoding/ReversibleClassical.lean

complete

abbrev QuantumBlockEncoding.ReversibleProgram (qubits : ℕ) : Type

abbrev QuantumBlockEncoding.ReversibleProgram
  (qubits : ℕ) : Type

Definition6.10.3

uses 0used by 0✓L∃∀N

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

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/ReversibleClassical.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.10.3●1 definition

defdefined in QuantumBlockEncoding/ReversibleClassical.lean

complete

def QuantumBlockEncoding.ccxBasisAction {qubits : ℕ}
  (control0 control1 target : Fin qubits)
  (state : QuantumBlockEncoding.PrimitiveBasis qubits) :
  QuantumBlockEncoding.PrimitiveBasis qubits

def QuantumBlockEncoding.ccxBasisAction
  {qubits : ℕ}
  (control0 control1 target : Fin qubits)
  (state :
    QuantumBlockEncoding.PrimitiveBasis
      qubits) :
  QuantumBlockEncoding.PrimitiveBasis
    qubits

Theorem6.10.4

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “ccx basis action involutive”; 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/ReversibleClassical.lean:30. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.10.4●1 theorem

theoremdefined in QuantumBlockEncoding/ReversibleClassical.lean

complete

theorem QuantumBlockEncoding.ccxBasisAction_involutive {qubits : ℕ}
  (control0 control1 target : Fin qubits)
  (c0_ne_target : control0 ≠ target)
  (c1_ne_target : control1 ≠ target) :
  Function.Involutive
    (QuantumBlockEncoding.ccxBasisAction control0 control1 target)

theorem QuantumBlockEncoding.ccxBasisAction_involutive
  {qubits : ℕ}
  (control0 control1 target : Fin qubits)
  (c0_ne_target : control0 ≠ target)
  (c1_ne_target : control1 ≠ target) :
  Function.Involutive
    (QuantumBlockEncoding.ccxBasisAction
      control0 control1 target)

Definition6.10.5

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition6.10.5●1 definition

defdefined in QuantumBlockEncoding/ReversibleClassical.lean

complete

def QuantumBlockEncoding.ccxBasisEquiv {qubits : ℕ}
  (control0 control1 target : Fin qubits)
  (c0_ne_target : control0 ≠ target)
  (c1_ne_target : control1 ≠ target) :
  QuantumBlockEncoding.PrimitiveBasis qubits ≃
    QuantumBlockEncoding.PrimitiveBasis qubits

def QuantumBlockEncoding.ccxBasisEquiv
  {qubits : ℕ}
  (control0 control1 target : Fin qubits)
  (c0_ne_target : control0 ≠ target)
  (c1_ne_target : control1 ≠ target) :
  QuantumBlockEncoding.PrimitiveBasis
      qubits ≃
    QuantumBlockEncoding.PrimitiveBasis
      qubits

Definition6.10.6

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “eval reversible 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/ReversibleClassical.lean:63. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition6.10.6●1 definition

defdefined in QuantumBlockEncoding/ReversibleClassical.lean

complete

def QuantumBlockEncoding.evalReversibleGate {qubits : ℕ} :
  QuantumBlockEncoding.ReversibleGate qubits →
    QuantumBlockEncoding.PrimitiveBasis qubits ≃
      QuantumBlockEncoding.PrimitiveBasis qubits

def QuantumBlockEncoding.evalReversibleGate
  {qubits : ℕ} :
  QuantumBlockEncoding.ReversibleGate
      qubits →
    QuantumBlockEncoding.PrimitiveBasis
        qubits ≃
      QuantumBlockEncoding.PrimitiveBasis
        qubits

Definition6.10.7

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition6.10.7●1 definition

defdefined in QuantumBlockEncoding/ReversibleClassical.lean

complete

def QuantumBlockEncoding.evalReversibleProgram {qubits : ℕ} :
  QuantumBlockEncoding.ReversibleProgram qubits →
    QuantumBlockEncoding.PrimitiveBasis qubits ≃
      QuantumBlockEncoding.PrimitiveBasis qubits

def QuantumBlockEncoding.evalReversibleProgram
  {qubits : ℕ} :
  QuantumBlockEncoding.ReversibleProgram
      qubits →
    QuantumBlockEncoding.PrimitiveBasis
        qubits ≃
      QuantumBlockEncoding.PrimitiveBasis
        qubits