QuantumBlockEncoding/GrayGivensCompiler.lean

Lean checks the proposition indexed as “bit eq or flip”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem bit_eq_or_flip (a b : Fin 2) : a = b ∨ a = flipBit b := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “x context”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem x_context {n : ℕ} (target : Fin n) (bits : PrimitiveBasis n) :
    (splitPrimitiveWire target (xBasisAction target bits)).2 =
      (splitPrimitiveWire target bits).2 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “same context iff”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem same_context_iff {n : ℕ} (target : Fin n) (a b : PrimitiveBasis n) :
    (splitPrimitiveWire target a).2 = (splitPrimitiveWire target b).2 ↔
      a = b ∨ a = xBasisAction target b := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “controls equiv”.

noncomputable def controlsEquiv {q : ℕ} (target : Fin (q + 1)) :
    Fin q ≃ OtherPrimitiveWires target :=
  Fintype.equivOfCardEq (by
    simp [OtherPrimitiveWires, Fintype.card_subtype_compl])

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “real transport”.

noncomputable def realTransport {N n : ℕ} (basis : Fin N ≃ PrimitiveBasis n) :
    _root_.Matrix (Fin N) (Fin N) ℝ ≃ₐ[ℝ]
      _root_.Matrix (PrimitiveBasis n) (PrimitiveBasis n) ℝ :=
  _root_.Matrix.reindexAlgEquiv ℝ ℝ basis

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “transport”.

noncomputable def transport {N n : ℕ} (basis : Fin N ≃ PrimitiveBasis n) :
    _root_.Matrix (Fin N) (Fin N) ℝ →+*
      _root_.Matrix (PrimitiveBasis n) (PrimitiveBasis n) ℂ :=
  Complex.ofRealHom.mapMatrix.comp (realTransport basis).toRingHom

set_option maxHeartbeats 600000 in

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “edge plane transport”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem edge_plane_transport {N n : ℕ} (basis : Fin N ≃ PrimitiveBasis n)
    (first second : Fin N) (distinct : first ≠ second) (target : Fin n)
    (action : basis second = xBasisAction target (basis first)) (theta : ℝ) :
    realTransport basis (planeMatrix first second theta) =
      selectedRyPlaneMatrix target (splitPrimitiveWire target (basis first)).2
        (if basis first target = 0 then theta else -theta) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “step target”.

noncomputable def stepTarget {q : ℕ} (step : AdjacentGivens.Step (2 ^ (q + 1))) : Fin (q + 1) :=
  Classical.choose (GrayBasis.adjacent step.first step.second step.adjacent)

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “step target action”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem stepTarget_action {q : ℕ} (step : AdjacentGivens.Step (2 ^ (q + 1))) :
    GrayBasis.equiv (q + 1) step.second =
      xBasisAction (stepTarget step) (GrayBasis.equiv (q + 1) step.first) :=
  Classical.choose_spec (GrayBasis.adjacent step.first step.second step.adjacent)

/-- One actual selected-rotation instruction. Reversed target-bit order negates
the RY angle, while every non-target wire is an explicit control. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “selected step”. One actual selected-rotation instruction.

noncomputable def selectedStep {q : ℕ} (step : AdjacentGivens.Step (2 ^ (q + 1))) :
    SelectedRyStep (q + 1) q where
  target := stepTarget step
  wires := fun i => (controlsEquiv (stepTarget step) i).val
  distinct := fun i => (controlsEquiv (stepTarget step) i).property
  chosen := fun i => GrayBasis.equiv (q + 1) step.first (controlsEquiv (stepTarget step) i).val
  angle := .real (if GrayBasis.equiv (q + 1) step.first (stepTarget step) = 0
    then step.angle else -step.angle)

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “selected step matrix”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem selectedStep_matrix {q : ℕ} (step : AdjacentGivens.Step (2 ^ (q + 1))) :
    (selectedStep step).matrix = transport (GrayBasis.equiv (q + 1)) step.matrix := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “compile steps”.

noncomputable def compileSteps {q : ℕ} (steps : List (AdjacentGivens.Step (2 ^ (q + 1)))) :
    PrimitiveCircuit (q + 1) := compileSelectedRySteps (steps.map selectedStep)

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “compile steps eval”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem compileSteps_eval {q : ℕ} (steps : List (AdjacentGivens.Step (2 ^ (q + 1)))) :
    evalPrimitiveCircuit (compileSteps steps) =
      transport (GrayBasis.equiv (q + 1)) (AdjacentGivens.stepsMatrix steps) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “compile steps gate count”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem compileSteps_gateCount {q : ℕ} (steps : List (AdjacentGivens.Step (2 ^ (q + 1)))) :
    (compileSteps steps).gateCount = steps.length * (2 ^ q + 2 * (2 ^ q - 1)) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “compile so gray”. Input coordinates here are Gray-ordered natural indices.

noncomputable def compileSOGray {q : ℕ}
    (A : _root_.Matrix (Fin (2 ^ (q + 1))) (Fin (2 ^ (q + 1))) ℝ) : PrimitiveCircuit (q + 1) :=
  compileSteps (decomposeSO A)

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “compile so gray eval”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem compileSOGray_eval {q : ℕ}
    (A : _root_.Matrix (Fin (2 ^ (q + 1))) (Fin (2 ^ (q + 1))) ℝ)
    (orthogonal : A.transpose * A = 1) (determinant : A.det = 1) :
    evalPrimitiveCircuit (compileSOGray A) = transport (GrayBasis.equiv (q + 1)) A := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “compile so gray cubic bound”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem compileSOGray_cubic_bound {q : ℕ}
    (A : _root_.Matrix (Fin (2 ^ (q + 1))) (Fin (2 ^ (q + 1))) ℝ) :
    (compileSOGray A).gateCount ≤ 6 * (2 ^ q) ^ 3 ∧
    (compileSOGray A).resource.oracleCalls = 0 := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “gray coordinates”.

noncomputable def grayCoordinates {q : ℕ}
    (A : _root_.Matrix (PrimitiveBasis (q + 1)) (PrimitiveBasis (q + 1)) ℝ) :
    _root_.Matrix (Fin (2 ^ (q + 1))) (Fin (2 ^ (q + 1))) ℝ :=
  _root_.Matrix.reindexAlgEquiv ℝ ℝ (GrayBasis.equiv (q + 1)).symm A

/-- A circuit on the original named wires; Gray order is internal only. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “compile so”. A circuit on the original named wires; Gray order is internal only.

noncomputable def compileSO {q : ℕ}
    (A : _root_.Matrix (PrimitiveBasis (q + 1)) (PrimitiveBasis (q + 1)) ℝ) :
    PrimitiveCircuit (q + 1) := compileSOGray (grayCoordinates A)

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “gray coordinates orthogonal”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem grayCoordinates_orthogonal {q : ℕ}
    (A : _root_.Matrix (PrimitiveBasis (q + 1)) (PrimitiveBasis (q + 1)) ℝ)
    (orthogonal : A.transpose * A = 1) :
    (grayCoordinates A).transpose * grayCoordinates A = 1 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “gray coordinates det”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem grayCoordinates_det {q : ℕ}
    (A : _root_.Matrix (PrimitiveBasis (q + 1)) (PrimitiveBasis (q + 1)) ℝ) :
    (grayCoordinates A).det = A.det := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “compile so eval”; the hypotheses and conclusion in the code panel fix its exact scope. No assumed plane realization or Gray adjacency: the actual finite primitive list realizes the original real SO matrix embedded in complex amplitudes.

theorem compileSO_eval {q : ℕ}
    (A : _root_.Matrix (PrimitiveBasis (q + 1)) (PrimitiveBasis (q + 1)) ℝ)
    (orthogonal : A.transpose * A = 1) (determinant : A.det = 1) :
    evalPrimitiveCircuit (compileSO A) = A.map Complex.ofReal := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “compile so cubic bound”; the hypotheses and conclusion in the code panel fix its exact scope. With 'S=2^q', the exact recursive selected-RY backend needs at most '6*S^3' primitive gates and no oracle calls, on the existing 'q+1' wires.

theorem compileSO_cubic_bound {q : ℕ}
    (A : _root_.Matrix (PrimitiveBasis (q + 1)) (PrimitiveBasis (q + 1)) ℝ) :
    (compileSO A).gateCount ≤ 6 * (2 ^ q) ^ 3 ∧ (compileSO A).resource.oracleCalls = 0 :=
  compileSOGray_cubic_bound (grayCoordinates A)

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “compile so gate count”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem compileSO_gateCount {q : ℕ}
    (A : _root_.Matrix (PrimitiveBasis (q + 1)) (PrimitiveBasis (q + 1)) ℝ) :
    (compileSO A).gateCount =
      (2 ^ (q + 1) * (2 ^ (q + 1) - 1) / 2) * (2 ^ q + 2 * (2 ^ q - 1)) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “compile so ry count”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem compileSO_ryCount {q : ℕ}
    (A : _root_.Matrix (PrimitiveBasis (q + 1)) (PrimitiveBasis (q + 1)) ℝ) :
    (compileSO A).ryCount = (2 ^ (q + 1) * (2 ^ (q + 1) - 1) / 2) * 2 ^ q := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “compile so cx count”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem compileSO_cxCount {q : ℕ}
    (A : _root_.Matrix (PrimitiveBasis (q + 1)) (PrimitiveBasis (q + 1)) ℝ) :
    (compileSO A).cxCount =
      (2 ^ (q + 1) * (2 ^ (q + 1) - 1) / 2) * (2 * (2 ^ q - 1)) := by

commit-pinned source · Verso Blueprint panel