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)'.
def mainCaseProSystemIndex (T tau S : Fin 2) : Fin 8 :=
⟨4 * T.val + 2 * tau.val + S.val, by
have hT : T.val ≤ 1 := Nat.le_of_lt_succ T.isLt
have hTau : tau.val ≤ 1 := Nat.le_of_lt_succ tau.isLt
have hS : S.val ≤ 1 := Nat.le_of_lt_succ S.isLt
omega⟩
/--
The target matrix for `E_1`.
It maps `|1>_T |1>_tau |s>_S` to `|0>_T |0>_tau |s>_S`
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “main case pro target”. The target matrix for 'E_1'.
def mainCaseProTarget : Matrix 8 8 Rat :=
fun row col =>
if (row = mainCaseProSystemIndex 0 0 0 ∧
col = mainCaseProSystemIndex 1 1 0) ∨
(row = mainCaseProSystemIndex 0 0 1 ∧
col = mainCaseProSystemIndex 1 1 1) then
1
else
0
/-- Operator-first target metadata for the Pro-isolated main-case benchmark. -/
commit-pinned source · Verso Blueprint panel
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.
def mainCaseProQueryTarget : QueryOperatorTarget Rat 8 8 where
operator := mainCaseProTarget
normalizer := 1
source :=
"QBE-MAIN-CASE-HIER-PRO-001: E_1 = |0><1|_T tensor |0><1|_tau tensor I_S"
semanticContract :=
"exact one-clean-signal block projection equals E_1; signalDim=2; signalIndex=0; epsilon=0"
freeParameters := [
"time qubits = 1",
"type qubits = 1",
"state qubits = 1",
commit-pinned source · Verso Blueprint panel
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.
def mainCaseProSignalIndex : Fin 2 := 0
/-- Clean embedding into the signal-system product basis. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “main case pro clean embed”. Clean embedding into the signal-system product basis.
def mainCaseProCleanEmbed (i : Fin 8) : Fin 16 :=
BlockEncodingClassics.productIndex mainCaseProSignalIndex i
/--
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.
-/
commit-pinned source · Verso Blueprint panel
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.
def mainCaseProBlockProjection
(U : Matrix (2 * 8) (2 * 8) Rat) : Prop :=
Matrix.PointwiseEq
(signalSystemBlockProjection 2 8 8 U mainCaseProSignalIndex)
mainCaseProTarget
/-- Exact normalizer for the requested block encoding. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “main case pro exact normalizer”. Exact normalizer for the requested block encoding.
def mainCaseProExactNormalizer : Rat := 1
/-- Exact error for the requested block encoding. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “main case pro exact error”. Exact error for the requested block encoding.
def mainCaseProExactError : Rat := 0
/-- Source-facing layout: three system qubits and one clean signal ancilla. -/
commit-pinned source · Verso Blueprint panel
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.
def mainCaseProSourceLayout : RegisterLayout where
systemQubits := 3
signalQubits := 1
pureAncillas := 0
/-- Logical `{X,CNOT,Toffoli}` transcript for the Pro equality-transfer idea. -/
commit-pinned source · Verso Blueprint panel
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.
def mainCaseProCircuit : Circuit :=
[ Gate.multiControlled [(1, true), (2, true)] (Gate.oneQubit "X" 3)
, Gate.cnot 3 2
, Gate.cnot 3 1
, Gate.oneQubit "X" 3
]
/-- Sequential high-level schedule for the current logical transcript. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “main case pro schedule”. Sequential high-level schedule for the current logical transcript.
def mainCaseProSchedule : LayeredCircuit :=
[ [Gate.multiControlled [(1, true), (2, true)] (Gate.oneQubit "X" 3)]
, [Gate.cnot 3 2]
, [Gate.cnot 3 1]
, [Gate.oneQubit "X" 3]
]
/--
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.
commit-pinned source · Verso Blueprint panel
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.
def mainCaseProHighLevelResource : Resource :=
Resource.ofCountsWithDepth 1 3 0 0 4
/-- Source-facing high-level score `(gateCount, depth, auxiliaryQubits, oracleCalls)`. -/
commit-pinned source · Verso Blueprint panel
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)'.
def mainCaseProHighLevelSeedCost : BlockEncodingCost :=
BlockEncodingCost.fromLayoutAndResource
mainCaseProSourceLayout mainCaseProHighLevelResource
commit-pinned source · Verso Blueprint panel
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.
theorem mainCaseProHighLevelSeedCost_gateCount :
mainCaseProHighLevelSeedCost.gateCount = 4 := rfl
commit-pinned source · Verso Blueprint panel
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.
theorem mainCaseProHighLevelSeedCost_depth :
mainCaseProHighLevelSeedCost.depth = 4 := rfl
commit-pinned source · Verso Blueprint panel
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.
theorem mainCaseProHighLevelSeedCost_auxiliaryQubits :
mainCaseProHighLevelSeedCost.auxiliaryQubits = 1 := rfl
commit-pinned source · Verso Blueprint panel
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.
theorem mainCaseProHighLevelSeedCost_oracleCalls :
mainCaseProHighLevelSeedCost.oracleCalls = 0 := rfl
/--
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`.
-/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “main case pro matrix table resource”. Matrix-table metadata for 'mainCaseProCandidate'.
def mainCaseProMatrixTableResource : Resource :=
Resource.ofCountsWithDepth 0 0 1 0 1
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “main case pro matrix table circuit”.
def mainCaseProMatrixTableCircuit : Circuit := []
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “main case pro matrix table schedule”.
def mainCaseProMatrixTableSchedule : LayeredCircuit := []
/--
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`.
-/
commit-pinned source · Verso Blueprint panel
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.
def mainCaseProCandidateImage : Fin 16 → Fin 16
| ⟨0, _⟩ => ⟨8, by decide⟩
| ⟨1, _⟩ => ⟨9, by decide⟩
| ⟨2, _⟩ => ⟨10, by decide⟩
| ⟨3, _⟩ => ⟨11, by decide⟩
| ⟨4, _⟩ => ⟨12, by decide⟩
| ⟨5, _⟩ => ⟨13, by decide⟩
| ⟨6, _⟩ => ⟨0, by decide⟩
| ⟨7, _⟩ => ⟨1, by decide⟩
| ⟨8, _⟩ => ⟨2, by decide⟩
| ⟨9, _⟩ => ⟨3, by decide⟩
commit-pinned source · Verso Blueprint panel
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'.
def mainCaseProCandidateMatrix : Matrix (2 * 8) (2 * 8) Rat :=
BlockEncodingClassics.permMatrix mainCaseProCandidateImage
commit-pinned source · Verso Blueprint panel
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.
theorem mainCaseProCandidateImage_clean_source_state0 :
mainCaseProCandidateImage ⟨6, by decide⟩ = ⟨0, by decide⟩ := by
commit-pinned source · Verso Blueprint panel
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.
theorem mainCaseProCandidateImage_clean_source_state1 :
mainCaseProCandidateImage ⟨7, by decide⟩ = ⟨1, by decide⟩ := by
commit-pinned source · Verso Blueprint panel
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.
theorem mainCaseProCandidateImage_injective_pointwise :
∀ x y : Fin 16,
mainCaseProCandidateImage x = mainCaseProCandidateImage y → x = y := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “main case pro candidate image injective”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem mainCaseProCandidateImage_injective :
Function.Injective mainCaseProCandidateImage := by
commit-pinned source · Verso Blueprint panel
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.
def mainCaseProCandidatePreimage : Fin 16 → Fin 16
| ⟨0, _⟩ => ⟨6, by decide⟩
| ⟨1, _⟩ => ⟨7, by decide⟩
| ⟨2, _⟩ => ⟨8, by decide⟩
| ⟨3, _⟩ => ⟨9, by decide⟩
| ⟨4, _⟩ => ⟨10, by decide⟩
| ⟨5, _⟩ => ⟨11, by decide⟩
| ⟨6, _⟩ => ⟨12, by decide⟩
| ⟨7, _⟩ => ⟨13, by decide⟩
| ⟨8, _⟩ => ⟨0, by decide⟩
| ⟨9, _⟩ => ⟨1, by decide⟩
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “main case pro candidate image preimage”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem mainCaseProCandidateImage_preimage :
∀ y : Fin 16,
mainCaseProCandidateImage (mainCaseProCandidatePreimage y) = y := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “main case pro candidate image surjective”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem mainCaseProCandidateImage_surjective :
Function.Surjective mainCaseProCandidateImage := by
commit-pinned source · Verso Blueprint panel
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.
def mainCaseProCandidateImageIsPermutation : Prop :=
Function.Injective mainCaseProCandidateImage ∧
Function.Surjective mainCaseProCandidateImage
commit-pinned source · Verso Blueprint panel
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.
theorem mainCaseProCandidateImage_permutation_certificate :
mainCaseProCandidateImageIsPermutation :=
⟨mainCaseProCandidateImage_injective, mainCaseProCandidateImage_surjective⟩
commit-pinned source · Verso Blueprint panel
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.
theorem mainCaseProCandidateMatrix_isRationalOrthogonal :
BlockEncodingClassics.IsRationalOrthogonal mainCaseProCandidateMatrix := by
commit-pinned source · Verso Blueprint panel
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)'.
def mainCaseProReducedOfFull (x : Fin 16) : Fin 8 :=
⟨x.val / 2, by omega⟩
/-- Passive state bit in the full `(signal,T,tau,S)` convention. -/
commit-pinned source · Verso Blueprint panel
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.
def mainCaseProStateOfFull (x : Fin 16) : Fin 2 :=
⟨x.val % 2, Nat.mod_lt x.val (by decide)⟩
/-- Lift a reduced active-register image while preserving the passive state bit. -/
commit-pinned source · Verso Blueprint panel
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.
def mainCaseProLiftReducedImage (f : Fin 8 → Fin 8) (x : Fin 16) : Fin 16 :=
⟨2 * (f (mainCaseProReducedOfFull x)).val + (mainCaseProStateOfFull x).val, by
have hf : (f (mainCaseProReducedOfFull x)).val < 8 :=
(f (mainCaseProReducedOfFull x)).isLt
have hs : (mainCaseProStateOfFull x).val < 2 :=
(mainCaseProStateOfFull x).isLt
omega⟩
/-- Reduced Toffoli `CCX012`, with controls `tau,T` and target `signal`. -/
commit-pinned source · Verso Blueprint panel
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'.
def mainCaseProRedCCX012 (x : Fin 8) : Fin 8 :=
if x.val = 3 then ⟨7, by decide⟩
else if x.val = 7 then ⟨3, by decide⟩
else x
/-- Reduced `CX21`, with control `signal` and target `T`. -/
commit-pinned source · Verso Blueprint panel
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'.
def mainCaseProRedCX21 (x : Fin 8) : Fin 8 :=
if x.val = 4 then ⟨6, by decide⟩
else if x.val = 6 then ⟨4, by decide⟩
else if x.val = 5 then ⟨7, by decide⟩
else if x.val = 7 then ⟨5, by decide⟩
else x
/-- Reduced `CX20`, with control `signal` and target `tau`. -/
commit-pinned source · Verso Blueprint panel
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'.
def mainCaseProRedCX20 (x : Fin 8) : Fin 8 :=
if x.val = 4 then ⟨5, by decide⟩
else if x.val = 5 then ⟨4, by decide⟩
else if x.val = 6 then ⟨7, by decide⟩
else if x.val = 7 then ⟨6, by decide⟩
else x
/-- Reduced final `X2`, flipping the signal bit. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “main case pro red x 2”. Reduced final 'X2', flipping the signal bit.
def mainCaseProRedX2 (x : Fin 8) : Fin 8 :=
if x.val = 0 then ⟨4, by decide⟩
else if x.val = 1 then ⟨5, by decide⟩
else if x.val = 2 then ⟨6, by decide⟩
else if x.val = 3 then ⟨7, by decide⟩
else if x.val = 4 then ⟨0, by decide⟩
else if x.val = 5 then ⟨1, by decide⟩
else if x.val = 6 then ⟨2, by decide⟩
else ⟨3, by decide⟩
/-- Task-local reduced image for the transcript `CCX012; CX21; CX20; X2`. -/
commit-pinned source · Verso Blueprint panel
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'.
def mainCaseProCircuitReducedImage (x : Fin 8) : Fin 8 :=
mainCaseProRedX2
(mainCaseProRedCX20
(mainCaseProRedCX21
(mainCaseProRedCCX012 x)))
/--
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`.
-/
commit-pinned source · Verso Blueprint panel
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'.
def mainCaseProCircuitImage : Fin 16 → Fin 16 :=
mainCaseProLiftReducedImage mainCaseProCircuitReducedImage
commit-pinned source · Verso Blueprint panel
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.
theorem mainCaseProCircuitImage_clean_source_state0 :
mainCaseProCircuitImage ⟨6, by decide⟩ = ⟨0, by decide⟩ := by
commit-pinned source · Verso Blueprint panel
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.
theorem mainCaseProCircuitImage_clean_source_state1 :
mainCaseProCircuitImage ⟨7, by decide⟩ = ⟨1, by decide⟩ := by
commit-pinned source · Verso Blueprint panel
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'.
theorem mainCaseProCircuitImage_candidate_mismatch_set :
∀ x : Fin 16,
(mainCaseProCircuitImage x ≠ mainCaseProCandidateImage x) ↔
x.val ∈ [8, 9, 12, 13] := by
commit-pinned source · Verso Blueprint panel
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.
theorem mainCaseProCircuitImage_not_pointwise_candidate :
¬ ∀ x : Fin 16, mainCaseProCircuitImage x = mainCaseProCandidateImage x := by
commit-pinned source · Verso Blueprint panel
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.
def mainCaseProCircuitMatrix : Matrix (2 * 8) (2 * 8) Rat :=
BlockEncodingClassics.permMatrix mainCaseProCircuitImage
commit-pinned source · Verso Blueprint panel
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.
theorem mainCaseProCircuitImage_injective_pointwise :
∀ x y : Fin 16,
mainCaseProCircuitImage x = mainCaseProCircuitImage y → x = y := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “main case pro circuit image injective”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem mainCaseProCircuitImage_injective :
Function.Injective mainCaseProCircuitImage := by
commit-pinned source · Verso Blueprint panel
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.
theorem mainCaseProCircuitImage_surjective_pointwise :
∀ y : Fin 16, ∃ x : Fin 16, mainCaseProCircuitImage x = y := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “main case pro circuit image surjective”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem mainCaseProCircuitImage_surjective :
Function.Surjective mainCaseProCircuitImage :=
mainCaseProCircuitImage_surjective_pointwise
/-- Task-local finite-permutation certificate for the Pro transcript image. -/
commit-pinned source · Verso Blueprint panel
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.
def mainCaseProCircuitImageIsPermutation : Prop :=
Function.Injective mainCaseProCircuitImage ∧
Function.Surjective mainCaseProCircuitImage
commit-pinned source · Verso Blueprint panel
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.
theorem mainCaseProCircuitImage_permutation_certificate :
mainCaseProCircuitImageIsPermutation :=
⟨mainCaseProCircuitImage_injective, mainCaseProCircuitImage_surjective⟩
commit-pinned source · Verso Blueprint panel
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.
theorem mainCaseProCircuitMatrix_isRationalOrthogonal :
BlockEncodingClassics.IsRationalOrthogonal mainCaseProCircuitMatrix := by
commit-pinned source · Verso Blueprint panel
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.
theorem mainCaseProCircuit_cleanEntry :
∀ row col : Fin 8,
(if mainCaseProCleanEmbed row =
mainCaseProCircuitImage (mainCaseProCleanEmbed col) then
1
else
0) =
mainCaseProTarget row col := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “main case pro circuit block projection”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem mainCaseProCircuit_blockProjection :
mainCaseProBlockProjection mainCaseProCircuitMatrix := by
commit-pinned source · Verso Blueprint panel
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.
theorem mainCaseProTarget_support_state0 :
mainCaseProTarget
(mainCaseProSystemIndex 0 0 0)
(mainCaseProSystemIndex 1 1 0) = 1 := by
commit-pinned source · Verso Blueprint panel
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.
theorem mainCaseProTarget_support_state1 :
mainCaseProTarget
(mainCaseProSystemIndex 0 0 1)
(mainCaseProSystemIndex 1 1 1) = 1 := by
commit-pinned source · Verso Blueprint panel
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.
theorem mainCaseProCandidate_cleanEntry :
∀ row col : Fin 8,
(if mainCaseProCleanEmbed row =
mainCaseProCandidateImage (mainCaseProCleanEmbed col) then
1
else
0) =
mainCaseProTarget row col := by
commit-pinned source · Verso Blueprint panel
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.
def mainCaseProExactCleanBlockCertificate :
BlockEncodingClassics.ExactCleanBlock 8 16 :=
BlockEncodingClassics.partialPermutationCertificate
mainCaseProCleanEmbed
mainCaseProCandidateImage
mainCaseProTarget
mainCaseProCandidate_cleanEntry
commit-pinned source · Verso Blueprint panel
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.
theorem mainCaseProExactCleanBlock_correct :
Matrix.PointwiseEq
(BlockEncodingClassics.ExactCleanBlock.clean
mainCaseProExactCleanBlockCertificate)
mainCaseProTarget :=
BlockEncodingClassics.ExactCleanBlock.clean_eq_target
mainCaseProExactCleanBlockCertificate
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “main case pro candidate block projection”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem mainCaseProCandidate_blockProjection :
mainCaseProBlockProjection mainCaseProCandidateMatrix := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “main case pro query target normalizer”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem mainCaseProQueryTarget_normalizer :
mainCaseProQueryTarget.normalizer = mainCaseProExactNormalizer := rfl
commit-pinned source · Verso Blueprint panel
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.
theorem mainCaseProSourceLayout_auxiliaryQubits :
mainCaseProSourceLayout.auxiliaryQubits = 1 := rfl
/--
Reusable proof obligation for a later shared bridge from finite bijections to
the project-local rational-orthogonality matrix predicate.
-/
commit-pinned source · Verso Blueprint panel
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.
def mainCaseProRationalOrthogonalBridgeObligation : SemanticObligation where
description :=
"prove a shared theorem that a bijective finite image induces a rational orthogonal permMatrix"
source := "QBE-MAIN-CASE-HIER-PRO-001, MAINCASE-PRO-ORTHO-BRIDGE-001"
proved := true
/-- Candidate record at the finite-permutation semantic tier. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “main case pro candidate”. Candidate record at the finite-permutation semantic tier.
def mainCaseProCandidate : OperatorBlockEncodingCandidate Rat 3 where
auxiliaryQubits := 1
target := mainCaseProQueryTarget
unitary := mainCaseProCandidateMatrix
layout := mainCaseProSourceLayout
circuit := mainCaseProMatrixTableCircuit
schedule := mainCaseProMatrixTableSchedule
resource := mainCaseProMatrixTableResource
layoutMatches := rfl
isUnitary := mainCaseProCandidateImageIsPermutation
blockContainsTarget := mainCaseProBlockProjection mainCaseProCandidateMatrix
commit-pinned source · Verso Blueprint panel
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.
def mainCaseProCircuitCandidate : OperatorBlockEncodingCandidate Rat 3 where
auxiliaryQubits := 1
target := mainCaseProQueryTarget
unitary := mainCaseProCircuitMatrix
layout := mainCaseProSourceLayout
circuit := mainCaseProCircuit
schedule := mainCaseProSchedule
resource := mainCaseProHighLevelResource
layoutMatches := rfl
isUnitary := mainCaseProCircuitImageIsPermutation
blockContainsTarget := mainCaseProBlockProjection mainCaseProCircuitMatrix
commit-pinned source · Verso Blueprint panel
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.
def mainCaseProVerified : VerifiedOperatorBlockEncoding Rat 3 where
candidate := mainCaseProCandidate
unitaryProof := by
commit-pinned source · Verso Blueprint panel
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.
def mainCaseProCircuitVerified : VerifiedOperatorBlockEncoding Rat 3 where
candidate := mainCaseProCircuitCandidate
unitaryProof := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “main case pro candidate cost”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem mainCaseProCandidate_cost :
mainCaseProCandidate.cost =
{ auxiliaryQubits := 1, gateCount := 1, depth := 1, oracleCalls := 1 } := by
commit-pinned source · Verso Blueprint panel
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.
theorem mainCaseProCandidate_uses_matrix_table_metadata :
mainCaseProCandidate.circuit = mainCaseProMatrixTableCircuit ∧
mainCaseProCandidate.schedule = mainCaseProMatrixTableSchedule ∧
mainCaseProCandidate.resource = mainCaseProMatrixTableResource := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “main case pro circuit candidate cost”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem mainCaseProCircuitCandidate_cost :
mainCaseProCircuitCandidate.cost =
{ auxiliaryQubits := 1, gateCount := 4, depth := 4, oracleCalls := 0 } := by
commit-pinned source · Verso Blueprint panel
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)'.
def mainCaseColdSystemIndex (T tau S : Fin 2) : Fin 8 :=
⟨4 * T.val + 2 * tau.val + S.val, by
have hT : T.val ≤ 1 := Nat.le_of_lt_succ T.isLt
have hTau : tau.val ≤ 1 := Nat.le_of_lt_succ tau.isLt
have hS : S.val ≤ 1 := Nat.le_of_lt_succ S.isLt
omega⟩
/--
The COLD target matrix for `E_1`.
It maps `|1>_T |1>_tau |s>_S` to `|0>_T |0>_tau |s>_S`
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “main case cold target”. The COLD target matrix for 'E_1'.
def mainCaseColdTarget : Matrix 8 8 Rat :=
fun row col =>
if (row = mainCaseColdSystemIndex 0 0 0 ∧
col = mainCaseColdSystemIndex 1 1 0) ∨
(row = mainCaseColdSystemIndex 0 0 1 ∧
col = mainCaseColdSystemIndex 1 1 1) then
1
else
0
/-- Exact normalizer for the no-Pro COLD target. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “main case cold exact normalizer”. Exact normalizer for the no-Pro COLD target.
def mainCaseColdExactNormalizer : Rat := 1
/-- Exact error for the no-Pro COLD target. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “main case cold exact error”. Exact error for the no-Pro COLD target.
def mainCaseColdExactError : Rat := 0
/-- Operator-first target metadata for the no-Pro COLD benchmark. -/
commit-pinned source · Verso Blueprint panel
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.
def mainCaseColdQueryTarget : QueryOperatorTarget Rat 8 8 where
operator := mainCaseColdTarget
normalizer := mainCaseColdExactNormalizer
source :=
"QBE-MAIN-CASE-HIER-COLD-001: E_1 = |0><1|_T tensor |0><1|_tau tensor I_S"
semanticContract :=
"exact one-clean-signal block projection equals E_1; signalDim=2; signalIndex=0; epsilon=0"
freeParameters := [
"time qubits = 1",
"type qubits = 1",
"state qubits = 1",
commit-pinned source · Verso Blueprint panel
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.
def mainCaseColdCleanSignal : Fin 2 := 0
/-- Clean embedding into the signal-system product basis. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “main case cold clean embed”. Clean embedding into the signal-system product basis.
def mainCaseColdCleanEmbed (i : Fin 8) : Fin 16 :=
BlockEncodingClassics.productIndex mainCaseColdCleanSignal i
/--
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.
-/
commit-pinned source · Verso Blueprint panel
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.
def mainCaseColdBlockProjection
(U : Matrix (2 * 8) (2 * 8) Rat) : Prop :=
Matrix.PointwiseEq
(signalSystemBlockProjection 2 8 8 U mainCaseColdCleanSignal)
mainCaseColdTarget
/-- Source-facing layout: three system qubits and one clean signal ancilla. -/
commit-pinned source · Verso Blueprint panel
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.
def mainCaseColdSourceLayout : RegisterLayout where
systemQubits := 3
signalQubits := 1
pureAncillas := 0
/--
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`.
-/
commit-pinned source · Verso Blueprint panel
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.
def mainCaseColdPartialPermImage : Fin 16 → Fin 16
| ⟨0, _⟩ => ⟨14, by decide⟩
| ⟨1, _⟩ => ⟨15, by decide⟩
| ⟨2, _⟩ => ⟨8, by decide⟩
| ⟨3, _⟩ => ⟨9, by decide⟩
| ⟨4, _⟩ => ⟨10, by decide⟩
| ⟨5, _⟩ => ⟨11, by decide⟩
| ⟨6, _⟩ => ⟨0, by decide⟩
| ⟨7, _⟩ => ⟨1, by decide⟩
| ⟨8, _⟩ => ⟨2, by decide⟩
| ⟨9, _⟩ => ⟨3, by decide⟩
commit-pinned source · Verso Blueprint panel
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'.
def mainCaseColdPartialPermMatrix : Matrix (2 * 8) (2 * 8) Rat :=
BlockEncodingClassics.permMatrix mainCaseColdPartialPermImage
/-- Reduced active index for the COLD table bits `(tau,T,signal)`. -/
commit-pinned source · Verso Blueprint panel
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)'.
def mainCaseColdReducedOfFull (x : Fin 16) : Fin 8 :=
⟨x.val / 2, by omega⟩
/-- Passive state bit in the full `(signal,T,tau,S)` convention. -/
commit-pinned source · Verso Blueprint panel
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.
def mainCaseColdStateOfFull (x : Fin 16) : Fin 2 :=
⟨x.val % 2, Nat.mod_lt x.val (by decide)⟩
/-- Lift a reduced active-register image while preserving the passive state bit. -/
commit-pinned source · Verso Blueprint panel
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.
def mainCaseColdLiftReducedImage (f : Fin 8 → Fin 8) (x : Fin 16) : Fin 16 :=
⟨2 * (f (mainCaseColdReducedOfFull x)).val +
(mainCaseColdStateOfFull x).val, by
have hf : (f (mainCaseColdReducedOfFull x)).val < 8 :=
(f (mainCaseColdReducedOfFull x)).isLt
have hs : (mainCaseColdStateOfFull x).val < 2 :=
(mainCaseColdStateOfFull x).isLt
omega⟩
/-- Reduced `X` on the `T` bit. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “main case cold red xt”. Reduced 'X' on the 'T' bit.
def mainCaseColdRedXT (x : Fin 8) : Fin 8 :=
if x.val = 0 then ⟨2, by decide⟩
else if x.val = 1 then ⟨3, by decide⟩
else if x.val = 2 then ⟨0, by decide⟩
else if x.val = 3 then ⟨1, by decide⟩
else if x.val = 4 then ⟨6, by decide⟩
else if x.val = 5 then ⟨7, by decide⟩
else if x.val = 6 then ⟨4, by decide⟩
else ⟨5, by decide⟩
/-- Reduced Toffoli with controls `tau,T` and target `signal`. -/
commit-pinned source · Verso Blueprint panel
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'.
def mainCaseColdRedCCXTauTSignal (x : Fin 8) : Fin 8 :=
if x.val = 3 then ⟨7, by decide⟩
else if x.val = 7 then ⟨3, by decide⟩
else x
/-- Reduced `X` on the `tau` bit. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “main case cold red x tau”. Reduced 'X' on the 'tau' bit.
def mainCaseColdRedXTau (x : Fin 8) : Fin 8 :=
if x.val = 0 then ⟨1, by decide⟩
else if x.val = 1 then ⟨0, by decide⟩
else if x.val = 2 then ⟨3, by decide⟩
else if x.val = 3 then ⟨2, by decide⟩
else if x.val = 4 then ⟨5, by decide⟩
else if x.val = 5 then ⟨4, by decide⟩
else if x.val = 6 then ⟨7, by decide⟩
else ⟨6, by decide⟩
/-- Reduced CNOT with control `signal` and target `T`. -/
commit-pinned source · Verso Blueprint panel
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'.
def mainCaseColdRedCXSignalT (x : Fin 8) : Fin 8 :=
if x.val = 4 then ⟨6, by decide⟩
else if x.val = 6 then ⟨4, by decide⟩
else if x.val = 5 then ⟨7, by decide⟩
else if x.val = 7 then ⟨5, by decide⟩
else x
/-- Reduced CNOT with control `tau` and target `signal`. -/
commit-pinned source · Verso Blueprint panel
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'.
def mainCaseColdRedCXTauSignal (x : Fin 8) : Fin 8 :=
if x.val = 1 then ⟨5, by decide⟩
else if x.val = 5 then ⟨1, by decide⟩
else if x.val = 3 then ⟨7, by decide⟩
else if x.val = 7 then ⟨3, by decide⟩
else x
/-- Evaluate reduced logical reversible gates as basis-state permutations. -/
commit-pinned source · Verso Blueprint panel
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.
def mainCaseColdEvalReducedGateImages
(gates : List (Fin 8 → Fin 8)) (x : Fin 8) : Fin 8 :=
gates.foldl (fun y gateImage => gateImage y) x
/-- Reduced COLD table induced by `mainCaseColdPartialPermImage`. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “main case cold partial perm reduced image”. Reduced COLD table induced by 'mainCaseColdPartialPermImage'.
def mainCaseColdPartialPermReducedImage (x : Fin 8) : Fin 8 :=
if x.val = 0 then ⟨7, by decide⟩
else if x.val = 1 then ⟨4, by decide⟩
else if x.val = 2 then ⟨5, by decide⟩
else if x.val = 3 then ⟨0, by decide⟩
else if x.val = 4 then ⟨1, by decide⟩
else if x.val = 5 then ⟨2, by decide⟩
else if x.val = 6 then ⟨3, by decide⟩
else ⟨6, by decide⟩
/-- Reduced gate-image transcript for the COLD resource schema. -/
commit-pinned source · Verso Blueprint panel
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.
def mainCaseColdReducedGateImages : List (Fin 8 → Fin 8) :=
[ mainCaseColdRedXT
, mainCaseColdRedCCXTauTSignal
, mainCaseColdRedXTau
, mainCaseColdRedCXSignalT
, mainCaseColdRedCXTauSignal
]
/-- Reduced active-register image induced by the COLD resource schema. -/
commit-pinned source · Verso Blueprint panel
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.
def mainCaseColdCircuitReducedImage (x : Fin 8) : Fin 8 :=
mainCaseColdEvalReducedGateImages mainCaseColdReducedGateImages x
/-- The COLD logical reversible circuit implements the reduced table. -/
commit-pinned source · Verso Blueprint panel
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.
theorem mainCaseColdReducedGateImages_eval :
∀ x : Fin 8,
mainCaseColdCircuitReducedImage x =
mainCaseColdPartialPermReducedImage x := by
commit-pinned source · Verso Blueprint panel
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.
def mainCaseColdCircuitImage : Fin 16 → Fin 16 :=
mainCaseColdLiftReducedImage mainCaseColdCircuitReducedImage
/-- The COLD logical reversible circuit implements the finite table. -/
commit-pinned source · Verso Blueprint panel
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.
theorem mainCaseColdCircuitImage_eq_partialPermImage :
∀ x : Fin 16,
mainCaseColdCircuitImage x = mainCaseColdPartialPermImage x := by
commit-pinned source · Verso Blueprint panel
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.
def mainCaseColdGateXT : Gate :=
Gate.oneQubit "X" 2
/-- Logical Toffoli with controls `tau,T` and target `signal`. -/
commit-pinned source · Verso Blueprint panel
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'.
def mainCaseColdGateCCXTauTSignal : Gate :=
Gate.multiControlled [(1, true), (2, true)] (Gate.oneQubit "X" 3)
/-- Logical `X` on the type register `tau` in the full wire layout. -/
commit-pinned source · Verso Blueprint panel
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.
def mainCaseColdGateXTau : Gate :=
Gate.oneQubit "X" 1
/-- Logical CNOT with control `signal` and target `T`. -/
commit-pinned source · Verso Blueprint panel
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'.
def mainCaseColdGateCXSignalT : Gate :=
Gate.cnot 3 2
/-- Logical CNOT with control `tau` and target `signal`. -/
commit-pinned source · Verso Blueprint panel
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'.
def mainCaseColdGateCXTauSignal : Gate :=
Gate.cnot 1 3
/-- COLD task-local logical circuit for the finite partial-permutation table. -/
commit-pinned source · Verso Blueprint panel
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.
def mainCaseColdCircuit : Circuit :=
[ mainCaseColdGateXT
, mainCaseColdGateCCXTauTSignal
, mainCaseColdGateXTau
, mainCaseColdGateCXSignalT
, mainCaseColdGateCXTauSignal
]
/-- Sequential COLD schedule for the current logical transcript. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “main case cold schedule”. Sequential COLD schedule for the current logical transcript.
def mainCaseColdSchedule : LayeredCircuit :=
[ [mainCaseColdGateXT]
, [mainCaseColdGateCCXTauTSignal]
, [mainCaseColdGateXTau]
, [mainCaseColdGateCXSignalT]
, [mainCaseColdGateCXTauSignal]
]
/--
High-level logical-library resource record for the COLD transcript. At this
semantic tier, Toffoli and CNOT are counted together as controlled logical
commit-pinned source · Verso Blueprint panel
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.
def mainCaseColdHighLevelResource : Resource :=
Resource.ofCountsWithDepth 2 3 0 0 5
/-- Source-facing COLD score `(gateCount, depth, auxiliaryQubits, oracleCalls)`. -/
commit-pinned source · Verso Blueprint panel
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)'.
def mainCaseColdPartialPermCost : BlockEncodingCost :=
BlockEncodingCost.fromLayoutAndResource
mainCaseColdSourceLayout mainCaseColdHighLevelResource
commit-pinned source · Verso Blueprint panel
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.
theorem mainCaseColdPartialPermCost_gateCount :
mainCaseColdPartialPermCost.gateCount = 5 := rfl
commit-pinned source · Verso Blueprint panel
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.
theorem mainCaseColdPartialPermCost_depth :
mainCaseColdPartialPermCost.depth = 5 := rfl
commit-pinned source · Verso Blueprint panel
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.
theorem mainCaseColdPartialPermCost_auxiliaryQubits :
mainCaseColdPartialPermCost.auxiliaryQubits = 1 := rfl
commit-pinned source · Verso Blueprint panel
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.
theorem mainCaseColdPartialPermCost_oracleCalls :
mainCaseColdPartialPermCost.oracleCalls = 0 := rfl
commit-pinned source · Verso Blueprint panel
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.
theorem mainCaseColdPartialPermImage_injective_pointwise :
∀ x y : Fin 16,
mainCaseColdPartialPermImage x = mainCaseColdPartialPermImage y → x = y := by
commit-pinned source · Verso Blueprint panel
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.
theorem mainCaseColdPartialPermImage_injective :
Function.Injective mainCaseColdPartialPermImage := by
commit-pinned source · Verso Blueprint panel
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.
def mainCaseColdPartialPermPreimage : Fin 16 → Fin 16
| ⟨0, _⟩ => ⟨6, by decide⟩
| ⟨1, _⟩ => ⟨7, by decide⟩
| ⟨2, _⟩ => ⟨8, by decide⟩
| ⟨3, _⟩ => ⟨9, by decide⟩
| ⟨4, _⟩ => ⟨10, by decide⟩
| ⟨5, _⟩ => ⟨11, by decide⟩
| ⟨6, _⟩ => ⟨12, by decide⟩
| ⟨7, _⟩ => ⟨13, by decide⟩
| ⟨8, _⟩ => ⟨2, by decide⟩
| ⟨9, _⟩ => ⟨3, by decide⟩
commit-pinned source · Verso Blueprint panel
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.
theorem mainCaseColdPartialPermImage_preimage :
∀ y : Fin 16,
mainCaseColdPartialPermImage (mainCaseColdPartialPermPreimage y) = y := by
commit-pinned source · Verso Blueprint panel
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.
theorem mainCaseColdPartialPermImage_surjective :
Function.Surjective mainCaseColdPartialPermImage := by
commit-pinned source · Verso Blueprint panel
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'.
def mainCaseColdPartialPermImageIsPermutation : Prop :=
Function.Injective mainCaseColdPartialPermImage ∧
Function.Surjective mainCaseColdPartialPermImage
commit-pinned source · Verso Blueprint panel
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.
theorem mainCaseColdPartialPermImage_bijective :
mainCaseColdPartialPermImageIsPermutation :=
⟨mainCaseColdPartialPermImage_injective,
mainCaseColdPartialPermImage_surjective⟩
/-- Entrywise image calculation for the reusable partial-permutation wrapper. -/
commit-pinned source · Verso Blueprint panel
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.
theorem mainCaseColdPartialPerm_entry :
∀ row col : Fin 8,
(if mainCaseColdCleanEmbed row =
mainCaseColdPartialPermImage (mainCaseColdCleanEmbed col) then
1
else
0) =
mainCaseColdTarget row col := by
commit-pinned source · Verso Blueprint panel
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.
def mainCaseColdPartialPermExactCleanBlock :
BlockEncodingClassics.ExactCleanBlock 8 16 :=
BlockEncodingClassics.partialPermutationCertificate
mainCaseColdCleanEmbed
mainCaseColdPartialPermImage
mainCaseColdTarget
mainCaseColdPartialPerm_entry
commit-pinned source · Verso Blueprint panel
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.
theorem mainCaseColdPartialPerm_clean_eq_target :
Matrix.PointwiseEq
(BlockEncodingClassics.ExactCleanBlock.clean
mainCaseColdPartialPermExactCleanBlock)
mainCaseColdTarget :=
BlockEncodingClassics.ExactCleanBlock.clean_eq_target
mainCaseColdPartialPermExactCleanBlock
commit-pinned source · Verso Blueprint panel
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.
theorem mainCaseColdPartialPerm_blockProjection :
mainCaseColdBlockProjection mainCaseColdPartialPermMatrix := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “main case cold query target normalizer”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem mainCaseColdQueryTarget_normalizer :
mainCaseColdQueryTarget.normalizer = mainCaseColdExactNormalizer := rfl
commit-pinned source · Verso Blueprint panel
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.
theorem mainCaseColdSourceLayout_auxiliaryQubits :
mainCaseColdSourceLayout.auxiliaryQubits = 1 := rfl
/--
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.
-/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “main case cold resource schema obligation”. Resource-schema obligation for 'MAIN-RESOURCE-001'.
def mainCaseColdResourceSchemaObligation : SemanticObligation where
description :=
"COLD-local circuit/schedule and honest resource tuple are compiled as mainCaseColdCircuitImage_eq_partialPermImage and mainCaseColdPartialPermCost_*"
source := "QBE-MAIN-CASE-HIER-COLD-001, MAIN-RESOURCE-001"
proved := true
/--
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*`
commit-pinned source · Verso Blueprint panel
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.
def mainCaseColdPartialPermCandidate :
OperatorBlockEncodingCandidate Rat 3 where
auxiliaryQubits := 1
target := mainCaseColdQueryTarget
unitary := mainCaseColdPartialPermMatrix
layout := mainCaseColdSourceLayout
circuit := mainCaseColdCircuit
schedule := mainCaseColdSchedule
resource := mainCaseColdHighLevelResource
layoutMatches := mainCaseColdSourceLayout_auxiliaryQubits
isUnitary := mainCaseColdPartialPermImageIsPermutation
commit-pinned source · Verso Blueprint panel
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.
def mainCaseColdPartialPermVerified :
VerifiedOperatorBlockEncoding Rat 3 where
candidate := mainCaseColdPartialPermCandidate
unitaryProof := by
commit-pinned source · Verso Blueprint panel
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.
theorem mainCaseColdPartialPermCandidate_cost :
mainCaseColdPartialPermCandidate.cost =
{ auxiliaryQubits := 1, gateCount := 5, depth := 5, oracleCalls := 0 } := by
commit-pinned source · Verso Blueprint panel