6.9. QuantumBlockEncoding/PromiseGateOptimization.lean🔗

17 explicit public declarations, in source order.

Definition6.9.1

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “lift target equiv”. Apply a target permutation without changing its control register.

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

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

Technical source note. Apply a target permutation without changing its control register.

Declaration kind. def.

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

Lean code for Definition6.9.1●1 definition

defdefined in QuantumBlockEncoding/PromiseGateOptimization.lean

complete

def QuantumBlockEncoding.PromiseGateOptimization.liftTargetEquiv.{u_1}
  {α : Type u_1} (target : Equiv.Perm α) : Equiv.Perm (Bool × α)

def QuantumBlockEncoding.PromiseGateOptimization.liftTargetEquiv.{u_1}
  {α : Type u_1} (target : Equiv.Perm α) :
  Equiv.Perm (Bool × α)

Apply a target permutation without changing its control register.

Definition6.9.2

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “controlled target equiv”. Apply the target permutation exactly on the 'true' control branch.

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

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

Technical source note. Apply the target permutation exactly on the 'true' control branch.

Declaration kind. def.

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

Lean code for Definition6.9.2●1 definition

defdefined in QuantumBlockEncoding/PromiseGateOptimization.lean

complete

def QuantumBlockEncoding.PromiseGateOptimization.controlledTargetEquiv.{u_1}
  {α : Type u_1} (target : Equiv.Perm α) : Equiv.Perm (Bool × α)

def QuantumBlockEncoding.PromiseGateOptimization.controlledTargetEquiv.{u_1}
  {α : Type u_1} (target : Equiv.Perm α) :
  Equiv.Perm (Bool × α)

Apply the target permutation exactly on the `true` control branch.

Definition6.9.3

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “conjugated target equiv”. Chronological 'V', then 'U', then 'V†'.

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

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

Technical source note. Chronological 'V', then 'U', then 'V†'.

Declaration kind. def.

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

Lean code for Definition6.9.3●1 definition

defdefined in QuantumBlockEncoding/PromiseGateOptimization.lean

complete

def QuantumBlockEncoding.PromiseGateOptimization.conjugatedTargetEquiv.{u_1}
  {α : Type u_1} (outer middle : Equiv.Perm α) : Equiv.Perm α

def QuantumBlockEncoding.PromiseGateOptimization.conjugatedTargetEquiv.{u_1}
  {α : Type u_1}
  (outer middle : Equiv.Perm α) :
  Equiv.Perm α

Chronological `V`, then `U`, then `V†`.

Theorem6.9.4

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “controlled conjugation equiv”; the hypotheses and conclusion in the code panel fix its exact scope. Figure 3(a): controlling 'V† U V' is equivalent to leaving 'V' and 'V†' uncontrolled and controlling only 'U'.

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

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

Technical source note. Figure 3(a): controlling 'V† U V' is equivalent to leaving 'V' and 'V†' uncontrolled and controlling only 'U'.

Declaration kind. theorem.

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

Lean code for Theorem6.9.4●1 theorem

theoremdefined in QuantumBlockEncoding/PromiseGateOptimization.lean

complete

theorem QuantumBlockEncoding.PromiseGateOptimization.controlledConjugation_equiv.{u_1}
  {α : Type u_1} (outer middle : Equiv.Perm α) :
  (Equiv.trans
          (QuantumBlockEncoding.PromiseGateOptimization.liftTargetEquiv
            outer)
          (QuantumBlockEncoding.PromiseGateOptimization.controlledTargetEquiv
            middle)).trans
      (QuantumBlockEncoding.PromiseGateOptimization.liftTargetEquiv
        (Equiv.symm outer)) =
    QuantumBlockEncoding.PromiseGateOptimization.controlledTargetEquiv
      (QuantumBlockEncoding.PromiseGateOptimization.conjugatedTargetEquiv
        outer middle)

theorem QuantumBlockEncoding.PromiseGateOptimization.controlledConjugation_equiv.{u_1}
  {α : Type u_1}
  (outer middle : Equiv.Perm α) :
  (Equiv.trans
          (QuantumBlockEncoding.PromiseGateOptimization.liftTargetEquiv
            outer)
          (QuantumBlockEncoding.PromiseGateOptimization.controlledTargetEquiv
            middle)).trans
      (QuantumBlockEncoding.PromiseGateOptimization.liftTargetEquiv
        (Equiv.symm outer)) =
    QuantumBlockEncoding.PromiseGateOptimization.controlledTargetEquiv
      (QuantumBlockEncoding.PromiseGateOptimization.conjugatedTargetEquiv
        outer middle)

Figure 3(a): controlling `V† U V` is equivalent to leaving `V` and `V†`
uncontrolled and controlling only `U`.

Theorem6.9.5

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “controlled conjugation matrix”; the hypotheses and conclusion in the code panel fix its exact scope. Matrix form of the controlled-conjugation identity.

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

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

Technical source note. Matrix form of the controlled-conjugation identity.

Declaration kind. theorem.

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

Lean code for Theorem6.9.5●1 theorem

theoremdefined in QuantumBlockEncoding/PromiseGateOptimization.lean

complete

theorem QuantumBlockEncoding.PromiseGateOptimization.controlledConjugation_matrix.{u_1}
  {α : Type u_1} [Fintype α] [DecidableEq α]
  (outer middle : Equiv.Perm α) :
  QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix
        (QuantumBlockEncoding.PromiseGateOptimization.liftTargetEquiv
          (Equiv.symm outer)) *
      (QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix
          (QuantumBlockEncoding.PromiseGateOptimization.controlledTargetEquiv
            middle) *
        QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix
          (QuantumBlockEncoding.PromiseGateOptimization.liftTargetEquiv
            outer)) =
    QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix
      (QuantumBlockEncoding.PromiseGateOptimization.controlledTargetEquiv
        (QuantumBlockEncoding.PromiseGateOptimization.conjugatedTargetEquiv
          outer middle))

theorem QuantumBlockEncoding.PromiseGateOptimization.controlledConjugation_matrix.{u_1}
  {α : Type u_1} [Fintype α]
  [DecidableEq α]
  (outer middle : Equiv.Perm α) :
  QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix
        (QuantumBlockEncoding.PromiseGateOptimization.liftTargetEquiv
          (Equiv.symm outer)) *
      (QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix
          (QuantumBlockEncoding.PromiseGateOptimization.controlledTargetEquiv
            middle) *
        QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix
          (QuantumBlockEncoding.PromiseGateOptimization.liftTargetEquiv
            outer)) =
    QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix
      (QuantumBlockEncoding.PromiseGateOptimization.controlledTargetEquiv
        (QuantumBlockEncoding.PromiseGateOptimization.conjugatedTargetEquiv
          outer middle))

Matrix form of the controlled-conjugation identity.

Definition6.9.6

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “weak promise spec”. Exact clean-branch contract for a weak promise gate.

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

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

Technical source note. Exact clean-branch contract for a weak promise gate. No behavior is required away from 'cleanPromise'.

Declaration kind. def.

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

Lean code for Definition6.9.6●1 definition

defdefined in QuantumBlockEncoding/PromiseGateOptimization.lean

complete

def QuantumBlockEncoding.PromiseGateOptimization.WeakPromiseSpec.{u_1, u_2}
  {ρ : Type u_1} {α : Type u_2} (cleanPromise : ρ)
  (implementation : Equiv.Perm (ρ × α)) (target : Equiv.Perm α) : Prop

def QuantumBlockEncoding.PromiseGateOptimization.WeakPromiseSpec.{u_1,
    u_2}
  {ρ : Type u_1} {α : Type u_2}
  (cleanPromise : ρ)
  (implementation : Equiv.Perm (ρ × α))
  (target : Equiv.Perm α) : Prop

Exact clean-branch contract for a weak promise gate.  No behavior is
required away from `cleanPromise`.

Definition6.9.7

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “strong promise spec”. A strong promise gate additionally restores its promise register for every basis input.

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

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

Technical source note. A strong promise gate additionally restores its promise register for every basis input.

Declaration kind. def.

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

Lean code for Definition6.9.7●1 definition

defdefined in QuantumBlockEncoding/PromiseGateOptimization.lean

complete

def QuantumBlockEncoding.PromiseGateOptimization.StrongPromiseSpec.{u_1,
    u_2}
  {ρ : Type u_1} {α : Type u_2} (cleanPromise : ρ)
  (implementation : Equiv.Perm (ρ × α)) (target : Equiv.Perm α) : Prop

def QuantumBlockEncoding.PromiseGateOptimization.StrongPromiseSpec.{u_1,
    u_2}
  {ρ : Type u_1} {α : Type u_2}
  (cleanPromise : ρ)
  (implementation : Equiv.Perm (ρ × α))
  (target : Equiv.Perm α) : Prop

A strong promise gate additionally restores its promise register for every
basis input.

Theorem6.9.8

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “weak”; the hypotheses and conclusion in the code panel fix its exact scope.

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

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

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

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

Lean code for Theorem6.9.8●1 theorem

theoremdefined in QuantumBlockEncoding/PromiseGateOptimization.lean

complete

theorem QuantumBlockEncoding.PromiseGateOptimization.StrongPromiseSpec.weak.{u_1,
    u_2}
  {ρ : Type u_1} {α : Type u_2} {cleanPromise : ρ}
  {implementation : Equiv.Perm (ρ × α)} {target : Equiv.Perm α}
  (spec :
    QuantumBlockEncoding.PromiseGateOptimization.StrongPromiseSpec
      cleanPromise implementation target) :
  QuantumBlockEncoding.PromiseGateOptimization.WeakPromiseSpec
    cleanPromise implementation target

theorem QuantumBlockEncoding.PromiseGateOptimization.StrongPromiseSpec.weak.{u_1,
    u_2}
  {ρ : Type u_1} {α : Type u_2}
  {cleanPromise : ρ}
  {implementation : Equiv.Perm (ρ × α)}
  {target : Equiv.Perm α}
  (spec :
    QuantumBlockEncoding.PromiseGateOptimization.StrongPromiseSpec
      cleanPromise implementation
      target) :
  QuantumBlockEncoding.PromiseGateOptimization.WeakPromiseSpec
    cleanPromise implementation target

Definition6.9.9

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “toggle dirty flag equiv”. Toggle a possibly dirty flag exactly when the control predicate holds.

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

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

Technical source note. Toggle a possibly dirty flag exactly when the control predicate holds.

Declaration kind. def.

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

Lean code for Definition6.9.9●1 definition

defdefined in QuantumBlockEncoding/PromiseGateOptimization.lean

complete

def QuantumBlockEncoding.PromiseGateOptimization.toggleDirtyFlagEquiv.{u_1,
    u_2}
  {κ : Type u_1} {α : Type u_2} (control : κ → Bool) :
  Equiv.Perm (κ × Bool × α)

def QuantumBlockEncoding.PromiseGateOptimization.toggleDirtyFlagEquiv.{u_1,
    u_2}
  {κ : Type u_1} {α : Type u_2}
  (control : κ → Bool) :
  Equiv.Perm (κ × Bool × α)

Toggle a possibly dirty flag exactly when the control predicate holds.

Definition6.9.10

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “dirty flag controlled target equiv”. Apply the target when the dirty flag is set, preserving key and flag.

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

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

Technical source note. Apply the target when the dirty flag is set, preserving key and flag.

Declaration kind. def.

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

Lean code for Definition6.9.10●1 definition

defdefined in QuantumBlockEncoding/PromiseGateOptimization.lean

complete

def QuantumBlockEncoding.PromiseGateOptimization.dirtyFlagControlledTargetEquiv.{u_1,
    u_2}
  {κ : Type u_1} {α : Type u_2} (target : Equiv.Perm α) :
  Equiv.Perm (κ × Bool × α)

def QuantumBlockEncoding.PromiseGateOptimization.dirtyFlagControlledTargetEquiv.{u_1,
    u_2}
  {κ : Type u_1} {α : Type u_2}
  (target : Equiv.Perm α) :
  Equiv.Perm (κ × Bool × α)

Apply the target when the dirty flag is set, preserving key and flag.

Definition6.9.11

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “dirty controlled involution equiv”. Compute-use-uncompute-use protocol from Figure 2(a), right-hand side.

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

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

Technical source note. Compute-use-uncompute-use protocol from Figure 2(a), right-hand side.

Declaration kind. def.

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

Lean code for Definition6.9.11●1 definition

defdefined in QuantumBlockEncoding/PromiseGateOptimization.lean

complete

def QuantumBlockEncoding.PromiseGateOptimization.dirtyControlledInvolutionEquiv.{u_1,
    u_2}
  {κ : Type u_1} {α : Type u_2} (control : κ → Bool)
  (target : Equiv.Perm α) : Equiv.Perm (κ × Bool × α)

def QuantumBlockEncoding.PromiseGateOptimization.dirtyControlledInvolutionEquiv.{u_1,
    u_2}
  {κ : Type u_1} {α : Type u_2}
  (control : κ → Bool)
  (target : Equiv.Perm α) :
  Equiv.Perm (κ × Bool × α)

Compute-use-uncompute-use protocol from Figure 2(a), right-hand side.

Theorem6.9.12

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “dirty controlled involution action”; the hypotheses and conclusion in the code panel fix its exact scope. A dirty flag is restored and the requested controlled target is applied, provided the target is involutory.

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

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

Technical source note. A dirty flag is restored and the requested controlled target is applied, provided the target is involutory.

Declaration kind. theorem.

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

Lean code for Theorem6.9.12●1 theorem

theoremdefined in QuantumBlockEncoding/PromiseGateOptimization.lean

complete

theorem QuantumBlockEncoding.PromiseGateOptimization.dirtyControlledInvolution_action.{u_1,
    u_2}
  {κ : Type u_1} {α : Type u_2} (control : κ → Bool)
  (target : Equiv.Perm α)
  (involutive : ∀ (value : α), target (target value) = value) (key : κ)
  (flag : Bool) (value : α) :
  (QuantumBlockEncoding.PromiseGateOptimization.dirtyControlledInvolutionEquiv
        control target)
      (key, flag, value) =
    (key, flag, if control key = true then target value else value)

theorem QuantumBlockEncoding.PromiseGateOptimization.dirtyControlledInvolution_action.{u_1,
    u_2}
  {κ : Type u_1} {α : Type u_2}
  (control : κ → Bool)
  (target : Equiv.Perm α)
  (involutive :
    ∀ (value : α),
      target (target value) = value)
  (key : κ) (flag : Bool) (value : α) :
  (QuantumBlockEncoding.PromiseGateOptimization.dirtyControlledInvolutionEquiv
        control target)
      (key, flag, value) =
    (key, flag,
      if control key = true then
        target value
      else value)

A dirty flag is restored and the requested controlled target is applied,
provided the target is involutory.

Theorem6.9.13

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “dirty controlled involution unitary”; the hypotheses and conclusion in the code panel fix its exact scope. The dirty-flag protocol is unitary because it is a basis permutation.

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

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

Technical source note. The dirty-flag protocol is unitary because it is a basis permutation.

Declaration kind. theorem.

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

Lean code for Theorem6.9.13●1 theorem

theoremdefined in QuantumBlockEncoding/PromiseGateOptimization.lean

complete

theorem QuantumBlockEncoding.PromiseGateOptimization.dirtyControlledInvolution_unitary.{u_1,
    u_2}
  {κ : Type u_1} {α : Type u_2} [Fintype κ] [DecidableEq κ] [Fintype α]
  [DecidableEq α] (control : κ → Bool) (target : Equiv.Perm α) :
  QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix
      (QuantumBlockEncoding.PromiseGateOptimization.dirtyControlledInvolutionEquiv
        control target) ∈
    Matrix.unitaryGroup (κ × Bool × α) ℂ

theorem QuantumBlockEncoding.PromiseGateOptimization.dirtyControlledInvolution_unitary.{u_1,
    u_2}
  {κ : Type u_1} {α : Type u_2}
  [Fintype κ] [DecidableEq κ] [Fintype α]
  [DecidableEq α] (control : κ → Bool)
  (target : Equiv.Perm α) :
  QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix
      (QuantumBlockEncoding.PromiseGateOptimization.dirtyControlledInvolutionEquiv
        control target) ∈
    Matrix.unitaryGroup (κ × Bool × α) ℂ

The dirty-flag protocol is unitary because it is a basis permutation.

Definition6.9.14

uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “controlled protocol cost”. A proposition-valued field is a requirement until a constructor supplies it. Abstract operation counts exposed to the ASPBE planner.

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

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

Technical source note. Abstract operation counts exposed to the ASPBE planner.

Declaration kind. structure.

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

Lean code for Definition6.9.14●1 definition

structure(4 fields)defined in QuantumBlockEncoding/PromiseGateOptimization.lean

complete

structure QuantumBlockEncoding.PromiseGateOptimization.ControlledProtocolCost :
  Type

structure QuantumBlockEncoding.PromiseGateOptimization.ControlledProtocolCost :
  Type

Abstract operation counts exposed to the ASPBE planner.

Fields

predicateToggles : ℕ

controlledTargetUses : ℕ

cleanFlags : ℕ

dirtyFlags : ℕ

Definition6.9.15

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “clean flag protocol cost”. Standard clean-flag construction: compute, use, uncompute.

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

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

Technical source note. Standard clean-flag construction: compute, use, uncompute.

Declaration kind. def.

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

Lean code for Definition6.9.15●1 definition

defdefined in QuantumBlockEncoding/PromiseGateOptimization.lean

complete

def QuantumBlockEncoding.PromiseGateOptimization.cleanFlagProtocolCost :
  QuantumBlockEncoding.PromiseGateOptimization.ControlledProtocolCost

def QuantumBlockEncoding.PromiseGateOptimization.cleanFlagProtocolCost :
  QuantumBlockEncoding.PromiseGateOptimization.ControlledProtocolCost

Standard clean-flag construction: compute, use, uncompute.

Definition6.9.16

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “dirty flag protocol cost”. Involutory dirty-flag construction: one extra controlled target use.

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

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

Technical source note. Involutory dirty-flag construction: one extra controlled target use.

Declaration kind. def.

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

Lean code for Definition6.9.16●1 definition

defdefined in QuantumBlockEncoding/PromiseGateOptimization.lean

complete

def QuantumBlockEncoding.PromiseGateOptimization.dirtyFlagProtocolCost :
  QuantumBlockEncoding.PromiseGateOptimization.ControlledProtocolCost

def QuantumBlockEncoding.PromiseGateOptimization.dirtyFlagProtocolCost :
  QuantumBlockEncoding.PromiseGateOptimization.ControlledProtocolCost

Involutory dirty-flag construction: one extra controlled target use.

Theorem6.9.17

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “dirty flag replaces clean flag”; the hypotheses and conclusion in the code panel fix its exact scope.

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

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

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

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

Lean code for Theorem6.9.17●1 theorem

theoremdefined in QuantumBlockEncoding/PromiseGateOptimization.lean

complete

theorem QuantumBlockEncoding.PromiseGateOptimization.dirtyFlag_replaces_cleanFlag :
  QuantumBlockEncoding.PromiseGateOptimization.dirtyFlagProtocolCost.cleanFlags =
      0 ∧
    QuantumBlockEncoding.PromiseGateOptimization.dirtyFlagProtocolCost.dirtyFlags =
        1 ∧
      QuantumBlockEncoding.PromiseGateOptimization.dirtyFlagProtocolCost.controlledTargetUses =
        QuantumBlockEncoding.PromiseGateOptimization.cleanFlagProtocolCost.controlledTargetUses +
          1

theorem QuantumBlockEncoding.PromiseGateOptimization.dirtyFlag_replaces_cleanFlag :
  QuantumBlockEncoding.PromiseGateOptimization.dirtyFlagProtocolCost.cleanFlags =
      0 ∧
    QuantumBlockEncoding.PromiseGateOptimization.dirtyFlagProtocolCost.dirtyFlags =
        1 ∧
      QuantumBlockEncoding.PromiseGateOptimization.dirtyFlagProtocolCost.controlledTargetUses =
        QuantumBlockEncoding.PromiseGateOptimization.cleanFlagProtocolCost.controlledTargetUses +
          1