This definition gives the library's named construction or computation for “absorb boundary”. Absorb the signed residual boundary into the actual first core.
noncomputable def absorbBoundary {n l r : ℕ} (u : Fin l → ℝ) :
Chain (n + 1) l r → Chain (n + 1) 1 r
| .cons A tail => .cons (boundaryRow u * A) tail
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “absorb boundary canonical”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem absorbBoundary_canonical {n l r : ℕ} (u : Fin l → ℝ) (hu : mass u = 1)
(D : Chain (n + 1) l r) (hD : RightCanonical D) :
RightCanonical (absorbBoundary u D) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “absorb boundary contract”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem absorbBoundary_contract {n l r : ℕ} (u : Fin l → ℝ)
(D : Chain (n + 1) l r) (x : Word (n + 1)) :
contract (absorbBoundary u D) x = boundaryRow u * contract D x := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “absorb boundary max bond”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem absorbBoundary_maxBond {n l r : ℕ} (u : Fin l → ℝ)
(D : Chain (n + 1) l r) : maxBond (absorbBoundary u D) ≤ max 1 (maxBond D) := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “unit boundary”. Concrete scalar-boundary canonical train, with no separate initialization circuit.
noncomputable def unitBoundary {n : ℕ} (C : Chain (n + 1) 1 1) : Chain (n + 1) 1 1 :=
absorbBoundary (ConstructiveTensorTrain.stateBoundary C)
(ConstructiveTensorTrain.canonicalize C).canonical
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “unit boundary canonical”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem unitBoundary_canonical {n : ℕ} (C : Chain (n + 1) 1 1)
(hNorm : (∑ x : Word (n + 1), (contract C x 0 0) ^ 2) = 1) :
RightCanonical (unitBoundary C) :=
absorbBoundary_canonical _ (ConstructiveTensorTrain.stateBoundary_normalized C hNorm)
_ (ConstructiveTensorTrain.canonicalize_rightCanonical C)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “unit boundary contract”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem unitBoundary_contract {n : ℕ} (C : Chain (n + 1) 1 1) (x : Word (n + 1)) :
contract (unitBoundary C) x 0 0 = contract C x 0 0 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “unit boundary max bond le”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem unitBoundary_maxBond_le {n : ℕ} (C : Chain (n + 1) 1 1) :
maxBond (unitBoundary C) ≤ maxBond C := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “stage”. Every local primitive list is computed from its actual completed SO matrix.
noncomputable def stage {n l r q : ℕ} (D : Chain n l r)
(hB : maxBond D ≤ 2 ^ q) (t : ℕ) : PrimitiveCircuit (q + 1) :=
GrayGivensCompiler.compileSO (ConstructiveIsometryLocal.completeStage D hB t)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “stage gate count”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem stage_gateCount {n l r q : ℕ} (D : Chain n l r)
(hB : maxBond D ≤ 2 ^ q) (t : ℕ) :
(stage D hB t).gateCount ≤ 6 * (2 ^ q) ^ 3 :=
(GrayGivensCompiler.compileSO_cubic_bound _).1
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “stage columns”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem stage_columns {n l r q : ℕ} (D : Chain n l r)
(hD : RightCanonical D) (hB : maxBond D ≤ 2 ^ q) (t : ℕ) (ht : t < n)
(bit : Fin 2) (b a : PrimitiveBasis q)
(ha : (primitiveBasisLEEquiv q a).val < rankAt D t) :
evalPrimitiveCircuit (stage D hB t) (Fin.snoc b bit) (Fin.snoc a 0) =
paddedAt D t (bit, primitiveBasisLEEquiv q b) (primitiveBasisLEEquiv q a) := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “compile”. Final physical circuit: data occupy the low wires, and the clean bond the high wires.
noncomputable def compile {n q : ℕ} (C : Chain (n + 1) 1 1)
(hB : maxBond C ≤ 2 ^ q) : PrimitiveCircuit ((n + 1) + q) :=
SequentialPrimitiveAssembly.publicCircuit []
(stage (unitBoundary C) ((unitBoundary_maxBond_le C).trans hB)) (n + 1)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “compile gate count”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem compile_gateCount {n q : ℕ} (C : Chain (n + 1) 1 1)
(hB : maxBond C ≤ 2 ^ q) :
(compile C hB).gateCount ≤ (n + 1) * (6 * (2 ^ q) ^ 3) :=
publicCircuit_gateCount_bound _ _ _ (fun t _ => stage_gateCount _ _ t)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “compile depth”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem compile_depth {n q : ℕ} (C : Chain (n + 1) 1 1)
(hB : maxBond C ≤ 2 ^ q) :
(compile C hB).resource.depth ≤ (n + 1) * (6 * (2 ^ q) ^ 3) :=
(compile C hB).resource_depth_le_gateCount.trans (compile_gateCount C hB)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “compile unitary”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem compile_unitary {n q : ℕ} (C : Chain (n + 1) 1 1)
(hB : maxBond C ≤ 2 ^ q) :
evalPrimitiveCircuit (compile C hB) ∈
_root_.Matrix.unitaryGroup (PrimitiveBasis ((n + 1) + q)) ℂ :=
evalPrimitiveCircuit_unitary _
/-- All data words and all bond sectors, including every non-clean output. -/
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “compile columns”; the hypotheses and conclusion in the code panel fix its exact scope. All data words and all bond sectors, including every non-clean output.
theorem compile_columns {n q : ℕ} (C : Chain (n + 1) 1 1)
(hB : maxBond C ≤ 2 ^ q)
(hNorm : (∑ x : Word (n + 1), (contract C x 0 0) ^ 2) = 1)
(x : PrimitiveBasis (n + 1)) (b : PrimitiveBasis q) :
evalPrimitiveCircuit (compile C hB) (Fin.append x b) (fun _ => 0) =
if b = (fun _ => 0) then
(contract C (wordOfBasis (fun i => x i.rev)) 0 0 : ℂ) else 0 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “compile word”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem compile_word {n q : ℕ} (C : Chain (n + 1) 1 1)
(hB : maxBond C ≤ 2 ^ q)
(hNorm : (∑ x : Word (n + 1), (contract C x 0 0) ^ 2) = 1)
(x : Word (n + 1)) (b : PrimitiveBasis q) :
evalPrimitiveCircuit (compile C hB)
(Fin.append (fun i => TensorTrainWord.toBasis x i.rev) b) (fun _ => 0) =
if b = (fun _ => 0) then (contract C x 0 0 : ℂ) else 0 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “compile spec”; the hypotheses and conclusion in the code panel fix its exact scope. Complete quantum correctness and resource certificate for the actual producer.
theorem compile_spec {n q : ℕ} (C : Chain (n + 1) 1 1)
(hB : maxBond C ≤ 2 ^ q)
(hNorm : (∑ x : Word (n + 1), (contract C x 0 0) ^ 2) = 1) :
(compile C hB).gateCount ≤ (n + 1) * (6 * (2 ^ q) ^ 3) ∧
(compile C hB).resource.depth ≤ (n + 1) * (6 * (2 ^ q) ^ 3) ∧
(compile C hB).resource.oracleCalls = 0 ∧
evalPrimitiveCircuit (compile C hB) ∈
_root_.Matrix.unitaryGroup (PrimitiveBasis ((n + 1) + q)) ℂ ∧
∀ (x : PrimitiveBasis (n + 1)) (b : PrimitiveBasis q),
evalPrimitiveCircuit (compile C hB) (Fin.append x b) (fun _ => 0) =
if b = (fun _ => 0) then
commit-pinned source · Verso Blueprint panel