8.2. QuantumBlockEncoding/MainCase.lean🔗

127 explicit public declarations, in source order.

Definition8.2.1

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case pro system index”. System-register index for one-bit registers ordered as '(T, tau, S)'.

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-register index for one-bit registers ordered as '(T, tau, S)'.

Declaration kind. def.

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

Lean code for Definition8.2.1●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseProSystemIndex (T tau S : Fin 2) : Fin 8

def QuantumBlockEncoding.mainCaseProSystemIndex
  (T tau S : Fin 2) : Fin 8

System-register index for one-bit registers ordered as `(T, tau, S)`.

Definition8.2.2

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case pro target”. The target matrix 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. The target matrix for 'E_1'. It maps '|1>_T |1>_tau |s>_S' to '|0>_T |0>_tau |s>_S' and annihilates every other computational-basis column.

Declaration kind. def.

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

Lean code for Definition8.2.2●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseProTarget :
  QuantumBlockEncoding.Matrix 8 8 ℚ

def QuantumBlockEncoding.mainCaseProTarget :
  QuantumBlockEncoding.Matrix 8 8 ℚ

The target matrix for `E_1`.

It maps `|1>_T |1>_tau |s>_S` to `|0>_T |0>_tau |s>_S`
and annihilates every other computational-basis column.

Definition8.2.3

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case pro query target”. Operator-first target metadata for the Pro-isolated main-case benchmark.

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. Operator-first target metadata for the Pro-isolated main-case benchmark.

Declaration kind. def.

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

Lean code for Definition8.2.3●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseProQueryTarget :
  QuantumBlockEncoding.QueryOperatorTarget ℚ 8 8

def QuantumBlockEncoding.mainCaseProQueryTarget :
  QuantumBlockEncoding.QueryOperatorTarget
    ℚ 8 8

Operator-first target metadata for the Pro-isolated main-case benchmark.

Definition8.2.4

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case pro signal index”. The clean block-selection index for the single signal ancilla.

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-selection index for the single signal ancilla.

Declaration kind. def.

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

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseProSignalIndex : Fin 2

def QuantumBlockEncoding.mainCaseProSignalIndex :
  Fin 2

The clean block-selection index for the single signal ancilla.

Definition8.2.5

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case pro clean embed”. Clean embedding into the signal-system product basis.

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 embedding into the signal-system product basis.

Declaration kind. def.

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

Lean code for Definition8.2.5●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseProCleanEmbed (i : Fin 8) : Fin 16

def QuantumBlockEncoding.mainCaseProCleanEmbed
  (i : Fin 8) : Fin 16

Clean embedding into the signal-system product basis.

Definition8.2.6

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case pro block projection”. Exact clean-block predicate for a one-signal-qubit candidate matrix.

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. Exact clean-block predicate for a one-signal-qubit candidate matrix. The block projection is the '(signalIndex, signalIndex)' block of 'U', and it must equal 'mainCaseProTarget' pointwise.

Declaration kind. def.

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

Lean code for Definition8.2.6●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseProBlockProjection
  (U : QuantumBlockEncoding.Matrix (2 * 8) (2 * 8) ℚ) : Prop

def QuantumBlockEncoding.mainCaseProBlockProjection
  (U :
    QuantumBlockEncoding.Matrix (2 * 8)
      (2 * 8) ℚ) :
  Prop

Exact clean-block predicate for a one-signal-qubit candidate matrix.

The block projection is the `(signalIndex, signalIndex)` block of `U`, and it
must equal `mainCaseProTarget` pointwise.

Definition8.2.7

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case pro exact normalizer”. Exact normalizer for the requested 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. Exact normalizer for the requested block encoding.

Declaration kind. def.

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

Lean code for Definition8.2.7●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseProExactNormalizer : ℚ

def QuantumBlockEncoding.mainCaseProExactNormalizer :
  ℚ

Exact normalizer for the requested block encoding.

Definition8.2.8

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case pro exact error”. Exact error for the requested 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. Exact error for the requested block encoding.

Declaration kind. def.

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

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseProExactError : ℚ

def QuantumBlockEncoding.mainCaseProExactError :
  ℚ

Exact error for the requested block encoding.

Definition8.2.9

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case pro source layout”. Source-facing layout: three system qubits and one clean signal ancilla.

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. Source-facing layout: three system qubits and one clean signal ancilla.

Declaration kind. def.

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

Lean code for Definition8.2.9●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseProSourceLayout :
  QuantumBlockEncoding.RegisterLayout

def QuantumBlockEncoding.mainCaseProSourceLayout :
  QuantumBlockEncoding.RegisterLayout

Source-facing layout: three system qubits and one clean signal ancilla.

Definition8.2.10

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case pro circuit”. Logical '{X,CNOT,Toffoli}' transcript for the Pro equality-transfer idea.

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,CNOT,Toffoli}' transcript for the Pro equality-transfer idea.

Declaration kind. def.

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

Lean code for Definition8.2.10●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseProCircuit : QuantumBlockEncoding.Circuit

def QuantumBlockEncoding.mainCaseProCircuit :
  QuantumBlockEncoding.Circuit

Logical `{X,CNOT,Toffoli}` transcript for the Pro equality-transfer idea.

Definition8.2.11

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case pro schedule”. Sequential high-level schedule for the current logical transcript.

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. Sequential high-level schedule for the current logical transcript.

Declaration kind. def.

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

Lean code for Definition8.2.11●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseProSchedule :
  QuantumBlockEncoding.LayeredCircuit

def QuantumBlockEncoding.mainCaseProSchedule :
  QuantumBlockEncoding.LayeredCircuit

Sequential high-level schedule for the current logical transcript.

Definition8.2.12

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case pro high level resource”. High-level logical-library resource record for the Pro equality-transfer transcript.

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. High-level logical-library resource record for the Pro equality-transfer transcript. The current 'Resource' type has no Toffoli field, so controlled logical gates are counted in the 'cnot' bucket at this semantic tier.

Declaration kind. def.

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

Lean code for Definition8.2.12●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseProHighLevelResource :
  QuantumBlockEncoding.Resource

def QuantumBlockEncoding.mainCaseProHighLevelResource :
  QuantumBlockEncoding.Resource

High-level logical-library resource record for the Pro equality-transfer
transcript.  The current `Resource` type has no Toffoli field, so controlled
logical gates are counted in the `cnot` bucket at this semantic tier.

Definition8.2.13

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case pro high level seed cost”. Source-facing high-level score '(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. Source-facing high-level score '(gateCount, depth, auxiliaryQubits, oracleCalls)'.

Declaration kind. def.

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

Lean code for Definition8.2.13●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseProHighLevelSeedCost :
  QuantumBlockEncoding.BlockEncodingCost

def QuantumBlockEncoding.mainCaseProHighLevelSeedCost :
  QuantumBlockEncoding.BlockEncodingCost

Source-facing high-level score `(gateCount, depth, auxiliaryQubits, oracleCalls)`.

Theorem8.2.14

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “main case pro high level seed 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/MainCase.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.2.14●1 theorem

theoremdefined in QuantumBlockEncoding/MainCase.lean

complete

theorem QuantumBlockEncoding.mainCaseProHighLevelSeedCost_gateCount :
  QuantumBlockEncoding.mainCaseProHighLevelSeedCost.gateCount = 4

theorem QuantumBlockEncoding.mainCaseProHighLevelSeedCost_gateCount :
  QuantumBlockEncoding.mainCaseProHighLevelSeedCost.gateCount =
    4

Theorem8.2.15

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “main case pro high level seed cost depth”; 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/MainCase.lean:122. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem8.2.15●1 theorem

theoremdefined in QuantumBlockEncoding/MainCase.lean

complete

theorem QuantumBlockEncoding.mainCaseProHighLevelSeedCost_depth :
  QuantumBlockEncoding.mainCaseProHighLevelSeedCost.depth = 4

theorem QuantumBlockEncoding.mainCaseProHighLevelSeedCost_depth :
  QuantumBlockEncoding.mainCaseProHighLevelSeedCost.depth =
    4

Theorem8.2.16

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “main case pro high level seed cost auxiliary qubits”; 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/MainCase.lean:125. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem8.2.16●1 theorem

theoremdefined in QuantumBlockEncoding/MainCase.lean

complete

theorem QuantumBlockEncoding.mainCaseProHighLevelSeedCost_auxiliaryQubits :
  QuantumBlockEncoding.mainCaseProHighLevelSeedCost.auxiliaryQubits = 1

theorem QuantumBlockEncoding.mainCaseProHighLevelSeedCost_auxiliaryQubits :
  QuantumBlockEncoding.mainCaseProHighLevelSeedCost.auxiliaryQubits =
    1

Theorem8.2.17

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “main case pro high level seed cost oracle calls”; 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/MainCase.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.2.17●1 theorem

theoremdefined in QuantumBlockEncoding/MainCase.lean

complete

theorem QuantumBlockEncoding.mainCaseProHighLevelSeedCost_oracleCalls :
  QuantumBlockEncoding.mainCaseProHighLevelSeedCost.oracleCalls = 0

theorem QuantumBlockEncoding.mainCaseProHighLevelSeedCost_oracleCalls :
  QuantumBlockEncoding.mainCaseProHighLevelSeedCost.oracleCalls =
    0

Definition8.2.18

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case pro matrix table resource”. Matrix-table metadata for 'mainCaseProCandidate'.

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-table metadata for 'mainCaseProCandidate'. This incumbent is a finite permutation witness, not the advertised Pro four-gate transcript. The single oracle call marks the unresolved executable realization instead of reusing 'mainCaseProCircuit'.

Declaration kind. def.

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

Lean code for Definition8.2.18●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseProMatrixTableResource :
  QuantumBlockEncoding.Resource

def QuantumBlockEncoding.mainCaseProMatrixTableResource :
  QuantumBlockEncoding.Resource

Matrix-table metadata for `mainCaseProCandidate`.

This incumbent is a finite permutation witness, not the advertised Pro
four-gate transcript.  The single oracle call marks the unresolved executable
realization instead of reusing `mainCaseProCircuit`.

Definition8.2.19

uses 0used by 0✓L∃∀N

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

Lean code for Definition8.2.19●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseProMatrixTableCircuit :
  QuantumBlockEncoding.Circuit

def QuantumBlockEncoding.mainCaseProMatrixTableCircuit :
  QuantumBlockEncoding.Circuit

Definition8.2.20

uses 0used by 0✓L∃∀N

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

Lean code for Definition8.2.20●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseProMatrixTableSchedule :
  QuantumBlockEncoding.LayeredCircuit

def QuantumBlockEncoding.mainCaseProMatrixTableSchedule :
  QuantumBlockEncoding.LayeredCircuit

Definition8.2.21

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case pro candidate image”. Candidate 'MAINCASE-PRO-PERM-001' as a finite image table on '(signal,T,tau,S)' basis states.

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. Candidate 'MAINCASE-PRO-PERM-001' as a finite image table on '(signal,T,tau,S)' basis states. The full index convention is 'signal * 8 + mainCaseProSystemIndex T tau S'.

Declaration kind. def.

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

Lean code for Definition8.2.21●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseProCandidateImage : Fin 16 → Fin 16

def QuantumBlockEncoding.mainCaseProCandidateImage :
  Fin 16 → Fin 16

Candidate `MAINCASE-PRO-PERM-001` as a finite image table on
`(signal,T,tau,S)` basis states.

The full index convention is `signal * 8 + mainCaseProSystemIndex T tau S`.

Definition8.2.22

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case pro candidate matrix”. Column-vector permutation matrix for 'MAINCASE-PRO-PERM-001'.

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-vector permutation matrix for 'MAINCASE-PRO-PERM-001'.

Declaration kind. def.

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

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseProCandidateMatrix :
  QuantumBlockEncoding.Matrix (2 * 8) (2 * 8) ℚ

def QuantumBlockEncoding.mainCaseProCandidateMatrix :
  QuantumBlockEncoding.Matrix (2 * 8)
    (2 * 8) ℚ

Column-vector permutation matrix for `MAINCASE-PRO-PERM-001`.

Theorem8.2.23

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “main case pro candidate image clean source state 0”; 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/MainCase.lean:174. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem8.2.23●1 theorem

theoremdefined in QuantumBlockEncoding/MainCase.lean

complete

theorem QuantumBlockEncoding.mainCaseProCandidateImage_clean_source_state0 :
  QuantumBlockEncoding.mainCaseProCandidateImage ⟨6, ⋯⟩ = ⟨0, ⋯⟩

theorem QuantumBlockEncoding.mainCaseProCandidateImage_clean_source_state0 :
  QuantumBlockEncoding.mainCaseProCandidateImage
      ⟨6, ⋯⟩ =
    ⟨0, ⋯⟩

Theorem8.2.24

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “main case pro candidate image clean source state 1”; 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/MainCase.lean:178. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem8.2.24●1 theorem

theoremdefined in QuantumBlockEncoding/MainCase.lean

complete

theorem QuantumBlockEncoding.mainCaseProCandidateImage_clean_source_state1 :
  QuantumBlockEncoding.mainCaseProCandidateImage ⟨7, ⋯⟩ = ⟨1, ⋯⟩

theorem QuantumBlockEncoding.mainCaseProCandidateImage_clean_source_state1 :
  QuantumBlockEncoding.mainCaseProCandidateImage
      ⟨7, ⋯⟩ =
    ⟨1, ⋯⟩

Theorem8.2.25

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “main case pro candidate image injective pointwise”; 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/MainCase.lean:182. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem8.2.25●1 theorem

theoremdefined in QuantumBlockEncoding/MainCase.lean

complete

theorem QuantumBlockEncoding.mainCaseProCandidateImage_injective_pointwise
  (x y : Fin 16) :
  QuantumBlockEncoding.mainCaseProCandidateImage x =
      QuantumBlockEncoding.mainCaseProCandidateImage y →
    x = y

theorem QuantumBlockEncoding.mainCaseProCandidateImage_injective_pointwise
  (x y : Fin 16) :
  QuantumBlockEncoding.mainCaseProCandidateImage
        x =
      QuantumBlockEncoding.mainCaseProCandidateImage
        y →
    x = y

Theorem8.2.26

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “main case pro candidate image injective”; the hypotheses and conclusion in the code panel fix its exact scope.

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

Why it is in this chapter. 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/MainCase.lean:187. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem8.2.26●1 theorem

theoremdefined in QuantumBlockEncoding/MainCase.lean

complete

theorem QuantumBlockEncoding.mainCaseProCandidateImage_injective :
  Function.Injective QuantumBlockEncoding.mainCaseProCandidateImage

theorem QuantumBlockEncoding.mainCaseProCandidateImage_injective :
  Function.Injective
    QuantumBlockEncoding.mainCaseProCandidateImage

Definition8.2.27

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case pro candidate preimage”. Explicit inverse image table for the task-local permutation certificate.

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

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

Technical source note. Explicit inverse image table for the task-local permutation certificate.

Declaration kind. def.

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

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseProCandidatePreimage : Fin 16 → Fin 16

def QuantumBlockEncoding.mainCaseProCandidatePreimage :
  Fin 16 → Fin 16

Explicit inverse image table for the task-local permutation certificate.

Theorem8.2.28

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “main case pro candidate image preimage”; 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/MainCase.lean:212. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem8.2.28●1 theorem

theoremdefined in QuantumBlockEncoding/MainCase.lean

complete

theorem QuantumBlockEncoding.mainCaseProCandidateImage_preimage (y : Fin 16) :
  QuantumBlockEncoding.mainCaseProCandidateImage
      (QuantumBlockEncoding.mainCaseProCandidatePreimage y) =
    y

theorem QuantumBlockEncoding.mainCaseProCandidateImage_preimage
  (y : Fin 16) :
  QuantumBlockEncoding.mainCaseProCandidateImage
      (QuantumBlockEncoding.mainCaseProCandidatePreimage
        y) =
    y

Theorem8.2.29

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “main case pro candidate image surjective”; 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/MainCase.lean:217. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem8.2.29●1 theorem

theoremdefined in QuantumBlockEncoding/MainCase.lean

complete

theorem QuantumBlockEncoding.mainCaseProCandidateImage_surjective :
  Function.Surjective QuantumBlockEncoding.mainCaseProCandidateImage

theorem QuantumBlockEncoding.mainCaseProCandidateImage_surjective :
  Function.Surjective
    QuantumBlockEncoding.mainCaseProCandidateImage

Definition8.2.30

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case pro candidate image is permutation”. Task-local finite-permutation certificate for the candidate image.

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. Task-local finite-permutation certificate for the candidate image.

Declaration kind. def.

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

Lean code for Definition8.2.30●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseProCandidateImageIsPermutation : Prop

def QuantumBlockEncoding.mainCaseProCandidateImageIsPermutation :
  Prop

Task-local finite-permutation certificate for the candidate image.

Theorem8.2.31

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “main case pro candidate image permutation certificate”; 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/MainCase.lean:228. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem8.2.31●1 theorem

theoremdefined in QuantumBlockEncoding/MainCase.lean

complete

theorem QuantumBlockEncoding.mainCaseProCandidateImage_permutation_certificate :
  QuantumBlockEncoding.mainCaseProCandidateImageIsPermutation

theorem QuantumBlockEncoding.mainCaseProCandidateImage_permutation_certificate :
  QuantumBlockEncoding.mainCaseProCandidateImageIsPermutation

Theorem8.2.32

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “main case pro candidate matrix is rational orthogonal”; 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/MainCase.lean:232. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem8.2.32●1 theorem

theoremdefined in QuantumBlockEncoding/MainCase.lean

complete

theorem QuantumBlockEncoding.mainCaseProCandidateMatrix_isRationalOrthogonal :
  QuantumBlockEncoding.BlockEncodingClassics.IsRationalOrthogonal
    QuantumBlockEncoding.mainCaseProCandidateMatrix

theorem QuantumBlockEncoding.mainCaseProCandidateMatrix_isRationalOrthogonal :
  QuantumBlockEncoding.BlockEncodingClassics.IsRationalOrthogonal
    QuantumBlockEncoding.mainCaseProCandidateMatrix

Definition8.2.33

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case pro reduced of full”. Reduced active index for the Pro transcript bits '(tau,T,signal)'.

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 index for the Pro transcript bits '(tau,T,signal)'.

Declaration kind. def.

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

Lean code for Definition8.2.33●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseProReducedOfFull (x : Fin 16) : Fin 8

def QuantumBlockEncoding.mainCaseProReducedOfFull
  (x : Fin 16) : Fin 8

Reduced active index for the Pro transcript bits `(tau,T,signal)`.

Definition8.2.34

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case pro state of full”. Passive state bit in the full '(signal,T,tau,S)' convention.

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. Passive state bit in the full '(signal,T,tau,S)' convention.

Declaration kind. def.

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

Lean code for Definition8.2.34●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseProStateOfFull (x : Fin 16) : Fin 2

def QuantumBlockEncoding.mainCaseProStateOfFull
  (x : Fin 16) : Fin 2

Passive state bit in the full `(signal,T,tau,S)` convention.

Definition8.2.35

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case pro lift reduced image”. Lift a reduced active-register image while preserving 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. Lift a reduced active-register image while preserving the passive state bit.

Declaration kind. def.

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

defdefined in QuantumBlockEncoding/MainCase.lean

complete

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

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

Lift a reduced active-register image while preserving the passive state bit.

Definition8.2.36

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case pro red ccx 012”. Reduced Toffoli 'CCX012', with controls 'tau,T' and target 'signal'.

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 Toffoli 'CCX012', with controls 'tau,T' and target 'signal'.

Declaration kind. def.

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

Lean code for Definition8.2.36●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseProRedCCX012 (x : Fin 8) : Fin 8

def QuantumBlockEncoding.mainCaseProRedCCX012
  (x : Fin 8) : Fin 8

Reduced Toffoli `CCX012`, with controls `tau,T` and target `signal`.

Definition8.2.37

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case pro red cx 21”. Reduced 'CX21', with control 'signal' and target 'T'.

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 'CX21', with control 'signal' and target 'T'.

Declaration kind. def.

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

Lean code for Definition8.2.37●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseProRedCX21 (x : Fin 8) : Fin 8

def QuantumBlockEncoding.mainCaseProRedCX21
  (x : Fin 8) : Fin 8

Reduced `CX21`, with control `signal` and target `T`.

Definition8.2.38

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case pro red cx 20”. Reduced 'CX20', with control 'signal' and target 'tau'.

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 'CX20', with control 'signal' and target 'tau'.

Declaration kind. def.

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

Lean code for Definition8.2.38●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseProRedCX20 (x : Fin 8) : Fin 8

def QuantumBlockEncoding.mainCaseProRedCX20
  (x : Fin 8) : Fin 8

Reduced `CX20`, with control `signal` and target `tau`.

Definition8.2.39

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case pro red x 2”. Reduced final 'X2', flipping the signal 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. Reduced final 'X2', flipping the signal bit.

Declaration kind. def.

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

Lean code for Definition8.2.39●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseProRedX2 (x : Fin 8) : Fin 8

def QuantumBlockEncoding.mainCaseProRedX2
  (x : Fin 8) : Fin 8

Reduced final `X2`, flipping the signal bit.

Definition8.2.40

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case pro circuit reduced image”. Task-local reduced image for the transcript 'CCX012; CX21; CX20; X2'.

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. Task-local reduced image for the transcript 'CCX012; CX21; CX20; X2'.

Declaration kind. def.

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

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseProCircuitReducedImage (x : Fin 8) : Fin 8

def QuantumBlockEncoding.mainCaseProCircuitReducedImage
  (x : Fin 8) : Fin 8

Task-local reduced image for the transcript `CCX012; CX21; CX20; X2`.

Definition8.2.41

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case pro circuit image”. Task-local full image induced by the advertised Pro four-gate transcript under the full wire map 'S=0', 'tau=1', 'T=2', 'signal=3'.

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. Task-local full image induced by the advertised Pro four-gate transcript under the full wire map 'S=0', 'tau=1', 'T=2', 'signal=3'.

Declaration kind. def.

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

Lean code for Definition8.2.41●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseProCircuitImage : Fin 16 → Fin 16

def QuantumBlockEncoding.mainCaseProCircuitImage :
  Fin 16 → Fin 16

Task-local full image induced by the advertised Pro four-gate transcript under
the full wire map `S=0`, `tau=1`, `T=2`, `signal=3`.

Theorem8.2.42

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “main case pro circuit image clean source state 0”; 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/MainCase.lean:303. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem8.2.42●1 theorem

theoremdefined in QuantumBlockEncoding/MainCase.lean

complete

theorem QuantumBlockEncoding.mainCaseProCircuitImage_clean_source_state0 :
  QuantumBlockEncoding.mainCaseProCircuitImage ⟨6, ⋯⟩ = ⟨0, ⋯⟩

theorem QuantumBlockEncoding.mainCaseProCircuitImage_clean_source_state0 :
  QuantumBlockEncoding.mainCaseProCircuitImage
      ⟨6, ⋯⟩ =
    ⟨0, ⋯⟩

Theorem8.2.43

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “main case pro circuit image clean source state 1”; 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/MainCase.lean:307. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem8.2.43●1 theorem

theoremdefined in QuantumBlockEncoding/MainCase.lean

complete

theorem QuantumBlockEncoding.mainCaseProCircuitImage_clean_source_state1 :
  QuantumBlockEncoding.mainCaseProCircuitImage ⟨7, ⋯⟩ = ⟨1, ⋯⟩

theorem QuantumBlockEncoding.mainCaseProCircuitImage_clean_source_state1 :
  QuantumBlockEncoding.mainCaseProCircuitImage
      ⟨7, ⋯⟩ =
    ⟨1, ⋯⟩

Theorem8.2.44

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “main case pro circuit image candidate mismatch set”; the hypotheses and conclusion in the code panel fix its exact scope. The advertised transcript and the finite-permutation incumbent differ exactly on dirty columns '8', '9', '12', and '13'.

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 advertised transcript and the finite-permutation incumbent differ exactly on dirty columns '8', '9', '12', and '13'.

Declaration kind. theorem.

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

Lean code for Theorem8.2.44●1 theorem

theoremdefined in QuantumBlockEncoding/MainCase.lean

complete

theorem QuantumBlockEncoding.mainCaseProCircuitImage_candidate_mismatch_set
  (x : Fin 16) :
  QuantumBlockEncoding.mainCaseProCircuitImage x ≠
      QuantumBlockEncoding.mainCaseProCandidateImage x ↔
    ↑x ∈ [8, 9, 12, 13]

theorem QuantumBlockEncoding.mainCaseProCircuitImage_candidate_mismatch_set
  (x : Fin 16) :
  QuantumBlockEncoding.mainCaseProCircuitImage
        x ≠
      QuantumBlockEncoding.mainCaseProCandidateImage
        x ↔
    ↑x ∈ [8, 9, 12, 13]

The advertised transcript and the finite-permutation incumbent differ exactly
on dirty columns `8`, `9`, `12`, and `13`.

Theorem8.2.45

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “main case pro circuit image not pointwise candidate”; 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/MainCase.lean:321. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem8.2.45●1 theorem

theoremdefined in QuantumBlockEncoding/MainCase.lean

complete

theorem QuantumBlockEncoding.mainCaseProCircuitImage_not_pointwise_candidate :
  ¬∀ (x : Fin 16),
      QuantumBlockEncoding.mainCaseProCircuitImage x =
        QuantumBlockEncoding.mainCaseProCandidateImage x

theorem QuantumBlockEncoding.mainCaseProCircuitImage_not_pointwise_candidate :
  ¬∀ (x : Fin 16),
      QuantumBlockEncoding.mainCaseProCircuitImage
          x =
        QuantumBlockEncoding.mainCaseProCandidateImage
          x

Definition8.2.46

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case pro circuit matrix”. Column-vector permutation matrix induced by the advertised Pro transcript.

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-vector permutation matrix induced by the advertised Pro transcript.

Declaration kind. def.

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

Lean code for Definition8.2.46●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseProCircuitMatrix :
  QuantumBlockEncoding.Matrix (2 * 8) (2 * 8) ℚ

def QuantumBlockEncoding.mainCaseProCircuitMatrix :
  QuantumBlockEncoding.Matrix (2 * 8)
    (2 * 8) ℚ

Column-vector permutation matrix induced by the advertised Pro transcript.

Theorem8.2.47

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “main case pro circuit image injective pointwise”; 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/MainCase.lean:334. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem8.2.47●1 theorem

theoremdefined in QuantumBlockEncoding/MainCase.lean

complete

theorem QuantumBlockEncoding.mainCaseProCircuitImage_injective_pointwise
  (x y : Fin 16) :
  QuantumBlockEncoding.mainCaseProCircuitImage x =
      QuantumBlockEncoding.mainCaseProCircuitImage y →
    x = y

theorem QuantumBlockEncoding.mainCaseProCircuitImage_injective_pointwise
  (x y : Fin 16) :
  QuantumBlockEncoding.mainCaseProCircuitImage
        x =
      QuantumBlockEncoding.mainCaseProCircuitImage
        y →
    x = y

Theorem8.2.48

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “main case pro circuit image injective”; the hypotheses and conclusion in the code panel fix its exact scope.

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

Why it is in this chapter. 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/MainCase.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.2.48●1 theorem

theoremdefined in QuantumBlockEncoding/MainCase.lean

complete

theorem QuantumBlockEncoding.mainCaseProCircuitImage_injective :
  Function.Injective QuantumBlockEncoding.mainCaseProCircuitImage

theorem QuantumBlockEncoding.mainCaseProCircuitImage_injective :
  Function.Injective
    QuantumBlockEncoding.mainCaseProCircuitImage

Theorem8.2.49

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “main case pro circuit image surjective pointwise”; 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/MainCase.lean:344. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem8.2.49●1 theorem

theoremdefined in QuantumBlockEncoding/MainCase.lean

complete

theorem QuantumBlockEncoding.mainCaseProCircuitImage_surjective_pointwise
  (y : Fin 16) : ∃ x, QuantumBlockEncoding.mainCaseProCircuitImage x = y

theorem QuantumBlockEncoding.mainCaseProCircuitImage_surjective_pointwise
  (y : Fin 16) :
  ∃ x,
    QuantumBlockEncoding.mainCaseProCircuitImage
        x =
      y

Theorem8.2.50

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “main case pro circuit image surjective”; 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/MainCase.lean:348. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem8.2.50●1 theorem

theoremdefined in QuantumBlockEncoding/MainCase.lean

complete

theorem QuantumBlockEncoding.mainCaseProCircuitImage_surjective :
  Function.Surjective QuantumBlockEncoding.mainCaseProCircuitImage

theorem QuantumBlockEncoding.mainCaseProCircuitImage_surjective :
  Function.Surjective
    QuantumBlockEncoding.mainCaseProCircuitImage

Definition8.2.51

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case pro circuit image is permutation”. Task-local finite-permutation certificate for the Pro transcript image.

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. Task-local finite-permutation certificate for the Pro transcript image.

Declaration kind. def.

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

Lean code for Definition8.2.51●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseProCircuitImageIsPermutation : Prop

def QuantumBlockEncoding.mainCaseProCircuitImageIsPermutation :
  Prop

Task-local finite-permutation certificate for the Pro transcript image.

Theorem8.2.52

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “main case pro circuit image permutation certificate”; 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/MainCase.lean:357. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem8.2.52●1 theorem

theoremdefined in QuantumBlockEncoding/MainCase.lean

complete

theorem QuantumBlockEncoding.mainCaseProCircuitImage_permutation_certificate :
  QuantumBlockEncoding.mainCaseProCircuitImageIsPermutation

theorem QuantumBlockEncoding.mainCaseProCircuitImage_permutation_certificate :
  QuantumBlockEncoding.mainCaseProCircuitImageIsPermutation

Theorem8.2.53

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “main case pro circuit matrix is rational orthogonal”; 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/MainCase.lean:361. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem8.2.53●1 theorem

theoremdefined in QuantumBlockEncoding/MainCase.lean

complete

theorem QuantumBlockEncoding.mainCaseProCircuitMatrix_isRationalOrthogonal :
  QuantumBlockEncoding.BlockEncodingClassics.IsRationalOrthogonal
    QuantumBlockEncoding.mainCaseProCircuitMatrix

theorem QuantumBlockEncoding.mainCaseProCircuitMatrix_isRationalOrthogonal :
  QuantumBlockEncoding.BlockEncodingClassics.IsRationalOrthogonal
    QuantumBlockEncoding.mainCaseProCircuitMatrix

Theorem8.2.54

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “main case pro circuit clean entry”; the hypotheses and conclusion in the code panel fix its exact scope. Clean-entry calculation for the gate-derived Pro transcript 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. Clean-entry calculation for the gate-derived Pro transcript image.

Declaration kind. theorem.

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

Lean code for Theorem8.2.54●1 theorem

theoremdefined in QuantumBlockEncoding/MainCase.lean

complete

theorem QuantumBlockEncoding.mainCaseProCircuit_cleanEntry (row col : Fin 8) :
  (if
        QuantumBlockEncoding.mainCaseProCleanEmbed row =
          QuantumBlockEncoding.mainCaseProCircuitImage
            (QuantumBlockEncoding.mainCaseProCleanEmbed col) then
      1
    else 0) =
    QuantumBlockEncoding.mainCaseProTarget row col

theorem QuantumBlockEncoding.mainCaseProCircuit_cleanEntry
  (row col : Fin 8) :
  (if
        QuantumBlockEncoding.mainCaseProCleanEmbed
            row =
          QuantumBlockEncoding.mainCaseProCircuitImage
            (QuantumBlockEncoding.mainCaseProCleanEmbed
              col) then
      1
    else 0) =
    QuantumBlockEncoding.mainCaseProTarget
      row col

Clean-entry calculation for the gate-derived Pro transcript image.

Theorem8.2.55

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “main case pro circuit block projection”; 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/MainCase.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.2.55●1 theorem

theoremdefined in QuantumBlockEncoding/MainCase.lean

complete

theorem QuantumBlockEncoding.mainCaseProCircuit_blockProjection :
  QuantumBlockEncoding.mainCaseProBlockProjection
    QuantumBlockEncoding.mainCaseProCircuitMatrix

theorem QuantumBlockEncoding.mainCaseProCircuit_blockProjection :
  QuantumBlockEncoding.mainCaseProBlockProjection
    QuantumBlockEncoding.mainCaseProCircuitMatrix

Theorem8.2.56

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “main case pro target support state 0”; 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/MainCase.lean:392. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem8.2.56●1 theorem

theoremdefined in QuantumBlockEncoding/MainCase.lean

complete

theorem QuantumBlockEncoding.mainCaseProTarget_support_state0 :
  QuantumBlockEncoding.mainCaseProTarget
      (QuantumBlockEncoding.mainCaseProSystemIndex 0 0 0)
      (QuantumBlockEncoding.mainCaseProSystemIndex 1 1 0) =
    1

theorem QuantumBlockEncoding.mainCaseProTarget_support_state0 :
  QuantumBlockEncoding.mainCaseProTarget
      (QuantumBlockEncoding.mainCaseProSystemIndex
        0 0 0)
      (QuantumBlockEncoding.mainCaseProSystemIndex
        1 1 0) =
    1

Theorem8.2.57

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “main case pro target support state 1”; 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/MainCase.lean:398. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem8.2.57●1 theorem

theoremdefined in QuantumBlockEncoding/MainCase.lean

complete

theorem QuantumBlockEncoding.mainCaseProTarget_support_state1 :
  QuantumBlockEncoding.mainCaseProTarget
      (QuantumBlockEncoding.mainCaseProSystemIndex 0 0 1)
      (QuantumBlockEncoding.mainCaseProSystemIndex 1 1 1) =
    1

theorem QuantumBlockEncoding.mainCaseProTarget_support_state1 :
  QuantumBlockEncoding.mainCaseProTarget
      (QuantumBlockEncoding.mainCaseProSystemIndex
        0 0 1)
      (QuantumBlockEncoding.mainCaseProSystemIndex
        1 1 1) =
    1

Theorem8.2.58

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “main case pro candidate clean entry”; the hypotheses and conclusion in the code panel fix its exact scope. Entrywise image calculation for the reusable partial-permutation wrapper.

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. Entrywise image calculation for the reusable partial-permutation wrapper.

Declaration kind. theorem.

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

Lean code for Theorem8.2.58●1 theorem

theoremdefined in QuantumBlockEncoding/MainCase.lean

complete

theorem QuantumBlockEncoding.mainCaseProCandidate_cleanEntry (row col : Fin 8) :
  (if
        QuantumBlockEncoding.mainCaseProCleanEmbed row =
          QuantumBlockEncoding.mainCaseProCandidateImage
            (QuantumBlockEncoding.mainCaseProCleanEmbed col) then
      1
    else 0) =
    QuantumBlockEncoding.mainCaseProTarget row col

theorem QuantumBlockEncoding.mainCaseProCandidate_cleanEntry
  (row col : Fin 8) :
  (if
        QuantumBlockEncoding.mainCaseProCleanEmbed
            row =
          QuantumBlockEncoding.mainCaseProCandidateImage
            (QuantumBlockEncoding.mainCaseProCleanEmbed
              col) then
      1
    else 0) =
    QuantumBlockEncoding.mainCaseProTarget
      row col

Entrywise image calculation for the reusable partial-permutation wrapper.

Definition8.2.59

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case pro exact clean block certificate”. Exact clean-block package from the compiled partial-permutation leaf.

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. Exact clean-block package from the compiled partial-permutation leaf.

Declaration kind. def.

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

Lean code for Definition8.2.59●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseProExactCleanBlockCertificate :
  QuantumBlockEncoding.BlockEncodingClassics.ExactCleanBlock 8 16

def QuantumBlockEncoding.mainCaseProExactCleanBlockCertificate :
  QuantumBlockEncoding.BlockEncodingClassics.ExactCleanBlock
    8 16

Exact clean-block package from the compiled partial-permutation leaf.

Theorem8.2.60

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “main case pro exact clean block correct”; 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/MainCase.lean:427. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem8.2.60●1 theorem

theoremdefined in QuantumBlockEncoding/MainCase.lean

complete

theorem QuantumBlockEncoding.mainCaseProExactCleanBlock_correct :
  QuantumBlockEncoding.mainCaseProExactCleanBlockCertificate.clean.PointwiseEq
    QuantumBlockEncoding.mainCaseProTarget

theorem QuantumBlockEncoding.mainCaseProExactCleanBlock_correct :
  QuantumBlockEncoding.mainCaseProExactCleanBlockCertificate.clean.PointwiseEq
    QuantumBlockEncoding.mainCaseProTarget

Theorem8.2.61

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “main case pro candidate block projection”; 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/MainCase.lean:435. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem8.2.61●1 theorem

theoremdefined in QuantumBlockEncoding/MainCase.lean

complete

theorem QuantumBlockEncoding.mainCaseProCandidate_blockProjection :
  QuantumBlockEncoding.mainCaseProBlockProjection
    QuantumBlockEncoding.mainCaseProCandidateMatrix

theorem QuantumBlockEncoding.mainCaseProCandidate_blockProjection :
  QuantumBlockEncoding.mainCaseProBlockProjection
    QuantumBlockEncoding.mainCaseProCandidateMatrix

Theorem8.2.62

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “main case pro query target normalizer”; 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/MainCase.lean:444. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem8.2.62●1 theorem

theoremdefined in QuantumBlockEncoding/MainCase.lean

complete

theorem QuantumBlockEncoding.mainCaseProQueryTarget_normalizer :
  QuantumBlockEncoding.mainCaseProQueryTarget.normalizer =
    QuantumBlockEncoding.mainCaseProExactNormalizer

theorem QuantumBlockEncoding.mainCaseProQueryTarget_normalizer :
  QuantumBlockEncoding.mainCaseProQueryTarget.normalizer =
    QuantumBlockEncoding.mainCaseProExactNormalizer

Theorem8.2.63

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “main case pro source layout auxiliary qubits”; 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/MainCase.lean:447. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem8.2.63●1 theorem

theoremdefined in QuantumBlockEncoding/MainCase.lean

complete

theorem QuantumBlockEncoding.mainCaseProSourceLayout_auxiliaryQubits :
  QuantumBlockEncoding.mainCaseProSourceLayout.auxiliaryQubits = 1

theorem QuantumBlockEncoding.mainCaseProSourceLayout_auxiliaryQubits :
  QuantumBlockEncoding.mainCaseProSourceLayout.auxiliaryQubits =
    1

Definition8.2.64

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case pro rational orthogonal bridge obligation”. Reusable proof obligation for a later shared bridge from finite bijections to the project-local rational-orthogonality matrix predicate.

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. Reusable proof obligation for a later shared bridge from finite bijections to the project-local rational-orthogonality matrix predicate.

Declaration kind. def.

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

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseProRationalOrthogonalBridgeObligation :
  QuantumBlockEncoding.SemanticObligation

def QuantumBlockEncoding.mainCaseProRationalOrthogonalBridgeObligation :
  QuantumBlockEncoding.SemanticObligation

Reusable proof obligation for a later shared bridge from finite bijections to
the project-local rational-orthogonality matrix predicate.

Definition8.2.65

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case pro candidate”. Candidate record at the finite-permutation semantic tier.

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. Candidate record at the finite-permutation semantic tier.

Declaration kind. def.

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

Lean code for Definition8.2.65●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseProCandidate :
  QuantumBlockEncoding.OperatorBlockEncodingCandidate ℚ 3

def QuantumBlockEncoding.mainCaseProCandidate :
  QuantumBlockEncoding.OperatorBlockEncodingCandidate
    ℚ 3

Candidate record at the finite-permutation semantic tier.

Definition8.2.66

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case pro circuit candidate”. Gate-derived candidate for the advertised Pro four-gate transcript.

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-derived candidate for the advertised Pro four-gate transcript.

Declaration kind. def.

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

Lean code for Definition8.2.66●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseProCircuitCandidate :
  QuantumBlockEncoding.OperatorBlockEncodingCandidate ℚ 3

def QuantumBlockEncoding.mainCaseProCircuitCandidate :
  QuantumBlockEncoding.OperatorBlockEncodingCandidate
    ℚ 3

Gate-derived candidate for the advertised Pro four-gate transcript.

Definition8.2.67

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case pro verified”. Verified task-local candidate at the finite-permutation semantic tier.

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 task-local candidate at the finite-permutation semantic tier. This certificate proves the block entry and the image bijection. The stronger matrix-orthogonality bridge is closed by 'mainCaseProRationalOrthogonalBridgeObligation'.

Declaration kind. def.

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

Lean code for Definition8.2.67●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseProVerified :
  QuantumBlockEncoding.VerifiedOperatorBlockEncoding ℚ 3

def QuantumBlockEncoding.mainCaseProVerified :
  QuantumBlockEncoding.VerifiedOperatorBlockEncoding
    ℚ 3

Verified task-local candidate at the finite-permutation semantic tier.

This certificate proves the block entry and the image bijection.  The stronger
matrix-orthogonality bridge is closed by
`mainCaseProRationalOrthogonalBridgeObligation`.

Definition8.2.68

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case pro circuit verified”. Verified task-local candidate for the advertised Pro transcript image.

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 task-local candidate for the advertised Pro transcript image.

Declaration kind. def.

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

Lean code for Definition8.2.68●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseProCircuitVerified :
  QuantumBlockEncoding.VerifiedOperatorBlockEncoding ℚ 3

def QuantumBlockEncoding.mainCaseProCircuitVerified :
  QuantumBlockEncoding.VerifiedOperatorBlockEncoding
    ℚ 3

Verified task-local candidate for the advertised Pro transcript image.

Theorem8.2.69

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “main case pro 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/MainCase.lean:512. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem8.2.69●1 theorem

theoremdefined in QuantumBlockEncoding/MainCase.lean

complete

theorem QuantumBlockEncoding.mainCaseProCandidate_cost :
  QuantumBlockEncoding.mainCaseProCandidate.cost =
    { auxiliaryQubits := 1, gateCount := 1, depth := 1,
      oracleCalls := 1 }

theorem QuantumBlockEncoding.mainCaseProCandidate_cost :
  QuantumBlockEncoding.mainCaseProCandidate.cost =
    { auxiliaryQubits := 1,
      gateCount := 1, depth := 1,
      oracleCalls := 1 }

Theorem8.2.70

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “main case pro candidate uses matrix table metadata”; 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/MainCase.lean:517. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem8.2.70●1 theorem

theoremdefined in QuantumBlockEncoding/MainCase.lean

complete

theorem QuantumBlockEncoding.mainCaseProCandidate_uses_matrix_table_metadata :
  QuantumBlockEncoding.mainCaseProCandidate.circuit =
      QuantumBlockEncoding.mainCaseProMatrixTableCircuit ∧
    QuantumBlockEncoding.mainCaseProCandidate.schedule =
        QuantumBlockEncoding.mainCaseProMatrixTableSchedule ∧
      QuantumBlockEncoding.mainCaseProCandidate.resource =
        QuantumBlockEncoding.mainCaseProMatrixTableResource

theorem QuantumBlockEncoding.mainCaseProCandidate_uses_matrix_table_metadata :
  QuantumBlockEncoding.mainCaseProCandidate.circuit =
      QuantumBlockEncoding.mainCaseProMatrixTableCircuit ∧
    QuantumBlockEncoding.mainCaseProCandidate.schedule =
        QuantumBlockEncoding.mainCaseProMatrixTableSchedule ∧
      QuantumBlockEncoding.mainCaseProCandidate.resource =
        QuantumBlockEncoding.mainCaseProMatrixTableResource

Theorem8.2.71

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “main case pro circuit 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/MainCase.lean:523. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem8.2.71●1 theorem

theoremdefined in QuantumBlockEncoding/MainCase.lean

complete

theorem QuantumBlockEncoding.mainCaseProCircuitCandidate_cost :
  QuantumBlockEncoding.mainCaseProCircuitCandidate.cost =
    { auxiliaryQubits := 1, gateCount := 4, depth := 4,
      oracleCalls := 0 }

theorem QuantumBlockEncoding.mainCaseProCircuitCandidate_cost :
  QuantumBlockEncoding.mainCaseProCircuitCandidate.cost =
    { auxiliaryQubits := 1,
      gateCount := 4, depth := 4,
      oracleCalls := 0 }

Definition8.2.72

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case cold system index”. System-register index for one-bit registers ordered as '(T, tau, S)'.

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-register index for one-bit registers ordered as '(T, tau, S)'.

Declaration kind. def.

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

Lean code for Definition8.2.72●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseColdSystemIndex (T tau S : Fin 2) : Fin 8

def QuantumBlockEncoding.mainCaseColdSystemIndex
  (T tau S : Fin 2) : Fin 8

System-register index for one-bit registers ordered as `(T, tau, S)`.

Definition8.2.73

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case cold target”. The COLD target matrix 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. The COLD target matrix for 'E_1'. It maps '|1>_T |1>_tau |s>_S' to '|0>_T |0>_tau |s>_S' and annihilates every other computational-basis column.

Declaration kind. def.

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

Lean code for Definition8.2.73●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseColdTarget :
  QuantumBlockEncoding.Matrix 8 8 ℚ

def QuantumBlockEncoding.mainCaseColdTarget :
  QuantumBlockEncoding.Matrix 8 8 ℚ

The COLD target matrix for `E_1`.

It maps `|1>_T |1>_tau |s>_S` to `|0>_T |0>_tau |s>_S`
and annihilates every other computational-basis column.

Definition8.2.74

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case cold exact normalizer”. Exact normalizer for the no-Pro COLD 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. Exact normalizer for the no-Pro COLD target.

Declaration kind. def.

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

Lean code for Definition8.2.74●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseColdExactNormalizer : ℚ

def QuantumBlockEncoding.mainCaseColdExactNormalizer :
  ℚ

Exact normalizer for the no-Pro COLD target.

Definition8.2.75

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case cold exact error”. Exact error for the no-Pro COLD 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. Exact error for the no-Pro COLD target.

Declaration kind. def.

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

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseColdExactError : ℚ

def QuantumBlockEncoding.mainCaseColdExactError :
  ℚ

Exact error for the no-Pro COLD target.

Definition8.2.76

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case cold query target”. Operator-first target metadata for the no-Pro COLD benchmark.

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. Operator-first target metadata for the no-Pro COLD benchmark.

Declaration kind. def.

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

Lean code for Definition8.2.76●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseColdQueryTarget :
  QuantumBlockEncoding.QueryOperatorTarget ℚ 8 8

def QuantumBlockEncoding.mainCaseColdQueryTarget :
  QuantumBlockEncoding.QueryOperatorTarget
    ℚ 8 8

Operator-first target metadata for the no-Pro COLD benchmark.

Definition8.2.77

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case cold clean signal”. The clean block-selection index for the single signal ancilla.

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-selection index for the single signal ancilla.

Declaration kind. def.

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

Lean code for Definition8.2.77●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseColdCleanSignal : Fin 2

def QuantumBlockEncoding.mainCaseColdCleanSignal :
  Fin 2

The clean block-selection index for the single signal ancilla.

Definition8.2.78

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case cold clean embed”. Clean embedding into the signal-system product basis.

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 embedding into the signal-system product basis.

Declaration kind. def.

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

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseColdCleanEmbed (i : Fin 8) : Fin 16

def QuantumBlockEncoding.mainCaseColdCleanEmbed
  (i : Fin 8) : Fin 16

Clean embedding into the signal-system product basis.

Definition8.2.79

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case cold block projection”. Exact clean-block predicate for a one-signal-qubit COLD candidate matrix.

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. Exact clean-block predicate for a one-signal-qubit COLD candidate matrix. The block projection is the '(signal,signal) = (0,0)' block of 'U', and it must equal 'mainCaseColdTarget' pointwise.

Declaration kind. def.

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

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseColdBlockProjection
  (U : QuantumBlockEncoding.Matrix (2 * 8) (2 * 8) ℚ) : Prop

def QuantumBlockEncoding.mainCaseColdBlockProjection
  (U :
    QuantumBlockEncoding.Matrix (2 * 8)
      (2 * 8) ℚ) :
  Prop

Exact clean-block predicate for a one-signal-qubit COLD candidate matrix.

The block projection is the `(signal,signal) = (0,0)` block of `U`, and it
must equal `mainCaseColdTarget` pointwise.

Definition8.2.80

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case cold source layout”. Source-facing layout: three system qubits and one clean signal ancilla.

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. Source-facing layout: three system qubits and one clean signal ancilla.

Declaration kind. def.

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

Lean code for Definition8.2.80●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseColdSourceLayout :
  QuantumBlockEncoding.RegisterLayout

def QuantumBlockEncoding.mainCaseColdSourceLayout :
  QuantumBlockEncoding.RegisterLayout

Source-facing layout: three system qubits and one clean signal ancilla.

Definition8.2.81

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case cold partial perm image”. Candidate 'MAIN-PARTIAL-PERM-001' as a COLD task-local finite image table on the '(signal,T,tau,S)' basis.

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. Candidate 'MAIN-PARTIAL-PERM-001' as a COLD task-local finite image table on the '(signal,T,tau,S)' basis. The full index convention is 'signal * 8 + mainCaseColdSystemIndex T tau S'.

Declaration kind. def.

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

Lean code for Definition8.2.81●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseColdPartialPermImage : Fin 16 → Fin 16

def QuantumBlockEncoding.mainCaseColdPartialPermImage :
  Fin 16 → Fin 16

Candidate `MAIN-PARTIAL-PERM-001` as a COLD task-local finite image table on
the `(signal,T,tau,S)` basis.

The full index convention is `signal * 8 + mainCaseColdSystemIndex T tau S`.

Definition8.2.82

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case cold partial perm matrix”. Column-vector permutation matrix for 'MAIN-PARTIAL-PERM-001'.

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-vector permutation matrix for 'MAIN-PARTIAL-PERM-001'.

Declaration kind. def.

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

Lean code for Definition8.2.82●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseColdPartialPermMatrix :
  QuantumBlockEncoding.Matrix (2 * 8) (2 * 8) ℚ

def QuantumBlockEncoding.mainCaseColdPartialPermMatrix :
  QuantumBlockEncoding.Matrix (2 * 8)
    (2 * 8) ℚ

Column-vector permutation matrix for `MAIN-PARTIAL-PERM-001`.

Definition8.2.83

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case cold reduced of full”. Reduced active index for the COLD table bits '(tau,T,signal)'.

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 index for the COLD table bits '(tau,T,signal)'.

Declaration kind. def.

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

Lean code for Definition8.2.83●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseColdReducedOfFull (x : Fin 16) : Fin 8

def QuantumBlockEncoding.mainCaseColdReducedOfFull
  (x : Fin 16) : Fin 8

Reduced active index for the COLD table bits `(tau,T,signal)`.

Definition8.2.84

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case cold state of full”. Passive state bit in the full '(signal,T,tau,S)' convention.

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. Passive state bit in the full '(signal,T,tau,S)' convention.

Declaration kind. def.

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

Lean code for Definition8.2.84●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseColdStateOfFull (x : Fin 16) : Fin 2

def QuantumBlockEncoding.mainCaseColdStateOfFull
  (x : Fin 16) : Fin 2

Passive state bit in the full `(signal,T,tau,S)` convention.

Definition8.2.85

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case cold lift reduced image”. Lift a reduced active-register image while preserving 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. Lift a reduced active-register image while preserving the passive state bit.

Declaration kind. def.

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

defdefined in QuantumBlockEncoding/MainCase.lean

complete

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

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

Lift a reduced active-register image while preserving the passive state bit.

Definition8.2.86

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case cold red xt”. Reduced 'X' on the 'T' 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. Reduced 'X' on the 'T' bit.

Declaration kind. def.

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

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseColdRedXT (x : Fin 8) : Fin 8

def QuantumBlockEncoding.mainCaseColdRedXT
  (x : Fin 8) : Fin 8

Reduced `X` on the `T` bit.

Definition8.2.87

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case cold red ccx tau t signal”. Reduced Toffoli with controls 'tau,T' and target 'signal'.

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 Toffoli with controls 'tau,T' and target 'signal'.

Declaration kind. def.

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

Lean code for Definition8.2.87●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseColdRedCCXTauTSignal (x : Fin 8) : Fin 8

def QuantumBlockEncoding.mainCaseColdRedCCXTauTSignal
  (x : Fin 8) : Fin 8

Reduced Toffoli with controls `tau,T` and target `signal`.

Definition8.2.88

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case cold red x tau”. Reduced 'X' on the 'tau' 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. Reduced 'X' on the 'tau' bit.

Declaration kind. def.

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

Lean code for Definition8.2.88●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseColdRedXTau (x : Fin 8) : Fin 8

def QuantumBlockEncoding.mainCaseColdRedXTau
  (x : Fin 8) : Fin 8

Reduced `X` on the `tau` bit.

Definition8.2.89

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case cold red cx signal t”. Reduced CNOT with control 'signal' and target 'T'.

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 CNOT with control 'signal' and target 'T'.

Declaration kind. def.

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

Lean code for Definition8.2.89●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseColdRedCXSignalT (x : Fin 8) : Fin 8

def QuantumBlockEncoding.mainCaseColdRedCXSignalT
  (x : Fin 8) : Fin 8

Reduced CNOT with control `signal` and target `T`.

Definition8.2.90

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case cold red cx tau signal”. Reduced CNOT with control 'tau' and target 'signal'.

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 CNOT with control 'tau' and target 'signal'.

Declaration kind. def.

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

Lean code for Definition8.2.90●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseColdRedCXTauSignal (x : Fin 8) : Fin 8

def QuantumBlockEncoding.mainCaseColdRedCXTauSignal
  (x : Fin 8) : Fin 8

Reduced CNOT with control `tau` and target `signal`.

Definition8.2.91

uses 0used by 0✓L∃∀N

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

Lean code for Definition8.2.91●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

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

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

Evaluate reduced logical reversible gates as basis-state permutations.

Definition8.2.92

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case cold partial perm reduced image”. Reduced COLD table induced by 'mainCaseColdPartialPermImage'.

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 COLD table induced by 'mainCaseColdPartialPermImage'.

Declaration kind. def.

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

Lean code for Definition8.2.92●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseColdPartialPermReducedImage (x : Fin 8) :
  Fin 8

def QuantumBlockEncoding.mainCaseColdPartialPermReducedImage
  (x : Fin 8) : Fin 8

Reduced COLD table induced by `mainCaseColdPartialPermImage`.

Definition8.2.93

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case cold reduced gate images”. Reduced gate-image transcript for the COLD resource schema.

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 gate-image transcript for the COLD resource schema.

Declaration kind. def.

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

Lean code for Definition8.2.93●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseColdReducedGateImages :
  List (Fin 8 → Fin 8)

def QuantumBlockEncoding.mainCaseColdReducedGateImages :
  List (Fin 8 → Fin 8)

Reduced gate-image transcript for the COLD resource schema.

Definition8.2.94

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case cold circuit reduced image”. Reduced active-register image induced by the COLD resource schema.

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 COLD resource schema.

Declaration kind. def.

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

Lean code for Definition8.2.94●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseColdCircuitReducedImage (x : Fin 8) : Fin 8

def QuantumBlockEncoding.mainCaseColdCircuitReducedImage
  (x : Fin 8) : Fin 8

Reduced active-register image induced by the COLD resource schema.

Theorem8.2.95

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “main case cold reduced gate images eval”; the hypotheses and conclusion in the code panel fix its exact scope. The COLD logical reversible circuit implements the reduced table.

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 COLD logical reversible circuit implements the reduced table.

Declaration kind. theorem.

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

Lean code for Theorem8.2.95●1 theorem

theoremdefined in QuantumBlockEncoding/MainCase.lean

complete

theorem QuantumBlockEncoding.mainCaseColdReducedGateImages_eval (x : Fin 8) :
  QuantumBlockEncoding.mainCaseColdCircuitReducedImage x =
    QuantumBlockEncoding.mainCaseColdPartialPermReducedImage x

theorem QuantumBlockEncoding.mainCaseColdReducedGateImages_eval
  (x : Fin 8) :
  QuantumBlockEncoding.mainCaseColdCircuitReducedImage
      x =
    QuantumBlockEncoding.mainCaseColdPartialPermReducedImage
      x

The COLD logical reversible circuit implements the reduced table.

Definition8.2.96

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case cold circuit image”. Full active-plus-passive image induced by the COLD resource schema.

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 active-plus-passive image induced by the COLD resource schema.

Declaration kind. def.

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

Lean code for Definition8.2.96●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseColdCircuitImage : Fin 16 → Fin 16

def QuantumBlockEncoding.mainCaseColdCircuitImage :
  Fin 16 → Fin 16

Full active-plus-passive image induced by the COLD resource schema.

Theorem8.2.97

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “main case cold circuit image eq partial perm image”; the hypotheses and conclusion in the code panel fix its exact scope. The COLD logical reversible circuit implements the finite table.

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 COLD logical reversible circuit implements the finite table.

Declaration kind. theorem.

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

Lean code for Theorem8.2.97●1 theorem

theoremdefined in QuantumBlockEncoding/MainCase.lean

complete

theorem QuantumBlockEncoding.mainCaseColdCircuitImage_eq_partialPermImage
  (x : Fin 16) :
  QuantumBlockEncoding.mainCaseColdCircuitImage x =
    QuantumBlockEncoding.mainCaseColdPartialPermImage x

theorem QuantumBlockEncoding.mainCaseColdCircuitImage_eq_partialPermImage
  (x : Fin 16) :
  QuantumBlockEncoding.mainCaseColdCircuitImage
      x =
    QuantumBlockEncoding.mainCaseColdPartialPermImage
      x

The COLD logical reversible circuit implements the finite table.

Definition8.2.98

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case cold gate xt”. Logical 'X' on the time register 'T' in the full wire 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 register 'T' in the full wire layout.

Declaration kind. def.

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

Lean code for Definition8.2.98●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseColdGateXT : QuantumBlockEncoding.Gate

def QuantumBlockEncoding.mainCaseColdGateXT :
  QuantumBlockEncoding.Gate

Logical `X` on the time register `T` in the full wire layout.

Definition8.2.99

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case cold gate ccx tau t signal”. Logical Toffoli with controls 'tau,T' and target 'signal'.

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 'tau,T' and target 'signal'.

Declaration kind. def.

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

Lean code for Definition8.2.99●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseColdGateCCXTauTSignal :
  QuantumBlockEncoding.Gate

def QuantumBlockEncoding.mainCaseColdGateCCXTauTSignal :
  QuantumBlockEncoding.Gate

Logical Toffoli with controls `tau,T` and target `signal`.

Definition8.2.100

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case cold gate x tau”. Logical 'X' on the type register 'tau' in the full wire 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 register 'tau' in the full wire layout.

Declaration kind. def.

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

Lean code for Definition8.2.100●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseColdGateXTau : QuantumBlockEncoding.Gate

def QuantumBlockEncoding.mainCaseColdGateXTau :
  QuantumBlockEncoding.Gate

Logical `X` on the type register `tau` in the full wire layout.

Definition8.2.101

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case cold gate cx signal t”. Logical CNOT with control 'signal' and target 'T'.

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 'signal' and target 'T'.

Declaration kind. def.

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

Lean code for Definition8.2.101●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseColdGateCXSignalT :
  QuantumBlockEncoding.Gate

def QuantumBlockEncoding.mainCaseColdGateCXSignalT :
  QuantumBlockEncoding.Gate

Logical CNOT with control `signal` and target `T`.

Definition8.2.102

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case cold gate cx tau signal”. Logical CNOT with control 'tau' and target 'signal'.

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 'tau' and target 'signal'.

Declaration kind. def.

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

Lean code for Definition8.2.102●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseColdGateCXTauSignal :
  QuantumBlockEncoding.Gate

def QuantumBlockEncoding.mainCaseColdGateCXTauSignal :
  QuantumBlockEncoding.Gate

Logical CNOT with control `tau` and target `signal`.

Definition8.2.103

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case cold circuit”. COLD task-local logical circuit for the finite partial-permutation table.

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. COLD task-local logical circuit for the finite partial-permutation table.

Declaration kind. def.

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

Lean code for Definition8.2.103●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseColdCircuit : QuantumBlockEncoding.Circuit

def QuantumBlockEncoding.mainCaseColdCircuit :
  QuantumBlockEncoding.Circuit

COLD task-local logical circuit for the finite partial-permutation table.

Definition8.2.104

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case cold schedule”. Sequential COLD schedule for the current logical transcript.

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. Sequential COLD schedule for the current logical transcript.

Declaration kind. def.

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

Lean code for Definition8.2.104●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseColdSchedule :
  QuantumBlockEncoding.LayeredCircuit

def QuantumBlockEncoding.mainCaseColdSchedule :
  QuantumBlockEncoding.LayeredCircuit

Sequential COLD schedule for the current logical transcript.

Definition8.2.105

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case cold high level resource”. High-level logical-library resource record for the COLD transcript.

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. High-level logical-library resource record for the COLD transcript. At this semantic tier, Toffoli and CNOT are counted together as controlled logical gates, matching the main-case resource convention.

Declaration kind. def.

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

Lean code for Definition8.2.105●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseColdHighLevelResource :
  QuantumBlockEncoding.Resource

def QuantumBlockEncoding.mainCaseColdHighLevelResource :
  QuantumBlockEncoding.Resource

High-level logical-library resource record for the COLD transcript.  At this
semantic tier, Toffoli and CNOT are counted together as controlled logical
gates, matching the main-case resource convention.

Definition8.2.106

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case cold partial perm cost”. Source-facing COLD score '(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. Source-facing COLD score '(gateCount, depth, auxiliaryQubits, oracleCalls)'.

Declaration kind. def.

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

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseColdPartialPermCost :
  QuantumBlockEncoding.BlockEncodingCost

def QuantumBlockEncoding.mainCaseColdPartialPermCost :
  QuantumBlockEncoding.BlockEncodingCost

Source-facing COLD score `(gateCount, depth, auxiliaryQubits, oracleCalls)`.

Theorem8.2.107

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “main case cold partial perm 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/MainCase.lean:796. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem8.2.107●1 theorem

theoremdefined in QuantumBlockEncoding/MainCase.lean

complete

theorem QuantumBlockEncoding.mainCaseColdPartialPermCost_gateCount :
  QuantumBlockEncoding.mainCaseColdPartialPermCost.gateCount = 5

theorem QuantumBlockEncoding.mainCaseColdPartialPermCost_gateCount :
  QuantumBlockEncoding.mainCaseColdPartialPermCost.gateCount =
    5

Theorem8.2.108

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “main case cold partial perm cost depth”; 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/MainCase.lean:799. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem8.2.108●1 theorem

theoremdefined in QuantumBlockEncoding/MainCase.lean

complete

theorem QuantumBlockEncoding.mainCaseColdPartialPermCost_depth :
  QuantumBlockEncoding.mainCaseColdPartialPermCost.depth = 5

theorem QuantumBlockEncoding.mainCaseColdPartialPermCost_depth :
  QuantumBlockEncoding.mainCaseColdPartialPermCost.depth =
    5

Theorem8.2.109

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “main case cold partial perm cost auxiliary qubits”; 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/MainCase.lean:802. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem8.2.109●1 theorem

theoremdefined in QuantumBlockEncoding/MainCase.lean

complete

theorem QuantumBlockEncoding.mainCaseColdPartialPermCost_auxiliaryQubits :
  QuantumBlockEncoding.mainCaseColdPartialPermCost.auxiliaryQubits = 1

theorem QuantumBlockEncoding.mainCaseColdPartialPermCost_auxiliaryQubits :
  QuantumBlockEncoding.mainCaseColdPartialPermCost.auxiliaryQubits =
    1

Theorem8.2.110

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “main case cold partial perm cost oracle calls”; 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/MainCase.lean:805. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem8.2.110●1 theorem

theoremdefined in QuantumBlockEncoding/MainCase.lean

complete

theorem QuantumBlockEncoding.mainCaseColdPartialPermCost_oracleCalls :
  QuantumBlockEncoding.mainCaseColdPartialPermCost.oracleCalls = 0

theorem QuantumBlockEncoding.mainCaseColdPartialPermCost_oracleCalls :
  QuantumBlockEncoding.mainCaseColdPartialPermCost.oracleCalls =
    0

Theorem8.2.111

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “main case cold partial perm image injective pointwise”; 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/MainCase.lean:808. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem8.2.111●1 theorem

theoremdefined in QuantumBlockEncoding/MainCase.lean

complete

theorem QuantumBlockEncoding.mainCaseColdPartialPermImage_injective_pointwise
  (x y : Fin 16) :
  QuantumBlockEncoding.mainCaseColdPartialPermImage x =
      QuantumBlockEncoding.mainCaseColdPartialPermImage y →
    x = y

theorem QuantumBlockEncoding.mainCaseColdPartialPermImage_injective_pointwise
  (x y : Fin 16) :
  QuantumBlockEncoding.mainCaseColdPartialPermImage
        x =
      QuantumBlockEncoding.mainCaseColdPartialPermImage
        y →
    x = y

Theorem8.2.112

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “main case cold partial perm image injective”; the hypotheses and conclusion in the code panel fix its exact scope.

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

Why it is in this chapter. 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/MainCase.lean:813. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem8.2.112●1 theorem

theoremdefined in QuantumBlockEncoding/MainCase.lean

complete

theorem QuantumBlockEncoding.mainCaseColdPartialPermImage_injective :
  Function.Injective QuantumBlockEncoding.mainCaseColdPartialPermImage

theorem QuantumBlockEncoding.mainCaseColdPartialPermImage_injective :
  Function.Injective
    QuantumBlockEncoding.mainCaseColdPartialPermImage

Definition8.2.113

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case cold partial perm preimage”. Explicit inverse image table for the COLD partial-permutation certificate.

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

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

Technical source note. Explicit inverse image table for the COLD partial-permutation certificate.

Declaration kind. def.

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

Lean code for Definition8.2.113●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseColdPartialPermPreimage : Fin 16 → Fin 16

def QuantumBlockEncoding.mainCaseColdPartialPermPreimage :
  Fin 16 → Fin 16

Explicit inverse image table for the COLD partial-permutation certificate.

Theorem8.2.114

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “main case cold partial perm image preimage”; 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/MainCase.lean:838. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem8.2.114●1 theorem

theoremdefined in QuantumBlockEncoding/MainCase.lean

complete

theorem QuantumBlockEncoding.mainCaseColdPartialPermImage_preimage
  (y : Fin 16) :
  QuantumBlockEncoding.mainCaseColdPartialPermImage
      (QuantumBlockEncoding.mainCaseColdPartialPermPreimage y) =
    y

theorem QuantumBlockEncoding.mainCaseColdPartialPermImage_preimage
  (y : Fin 16) :
  QuantumBlockEncoding.mainCaseColdPartialPermImage
      (QuantumBlockEncoding.mainCaseColdPartialPermPreimage
        y) =
    y

Theorem8.2.115

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “main case cold partial perm image surjective”; 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/MainCase.lean:843. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem8.2.115●1 theorem

theoremdefined in QuantumBlockEncoding/MainCase.lean

complete

theorem QuantumBlockEncoding.mainCaseColdPartialPermImage_surjective :
  Function.Surjective QuantumBlockEncoding.mainCaseColdPartialPermImage

theorem QuantumBlockEncoding.mainCaseColdPartialPermImage_surjective :
  Function.Surjective
    QuantumBlockEncoding.mainCaseColdPartialPermImage

Definition8.2.116

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case cold partial perm image is permutation”. Task-local finite-permutation certificate for 'MAIN-PARTIAL-PERM-001'.

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. Task-local finite-permutation certificate for 'MAIN-PARTIAL-PERM-001'.

Declaration kind. def.

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

Lean code for Definition8.2.116●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseColdPartialPermImageIsPermutation : Prop

def QuantumBlockEncoding.mainCaseColdPartialPermImageIsPermutation :
  Prop

Task-local finite-permutation certificate for `MAIN-PARTIAL-PERM-001`.

Theorem8.2.117

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “main case cold partial perm image bijective”; 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/MainCase.lean:854. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem8.2.117●1 theorem

theoremdefined in QuantumBlockEncoding/MainCase.lean

complete

theorem QuantumBlockEncoding.mainCaseColdPartialPermImage_bijective :
  QuantumBlockEncoding.mainCaseColdPartialPermImageIsPermutation

theorem QuantumBlockEncoding.mainCaseColdPartialPermImage_bijective :
  QuantumBlockEncoding.mainCaseColdPartialPermImageIsPermutation

Theorem8.2.118

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “main case cold partial perm entry”; the hypotheses and conclusion in the code panel fix its exact scope. Entrywise image calculation for the reusable partial-permutation wrapper.

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. Entrywise image calculation for the reusable partial-permutation wrapper.

Declaration kind. theorem.

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

Lean code for Theorem8.2.118●1 theorem

theoremdefined in QuantumBlockEncoding/MainCase.lean

complete

theorem QuantumBlockEncoding.mainCaseColdPartialPerm_entry (row col : Fin 8) :
  (if
        QuantumBlockEncoding.mainCaseColdCleanEmbed row =
          QuantumBlockEncoding.mainCaseColdPartialPermImage
            (QuantumBlockEncoding.mainCaseColdCleanEmbed col) then
      1
    else 0) =
    QuantumBlockEncoding.mainCaseColdTarget row col

theorem QuantumBlockEncoding.mainCaseColdPartialPerm_entry
  (row col : Fin 8) :
  (if
        QuantumBlockEncoding.mainCaseColdCleanEmbed
            row =
          QuantumBlockEncoding.mainCaseColdPartialPermImage
            (QuantumBlockEncoding.mainCaseColdCleanEmbed
              col) then
      1
    else 0) =
    QuantumBlockEncoding.mainCaseColdTarget
      row col

Entrywise image calculation for the reusable partial-permutation wrapper.

Definition8.2.119

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case cold partial perm exact clean block”. Exact clean-block package from the compiled partial-permutation leaf.

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. Exact clean-block package from the compiled partial-permutation leaf.

Declaration kind. def.

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

Lean code for Definition8.2.119●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseColdPartialPermExactCleanBlock :
  QuantumBlockEncoding.BlockEncodingClassics.ExactCleanBlock 8 16

def QuantumBlockEncoding.mainCaseColdPartialPermExactCleanBlock :
  QuantumBlockEncoding.BlockEncodingClassics.ExactCleanBlock
    8 16

Exact clean-block package from the compiled partial-permutation leaf.

Theorem8.2.120

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “main case cold partial perm clean eq target”; 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/MainCase.lean:883. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem8.2.120●1 theorem

theoremdefined in QuantumBlockEncoding/MainCase.lean

complete

theorem QuantumBlockEncoding.mainCaseColdPartialPerm_clean_eq_target :
  QuantumBlockEncoding.mainCaseColdPartialPermExactCleanBlock.clean.PointwiseEq
    QuantumBlockEncoding.mainCaseColdTarget

theorem QuantumBlockEncoding.mainCaseColdPartialPerm_clean_eq_target :
  QuantumBlockEncoding.mainCaseColdPartialPermExactCleanBlock.clean.PointwiseEq
    QuantumBlockEncoding.mainCaseColdTarget

Theorem8.2.121

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “main case cold partial perm block projection”; 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/MainCase.lean:891. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem8.2.121●1 theorem

theoremdefined in QuantumBlockEncoding/MainCase.lean

complete

theorem QuantumBlockEncoding.mainCaseColdPartialPerm_blockProjection :
  QuantumBlockEncoding.mainCaseColdBlockProjection
    QuantumBlockEncoding.mainCaseColdPartialPermMatrix

theorem QuantumBlockEncoding.mainCaseColdPartialPerm_blockProjection :
  QuantumBlockEncoding.mainCaseColdBlockProjection
    QuantumBlockEncoding.mainCaseColdPartialPermMatrix

Theorem8.2.122

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “main case cold query target normalizer”; 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/MainCase.lean:900. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem8.2.122●1 theorem

theoremdefined in QuantumBlockEncoding/MainCase.lean

complete

theorem QuantumBlockEncoding.mainCaseColdQueryTarget_normalizer :
  QuantumBlockEncoding.mainCaseColdQueryTarget.normalizer =
    QuantumBlockEncoding.mainCaseColdExactNormalizer

theorem QuantumBlockEncoding.mainCaseColdQueryTarget_normalizer :
  QuantumBlockEncoding.mainCaseColdQueryTarget.normalizer =
    QuantumBlockEncoding.mainCaseColdExactNormalizer

Theorem8.2.123

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “main case cold source layout auxiliary qubits”; 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/MainCase.lean:903. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem8.2.123●1 theorem

theoremdefined in QuantumBlockEncoding/MainCase.lean

complete

theorem QuantumBlockEncoding.mainCaseColdSourceLayout_auxiliaryQubits :
  QuantumBlockEncoding.mainCaseColdSourceLayout.auxiliaryQubits = 1

theorem QuantumBlockEncoding.mainCaseColdSourceLayout_auxiliaryQubits :
  QuantumBlockEncoding.mainCaseColdSourceLayout.auxiliaryQubits =
    1

Definition8.2.124

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case cold resource schema obligation”. Resource-schema obligation for 'MAIN-RESOURCE-001'.

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-schema obligation for 'MAIN-RESOURCE-001'. The COLD-local circuit image and resource field theorems below justify the advertised high-level logical resource tuple for the candidate package.

Declaration kind. def.

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

Lean code for Definition8.2.124●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseColdResourceSchemaObligation :
  QuantumBlockEncoding.SemanticObligation

def QuantumBlockEncoding.mainCaseColdResourceSchemaObligation :
  QuantumBlockEncoding.SemanticObligation

Resource-schema obligation for `MAIN-RESOURCE-001`.

The COLD-local circuit image and resource field theorems below justify the
advertised high-level logical resource tuple for the candidate package.

Definition8.2.125

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case cold partial perm candidate”. COLD task-local candidate package at the finite-permutation semantic tier.

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. COLD task-local candidate package at the finite-permutation semantic tier. The target, candidate matrix, block projection, and logical resource tuple are all COLD-local declarations; this package does not use the separate 'mainCasePro*' arm as evidence.

Declaration kind. def.

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

Lean code for Definition8.2.125●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseColdPartialPermCandidate :
  QuantumBlockEncoding.OperatorBlockEncodingCandidate ℚ 3

def QuantumBlockEncoding.mainCaseColdPartialPermCandidate :
  QuantumBlockEncoding.OperatorBlockEncodingCandidate
    ℚ 3

COLD task-local candidate package at the finite-permutation semantic tier.

The target, candidate matrix, block projection, and logical resource tuple are
all COLD-local declarations; this package does not use the separate `mainCasePro*`
arm as evidence.

Definition8.2.126

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “main case cold partial perm verified”. Verified COLD block-encoding package for the transfer operator at the current finite-permutation semantic tier.

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 COLD block-encoding package for the transfer operator at the current finite-permutation semantic tier.

Declaration kind. def.

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

Lean code for Definition8.2.126●1 definition

defdefined in QuantumBlockEncoding/MainCase.lean

complete

def QuantumBlockEncoding.mainCaseColdPartialPermVerified :
  QuantumBlockEncoding.VerifiedOperatorBlockEncoding ℚ 3

def QuantumBlockEncoding.mainCaseColdPartialPermVerified :
  QuantumBlockEncoding.VerifiedOperatorBlockEncoding
    ℚ 3

Verified COLD block-encoding package for the transfer operator at the current
finite-permutation semantic tier.

Theorem8.2.127

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “main case cold partial perm 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/MainCase.lean:952. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem8.2.127●1 theorem

theoremdefined in QuantumBlockEncoding/MainCase.lean

complete

theorem QuantumBlockEncoding.mainCaseColdPartialPermCandidate_cost :
  QuantumBlockEncoding.mainCaseColdPartialPermCandidate.cost =
    { auxiliaryQubits := 1, gateCount := 5, depth := 5,
      oracleCalls := 0 }

theorem QuantumBlockEncoding.mainCaseColdPartialPermCandidate_cost :
  QuantumBlockEncoding.mainCaseColdPartialPermCandidate.cost =
    { auxiliaryQubits := 1,
      gateCount := 5, depth := 5,
      oracleCalls := 0 }