8.3. QuantumBlockEncoding/OptimalControl.lean🔗

133 explicit public declarations, in source order.

Definition8.3.1

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “is permutation”. Local finite-permutation certificate used as a lightweight unitarity proxy.

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Local finite-permutation certificate used as a lightweight unitarity proxy.

Declaration kind. def.

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

Lean code for Definition8.3.1●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.IsPermutation {n : ℕ}
  (f : Fin n → Fin n) : Prop

def QuantumBlockEncoding.OptimalControl.IsPermutation
  {n : ℕ} (f : Fin n → Fin n) : Prop

Local finite-permutation certificate used as a lightweight unitarity proxy.

Definition8.3.2

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “target state 0”. System index for 'time=0', 'type=0', 'state=0'.

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. System index for 'time=0', 'type=0', 'state=0'.

Declaration kind. def.

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

Lean code for Definition8.3.2●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.targetState0 : Fin 8

def QuantumBlockEncoding.OptimalControl.targetState0 :
  Fin 8

System index for `time=0`, `type=0`, `state=0`.

Definition8.3.3

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “target state 1”. System index for 'time=0', 'type=0', 'state=1'.

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. System index for 'time=0', 'type=0', 'state=1'.

Declaration kind. def.

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

Lean code for Definition8.3.3●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.targetState1 : Fin 8

def QuantumBlockEncoding.OptimalControl.targetState1 :
  Fin 8

System index for `time=0`, `type=0`, `state=1`.

Definition8.3.4

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “source state 0”. System index for 'time=1', 'type=1', 'state=0'.

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. System index for 'time=1', 'type=1', 'state=0'.

Declaration kind. def.

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

Lean code for Definition8.3.4●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.sourceState0 : Fin 8

def QuantumBlockEncoding.OptimalControl.sourceState0 :
  Fin 8

System index for `time=1`, `type=1`, `state=0`.

Definition8.3.5

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “source state 1”. System index for 'time=1', 'type=1', 'state=1'.

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. System index for 'time=1', 'type=1', 'state=1'.

Declaration kind. def.

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

Lean code for Definition8.3.5●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.sourceState1 : Fin 8

def QuantumBlockEncoding.OptimalControl.sourceState1 :
  Fin 8

System index for `time=1`, `type=1`, `state=1`.

Definition8.3.6

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “example operator”. The concrete 'E_1' operator for one time qubit, one type qubit, and one state qubit.

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Declaration kind. def.

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

Lean code for Definition8.3.6●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.exampleOperator :
  QuantumBlockEncoding.Matrix 8 8 ℚ

def QuantumBlockEncoding.OptimalControl.exampleOperator :
  QuantumBlockEncoding.Matrix 8 8 ℚ

The concrete `E_1` operator for one time qubit, one type qubit, and one state
qubit.  It maps `|1>_time |1>_type |s>` to
`|0>_time |0>_type |s>` and annihilates every other basis state.

Definition8.3.7

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “clean index”. Clean-ancilla embedding into the first half of the one-ancilla space.

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Clean-ancilla embedding into the first half of the one-ancilla space.

Declaration kind. def.

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

Lean code for Definition8.3.7●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.cleanIndex (i : Fin 8) : Fin 16

def QuantumBlockEncoding.OptimalControl.cleanIndex
  (i : Fin 8) : Fin 16

Clean-ancilla embedding into the first half of the one-ancilla space.

Definition8.3.8

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “example 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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

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

Lean code for Definition8.3.8●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.exampleTarget :
  QuantumBlockEncoding.QueryOperatorTarget ℚ 8 8

def QuantumBlockEncoding.OptimalControl.exampleTarget :
  QuantumBlockEncoding.QueryOperatorTarget
    ℚ 8 8

Definition8.3.9

uses 0used by 0✓L∃∀N

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

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

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

Lean code for Definition8.3.9●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.exampleLayout :
  QuantumBlockEncoding.RegisterLayout

def QuantumBlockEncoding.OptimalControl.exampleLayout :
  QuantumBlockEncoding.RegisterLayout

Definition8.3.10

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “example image”. Permutation image for the one-ancilla unitary completion.

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Permutation image for the one-ancilla unitary completion. For each state bit 's', the four-cycle is '(0, source_s) -> (0, target_s) -> (1, source_s) -> (1, target_s) -> (0, source_s)'. Every other system basis state just swaps the auxiliary qubit.

Declaration kind. def.

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

Lean code for Definition8.3.10●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.exampleImage (x : Fin 16) : Fin 16

def QuantumBlockEncoding.OptimalControl.exampleImage
  (x : Fin 16) : Fin 16

Permutation image for the one-ancilla unitary completion.

For each state bit `s`, the four-cycle is

`(0, source_s) -> (0, target_s) -> (1, source_s)
-> (1, target_s) -> (0, source_s)`.

Every other system basis state just swaps the auxiliary qubit.

Definition8.3.11

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “example image inv”. Inverse permutation for 'exampleImage'.

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Inverse permutation for 'exampleImage'.

Declaration kind. def.

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

Lean code for Definition8.3.11●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.exampleImageInv (x : Fin 16) :
  Fin 16

def QuantumBlockEncoding.OptimalControl.exampleImageInv
  (x : Fin 16) : Fin 16

Inverse permutation for `exampleImage`.

Theorem8.3.12

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “example image left inverse”; 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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

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

Lean code for Theorem8.3.12●1 theorem

theoremdefined in QuantumBlockEncoding/OptimalControl.lean

complete

theorem QuantumBlockEncoding.OptimalControl.exampleImage_leftInverse
  (x : Fin 16) :
  QuantumBlockEncoding.OptimalControl.exampleImageInv
      (QuantumBlockEncoding.OptimalControl.exampleImage x) =
    x

theorem QuantumBlockEncoding.OptimalControl.exampleImage_leftInverse
  (x : Fin 16) :
  QuantumBlockEncoding.OptimalControl.exampleImageInv
      (QuantumBlockEncoding.OptimalControl.exampleImage
        x) =
    x

Theorem8.3.13

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “example image right inverse”; 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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

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

Lean code for Theorem8.3.13●1 theorem

theoremdefined in QuantumBlockEncoding/OptimalControl.lean

complete

theorem QuantumBlockEncoding.OptimalControl.exampleImage_rightInverse
  (x : Fin 16) :
  QuantumBlockEncoding.OptimalControl.exampleImage
      (QuantumBlockEncoding.OptimalControl.exampleImageInv x) =
    x

theorem QuantumBlockEncoding.OptimalControl.exampleImage_rightInverse
  (x : Fin 16) :
  QuantumBlockEncoding.OptimalControl.exampleImage
      (QuantumBlockEncoding.OptimalControl.exampleImageInv
        x) =
    x

Theorem8.3.14

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “example image is permutation”; the hypotheses and conclusion in the code panel fix its exact scope. The image function is a finite permutation, hence a permutation unitary.

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

Why it is in this chapter. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. The image function is a finite permutation, hence a permutation unitary.

Declaration kind. theorem.

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

Lean code for Theorem8.3.14●1 theorem

theoremdefined in QuantumBlockEncoding/OptimalControl.lean

complete

theorem QuantumBlockEncoding.OptimalControl.exampleImage_isPermutation :
  QuantumBlockEncoding.OptimalControl.IsPermutation
    QuantumBlockEncoding.OptimalControl.exampleImage

theorem QuantumBlockEncoding.OptimalControl.exampleImage_isPermutation :
  QuantumBlockEncoding.OptimalControl.IsPermutation
    QuantumBlockEncoding.OptimalControl.exampleImage

The image function is a finite permutation, hence a permutation unitary.

Definition8.3.15

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “reduced target image”. The reduced three-bit permutation induced by 'exampleImage' on '(type,time,aux)'.

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. The reduced three-bit permutation induced by 'exampleImage' on '(type,time,aux)'.

Declaration kind. def.

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

Lean code for Definition8.3.15●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.reducedTargetImage (x : Fin 8) :
  Fin 8

def QuantumBlockEncoding.OptimalControl.reducedTargetImage
  (x : Fin 8) : Fin 8

The reduced three-bit permutation induced by `exampleImage` on `(type,time,aux)`.

Definition8.3.16

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “red x 0”. Logical 'X' on reduced bit 0.

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Logical 'X' on reduced bit 0.

Declaration kind. def.

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

Lean code for Definition8.3.16●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.redX0 (x : Fin 8) : Fin 8

def QuantumBlockEncoding.OptimalControl.redX0
  (x : Fin 8) : Fin 8

Logical `X` on reduced bit 0.

Definition8.3.17

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “red x 2”. Logical 'X' on reduced bit 2.

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Logical 'X' on reduced bit 2.

Declaration kind. def.

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

Lean code for Definition8.3.17●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.redX2 (x : Fin 8) : Fin 8

def QuantumBlockEncoding.OptimalControl.redX2
  (x : Fin 8) : Fin 8

Logical `X` on reduced bit 2.

Definition8.3.18

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “red x 1”. Logical 'X' on reduced bit 1.

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Logical 'X' on reduced bit 1.

Declaration kind. def.

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

Lean code for Definition8.3.18●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.redX1 (x : Fin 8) : Fin 8

def QuantumBlockEncoding.OptimalControl.redX1
  (x : Fin 8) : Fin 8

Logical `X` on reduced bit 1.

Definition8.3.19

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “red cx 01”. Logical CNOT with control reduced bit 0 and target reduced bit 1.

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Logical CNOT with control reduced bit 0 and target reduced bit 1.

Declaration kind. def.

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

Lean code for Definition8.3.19●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.redCX01 (x : Fin 8) : Fin 8

def QuantumBlockEncoding.OptimalControl.redCX01
  (x : Fin 8) : Fin 8

Logical CNOT with control reduced bit 0 and target reduced bit 1.

Definition8.3.20

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “red cx 10”. Logical CNOT with control reduced bit 1 and target reduced bit 0.

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Logical CNOT with control reduced bit 1 and target reduced bit 0.

Declaration kind. def.

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

Lean code for Definition8.3.20●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.redCX10 (x : Fin 8) : Fin 8

def QuantumBlockEncoding.OptimalControl.redCX10
  (x : Fin 8) : Fin 8

Logical CNOT with control reduced bit 1 and target reduced bit 0.

Definition8.3.21

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “red cx 20”. Logical CNOT with control reduced bit 2 and target reduced bit 0.

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Logical CNOT with control reduced bit 2 and target reduced bit 0.

Declaration kind. def.

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

Lean code for Definition8.3.21●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.redCX20 (x : Fin 8) : Fin 8

def QuantumBlockEncoding.OptimalControl.redCX20
  (x : Fin 8) : Fin 8

Logical CNOT with control reduced bit 2 and target reduced bit 0.

Definition8.3.22

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “red cx 21”. Logical CNOT with control reduced bit 2 and target reduced bit 1.

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Logical CNOT with control reduced bit 2 and target reduced bit 1.

Declaration kind. def.

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

Lean code for Definition8.3.22●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.redCX21 (x : Fin 8) : Fin 8

def QuantumBlockEncoding.OptimalControl.redCX21
  (x : Fin 8) : Fin 8

Logical CNOT with control reduced bit 2 and target reduced bit 1.

Definition8.3.23

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “red ccx 012”. Logical Toffoli with controls reduced bits 0,1 and target reduced bit 2.

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Logical Toffoli with controls reduced bits 0,1 and target reduced bit 2.

Declaration kind. def.

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

Lean code for Definition8.3.23●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.redCCX012 (x : Fin 8) : Fin 8

def QuantumBlockEncoding.OptimalControl.redCCX012
  (x : Fin 8) : Fin 8

Logical Toffoli with controls reduced bits 0,1 and target reduced bit 2.

Definition8.3.24

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “reduced depth 5 image”. Depth-5 logical circuit found by the first EoH-style explore pass: 1.

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Depth-5 logical circuit found by the first EoH-style explore pass: 1. 'CCX(0,1;2)' 2. 'CX(0,1)' 3. 'CX(1,0)' 4. 'X(0)' 5. parallel layer '{X(2), CX(0,1)}'

Declaration kind. def.

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

Lean code for Definition8.3.24●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.reducedDepth5Image (x : Fin 8) :
  Fin 8

def QuantumBlockEncoding.OptimalControl.reducedDepth5Image
  (x : Fin 8) : Fin 8

Depth-5 logical circuit found by the first EoH-style explore pass:

1. `CCX(0,1;2)`
2. `CX(0,1)`
3. `CX(1,0)`
4. `X(0)`
5. parallel layer `{X(2), CX(0,1)}`

Theorem8.3.25

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “reduced depth 5 image eq target”; the hypotheses and conclusion in the code panel fix its exact scope. The expanded logical circuit realizes the same reduced permutation.

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

Why it is in this chapter. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. The expanded logical circuit realizes the same reduced permutation.

Declaration kind. theorem.

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

Lean code for Theorem8.3.25●1 theorem

theoremdefined in QuantumBlockEncoding/OptimalControl.lean

complete

theorem QuantumBlockEncoding.OptimalControl.reducedDepth5Image_eq_target
  (x : Fin 8) :
  QuantumBlockEncoding.OptimalControl.reducedDepth5Image x =
    QuantumBlockEncoding.OptimalControl.reducedTargetImage x

theorem QuantumBlockEncoding.OptimalControl.reducedDepth5Image_eq_target
  (x : Fin 8) :
  QuantumBlockEncoding.OptimalControl.reducedDepth5Image
      x =
    QuantumBlockEncoding.OptimalControl.reducedTargetImage
      x

The expanded logical circuit realizes the same reduced permutation.

Definition8.3.26

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “reduced of full”. Extract the active '(type,time,aux)' register from the full 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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Extract the active '(type,time,aux)' register from the full index.

Declaration kind. def.

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

Lean code for Definition8.3.26●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.reducedOfFull (x : Fin 16) : Fin 8

def QuantumBlockEncoding.OptimalControl.reducedOfFull
  (x : Fin 16) : Fin 8

Extract the active `(type,time,aux)` register from the full index.

Definition8.3.27

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “state of full”. Extract the passive state bit from the full 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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Extract the passive state bit from the full index.

Declaration kind. def.

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

Lean code for Definition8.3.27●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.stateOfFull (x : Fin 16) : Fin 2

def QuantumBlockEncoding.OptimalControl.stateOfFull
  (x : Fin 16) : Fin 2

Extract the passive state bit from the full index.

Definition8.3.28

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “lift reduced image”. Lift a reduced active-register permutation while leaving the state bit fixed.

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Lift a reduced active-register permutation while leaving the state bit fixed.

Declaration kind. def.

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

Lean code for Definition8.3.28●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.liftReducedImage (f : Fin 8 → Fin 8)
  (x : Fin 16) : Fin 16

def QuantumBlockEncoding.OptimalControl.liftReducedImage
  (f : Fin 8 → Fin 8) (x : Fin 16) :
  Fin 16

Lift a reduced active-register permutation while leaving the state bit fixed.

Theorem8.3.29

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “reduced depth 5 lifts example image”; the hypotheses and conclusion in the code panel fix its exact scope. The depth-5 reduced circuit lifts to the full one-ancilla permutation because the state bit is passive.

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

Why it is in this chapter. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. The depth-5 reduced circuit lifts to the full one-ancilla permutation because the state bit is passive.

Declaration kind. theorem.

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

Lean code for Theorem8.3.29●1 theorem

theoremdefined in QuantumBlockEncoding/OptimalControl.lean

complete

theorem QuantumBlockEncoding.OptimalControl.reducedDepth5_lifts_exampleImage
  (x : Fin 16) :
  QuantumBlockEncoding.OptimalControl.liftReducedImage
      QuantumBlockEncoding.OptimalControl.reducedDepth5Image x =
    QuantumBlockEncoding.OptimalControl.exampleImage x

theorem QuantumBlockEncoding.OptimalControl.reducedDepth5_lifts_exampleImage
  (x : Fin 16) :
  QuantumBlockEncoding.OptimalControl.liftReducedImage
      QuantumBlockEncoding.OptimalControl.reducedDepth5Image
      x =
    QuantumBlockEncoding.OptimalControl.exampleImage
      x

The depth-5 reduced circuit lifts to the full one-ancilla permutation because
the state bit is passive.

Theorem8.3.30

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “reduced depth 5 full is permutation”; the hypotheses and conclusion in the code panel fix its exact scope. The depth-5 full active-plus-state completion is a permutation.

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

Why it is in this chapter. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. The depth-5 full active-plus-state completion is a permutation.

Declaration kind. theorem.

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

Lean code for Theorem8.3.30●1 theorem

theoremdefined in QuantumBlockEncoding/OptimalControl.lean

complete

theorem QuantumBlockEncoding.OptimalControl.reducedDepth5Full_isPermutation :
  QuantumBlockEncoding.OptimalControl.IsPermutation
    (QuantumBlockEncoding.OptimalControl.liftReducedImage
      QuantumBlockEncoding.OptimalControl.reducedDepth5Image)

theorem QuantumBlockEncoding.OptimalControl.reducedDepth5Full_isPermutation :
  QuantumBlockEncoding.OptimalControl.IsPermutation
    (QuantumBlockEncoding.OptimalControl.liftReducedImage
      QuantumBlockEncoding.OptimalControl.reducedDepth5Image)

The depth-5 full active-plus-state completion is a permutation.

Definition8.3.31

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “unitary from reduced image”. Matrix induced by a reduced active-register permutation lifted over the passive state bit.

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Matrix induced by a reduced active-register permutation lifted over the passive state bit.

Declaration kind. def.

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

Lean code for Definition8.3.31●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.unitaryFromReducedImage
  (f : Fin 8 → Fin 8) : QuantumBlockEncoding.Matrix 16 16 ℚ

def QuantumBlockEncoding.OptimalControl.unitaryFromReducedImage
  (f : Fin 8 → Fin 8) :
  QuantumBlockEncoding.Matrix 16 16 ℚ

Matrix induced by a reduced active-register permutation lifted over the passive
state bit.

Definition8.3.32

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “clean block e 1”. The clean block condition for the concrete optimal-control 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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. The clean block condition for the concrete optimal-control target.

Declaration kind. def.

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

Lean code for Definition8.3.32●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.CleanBlockE1 (f : Fin 8 → Fin 8) :
  Prop

def QuantumBlockEncoding.OptimalControl.CleanBlockE1
  (f : Fin 8 → Fin 8) : Prop

The clean block condition for the concrete optimal-control target.

Definition8.3.33

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “column inner”. Column inner products for concrete rational matrix-level unitarity checks.

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Column inner products for concrete rational matrix-level unitarity checks.

Declaration kind. def.

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

Lean code for Definition8.3.33●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.columnInner {n : ℕ}
  (U : QuantumBlockEncoding.Matrix n n ℚ) (i j : Fin n) : ℚ

def QuantumBlockEncoding.OptimalControl.columnInner
  {n : ℕ}
  (U : QuantumBlockEncoding.Matrix n n ℚ)
  (i j : Fin n) : ℚ

Column inner products for concrete rational matrix-level unitarity checks.

Definition8.3.34

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “row inner”. Row inner products for concrete rational matrix-level unitarity checks.

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Row inner products for concrete rational matrix-level unitarity checks.

Declaration kind. def.

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

Lean code for Definition8.3.34●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.rowInner {n : ℕ}
  (U : QuantumBlockEncoding.Matrix n n ℚ) (i j : Fin n) : ℚ

def QuantumBlockEncoding.OptimalControl.rowInner
  {n : ℕ}
  (U : QuantumBlockEncoding.Matrix n n ℚ)
  (i j : Fin n) : ℚ

Row inner products for concrete rational matrix-level unitarity checks.

Definition8.3.35

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “is rational orthogonal”. Concrete real/rational unitary proxy for this finite permutation-matrix sandbox.

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Concrete real/rational unitary proxy for this finite permutation-matrix sandbox. Since all entries are rational and all current exact circuits are real, this is the finite 'UᵀU = I' and 'UUᵀ = I' condition.

Declaration kind. def.

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

Lean code for Definition8.3.35●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.IsRationalOrthogonal {n : ℕ}
  (U : QuantumBlockEncoding.Matrix n n ℚ) : Prop

def QuantumBlockEncoding.OptimalControl.IsRationalOrthogonal
  {n : ℕ}
  (U :
    QuantumBlockEncoding.Matrix n n ℚ) :
  Prop

Concrete real/rational unitary proxy for this finite permutation-matrix
sandbox.  Since all entries are rational and all current exact circuits are
real, this is the finite `UᵀU = I` and `UUᵀ = I` condition.

Theorem8.3.36

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “example operator not rational orthogonal”; the hypotheses and conclusion in the code panel fix its exact scope. The target operator itself is not unitary.

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

Why it is in this chapter. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. The target operator itself is not unitary. Therefore an exact unscaled zero-auxiliary block encoding cannot use 'E_1' as the whole unitary matrix. One auxiliary qubit is locally necessary for this concrete exact construction model.

Declaration kind. theorem.

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

Lean code for Theorem8.3.36●1 theorem

theoremdefined in QuantumBlockEncoding/OptimalControl.lean

complete

theorem QuantumBlockEncoding.OptimalControl.exampleOperator_not_rationalOrthogonal :
  ¬QuantumBlockEncoding.OptimalControl.IsRationalOrthogonal
      QuantumBlockEncoding.OptimalControl.exampleOperator

theorem QuantumBlockEncoding.OptimalControl.exampleOperator_not_rationalOrthogonal :
  ¬QuantumBlockEncoding.OptimalControl.IsRationalOrthogonal
      QuantumBlockEncoding.OptimalControl.exampleOperator

The target operator itself is not unitary.  Therefore an exact unscaled
zero-auxiliary block encoding cannot use `E_1` as the whole unitary matrix.
One auxiliary qubit is locally necessary for this concrete exact construction
model.

Theorem8.3.37

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “reduced depth 5 clean block”; the hypotheses and conclusion in the code panel fix its exact scope. The depth-5 fixed-completion candidate has the required clean block.

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

Why it is in this chapter. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. The depth-5 fixed-completion candidate has the required clean block.

Declaration kind. theorem.

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

Lean code for Theorem8.3.37●1 theorem

theoremdefined in QuantumBlockEncoding/OptimalControl.lean

complete

theorem QuantumBlockEncoding.OptimalControl.reducedDepth5_cleanBlock :
  QuantumBlockEncoding.OptimalControl.CleanBlockE1
    QuantumBlockEncoding.OptimalControl.reducedDepth5Image

theorem QuantumBlockEncoding.OptimalControl.reducedDepth5_cleanBlock :
  QuantumBlockEncoding.OptimalControl.CleanBlockE1
    QuantumBlockEncoding.OptimalControl.reducedDepth5Image

The depth-5 fixed-completion candidate has the required clean block.

Definition8.3.38

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “reduced depth 5 unitary”. Matrix of the depth-5 fixed-completion logical 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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Matrix of the depth-5 fixed-completion logical circuit.

Declaration kind. def.

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

Lean code for Definition8.3.38●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.reducedDepth5Unitary :
  QuantumBlockEncoding.Matrix 16 16 ℚ

def QuantumBlockEncoding.OptimalControl.reducedDepth5Unitary :
  QuantumBlockEncoding.Matrix 16 16 ℚ

Matrix of the depth-5 fixed-completion logical circuit.

Theorem8.3.39

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “reduced depth 5 unitary is rational orthogonal”; the hypotheses and conclusion in the code panel fix its exact scope. The depth-5 fixed-completion matrix is rational orthogonal/unitary.

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

Why it is in this chapter. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. The depth-5 fixed-completion matrix is rational orthogonal/unitary.

Declaration kind. theorem.

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

Lean code for Theorem8.3.39●1 theorem

theoremdefined in QuantumBlockEncoding/OptimalControl.lean

complete

theorem QuantumBlockEncoding.OptimalControl.reducedDepth5Unitary_isRationalOrthogonal :
  QuantumBlockEncoding.OptimalControl.IsRationalOrthogonal
    QuantumBlockEncoding.OptimalControl.reducedDepth5Unitary

theorem QuantumBlockEncoding.OptimalControl.reducedDepth5Unitary_isRationalOrthogonal :
  QuantumBlockEncoding.OptimalControl.IsRationalOrthogonal
    QuantumBlockEncoding.OptimalControl.reducedDepth5Unitary

The depth-5 fixed-completion matrix is rational orthogonal/unitary.

Theorem8.3.40

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “reduced depth 5 unitary clean block”; the hypotheses and conclusion in the code panel fix its exact scope. The depth-5 fixed-completion matrix has the required clean block.

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

Why it is in this chapter. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. The depth-5 fixed-completion matrix has the required clean block.

Declaration kind. theorem.

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

Lean code for Theorem8.3.40●1 theorem

theoremdefined in QuantumBlockEncoding/OptimalControl.lean

complete

theorem QuantumBlockEncoding.OptimalControl.reducedDepth5Unitary_cleanBlock
  (row col : Fin 8) :
  QuantumBlockEncoding.OptimalControl.reducedDepth5Unitary
      (QuantumBlockEncoding.OptimalControl.cleanIndex row)
      (QuantumBlockEncoding.OptimalControl.cleanIndex col) =
    QuantumBlockEncoding.OptimalControl.exampleOperator row col

theorem QuantumBlockEncoding.OptimalControl.reducedDepth5Unitary_cleanBlock
  (row col : Fin 8) :
  QuantumBlockEncoding.OptimalControl.reducedDepth5Unitary
      (QuantumBlockEncoding.OptimalControl.cleanIndex
        row)
      (QuantumBlockEncoding.OptimalControl.cleanIndex
        col) =
    QuantumBlockEncoding.OptimalControl.exampleOperator
      row col

The depth-5 fixed-completion matrix has the required clean block.

Definition8.3.41

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “pro eq transfer image”. ChatGPT Pro's structured equality-flag/transfer construction specialized to the concrete 'r = 1, k = 1' instance: 1.

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. ChatGPT Pro's structured equality-flag/transfer construction specialized to the concrete 'r = 1, k = 1' instance: 1. 'CCX(type,time;aux)' flags 'time=1,type=1'. 2. 'CX(aux,time)' transfers flagged 'time' to '0'. 3. 'CX(aux,type)' transfers flagged 'type' to '0'. 4. 'X(aux)' moves the selected branch back into the clean block.

Declaration kind. def.

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

Lean code for Definition8.3.41●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.proEqTransferImage (x : Fin 8) :
  Fin 8

def QuantumBlockEncoding.OptimalControl.proEqTransferImage
  (x : Fin 8) : Fin 8

ChatGPT Pro's structured equality-flag/transfer construction specialized to
the concrete `r = 1, k = 1` instance:

1. `CCX(type,time;aux)` flags `time=1,type=1`.
2. `CX(aux,time)` transfers flagged `time` to `0`.
3. `CX(aux,type)` transfers flagged `type` to `0`.
4. `X(aux)` moves the selected branch back into the clean block.

Theorem8.3.42

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “pro eq transfer image is permutation”; the hypotheses and conclusion in the code panel fix its exact scope. Pro's reduced active-register map is a permutation.

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

Why it is in this chapter. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Pro's reduced active-register map is a permutation.

Declaration kind. theorem.

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

Lean code for Theorem8.3.42●1 theorem

theoremdefined in QuantumBlockEncoding/OptimalControl.lean

complete

theorem QuantumBlockEncoding.OptimalControl.proEqTransferImage_isPermutation :
  QuantumBlockEncoding.OptimalControl.IsPermutation
    QuantumBlockEncoding.OptimalControl.proEqTransferImage

theorem QuantumBlockEncoding.OptimalControl.proEqTransferImage_isPermutation :
  QuantumBlockEncoding.OptimalControl.IsPermutation
    QuantumBlockEncoding.OptimalControl.proEqTransferImage

Pro's reduced active-register map is a permutation.

Theorem8.3.43

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “pro eq transfer full is permutation”; the hypotheses and conclusion in the code panel fix its exact scope. Pro's full active-plus-state completion is a permutation.

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

Why it is in this chapter. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Pro's full active-plus-state completion is a permutation.

Declaration kind. theorem.

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

Lean code for Theorem8.3.43●1 theorem

theoremdefined in QuantumBlockEncoding/OptimalControl.lean

complete

theorem QuantumBlockEncoding.OptimalControl.proEqTransferFull_isPermutation :
  QuantumBlockEncoding.OptimalControl.IsPermutation
    (QuantumBlockEncoding.OptimalControl.liftReducedImage
      QuantumBlockEncoding.OptimalControl.proEqTransferImage)

theorem QuantumBlockEncoding.OptimalControl.proEqTransferFull_isPermutation :
  QuantumBlockEncoding.OptimalControl.IsPermutation
    (QuantumBlockEncoding.OptimalControl.liftReducedImage
      QuantumBlockEncoding.OptimalControl.proEqTransferImage)

Pro's full active-plus-state completion is a permutation.

Theorem8.3.44

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “pro eq transfer clean block”; the hypotheses and conclusion in the code panel fix its exact scope. Pro's construction has the required clean block for the concrete target.

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

Why it is in this chapter. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Pro's construction has the required clean block for the concrete target.

Declaration kind. theorem.

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

Lean code for Theorem8.3.44●1 theorem

theoremdefined in QuantumBlockEncoding/OptimalControl.lean

complete

theorem QuantumBlockEncoding.OptimalControl.proEqTransfer_cleanBlock :
  QuantumBlockEncoding.OptimalControl.CleanBlockE1
    QuantumBlockEncoding.OptimalControl.proEqTransferImage

theorem QuantumBlockEncoding.OptimalControl.proEqTransfer_cleanBlock :
  QuantumBlockEncoding.OptimalControl.CleanBlockE1
    QuantumBlockEncoding.OptimalControl.proEqTransferImage

Pro's construction has the required clean block for the concrete target.

Definition8.3.45

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “pro eq transfer unitary”. Matrix of Pro's equality-flag/transfer construction.

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Matrix of Pro's equality-flag/transfer construction.

Declaration kind. def.

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

Lean code for Definition8.3.45●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.proEqTransferUnitary :
  QuantumBlockEncoding.Matrix 16 16 ℚ

def QuantumBlockEncoding.OptimalControl.proEqTransferUnitary :
  QuantumBlockEncoding.Matrix 16 16 ℚ

Matrix of Pro's equality-flag/transfer construction.

Theorem8.3.46

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “pro eq transfer unitary is rational orthogonal”; the hypotheses and conclusion in the code panel fix its exact scope. Pro's equality-flag/transfer matrix is rational orthogonal/unitary.

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

Why it is in this chapter. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Pro's equality-flag/transfer matrix is rational orthogonal/unitary.

Declaration kind. theorem.

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

Lean code for Theorem8.3.46●1 theorem

theoremdefined in QuantumBlockEncoding/OptimalControl.lean

complete

theorem QuantumBlockEncoding.OptimalControl.proEqTransferUnitary_isRationalOrthogonal :
  QuantumBlockEncoding.OptimalControl.IsRationalOrthogonal
    QuantumBlockEncoding.OptimalControl.proEqTransferUnitary

theorem QuantumBlockEncoding.OptimalControl.proEqTransferUnitary_isRationalOrthogonal :
  QuantumBlockEncoding.OptimalControl.IsRationalOrthogonal
    QuantumBlockEncoding.OptimalControl.proEqTransferUnitary

Pro's equality-flag/transfer matrix is rational orthogonal/unitary.

Theorem8.3.47

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “pro eq transfer unitary clean block”; the hypotheses and conclusion in the code panel fix its exact scope. Pro's equality-flag/transfer matrix has the required clean block.

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

Why it is in this chapter. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Pro's equality-flag/transfer matrix has the required clean block.

Declaration kind. theorem.

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

Lean code for Theorem8.3.47●1 theorem

theoremdefined in QuantumBlockEncoding/OptimalControl.lean

complete

theorem QuantumBlockEncoding.OptimalControl.proEqTransferUnitary_cleanBlock
  (row col : Fin 8) :
  QuantumBlockEncoding.OptimalControl.proEqTransferUnitary
      (QuantumBlockEncoding.OptimalControl.cleanIndex row)
      (QuantumBlockEncoding.OptimalControl.cleanIndex col) =
    QuantumBlockEncoding.OptimalControl.exampleOperator row col

theorem QuantumBlockEncoding.OptimalControl.proEqTransferUnitary_cleanBlock
  (row col : Fin 8) :
  QuantumBlockEncoding.OptimalControl.proEqTransferUnitary
      (QuantumBlockEncoding.OptimalControl.cleanIndex
        row)
      (QuantumBlockEncoding.OptimalControl.cleanIndex
        col) =
    QuantumBlockEncoding.OptimalControl.exampleOperator
      row col

Pro's equality-flag/transfer matrix has the required clean block.

Definition8.3.48

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “evolved eq flip image”. An evolved child of the Pro construction.

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. An evolved child of the Pro construction. The same equality flag is followed by a parallel layer of three 'X' gates on '(type,time,aux)'. This uses the freedom in the unitary completion: it does not reproduce 'exampleImage', but it does satisfy the same clean-block contract.

Declaration kind. def.

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

Lean code for Definition8.3.48●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.evolvedEqFlipImage (x : Fin 8) :
  Fin 8

def QuantumBlockEncoding.OptimalControl.evolvedEqFlipImage
  (x : Fin 8) : Fin 8

An evolved child of the Pro construction.  The same equality flag is followed
by a parallel layer of three `X` gates on `(type,time,aux)`.  This uses the
freedom in the unitary completion: it does not reproduce `exampleImage`, but it
does satisfy the same clean-block contract.

Theorem8.3.49

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “evolved eq flip image is permutation”; the hypotheses and conclusion in the code panel fix its exact scope. The evolved reduced active-register map is a permutation.

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

Why it is in this chapter. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. The evolved reduced active-register map is a permutation.

Declaration kind. theorem.

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

Lean code for Theorem8.3.49●1 theorem

theoremdefined in QuantumBlockEncoding/OptimalControl.lean

complete

theorem QuantumBlockEncoding.OptimalControl.evolvedEqFlipImage_isPermutation :
  QuantumBlockEncoding.OptimalControl.IsPermutation
    QuantumBlockEncoding.OptimalControl.evolvedEqFlipImage

theorem QuantumBlockEncoding.OptimalControl.evolvedEqFlipImage_isPermutation :
  QuantumBlockEncoding.OptimalControl.IsPermutation
    QuantumBlockEncoding.OptimalControl.evolvedEqFlipImage

The evolved reduced active-register map is a permutation.

Theorem8.3.50

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “evolved eq flip full is permutation”; the hypotheses and conclusion in the code panel fix its exact scope. The evolved full active-plus-state completion is a permutation.

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

Why it is in this chapter. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. The evolved full active-plus-state completion is a permutation.

Declaration kind. theorem.

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

Lean code for Theorem8.3.50●1 theorem

theoremdefined in QuantumBlockEncoding/OptimalControl.lean

complete

theorem QuantumBlockEncoding.OptimalControl.evolvedEqFlipFull_isPermutation :
  QuantumBlockEncoding.OptimalControl.IsPermutation
    (QuantumBlockEncoding.OptimalControl.liftReducedImage
      QuantumBlockEncoding.OptimalControl.evolvedEqFlipImage)

theorem QuantumBlockEncoding.OptimalControl.evolvedEqFlipFull_isPermutation :
  QuantumBlockEncoding.OptimalControl.IsPermutation
    (QuantumBlockEncoding.OptimalControl.liftReducedImage
      QuantumBlockEncoding.OptimalControl.evolvedEqFlipImage)

The evolved full active-plus-state completion is a permutation.

Theorem8.3.51

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “evolved eq flip clean block”; the hypotheses and conclusion in the code panel fix its exact scope. The evolved depth-2 construction has the required clean block.

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

Why it is in this chapter. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. The evolved depth-2 construction has the required clean block.

Declaration kind. theorem.

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

Lean code for Theorem8.3.51●1 theorem

theoremdefined in QuantumBlockEncoding/OptimalControl.lean

complete

theorem QuantumBlockEncoding.OptimalControl.evolvedEqFlip_cleanBlock :
  QuantumBlockEncoding.OptimalControl.CleanBlockE1
    QuantumBlockEncoding.OptimalControl.evolvedEqFlipImage

theorem QuantumBlockEncoding.OptimalControl.evolvedEqFlip_cleanBlock :
  QuantumBlockEncoding.OptimalControl.CleanBlockE1
    QuantumBlockEncoding.OptimalControl.evolvedEqFlipImage

The evolved depth-2 construction has the required clean block.

Definition8.3.52

uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “logical reversible cost”. A proposition-valued field is a requirement until a constructor supplies it. Lightweight score for the logical reversible gate library '{X,CNOT,Toffoli}'.

Formal status. Data contract in the default import surface; proposition-valued fields are obligations, not automatically established facts.

Why it is in this chapter. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Lightweight score for the logical reversible gate library '{X,CNOT,Toffoli}'.

Declaration kind. structure.

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

Lean code for Definition8.3.52●1 definition

structure(6 fields)defined in QuantumBlockEncoding/OptimalControl.lean

complete

structure QuantumBlockEncoding.OptimalControl.LogicalReversibleCost : Type

structure QuantumBlockEncoding.OptimalControl.LogicalReversibleCost :
  Type

Lightweight score for the logical reversible gate library `{X,CNOT,Toffoli}`.

Fields

auxiliaryQubits : ℕ

xGates : ℕ

cnotGates : ℕ

toffoliGates : ℕ

depth : ℕ

oracleCalls : ℕ

Definition8.3.53

uses 0used by 0✓L∃∀N

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

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

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

Lean code for Definition8.3.53●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.LogicalReversibleCost.gateCount
  (c : QuantumBlockEncoding.OptimalControl.LogicalReversibleCost) : ℕ

def QuantumBlockEncoding.OptimalControl.LogicalReversibleCost.gateCount
  (c :
    QuantumBlockEncoding.OptimalControl.LogicalReversibleCost) :
  ℕ

Definition8.3.54

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “better than”. Lexicographic order inside one fixed logical reversible gate library.

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Lexicographic order inside one fixed logical reversible gate library. ABEIS compares asymptotic scale first outside this concrete record. Once two candidates are in the same scale class for the chosen backend, the local priority is gate count, then parallel depth, then auxiliary qubits, then unexpanded oracle calls.

Declaration kind. def.

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

Lean code for Definition8.3.54●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.LogicalReversibleCost.betterThan
  (x y : QuantumBlockEncoding.OptimalControl.LogicalReversibleCost) :
  Prop

def QuantumBlockEncoding.OptimalControl.LogicalReversibleCost.betterThan
  (x y :
    QuantumBlockEncoding.OptimalControl.LogicalReversibleCost) :
  Prop

Lexicographic order inside one fixed logical reversible gate library.

ABEIS compares asymptotic scale first outside this concrete record.  Once two
candidates are in the same scale class for the chosen backend, the local
priority is gate count, then parallel depth, then auxiliary qubits, then
unexpanded oracle calls.

Definition8.3.55

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “reduced depth 5 cost”. Expanded score for 'reducedDepth5Image' before hardware decomposition.

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Expanded score for 'reducedDepth5Image' before hardware decomposition.

Declaration kind. def.

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

Lean code for Definition8.3.55●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.reducedDepth5Cost :
  QuantumBlockEncoding.OptimalControl.LogicalReversibleCost

def QuantumBlockEncoding.OptimalControl.reducedDepth5Cost :
  QuantumBlockEncoding.OptimalControl.LogicalReversibleCost

Expanded score for `reducedDepth5Image` before hardware decomposition.

Theorem8.3.56

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “reduced depth 5 cost gate count”; 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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

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

Lean code for Theorem8.3.56●1 theorem

theoremdefined in QuantumBlockEncoding/OptimalControl.lean

complete

theorem QuantumBlockEncoding.OptimalControl.reducedDepth5Cost_gateCount :
  QuantumBlockEncoding.OptimalControl.reducedDepth5Cost.gateCount = 6

theorem QuantumBlockEncoding.OptimalControl.reducedDepth5Cost_gateCount :
  QuantumBlockEncoding.OptimalControl.reducedDepth5Cost.gateCount =
    6

Theorem8.3.57

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “reduced depth 5 cost oracle free”; 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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

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

Lean code for Theorem8.3.57●1 theorem

theoremdefined in QuantumBlockEncoding/OptimalControl.lean

complete

theorem QuantumBlockEncoding.OptimalControl.reducedDepth5Cost_oracleFree :
  QuantumBlockEncoding.OptimalControl.reducedDepth5Cost.oracleCalls = 0

theorem QuantumBlockEncoding.OptimalControl.reducedDepth5Cost_oracleFree :
  QuantumBlockEncoding.OptimalControl.reducedDepth5Cost.oracleCalls =
    0

Definition8.3.58

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “pro eq transfer cost”. Expanded score for Pro's equality-flag/transfer construction.

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Expanded score for Pro's equality-flag/transfer construction.

Declaration kind. def.

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

Lean code for Definition8.3.58●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.proEqTransferCost :
  QuantumBlockEncoding.OptimalControl.LogicalReversibleCost

def QuantumBlockEncoding.OptimalControl.proEqTransferCost :
  QuantumBlockEncoding.OptimalControl.LogicalReversibleCost

Expanded score for Pro's equality-flag/transfer construction.

Theorem8.3.59

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “pro eq transfer cost gate count”; 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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

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

Lean code for Theorem8.3.59●1 theorem

theoremdefined in QuantumBlockEncoding/OptimalControl.lean

complete

theorem QuantumBlockEncoding.OptimalControl.proEqTransferCost_gateCount :
  QuantumBlockEncoding.OptimalControl.proEqTransferCost.gateCount = 4

theorem QuantumBlockEncoding.OptimalControl.proEqTransferCost_gateCount :
  QuantumBlockEncoding.OptimalControl.proEqTransferCost.gateCount =
    4

Theorem8.3.60

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “pro eq transfer cost better than depth 5”; 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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

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

Lean code for Theorem8.3.60●1 theorem

theoremdefined in QuantumBlockEncoding/OptimalControl.lean

complete

theorem QuantumBlockEncoding.OptimalControl.proEqTransferCost_betterThan_depth5 :
  QuantumBlockEncoding.OptimalControl.proEqTransferCost.betterThan
    QuantumBlockEncoding.OptimalControl.reducedDepth5Cost

theorem QuantumBlockEncoding.OptimalControl.proEqTransferCost_betterThan_depth5 :
  QuantumBlockEncoding.OptimalControl.proEqTransferCost.betterThan
    QuantumBlockEncoding.OptimalControl.reducedDepth5Cost

Definition8.3.61

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “evolved eq flip cost”. Expanded score for the evolved equality-flag/parallel-flip construction.

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Expanded score for the evolved equality-flag/parallel-flip construction.

Declaration kind. def.

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

Lean code for Definition8.3.61●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.evolvedEqFlipCost :
  QuantumBlockEncoding.OptimalControl.LogicalReversibleCost

def QuantumBlockEncoding.OptimalControl.evolvedEqFlipCost :
  QuantumBlockEncoding.OptimalControl.LogicalReversibleCost

Expanded score for the evolved equality-flag/parallel-flip construction.

Theorem8.3.62

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “evolved eq flip cost gate count”; 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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

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

Lean code for Theorem8.3.62●1 theorem

theoremdefined in QuantumBlockEncoding/OptimalControl.lean

complete

theorem QuantumBlockEncoding.OptimalControl.evolvedEqFlipCost_gateCount :
  QuantumBlockEncoding.OptimalControl.evolvedEqFlipCost.gateCount = 4

theorem QuantumBlockEncoding.OptimalControl.evolvedEqFlipCost_gateCount :
  QuantumBlockEncoding.OptimalControl.evolvedEqFlipCost.gateCount =
    4

Theorem8.3.63

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “evolved eq flip cost better than pro”; 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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

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

Lean code for Theorem8.3.63●1 theorem

theoremdefined in QuantumBlockEncoding/OptimalControl.lean

complete

theorem QuantumBlockEncoding.OptimalControl.evolvedEqFlipCost_betterThan_pro :
  QuantumBlockEncoding.OptimalControl.evolvedEqFlipCost.betterThan
    QuantumBlockEncoding.OptimalControl.proEqTransferCost

theorem QuantumBlockEncoding.OptimalControl.evolvedEqFlipCost_betterThan_pro :
  QuantumBlockEncoding.OptimalControl.evolvedEqFlipCost.betterThan
    QuantumBlockEncoding.OptimalControl.proEqTransferCost

Theorem8.3.64

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “evolved eq flip cost better than depth 5”; 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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

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

Lean code for Theorem8.3.64●1 theorem

theoremdefined in QuantumBlockEncoding/OptimalControl.lean

complete

theorem QuantumBlockEncoding.OptimalControl.evolvedEqFlipCost_betterThan_depth5 :
  QuantumBlockEncoding.OptimalControl.evolvedEqFlipCost.betterThan
    QuantumBlockEncoding.OptimalControl.reducedDepth5Cost

theorem QuantumBlockEncoding.OptimalControl.evolvedEqFlipCost_betterThan_depth5 :
  QuantumBlockEncoding.OptimalControl.evolvedEqFlipCost.betterThan
    QuantumBlockEncoding.OptimalControl.reducedDepth5Cost

Definition8.3.65

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “evolved eq flip unitary”. Matrix of the evolved depth-2 logical gate product.

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Matrix of the evolved depth-2 logical gate product.

Declaration kind. def.

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

Lean code for Definition8.3.65●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.evolvedEqFlipUnitary :
  QuantumBlockEncoding.Matrix 16 16 ℚ

def QuantumBlockEncoding.OptimalControl.evolvedEqFlipUnitary :
  QuantumBlockEncoding.Matrix 16 16 ℚ

Matrix of the evolved depth-2 logical gate product.

Theorem8.3.66

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “evolved eq flip unitary is rational orthogonal”; the hypotheses and conclusion in the code panel fix its exact scope. The evolved matrix is a concrete rational unitary matrix in the project-local real/permutation sense: both its column and row Gram matrices are identity.

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

Why it is in this chapter. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. The evolved matrix is a concrete rational unitary matrix in the project-local real/permutation sense: both its column and row Gram matrices are identity.

Declaration kind. theorem.

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

Lean code for Theorem8.3.66●1 theorem

theoremdefined in QuantumBlockEncoding/OptimalControl.lean

complete

theorem QuantumBlockEncoding.OptimalControl.evolvedEqFlipUnitary_isRationalOrthogonal :
  QuantumBlockEncoding.OptimalControl.IsRationalOrthogonal
    QuantumBlockEncoding.OptimalControl.evolvedEqFlipUnitary

theorem QuantumBlockEncoding.OptimalControl.evolvedEqFlipUnitary_isRationalOrthogonal :
  QuantumBlockEncoding.OptimalControl.IsRationalOrthogonal
    QuantumBlockEncoding.OptimalControl.evolvedEqFlipUnitary

The evolved matrix is a concrete rational unitary matrix in the project-local
real/permutation sense: both its column and row Gram matrices are identity.

Theorem8.3.67

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “evolved eq flip unitary clean block”; the hypotheses and conclusion in the code panel fix its exact scope. The evolved concrete matrix has the required clean block.

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

Why it is in this chapter. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. The evolved concrete matrix has the required clean block.

Declaration kind. theorem.

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

Lean code for Theorem8.3.67●1 theorem

theoremdefined in QuantumBlockEncoding/OptimalControl.lean

complete

theorem QuantumBlockEncoding.OptimalControl.evolvedEqFlipUnitary_cleanBlock
  (row col : Fin 8) :
  QuantumBlockEncoding.OptimalControl.evolvedEqFlipUnitary
      (QuantumBlockEncoding.OptimalControl.cleanIndex row)
      (QuantumBlockEncoding.OptimalControl.cleanIndex col) =
    QuantumBlockEncoding.OptimalControl.exampleOperator row col

theorem QuantumBlockEncoding.OptimalControl.evolvedEqFlipUnitary_cleanBlock
  (row col : Fin 8) :
  QuantumBlockEncoding.OptimalControl.evolvedEqFlipUnitary
      (QuantumBlockEncoding.OptimalControl.cleanIndex
        row)
      (QuantumBlockEncoding.OptimalControl.cleanIndex
        col) =
    QuantumBlockEncoding.OptimalControl.exampleOperator
      row col

The evolved concrete matrix has the required clean block.

Definition8.3.68

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “reduced gate matrix”. Full-space gate matrix for a reduced active-register permutation.

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Full-space gate matrix for a reduced active-register permutation.

Declaration kind. def.

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

Lean code for Definition8.3.68●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.reducedGateMatrix
  (gate : QuantumBlockEncoding.Gate) (f : Fin 8 → Fin 8) :
  QuantumBlockEncoding.GateMatrix ℚ 4

def QuantumBlockEncoding.OptimalControl.reducedGateMatrix
  (gate : QuantumBlockEncoding.Gate)
  (f : Fin 8 → Fin 8) :
  QuantumBlockEncoding.GateMatrix ℚ 4

Full-space gate matrix for a reduced active-register permutation.

Definition8.3.69

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “gate ccx type time aux”. Logical Toffoli gate 'CCX(type,time;aux)' in the concrete layout.

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Logical Toffoli gate 'CCX(type,time;aux)' in the concrete layout.

Declaration kind. def.

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

Lean code for Definition8.3.69●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.gateCCX_type_time_aux :
  QuantumBlockEncoding.Gate

def QuantumBlockEncoding.OptimalControl.gateCCX_type_time_aux :
  QuantumBlockEncoding.Gate

Logical Toffoli gate `CCX(type,time;aux)` in the concrete layout.

Definition8.3.70

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “gate x type”. Logical 'X' on the type bit in the concrete layout.

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Logical 'X' on the type bit in the concrete layout.

Declaration kind. def.

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

Lean code for Definition8.3.70●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.gateX_type :
  QuantumBlockEncoding.Gate

def QuantumBlockEncoding.OptimalControl.gateX_type :
  QuantumBlockEncoding.Gate

Logical `X` on the type bit in the concrete layout.

Definition8.3.71

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “gate x time”. Logical 'X' on the time bit in the concrete layout.

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Logical 'X' on the time bit in the concrete layout.

Declaration kind. def.

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

Lean code for Definition8.3.71●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.gateX_time :
  QuantumBlockEncoding.Gate

def QuantumBlockEncoding.OptimalControl.gateX_time :
  QuantumBlockEncoding.Gate

Logical `X` on the time bit in the concrete layout.

Definition8.3.72

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “gate x aux”. Logical 'X' on the block-encoding auxiliary bit in the concrete layout.

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Logical 'X' on the block-encoding auxiliary bit in the concrete layout.

Declaration kind. def.

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

Lean code for Definition8.3.72●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.gateX_aux :
  QuantumBlockEncoding.Gate

def QuantumBlockEncoding.OptimalControl.gateX_aux :
  QuantumBlockEncoding.Gate

Logical `X` on the block-encoding auxiliary bit in the concrete layout.

Definition8.3.73

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “gate cx type time”. Logical CNOT from type to time in the concrete layout.

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Logical CNOT from type to time in the concrete layout.

Declaration kind. def.

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

Lean code for Definition8.3.73●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.gateCX_type_time :
  QuantumBlockEncoding.Gate

def QuantumBlockEncoding.OptimalControl.gateCX_type_time :
  QuantumBlockEncoding.Gate

Logical CNOT from type to time in the concrete layout.

Definition8.3.74

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “gate cx time type”. Logical CNOT from time to type in the concrete layout.

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Logical CNOT from time to type in the concrete layout.

Declaration kind. def.

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

Lean code for Definition8.3.74●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.gateCX_time_type :
  QuantumBlockEncoding.Gate

def QuantumBlockEncoding.OptimalControl.gateCX_time_type :
  QuantumBlockEncoding.Gate

Logical CNOT from time to type in the concrete layout.

Definition8.3.75

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “gate cx aux type”. Logical CNOT from auxiliary to type in the concrete layout.

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Logical CNOT from auxiliary to type in the concrete layout.

Declaration kind. def.

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

Lean code for Definition8.3.75●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.gateCX_aux_type :
  QuantumBlockEncoding.Gate

def QuantumBlockEncoding.OptimalControl.gateCX_aux_type :
  QuantumBlockEncoding.Gate

Logical CNOT from auxiliary to type in the concrete layout.

Definition8.3.76

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “gate cx aux time”. Logical CNOT from auxiliary to time in the concrete layout.

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Logical CNOT from auxiliary to time in the concrete layout.

Declaration kind. def.

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

Lean code for Definition8.3.76●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.gateCX_aux_time :
  QuantumBlockEncoding.Gate

def QuantumBlockEncoding.OptimalControl.gateCX_aux_time :
  QuantumBlockEncoding.Gate

Logical CNOT from auxiliary to time in the concrete layout.

Definition8.3.77

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “reduced depth 5 circuit”. The depth-5 fixed-completion circuit in sequential-list form.

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. The depth-5 fixed-completion circuit in sequential-list form.

Declaration kind. def.

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

Lean code for Definition8.3.77●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.reducedDepth5Circuit :
  QuantumBlockEncoding.Circuit

def QuantumBlockEncoding.OptimalControl.reducedDepth5Circuit :
  QuantumBlockEncoding.Circuit

The depth-5 fixed-completion circuit in sequential-list form.

Definition8.3.78

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “reduced depth 5 schedule”. The depth-5 fixed-completion schedule.

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. The depth-5 fixed-completion schedule.

Declaration kind. def.

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

Lean code for Definition8.3.78●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.reducedDepth5Schedule :
  QuantumBlockEncoding.LayeredCircuit

def QuantumBlockEncoding.OptimalControl.reducedDepth5Schedule :
  QuantumBlockEncoding.LayeredCircuit

The depth-5 fixed-completion schedule.

Definition8.3.79

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “reduced depth 5 gate matrices”. Gate matrices for the depth-5 fixed-completion 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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Gate matrices for the depth-5 fixed-completion circuit.

Declaration kind. def.

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

Lean code for Definition8.3.79●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.reducedDepth5GateMatrices :
  List (QuantumBlockEncoding.GateMatrix ℚ 4)

def QuantumBlockEncoding.OptimalControl.reducedDepth5GateMatrices :
  List
    (QuantumBlockEncoding.GateMatrix ℚ 4)

Gate matrices for the depth-5 fixed-completion circuit.

Theorem8.3.80

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “reduced depth 5 gate matrices match circuit”; the hypotheses and conclusion in the code panel fix its exact scope. The gate-matrix labels match the depth-5 circuit transcript.

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

Why it is in this chapter. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. The gate-matrix labels match the depth-5 circuit transcript.

Declaration kind. theorem.

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

Lean code for Theorem8.3.80●1 theorem

theoremdefined in QuantumBlockEncoding/OptimalControl.lean

complete

theorem QuantumBlockEncoding.OptimalControl.reducedDepth5GateMatrices_matchCircuit :
  QuantumBlockEncoding.gateMatricesMatchCircuit
      QuantumBlockEncoding.OptimalControl.reducedDepth5Circuit
      QuantumBlockEncoding.OptimalControl.reducedDepth5GateMatrices =
    true

theorem QuantumBlockEncoding.OptimalControl.reducedDepth5GateMatrices_matchCircuit :
  QuantumBlockEncoding.gateMatricesMatchCircuit
      QuantumBlockEncoding.OptimalControl.reducedDepth5Circuit
      QuantumBlockEncoding.OptimalControl.reducedDepth5GateMatrices =
    true

The gate-matrix labels match the depth-5 circuit transcript.

Definition8.3.81

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “eval reduced gate images”. Evaluate reduced logical reversible gates as basis-state permutations.

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Evaluate reduced logical reversible gates as basis-state permutations.

Declaration kind. def.

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

Lean code for Definition8.3.81●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.evalReducedGateImages
  (gates : List (Fin 8 → Fin 8)) (x : Fin 8) : Fin 8

def QuantumBlockEncoding.OptimalControl.evalReducedGateImages
  (gates : List (Fin 8 → Fin 8))
  (x : Fin 8) : Fin 8

Evaluate reduced logical reversible gates as basis-state permutations.

Definition8.3.82

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “reduced depth 5 gate images”. Reduced permutation images of the depth-5 logical 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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Reduced permutation images of the depth-5 logical circuit.

Declaration kind. def.

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

Lean code for Definition8.3.82●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.reducedDepth5GateImages :
  List (Fin 8 → Fin 8)

def QuantumBlockEncoding.OptimalControl.reducedDepth5GateImages :
  List (Fin 8 → Fin 8)

Reduced permutation images of the depth-5 logical circuit.

Theorem8.3.83

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “reduced depth 5 gate images eval”; the hypotheses and conclusion in the code panel fix its exact scope. The depth-5 logical reversible circuit implements 'reducedDepth5Image'.

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

Why it is in this chapter. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. The depth-5 logical reversible circuit implements 'reducedDepth5Image'.

Declaration kind. theorem.

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

Lean code for Theorem8.3.83●1 theorem

theoremdefined in QuantumBlockEncoding/OptimalControl.lean

complete

theorem QuantumBlockEncoding.OptimalControl.reducedDepth5GateImages_eval
  (x : Fin 8) :
  QuantumBlockEncoding.OptimalControl.evalReducedGateImages
      QuantumBlockEncoding.OptimalControl.reducedDepth5GateImages x =
    QuantumBlockEncoding.OptimalControl.reducedDepth5Image x

theorem QuantumBlockEncoding.OptimalControl.reducedDepth5GateImages_eval
  (x : Fin 8) :
  QuantumBlockEncoding.OptimalControl.evalReducedGateImages
      QuantumBlockEncoding.OptimalControl.reducedDepth5GateImages
      x =
    QuantumBlockEncoding.OptimalControl.reducedDepth5Image
      x

The depth-5 logical reversible circuit implements `reducedDepth5Image`.

Definition8.3.84

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “pro eq transfer circuit”. Pro's equality-flag/transfer circuit in sequential-list form.

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Pro's equality-flag/transfer circuit in sequential-list form.

Declaration kind. def.

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

Lean code for Definition8.3.84●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.proEqTransferCircuit :
  QuantumBlockEncoding.Circuit

def QuantumBlockEncoding.OptimalControl.proEqTransferCircuit :
  QuantumBlockEncoding.Circuit

Pro's equality-flag/transfer circuit in sequential-list form.

Definition8.3.85

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “pro eq transfer schedule”. Pro's equality-flag/transfer schedule.

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Pro's equality-flag/transfer schedule.

Declaration kind. def.

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

Lean code for Definition8.3.85●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.proEqTransferSchedule :
  QuantumBlockEncoding.LayeredCircuit

def QuantumBlockEncoding.OptimalControl.proEqTransferSchedule :
  QuantumBlockEncoding.LayeredCircuit

Pro's equality-flag/transfer schedule.

Definition8.3.86

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “pro eq transfer gate matrices”. Gate matrices for Pro's equality-flag/transfer 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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Gate matrices for Pro's equality-flag/transfer circuit.

Declaration kind. def.

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

Lean code for Definition8.3.86●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.proEqTransferGateMatrices :
  List (QuantumBlockEncoding.GateMatrix ℚ 4)

def QuantumBlockEncoding.OptimalControl.proEqTransferGateMatrices :
  List
    (QuantumBlockEncoding.GateMatrix ℚ 4)

Gate matrices for Pro's equality-flag/transfer circuit.

Theorem8.3.87

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “pro eq transfer gate matrices match circuit”; the hypotheses and conclusion in the code panel fix its exact scope. The gate-matrix labels match Pro's circuit transcript.

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

Why it is in this chapter. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. The gate-matrix labels match Pro's circuit transcript.

Declaration kind. theorem.

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

Lean code for Theorem8.3.87●1 theorem

theoremdefined in QuantumBlockEncoding/OptimalControl.lean

complete

theorem QuantumBlockEncoding.OptimalControl.proEqTransferGateMatrices_matchCircuit :
  QuantumBlockEncoding.gateMatricesMatchCircuit
      QuantumBlockEncoding.OptimalControl.proEqTransferCircuit
      QuantumBlockEncoding.OptimalControl.proEqTransferGateMatrices =
    true

theorem QuantumBlockEncoding.OptimalControl.proEqTransferGateMatrices_matchCircuit :
  QuantumBlockEncoding.gateMatricesMatchCircuit
      QuantumBlockEncoding.OptimalControl.proEqTransferCircuit
      QuantumBlockEncoding.OptimalControl.proEqTransferGateMatrices =
    true

The gate-matrix labels match Pro's circuit transcript.

Definition8.3.88

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “pro eq transfer gate images”. Reduced permutation images of Pro's logical 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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Reduced permutation images of Pro's logical circuit.

Declaration kind. def.

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

Lean code for Definition8.3.88●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.proEqTransferGateImages :
  List (Fin 8 → Fin 8)

def QuantumBlockEncoding.OptimalControl.proEqTransferGateImages :
  List (Fin 8 → Fin 8)

Reduced permutation images of Pro's logical circuit.

Theorem8.3.89

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “pro eq transfer gate images eval”; the hypotheses and conclusion in the code panel fix its exact scope. Pro's logical reversible circuit implements 'proEqTransferImage'.

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

Why it is in this chapter. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Pro's logical reversible circuit implements 'proEqTransferImage'.

Declaration kind. theorem.

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

Lean code for Theorem8.3.89●1 theorem

theoremdefined in QuantumBlockEncoding/OptimalControl.lean

complete

theorem QuantumBlockEncoding.OptimalControl.proEqTransferGateImages_eval
  (x : Fin 8) :
  QuantumBlockEncoding.OptimalControl.evalReducedGateImages
      QuantumBlockEncoding.OptimalControl.proEqTransferGateImages x =
    QuantumBlockEncoding.OptimalControl.proEqTransferImage x

theorem QuantumBlockEncoding.OptimalControl.proEqTransferGateImages_eval
  (x : Fin 8) :
  QuantumBlockEncoding.OptimalControl.evalReducedGateImages
      QuantumBlockEncoding.OptimalControl.proEqTransferGateImages
      x =
    QuantumBlockEncoding.OptimalControl.proEqTransferImage
      x

Pro's logical reversible circuit implements `proEqTransferImage`.

Definition8.3.90

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “evolved eq flip circuit”. The evolved depth-2 circuit in sequential-list form.

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. The evolved depth-2 circuit in sequential-list form.

Declaration kind. def.

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

Lean code for Definition8.3.90●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.evolvedEqFlipCircuit :
  QuantumBlockEncoding.Circuit

def QuantumBlockEncoding.OptimalControl.evolvedEqFlipCircuit :
  QuantumBlockEncoding.Circuit

The evolved depth-2 circuit in sequential-list form.

Definition8.3.91

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “evolved eq flip schedule”. The evolved depth-2 schedule: one Toffoli layer, then three parallel flips.

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. The evolved depth-2 schedule: one Toffoli layer, then three parallel flips.

Declaration kind. def.

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

Lean code for Definition8.3.91●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.evolvedEqFlipSchedule :
  QuantumBlockEncoding.LayeredCircuit

def QuantumBlockEncoding.OptimalControl.evolvedEqFlipSchedule :
  QuantumBlockEncoding.LayeredCircuit

The evolved depth-2 schedule: one Toffoli layer, then three parallel flips.

Definition8.3.92

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “evolved eq flip gate matrices”. Gate matrices for the evolved concrete 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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Gate matrices for the evolved concrete circuit.

Declaration kind. def.

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

Lean code for Definition8.3.92●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.evolvedEqFlipGateMatrices :
  List (QuantumBlockEncoding.GateMatrix ℚ 4)

def QuantumBlockEncoding.OptimalControl.evolvedEqFlipGateMatrices :
  List
    (QuantumBlockEncoding.GateMatrix ℚ 4)

Gate matrices for the evolved concrete circuit.

Theorem8.3.93

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “evolved eq flip gate matrices match circuit”; the hypotheses and conclusion in the code panel fix its exact scope. The gate-matrix labels match the evolved circuit transcript.

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

Why it is in this chapter. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. The gate-matrix labels match the evolved circuit transcript.

Declaration kind. theorem.

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

Lean code for Theorem8.3.93●1 theorem

theoremdefined in QuantumBlockEncoding/OptimalControl.lean

complete

theorem QuantumBlockEncoding.OptimalControl.evolvedEqFlipGateMatrices_matchCircuit :
  QuantumBlockEncoding.gateMatricesMatchCircuit
      QuantumBlockEncoding.OptimalControl.evolvedEqFlipCircuit
      QuantumBlockEncoding.OptimalControl.evolvedEqFlipGateMatrices =
    true

theorem QuantumBlockEncoding.OptimalControl.evolvedEqFlipGateMatrices_matchCircuit :
  QuantumBlockEncoding.gateMatricesMatchCircuit
      QuantumBlockEncoding.OptimalControl.evolvedEqFlipCircuit
      QuantumBlockEncoding.OptimalControl.evolvedEqFlipGateMatrices =
    true

The gate-matrix labels match the evolved circuit transcript.

Definition8.3.94

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “evolved eq flip gate images”. Reduced permutation images of the evolved logical 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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Reduced permutation images of the evolved logical circuit.

Declaration kind. def.

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

Lean code for Definition8.3.94●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.evolvedEqFlipGateImages :
  List (Fin 8 → Fin 8)

def QuantumBlockEncoding.OptimalControl.evolvedEqFlipGateImages :
  List (Fin 8 → Fin 8)

Reduced permutation images of the evolved logical circuit.

Theorem8.3.95

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “evolved eq flip gate images eval”; the hypotheses and conclusion in the code panel fix its exact scope. The logical reversible circuit implements exactly the reduced permutation used to build 'evolvedEqFlipUnitary'.

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

Why it is in this chapter. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. The logical reversible circuit implements exactly the reduced permutation used to build 'evolvedEqFlipUnitary'. This is the efficient semantic bridge for the current logical reversible tier; the heavier raw 'evalGateMatrices' product is left to a later backend if the project chooses a hardware decomposition.

Declaration kind. theorem.

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

Lean code for Theorem8.3.95●1 theorem

theoremdefined in QuantumBlockEncoding/OptimalControl.lean

complete

theorem QuantumBlockEncoding.OptimalControl.evolvedEqFlipGateImages_eval
  (x : Fin 8) :
  QuantumBlockEncoding.OptimalControl.evalReducedGateImages
      QuantumBlockEncoding.OptimalControl.evolvedEqFlipGateImages x =
    QuantumBlockEncoding.OptimalControl.evolvedEqFlipImage x

theorem QuantumBlockEncoding.OptimalControl.evolvedEqFlipGateImages_eval
  (x : Fin 8) :
  QuantumBlockEncoding.OptimalControl.evalReducedGateImages
      QuantumBlockEncoding.OptimalControl.evolvedEqFlipGateImages
      x =
    QuantumBlockEncoding.OptimalControl.evolvedEqFlipImage
      x

The logical reversible circuit implements exactly the reduced permutation used
to build `evolvedEqFlipUnitary`.  This is the efficient semantic bridge for the
current logical reversible tier; the heavier raw `evalGateMatrices` product is
left to a later backend if the project chooses a hardware decomposition.

Theorem8.3.96

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “evolved eq flip gate images lift eval”; the hypotheses and conclusion in the code panel fix its exact scope. The lifted logical circuit implements the full active-plus-state image.

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

Why it is in this chapter. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. The lifted logical circuit implements the full active-plus-state image.

Declaration kind. theorem.

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

Lean code for Theorem8.3.96●1 theorem

theoremdefined in QuantumBlockEncoding/OptimalControl.lean

complete

theorem QuantumBlockEncoding.OptimalControl.evolvedEqFlipGateImages_lift_eval
  (x : Fin 16) :
  QuantumBlockEncoding.OptimalControl.liftReducedImage
      (QuantumBlockEncoding.OptimalControl.evalReducedGateImages
        QuantumBlockEncoding.OptimalControl.evolvedEqFlipGateImages)
      x =
    QuantumBlockEncoding.OptimalControl.liftReducedImage
      QuantumBlockEncoding.OptimalControl.evolvedEqFlipImage x

theorem QuantumBlockEncoding.OptimalControl.evolvedEqFlipGateImages_lift_eval
  (x : Fin 16) :
  QuantumBlockEncoding.OptimalControl.liftReducedImage
      (QuantumBlockEncoding.OptimalControl.evalReducedGateImages
        QuantumBlockEncoding.OptimalControl.evolvedEqFlipGateImages)
      x =
    QuantumBlockEncoding.OptimalControl.liftReducedImage
      QuantumBlockEncoding.OptimalControl.evolvedEqFlipImage
      x

The lifted logical circuit implements the full active-plus-state image.

Definition8.3.97

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “reduced depth 5 resource”. Resource record for the depth-5 logical '{X,CNOT,Toffoli}' interpretation.

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Resource record for the depth-5 logical '{X,CNOT,Toffoli}' interpretation. The current 'Resource' type has no Toffoli field, so 'cnot' stores all controlled logical gates in this tier.

Declaration kind. def.

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

Lean code for Definition8.3.97●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.reducedDepth5Resource :
  QuantumBlockEncoding.Resource

def QuantumBlockEncoding.OptimalControl.reducedDepth5Resource :
  QuantumBlockEncoding.Resource

Resource record for the depth-5 logical `{X,CNOT,Toffoli}` interpretation.
The current `Resource` type has no Toffoli field, so `cnot` stores all
controlled logical gates in this tier.

Definition8.3.98

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “pro eq transfer resource”. Resource record for Pro's logical '{X,CNOT,Toffoli}' interpretation.

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Resource record for Pro's logical '{X,CNOT,Toffoli}' interpretation. The current 'Resource' type has no Toffoli field, so 'cnot' stores all controlled logical gates in this tier.

Declaration kind. def.

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

Lean code for Definition8.3.98●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.proEqTransferResource :
  QuantumBlockEncoding.Resource

def QuantumBlockEncoding.OptimalControl.proEqTransferResource :
  QuantumBlockEncoding.Resource

Resource record for Pro's logical `{X,CNOT,Toffoli}` interpretation.  The
current `Resource` type has no Toffoli field, so `cnot` stores all controlled
logical gates in this tier.

Definition8.3.99

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “evolved eq flip resource”. Resource record for the evolved logical '{X,CNOT,Toffoli}' interpretation.

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Resource record for the evolved logical '{X,CNOT,Toffoli}' interpretation. The current 'Resource' type has no Toffoli field, so 'cnot' stores the single logical Toffoli in this tier.

Declaration kind. def.

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

Lean code for Definition8.3.99●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.evolvedEqFlipResource :
  QuantumBlockEncoding.Resource

def QuantumBlockEncoding.OptimalControl.evolvedEqFlipResource :
  QuantumBlockEncoding.Resource

Resource record for the evolved logical `{X,CNOT,Toffoli}` interpretation.
The current `Resource` type has no Toffoli field, so `cnot` stores the single
logical Toffoli in this tier.

Definition8.3.100

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “reduced depth 5 candidate”. Verified candidate data for the older depth-5 concrete logical BE.

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Verified candidate data for the older depth-5 concrete logical BE.

Declaration kind. def.

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

Lean code for Definition8.3.100●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.reducedDepth5Candidate :
  QuantumBlockEncoding.OperatorBlockEncodingCandidate ℚ 3

def QuantumBlockEncoding.OptimalControl.reducedDepth5Candidate :
  QuantumBlockEncoding.OperatorBlockEncodingCandidate
    ℚ 3

Verified candidate data for the older depth-5 concrete logical BE.

Definition8.3.101

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “reduced depth 5 verified”. Verified concrete depth-5 block encoding for 'E_1'.

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Verified concrete depth-5 block encoding for 'E_1'.

Declaration kind. def.

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

Lean code for Definition8.3.101●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.reducedDepth5Verified :
  QuantumBlockEncoding.VerifiedOperatorBlockEncoding ℚ 3

def QuantumBlockEncoding.OptimalControl.reducedDepth5Verified :
  QuantumBlockEncoding.VerifiedOperatorBlockEncoding
    ℚ 3

Verified concrete depth-5 block encoding for `E_1`.

Theorem8.3.102

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “reduced depth 5 candidate cost”; the hypotheses and conclusion in the code panel fix its exact scope. The verified depth-5 candidate has the advertised logical-library score.

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

Why it is in this chapter. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. The verified depth-5 candidate has the advertised logical-library score.

Declaration kind. theorem.

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

Lean code for Theorem8.3.102●1 theorem

theoremdefined in QuantumBlockEncoding/OptimalControl.lean

complete

theorem QuantumBlockEncoding.OptimalControl.reducedDepth5Candidate_cost :
  QuantumBlockEncoding.OptimalControl.reducedDepth5Candidate.cost =
    { auxiliaryQubits := 1, gateCount := 6, depth := 5,
      oracleCalls := 0 }

theorem QuantumBlockEncoding.OptimalControl.reducedDepth5Candidate_cost :
  QuantumBlockEncoding.OptimalControl.reducedDepth5Candidate.cost =
    { auxiliaryQubits := 1,
      gateCount := 6, depth := 5,
      oracleCalls := 0 }

The verified depth-5 candidate has the advertised logical-library score.

Definition8.3.103

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “pro eq transfer candidate”. Verified candidate data for Pro's equality-flag/transfer BE.

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Verified candidate data for Pro's equality-flag/transfer BE.

Declaration kind. def.

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

Lean code for Definition8.3.103●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.proEqTransferCandidate :
  QuantumBlockEncoding.OperatorBlockEncodingCandidate ℚ 3

def QuantumBlockEncoding.OptimalControl.proEqTransferCandidate :
  QuantumBlockEncoding.OperatorBlockEncodingCandidate
    ℚ 3

Verified candidate data for Pro's equality-flag/transfer BE.

Definition8.3.104

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “pro eq transfer verified”. Verified concrete Pro block encoding for 'E_1'.

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Verified concrete Pro block encoding for 'E_1'.

Declaration kind. def.

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

Lean code for Definition8.3.104●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.proEqTransferVerified :
  QuantumBlockEncoding.VerifiedOperatorBlockEncoding ℚ 3

def QuantumBlockEncoding.OptimalControl.proEqTransferVerified :
  QuantumBlockEncoding.VerifiedOperatorBlockEncoding
    ℚ 3

Verified concrete Pro block encoding for `E_1`.

Theorem8.3.105

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “pro eq transfer candidate cost”; the hypotheses and conclusion in the code panel fix its exact scope. The verified Pro candidate has the advertised logical-library score.

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

Why it is in this chapter. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. The verified Pro candidate has the advertised logical-library score.

Declaration kind. theorem.

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

Lean code for Theorem8.3.105●1 theorem

theoremdefined in QuantumBlockEncoding/OptimalControl.lean

complete

theorem QuantumBlockEncoding.OptimalControl.proEqTransferCandidate_cost :
  QuantumBlockEncoding.OptimalControl.proEqTransferCandidate.cost =
    { auxiliaryQubits := 1, gateCount := 4, depth := 4,
      oracleCalls := 0 }

theorem QuantumBlockEncoding.OptimalControl.proEqTransferCandidate_cost :
  QuantumBlockEncoding.OptimalControl.proEqTransferCandidate.cost =
    { auxiliaryQubits := 1,
      gateCount := 4, depth := 4,
      oracleCalls := 0 }

The verified Pro candidate has the advertised logical-library score.

Definition8.3.106

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “evolved eq flip candidate”. Final concrete block-encoding candidate for the one-time-bit, one-type-bit, one-state-bit optimal-control 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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Final concrete block-encoding candidate for the one-time-bit, one-type-bit, one-state-bit optimal-control target. This is final only for this concrete logical gate-matrix tier; general 'k', wider time registers, and hardware decomposition remain separate tasks.

Declaration kind. def.

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

Lean code for Definition8.3.106●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.evolvedEqFlipCandidate :
  QuantumBlockEncoding.OperatorBlockEncodingCandidate ℚ 3

def QuantumBlockEncoding.OptimalControl.evolvedEqFlipCandidate :
  QuantumBlockEncoding.OperatorBlockEncodingCandidate
    ℚ 3

Final concrete block-encoding candidate for the one-time-bit, one-type-bit,
one-state-bit optimal-control target.  This is final only for this concrete
logical gate-matrix tier; general `k`, wider time registers, and hardware
decomposition remain separate tasks.

Definition8.3.107

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “evolved eq flip verified”. Verified concrete depth-2 block encoding for 'E_1'.

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Verified concrete depth-2 block encoding for 'E_1'.

Declaration kind. def.

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

Lean code for Definition8.3.107●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.evolvedEqFlipVerified :
  QuantumBlockEncoding.VerifiedOperatorBlockEncoding ℚ 3

def QuantumBlockEncoding.OptimalControl.evolvedEqFlipVerified :
  QuantumBlockEncoding.VerifiedOperatorBlockEncoding
    ℚ 3

Verified concrete depth-2 block encoding for `E_1`.

Definition8.3.108

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “evolved eq flip zero error approx”. The exact evolved candidate is also a zero-error approximate block encoding.

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. The exact evolved candidate is also a zero-error approximate block encoding. This is the Lean anchor for Scenario 1 of the adaptive exact-to-approximate policy: after exact convergence, approximate search may continue, but the current champion already satisfies every nonnegative requested tolerance.

Declaration kind. def.

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

Lean code for Definition8.3.108●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.evolvedEqFlipZeroErrorApprox :
  QuantumBlockEncoding.VerifiedApproximateOperatorBlockEncoding ℚ 3

def QuantumBlockEncoding.OptimalControl.evolvedEqFlipZeroErrorApprox :
  QuantumBlockEncoding.VerifiedApproximateOperatorBlockEncoding
    ℚ 3

The exact evolved candidate is also a zero-error approximate block encoding.
This is the Lean anchor for Scenario 1 of the adaptive exact-to-approximate
policy: after exact convergence, approximate search may continue, but the
current champion already satisfies every nonnegative requested tolerance.

Theorem8.3.109

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “evolved eq flip candidate cost”; the hypotheses and conclusion in the code panel fix its exact scope. The verified evolved candidate has the advertised logical-library score.

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

Why it is in this chapter. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. The verified evolved candidate has the advertised logical-library score.

Declaration kind. theorem.

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

Lean code for Theorem8.3.109●1 theorem

theoremdefined in QuantumBlockEncoding/OptimalControl.lean

complete

theorem QuantumBlockEncoding.OptimalControl.evolvedEqFlipCandidate_cost :
  QuantumBlockEncoding.OptimalControl.evolvedEqFlipCandidate.cost =
    { auxiliaryQubits := 1, gateCount := 4, depth := 2,
      oracleCalls := 0 }

theorem QuantumBlockEncoding.OptimalControl.evolvedEqFlipCandidate_cost :
  QuantumBlockEncoding.OptimalControl.evolvedEqFlipCandidate.cost =
    { auxiliaryQubits := 1,
      gateCount := 4, depth := 2,
      oracleCalls := 0 }

The verified evolved candidate has the advertised logical-library score.

Definition8.3.110

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “direct route ablation target”. Route-ablation target block with entries 'target[0, 6] = 1' and 'target[1, 7] = 1', and all other entries zero.

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Route-ablation target block with entries 'target[0, 6] = 1' and 'target[1, 7] = 1', and all other entries zero.

Declaration kind. def.

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

Lean code for Definition8.3.110●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.directRouteAblationTarget :
  QuantumBlockEncoding.Matrix 8 8 ℚ

def QuantumBlockEncoding.OptimalControl.directRouteAblationTarget :
  QuantumBlockEncoding.Matrix 8 8 ℚ

Route-ablation target block with entries `target[0, 6] = 1` and
`target[1, 7] = 1`, and all other entries zero.

Theorem8.3.111

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “direct route ablation target eq example operator”; the hypotheses and conclusion in the code panel fix its exact scope. The route-ablation target is entrywise the concrete 'E_1' target used above.

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

Why it is in this chapter. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. The route-ablation target is entrywise the concrete 'E_1' target used above.

Declaration kind. theorem.

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

Lean code for Theorem8.3.111●1 theorem

theoremdefined in QuantumBlockEncoding/OptimalControl.lean

complete

theorem QuantumBlockEncoding.OptimalControl.directRouteAblationTarget_eq_exampleOperator
  (row col : Fin 8) :
  QuantumBlockEncoding.OptimalControl.directRouteAblationTarget row
      col =
    QuantumBlockEncoding.OptimalControl.exampleOperator row col

theorem QuantumBlockEncoding.OptimalControl.directRouteAblationTarget_eq_exampleOperator
  (row col : Fin 8) :
  QuantumBlockEncoding.OptimalControl.directRouteAblationTarget
      row col =
    QuantumBlockEncoding.OptimalControl.exampleOperator
      row col

The route-ablation target is entrywise the concrete `E_1` target used above.

Definition8.3.112

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “direct route ablation circuit”. Direct route-ablation circuit in sequential-list form.

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Direct route-ablation circuit in sequential-list form.

Declaration kind. def.

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

Lean code for Definition8.3.112●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.directRouteAblationCircuit :
  QuantumBlockEncoding.Circuit

def QuantumBlockEncoding.OptimalControl.directRouteAblationCircuit :
  QuantumBlockEncoding.Circuit

Direct route-ablation circuit in sequential-list form.

Definition8.3.113

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “direct route ablation schedule”. Direct route-ablation schedule: Toffoli first, then the three flips.

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Direct route-ablation schedule: Toffoli first, then the three flips.

Declaration kind. def.

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

Lean code for Definition8.3.113●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.directRouteAblationSchedule :
  QuantumBlockEncoding.LayeredCircuit

def QuantumBlockEncoding.OptimalControl.directRouteAblationSchedule :
  QuantumBlockEncoding.LayeredCircuit

Direct route-ablation schedule: Toffoli first, then the three flips.

Definition8.3.114

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “direct route ablation gate images”. Reduced permutation images for the direct route-ablation 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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Reduced permutation images for the direct route-ablation circuit.

Declaration kind. def.

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

Lean code for Definition8.3.114●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.directRouteAblationGateImages :
  List (Fin 8 → Fin 8)

def QuantumBlockEncoding.OptimalControl.directRouteAblationGateImages :
  List (Fin 8 → Fin 8)

Reduced permutation images for the direct route-ablation circuit.

Definition8.3.115

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “direct route ablation image”. Reduced active-register image induced by the direct route-ablation 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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Reduced active-register image induced by the direct route-ablation circuit.

Declaration kind. def.

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

Lean code for Definition8.3.115●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.directRouteAblationImage
  (x : Fin 8) : Fin 8

def QuantumBlockEncoding.OptimalControl.directRouteAblationImage
  (x : Fin 8) : Fin 8

Reduced active-register image induced by the direct route-ablation circuit.

Theorem8.3.116

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “direct route ablation gate images eval”; the hypotheses and conclusion in the code panel fix its exact scope. The direct route-ablation circuit is the stated 'CCX; X(type); X(time); X(aux)' map.

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

Why it is in this chapter. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. The direct route-ablation circuit is the stated 'CCX; X(type); X(time); X(aux)' map.

Declaration kind. theorem.

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

Lean code for Theorem8.3.116●1 theorem

theoremdefined in QuantumBlockEncoding/OptimalControl.lean

complete

theorem QuantumBlockEncoding.OptimalControl.directRouteAblationGateImages_eval
  (x : Fin 8) :
  QuantumBlockEncoding.OptimalControl.directRouteAblationImage x =
    QuantumBlockEncoding.OptimalControl.redX2
      (QuantumBlockEncoding.OptimalControl.redX1
        (QuantumBlockEncoding.OptimalControl.redX0
          (QuantumBlockEncoding.OptimalControl.redCCX012 x)))

theorem QuantumBlockEncoding.OptimalControl.directRouteAblationGateImages_eval
  (x : Fin 8) :
  QuantumBlockEncoding.OptimalControl.directRouteAblationImage
      x =
    QuantumBlockEncoding.OptimalControl.redX2
      (QuantumBlockEncoding.OptimalControl.redX1
        (QuantumBlockEncoding.OptimalControl.redX0
          (QuantumBlockEncoding.OptimalControl.redCCX012
            x)))

The direct route-ablation circuit is the stated `CCX; X(type); X(time); X(aux)` map.

Theorem8.3.117

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “direct route ablation image is permutation”; the hypotheses and conclusion in the code panel fix its exact scope. The direct route-ablation image is a finite permutation.

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

Why it is in this chapter. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. The direct route-ablation image is a finite permutation.

Declaration kind. theorem.

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

Lean code for Theorem8.3.117●1 theorem

theoremdefined in QuantumBlockEncoding/OptimalControl.lean

complete

theorem QuantumBlockEncoding.OptimalControl.directRouteAblationImage_isPermutation :
  QuantumBlockEncoding.OptimalControl.IsPermutation
    QuantumBlockEncoding.OptimalControl.directRouteAblationImage

theorem QuantumBlockEncoding.OptimalControl.directRouteAblationImage_isPermutation :
  QuantumBlockEncoding.OptimalControl.IsPermutation
    QuantumBlockEncoding.OptimalControl.directRouteAblationImage

The direct route-ablation image is a finite permutation.

Definition8.3.118

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “direct route ablation unitary”. Matrix of the direct route-ablation logical 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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Matrix of the direct route-ablation logical circuit.

Declaration kind. def.

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

Lean code for Definition8.3.118●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.directRouteAblationUnitary :
  QuantumBlockEncoding.Matrix 16 16 ℚ

def QuantumBlockEncoding.OptimalControl.directRouteAblationUnitary :
  QuantumBlockEncoding.Matrix 16 16 ℚ

Matrix of the direct route-ablation logical circuit.

Theorem8.3.119

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “direct route ablation unitary is rational orthogonal”; the hypotheses and conclusion in the code panel fix its exact scope. The direct route-ablation matrix is rational orthogonal/unitary in the project-local finite permutation sense.

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

Why it is in this chapter. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. The direct route-ablation matrix is rational orthogonal/unitary in the project-local finite permutation sense.

Declaration kind. theorem.

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

Lean code for Theorem8.3.119●1 theorem

theoremdefined in QuantumBlockEncoding/OptimalControl.lean

complete

theorem QuantumBlockEncoding.OptimalControl.directRouteAblationUnitary_isRationalOrthogonal :
  QuantumBlockEncoding.OptimalControl.IsRationalOrthogonal
    QuantumBlockEncoding.OptimalControl.directRouteAblationUnitary

theorem QuantumBlockEncoding.OptimalControl.directRouteAblationUnitary_isRationalOrthogonal :
  QuantumBlockEncoding.OptimalControl.IsRationalOrthogonal
    QuantumBlockEncoding.OptimalControl.directRouteAblationUnitary

The direct route-ablation matrix is rational orthogonal/unitary in the
project-local finite permutation sense.

Theorem8.3.120

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “direct route ablation clean block”; the hypotheses and conclusion in the code panel fix its exact scope. Named clean-block theorem for the controlled route ablation.

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

Why it is in this chapter. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Named clean-block theorem for the controlled route ablation. The top-left auxiliary block, with auxiliary input and output both '0', is exactly the requested 'E_1' matrix.

Declaration kind. theorem.

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

Lean code for Theorem8.3.120●1 theorem

theoremdefined in QuantumBlockEncoding/OptimalControl.lean

complete

theorem QuantumBlockEncoding.OptimalControl.directRouteAblation_cleanBlock
  (row col : Fin 8) :
  QuantumBlockEncoding.OptimalControl.directRouteAblationUnitary
      (QuantumBlockEncoding.OptimalControl.cleanIndex row)
      (QuantumBlockEncoding.OptimalControl.cleanIndex col) =
    QuantumBlockEncoding.OptimalControl.directRouteAblationTarget row
      col

theorem QuantumBlockEncoding.OptimalControl.directRouteAblation_cleanBlock
  (row col : Fin 8) :
  QuantumBlockEncoding.OptimalControl.directRouteAblationUnitary
      (QuantumBlockEncoding.OptimalControl.cleanIndex
        row)
      (QuantumBlockEncoding.OptimalControl.cleanIndex
        col) =
    QuantumBlockEncoding.OptimalControl.directRouteAblationTarget
      row col

Named clean-block theorem for the controlled route ablation.  The top-left
auxiliary block, with auxiliary input and output both `0`, is exactly the
requested `E_1` matrix.

Definition8.3.121

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “direct route ablation gate matrices”. Gate matrices for the direct route-ablation 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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Gate matrices for the direct route-ablation circuit.

Declaration kind. def.

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

Lean code for Definition8.3.121●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.directRouteAblationGateMatrices :
  List (QuantumBlockEncoding.GateMatrix ℚ 4)

def QuantumBlockEncoding.OptimalControl.directRouteAblationGateMatrices :
  List
    (QuantumBlockEncoding.GateMatrix ℚ 4)

Gate matrices for the direct route-ablation circuit.

Theorem8.3.122

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “direct route ablation gate matrices match circuit”; the hypotheses and conclusion in the code panel fix its exact scope. The direct route-ablation gate-matrix labels match its circuit transcript.

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

Why it is in this chapter. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. The direct route-ablation gate-matrix labels match its circuit transcript.

Declaration kind. theorem.

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

Lean code for Theorem8.3.122●1 theorem

theoremdefined in QuantumBlockEncoding/OptimalControl.lean

complete

theorem QuantumBlockEncoding.OptimalControl.directRouteAblationGateMatrices_matchCircuit :
  QuantumBlockEncoding.gateMatricesMatchCircuit
      QuantumBlockEncoding.OptimalControl.directRouteAblationCircuit
      QuantumBlockEncoding.OptimalControl.directRouteAblationGateMatrices =
    true

theorem QuantumBlockEncoding.OptimalControl.directRouteAblationGateMatrices_matchCircuit :
  QuantumBlockEncoding.gateMatricesMatchCircuit
      QuantumBlockEncoding.OptimalControl.directRouteAblationCircuit
      QuantumBlockEncoding.OptimalControl.directRouteAblationGateMatrices =
    true

The direct route-ablation gate-matrix labels match its circuit transcript.

Definition8.3.123

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “direct route ablation cost”. Logical-library cost for the direct route-ablation 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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Logical-library cost for the direct route-ablation circuit.

Declaration kind. def.

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

Lean code for Definition8.3.123●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.directRouteAblationCost :
  QuantumBlockEncoding.OptimalControl.LogicalReversibleCost

def QuantumBlockEncoding.OptimalControl.directRouteAblationCost :
  QuantumBlockEncoding.OptimalControl.LogicalReversibleCost

Logical-library cost for the direct route-ablation circuit.

Definition8.3.124

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “direct route ablation resource tuple”. Resource tuple in route-ablation order: '(gateCount, depth, auxiliaryQubits, oracleCalls)'.

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Resource tuple in route-ablation order: '(gateCount, depth, auxiliaryQubits, oracleCalls)'.

Declaration kind. def.

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

Lean code for Definition8.3.124●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.directRouteAblationResourceTuple :
  ℕ × ℕ × ℕ × ℕ

def QuantumBlockEncoding.OptimalControl.directRouteAblationResourceTuple :
  ℕ × ℕ × ℕ × ℕ

Resource tuple in route-ablation order: `(gateCount, depth, auxiliaryQubits, oracleCalls)`.

Theorem8.3.125

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “direct route ablation resource tuple eq”; the hypotheses and conclusion in the code panel fix its exact scope. The direct route-ablation resource tuple is '(4, 2, 1, 0)'.

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

Why it is in this chapter. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. The direct route-ablation resource tuple is '(4, 2, 1, 0)'.

Declaration kind. theorem.

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

Lean code for Theorem8.3.125●1 theorem

theoremdefined in QuantumBlockEncoding/OptimalControl.lean

complete

theorem QuantumBlockEncoding.OptimalControl.directRouteAblationResourceTuple_eq :
  QuantumBlockEncoding.OptimalControl.directRouteAblationResourceTuple =
    (4, 2, 1, 0)

theorem QuantumBlockEncoding.OptimalControl.directRouteAblationResourceTuple_eq :
  QuantumBlockEncoding.OptimalControl.directRouteAblationResourceTuple =
    (4, 2, 1, 0)

The direct route-ablation resource tuple is `(4, 2, 1, 0)`.

Definition8.3.126

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “example unitary”. Matrix of the one-ancilla permutation unitary completion.

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. Matrix of the one-ancilla permutation unitary completion.

Declaration kind. def.

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

Lean code for Definition8.3.126●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.exampleUnitary :
  QuantumBlockEncoding.Matrix 16 16 ℚ

def QuantumBlockEncoding.OptimalControl.exampleUnitary :
  QuantumBlockEncoding.Matrix 16 16 ℚ

Matrix of the one-ancilla permutation unitary completion.

Theorem8.3.127

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “example clean block”; the hypotheses and conclusion in the code panel fix its exact scope. The clean block of 'exampleUnitary' is exactly the optimal-control operator 'E_1' on the 8-dimensional system register.

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

Why it is in this chapter. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

Technical source note. The clean block of 'exampleUnitary' is exactly the optimal-control operator 'E_1' on the 8-dimensional system register.

Declaration kind. theorem.

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

Lean code for Theorem8.3.127●1 theorem

theoremdefined in QuantumBlockEncoding/OptimalControl.lean

complete

theorem QuantumBlockEncoding.OptimalControl.example_cleanBlock
  (row col : Fin 8) :
  QuantumBlockEncoding.OptimalControl.exampleUnitary
      (QuantumBlockEncoding.OptimalControl.cleanIndex row)
      (QuantumBlockEncoding.OptimalControl.cleanIndex col) =
    QuantumBlockEncoding.OptimalControl.exampleOperator row col

theorem QuantumBlockEncoding.OptimalControl.example_cleanBlock
  (row col : Fin 8) :
  QuantumBlockEncoding.OptimalControl.exampleUnitary
      (QuantumBlockEncoding.OptimalControl.cleanIndex
        row)
      (QuantumBlockEncoding.OptimalControl.cleanIndex
        col) =
    QuantumBlockEncoding.OptimalControl.exampleOperator
      row col

The clean block of `exampleUnitary` is exactly the optimal-control operator
`E_1` on the 8-dimensional system register.

Definition8.3.128

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “example 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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

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

Lean code for Definition8.3.128●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.exampleCircuit :
  QuantumBlockEncoding.Circuit

def QuantumBlockEncoding.OptimalControl.exampleCircuit :
  QuantumBlockEncoding.Circuit

Definition8.3.129

uses 0used by 0✓L∃∀N

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

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

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

Lean code for Definition8.3.129●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.exampleSchedule :
  QuantumBlockEncoding.LayeredCircuit

def QuantumBlockEncoding.OptimalControl.exampleSchedule :
  QuantumBlockEncoding.LayeredCircuit

Definition8.3.130

uses 0used by 0✓L∃∀N

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

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

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

Lean code for Definition8.3.130●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.exampleResource :
  QuantumBlockEncoding.Resource

def QuantumBlockEncoding.OptimalControl.exampleResource :
  QuantumBlockEncoding.Resource

Definition8.3.131

uses 0used by 0✓L∃∀N

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

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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

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

Lean code for Definition8.3.131●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.exampleCandidate :
  QuantumBlockEncoding.OperatorBlockEncodingCandidate ℚ 3

def QuantumBlockEncoding.OptimalControl.exampleCandidate :
  QuantumBlockEncoding.OperatorBlockEncodingCandidate
    ℚ 3

Definition8.3.132

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “example 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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

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

Lean code for Definition8.3.132●1 definition

defdefined in QuantumBlockEncoding/OptimalControl.lean

complete

def QuantumBlockEncoding.OptimalControl.exampleVerified :
  QuantumBlockEncoding.VerifiedOperatorBlockEncoding ℚ 3

def QuantumBlockEncoding.OptimalControl.exampleVerified :
  QuantumBlockEncoding.VerifiedOperatorBlockEncoding
    ℚ 3

Theorem8.3.133

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “example candidate 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. Completed transfer-operator and optimal-control certificates used as end-to-end case studies.

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

Lean code for Theorem8.3.133●1 theorem

theoremdefined in QuantumBlockEncoding/OptimalControl.lean

complete

theorem QuantumBlockEncoding.OptimalControl.exampleCandidate_cost :
  QuantumBlockEncoding.OptimalControl.exampleCandidate.cost =
    { auxiliaryQubits := 1, gateCount := 1, depth := 1,
      oracleCalls := 1 }

theorem QuantumBlockEncoding.OptimalControl.exampleCandidate_cost :
  QuantumBlockEncoding.OptimalControl.exampleCandidate.cost =
    { auxiliaryQubits := 1,
      gateCount := 1, depth := 1,
      oracleCalls := 1 }