8.1. QuantumBlockEncoding/ColdStartTransferE1.lean🔗

28 explicit public declarations, in source order.

Definition8.1.1

uses 0used by 0✓L∃∀N

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

Lean code for Definition8.1.1●1 definition

defdefined in QuantumBlockEncoding/ColdStartTransferE1.lean

complete

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

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

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

Definition8.1.2

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “cold e 1 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 has support exactly on the two entries mapping '|1>_T |1>_tau |s>_S' to '|0>_T |0>_tau |s>_S'.

Declaration kind. def.

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

Lean code for Definition8.1.2●1 definition

defdefined in QuantumBlockEncoding/ColdStartTransferE1.lean

complete

def QuantumBlockEncoding.coldE1Target : QuantumBlockEncoding.Matrix 8 8 ℚ

def QuantumBlockEncoding.coldE1Target :
  QuantumBlockEncoding.Matrix 8 8 ℚ

The target matrix for `E_1`.

It has support exactly on the two entries mapping
`|1>_T |1>_tau |s>_S` to `|0>_T |0>_tau |s>_S`.

Definition8.1.3

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “cold e 1 query target”. Operator-first target metadata for the strict cold-start 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 strict cold-start benchmark.

Declaration kind. def.

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

Lean code for Definition8.1.3●1 definition

defdefined in QuantumBlockEncoding/ColdStartTransferE1.lean

complete

def QuantumBlockEncoding.coldE1QueryTarget :
  QuantumBlockEncoding.QueryOperatorTarget ℚ 8 8

def QuantumBlockEncoding.coldE1QueryTarget :
  QuantumBlockEncoding.QueryOperatorTarget
    ℚ 8 8

Operator-first target metadata for the strict cold-start benchmark.

Definition8.1.4

uses 0used by 0✓L∃∀N

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

Lean code for Definition8.1.4●1 definition

defdefined in QuantumBlockEncoding/ColdStartTransferE1.lean

complete

def QuantumBlockEncoding.coldE1SignalIndex : Fin 2

def QuantumBlockEncoding.coldE1SignalIndex :
  Fin 2

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

Definition8.1.5

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “cold e 1 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 'coldE1Target' pointwise.

Declaration kind. def.

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

defdefined in QuantumBlockEncoding/ColdStartTransferE1.lean

complete

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

def QuantumBlockEncoding.coldE1BlockProjection
  (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 `coldE1Target` pointwise.

Definition8.1.6

uses 0used by 0✓L∃∀N

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

Lean code for Definition8.1.6●1 definition

defdefined in QuantumBlockEncoding/ColdStartTransferE1.lean

complete

def QuantumBlockEncoding.coldE1ExactNormalizer : ℚ

def QuantumBlockEncoding.coldE1ExactNormalizer :
  ℚ

Exact normalizer for the requested block encoding.

Definition8.1.7

uses 0used by 0✓L∃∀N

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

Lean code for Definition8.1.7●1 definition

defdefined in QuantumBlockEncoding/ColdStartTransferE1.lean

complete

def QuantumBlockEncoding.coldE1ExactError : ℚ

def QuantumBlockEncoding.coldE1ExactError : ℚ

Exact error for the requested block encoding.

Definition8.1.8

uses 0used by 0✓L∃∀N

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

Lean code for Definition8.1.8●1 definition

defdefined in QuantumBlockEncoding/ColdStartTransferE1.lean

complete

def QuantumBlockEncoding.coldE1SourceLayout :
  QuantumBlockEncoding.RegisterLayout

def QuantumBlockEncoding.coldE1SourceLayout :
  QuantumBlockEncoding.RegisterLayout

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

Definition8.1.9

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “cold e 1 high level seed cost”. Source-facing seed cost under the high-level reversible-gate convention in the conversion window.

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 seed cost under the high-level reversible-gate convention in the conversion window. This is not a certified 'Circuit.resource' expansion.

Declaration kind. def.

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

defdefined in QuantumBlockEncoding/ColdStartTransferE1.lean

complete

def QuantumBlockEncoding.coldE1HighLevelSeedCost :
  QuantumBlockEncoding.BlockEncodingCost

def QuantumBlockEncoding.coldE1HighLevelSeedCost :
  QuantumBlockEncoding.BlockEncodingCost

Source-facing seed cost under the high-level reversible-gate convention in the
conversion window.  This is not a certified `Circuit.resource` expansion.

Theorem8.1.10

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “cold e 1 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/ColdStartTransferE1.lean:91. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem8.1.10●1 theorem

theoremdefined in QuantumBlockEncoding/ColdStartTransferE1.lean

complete

theorem QuantumBlockEncoding.coldE1HighLevelSeedCost_gateCount :
  QuantumBlockEncoding.coldE1HighLevelSeedCost.gateCount = 4

theorem QuantumBlockEncoding.coldE1HighLevelSeedCost_gateCount :
  QuantumBlockEncoding.coldE1HighLevelSeedCost.gateCount =
    4

Theorem8.1.11

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “cold e 1 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/ColdStartTransferE1.lean:94. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem8.1.11●1 theorem

theoremdefined in QuantumBlockEncoding/ColdStartTransferE1.lean

complete

theorem QuantumBlockEncoding.coldE1HighLevelSeedCost_depth :
  QuantumBlockEncoding.coldE1HighLevelSeedCost.depth = 4

theorem QuantumBlockEncoding.coldE1HighLevelSeedCost_depth :
  QuantumBlockEncoding.coldE1HighLevelSeedCost.depth =
    4

Theorem8.1.12

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “cold e 1 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/ColdStartTransferE1.lean:97. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem8.1.12●1 theorem

theoremdefined in QuantumBlockEncoding/ColdStartTransferE1.lean

complete

theorem QuantumBlockEncoding.coldE1HighLevelSeedCost_auxiliaryQubits :
  QuantumBlockEncoding.coldE1HighLevelSeedCost.auxiliaryQubits = 1

theorem QuantumBlockEncoding.coldE1HighLevelSeedCost_auxiliaryQubits :
  QuantumBlockEncoding.coldE1HighLevelSeedCost.auxiliaryQubits =
    1

Theorem8.1.13

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “cold e 1 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/ColdStartTransferE1.lean:100. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem8.1.13●1 theorem

theoremdefined in QuantumBlockEncoding/ColdStartTransferE1.lean

complete

theorem QuantumBlockEncoding.coldE1HighLevelSeedCost_oracleCalls :
  QuantumBlockEncoding.coldE1HighLevelSeedCost.oracleCalls = 0

theorem QuantumBlockEncoding.coldE1HighLevelSeedCost_oracleCalls :
  QuantumBlockEncoding.coldE1HighLevelSeedCost.oracleCalls =
    0

Definition8.1.14

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “cold e 1 candidate image”. Candidate 'COLD-CLEAN-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 'COLD-CLEAN-PERM-001' as a finite image table on '(signal,T,tau,S)' basis states. The full index convention is 'signal * 8 + coldE1SystemIndex T tau S'.

Declaration kind. def.

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

Lean code for Definition8.1.14●1 definition

defdefined in QuantumBlockEncoding/ColdStartTransferE1.lean

complete

def QuantumBlockEncoding.coldE1CandidateImage : Fin 16 → Fin 16

def QuantumBlockEncoding.coldE1CandidateImage :
  Fin 16 → Fin 16

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

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

Definition8.1.15

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “cold e 1 candidate matrix”. Column-vector permutation matrix for 'COLD-CLEAN-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 'COLD-CLEAN-PERM-001'.

Declaration kind. def.

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

Lean code for Definition8.1.15●1 definition

defdefined in QuantumBlockEncoding/ColdStartTransferE1.lean

complete

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

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

Column-vector permutation matrix for `COLD-CLEAN-PERM-001`.

Theorem8.1.16

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “cold e 1 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/ColdStartTransferE1.lean:132. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem8.1.16●1 theorem

theoremdefined in QuantumBlockEncoding/ColdStartTransferE1.lean

complete

theorem QuantumBlockEncoding.coldE1CandidateImage_clean_source_state0 :
  QuantumBlockEncoding.coldE1CandidateImage ⟨6, ⋯⟩ = ⟨0, ⋯⟩

theorem QuantumBlockEncoding.coldE1CandidateImage_clean_source_state0 :
  QuantumBlockEncoding.coldE1CandidateImage
      ⟨6, ⋯⟩ =
    ⟨0, ⋯⟩

Theorem8.1.17

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “cold e 1 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/ColdStartTransferE1.lean:136. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem8.1.17●1 theorem

theoremdefined in QuantumBlockEncoding/ColdStartTransferE1.lean

complete

theorem QuantumBlockEncoding.coldE1CandidateImage_clean_source_state1 :
  QuantumBlockEncoding.coldE1CandidateImage ⟨7, ⋯⟩ = ⟨1, ⋯⟩

theorem QuantumBlockEncoding.coldE1CandidateImage_clean_source_state1 :
  QuantumBlockEncoding.coldE1CandidateImage
      ⟨7, ⋯⟩ =
    ⟨1, ⋯⟩

Theorem8.1.18

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “cold e 1 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/ColdStartTransferE1.lean:140. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem8.1.18●1 theorem

theoremdefined in QuantumBlockEncoding/ColdStartTransferE1.lean

complete

theorem QuantumBlockEncoding.coldE1CandidateImage_injective_pointwise
  (x y : Fin 16) :
  QuantumBlockEncoding.coldE1CandidateImage x =
      QuantumBlockEncoding.coldE1CandidateImage y →
    x = y

theorem QuantumBlockEncoding.coldE1CandidateImage_injective_pointwise
  (x y : Fin 16) :
  QuantumBlockEncoding.coldE1CandidateImage
        x =
      QuantumBlockEncoding.coldE1CandidateImage
        y →
    x = y

Theorem8.1.19

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “cold e 1 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/ColdStartTransferE1.lean:144. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem8.1.19●1 theorem

theoremdefined in QuantumBlockEncoding/ColdStartTransferE1.lean

complete

theorem QuantumBlockEncoding.coldE1CandidateImage_injective :
  Function.Injective QuantumBlockEncoding.coldE1CandidateImage

theorem QuantumBlockEncoding.coldE1CandidateImage_injective :
  Function.Injective
    QuantumBlockEncoding.coldE1CandidateImage

Definition8.1.20

uses 0used by 0✓L∃∀N

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

Lean code for Definition8.1.20●1 definition

defdefined in QuantumBlockEncoding/ColdStartTransferE1.lean

complete

def QuantumBlockEncoding.coldE1CandidatePreimage : Fin 16 → Fin 16

def QuantumBlockEncoding.coldE1CandidatePreimage :
  Fin 16 → Fin 16

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

Theorem8.1.21

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “cold e 1 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/ColdStartTransferE1.lean:169. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem8.1.21●1 theorem

theoremdefined in QuantumBlockEncoding/ColdStartTransferE1.lean

complete

theorem QuantumBlockEncoding.coldE1CandidateImage_preimage (y : Fin 16) :
  QuantumBlockEncoding.coldE1CandidateImage
      (QuantumBlockEncoding.coldE1CandidatePreimage y) =
    y

theorem QuantumBlockEncoding.coldE1CandidateImage_preimage
  (y : Fin 16) :
  QuantumBlockEncoding.coldE1CandidateImage
      (QuantumBlockEncoding.coldE1CandidatePreimage
        y) =
    y

Theorem8.1.22

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “cold e 1 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/ColdStartTransferE1.lean:173. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem8.1.22●1 theorem

theoremdefined in QuantumBlockEncoding/ColdStartTransferE1.lean

complete

theorem QuantumBlockEncoding.coldE1CandidateImage_surjective :
  Function.Surjective QuantumBlockEncoding.coldE1CandidateImage

theorem QuantumBlockEncoding.coldE1CandidateImage_surjective :
  Function.Surjective
    QuantumBlockEncoding.coldE1CandidateImage

Theorem8.1.23

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “cold e 1 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/ColdStartTransferE1.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.1.23●1 theorem

theoremdefined in QuantumBlockEncoding/ColdStartTransferE1.lean

complete

theorem QuantumBlockEncoding.coldE1CandidateImage_permutation_certificate :
  Function.Injective QuantumBlockEncoding.coldE1CandidateImage ∧
    Function.Surjective QuantumBlockEncoding.coldE1CandidateImage

theorem QuantumBlockEncoding.coldE1CandidateImage_permutation_certificate :
  Function.Injective
      QuantumBlockEncoding.coldE1CandidateImage ∧
    Function.Surjective
      QuantumBlockEncoding.coldE1CandidateImage

Theorem8.1.24

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “cold e 1 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/ColdStartTransferE1.lean:183. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem8.1.24●1 theorem

theoremdefined in QuantumBlockEncoding/ColdStartTransferE1.lean

complete

theorem QuantumBlockEncoding.coldE1Target_support_state0 :
  QuantumBlockEncoding.coldE1Target
      (QuantumBlockEncoding.coldE1SystemIndex 0 0 0)
      (QuantumBlockEncoding.coldE1SystemIndex 1 1 0) =
    1

theorem QuantumBlockEncoding.coldE1Target_support_state0 :
  QuantumBlockEncoding.coldE1Target
      (QuantumBlockEncoding.coldE1SystemIndex
        0 0 0)
      (QuantumBlockEncoding.coldE1SystemIndex
        1 1 0) =
    1

Theorem8.1.25

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “cold e 1 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/ColdStartTransferE1.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.1.25●1 theorem

theoremdefined in QuantumBlockEncoding/ColdStartTransferE1.lean

complete

theorem QuantumBlockEncoding.coldE1Target_support_state1 :
  QuantumBlockEncoding.coldE1Target
      (QuantumBlockEncoding.coldE1SystemIndex 0 0 1)
      (QuantumBlockEncoding.coldE1SystemIndex 1 1 1) =
    1

theorem QuantumBlockEncoding.coldE1Target_support_state1 :
  QuantumBlockEncoding.coldE1Target
      (QuantumBlockEncoding.coldE1SystemIndex
        0 0 1)
      (QuantumBlockEncoding.coldE1SystemIndex
        1 1 1) =
    1

Theorem8.1.26

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “cold e 1 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/ColdStartTransferE1.lean:191. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem8.1.26●1 theorem

theoremdefined in QuantumBlockEncoding/ColdStartTransferE1.lean

complete

theorem QuantumBlockEncoding.coldE1Candidate_blockProjection :
  QuantumBlockEncoding.coldE1BlockProjection
    QuantumBlockEncoding.coldE1CandidateMatrix

theorem QuantumBlockEncoding.coldE1Candidate_blockProjection :
  QuantumBlockEncoding.coldE1BlockProjection
    QuantumBlockEncoding.coldE1CandidateMatrix

Theorem8.1.27

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “cold e 1 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/ColdStartTransferE1.lean:199. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem8.1.27●1 theorem

theoremdefined in QuantumBlockEncoding/ColdStartTransferE1.lean

complete

theorem QuantumBlockEncoding.coldE1QueryTarget_normalizer :
  QuantumBlockEncoding.coldE1QueryTarget.normalizer =
    QuantumBlockEncoding.coldE1ExactNormalizer

theorem QuantumBlockEncoding.coldE1QueryTarget_normalizer :
  QuantumBlockEncoding.coldE1QueryTarget.normalizer =
    QuantumBlockEncoding.coldE1ExactNormalizer

Theorem8.1.28

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “cold e 1 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/ColdStartTransferE1.lean:202. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem8.1.28●1 theorem

theoremdefined in QuantumBlockEncoding/ColdStartTransferE1.lean

complete

theorem QuantumBlockEncoding.coldE1SourceLayout_auxiliaryQubits :
  QuantumBlockEncoding.coldE1SourceLayout.auxiliaryQubits = 1

theorem QuantumBlockEncoding.coldE1SourceLayout_auxiliaryQubits :
  QuantumBlockEncoding.coldE1SourceLayout.auxiliaryQubits =
    1