This definition gives the library's named construction or computation for “lift target equiv”. Apply a target permutation without changing its control register.
def liftTargetEquiv {α : Type*} (target : Equiv.Perm α) :
Equiv.Perm (Bool × α) :=
Equiv.prodCongr (Equiv.refl Bool) target
/-- Apply the target permutation exactly on the `true` control branch. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “controlled target equiv”. Apply the target permutation exactly on the 'true' control branch.
def controlledTargetEquiv {α : Type*} (target : Equiv.Perm α) :
Equiv.Perm (Bool × α) where
toFun state :=
if state.1 then (state.1, target state.2) else state
invFun state :=
if state.1 then (state.1, target.symm state.2) else state
left_inv state := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “conjugated target equiv”. Chronological 'V', then 'U', then 'V†'.
def conjugatedTargetEquiv {α : Type*}
(outer middle : Equiv.Perm α) : Equiv.Perm α :=
outer.trans (middle.trans outer.symm)
/-- Figure 3(a): controlling `V† U V` is equivalent to leaving `V` and `V†`
uncontrolled and controlling only `U`. -/
commit-pinned source · Verso Blueprint panel
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'.
theorem controlledConjugation_equiv {α : Type*}
(outer middle : Equiv.Perm α) :
((liftTargetEquiv outer).trans
(controlledTargetEquiv middle)).trans
(liftTargetEquiv outer.symm) =
controlledTargetEquiv (conjugatedTargetEquiv outer middle) := by
commit-pinned source · Verso Blueprint panel
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.
theorem controlledConjugation_matrix
{α : Type*} [Fintype α] [DecidableEq α]
(outer middle : Equiv.Perm α) :
Robin.ComplexLCU.equivPermutationMatrix (liftTargetEquiv outer.symm) *
(Robin.ComplexLCU.equivPermutationMatrix (controlledTargetEquiv middle) *
Robin.ComplexLCU.equivPermutationMatrix (liftTargetEquiv outer)) =
Robin.ComplexLCU.equivPermutationMatrix
(controlledTargetEquiv (conjugatedTargetEquiv outer middle)) := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “weak promise spec”. Exact clean-branch contract for a weak promise gate.
def WeakPromiseSpec {ρ α : Type*}
(cleanPromise : ρ) (implementation : Equiv.Perm (ρ × α))
(target : Equiv.Perm α) : Prop :=
∀ value, implementation (cleanPromise, value) =
(cleanPromise, target value)
/-- A strong promise gate additionally restores its promise register for every
basis input. -/
commit-pinned source · Verso Blueprint panel
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.
def StrongPromiseSpec {ρ α : Type*}
(cleanPromise : ρ) (implementation : Equiv.Perm (ρ × α))
(target : Equiv.Perm α) : Prop :=
WeakPromiseSpec cleanPromise implementation target ∧
∀ promise value, (implementation (promise, value)).1 = promise
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “weak”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem StrongPromiseSpec.weak {ρ α : Type*}
{cleanPromise : ρ} {implementation : Equiv.Perm (ρ × α)}
{target : Equiv.Perm α}
(spec : StrongPromiseSpec cleanPromise implementation target) :
WeakPromiseSpec cleanPromise implementation target :=
spec.1
/-- Toggle a possibly dirty flag exactly when the control predicate holds. -/
commit-pinned source · Verso Blueprint panel
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.
def toggleDirtyFlagEquiv {κ α : Type*} (control : κ → Bool) :
Equiv.Perm (κ × Bool × α) where
toFun state :=
(state.1, if control state.1 then !state.2.1 else state.2.1, state.2.2)
invFun state :=
(state.1, if control state.1 then !state.2.1 else state.2.1, state.2.2)
left_inv state := by
commit-pinned source · Verso Blueprint panel
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.
def dirtyFlagControlledTargetEquiv {κ α : Type*}
(target : Equiv.Perm α) : Equiv.Perm (κ × Bool × α) where
toFun state :=
if state.2.1 then (state.1, state.2.1, target state.2.2) else state
invFun state :=
if state.2.1 then (state.1, state.2.1, target.symm state.2.2) else state
left_inv state := by
commit-pinned source · Verso Blueprint panel
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.
def dirtyControlledInvolutionEquiv {κ α : Type*}
(control : κ → Bool) (target : Equiv.Perm α) :
Equiv.Perm (κ × Bool × α) :=
(toggleDirtyFlagEquiv control).trans
((dirtyFlagControlledTargetEquiv target).trans
((toggleDirtyFlagEquiv control).trans
(dirtyFlagControlledTargetEquiv target)))
/-- A dirty flag is restored and the requested controlled target is applied,
provided the target is involutory. -/
commit-pinned source · Verso Blueprint panel
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.
theorem dirtyControlledInvolution_action
{κ α : Type*} (control : κ → Bool) (target : Equiv.Perm α)
(involutive : ∀ value, target (target value) = value)
(key : κ) (flag : Bool) (value : α) :
dirtyControlledInvolutionEquiv control target (key, flag, value) =
(key, flag, if control key then target value else value) := by
commit-pinned source · Verso Blueprint panel
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.
theorem dirtyControlledInvolution_unitary
{κ α : Type*} [Fintype κ] [DecidableEq κ]
[Fintype α] [DecidableEq α]
(control : κ → Bool) (target : Equiv.Perm α) :
Robin.ComplexLCU.equivPermutationMatrix
(dirtyControlledInvolutionEquiv control target) ∈
_root_.Matrix.unitaryGroup (κ × Bool × α) ℂ :=
Robin.ComplexLCU.equivPermutationMatrix_unitary _
/-- Abstract operation counts exposed to the ASPBE planner. -/
commit-pinned source · Verso Blueprint panel
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.
structure ControlledProtocolCost where
predicateToggles : Nat
controlledTargetUses : Nat
cleanFlags : Nat
dirtyFlags : Nat
deriving DecidableEq, Repr
/-- Standard clean-flag construction: compute, use, uncompute. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “clean flag protocol cost”. Standard clean-flag construction: compute, use, uncompute.
def cleanFlagProtocolCost : ControlledProtocolCost where
predicateToggles := 2
controlledTargetUses := 1
cleanFlags := 1
dirtyFlags := 0
/-- Involutory dirty-flag construction: one extra controlled target use. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “dirty flag protocol cost”. Involutory dirty-flag construction: one extra controlled target use.
def dirtyFlagProtocolCost : ControlledProtocolCost where
predicateToggles := 2
controlledTargetUses := 2
cleanFlags := 0
dirtyFlags := 1
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “dirty flag replaces clean flag”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem dirtyFlag_replaces_cleanFlag :
dirtyFlagProtocolCost.cleanFlags = 0 ∧
dirtyFlagProtocolCost.dirtyFlags = 1 ∧
dirtyFlagProtocolCost.controlledTargetUses =
cleanFlagProtocolCost.controlledTargetUses + 1 := by
commit-pinned source · Verso Blueprint panel