QuantumBlockEncoding/CubicStatePreparation.lean

This definition gives the library's named construction or computation for “task id”. Task identifier used by the retrieval and verifier ledgers.

def taskId : String := "QBE-OP-CUBIC-STATEPREP-001"

/-- User-requested error tolerance `1e-10`. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “requested epsilon”. User-requested error tolerance '1e-10'.

def requestedEpsilon : Rat := (1 : Rat) / 10000000000

/-- Grid point `x_j = j / 2^n`. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “grid point”. Grid point 'x_j = j / 2^n'.

def gridPoint (n : Nat) (j : Fin (gridSize n)) : Rat :=
  (j.val : Rat) / (gridSize n : Rat)

/-- Cubic amplitude `f(x_j) = x_j^3`. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “cubic amplitude”. Cubic amplitude 'f(x_j) = x_j^3'.

def cubicAmplitude (n : Nat) (j : Fin (gridSize n)) : Rat :=
  (gridPoint n j) ^ 3

/--
The rank-one operator `O_n = |v_n><0^n|`.  In column-vector convention this
maps the input basis state `|0^n>` to the unnormalized vector with entries
`(j / 2^n)^3`, and maps every other input basis state to zero.
-/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “cubic operator”. The rank-one operator 'O_n = |v_n><0^n|'.

def cubicOperator (n : Nat) : Matrix (gridSize n) (gridSize n) Rat :=
  fun row col => if col.val = 0 then cubicAmplitude n row else 0

/--
Exact rational squared norm of the unnormalized target vector.  The analytic
normalizer is its square root; this rational quantity is the cheap diagnostic
used before any approximate rotation-synthesis route is accepted.
-/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “cubic norm sq”. Exact rational squared norm of the unnormalized target vector.

def cubicNormSq (n : Nat) : Rat :=
  (List.finRange (gridSize n)).foldl
    (fun acc j => acc + cubicAmplitude n j ^ 2) 0

/--
A conservative rational normalizer.  It is not intended to be optimal; it is a
stable placeholder until the approximate synthesis backend proves a sharper
normalizer and error bound.
-/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “conservative normalizer”. A conservative rational normalizer.

def conservativeNormalizer (n : Nat) : Rat :=
  (gridSize n : Rat)

/-- Operator-first target record used by the ABEIS harness. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “cubic target”. Operator-first target record used by the ABEIS harness.

def cubicTarget (n : Nat) : QueryOperatorTarget Rat (gridSize n) (gridSize n) where
  operator := cubicOperator n
  normalizer := conservativeNormalizer n
  source := "QBE-OP-CUBIC-STATEPREP-001: O_n = |v_n><0^n|, v_j=(j/2^n)^3"
  semanticContract :=
    "rank-one unnormalized cubic grid state-preparation operator; approximate BE target epsilon=1e-10"
  freeParameters := [
    "n positive",
    "epsilon = 1e-10",
    "exact search first, then Scenario 2 approximate arithmetic synthesis"
  ]

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “default required cost”. Resource floor used for the first Scenario 2 run.

def defaultRequiredCost : BlockEncodingCost where
  auxiliaryQubits := 4
  gateCount := 0
  depth := 0
  oracleCalls := 0

/--
Adaptive search policy for the cubic benchmark.  The zero gate/depth fields in
`defaultRequiredCost` deliberately mean "discover a concrete candidate and then
rank it"; the active search is expected to relax from exact to approximate
construction after a small exact-search stall window.

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “default policy”. Adaptive search policy for the cubic benchmark.

def defaultPolicy : AdaptiveBlockEncodingPolicy Rat where
  maxExactIterations := 2
  exactStallIterations := 1
  requiredCost := defaultRequiredCost
  requestedEpsilon := requestedEpsilon
  allowRelaxedEpsilon := true
  maxUpperAgents := 4
  maxMiddleAgents := 5
  maxLowerAgents := 8

/-- First arithmetic-route precision seed for Scenario 2. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “arithmetic cubic default precision”. First arithmetic-route precision seed for Scenario 2.

def arithmeticCubicDefaultPrecision : Nat := 40

/--
Register layout for the first arithmetic-transduction candidate route.

The single signal qubit is the clean block selector.  The pure workspace keeps
an address copy, reversible square/cube work registers, and fixed-point
precision workspace.  This is a candidate interface only; it does not certify
the arithmetic or rotation subroutines.
-/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “arithmetic cubic layout”. Register layout for the first arithmetic-transduction candidate route.

def arithmeticCubicLayout (n precision : Nat) : RegisterLayout where
  systemQubits := n
  signalQubits := 1
  pureAncillas := 3 * n + precision + 2

/--
Oracle-level transcript for the scalable cubic route.

The clean branch is intended to compute `j / 2^n`, reversibly form the cubic
fixed-point amplitude, apply one amplitude-transduction rotation, and uncompute
the arithmetic workspace.  Each label remains a semantic proof obligation.

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “arithmetic cubic circuit”. Oracle-level transcript for the scalable cubic route.

def arithmeticCubicCircuit (_n _precision : Nat) : Circuit :=
  [ Gate.oracleCall "cubic-load-j-over-2^n"
  , Gate.oracleCall "cubic-square-fixed-point"
  , Gate.oracleCall "cubic-multiply-by-x"
  , Gate.oracleCall "cubic-amplitude-transduction-Ry"
  , Gate.oracleCall "(cubic-multiply-by-x)^dagger"
  , Gate.oracleCall "(cubic-square-fixed-point)^dagger"
  , Gate.oracleCall "(cubic-load-j-over-2^n)^dagger"
  ]

/-- Local resource count for the unexpanded oracle-level transcript. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “arithmetic cubic resource”. Local resource count for the unexpanded oracle-level transcript.

def arithmeticCubicResource (n precision : Nat) : Resource :=
  (arithmeticCubicCircuit n precision).resource

/-- Normalizer used by the first arithmetic-transduction route. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “arithmetic cubic normalizer”. Normalizer used by the first arithmetic-transduction route.

def arithmeticCubicNormalizer (n : Nat) : Rat :=
  conservativeNormalizer n

/-- Candidate score extracted from the arithmetic-route layout and transcript. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “arithmetic cubic cost”. Candidate score extracted from the arithmetic-route layout and transcript.

def arithmeticCubicCost (n precision : Nat) : BlockEncodingCost :=
  BlockEncodingCost.fromLayoutAndResource
    (arithmeticCubicLayout n precision)
    (arithmeticCubicResource n precision)

/-- Resource tuple in QBE candidate-population order. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “arithmetic cubic resource tuple”. Resource tuple in QBE candidate-population order.

def arithmeticCubicResourceTuple (n precision : Nat) : Nat × Nat × Nat × Nat :=
  ( (arithmeticCubicCost n precision).gateCount
  , (arithmeticCubicCost n precision).depth
  , (arithmeticCubicCost n precision).auxiliaryQubits
  , (arithmeticCubicCost n precision).oracleCalls
  )

/-- The oracle-level transcript has seven unresolved calls and depth seven. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “arithmetic cubic resource eq”; the hypotheses and conclusion in the code panel fix its exact scope. The oracle-level transcript has seven unresolved calls and depth seven.

theorem arithmeticCubicResource_eq (n precision : Nat) :
    arithmeticCubicResource n precision =
      Resource.ofCountsWithDepth 0 0 7 0 7 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “arithmetic cubic layout auxiliary qubits”; the hypotheses and conclusion in the code panel fix its exact scope. The first arithmetic route records one signal qubit plus pure workspace.

theorem arithmeticCubicLayout_auxiliaryQubits (n precision : Nat) :
    (arithmeticCubicLayout n precision).auxiliaryQubits =
      1 + (3 * n + precision + 2) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “arithmetic cubic claim”. Human-facing construction claim for the first scalable route.

def arithmeticCubicClaim : ConstructionClaim where
  name := "arithmetic-cubic-amplitude-transduction"
  source := "QBE-OP-CUBIC-STATEPREP-001 exploratory candidate CUBIC-CAND-001"
  target := "O_n = |v_n><0^n|, v_n[j] = (j / 2^n)^3"
  normalization := "alpha = conservativeNormalizer n"
  layout := "one signal qubit plus 3*n + precision + 2 pure arithmetic ancillas"
  resource := {
    gates :=
      CostExpr.atom "poly(n, precision)" +
      CostExpr.atom "rotation_synthesis(precision)"
    pureAncilla :=

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “arithmetic rank one cubic layout”. Rank-one wrapper layout for the arithmetic cubic route.

def arithmeticRankOneCubicLayout (n precision : Nat) : RegisterLayout where
  systemQubits := n
  signalQubits := 1
  pureAncillas := (arithmeticCubicLayout n precision).pureAncillas + n + 1

/--
Rank-one candidate transcript around the arithmetic middle block.

The first two calls are the missing wrapper from `CUBIC-CAND-SHAPE-001`: reject
nonzero input columns from the clean branch, then generate the output row
register on the zero-input branch.  The final call is a placeholder cleanup for

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “arithmetic rank one cubic circuit”. Rank-one candidate transcript around the arithmetic middle block.

def arithmeticRankOneCubicCircuit (n precision : Nat) : Circuit :=
  [ Gate.oracleCall "rank-one-zero-input-clean-filter"
  , Gate.oracleCall "rank-one-row-generation-on-zero-input"
  ] ++
  arithmeticCubicCircuit n precision ++
  [ Gate.oracleCall "rank-one-zero-input-filter-cleanup" ]

/-- Oracle-level resource count for the rank-one wrapped transcript. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “arithmetic rank one cubic resource”. Oracle-level resource count for the rank-one wrapped transcript.

def arithmeticRankOneCubicResource (n precision : Nat) : Resource :=
  (arithmeticRankOneCubicCircuit n precision).resource

/-- Normalizer used by the rank-one wrapped arithmetic route. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “arithmetic rank one cubic normalizer”. Normalizer used by the rank-one wrapped arithmetic route.

def arithmeticRankOneCubicNormalizer (n : Nat) : Rat :=
  arithmeticCubicNormalizer n

/-- Candidate score for the rank-one wrapped arithmetic route. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “arithmetic rank one cubic cost”. Candidate score for the rank-one wrapped arithmetic route.

def arithmeticRankOneCubicCost (n precision : Nat) : BlockEncodingCost :=
  BlockEncodingCost.fromLayoutAndResource
    (arithmeticRankOneCubicLayout n precision)
    (arithmeticRankOneCubicResource n precision)

/-- Resource tuple in QBE candidate-population order for the wrapped route. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “arithmetic rank one cubic resource tuple”. Resource tuple in QBE candidate-population order for the wrapped route.

def arithmeticRankOneCubicResourceTuple (n precision : Nat) :
    Nat × Nat × Nat × Nat :=
  ( (arithmeticRankOneCubicCost n precision).gateCount
  , (arithmeticRankOneCubicCost n precision).depth
  , (arithmeticRankOneCubicCost n precision).auxiliaryQubits
  , (arithmeticRankOneCubicCost n precision).oracleCalls
  )

/-- The rank-one wrapper adds three oracle-level calls to the middle block. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “arithmetic rank one cubic resource eq”; the hypotheses and conclusion in the code panel fix its exact scope. The rank-one wrapper adds three oracle-level calls to the middle block.

theorem arithmeticRankOneCubicResource_eq (n precision : Nat) :
    arithmeticRankOneCubicResource n precision =
      Resource.ofCountsWithDepth 0 0 10 0 10 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “arithmetic rank one cubic layout auxiliary qubits”; the hypotheses and conclusion in the code panel fix its exact scope. Auxiliary qubits for the wrapped route include the zero-test workspace.

theorem arithmeticRankOneCubicLayout_auxiliaryQubits (n precision : Nat) :
    (arithmeticRankOneCubicLayout n precision).auxiliaryQubits =
      1 + ((arithmeticCubicLayout n precision).pureAncillas + n + 1) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “arithmetic rank one cubic resource tuple n 2 default”; the hypotheses and conclusion in the code panel fix its exact scope. Default small diagnostic score for the wrapped route at 'n = 2', 'p = 40'.

theorem arithmeticRankOneCubicResourceTuple_n2_default :
    arithmeticRankOneCubicResourceTuple 2 arithmeticCubicDefaultPrecision =
      (10, 10, 52, 10) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “arithmetic rank one cubic claim”. Human-facing construction claim for the rank-one wrapped scalable route.

def arithmeticRankOneCubicClaim : ConstructionClaim where
  name := "rank-one-arithmetic-cubic-amplitude-transduction"
  source := "QBE-OP-CUBIC-STATEPREP-001 exploratory candidate CUBIC-CAND-SHAPE-001"
  target := "O_n = |v_n><0^n|, v_n[j] = (j / 2^n)^3"
  normalization := "alpha = conservativeNormalizer n"
  layout := "one signal qubit plus arithmetic workspace, zero-input filter, and row-generation workspace"
  resource := {
    gates :=
      CostExpr.atom "zero_input_filter(n)" +
      CostExpr.atom "row_generation(n, precision)" +
      CostExpr.atom "poly(n, precision)" +

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “hadamard counting cubic workspace”. Workspace seed for the Hadamard-counting mutation.

def hadamardCountingCubicWorkspace (n : Nat) : Nat :=
  4 * n + 3

/--
Register layout for the exact Hadamard-counting candidate.

The signal qubit is the reject flag.  Pure ancillas are the nonzero-input flag,
the `R,T` path registers of total width `4*n`, and the reversible
cube/comparator workspace.  Nonzero input columns set the reject signal before
the `nz` cleanup, so the clean projection cannot leak identity entries.
-/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “hadamard counting cubic layout”. Register layout for the exact Hadamard-counting candidate.

def hadamardCountingCubicLayout (n : Nat) : RegisterLayout where
  systemQubits := n
  signalQubits := 1
  pureAncillas := 1 + 4 * n + hadamardCountingCubicWorkspace n

/--
Oracle-level transcript for the Hadamard-counting route.

The row XOR is not uncomputed, because it writes the output system row for the
rank-one operator.  The separate nonzero-column reject signal is applied before
the `nz` cleanup, so nonzero input columns keep a clean-projection rejection

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “hadamard counting cubic circuit”. Oracle-level transcript for the Hadamard-counting route.

def hadamardCountingCubicCircuit (_n : Nat) : Circuit :=
  [ Gate.oracleCall "hcount-zero-input-flag"
  , Gate.oracleCall "hcount-nonzero-column-reject"
  , Gate.oracleCall "hcount-path-H-on-R-T"
  , Gate.oracleCall "hcount-row-xor-R-into-system"
  , Gate.oracleCall "hcount-cubic-threshold-compare"
  , Gate.oracleCall "(hcount-cubic-threshold-compare)^dagger"
  , Gate.oracleCall "hcount-path-H-on-R-T"
  , Gate.oracleCall "(hcount-zero-input-flag)^dagger"
  ]

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “hadamard counting cubic circuit reject signal repair”; the hypotheses and conclusion in the code panel fix its exact scope. The repaired transcript records a separate nonzero-column reject signal before the final 'nz' cleanup.

theorem hadamardCountingCubicCircuit_rejectSignalRepair (n : Nat) :
    hadamardCountingCubicCircuit n =
      [ Gate.oracleCall "hcount-zero-input-flag"
      , Gate.oracleCall "hcount-nonzero-column-reject"
      , Gate.oracleCall "hcount-path-H-on-R-T"
      , Gate.oracleCall "hcount-row-xor-R-into-system"
      , Gate.oracleCall "hcount-cubic-threshold-compare"
      , Gate.oracleCall "(hcount-cubic-threshold-compare)^dagger"
      , Gate.oracleCall "hcount-path-H-on-R-T"
      , Gate.oracleCall "(hcount-zero-input-flag)^dagger"
      ] := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “hadamard counting cubic resource”. Oracle-level resource count for the Hadamard-counting route.

def hadamardCountingCubicResource (n : Nat) : Resource :=
  (hadamardCountingCubicCircuit n).resource

/-- Normalizer used by the Hadamard-counting route. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “hadamard counting cubic normalizer”. Normalizer used by the Hadamard-counting route.

def hadamardCountingCubicNormalizer (n : Nat) : Rat :=
  conservativeNormalizer n

/-- Candidate score for the Hadamard-counting route. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “hadamard counting cubic cost”. Candidate score for the Hadamard-counting route.

def hadamardCountingCubicCost (n : Nat) : BlockEncodingCost :=
  BlockEncodingCost.fromLayoutAndResource
    (hadamardCountingCubicLayout n)
    (hadamardCountingCubicResource n)

/-- Resource tuple in QBE candidate-population order. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “hadamard counting cubic resource tuple”. Resource tuple in QBE candidate-population order.

def hadamardCountingCubicResourceTuple (n : Nat) : Nat × Nat × Nat × Nat :=
  ( (hadamardCountingCubicCost n).gateCount
  , (hadamardCountingCubicCost n).depth
  , (hadamardCountingCubicCost n).auxiliaryQubits
  , (hadamardCountingCubicCost n).oracleCalls
  )

/-- The Hadamard-counting interface has eight unresolved oracle-level calls. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “hadamard counting cubic resource eq”; the hypotheses and conclusion in the code panel fix its exact scope. The Hadamard-counting interface has eight unresolved oracle-level calls.

theorem hadamardCountingCubicResource_eq (n : Nat) :
    hadamardCountingCubicResource n =
      Resource.ofCountsWithDepth 0 0 8 0 8 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “hadamard counting cubic layout auxiliary qubits”; the hypotheses and conclusion in the code panel fix its exact scope. Auxiliary qubits for the counting route include reject, 'nz', path, and workspace registers.

theorem hadamardCountingCubicLayout_auxiliaryQubits (n : Nat) :
    (hadamardCountingCubicLayout n).auxiliaryQubits =
      1 + (1 + 4 * n + hadamardCountingCubicWorkspace n) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “hadamard counting cubic resource tuple n 2”; the hypotheses and conclusion in the code panel fix its exact scope. Default small diagnostic score for the counting route at 'n = 2'.

theorem hadamardCountingCubicResourceTuple_n2 :
    hadamardCountingCubicResourceTuple 2 = (8, 8, 21, 8) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “hadamard counting cubic claim”. Human-facing construction claim for the Hadamard-counting exact route.

def hadamardCountingCubicClaim : ConstructionClaim where
  name := "hadamard-counting-cubic-rank-one"
  source := "QBE-OP-CUBIC-STATEPREP-001 exploratory candidate CUBIC-HCOUNT-IFACE-001"
  target := "O_n = |v_n><0^n|, v_n[j] = (j / 2^n)^3"
  normalization := "alpha = conservativeNormalizer n"
  layout := "one reject signal qubit plus nz flag, 4*n path qubits, and reversible cube/comparator workspace"
  resource := {
    gates :=
      CostExpr.atom "path_hadamards(4*n)" +
      CostExpr.atom "zero_input_test(n)" +
      CostExpr.atom "nonzero_column_reject(n)" +

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “hard mode upper agent schedule”. Hard Mode panel escalation schedule.

def hardModeUpperAgentSchedule : List Nat := [1, 2, 3, 4]

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “hard mode middle agent schedule”.

def hardModeMiddleAgentSchedule : List Nat := [1, 2, 3, 4]

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “hard mode lower agent schedule”.

def hardModeLowerAgentSchedule : List Nat := [3, 4, 5, 6]

/-- Number of consecutive cycles without a closed leaf before the first escalation. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “hard mode exact stall window”. Number of consecutive cycles without a closed leaf before the first escalation.

def hardModeExactStallWindow : Nat := 1

/--
Number of consecutive cycles without an improving certified or finite
candidate before the next Hard Mode level is considered.
-/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “hard mode construction stall window”. Number of consecutive cycles without an improving certified or finite candidate before the next Hard Mode level is considered.

def hardModeConstructionStallWindow : Nat := 1

/-- Per-level cycle budgets before the upper panel must explicitly review progress. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “hard mode level cycle budget”. Per-level cycle budgets before the upper panel must explicitly review progress.

def hardModeLevelCycleBudget : List Nat := [1, 1, 1, 1]

/--
Scenario 2 epsilon ladder.  The first entry is the user-requested tolerance.
Later entries are relaxed exploratory waypoints used only if the exact or
requested-epsilon search stalls; a relaxed waypoint is not a substitute for a
certificate at `requestedEpsilon`.
-/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “relaxed epsilon ladder”. Scenario 2 epsilon ladder.

def relaxedEpsilonLadder : List Rat :=
  [requestedEpsilon, (1 : Rat) / 100000000, (1 : Rat) / 1000000]

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “relaxed epsilon ladder starts with requested”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem relaxedEpsilonLadder_startsWithRequested :
    relaxedEpsilonLadder.head? = some requestedEpsilon := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “hard mode schedules have four levels”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem hardModeSchedules_have_four_levels :
    hardModeUpperAgentSchedule.length = 4 ∧
    hardModeMiddleAgentSchedule.length = 4 ∧
    hardModeLowerAgentSchedule.length = 4 ∧
    hardModeLevelCycleBudget.length = 4 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “hard mode lower agent schedule final”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem hardModeLowerAgentSchedule_final :
    hardModeLowerAgentSchedule.getLast? = some 6 := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “initial expected phase”. Current expected phase.

def initialExpectedPhase : BlockEncodingSearchPhase :=
  BlockEncodingSearchPhase.relaxedApproxSearch

commit-pinned source · Verso Blueprint panel

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

theorem gridSize_pos (n : Nat) : 0 < gridSize n := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “cubic operator first column”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem cubicOperator_first_column (n : Nat) (row : Fin (gridSize n)) :
    cubicOperator n row ⟨0, gridSize_pos n⟩ = cubicAmplitude n row := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “cubic operator only first column”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem cubicOperator_only_first_column (n : Nat)
    (row col : Fin (gridSize n)) (h : col.val ≠ 0) :
    cubicOperator n row col = 0 := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “rank one clean block contract”. Entrywise clean-block contract for a rank-one cubic candidate.

def rankOneCleanBlockContract (n : Nat) (alpha : Rat)
    (block : Matrix (gridSize n) (gridSize n) Rat) : Prop :=
  (∀ row : Fin (gridSize n),
      alpha * block row ⟨0, gridSize_pos n⟩ = cubicAmplitude n row) ∧
  (∀ row col : Fin (gridSize n), col.val ≠ 0 → block row col = 0)

/-- Candidate-specific clean-block contract for the repaired rank-one route. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “arithmetic rank one cubic clean block contract”. Candidate-specific clean-block contract for the repaired rank-one route.

def arithmeticRankOneCubicCleanBlockContract (n : Nat)
    (block : Matrix (gridSize n) (gridSize n) Rat) : Prop :=
  rankOneCleanBlockContract n (arithmeticRankOneCubicNormalizer n) block

/--
The rank-one clean-block contract is exactly the target matrix, entry by entry,
after multiplying by its normalizer.
-/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “rank one clean block contract pointwise eq”; the hypotheses and conclusion in the code panel fix its exact scope. The rank-one clean-block contract is exactly the target matrix, entry by entry, after multiplying by its normalizer.

theorem rankOneCleanBlockContract_pointwise_eq {n : Nat} {alpha : Rat}
    {block : Matrix (gridSize n) (gridSize n) Rat}
    (h : rankOneCleanBlockContract n alpha block) :
    Matrix.PointwiseEq
      (fun row col => alpha * block row col)
      (cubicOperator n) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “arithmetic rank one cubic clean block contract pointwise eq”; the hypotheses and conclusion in the code panel fix its exact scope. Candidate-specific bridge from the repaired wrapper's clean-block contract to the fixed cubic target.

theorem arithmeticRankOneCubicCleanBlockContract_pointwise_eq {n : Nat}
    {block : Matrix (gridSize n) (gridSize n) Rat}
    (h : arithmeticRankOneCubicCleanBlockContract n block) :
    Matrix.PointwiseEq
      (fun row col => arithmeticRankOneCubicNormalizer n * block row col)
      (cubicOperator n) :=
  rankOneCleanBlockContract_pointwise_eq h

/-- Candidate-specific clean-block contract for the Hadamard-counting route. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “hadamard counting cubic clean block contract”. Candidate-specific clean-block contract for the Hadamard-counting route.

def hadamardCountingCubicCleanBlockContract (n : Nat)
    (block : Matrix (gridSize n) (gridSize n) Rat) : Prop :=
  rankOneCleanBlockContract n (hadamardCountingCubicNormalizer n) block

/--
Candidate-specific bridge from the Hadamard-counting clean-block contract to
the fixed cubic target.
-/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “hadamard counting cubic clean block contract pointwise eq”; the hypotheses and conclusion in the code panel fix its exact scope. Candidate-specific bridge from the Hadamard-counting clean-block contract to the fixed cubic target.

theorem hadamardCountingCubicCleanBlockContract_pointwise_eq {n : Nat}
    {block : Matrix (gridSize n) (gridSize n) Rat}
    (h : hadamardCountingCubicCleanBlockContract n block) :
    Matrix.PointwiseEq
      (fun row col => hadamardCountingCubicNormalizer n * block row col)
      (cubicOperator n) :=
  rankOneCleanBlockContract_pointwise_eq h

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “rat cube sq eq sixth”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem rat_cube_sq_eq_sixth (x : Rat) : (x ^ 3) ^ 2 = x ^ 6 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “cubic amplitude sq eq grid point sixth”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem cubicAmplitude_sq_eq_gridPoint_sixth (n : Nat)
    (j : Fin (gridSize n)) :
    cubicAmplitude n j ^ 2 = gridPoint n j ^ 6 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “cubic norm sq sixth power fold”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem cubicNormSq_sixthPowerFold (n : Nat) :
    cubicNormSq n =
      (List.finRange (gridSize n)).foldl
        (fun acc j => acc + gridPoint n j ^ 6) 0 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “grid size rat ne zero”; the hypotheses and conclusion in the code panel fix its exact scope. The rational grid dimension is nonzero, for denominator side conditions.

theorem gridSize_rat_ne_zero (n : Nat) : (gridSize n : Rat) ≠ 0 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “grid size rat pos”; the hypotheses and conclusion in the code panel fix its exact scope. The rational grid dimension is positive.

theorem gridSize_rat_pos (n : Nat) : (0 : Rat) < (gridSize n : Rat) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “rat div cube div eq”; the hypotheses and conclusion in the code panel fix its exact scope. Core rational normalization for the Hadamard-counting path ratio.

theorem rat_div_cube_div_eq (a b : Rat) :
    (a / b) ^ 3 / b = a ^ 3 / b ^ 4 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “cubic amplitude div conservative normalizer eq”; the hypotheses and conclusion in the code panel fix its exact scope. Arithmetic bridge for the Hadamard-counting path formula.

theorem cubicAmplitude_div_conservativeNormalizer_eq (n : Nat)
    (j : Fin (gridSize n)) :
    cubicAmplitude n j / conservativeNormalizer n =
      (j.val : Rat) ^ 3 / (gridSize n : Rat) ^ 4 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “grid size three mul eq cube”; the hypotheses and conclusion in the code panel fix its exact scope. Path-register capacity identity for the Hadamard-counting route.

theorem gridSize_three_mul_eq_cube (n : Nat) :
    gridSize (3 * n) = gridSize n ^ 3 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “grid size four mul eq fourth”; the hypotheses and conclusion in the code panel fix its exact scope. Four-register path-space identity for the Hadamard-counting denominator.

theorem gridSize_four_mul_eq_fourth (n : Nat) :
    gridSize (4 * n) = gridSize n ^ 4 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “hadamard counting cubic threshold count p fin range”; the hypotheses and conclusion in the code panel fix its exact scope. Reusable threshold count over 'List.finRange'.

theorem hadamardCountingCubic_thresholdCountP_finRange
    (m k : Nat) (hk : k ≤ m) :
    List.countP (fun t : Fin m => t.val < k) (List.finRange m) = k := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “hadamard counting cubic threshold filter length”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem hadamardCountingCubic_thresholdFilterLength
    (m k : Nat) (hk : k ≤ m) :
    ((List.finRange m).filter (fun t => t.val < k)).length = k := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “hadamard counting cubic threshold le path capacity”; the hypotheses and conclusion in the code panel fix its exact scope. The cubic threshold for row 'j' fits in the '3*n'-qubit path register.

theorem hadamardCountingCubic_threshold_le_pathCapacity
    (n : Nat) (j : Fin (gridSize n)) :
    j.val ^ 3 <= gridSize (3 * n) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “hadamard counting cubic threshold path count”; the hypotheses and conclusion in the code panel fix its exact scope. Symbolic accepted-path count for the Hadamard-counting threshold register.

theorem hadamardCountingCubic_thresholdPathCount
    (n : Nat) (j : Fin (gridSize n)) :
    ((List.finRange (gridSize (3 * n))).filter
        (fun t => t.val < j.val ^ 3)).length = j.val ^ 3 := by

commit-pinned source · Verso Blueprint panel

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

theorem gridPoint_nonneg (n : Nat) (j : Fin (gridSize n)) :
    (0 : Rat) ≤ gridPoint n j := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “grid point lt one”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem gridPoint_lt_one (n : Nat) (j : Fin (gridSize n)) :
    gridPoint n j < 1 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “grid point le one”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem gridPoint_le_one (n : Nat) (j : Fin (gridSize n)) :
    gridPoint n j ≤ 1 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “rat pow le one of nonneg le one”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem rat_pow_le_one_of_nonneg_le_one (x : Rat) (k : Nat)
    (hx0 : 0 ≤ x) (hx1 : x ≤ 1) :
    x ^ k ≤ 1 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “cubic amplitude sq le one”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem cubicAmplitude_sq_le_one (n : Nat) (j : Fin (gridSize n)) :
    cubicAmplitude n j ^ 2 ≤ 1 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “foldl add le add length”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem foldl_add_le_add_length {α : Type u} (xs : List α) (f : α → Rat)
    (h : ∀ x, x ∈ xs → f x ≤ 1) (acc : Rat) :
    xs.foldl (fun acc x => acc + f x) acc ≤ acc + (xs.length : Rat) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “cubic norm sq le grid size”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem cubicNormSq_le_gridSize (n : Nat) :
    cubicNormSq n ≤ (gridSize n : Rat) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “grid size rat le sq”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem gridSize_rat_le_sq (n : Nat) :
    (gridSize n : Rat) ≤ (gridSize n : Rat) ^ 2 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “cubic norm sq le conservative normalizer sq”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem cubicNormSq_le_conservativeNormalizer_sq (n : Nat) :
    cubicNormSq n ≤ conservativeNormalizer n ^ 2 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “cubic norm sq le arithmetic cubic normalizer sq”; the hypotheses and conclusion in the code panel fix its exact scope. Candidate-specific normalizer bridge for the first arithmetic route.

theorem cubicNormSq_le_arithmeticCubicNormalizer_sq (n : Nat) :
    cubicNormSq n ≤ arithmeticCubicNormalizer n ^ 2 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “cubic norm sq le hadamard counting cubic normalizer sq”; the hypotheses and conclusion in the code panel fix its exact scope. Candidate-specific normalizer bridge for the Hadamard-counting route.

theorem cubicNormSq_le_hadamardCountingCubicNormalizer_sq (n : Nat) :
    cubicNormSq n ≤ hadamardCountingCubicNormalizer n ^ 2 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “cubic norm sq n 1”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem cubicNormSq_n1 :
    cubicNormSq 1 = (1 : Rat) / 64 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “cubic norm sq n 2”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem cubicNormSq_n2 :
    cubicNormSq 2 = (397 : Rat) / 2048 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “cubic norm sq n 3”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem cubicNormSq_n3 :
    cubicNormSq 3 = (46205 : Rat) / 65536 := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “task id”. Task identifier used by the retrieval and verifier ledgers.

def taskId : String := "QBE-OP-CUBIC-DIAGONAL-001"

/-- The diagonal cubic oracle target `D_n[row,col] = (row/2^n)^3` if `row=col`, else zero. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “cubic diagonal operator”. The diagonal cubic oracle target 'D_n[row,col] = (row/2^n)^3' if 'row=col', else zero.

def cubicDiagonalOperator (n : Nat) :
    Matrix (gridSize n) (gridSize n) Rat :=
  fun row col =>
    if row = col then CubicStatePreparation.cubicAmplitude n row else 0

/-- Exact normalizer for the diagonal target at the primitive amplitude-oracle tier. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “exact normalizer”. Exact normalizer for the diagonal target at the primitive amplitude-oracle tier.

def exactNormalizer (_n : Nat) : Rat := 1

/-- Operator-first target record for the diagonal cubic oracle. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “cubic diagonal target”. Operator-first target record for the diagonal cubic oracle.

def cubicDiagonalTarget (n : Nat) :
    QueryOperatorTarget Rat (gridSize n) (gridSize n) where
  operator := cubicDiagonalOperator n
  normalizer := exactNormalizer n
  source :=
    "QBE-OP-CUBIC-DIAGONAL-001: D_n=sum_j (j/2^n)^3 |j><j|"
  semanticContract :=
    "diagonal cubic oracle; exact primitive amplitude-oracle route first"
  freeParameters := [
    "n positive",
    "diagonal target, not rank-one state preparation",

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “linear diagonal operator”. Hinted linear diagonal target 'O_0[row,col] = row/2^n' if 'row=col', else zero.

def linearDiagonalOperator (n : Nat) :
    Matrix (gridSize n) (gridSize n) Rat :=
  fun row col =>
    if row = col then CubicStatePreparation.gridPoint n row else 0

/-- Operator-first target record for the hinted linear diagonal input `O_0`. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “linear diagonal target”. Operator-first target record for the hinted linear diagonal input 'O_0'.

def linearDiagonalTarget (n : Nat) :
    QueryOperatorTarget Rat (gridSize n) (gridSize n) where
  operator := linearDiagonalOperator n
  normalizer := exactNormalizer n
  source :=
    "QBE-OP-CUBIC-DIAGONAL-001: O_0=sum_j (j/2^n) |j><j|"
  semanticContract :=
    "linear diagonal input target for compiled product and optional QSVT x^3 routes"
  freeParameters := [
    "n positive",
    "exact input block encoding required before QSVT consumption",

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “linear diagonal clean block contract”. Clean-block contract for the hinted linear diagonal input target.

def linearDiagonalCleanBlockContract (n : Nat)
    (block : Matrix (gridSize n) (gridSize n) Rat) : Prop :=
  ∀ row col,
    block row col =
      if row = col then CubicStatePreparation.gridPoint n row else 0

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “linear diagonal clean block contract pointwise eq”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem linearDiagonalCleanBlockContract_pointwise_eq
    (n : Nat) (block : Matrix (gridSize n) (gridSize n) Rat)
    (h : linearDiagonalCleanBlockContract n block) :
    Matrix.PointwiseEq block (linearDiagonalOperator n) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “linear diagonal clean block eq target”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem linearDiagonalCleanBlock_eq_target
    (n : Nat) (block : Matrix (gridSize n) (gridSize n) Rat)
    (h : linearDiagonalCleanBlockContract n block) :
    Matrix.PointwiseEq block (linearDiagonalTarget n).operator := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “linear diagonal exact clean block from pointwise”. Package a supplied clean-block equality for the hinted linear diagonal target as an 'ExactCleanBlock' payload.

def linearDiagonalExactCleanBlockFromPointwise
    {n total : Nat}
    (U : Matrix total total Rat)
    (embed : Fin (gridSize n) -> Fin total)
    (h :
      Matrix.PointwiseEq
        (BlockEncodingClassics.cleanBlockBy embed U)
        (linearDiagonalOperator n)) :
    BlockEncodingClassics.ExactCleanBlock (gridSize n) total where
  U := U
  A := linearDiagonalOperator n

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “linear diagonal exact clean block from pointwise clean eq target”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem linearDiagonalExactCleanBlockFromPointwise_clean_eq_target
    {n total : Nat}
    (U : Matrix total total Rat)
    (embed : Fin (gridSize n) -> Fin total)
    (h :
      Matrix.PointwiseEq
        (BlockEncodingClassics.cleanBlockBy embed U)
        (linearDiagonalOperator n)) :
    Matrix.PointwiseEq
      (BlockEncodingClassics.ExactCleanBlock.clean
        (linearDiagonalExactCleanBlockFromPointwise U embed h))

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “linear diagonal input be contract”. A proposition-valued field is a requirement until a constructor supplies it. Interface for a concrete block encoding of the hinted linear diagonal input.

structure LinearDiagonalInputBEContract (n total : Nat) where
  U : Matrix total total Rat
  embed : Fin (gridSize n) -> Fin total
  unitaryProof : BlockEncodingClassics.IsRationalOrthogonal U
  cleanupStatement : Prop
  cleanupDescription : String
  cleanupProof : cleanupStatement
  cleanBlockProof :
    Matrix.PointwiseEq
      (BlockEncodingClassics.cleanBlockBy embed U)
      (linearDiagonalOperator n)

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “exact payload”. Extract the reusable exact clean-block payload from a concrete linear-diagonal input contract.

def exactPayload {n total : Nat}
    (cert : LinearDiagonalInputBEContract n total) :
    BlockEncodingClassics.ExactCleanBlock (gridSize n) total :=
  linearDiagonalExactCleanBlockFromPointwise cert.U cert.embed cert.cleanBlockProof

/-- The extracted clean block equals the hinted linear diagonal target. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “clean eq target”; the hypotheses and conclusion in the code panel fix its exact scope. The extracted clean block equals the hinted linear diagonal target.

theorem clean_eq_target {n total : Nat}
    (cert : LinearDiagonalInputBEContract n total) :
    Matrix.PointwiseEq
      (BlockEncodingClassics.ExactCleanBlock.clean cert.exactPayload)
      (linearDiagonalTarget n).operator := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “householder zero”. Clean basis index for the 8-dimensional rational Householder signal block.

def householderZero : Fin 8 := 0

/-- Explicit rational dot product for the 8-dimensional Householder support leaf. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “dot 8”. Explicit rational dot product for the 8-dimensional Householder support leaf.

def dot8 (u v : Fin 8 -> Rat) : Rat :=
  u 0 * v 0 + u 1 * v 1 + u 2 * v 2 + u 3 * v 3 +
    u 4 * v 4 + u 5 * v 5 + u 6 * v 6 + u 7 * v 7

/-- Vector `e_0 - v` used in the rational Householder reflection. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “householder 8 e 0 minus”. Vector 'e_0 - v' used in the rational Householder reflection.

def householder8E0Minus (v : Fin 8 -> Rat) : Fin 8 -> Rat :=
  fun i => (if i = householderZero then 1 else 0) - v i

/--
Rational 8-by-8 Householder block used by the hinted `O_0` backend route.

The later backend still has to supply rational unit-vector completions for the
grid values and prove orthogonality of this block family.
-/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “householder 8”. Rational 8-by-8 Householder block used by the hinted 'O_0' backend route.

def householder8 (v : Fin 8 -> Rat) : Matrix 8 8 Rat :=
  fun row col =>
    (if row = col then 1 else 0) -
      (2 / dot8 (householder8E0Minus v) (householder8E0Minus v)) *
        householder8E0Minus v row * householder8E0Minus v col

/-- Norm identity for `e_0 - v` under the rational unit-vector hypothesis. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “householder 8 e 0 minus norm sq”; the hypotheses and conclusion in the code panel fix its exact scope. Norm identity for 'e_0 - v' under the rational unit-vector hypothesis.

theorem householder8E0Minus_normSq
    (v : Fin 8 -> Rat)
    (hunit : dot8 v v = 1) :
    dot8 (householder8E0Minus v) (householder8E0Minus v) =
      2 * (1 - v householderZero) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “householder 8 e 0 minus norm sq ne zero”; the hypotheses and conclusion in the code panel fix its exact scope. The Householder denominator is nonzero when the clean coordinate is not one.

theorem householder8E0Minus_normSq_ne_zero
    (v : Fin 8 -> Rat)
    (hunit : dot8 v v = 1)
    (hnot : v householderZero ≠ 1) :
    dot8 (householder8E0Minus v) (householder8E0Minus v) ≠ 0 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “householder 8 clean entry”; the hypotheses and conclusion in the code panel fix its exact scope. Active leaf 'HINT-HOUSEHOLDER8-CLEAN-ENTRY': the clean entry of the rational Householder block is the first coordinate of the supplied unit vector.

theorem householder8_clean_entry
    (v : Fin 8 -> Rat)
    (hunit : dot8 v v = 1)
    (hnot : v householderZero ≠ 1) :
    householder8 v householderZero householderZero =
      v householderZero := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “householder 8 is rational orthogonal”; the hypotheses and conclusion in the code panel fix its exact scope. Active leaf 'HINT-HOUSEHOLDER8-ORTHO': the rational 8-dimensional Householder block is orthogonal whenever the input vector has 'dot8 v v = 1' and does not equal the clean basis vector.

theorem householder8_isRationalOrthogonal
    (v : Fin 8 -> Rat)
    (hunit : dot8 v v = 1)
    (hnot : v householderZero ≠ 1) :
    BlockEncodingClassics.IsRationalOrthogonal (householder8 v) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “controlled householder 8 system index”. System component for the task-local 'ancilla × system' direct-sum matrix.

def controlledHouseholder8SystemIndex (n : Nat)
    (idx : Fin (8 * gridSize n)) : Fin (gridSize n) :=
  ⟨idx.val % gridSize n, Nat.mod_lt _ (CubicStatePreparation.gridSize_pos n)⟩

/-- Ancilla component for the task-local `ancilla × system` direct-sum matrix. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “controlled householder 8 ancilla index”. Ancilla component for the task-local 'ancilla × system' direct-sum matrix.

def controlledHouseholder8AncillaIndex (n : Nat)
    (idx : Fin (8 * gridSize n)) : Fin 8 :=
  ⟨idx.val / gridSize n, by
    have hlt : idx.val < gridSize n * 8 := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “controlled householder 8 embed”. Clean embedding for the controlled Householder direct sum.

def controlledHouseholder8Embed (n : Nat) :
    Fin (gridSize n) -> Fin (8 * gridSize n) :=
  BlockEncodingClassics.productIndex householderZero

/-- Task-local controlled direct sum of supplied Householder blocks over system branches. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “controlled householder 8 direct sum”. Task-local controlled direct sum of supplied Householder blocks over system branches.

def controlledHouseholder8DirectSum
    (n : Nat) (v : Fin (gridSize n) -> Fin 8 -> Rat) :
    Matrix (8 * gridSize n) (8 * gridSize n) Rat :=
  fun row col =>
    if controlledHouseholder8SystemIndex n row =
        controlledHouseholder8SystemIndex n col then
      householder8 (v (controlledHouseholder8SystemIndex n row))
        (controlledHouseholder8AncillaIndex n row)
        (controlledHouseholder8AncillaIndex n col)
    else 0

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “controlled householder 8 branch nontrivial of clean”; the hypotheses and conclusion in the code panel fix its exact scope. Grid branches for the linear diagonal input never have clean Householder coordinate equal to one.

theorem controlledHouseholder8_branchNontrivial_of_clean
    (n : Nat)
    (v : Fin (gridSize n) -> Fin 8 -> Rat)
    (branchClean :
      forall j : Fin (gridSize n),
        v j householderZero = CubicStatePreparation.gridPoint n j) :
    forall j : Fin (gridSize n), v j householderZero ≠ 1 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “controlled householder 8 direct sum clean entry”; the hypotheses and conclusion in the code panel fix its exact scope. Active leaf 'HINT-CONTROLLED-DIRECT-SUM': the clean block of the controlled Householder direct sum is the hinted linear diagonal operator.

theorem controlledHouseholder8DirectSum_clean_entry
    (n : Nat)
    (v : Fin (gridSize n) -> Fin 8 -> Rat)
    (branchUnit :
      forall j : Fin (gridSize n), dot8 (v j) (v j) = 1)
    (branchClean :
      forall j : Fin (gridSize n),
        v j householderZero = CubicStatePreparation.gridPoint n j)
    (branchNontrivial :
      forall j : Fin (gridSize n), v j householderZero ≠ 1) :
    Matrix.PointwiseEq

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “controlled householder 8 direct sum column inner eq identity of system ne”; the hypotheses and conclusion in the code panel fix its exact scope. Column-inner bridge for the controlled Householder direct sum in the cross-branch case.

theorem controlledHouseholder8DirectSum_columnInner_eq_identity_of_system_ne
    (n : Nat)
    (v : Fin (gridSize n) -> Fin 8 -> Rat)
    (i j : Fin (8 * gridSize n))
    (hsys :
      controlledHouseholder8SystemIndex n i ≠
        controlledHouseholder8SystemIndex n j) :
    BlockEncodingClassics.columnInner (controlledHouseholder8DirectSum n v) i j =
      Matrix.identity (8 * gridSize n) Rat i j := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “controlled householder 8 direct sum column inner eq branch”; the hypotheses and conclusion in the code panel fix its exact scope. Support leaf 'CDS-COL-FOLD': inside one decoded system branch, the column inner product of the controlled direct sum is the column inner product of that branch's Householder block.

theorem controlledHouseholder8DirectSum_columnInner_eq_branch
    (n : Nat)
    (v : Fin (gridSize n) -> Fin 8 -> Rat)
    (i j : Fin (8 * gridSize n))
    (hsys :
      controlledHouseholder8SystemIndex n i =
        controlledHouseholder8SystemIndex n j) :
    BlockEncodingClassics.columnInner
      (controlledHouseholder8DirectSum n v) i j =
    BlockEncodingClassics.columnInner
      (householder8 (v (controlledHouseholder8SystemIndex n i)))

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “controlled householder 8 direct sum row inner eq branch”; the hypotheses and conclusion in the code panel fix its exact scope. Support leaf 'CDS-ROW-FOLD': inside one decoded system branch, the row inner product of the controlled direct sum is the row inner product of that branch's Householder block.

theorem controlledHouseholder8DirectSum_rowInner_eq_branch
    (n : Nat)
    (v : Fin (gridSize n) -> Fin 8 -> Rat)
    (i j : Fin (8 * gridSize n))
    (hsys :
      controlledHouseholder8SystemIndex n i =
        controlledHouseholder8SystemIndex n j) :
    BlockEncodingClassics.rowInner
      (controlledHouseholder8DirectSum n v) i j =
    BlockEncodingClassics.rowInner
      (householder8 (v (controlledHouseholder8SystemIndex n i)))

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “controlled householder 8 direct sum row inner eq identity of system ne”; the hypotheses and conclusion in the code panel fix its exact scope. Row-inner bridge for the controlled Householder direct sum in the cross-branch case.

theorem controlledHouseholder8DirectSum_rowInner_eq_identity_of_system_ne
    (n : Nat)
    (v : Fin (gridSize n) -> Fin 8 -> Rat)
    (i j : Fin (8 * gridSize n))
    (hsys :
      controlledHouseholder8SystemIndex n i ≠
        controlledHouseholder8SystemIndex n j) :
    BlockEncodingClassics.rowInner (controlledHouseholder8DirectSum n v) i j =
      Matrix.identity (8 * gridSize n) Rat i j := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “controlled householder 8 direct sum is rational orthogonal”; the hypotheses and conclusion in the code panel fix its exact scope. Active leaf 'HINT-CONTROLLED-DIRECT-SUM-ORTHO': branchwise rational orthogonality for the controlled direct sum of supplied 8-dimensional Householder blocks.

theorem controlledHouseholder8DirectSum_isRationalOrthogonal
    (n : Nat)
    (v : Fin (gridSize n) -> Fin 8 -> Rat)
    (branchUnit :
      forall j : Fin (gridSize n), dot8 (v j) (v j) = 1)
    (branchNontrivial :
      forall j : Fin (gridSize n), v j householderZero ≠ 1) :
    BlockEncodingClassics.IsRationalOrthogonal
      (controlledHouseholder8DirectSum n v) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “linear diagonal rational completion”. Branch-vector completion contract for the rational Householder backend of the hinted linear diagonal input 'O_0'.

def LinearDiagonalRationalCompletion (n : Nat) : Prop :=
  exists v : Fin (gridSize n) -> Fin 8 -> Rat,
    (forall j : Fin (gridSize n), dot8 (v j) (v j) = 1) ∧
    (forall j : Fin (gridSize n),
      v j householderZero = CubicStatePreparation.gridPoint n j)

/--
Branch vector obtained from a four-square completion of the residual
`(2^n)^2 - j^2`.

The first coordinate is the grid value `j / 2^n`; the next four coordinates

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “linear diagonal four square branch vector”. Branch vector obtained from a four-square completion of the residual '(2^n)^2 - j^2'.

def linearDiagonalFourSquareBranchVector
    (n : Nat) (j : Fin (gridSize n)) (a b c d : Nat) : Fin 8 -> Rat :=
  fun i =>
    if i = (0 : Fin 8) then (j.val : Rat) / (gridSize n : Rat)
    else if i = (1 : Fin 8) then (a : Rat) / (gridSize n : Rat)
    else if i = (2 : Fin 8) then (b : Rat) / (gridSize n : Rat)
    else if i = (3 : Fin 8) then (c : Rat) / (gridSize n : Rat)
    else if i = (4 : Fin 8) then (d : Rat) / (gridSize n : Rat)
    else 0

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “linear diagonal four square branch vector clean”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem linearDiagonalFourSquareBranchVector_clean
    (n : Nat) (j : Fin (gridSize n)) (a b c d : Nat) :
    linearDiagonalFourSquareBranchVector n j a b c d householderZero =
      CubicStatePreparation.gridPoint n j := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “linear diagonal four square branch vector unit”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem linearDiagonalFourSquareBranchVector_unit
    (n : Nat) (j : Fin (gridSize n)) (a b c d : Nat)
    (hsq :
      gridSize n ^ 2 =
        j.val ^ 2 + a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2) :
    dot8 (linearDiagonalFourSquareBranchVector n j a b c d)
      (linearDiagonalFourSquareBranchVector n j a b c d) = 1 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “linear diagonal rational completion of four square witnesses”; the hypotheses and conclusion in the code panel fix its exact scope. Adapter from explicit four-square witnesses to the rational-completion predicate.

theorem linearDiagonalRationalCompletion_of_fourSquareWitnesses
    (n : Nat)
    (a b c d : Fin (gridSize n) -> Nat)
    (hsq : forall j : Fin (gridSize n),
      gridSize n ^ 2 =
        j.val ^ 2 + a j ^ 2 + b j ^ 2 + c j ^ 2 + d j ^ 2) :
    LinearDiagonalRationalCompletion n := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “linear diagonal rational completion exists”; the hypotheses and conclusion in the code panel fix its exact scope. Every dyadic grid value has an unconditional rational unit-vector completion.

theorem linearDiagonalRationalCompletion_exists (n : Nat) :
    LinearDiagonalRationalCompletion n := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “linear diagonal rational completion branch data”; the hypotheses and conclusion in the code panel fix its exact scope. Adapter leaf for 'HINT-O0-RATIONAL-COMPLETION': a rational-completion witness also supplies the nontrivial clean-coordinate side condition needed by the Householder block.

theorem linearDiagonalRationalCompletion_branchData
    (n : Nat)
    (h : LinearDiagonalRationalCompletion n) :
    exists v : Fin (gridSize n) -> Fin 8 -> Rat,
      (forall j : Fin (gridSize n), dot8 (v j) (v j) = 1) ∧
      (forall j : Fin (gridSize n),
        v j householderZero = CubicStatePreparation.gridPoint n j) ∧
      (forall j : Fin (gridSize n), v j householderZero ≠ 1) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “linear diagonal rational completion backend support”; the hypotheses and conclusion in the code panel fix its exact scope. A rational-completion witness supplies the clean-block equality and rational orthogonality facts for the controlled Householder direct sum.

theorem linearDiagonalRationalCompletion_backendSupport
    (n : Nat)
    (h : LinearDiagonalRationalCompletion n) :
    exists v : Fin (gridSize n) -> Fin 8 -> Rat,
      Matrix.PointwiseEq
        (BlockEncodingClassics.cleanBlockBy
          (controlledHouseholder8Embed n)
          (controlledHouseholder8DirectSum n v))
        (linearDiagonalOperator n) ∧
      BlockEncodingClassics.IsRationalOrthogonal
        (controlledHouseholder8DirectSum n v) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “linear diagonal householder circuit”. Oracle-label circuit for the proved rational Householder realization of 'O_0'.

def linearDiagonalHouseholderCircuit (_n : Nat) : Circuit :=
  [Gate.oracleCall "controlled-rational-householder-linear-diagonal"]

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “linear diagonal householder resource”.

def linearDiagonalHouseholderResource (n : Nat) : Resource :=
  (linearDiagonalHouseholderCircuit n).resource

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “linear diagonal householder resource eq”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem linearDiagonalHouseholderResource_eq (n : Nat) :
    linearDiagonalHouseholderResource n =
      Resource.ofCountsWithDepth 0 0 1 0 1 := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “linear diagonal householder input be contract”. Unconditional exact matrix-level block encoding of the hinted input 'O_0'.

noncomputable def linearDiagonalHouseholderInputBEContract (n : Nat) :
    LinearDiagonalInputBEContract n (8 * gridSize n) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “linear diagonal householder input be contract clean eq target”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem linearDiagonalHouseholderInputBEContract_clean_eq_target (n : Nat) :
    Matrix.PointwiseEq
      (BlockEncodingClassics.ExactCleanBlock.clean
        (linearDiagonalHouseholderInputBEContract n).exactPayload)
      (linearDiagonalTarget n).operator := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “linear diagonal householder input be contract complete”; the hypotheses and conclusion in the code panel fix its exact scope. Root certificate for the hinted input operator 'O_0'.

theorem linearDiagonalHouseholderInputBEContract_complete (n : Nat) :
    BlockEncodingClassics.IsRationalOrthogonal
        (linearDiagonalHouseholderInputBEContract n).U ∧
      Matrix.PointwiseEq
        (BlockEncodingClassics.cleanBlockBy
          (linearDiagonalHouseholderInputBEContract n).embed
          (linearDiagonalHouseholderInputBEContract n).U)
        (linearDiagonalTarget n).operator ∧
      (linearDiagonalTarget n).normalizer = 1 ∧
      (linearDiagonalHouseholderInputBEContract n).resource =
        Resource.ofCountsWithDepth 0 0 1 0 1 := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “approx diagonal operator”. Supplied diagonal matrix for the first Scenario 2 approximate route.

def approxDiagonalOperator (n : Nat) (q : Fin (gridSize n) -> Rat) :
    Matrix (gridSize n) (gridSize n) Rat :=
  fun row col => if row = col then q row else 0

/-- Task-local rational absolute value used before a project norm API exists. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “rat abs”. Task-local rational absolute value used before a project norm API exists.

def ratAbs (x : Rat) : Rat := if 0 ≤ x then x else -x

/-- Project-local rational matrices whose off-diagonal entries are zero. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “is diagonal rat matrix”. Project-local rational matrices whose off-diagonal entries are zero.

def IsDiagonalRatMatrix (dim : Nat) (A : Matrix dim dim Rat) : Prop :=
  ∀ row col : Fin dim, row ≠ col -> A row col = 0

/--
Typed contract for the missing rational-matrix operator-norm bridge.

This structure is deliberately conditional: it does not assert that the bridge
is already available in this repository.  A future Mathlib-backed proof or a
human-accepted external contract must supply this record before an approximate
block-encoding certificate may consume the norm bound.
-/

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “diagonal rat operator norm bridge”. A proposition-valued field is a requirement until a constructor supplies it. Typed contract for the missing rational-matrix operator-norm bridge.

structure DiagonalRatOperatorNormBridge (dim : Nat) where
  opNormErrorAtMost : Matrix dim dim Rat -> Matrix dim dim Rat -> Rat -> Prop
  diagonal_entrywise_error_operatorNorm_le :
    ∀ (A B : Matrix dim dim Rat) (epsilon : Rat),
      IsDiagonalRatMatrix dim A ->
      IsDiagonalRatMatrix dim B ->
      0 ≤ epsilon ->
      (∀ j : Fin dim, ratAbs (A j j - B j j) ≤ epsilon) ->
      opNormErrorAtMost A B epsilon

/-- Squared Euclidean norm on project-local finite rational vectors. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “rat squared euclidean norm”. Squared Euclidean norm on project-local finite rational vectors.

def ratSquaredEuclideanNorm {dim : Nat} (v : Fin dim -> Rat) : Rat :=
  (List.finRange dim).foldl (fun acc j => acc + v j * v j) 0

/-- Action of the matrix error `A - B` on a finite rational vector. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “rat matrix error action”. Action of the matrix error 'A - B' on a finite rational vector.

def ratMatrixErrorAction {dim : Nat}
    (A B : Matrix dim dim Rat) (v : Fin dim -> Rat) : Fin dim -> Rat :=
  fun row =>
    (List.finRange dim).foldl
      (fun acc col => acc + (A row col - B row col) * v col) 0

/--
Non-vacuous squared Euclidean induced operator-norm error semantics.

For nonnegative `epsilon`, this states `||(A-B)v||₂² ≤ ||epsilon v||₂²`
for every rational vector `v`.  Squared norms avoid introducing square roots

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “rat euclidean operator norm error at most”. Non-vacuous squared Euclidean induced operator-norm error semantics.

def ratEuclideanOperatorNormErrorAtMost {dim : Nat}
    (A B : Matrix dim dim Rat) (epsilon : Rat) : Prop :=
  0 ≤ epsilon ∧
    ∀ v : Fin dim -> Rat,
      ratSquaredEuclideanNorm (ratMatrixErrorAction A B v) ≤
        ratSquaredEuclideanNorm (fun j => epsilon * v j)

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “rat matrix error action eq diagonal”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem ratMatrixErrorAction_eq_diagonal {dim : Nat}
    (A B : Matrix dim dim Rat) (v : Fin dim -> Rat) (row : Fin dim)
    (hA : IsDiagonalRatMatrix dim A)
    (hB : IsDiagonalRatMatrix dim B) :
    ratMatrixErrorAction A B v row = (A row row - B row row) * v row := by

commit-pinned source · Verso Blueprint panel

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

theorem ratAbs_nonneg (x : Rat) : 0 ≤ ratAbs x := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “rat mul self eq rat abs mul self”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem rat_mul_self_eq_ratAbs_mul_self (x : Rat) :
    x * x = ratAbs x * ratAbs x := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “rat mul self nonneg”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem rat_mul_self_nonneg (x : Rat) : 0 ≤ x * x := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “rat mul self le of abs le”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem rat_mul_self_le_of_abs_le (x epsilon : Rat)
    (hepsilon : 0 ≤ epsilon) (habs : ratAbs x ≤ epsilon) :
    x * x ≤ epsilon * epsilon := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “rat mul self vector le of abs le”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem rat_mul_self_vector_le_of_abs_le (x epsilon value : Rat)
    (hepsilon : 0 ≤ epsilon) (habs : ratAbs x ≤ epsilon) :
    (x * value) * (x * value) ≤
      (epsilon * value) * (epsilon * value) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “rat euclidean diagonal operator norm bridge”. Concrete proof that diagonal entrywise bounds imply the squared Euclidean bound.

def ratEuclideanDiagonalOperatorNormBridge (dim : Nat) :
    DiagonalRatOperatorNormBridge dim where
  opNormErrorAtMost := ratEuclideanOperatorNormErrorAtMost
  diagonal_entrywise_error_operatorNorm_le := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “rat euclidean operator norm error at most not vacuous”; the hypotheses and conclusion in the code panel fix its exact scope. The local Euclidean error predicate is observably non-vacuous.

theorem ratEuclideanOperatorNormErrorAtMost_not_vacuous :
    ¬ ratEuclideanOperatorNormErrorAtMost
      (Matrix.identity 1 Rat) (Matrix.zero 1 1 Rat) 0 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “approx diagonal operator is diagonal”; the hypotheses and conclusion in the code panel fix its exact scope. The supplied approximate diagonal matrix has zero off-diagonal entries.

theorem approxDiagonalOperator_isDiagonal
    (n : Nat) (q : Fin (gridSize n) -> Rat) :
    IsDiagonalRatMatrix (gridSize n) (approxDiagonalOperator n q) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “cubic diagonal operator is diagonal”; the hypotheses and conclusion in the code panel fix its exact scope. The exact cubic diagonal target has zero off-diagonal entries.

theorem cubicDiagonalOperator_isDiagonal
    (n : Nat) :
    IsDiagonalRatMatrix (gridSize n) (cubicDiagonalOperator n) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “approx diagonal entrywise error at most”. Entrywise scalar-error predicate for the Scenario 2 approximate diagonal route.

def approxDiagonalEntrywiseErrorAtMost
    (n : Nat) (q : Fin (gridSize n) -> Rat) (epsilon : Rat) : Prop :=
  ∀ j : Fin (gridSize n),
    ratAbs (q j - CubicStatePreparation.cubicAmplitude n j) ≤ epsilon

/--
Local entrywise bridge for `APPROX-DIAG-NORM`: diagonal scalar errors transfer
to every matrix entry of the supplied diagonal operator.

This does not prove an operator-norm bound; it is the reusable finite-matrix
side of the still-open diagonal norm obligation.

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “approx diagonal operator entrywise error”; the hypotheses and conclusion in the code panel fix its exact scope. Local entrywise bridge for 'APPROX-DIAG-NORM': diagonal scalar errors transfer to every matrix entry of the supplied diagonal operator.

theorem approxDiagonalOperator_entrywise_error
    (n : Nat) (q : Fin (gridSize n) -> Rat) (epsilon : Rat)
    (hdiag : approxDiagonalEntrywiseErrorAtMost n q epsilon)
    (hepsilon : 0 ≤ epsilon) :
    ∀ row col : Fin (gridSize n),
      ratAbs
        (approxDiagonalOperator n q row col -
          cubicDiagonalOperator n row col) ≤ epsilon := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “approx diagonal operator operator norm error of contract”; the hypotheses and conclusion in the code panel fix its exact scope. Conditional adapter from the compiled diagonal entrywise theorem to the task-local operator-norm contract.

theorem approxDiagonalOperator_operatorNorm_error_of_contract
    (n : Nat) (q : Fin (gridSize n) -> Rat) (epsilon : Rat)
    (bridge : DiagonalRatOperatorNormBridge (gridSize n))
    (hdiag : approxDiagonalEntrywiseErrorAtMost n q epsilon)
    (hepsilon : 0 ≤ epsilon) :
    bridge.opNormErrorAtMost
      (approxDiagonalOperator n q)
      (cubicDiagonalOperator n)
      epsilon := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “approx diagonal operator operator norm error”; the hypotheses and conclusion in the code panel fix its exact scope. Unconditional local Euclidean operator-norm bound for the supplied diagonal approximation.

theorem approxDiagonalOperator_operatorNorm_error
    (n : Nat) (q : Fin (gridSize n) -> Rat) (epsilon : Rat)
    (hdiag : approxDiagonalEntrywiseErrorAtMost n q epsilon)
    (hepsilon : 0 ≤ epsilon) :
    ratEuclideanOperatorNormErrorAtMost
      (approxDiagonalOperator n q)
      (cubicDiagonalOperator n)
      epsilon := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “rational circle branch vector”. Two-coordinate rational unit-circle branch vector for the approximate controlled-Householder route.

def rationalCircleBranchVector (q r : Rat) : Fin 8 -> Rat :=
  fun i =>
    if i = (0 : Fin 8) then q
    else if i = (1 : Fin 8) then r
    else 0

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “rational circle branch vector clean”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem rationalCircleBranchVector_clean (q r : Rat) :
    rationalCircleBranchVector q r householderZero = q := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “rational circle branch vector unit”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem rationalCircleBranchVector_unit
    (q r : Rat)
    (hcircle : q ^ 2 + r ^ 2 = 1) :
    dot8 (rationalCircleBranchVector q r)
      (rationalCircleBranchVector q r) = 1 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “controlled householder 8 direct sum clean entry of branch value”; the hypotheses and conclusion in the code panel fix its exact scope. Approximate-route support leaf 'APPROX-CDS-CLEAN': if each controlled Householder branch has clean coordinate 'q j', then the clean block is the supplied diagonal matrix 'diag(q)'.

theorem controlledHouseholder8DirectSum_clean_entry_of_branchValue
    (n : Nat)
    (q : Fin (gridSize n) -> Rat)
    (v : Fin (gridSize n) -> Fin 8 -> Rat)
    (branchUnit :
      forall j : Fin (gridSize n), dot8 (v j) (v j) = 1)
    (branchClean :
      forall j : Fin (gridSize n), v j householderZero = q j)
    (branchNontrivial :
      forall j : Fin (gridSize n), v j householderZero ≠ 1) :
    Matrix.PointwiseEq

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “cubic diagonal four square branch vector”. Rational branch vector whose clean coordinate is '(j / 2^n)^3'.

def cubicDiagonalFourSquareBranchVector
    (n : Nat) (j : Fin (gridSize n)) (a b c d : Nat) : Fin 8 -> Rat :=
  fun i =>
    if i = (0 : Fin 8) then (j.val : Rat) ^ 3 / (gridSize n : Rat) ^ 3
    else if i = (1 : Fin 8) then (a : Rat) / (gridSize n : Rat) ^ 3
    else if i = (2 : Fin 8) then (b : Rat) / (gridSize n : Rat) ^ 3
    else if i = (3 : Fin 8) then (c : Rat) / (gridSize n : Rat) ^ 3
    else if i = (4 : Fin 8) then (d : Rat) / (gridSize n : Rat) ^ 3
    else 0

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “cubic diagonal four square branch vector clean”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem cubicDiagonalFourSquareBranchVector_clean
    (n : Nat) (j : Fin (gridSize n)) (a b c d : Nat) :
    cubicDiagonalFourSquareBranchVector n j a b c d householderZero =
      CubicStatePreparation.cubicAmplitude n j := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “cubic diagonal four square branch vector unit”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem cubicDiagonalFourSquareBranchVector_unit
    (n : Nat) (j : Fin (gridSize n)) (a b c d : Nat)
    (hsq :
      gridSize n ^ 6 =
        j.val ^ 6 + a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2) :
    dot8 (cubicDiagonalFourSquareBranchVector n j a b c d)
      (cubicDiagonalFourSquareBranchVector n j a b c d) = 1 := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “cubic diagonal rational completion”.

def CubicDiagonalRationalCompletion (n : Nat) : Prop :=
  exists v : Fin (gridSize n) -> Fin 8 -> Rat,
    (forall j : Fin (gridSize n), dot8 (v j) (v j) = 1) ∧
    (forall j : Fin (gridSize n),
      v j householderZero = CubicStatePreparation.cubicAmplitude n j)

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “cubic diagonal rational completion of four square witnesses”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem cubicDiagonalRationalCompletion_of_fourSquareWitnesses
    (n : Nat)
    (a b c d : Fin (gridSize n) -> Nat)
    (hsq : forall j : Fin (gridSize n),
      gridSize n ^ 6 =
        j.val ^ 6 + a j ^ 2 + b j ^ 2 + c j ^ 2 + d j ^ 2) :
    CubicDiagonalRationalCompletion n := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “cubic diagonal rational completion exists”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem cubicDiagonalRationalCompletion_exists (n : Nat) :
    CubicDiagonalRationalCompletion n := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “cubic amplitude lt one”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem cubicAmplitude_lt_one
    (n : Nat) (j : Fin (gridSize n)) :
    CubicStatePreparation.cubicAmplitude n j < 1 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “cubic diagonal rational completion backend support”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem cubicDiagonalRationalCompletion_backendSupport
    (n : Nat) :
    exists v : Fin (gridSize n) -> Fin 8 -> Rat,
      Matrix.PointwiseEq
        (BlockEncodingClassics.cleanBlockBy
          (controlledHouseholder8Embed n)
          (controlledHouseholder8DirectSum n v))
        (cubicDiagonalOperator n) ∧
      BlockEncodingClassics.IsRationalOrthogonal
        (controlledHouseholder8DirectSum n v) := by

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “cubic diagonal exact be contract”. A proposition-valued field is a requirement until a constructor supplies it. Strong exact certificate for the cubic target, including orthogonality.

structure CubicDiagonalExactBEContract (n total : Nat) where
  exactPayload : BlockEncodingClassics.ExactCleanBlock (gridSize n) total
  unitaryProof : BlockEncodingClassics.IsRationalOrthogonal exactPayload.U
  normalizerProof : (cubicDiagonalTarget n).normalizer = 1
  cleanupStatement : Prop
  cleanupProof : cleanupStatement
  resource : Resource
  resourceStatement : Prop
  resourceProof : resourceStatement

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “cubic diagonal householder exact be contract”.

noncomputable def cubicDiagonalHouseholderExactBEContract (n : Nat) :
    CubicDiagonalExactBEContract n (8 * gridSize n) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “cubic diagonal householder exact be contract clean eq target”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem cubicDiagonalHouseholderExactBEContract_clean_eq_target (n : Nat) :
    Matrix.PointwiseEq
      (cubicDiagonalHouseholderExactBEContract n).exactPayload.clean
      (cubicDiagonalTarget n).operator := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “cubic diagonal householder exact be contract complete”; the hypotheses and conclusion in the code panel fix its exact scope. Unconditional exact root certificate for the cubic diagonal operator.

theorem cubicDiagonalHouseholderExactBEContract_complete (n : Nat) :
    BlockEncodingClassics.IsRationalOrthogonal
        (cubicDiagonalHouseholderExactBEContract n).exactPayload.U ∧
      Matrix.PointwiseEq
        (cubicDiagonalHouseholderExactBEContract n).exactPayload.clean
        (cubicDiagonalTarget n).operator ∧
      (cubicDiagonalTarget n).normalizer = 1 ∧
      (cubicDiagonalHouseholderExactBEContract n).resource =
        Resource.ofCountsWithDepth 0 0 1 0 1 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “linear diagonal cube eq cubic diagonal operator”; the hypotheses and conclusion in the code panel fix its exact scope. Target-identification leaf for the hinted route: the project-local matrix cube of 'O_0' is the cubic diagonal target 'D_n'.

theorem linearDiagonal_cube_eq_cubicDiagonalOperator (n : Nat) :
    Matrix.PointwiseEq
      (Matrix.mul
        (Matrix.mul (linearDiagonalOperator n) (linearDiagonalOperator n))
        (linearDiagonalOperator n))
      (cubicDiagonalOperator n) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “linear diagonal cubic product certificate”. The compiled non-QSVT polynomial consumer for the human hint.

noncomputable def linearDiagonalCubicProductCertificate (n : Nat) :
    BlockEncodingClassics.LCUCertificate (gridSize n) :=
  let input :=
    BlockEncodingClassics.ExactCleanBlock.toLCUCertificate
      (linearDiagonalHouseholderInputBEContract n).exactPayload
  BlockEncodingClassics.productCleanBlockCertificate
    (BlockEncodingClassics.productCleanBlockCertificate input input) input

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “linear diagonal cubic product certificate target eq”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem linearDiagonalCubicProductCertificate_target_eq (n : Nat) :
    Matrix.PointwiseEq
      (linearDiagonalCubicProductCertificate n).target
      (cubicDiagonalTarget n).operator := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “linear diagonal cubic product certificate clean eq target”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem linearDiagonalCubicProductCertificate_clean_eq_target (n : Nat) :
    Matrix.PointwiseEq
      (linearDiagonalCubicProductCertificate n).cleanBlock
      (cubicDiagonalTarget n).operator := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “cubic qsvt polynomial”. The polynomial selected by the human-hinted QSVT route.

def cubicQSVTPolynomial (x : Rat) : Rat := x ^ 3

/-- The cubic QSVT polynomial is bounded on every spectral value used by `O_0`. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “cubic qsvt polynomial grid point abs le one”; the hypotheses and conclusion in the code panel fix its exact scope. The cubic QSVT polynomial is bounded on every spectral value used by 'O_0'.

theorem cubicQSVTPolynomial_gridPoint_abs_le_one
    (n : Nat) (j : Fin (gridSize n)) :
    Rat.abs (cubicQSVTPolynomial (CubicStatePreparation.gridPoint n j)) ≤ 1 := by

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “cubic qsvt local side conditions”. A proposition-valued field is a requirement until a constructor supplies it. Locally checkable side conditions for the cubic polynomial on the 'O_0' spectrum.

structure CubicQSVTLocalSideConditions (n : Nat) where
  degree : Nat
  degree_eq : degree = 3
  oddParity : Bool
  oddParity_eq : oddParity = true
  boundedOnInputSpectrum :
    forall j : Fin (gridSize n),
      Rat.abs (cubicQSVTPolynomial (CubicStatePreparation.gridPoint n j)) ≤ 1

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “cubic qsvt local side conditions”.

def cubicQSVTLocalSideConditions (n : Nat) :
    CubicQSVTLocalSideConditions n := by

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “cubic qsvt external semantics”. A proposition-valued field is a requirement until a constructor supplies it. Single external boundary for the hinted route.

structure CubicQSVTExternalSemantics (n inputTotal outputTotal : Nat) where
  input : LinearDiagonalInputBEContract n inputTotal
  output : BlockEncodingClassics.ExactCleanBlock (gridSize n) outputTotal
  outputUnitary : BlockEncodingClassics.IsRationalOrthogonal output.U
  outputIsCubicTransform :
    Matrix.PointwiseEq output.A
      (Matrix.mul
        (Matrix.mul (linearDiagonalOperator n) (linearDiagonalOperator n))
        (linearDiagonalOperator n))
  globalPolynomialAdmissibility : Prop
  globalPolynomialAdmissibilityDescription : String

commit-pinned source · Verso Blueprint panel

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

theorem output_eq_cubic_target {n inputTotal outputTotal : Nat}
    (semantics : CubicQSVTExternalSemantics n inputTotal outputTotal) :
    Matrix.PointwiseEq semantics.output.A (cubicDiagonalTarget n).operator := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “consumer contract”. Instantiate the generic consumer boundary without reopening QSVT search.

def consumerContract {n inputTotal outputTotal : Nat}
    (semantics : CubicQSVTExternalSemantics n inputTotal outputTotal) :
    BlockEncodingClassics.QSVTConsumerContract (gridSize n) inputTotal where
  input := semantics.input.exactPayload
  polynomialDescription := "P(x)=x^3; degree 3; odd; bounded on [-1,1]"
  sideConditions :=
    Nonempty (CubicQSVTLocalSideConditions n) ∧
      semantics.globalPolynomialAdmissibility
  outputStatement :=
    Matrix.PointwiseEq semantics.output.A (cubicDiagonalTarget n).operator
  sideConditionProof :=

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “amplitude oracle layout”. One signal qubit and no pure workspace at the oracle-label tier.

def amplitudeOracleLayout (n : Nat) : RegisterLayout where
  systemQubits := n
  signalQubits := 1
  pureAncillas := 0

/-- Oracle-level exact diagonal amplitude transcript. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “amplitude oracle circuit”. Oracle-level exact diagonal amplitude transcript.

def amplitudeOracleCircuit (_n : Nat) : Circuit :=
  [Gate.oracleCall "diag-cubic-amplitude-oracle"]

/-- Resource of the oracle-label diagonal candidate. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “amplitude oracle resource”. Resource of the oracle-label diagonal candidate.

def amplitudeOracleResource (n : Nat) : Resource :=
  (amplitudeOracleCircuit n).resource

/-- Candidate score for the oracle-label diagonal candidate. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “amplitude oracle cost”. Candidate score for the oracle-label diagonal candidate.

def amplitudeOracleCost (n : Nat) : BlockEncodingCost :=
  BlockEncodingCost.fromLayoutAndResource
    (amplitudeOracleLayout n) (amplitudeOracleResource n)

/-- Tuple in the QBE score order `(gateCount, depth, auxiliaryQubits, oracleCalls)`. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “amplitude oracle resource tuple”. Tuple in the QBE score order '(gateCount, depth, auxiliaryQubits, oracleCalls)'.

def amplitudeOracleResourceTuple (n : Nat) : Nat × Nat × Nat × Nat :=
  ( (amplitudeOracleCost n).gateCount
  , (amplitudeOracleCost n).depth
  , (amplitudeOracleCost n).auxiliaryQubits
  , (amplitudeOracleCost n).oracleCalls
  )

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “amplitude oracle resource eq”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem amplitudeOracleResource_eq (n : Nat) :
    amplitudeOracleResource n = Resource.ofCountsWithDepth 0 0 1 0 1 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “amplitude oracle resource tuple eq”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem amplitudeOracleResourceTuple_eq (n : Nat) :
    amplitudeOracleResourceTuple n = (1, 1, 1, 1) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “diagonal clean block contract”. Clean-block contract for the diagonal cubic candidate.

def diagonalCleanBlockContract (n : Nat)
    (block : Matrix (gridSize n) (gridSize n) Rat) : Prop :=
  ∀ row col,
    block row col =
      if row = col then CubicStatePreparation.cubicAmplitude n row else 0

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “diagonal clean block contract pointwise eq”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem diagonalCleanBlockContract_pointwise_eq
    (n : Nat) (block : Matrix (gridSize n) (gridSize n) Rat)
    (h : diagonalCleanBlockContract n block) :
    Matrix.PointwiseEq block (cubicDiagonalOperator n) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “primitive oracle clean block eq target”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem primitiveOracleCleanBlock_eq_target
    (n : Nat) (block : Matrix (gridSize n) (gridSize n) Rat)
    (h : diagonalCleanBlockContract n block) :
    Matrix.PointwiseEq block (cubicDiagonalTarget n).operator := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “cubic amplitude le one”; the hypotheses and conclusion in the code panel fix its exact scope. Amplitude range needed by the one-signal diagonal construction.

theorem cubicAmplitude_le_one (n : Nat) (j : Fin (gridSize n)) :
    CubicStatePreparation.cubicAmplitude n j ≤ 1 := by

commit-pinned source · Verso Blueprint panel

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

theorem cubicAmplitude_nonneg (n : Nat) (j : Fin (gridSize n)) :
    0 ≤ CubicStatePreparation.cubicAmplitude n j := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “primitive amplitude oracle dimension”. Full matrix dimension of the unexpanded one-signal primitive oracle.

def primitiveAmplitudeOracleDimension (n : Nat) : Nat :=
  gridSize (n + (amplitudeOracleLayout n).auxiliaryQubits)

/--
External primitive matrix supplied by the oracle-label tier.

This is only a named object for the semantic contract below.  The current file
does not prove that this opaque matrix is a gate-expanded unitary.
-/

commit-pinned source · Verso Blueprint panel

This opaque declaration exposes the interface for “primitive amplitude oracle unitary” while keeping its implementation from unfolding automatically. External primitive matrix supplied by the oracle-label tier.

opaque primitiveAmplitudeOracleUnitary (n : Nat) :
    Matrix (primitiveAmplitudeOracleDimension n)
      (primitiveAmplitudeOracleDimension n) Rat

/-- Explicit unitarity obligation for the primitive oracle-label matrix. -/

commit-pinned source · Verso Blueprint panel

This opaque declaration exposes the interface for “primitive amplitude oracle is unitary” while keeping its implementation from unfolding automatically. Explicit unitarity obligation for the primitive oracle-label matrix.

opaque primitiveAmplitudeOracleIsUnitary (n : Nat)
    (unitary : Matrix (primitiveAmplitudeOracleDimension n)
      (primitiveAmplitudeOracleDimension n) Rat) : Prop

/-- Explicit clean-block extraction obligation for the primitive oracle-label matrix. -/

commit-pinned source · Verso Blueprint panel

This opaque declaration exposes the interface for “primitive amplitude oracle clean block extracts” while keeping its implementation from unfolding automatically. Explicit clean-block extraction obligation for the primitive oracle-label matrix.

opaque primitiveAmplitudeOracleCleanBlockExtracts (n : Nat)
    (unitary : Matrix (primitiveAmplitudeOracleDimension n)
      (primitiveAmplitudeOracleDimension n) Rat)
    (block : Matrix (gridSize n) (gridSize n) Rat) : Prop

/--
Primitive one-signal amplitude-oracle semantic contract.

This contract keeps the unexpanded primitive tier honest: it requires both a
unitarity obligation for the named oracle matrix and a clean-block extraction
obligation whose extracted block satisfies the diagonal target contract.

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “primitive amplitude oracle semantic contract”. Primitive one-signal amplitude-oracle semantic contract.

def primitiveAmplitudeOracleSemanticContract (n : Nat) : Prop :=
  primitiveAmplitudeOracleIsUnitary n (primitiveAmplitudeOracleUnitary n) ∧
    ∃ block : Matrix (gridSize n) (gridSize n) Rat,
      primitiveAmplitudeOracleCleanBlockExtracts n
        (primitiveAmplitudeOracleUnitary n) block ∧
        diagonalCleanBlockContract n block

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “primitive amplitude oracle semantic contract unitary”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem primitiveAmplitudeOracleSemanticContract_unitary
    (n : Nat) (h : primitiveAmplitudeOracleSemanticContract n) :
    primitiveAmplitudeOracleIsUnitary n (primitiveAmplitudeOracleUnitary n) :=
  h.1

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “primitive amplitude oracle semantic contract clean block eq target”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem primitiveAmplitudeOracleSemanticContract_cleanBlock_eq_target
    (n : Nat) (h : primitiveAmplitudeOracleSemanticContract n) :
    ∃ block : Matrix (gridSize n) (gridSize n) Rat,
      primitiveAmplitudeOracleCleanBlockExtracts n
        (primitiveAmplitudeOracleUnitary n) block ∧
        Matrix.PointwiseEq block (cubicDiagonalTarget n).operator := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “expanded amplitude oracle layout”. Expanded arithmetic route layout.

def expandedAmplitudeOracleLayout (n workspaceQubits : Nat) : RegisterLayout where
  systemQubits := n
  signalQubits := 1
  pureAncillas := workspaceQubits

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “expanded amplitude oracle layout auxiliary qubits”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem expandedAmplitudeOracleLayout_auxiliaryQubits
    (n workspaceQubits : Nat) :
    (expandedAmplitudeOracleLayout n workspaceQubits).auxiliaryQubits =
      1 + workspaceQubits := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “expanded amplitude oracle normalizer eq”; the hypotheses and conclusion in the code panel fix its exact scope. The expanded route targets the same exact normalizer 'alpha = 1'.

theorem expandedAmplitudeOracleNormalizer_eq (n _workspaceQubits : Nat) :
    exactNormalizer n = 1 := by

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “standard ry clean entry scalar tier”. A proposition-valued field is a requirement until a constructor supplies it. Scalar-tier contract for the standard 'R_y' clean-entry identity.

structure StandardRyCleanEntryScalarTier where
  Scalar : Type
  ratAmplitude : Rat -> Scalar
  thetaForAmplitude : Scalar -> Scalar
  cleanEntry : Scalar -> Scalar
  cleanEntry_of_range :
    ∀ a : Rat, 0 ≤ a -> a ≤ 1 ->
      cleanEntry (thetaForAmplitude (ratAmplitude a)) = ratAmplitude a
  thetaFormula : String := "theta = 2 * arccos(amplitude)"
  cleanEntryFormula : String := "cos(theta / 2)"

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “expanded ry clean entry for cubic amplitudes”. Indexwise clean-entry obligation for the cubic diagonal amplitudes in a chosen standard-'R_y' scalar tier.

def expandedRyCleanEntryForCubicAmplitudes
    (tier : StandardRyCleanEntryScalarTier) (n : Nat) : Prop :=
  ∀ j : Fin (gridSize n),
    tier.cleanEntry
        (tier.thetaForAmplitude
          (tier.ratAmplitude (CubicStatePreparation.cubicAmplitude n j))) =
      tier.ratAmplitude (CubicStatePreparation.cubicAmplitude n j)

/--
`DIAG-EXP-RY-001`: the standard scalar-tier `R_y` clean-entry contract applies
to every cubic grid amplitude because the existing Lean range lemmas prove

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “expanded ry clean entry for cubic amplitudes of standard tier”; the hypotheses and conclusion in the code panel fix its exact scope. 'DIAG-EXP-RY-001': the standard scalar-tier 'R_y' clean-entry contract applies to every cubic grid amplitude because the existing Lean range lemmas prove '0 <= (j / 2^n)^3 <= 1'.

theorem expandedRyCleanEntryForCubicAmplitudes_of_standardTier
    (tier : StandardRyCleanEntryScalarTier) (n : Nat) :
    expandedRyCleanEntryForCubicAmplitudes tier n := by

commit-pinned source · Verso Blueprint panel

This opaque declaration exposes the interface for “expanded arithmetic computes cubic amplitude” while keeping its implementation from unfolding automatically. Semantic obligation that the expanded reversible arithmetic computes 'a_j = (j / 2^n)^3' into the named workspace.

opaque expandedArithmeticComputesCubicAmplitude
    (n workspaceQubits : Nat) : Prop

/--
Backend-level shape for the expanded reversible arithmetic compute phase.

The structure records only the compute half of the route: starting from a
clean workspace, the backend returns the same system index together with a
workspace whose distinguished amplitude register contains
`CubicStatePreparation.cubicAmplitude n j`.  Clean uncompute remains the
separate obligation `expandedWorkspaceCleanUncomputed`.

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “expanded cubic arithmetic backend”. A proposition-valued field is a requirement until a constructor supplies it. Backend-level shape for the expanded reversible arithmetic compute phase.

structure ExpandedCubicArithmeticBackend (n workspaceQubits : Nat) where
  Workspace : Type
  workspaceQubitCount : Nat
  workspaceQubitCount_eq : workspaceQubitCount = workspaceQubits
  zeroWorkspace : Workspace
  amplitudeRegister : Workspace -> Rat
  compute : Fin (gridSize n) -> Workspace -> Fin (gridSize n) × Workspace

/--
Symbolic compute-phase backend for `DIAG-EXP-ARITH-BACKEND-001`.

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “symbolic expanded cubic arithmetic backend”. Symbolic compute-phase backend for 'DIAG-EXP-ARITH-BACKEND-001'.

def symbolicExpandedCubicArithmeticBackend (n workspaceQubits : Nat) :
    ExpandedCubicArithmeticBackend n workspaceQubits where
  Workspace := Rat
  workspaceQubitCount := workspaceQubits
  workspaceQubitCount_eq := rfl
  zeroWorkspace := 0
  amplitudeRegister := fun a => a
  compute := fun j _workspace =>
    (j, CubicStatePreparation.cubicAmplitude n j)

/--

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “expanded arithmetic backend computes cubic amplitude”. Pointwise arithmetic-backend semantics for 'DIAG-EXP-ARITH-001'.

def expandedArithmeticBackendComputesCubicAmplitude
    {n workspaceQubits : Nat}
    (backend : ExpandedCubicArithmeticBackend n workspaceQubits) : Prop :=
  backend.workspaceQubitCount = workspaceQubits ∧
    ∀ j : Fin (gridSize n),
      (backend.compute j backend.zeroWorkspace).1 = j ∧
        backend.amplitudeRegister ((backend.compute j backend.zeroWorkspace).2) =
          CubicStatePreparation.cubicAmplitude n j

/--
The symbolic backend satisfies the pointwise compute contract for every system

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “symbolic expanded cubic arithmetic backend computes”; the hypotheses and conclusion in the code panel fix its exact scope. The symbolic backend satisfies the pointwise compute contract for every system index.

theorem symbolicExpandedCubicArithmeticBackend_computes
    (n workspaceQubits : Nat) :
    expandedArithmeticBackendComputesCubicAmplitude
      (symbolicExpandedCubicArithmeticBackend n workspaceQubits) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “expanded arithmetic backend bridge”. Bridge obligation from a concrete arithmetic backend to the expanded route predicate.

def expandedArithmeticBackendBridge
    {n workspaceQubits : Nat}
    (backend : ExpandedCubicArithmeticBackend n workspaceQubits) : Prop :=
  expandedArithmeticBackendComputesCubicAmplitude backend ->
    expandedArithmeticComputesCubicAmplitude n workspaceQubits

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “expanded arithmetic computes cubic amplitude of backend bridge”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem expandedArithmeticComputesCubicAmplitude_of_backendBridge
    {n workspaceQubits : Nat}
    (backend : ExpandedCubicArithmeticBackend n workspaceQubits)
    (hBackend : expandedArithmeticBackendComputesCubicAmplitude backend)
    (hBridge : expandedArithmeticBackendBridge backend) :
    expandedArithmeticComputesCubicAmplitude n workspaceQubits :=
  hBridge hBackend

/--
General normal form for arithmetic backend bridge proof search.

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “expanded arithmetic backend bridge iff of computes”; the hypotheses and conclusion in the code panel fix its exact scope. General normal form for arithmetic backend bridge proof search.

theorem expandedArithmeticBackendBridge_iff_of_computes
    {n workspaceQubits : Nat}
    (backend : ExpandedCubicArithmeticBackend n workspaceQubits)
    (hBackend : expandedArithmeticBackendComputesCubicAmplitude backend) :
    expandedArithmeticBackendBridge backend ↔
      expandedArithmeticComputesCubicAmplitude n workspaceQubits := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “expanded arithmetic computes cubic amplitude of symbolic backend bridge”; the hypotheses and conclusion in the code panel fix its exact scope. Specialized conditional closure for the symbolic arithmetic backend.

theorem expandedArithmeticComputesCubicAmplitude_of_symbolicBackendBridge
    (n workspaceQubits : Nat)
    (hBridge :
      expandedArithmeticBackendBridge
        (symbolicExpandedCubicArithmeticBackend n workspaceQubits)) :
    expandedArithmeticComputesCubicAmplitude n workspaceQubits := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “symbolic expanded cubic arithmetic backend bridge iff”; the hypotheses and conclusion in the code panel fix its exact scope. Normal form for the symbolic arithmetic bridge obligation.

theorem symbolicExpandedCubicArithmeticBackend_bridge_iff
    (n workspaceQubits : Nat) :
    expandedArithmeticBackendBridge
        (symbolicExpandedCubicArithmeticBackend n workspaceQubits) ↔
      expandedArithmeticComputesCubicAmplitude n workspaceQubits := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “fixed denom cubic payload lt capacity”; the hypotheses and conclusion in the code panel fix its exact scope. 'DIAG-ARITH-FIXED-DENOM-CAP-001': the fixed-denominator cubic payload fits in the '3 * n'-qubit workspace register.

theorem fixedDenomCubicPayload_lt_capacity
    (n : Nat) (j : Fin (gridSize n)) :
    j.val ^ 3 < gridSize (3 * n) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “fixed denom cubic amplitude eq”; the hypotheses and conclusion in the code panel fix its exact scope. 'DIAG-ARITH-FIXED-DENOM-ALG-001': projecting the fixed-denominator payload 'j.val ^ 3' by the '3 * n'-qubit denominator recovers the cubic grid amplitude.

theorem fixedDenomCubicAmplitude_eq
    (n : Nat) (j : Fin (gridSize n)) :
    (j.val : Rat) ^ 3 / (gridSize (3 * n) : Rat) =
      CubicStatePreparation.cubicAmplitude n j := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “fixed denom cubic arithmetic backend”. 'DIAG-ARITH-FIXED-DENOM-BACKEND-001': concrete compute-phase backend whose '3 * n'-qubit workspace stores the fixed-denominator payload 'j.val ^ 3'.

def fixedDenomCubicArithmeticBackend (n : Nat) :
    ExpandedCubicArithmeticBackend n (3 * n) where
  Workspace := Fin (gridSize (3 * n))
  workspaceQubitCount := 3 * n
  workspaceQubitCount_eq := rfl
  zeroWorkspace := ⟨0, CubicStatePreparation.gridSize_pos (3 * n)⟩
  amplitudeRegister := fun payload =>
    (payload.val : Rat) / (gridSize (3 * n) : Rat)
  compute := fun j _workspace =>
    (j, ⟨j.val ^ 3, fixedDenomCubicPayload_lt_capacity n j⟩)

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “fixed denom cubic arithmetic backend computes”; the hypotheses and conclusion in the code panel fix its exact scope. Pointwise compute contract for the fixed-denominator arithmetic backend.

theorem fixedDenomCubicArithmeticBackend_computes
    (n : Nat) :
    expandedArithmeticBackendComputesCubicAmplitude
      (fixedDenomCubicArithmeticBackend n) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “expanded arithmetic computes cubic amplitude transparent”. Transparent arithmetic-route interface for 'DIAG-ARITH-ROUTE-TRANSPARENT-001'.

def expandedArithmeticComputesCubicAmplitudeTransparent
    (n workspaceQubits : Nat) : Prop :=
  Exists fun backend : ExpandedCubicArithmeticBackend n workspaceQubits =>
    expandedArithmeticBackendComputesCubicAmplitude backend

/--
Fixed-denominator witness for the transparent arithmetic route interface.

This packages the already compiled fixed-denominator backend and its pointwise
compute theorem.  It does not prove
`expandedArithmeticComputesCubicAmplitude n (3 * n)`.

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “fixed denom cubic arithmetic route transparent”; the hypotheses and conclusion in the code panel fix its exact scope. Fixed-denominator witness for the transparent arithmetic route interface.

theorem fixedDenomCubicArithmeticRouteTransparent
    (n : Nat) :
    expandedArithmeticComputesCubicAmplitudeTransparent n (3 * n) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “fixed denom cubic arithmetic backend bridge iff”; the hypotheses and conclusion in the code panel fix its exact scope. Fixed-denominator normal form for the arithmetic bridge obligation.

theorem fixedDenomCubicArithmeticBackend_bridge_iff
    (n : Nat) :
    expandedArithmeticBackendBridge (fixedDenomCubicArithmeticBackend n) ↔
      expandedArithmeticComputesCubicAmplitude n (3 * n) := by

commit-pinned source · Verso Blueprint panel

This opaque declaration exposes the interface for “expanded controlled ry uses cubic angle” while keeping its implementation from unfolding automatically. Semantic obligation for the standard 'R_y' convention on the signal qubit: for each basis index 'j', the route uses 'theta_j = 2 * arccos ((j / 2^n)^3)', so the clean entry is 'cos (theta_j / 2) = (j / 2^n)^3'.

opaque expandedControlledRyUsesCubicAngle
    (n workspaceQubits : Nat) : Prop

/--
Transparent controlled-`R_y` angle-convention interface for
`DIAG-RY-TRANSPARENT-INTERFACE-001`.

This records only the already compiled scalar clean-entry fact for every
standard tier.  It does not prove the opaque route predicate
`expandedControlledRyUsesCubicAngle`.
-/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “expanded controlled ry uses cubic angle transparent”. Transparent controlled-'R_y' angle-convention interface for 'DIAG-RY-TRANSPARENT-INTERFACE-001'.

def expandedControlledRyUsesCubicAngleTransparent
    (n _workspaceQubits : Nat) : Prop :=
  forall tier : StandardRyCleanEntryScalarTier,
    expandedRyCleanEntryForCubicAmplitudes tier n

/--
Fixed-denominator wrapper for the transparent controlled-`R_y` route.

This packages the scalar-tier theorem at workspace size `3 * n`.  It does not
provide a backend witness for `expandedControlledRyUsesCubicAngle`.
-/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “fixed denom controlled ry route transparent”; the hypotheses and conclusion in the code panel fix its exact scope. Fixed-denominator wrapper for the transparent controlled-'R_y' route.

theorem fixedDenomControlledRyRouteTransparent
    (n : Nat) :
    expandedControlledRyUsesCubicAngleTransparent n (3 * n) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “expanded controlled ry backend bridge”. Backend bridge obligation from the scalar-tier 'R_y' clean-entry interface to the expanded route predicate.

def expandedControlledRyBackendBridge
    (tier : StandardRyCleanEntryScalarTier)
    (n workspaceQubits : Nat) : Prop :=
  expandedRyCleanEntryForCubicAmplitudes tier n ->
    expandedControlledRyUsesCubicAngle n workspaceQubits

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “expanded controlled ry uses cubic angle of backend bridge”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem expandedControlledRyUsesCubicAngle_of_backendBridge
    (tier : StandardRyCleanEntryScalarTier)
    (n workspaceQubits : Nat)
    (hBridge : expandedControlledRyBackendBridge tier n workspaceQubits) :
    expandedControlledRyUsesCubicAngle n workspaceQubits :=
  hBridge (expandedRyCleanEntryForCubicAmplitudes_of_standardTier tier n)

/--
Normal form for controlled-rotation backend-bridge proof search.

The scalar-tier clean-entry theorem is already compiled, so proving a backend

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “expanded controlled ry backend bridge iff of standard tier”; the hypotheses and conclusion in the code panel fix its exact scope. Normal form for controlled-rotation backend-bridge proof search.

theorem expandedControlledRyBackendBridge_iff_of_standardTier
    (tier : StandardRyCleanEntryScalarTier)
    (n workspaceQubits : Nat) :
    expandedControlledRyBackendBridge tier n workspaceQubits ↔
      expandedControlledRyUsesCubicAngle n workspaceQubits := by

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “expanded controlled ry workspace readonly witness”. A proposition-valued field is a requirement until a constructor supplies it. Transparent readonly-rotation interface for 'DIAG-RY-WORKSPACE-READONLY-001'.

structure ExpandedControlledRyWorkspaceReadonlyWitness
    (n workspaceQubits : Nat) where
  backend : ExpandedCubicArithmeticBackend n workspaceQubits
  angleConvention :
    expandedControlledRyUsesCubicAngleTransparent n workspaceQubits
  rotationStep :
    Fin (gridSize n) -> backend.Workspace -> Fin 2 ->
      Prod (Prod (Fin (gridSize n)) backend.Workspace) (Fin 2)
  preserves_index :
    forall j w signal, (rotationStep j w signal).1.1 = j
  preserves_workspace :

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “expanded controlled ry workspace readonly transparent”. Transparent predicate for a controlled-rotation step that preserves the arithmetic workspace.

def expandedControlledRyWorkspaceReadonlyTransparent
    (n workspaceQubits : Nat) : Prop :=
  Nonempty (ExpandedControlledRyWorkspaceReadonlyWitness n workspaceQubits)

/-- Semantic obligation that the arithmetic workspace is returned clean. -/

commit-pinned source · Verso Blueprint panel

This opaque declaration exposes the interface for “expanded workspace clean uncomputed” while keeping its implementation from unfolding automatically. Semantic obligation that the arithmetic workspace is returned clean.

opaque expandedWorkspaceCleanUncomputed
    (n workspaceQubits : Nat) : Prop

/--
Transparent clean-uncompute interface for
`DIAG-EXP-UNCOMP-TRANSPARENT-INTERFACE-001`.

This records the data needed to state honest reversible cleanup: a compute step
matching the backend on clean workspace, an uncompute step that preserves the
system index, and a two-sided cleanup condition after compute.  It does not
prove the opaque route predicate `expandedWorkspaceCleanUncomputed`.

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “expanded arithmetic clean uncompute witness”. A proposition-valued field is a requirement until a constructor supplies it. Transparent clean-uncompute interface for 'DIAG-EXP-UNCOMP-TRANSPARENT-INTERFACE-001'.

structure ExpandedArithmeticCleanUncomputeWitness
    (n workspaceQubits : Nat) where
  backend : ExpandedCubicArithmeticBackend n workspaceQubits
  computes : expandedArithmeticBackendComputesCubicAmplitude backend
  computeStep :
    Fin (gridSize n) -> backend.Workspace ->
      Prod (Fin (gridSize n)) backend.Workspace
  uncomputeStep :
    Fin (gridSize n) -> backend.Workspace ->
      Prod (Fin (gridSize n)) backend.Workspace
  computeStep_matches_backend_on_clean :

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “expanded workspace clean uncomputed transparent”. Transparent cleanup predicate backed by an explicit reversible witness.

def expandedWorkspaceCleanUncomputedTransparent
    (n workspaceQubits : Nat) : Prop :=
  Nonempty (ExpandedArithmeticCleanUncomputeWitness n workspaceQubits)

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “expanded workspace clean uncomputed transparent of witness”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem expandedWorkspaceCleanUncomputedTransparent_of_witness
    {n workspaceQubits : Nat}
    (w : ExpandedArithmeticCleanUncomputeWitness n workspaceQubits) :
    expandedWorkspaceCleanUncomputedTransparent n workspaceQubits := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “fixed denom cubic compute step”. Fixed-denominator reversible compute lift for 'DIAG-EXP-UNCOMP-FIXED-DENOM-WITNESS-001'.

def fixedDenomCubicComputeStep (n : Nat) :
    Fin (gridSize n) -> (fixedDenomCubicArithmeticBackend n).Workspace ->
      Prod (Fin (gridSize n)) (fixedDenomCubicArithmeticBackend n).Workspace :=
  fun j workspace =>
    (j, ⟨(workspace.val + j.val ^ 3) % gridSize (3 * n),
      Nat.mod_lt _ (CubicStatePreparation.gridSize_pos (3 * n))⟩)

/-- Modular-subtract inverse for `fixedDenomCubicComputeStep`. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “fixed denom cubic uncompute step”. Modular-subtract inverse for 'fixedDenomCubicComputeStep'.

def fixedDenomCubicUncomputeStep (n : Nat) :
    Fin (gridSize n) -> (fixedDenomCubicArithmeticBackend n).Workspace ->
      Prod (Fin (gridSize n)) (fixedDenomCubicArithmeticBackend n).Workspace :=
  fun j workspace =>
    (j, ⟨(workspace.val + gridSize (3 * n) - j.val ^ 3) % gridSize (3 * n),
      Nat.mod_lt _ (CubicStatePreparation.gridSize_pos (3 * n))⟩)

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “fixed denom cubic compute step matches backend on clean”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem fixedDenomCubicComputeStep_matches_backend_on_clean
    (n : Nat) (j : Fin (gridSize n)) :
    fixedDenomCubicComputeStep n j
        (fixedDenomCubicArithmeticBackend n).zeroWorkspace =
      (fixedDenomCubicArithmeticBackend n).compute j
        (fixedDenomCubicArithmeticBackend n).zeroWorkspace := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “fixed denom cubic uncompute step after compute”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem fixedDenomCubicUncomputeStep_after_compute
    (n : Nat) (j : Fin (gridSize n))
    (workspace : (fixedDenomCubicArithmeticBackend n).Workspace) :
    fixedDenomCubicUncomputeStep n j
        (fixedDenomCubicComputeStep n j workspace).2 =
      (j, workspace) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “fixed denom expanded arithmetic clean uncompute witness”. Fixed-denominator witness for the transparent clean-uncompute interface.

def fixedDenomExpandedArithmeticCleanUncomputeWitness
    (n : Nat) : ExpandedArithmeticCleanUncomputeWitness n (3 * n) where
  backend := fixedDenomCubicArithmeticBackend n
  computes := fixedDenomCubicArithmeticBackend_computes n
  computeStep := fixedDenomCubicComputeStep n
  uncomputeStep := fixedDenomCubicUncomputeStep n
  computeStep_matches_backend_on_clean := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “fixed denom workspace clean uncomputed transparent”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem fixedDenomWorkspaceCleanUncomputedTransparent
    (n : Nat) :
    expandedWorkspaceCleanUncomputedTransparent n (3 * n) := by

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “linear diagonal value backend”. A proposition-valued field is a requirement until a constructor supplies it. Backend-level shape for computing the hinted linear diagonal value 'x_j = j / 2^n'.

structure LinearDiagonalValueBackend (n workspaceQubits : Nat) where
  Workspace : Type
  workspaceQubitCount : Nat
  workspaceQubitCount_eq : workspaceQubitCount = workspaceQubits
  zeroWorkspace : Workspace
  amplitudeRegister : Workspace -> Rat
  compute : Fin (gridSize n) -> Workspace -> Fin (gridSize n) × Workspace

/--
Pointwise value-computation contract for a linear diagonal backend.

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “linear diagonal value backend computes grid point”. Pointwise value-computation contract for a linear diagonal backend.

def linearDiagonalValueBackendComputesGridPoint
    {n workspaceQubits : Nat}
    (backend : LinearDiagonalValueBackend n workspaceQubits) : Prop :=
  backend.workspaceQubitCount = workspaceQubits ∧
    ∀ j : Fin (gridSize n),
      (backend.compute j backend.zeroWorkspace).1 = j ∧
        backend.amplitudeRegister ((backend.compute j backend.zeroWorkspace).2) =
          CubicStatePreparation.gridPoint n j

/--
Fixed-denominator value backend for `O_0`.

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “fixed denom linear diagonal value backend”. Fixed-denominator value backend for 'O_0'.

def fixedDenomLinearDiagonalValueBackend (n : Nat) :
    LinearDiagonalValueBackend n n where
  Workspace := Fin (gridSize n)
  workspaceQubitCount := n
  workspaceQubitCount_eq := rfl
  zeroWorkspace := ⟨0, CubicStatePreparation.gridSize_pos n⟩
  amplitudeRegister := fun payload =>
    (payload.val : Rat) / (gridSize n : Rat)
  compute := fun j _workspace =>
    (j, ⟨j.val, j.isLt⟩)

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “fixed denom linear diagonal value backend computes”; the hypotheses and conclusion in the code panel fix its exact scope. The fixed-denominator linear backend computes 'x_j = j / 2^n' on clean workspace.

theorem fixedDenomLinearDiagonalValueBackend_computes
    (n : Nat) :
    linearDiagonalValueBackendComputesGridPoint
      (fixedDenomLinearDiagonalValueBackend n) := by

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “linear diagonal value clean uncompute witness”. A proposition-valued field is a requirement until a constructor supplies it. Transparent cleanup witness for a linear value backend.

structure LinearDiagonalValueCleanUncomputeWitness
    (n workspaceQubits : Nat) where
  backend : LinearDiagonalValueBackend n workspaceQubits
  computes : linearDiagonalValueBackendComputesGridPoint backend
  computeStep :
    Fin (gridSize n) -> backend.Workspace ->
      Prod (Fin (gridSize n)) backend.Workspace
  uncomputeStep :
    Fin (gridSize n) -> backend.Workspace ->
      Prod (Fin (gridSize n)) backend.Workspace
  computeStep_matches_backend_on_clean :

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “linear diagonal workspace clean uncomputed transparent”. Transparent predicate for honest compute/uncompute cleanup of an 'O_0' value backend.

def linearDiagonalWorkspaceCleanUncomputedTransparent
    (n workspaceQubits : Nat) : Prop :=
  Nonempty (LinearDiagonalValueCleanUncomputeWitness n workspaceQubits)

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “linear diagonal workspace clean uncomputed transparent of witness”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem linearDiagonalWorkspaceCleanUncomputedTransparent_of_witness
    {n workspaceQubits : Nat}
    (w : LinearDiagonalValueCleanUncomputeWitness n workspaceQubits) :
    linearDiagonalWorkspaceCleanUncomputedTransparent n workspaceQubits := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “fixed denom linear diagonal compute step”. Modular-add compute step for the fixed-denominator linear backend.

def fixedDenomLinearDiagonalComputeStep (n : Nat) :
    Fin (gridSize n) -> (fixedDenomLinearDiagonalValueBackend n).Workspace ->
      Prod (Fin (gridSize n)) (fixedDenomLinearDiagonalValueBackend n).Workspace :=
  fun j workspace =>
    (j, ⟨(workspace.val + j.val) % gridSize n,
      Nat.mod_lt _ (CubicStatePreparation.gridSize_pos n)⟩)

/-- Modular-subtract inverse for `fixedDenomLinearDiagonalComputeStep`. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “fixed denom linear diagonal uncompute step”. Modular-subtract inverse for 'fixedDenomLinearDiagonalComputeStep'.

def fixedDenomLinearDiagonalUncomputeStep (n : Nat) :
    Fin (gridSize n) -> (fixedDenomLinearDiagonalValueBackend n).Workspace ->
      Prod (Fin (gridSize n)) (fixedDenomLinearDiagonalValueBackend n).Workspace :=
  fun j workspace =>
    (j, ⟨(workspace.val + gridSize n - j.val) % gridSize n,
      Nat.mod_lt _ (CubicStatePreparation.gridSize_pos n)⟩)

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “fixed denom linear diagonal compute step matches backend on clean”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem fixedDenomLinearDiagonalComputeStep_matches_backend_on_clean
    (n : Nat) (j : Fin (gridSize n)) :
    fixedDenomLinearDiagonalComputeStep n j
        (fixedDenomLinearDiagonalValueBackend n).zeroWorkspace =
      (fixedDenomLinearDiagonalValueBackend n).compute j
        (fixedDenomLinearDiagonalValueBackend n).zeroWorkspace := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “fixed denom linear diagonal uncompute step after compute”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem fixedDenomLinearDiagonalUncomputeStep_after_compute
    (n : Nat) (j : Fin (gridSize n))
    (workspace : (fixedDenomLinearDiagonalValueBackend n).Workspace) :
    fixedDenomLinearDiagonalUncomputeStep n j
        (fixedDenomLinearDiagonalComputeStep n j workspace).2 =
      (j, workspace) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “fixed denom linear diagonal clean uncompute witness”. Fixed-denominator cleanup witness for the hinted 'O_0' value backend.

def fixedDenomLinearDiagonalCleanUncomputeWitness
    (n : Nat) : LinearDiagonalValueCleanUncomputeWitness n n where
  backend := fixedDenomLinearDiagonalValueBackend n
  computes := fixedDenomLinearDiagonalValueBackend_computes n
  computeStep := fixedDenomLinearDiagonalComputeStep n
  uncomputeStep := fixedDenomLinearDiagonalUncomputeStep n
  computeStep_matches_backend_on_clean := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “fixed denom linear diagonal workspace clean uncomputed transparent”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem fixedDenomLinearDiagonalWorkspaceCleanUncomputedTransparent
    (n : Nat) :
    linearDiagonalWorkspaceCleanUncomputedTransparent n n := by

commit-pinned source · Verso Blueprint panel

This opaque declaration exposes the interface for “expanded amplitude oracle clean block extracts” while keeping its implementation from unfolding automatically. Clean-block extraction obligation for the expanded arithmetic/rotation route.

opaque expandedAmplitudeOracleCleanBlockExtracts
    (n workspaceQubits : Nat)
    (block : Matrix (gridSize n) (gridSize n) Rat) : Prop

/--
Expanded-route clean-block contract for `DIAG-EXPANDED-CONTRACT-001`.

This is an interface, not a proof of the expanded circuit.  It keeps the
transparent arithmetic witness, transparent controlled-rotation witness, and
clean-uncompute obligations explicit and requires the extracted clean block to
satisfy the existing diagonal contract.

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “expanded amplitude oracle clean block contract”. Expanded-route clean-block contract for 'DIAG-EXPANDED-CONTRACT-001'.

def expandedAmplitudeOracleCleanBlockContract
    (n workspaceQubits : Nat)
    (block : Matrix (gridSize n) (gridSize n) Rat) : Prop :=
  expandedArithmeticComputesCubicAmplitudeTransparent n workspaceQubits ∧
    expandedControlledRyUsesCubicAngleTransparent n workspaceQubits ∧
    expandedWorkspaceCleanUncomputed n workspaceQubits ∧
    expandedAmplitudeOracleCleanBlockExtracts n workspaceQubits block ∧
    diagonalCleanBlockContract n block

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “expanded amplitude oracle clean block contract diagonal”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem expandedAmplitudeOracleCleanBlockContract_diagonal
    (n workspaceQubits : Nat)
    (block : Matrix (gridSize n) (gridSize n) Rat)
    (h : expandedAmplitudeOracleCleanBlockContract n workspaceQubits block) :
    diagonalCleanBlockContract n block := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “expanded amplitude oracle clean block contract eq target”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem expandedAmplitudeOracleCleanBlockContract_eq_target
    (n workspaceQubits : Nat)
    (block : Matrix (gridSize n) (gridSize n) Rat)
    (h : expandedAmplitudeOracleCleanBlockContract n workspaceQubits block) :
    Matrix.PointwiseEq block (cubicDiagonalTarget n).operator := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “expanded amplitude oracle semantic contract”. Conditional semantic interface for an expanded arithmetic/rotation route with an explicit workspace size.

def expandedAmplitudeOracleSemanticContract
    (n workspaceQubits : Nat) : Prop :=
  ∃ block : Matrix (gridSize n) (gridSize n) Rat,
    expandedAmplitudeOracleCleanBlockContract n workspaceQubits block

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “expanded amplitude oracle semantic contract clean block eq target”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem expandedAmplitudeOracleSemanticContract_cleanBlock_eq_target
    (n workspaceQubits : Nat)
    (h : expandedAmplitudeOracleSemanticContract n workspaceQubits) :
    ∃ block : Matrix (gridSize n) (gridSize n) Rat,
      expandedAmplitudeOracleCleanBlockExtracts n workspaceQubits block ∧
        Matrix.PointwiseEq block (cubicDiagonalTarget n).operator := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “primitive amplitude oracle candidate”. Conditional candidate at the primitive oracle-label tier.

def primitiveAmplitudeOracleCandidate (n : Nat) :
    OperatorBlockEncodingCandidate Rat n where
  auxiliaryQubits := (amplitudeOracleLayout n).auxiliaryQubits
  target := cubicDiagonalTarget n
  unitary := primitiveAmplitudeOracleUnitary n
  layout := amplitudeOracleLayout n
  circuit := amplitudeOracleCircuit n
  resource := amplitudeOracleResource n
  layoutMatches := rfl
  isUnitary :=
    primitiveAmplitudeOracleIsUnitary n (primitiveAmplitudeOracleUnitary n)

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “primitive amplitude oracle candidate cost tuple eq”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem primitiveAmplitudeOracleCandidate_costTuple_eq (n : Nat) :
    ( (primitiveAmplitudeOracleCandidate n).cost.gateCount
    , (primitiveAmplitudeOracleCandidate n).cost.depth
    , (primitiveAmplitudeOracleCandidate n).cost.auxiliaryQubits
    , (primitiveAmplitudeOracleCandidate n).cost.oracleCalls
    ) = (1, 1, 1, 1) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “primitive amplitude oracle candidate unitary from contract”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem primitiveAmplitudeOracleCandidate_unitary_from_contract
    (n : Nat) (h : primitiveAmplitudeOracleSemanticContract n) :
    (primitiveAmplitudeOracleCandidate n).isUnitary := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “primitive amplitude oracle candidate block from contract”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem primitiveAmplitudeOracleCandidate_block_from_contract
    (n : Nat) (h : primitiveAmplitudeOracleSemanticContract n) :
    (primitiveAmplitudeOracleCandidate n).blockContainsTarget := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “primitive amplitude oracle verified”. Conditional exact certificate for the primitive oracle-label tier.

def primitiveAmplitudeOracleVerified
    (n : Nat) (h : primitiveAmplitudeOracleSemanticContract n) :
    VerifiedOperatorBlockEncoding Rat n where
  candidate := primitiveAmplitudeOracleCandidate n
  unitaryProof := primitiveAmplitudeOracleCandidate_unitary_from_contract n h
  blockProof := primitiveAmplitudeOracleCandidate_block_from_contract n h

/-- Human-facing construction claim for the first exact diagonal route. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “amplitude oracle claim”. Human-facing construction claim for the first exact diagonal route.

def amplitudeOracleClaim : ConstructionClaim where
  name := "diagonal-cubic-amplitude-oracle"
  source := "QBE-OP-CUBIC-DIAGONAL-001 exploratory exact candidate"
  target := "D_n = sum_j (j/2^n)^3 |j><j|"
  normalization := "alpha = 1"
  layout := "one signal qubit, no pure ancilla at the oracle-label tier"
  resource := {
    gates := CostExpr.atom "diag_cubic_amplitude_oracle"
    pureAncilla := 0
  }

commit-pinned source · Verso Blueprint panel