QuantumBlockEncoding/GHL2025.lean

This record groups the data and proof fields needed for “one term robin parameters”. A proposition-valued field is a requirement until a constructor supplies it.

structure OneTermRobinParameters where
  n : Nat
  kappa : Nat
  functionPieces : Nat
  polynomialDegreeCost : Nat
deriving Repr, DecidableEq

/--
Classical specification of the indicator oracle U_indic(K1,K2).
Returns `true` when row index `i` is in the bulk region [K1, K2],
meaning U_indic maps |i⟩|0⟩ → |i⟩|1⟩.

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “is bulk row”. Classical specification of the indicator oracle U_indic(K1,K2).

def isBulkRow (K1 K2 i : Nat) : Bool :=
  K1 ≤ i && i ≤ K2

/--
Complement of isBulkRow: returns true for boundary rows (j < K1 or K2 < j).
The paper's boundary set is {0,...,K1-1} union {K2+1,...,2^n-1}.
main.tex:1113, 1035-1038 --/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “is boundary row”. Complement of isBulkRow: returns true for boundary rows (j < K1 or K2 < j).

def isBoundaryRow (K1 K2 _gridSize : Nat) (j : Nat) : Bool :=
  j < K1 || K2 < j

/--
Detailed register partition matching the wavefunction ket labels
in Eq. ROBIN clarified (main.tex:1113-1117).
Each field is the qubit count for one register in the circuit.
Total signal qubits = m_f + 1 + ceil(log2 kappa) + 4 (indicator + ancilla + 1),
plus n system qubits. Pure ancillas appear in two groups totaling 2n.
figure:1_term_ROBIN caption --/

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “robin register partition”. A proposition-valued field is a requirement until a constructor supplies it. Detailed register partition matching the wavefunction ket labels in Eq.

structure RobinRegisterPartition where
  /-- m_f = ceil(log2 n) + ceil(log2 G_f) + 3 qubits for function oracle O_f.
  main.tex:1141 --/
  mfQubits : Nat
  /-- 1 indicator ancilla qubit set by U_indic. main.tex:1060-1065, 1113 --/
  indicatorQubit : Nat
  /-- ceil(log2 kappa) qubits for sparse index s. main.tex:1113 --/
  sparseIndexQubits : Nat
  /-- n - ceil(log2 kappa) qubits used as pure ancillas for O_D^BS register.
  main.tex:1113, 1149 --/
  odPureAncillaQubits : Nat

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “total qubits”. Total qubits used by the register partition (all registers summed).

def RobinRegisterPartition.totalQubits (rp : RobinRegisterPartition) : Nat :=
  rp.mfQubits + rp.indicatorQubit + rp.sparseIndexQubits +
  rp.odPureAncillaQubits + rp.systemQubits + rp.ancillaQubit

/--
Default register partition from concrete parameters.
figure:1_term_ROBIN --/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “default robin register partition”. Default register partition from concrete parameters.

def defaultRobinRegisterPartition (p : OneTermRobinParameters) : RobinRegisterPartition where
  mfQubits := clog2 p.n + clog2 p.functionPieces + 3
  indicatorQubit := 1
  sparseIndexQubits := clog2 p.kappa
  odPureAncillaQubits := p.n - clog2 p.kappa
  systemQubits := p.n
  ancillaQubit := 1

/--
Pure ancilla qubits visible in the Eq. ROBIN register partition:
`(n - ceil(log2 kappa)) + 1` from the O_D^BS register plus the trailing

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “total pure ancillas”. Pure ancilla qubits visible in the Eq.

def RobinRegisterPartition.totalPureAncillas (rp : RobinRegisterPartition) : Nat :=
  rp.odPureAncillaQubits + rp.ancillaQubit

/--
Theorem 1-term Robin resource shape:
`O(sum_g Q_g n log n + kappa n)` gates and `2n` pure ancillas.
-/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin resource expr”. Theorem 1-term Robin resource shape: 'O(sum_g Q_g n log n + kappa n)' gates and '2n' pure ancillas.

def oneTermRobinResourceExpr : AsymptoticResource where
  gates :=
    (CostExpr.atom "sum_g(Q_g)") * (CostExpr.atom "n") * (CostExpr.log (CostExpr.atom "n")) +
    (CostExpr.atom "kappa") * (CostExpr.atom "n")
  pureAncilla := (2 : CostExpr) * CostExpr.atom "n"

/-- Number of deviating (boundary) indices: K1 + 2^n - K2.
The paper notes this is O(1) as it depends on the finite-difference accuracy order.
main.tex:1092-1095 --/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “deviating indices”. Number of deviating (boundary) indices: K1 + 2^n - K2.

def deviatingIndices (K1 K2 gridSize : Nat) : Nat :=
  K1 + gridSize - K2

/--
Precise gate cost formula from the text (main.tex:1088-1089), before absorbing the
O(1) boundary deviation count into the Theorem's simplified formula.
`O(sum_g Q_g n log n + kappa * (K1 + 2^n - K2) * n)` gates.
The term `K1 + 2^n - K2` is the number of deviating rows, which is O(1).
main.tex:1088-1089 --/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin precise resource expr”. Precise gate cost formula from the text (main.tex:1088-1089), before absorbing the O(1) boundary deviation count into the Theorem's simplified formula.

def oneTermRobinPreciseResourceExpr : AsymptoticResource where
  gates :=
    (CostExpr.atom "sum_g(Q_g)") * (CostExpr.atom "n") * (CostExpr.log (CostExpr.atom "n")) +
    (CostExpr.atom "kappa") * (CostExpr.atom "(K1 + 2^n - K2)") * (CostExpr.atom "n")
  pureAncilla := (2 : CostExpr) * CostExpr.atom "n"

/-- deviatingIndices computes K1 + gridSize - K2, the number of boundary rows.
For the fourth-order stencil with K1=2, K2=gridSize(n)-3, this gives 2+3=5.
main.tex:1092-1095 --/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “deviating indices example”; the hypotheses and conclusion in the code panel fix its exact scope. deviatingIndices computes K1 + gridSize - K2, the number of boundary rows.

theorem deviatingIndices_example :
    deviatingIndices 2 (gridSize 3 - 3) (gridSize 3) = 5 := rfl

/-- Numeric resource useful for concrete search runs with fixed parameters. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin resource”. Numeric resource useful for concrete search runs with fixed parameters.

def oneTermRobinResource (p : OneTermRobinParameters) : Resource :=
  Resource.ofCounts
    (p.polynomialDegreeCost * p.n * clog2 p.n + p.kappa * p.n)
    0
    (2 * p.n)

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “one term robin pure ancilla”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem oneTermRobin_pureAncilla (p : OneTermRobinParameters) :
    (oneTermRobinResource p).pureAncilla = 2 * p.n := rfl

/--
Register layout for the one-term Robin block encoding.
Signal qubits = ⌈log₂ n⌉ + ⌈log₂ G_f⌉ + ⌈log₂ κ⌉ + 4
match the paper's Theorem (main.tex:1098-1109).
System qubits address `n` grid points; pure ancillas are workspace.
-/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin layout”. Register layout for the one-term Robin block encoding.

def oneTermRobinLayout (p : OneTermRobinParameters) : RegisterLayout where
  systemQubits := clog2 (gridSize p.n)
  signalQubits := clog2 p.n + clog2 p.functionPieces + clog2 p.kappa + 4
  pureAncillas := 2 * p.n

/--
Placeholder circuit for the one-term Robin block encoding.
Gate order matches Fig. 1_term_ROBIN (main.tex:1125-1163):
  1. U_indic sets bulk/boundary indicator ancilla.
  2. O_DT^S encodes D^T amplitudes (bulk) via sparse-amplitude oracle.
  3. Ry_boundary applies controlled rotations for boundary entries.

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin circuit”. Placeholder circuit for the one-term Robin block encoding.

def oneTermRobinCircuit : Circuit :=
  [ Gate.oracleCall "U_indic"
  , Gate.oracleCall "O_DT^S"
  , Gate.oracleCall "Ry_boundary"
  , Gate.oracleCall "O_D^BS"
  , Gate.oracleCall "O_f"
  , Gate.swap 0 0   -- placeholder qubit indices; SWAP is a native gate
  , Gate.oracleCall "(O_D^BS)^†"
  ]

/--

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin theorem facing fig 4 circuit”. Theorem-facing Fig.

def oneTermRobinTheoremFacingFig4Circuit : Circuit :=
  [ Gate.oracleCall "H_W^(kappa)"
  , Gate.oracleCall "U_indic"
  , Gate.oracleCall "O_DT^S"
  , Gate.oracleCall "Ry_boundary"
  , Gate.oracleCall "O_DT^BS"
  , Gate.oracleCall "U_indic^dagger"
  , Gate.oracleCall "O_f"
  , Gate.swap 0 0
  , Gate.oracleCall "(O_D^BS)^dagger"
  , Gate.oracleCall "(H_W^(kappa))^dagger"

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “one term robin theorem facing fig 4 circuit gate list”; the hypotheses and conclusion in the code panel fix its exact scope. The theorem-facing transcript exposes the source-correction slots explicitly.

theorem oneTermRobinTheoremFacingFig4Circuit_gateList :
    oneTermRobinTheoremFacingFig4Circuit =
      [ Gate.oracleCall "H_W^(kappa)"
      , Gate.oracleCall "U_indic"
      , Gate.oracleCall "O_DT^S"
      , Gate.oracleCall "Ry_boundary"
      , Gate.oracleCall "O_DT^BS"
      , Gate.oracleCall "U_indic^dagger"
      , Gate.oracleCall "O_f"
      , Gate.swap 0 0
      , Gate.oracleCall "(O_D^BS)^dagger"

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “one term robin active backend circuit gate list”; the hypotheses and conclusion in the code panel fix its exact scope. The active backend circuit remains the seven-gate product currently used by the finite matrix semantics.

theorem oneTermRobinActiveBackendCircuit_gateList :
    oneTermRobinCircuit =
      [ Gate.oracleCall "U_indic"
      , Gate.oracleCall "O_DT^S"
      , Gate.oracleCall "Ry_boundary"
      , Gate.oracleCall "O_D^BS"
      , Gate.oracleCall "O_f"
      , Gate.swap 0 0
      , Gate.oracleCall "(O_D^BS)^†"
      ] := rfl

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin normalizer”. Symbolic normalizer α = N_D · N_f · κ for the one-term Robin construction.

def oneTermRobinNormalizer : Coeff :=
  Coeff.mul (Coeff.mul (Coeff.symbol "N_D") (Coeff.symbol "N_f")) (Coeff.symbol "kappa")

/--
Block-encoding spec for the one-term Robin derivative operator.
Takes the target matrix as a parameter so the spec is reusable across different
stencil choices and boundary data without creating import cycles.
Normalizer: symbolic `N_D · N_f · κ`.
Error: zero (exact encoding, no approximation yet).
-/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin spec”. Block-encoding spec for the one-term Robin derivative operator.

def oneTermRobinSpec (p : OneTermRobinParameters)
    (mat : Matrix (gridSize p.n) (gridSize p.n) Coeff) :
    BlockEncodingSpec Coeff (gridSize p.n) (gridSize p.n) where
  matrix := mat
  normalizer := oneTermRobinNormalizer
  error := Coeff.rat 0
  layout := oneTermRobinLayout p
  circuit := oneTermRobinCircuit
  resource := oneTermRobinResource p

/-- The spec's pure ancilla matches the resource formula. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “one term robin spec ancilla”; the hypotheses and conclusion in the code panel fix its exact scope. The spec's pure ancilla matches the resource formula.

theorem oneTermRobinSpec_ancilla (p : OneTermRobinParameters)
    (mat : Matrix (gridSize p.n) (gridSize p.n) Coeff) :
    (oneTermRobinSpec p mat).resource.pureAncilla = 2 * p.n := rfl

/--
The spec's circuit local cost: the SWAP placeholder costs 3 CNOTs and each
unexpanded oracle call is counted as one unresolved call in the candidate score.
figure:1_term_ROBIN
-/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “one term robin spec circuit cost”; the hypotheses and conclusion in the code panel fix its exact scope. The spec's circuit local cost: the SWAP placeholder costs 3 CNOTs and each unexpanded oracle call is counted as one unresolved call in the candidate score.

theorem oneTermRobinSpec_circuitCost :
    Circuit.resource oneTermRobinCircuit = Resource.ofCountsWithDepth 0 3 6 0 9 := rfl

/-- Evaluating the symbolic normalizer `N_D · N_f · κ` under an environment gives
the product of the three symbol values. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “one term robin normalizer eval”; the hypotheses and conclusion in the code panel fix its exact scope. Evaluating the symbolic normalizer 'N_D · N_f · κ' under an environment gives the product of the three symbol values.

@[simp] theorem oneTermRobinNormalizer_eval (env : String → Rat) :
    Coeff.evalWith env oneTermRobinNormalizer = env "N_D" * env "N_f" * env "kappa" := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin claim”. The paper's one-term Robin block-encoding construction claim.

def oneTermRobinClaim : ConstructionClaim where
  name := "one-term-robin-block-encoding"
  source := "Guseynov-Huang-Liu 2025, Theorem one-term block-encoding"
  target := "A_k = f(x) * d^m/dx^m with Robin boundary corrections"
  normalization := "N_D * N_f * kappa"
  layout := "ceil(log2 n) + ceil(log2 G_f) + ceil(log2 kappa) + 4 signal qubits, 2n pure ancillas"
  resource := oneTermRobinResourceExpr

/-- One-dimensional Hamiltonian block-encoding resource shape. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one dim hamiltonian resource expr”. One-dimensional Hamiltonian block-encoding resource shape.

def oneDimHamiltonianResourceExpr : AsymptoticResource where
  gates :=
    CostExpr.atom "sum_g(Q_v_g) * n * log(n)" +
    CostExpr.sum "k < eta" (CostExpr.atom "kappa_k * n + sum_g(Q_fkg) * n * log(n)") +
    CostExpr.atom "n_xi * log(n_xi)"
  pureAncilla := (2 : CostExpr) * CostExpr.atom "n" + (2 : CostExpr)

/-- The paper's 1D Hamiltonian block-encoding construction claim. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one dim hamiltonian claim”. The paper's 1D Hamiltonian block-encoding construction claim.

def oneDimHamiltonianClaim : ConstructionClaim where
  name := "one-dimensional-pde-hamiltonian-block-encoding"
  source := "Guseynov-Huang-Liu 2025, Theorem one-dimensional block-encoding"
  target := "H = S1 tensor x_xi + S2 tensor I_xi"
  normalization := "O(kappa * ||H||_max)"
  layout := "ceil(log2 n_xi)+ceil(log2 n)+ceil(log2 G)+ceil(log2 kappa)+ceil(log2 eta)+7 signal qubits"
  resource := oneDimHamiltonianResourceExpr

/-- Multidimensional Hamiltonian block-encoding resource shape. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “multi dim hamiltonian resource expr”. Multidimensional Hamiltonian block-encoding resource shape.

def multiDimHamiltonianResourceExpr : AsymptoticResource where
  gates :=
    CostExpr.atom "M * Q_PET * G * Q * (d*n*log(n)+n_s*log(n_s))" +
    CostExpr.atom "n_xi * log(n_xi)" +
    CostExpr.atom "d * eta * kappa * n"
  pureAncilla := CostExpr.atom "O(n)"

/-- The paper's multidimensional Hamiltonian block-encoding construction claim. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “multi dim hamiltonian claim”. The paper's multidimensional Hamiltonian block-encoding construction claim.

def multiDimHamiltonianClaim : ConstructionClaim where
  name := "multidimensional-pde-hamiltonian-block-encoding"
  source := "Guseynov-Huang-Liu 2025, Theorem multi-dimensional block-encoding"
  target := "H = I tensor p_s tensor I_xi + S1^(d) tensor x_xi + S2^(d) tensor I_xi"
  normalization := "O(kappa * ||H||_max)"
  layout := "d*ceil(log2 n)+ceil(log2 n_s)+ceil(log2 n_xi)+ceil(log2 G)+ceil(log2 kappa)+ceil(log2 eta)+ceil(log2 M)+4d+5 signal qubits"
  resource := multiDimHamiltonianResourceExpr

/-- A proof obligation tracked by description and paper source anchor.
`proved` is `Bool` (not `Prop`) so that unproved obligations are honest data,
not mathematically false claims. main.tex --/

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “obligation record”. A proposition-valued field is a requirement until a constructor supplies it. A proof obligation tracked by description and paper source anchor.

structure ObligationRecord where
  description : String
  source : String
  proved : Bool := false
deriving Repr, DecidableEq

/-- Circuit skeleton matching Fig. 1_term_ROBIN (main.tex:1137-1167).
Each field corresponds to a labeled box or operation in the figure.
All oracles are recorded as symbolic names; their implementation is delegated
to separate oracle-contract structures. figure:1_term_ROBIN --/

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “robin circuit skeleton”. A proposition-valued field is a requirement until a constructor supplies it. Circuit skeleton matching Fig.

structure RobinCircuitSkeleton where
  /-- Bulk/boundary indicator unitary U_indic(K1,K2). main.tex:1088-1099 --/
  indicatorOracle : String
  /-- Bulk window lower bound K1. main.tex:1095 --/
  K1 : Nat
  /-- Bulk window upper bound K2. main.tex:1095 --/
  K2 : Nat
  /-- Sparse-amplitude oracle for transposed derivative D^T.
  Lemma 3 (main.tex:822-849). --/
  sparseAmplitudeOracleDT : String
  /-- Banded-sparse-access oracle for D. Lemma 1 (main.tex:784-801). --/

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “robin gamma 1”. A proposition-valued field is a requirement until a constructor supplies it. Eq.

structure RobinGamma1 where
  /-- Sparse index upper bound: s in {0, ..., kappa-1}. main.tex:1113 --/
  kappa : Nat
  /-- Bulk window lower bound. main.tex:1095, 1113 --/
  K1 : Nat
  /-- Bulk window upper bound. main.tex:1095, 1113 --/
  K2 : Nat
  /-- Grid size = 2^n. main.tex:1113 --/
  gridSize : Nat
  /-- Boundary normalizer N_D · sqrt(kappa) (symbolic).
  The boundary summation in gamma_1 is scaled by 1/(N_D · sqrt(kappa)). main.tex:1113 --/

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “robin gamma 2”. A proposition-valued field is a requirement until a constructor supplies it. Eq.

structure RobinGamma2 where
  /-- Sparse index upper bound. main.tex:1115 --/
  kappa : Nat
  /-- Bulk window lower bound. main.tex:1115 --/
  K1 : Nat
  /-- Bulk window upper bound. main.tex:1115 --/
  K2 : Nat
  /-- Grid size. main.tex:1115 --/
  gridSize : Nat
  /-- Normalization factor N_D * sqrt(kappa) (symbolic). main.tex:1115 --/
  normalizer : Coeff

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “robin gamma 3”. A proposition-valued field is a requirement until a constructor supplies it. Eq.

structure RobinGamma3 where
  /-- Sparse index upper bound. main.tex:1117 --/
  kappa : Nat
  /-- Bulk window lower bound. main.tex:1117 --/
  K1 : Nat
  /-- Bulk window upper bound. main.tex:1117 --/
  K2 : Nat
  /-- Grid size. main.tex:1117 --/
  gridSize : Nat
  /-- Normalization factor N_D * N_f * kappa (symbolic). main.tex:1117 --/
  normalizer : Coeff

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “robin wavefunction decomposition”. A proposition-valued field is a requirement until a constructor supplies it. Bundle of the three intermediate wavefunction states from Eq.

structure RobinWavefunctionDecomposition where
  /-- gamma_1: state after U_indic. main.tex:1113 --/
  gamma1 : RobinGamma1
  /-- gamma_2: state after sparse-amplitude oracle. main.tex:1115 --/
  gamma2 : RobinGamma2
  /-- gamma_3: state after function oracle O_f. main.tex:1117 --/
  gamma3 : RobinGamma3
  /-- The shared sparse index upper bound. --/
  kappa : Nat
  /-- The shared bulk window lower bound. --/
  K1 : Nat

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “default robin wavefunction decomposition”. Default wavefunction decomposition from concrete parameters.

def defaultRobinWavefunctionDecomposition (p : OneTermRobinParameters) : RobinWavefunctionDecomposition where
  gamma1 := {
    kappa := p.kappa
    K1 := 2
    K2 := gridSize p.n - 3
    gridSize := gridSize p.n
    boundaryNormalizer := Coeff.mul (Coeff.symbol "N_D") (Coeff.symbol "sqrt(kappa)")
    bulkNormalizer := Coeff.symbol "sqrt(kappa)"
    mfQubits := clog2 p.n + clog2 p.functionPieces + 3
  }
  gamma2 := {

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “robin proof obligations”. A proposition-valued field is a requirement until a constructor supplies it. Bundle of proof obligations for the one-term Robin block encoding.

structure RobinProofObligations where
  /-- U_indic is unitary and implements the bulk-window predicate. --/
  indicatorUnitary : ObligationRecord := {
    description := "U_indic(K1,K2) implements the bulk/boundary indicator correctly"
    source := "Guseynov-Huang-Liu 2025, U_indic definition and Fig. 1-term Robin, arXiv:2506.20478"
    proved := false
  }
  /-- Sparse-amplitude oracle O_D^S is unitary and encodes D^(s)/N_D. --/
  sparseAmplitudeOracleCorrect : ObligationRecord := {
    description := "O_DT^S prepares the D^T sparse-amplitude branch D_j^(s)/N_D from Lemma 3, Eq. (20)"
    source := "Guseynov-Huang-Liu 2025, Lemma 3, Eq. (20), arXiv:2506.20478"

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “default robin circuit skeleton”. Default circuit skeleton for the one-term Robin construction, with oracle names matching the paper's notation.

def defaultRobinCircuitSkeleton (p : OneTermRobinParameters) : RobinCircuitSkeleton where
  indicatorOracle := "U_indic"
  K1 := 2  -- depends on stencil accuracy order; main.tex:1095
  K2 := gridSize p.n - 3  -- symmetric boundary; main.tex:1095
  sparseAmplitudeOracleDT := "O_DT^S"
  bandedSparseAccessOracleD := "O_D^BS"
  bandedSparseAccessOracleD_dagger := "(O_D^BS)^†"
  controlledRyBoundary := "Ry_boundary"
  functionOracle := "O_f"
  swapOperation := "SWAP"
  mergeFrame := "merge"

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “banded sparse access paper contract”. A proposition-valued field is a requirement until a constructor supplies it. Paper-level source contract for the banded sparse-access oracle in Lemma 1.

structure BandedSparseAccessPaperContract where
  sourceAnchor : String
  rowRegisterQubits : Nat
  paddedZeroQubits : Nat
  sparseIndexQubits : Nat
  outputAddressQubits : Nat
  inputKet : String
  outputKet : String
  imageFormula : String
  cleanInputDomain : ObligationRecord
  widthCompatible : ObligationRecord

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “default banded sparse access paper contract”. Default Lemma 1 register contract for the one-term Robin parameters.

def defaultBandedSparseAccessPaperContract
    (p : OneTermRobinParameters) : BandedSparseAccessPaperContract where
  sourceAnchor := "Guseynov-Huang-Liu 2025, Lemma 1, arXiv:2506.20478"
  rowRegisterQubits := p.n
  paddedZeroQubits := p.n - clog2 p.kappa
  sparseIndexQubits := clog2 p.kappa
  outputAddressQubits := p.n
  inputKet := "|0>^(n-l)|s>^l|i>^n"
  outputKet := "|r_si>^n|i>^n"
  imageFormula := "r_si = r_s0 + i mod 2^n"
  cleanInputDomain := {

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “derivative oracle contract”. A proposition-valued field is a requirement until a constructor supplies it. Contract for the derivative oracle O_D: sparse-access oracle for the banded stencil matrix.

structure DerivativeOracleContract (n : Nat) where
  stencil : Stencil
  bandwidth : Nat
  matrix : Matrix (gridSize n) (gridSize n) Coeff
  /-- Obligation: O_D^BS correctly maps sparse indices to matrix entries.
  main.tex:784-801 --/
  sparseCorrect : ObligationRecord
  bandwidth_eq : bandwidth = stencil.width

/-- Contract for the function oracle O_f: amplitude oracle encoding f(x) on the
grid. Records the piece count, normalization bound, and a correctness obligation. main.tex:870-910 -/

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “function oracle contract”. A proposition-valued field is a requirement until a constructor supplies it. Contract for the function oracle O_f: amplitude oracle encoding f(x) on the grid.

structure FunctionOracleContract (n : Nat) where
  functionPieces : Nat
  normalizerBound : Coeff
  /-- Obligation: O_f correctly block-encodes f(x_j)/N_f on the grid.
  main.tex:870-910 --/
  amplitudeCorrect : ObligationRecord

/-- Resource for the derivative oracle O_D using the banded sparse-access formula
from Lemma 1 of Guseynov-Huang-Liu 2025. The half-bandwidth parameter is
`stencil.leftRadius` (assumes a symmetric stencil where leftRadius = rightRadius). -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “derivative oracle resource”. Resource for the derivative oracle O_D using the banded sparse-access formula from Lemma 1 of Guseynov-Huang-Liu 2025.

def derivativeOracleResource (n : Nat) (s : Stencil) : Resource :=
  bandedSparseAccessResource n s.leftRadius

/-- The derivative oracle's pure ancilla count is n - 1 (from Lemma 1). -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “derivative oracle resource pure ancilla”; the hypotheses and conclusion in the code panel fix its exact scope. The derivative oracle's pure ancilla count is n - 1 (from Lemma 1).

@[simp] theorem derivativeOracleResource_pureAncilla (n : Nat) (s : Stencil) :
    (derivativeOracleResource n s).pureAncilla = n - 1 := rfl

/-- Typed theorem data for Theorem one-term block-encoding (main.tex:1098-1109).
Captures the exact block-encoding tuple (α, m, a) from the paper:
  α = N_D · N_f · κ    (normalizer)
  m = ⌈log₂ n⌉ + ⌈log₂ G_f⌉ + ⌈log₂ κ⌉ + 4   (signal ancilla qubits)
  a = 0                (zero approximation error)
along with the gate-count and pure-ancilla resource claims. -/

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin theorem data”. A proposition-valued field is a requirement until a constructor supplies it. Typed theorem data for Theorem one-term block-encoding (main.tex:1098-1109).

structure OneTermRobinTheoremData where
  /-- Block-encoding normalizer α = N_D · N_f · κ. main.tex:1102 --/
  alpha : Coeff
  /-- Signal ancilla qubits m = ⌈log₂ n⌉ + ⌈log₂ G_f⌉ + ⌈log₂ κ⌉ + 4. main.tex:1102 --/
  signalQubits : Nat
  /-- Approximation error a = 0 (exact block encoding). main.tex:1098-1109 --/
  error : Coeff
  /-- Gate-count bound: O(∑_g Q_g n log n + κ n). main.tex:1105-1108 --/
  gatesBound : String
  /-- Pure ancilla qubits: 2n. main.tex:1107 --/
  pureAncillas : Nat

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “default one term robin theorem data”. Default theorem data instance from concrete parameters.

def defaultOneTermRobinTheoremData (p : OneTermRobinParameters) : OneTermRobinTheoremData where
  alpha := oneTermRobinNormalizer
  signalQubits := clog2 p.n + clog2 p.functionPieces + clog2 p.kappa + 4
  error := Coeff.rat 0
  gatesBound := "O(sum_g Q_g n log n + kappa n)"
  pureAncillas := 2 * p.n
  obligations := {}

/--
A controlled R_y rotation angle for a single boundary row entry.
The paper (Eq. angles for Ry, main.tex:1081-1083) defines:

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “robin boundary rotation angle”. A proposition-valued field is a requirement until a constructor supplies it. A controlled R_y rotation angle for a single boundary row entry.

structure RobinBoundaryRotationAngle where
  /-- Row index j (boundary row: j < K1 or j > K2). main.tex:1082 --/
  row : Nat
  /-- Sparse index s in {0,...,kappa-1}. main.tex:1082 --/
  sparseIndex : Nat
  /-- The matrix entry D_j^(s) being encoded. main.tex:1082 --/
  matrixEntry : Coeff
  /-- The argument to arccos: D_j^(s) / N_D (symbolic Coeff).
  The caller must ensure this evaluates to a value in [-1, 1].
  main.tex:1081-1083 --/
  arccosArgument : Coeff

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “robin boundary rotation set”. A proposition-valued field is a requirement until a constructor supplies it. The set of all boundary-controlled rotation angles for a given Robin construction.

structure RobinBoundaryRotationSet where
  /-- Bulk window lower bound. main.tex:1095 --/
  K1 : Nat
  /-- Bulk window upper bound. main.tex:1095 --/
  K2 : Nat
  /-- Grid size = 2^n. main.tex:1082 --/
  gridSize : Nat
  /-- Diagonal sparsity bound (number of nonzero entries per row). main.tex:1075 --/
  kappa : Nat
  /-- Normalizer N_D >= ||D||_max. main.tex:1085 --/
  normalizerND : Coeff

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “expected count”. Number of boundary rows = K1 + gridSize - K2.

def RobinBoundaryRotationSet.expectedCount (rs : RobinBoundaryRotationSet) : Nat :=
  rs.kappa * deviatingIndices rs.K1 rs.K2 rs.gridSize

commit-pinned source · Verso Blueprint panel

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

def importedClaims : List ConstructionClaim :=
  [oneTermRobinClaim, oneDimHamiltonianClaim, multiDimHamiltonianClaim]

/-! ## Gate matrix placeholders for the one-term Robin circuit

Each gate in `oneTermRobinCircuit` gets a placeholder `GateMatrix` record.
The placeholder matrices are identity matrices on the full Hilbert space;
each carries a `SemanticObligation` with `proved := false` tracking that
the real matrix implementation is still pending.
figure:1_term_ROBIN, main.tex:1125-1163 --/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin total qubits”. Total number of qubits in the one-term Robin circuit.

def oneTermRobinTotalQubits (p : OneTermRobinParameters) : Nat :=
  (defaultRobinRegisterPartition p).totalQubits

/--
Effective signal qubits: total circuit qubits minus the system register width.
This is the number of non-system qubits in the register partition.
main.tex:1098-1109 --/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “effective robin signal qubits”. Effective signal qubits: total circuit qubits minus the system register width.

def effectiveRobinSignalQubits (p : OneTermRobinParameters) : Nat :=
  (defaultRobinRegisterPartition p).totalQubits - clog2 (gridSize p.n)

/--
The theorem tuple uses the paper's signal-qubit count.

This is the block-encoding parameter
`ceil(log2 n) + ceil(log2 G_f) + ceil(log2 kappa) + 4`, not the number of
all non-system wires in the concrete circuit register partition.
Guseynov-Huang-Liu 2025, Theorem one-term block-encoding,
arXiv:2506.20478.

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “default one term robin theorem data signal qubits eq layout”; the hypotheses and conclusion in the code panel fix its exact scope. The theorem tuple uses the paper's signal-qubit count.

theorem defaultOneTermRobinTheoremData_signalQubits_eq_layout
    (p : OneTermRobinParameters) :
    (defaultOneTermRobinTheoremData p).signalQubits =
      (oneTermRobinLayout p).signalQubits := rfl

/--
The theorem tuple and the reusable layout record carry the same `2n`
pure-ancilla resource count.
-/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “default one term robin theorem data pure ancillas eq layout”; the hypotheses and conclusion in the code panel fix its exact scope. The theorem tuple and the reusable layout record carry the same '2n' pure-ancilla resource count.

theorem defaultOneTermRobinTheoremData_pureAncillas_eq_layout
    (p : OneTermRobinParameters) :
    (defaultOneTermRobinTheoremData p).pureAncillas =
      (oneTermRobinLayout p).pureAncillas := rfl

/--
The theorem tuple and concrete resource record carry the same `2n`
pure-ancilla count.
-/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “default one term robin theorem data pure ancillas eq resource”; the hypotheses and conclusion in the code panel fix its exact scope. The theorem tuple and concrete resource record carry the same '2n' pure-ancilla count.

theorem defaultOneTermRobinTheoremData_pureAncillas_eq_resource
    (p : OneTermRobinParameters) :
    (defaultOneTermRobinTheoremData p).pureAncillas =
      (oneTermRobinResource p).pureAncilla := rfl

/--
The concrete block projection has to project all non-system wires.

Compared with the theorem-level signal parameter, the circuit-level projection
also includes the visible padded `O_D^BS` pure-register qubits and the trailing
one-qubit ancilla in the register partition.  This is an arithmetic bridge

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “effective robin signal qubits eq layout signal plus visible workspace”; the hypotheses and conclusion in the code panel fix its exact scope. The concrete block projection has to project all non-system wires.

theorem effectiveRobinSignalQubits_eq_layout_signal_plus_visibleWorkspace
    (p : OneTermRobinParameters) :
    effectiveRobinSignalQubits p =
      (oneTermRobinLayout p).signalQubits +
        (defaultRobinRegisterPartition p).odPureAncillaQubits + 1 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “effective robin signal qubits eq theorem data signal plus visible workspace”; the hypotheses and conclusion in the code panel fix its exact scope. Same projection bridge, stated directly against the theorem-data tuple.

theorem effectiveRobinSignalQubits_eq_theoremData_signal_plus_visibleWorkspace
    (p : OneTermRobinParameters) :
    effectiveRobinSignalQubits p =
      (defaultOneTermRobinTheoremData p).signalQubits +
        (defaultRobinRegisterPartition p).odPureAncillaQubits + 1 := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “robin indicator bit position”. Bit position of the indicator qubit in the compound register.

def robinIndicatorBitPosition (p : OneTermRobinParameters) : Nat :=
  let rp := defaultRobinRegisterPartition p
  rp.ancillaQubit + rp.systemQubits + rp.odPureAncillaQubits + rp.sparseIndexQubits

/--
Column mapping for the banded sparse access oracle O_D^BS.
Returns the column index for sparse index s in row i of the Robin derivative matrix.

For bulk rows (K1 ≤ i ≤ K2): 5 entries, col(s,i) = i - 2 + s for s < 5.
For left boundary:
  - Row 0 (3 entries): col(s,0) = s for s < 3

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “robin sparse column map”. Column mapping for the banded sparse access oracle O_D^BS.

def robinSparseColumnMap (n s i : Nat) : Nat :=
  let N := gridSize n
  let K1 := 2
  let K2 := N - 3
  if K1 ≤ i ∧ i ≤ K2 then
    if s < 5 then i - 2 + s else i
  else if i = 0 then
    if s < 3 then s else i
  else if i = 1 then
    if s < 4 then s else i
  else if i = N - 2 then

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin global sparse offset”. Global sparse-slot offset table for the one-term Robin 'κ = 7' construction.

def oneTermRobinGlobalSparseOffset (n s : Nat) : Nat :=
  let N := gridSize n
  match s with
  | 0 => N - 2
  | 1 => N - 1
  | 2 => 0
  | 3 => 1
  | 4 => 2
  | 5 => N - 3
  | 6 => 3
  | _ => 0

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin global sparse address”. Global sparse-access address 'r_{si}=r_{s0}+i mod 2^n'.

def oneTermRobinGlobalSparseAddress (n s i : Nat) : Nat :=
  (oneTermRobinGlobalSparseOffset n s + i) % gridSize n

/-- The global sparse-slot address is always an `n`-bit row address. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “one term robin global sparse address lt grid size”; the hypotheses and conclusion in the code panel fix its exact scope. The global sparse-slot address is always an 'n'-bit row address.

theorem oneTermRobinGlobalSparseAddress_lt_gridSize
    (n s i : Nat) :
    oneTermRobinGlobalSparseAddress n s i < gridSize n := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin global sparse inverse slot”. Inverse sparse slot used by the post-SWAP cleanup candidate for the global offset table.

def oneTermRobinGlobalSparseInverseSlot (s : Nat) : Nat :=
  match s with
  | 0 => 4
  | 1 => 3
  | 2 => 2
  | 3 => 1
  | 4 => 0
  | 5 => 6
  | 6 => 5
  | _ => 2

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “one term robin global sparse inverse slot lt eight”; the hypotheses and conclusion in the code panel fix its exact scope. The global inverse-slot helper fits in the three-bit sparse register.

theorem oneTermRobinGlobalSparseInverseSlot_lt_eight (s : Nat) :
    oneTermRobinGlobalSparseInverseSlot s < 8 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “one term robin global sparse inverse slot lt seven”; the hypotheses and conclusion in the code panel fix its exact scope. The inverse sparse-slot helper stays in the active seven-slot table.

theorem oneTermRobinGlobalSparseInverseSlot_lt_seven
    {s : Nat} (hs : s < 7) :
    oneTermRobinGlobalSparseInverseSlot s < 7 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “one term robin global sparse inverse slot involutive of lt seven”; the hypotheses and conclusion in the code panel fix its exact scope. The inverse sparse-slot helper is an involution on the active 'κ = 7' slot set.

theorem oneTermRobinGlobalSparseInverseSlot_involutive_of_lt_seven
    {s : Nat} (hs : s < 7) :
    oneTermRobinGlobalSparseInverseSlot
        (oneTermRobinGlobalSparseInverseSlot s) = s := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “one term robin global sparse inverse slot injective of lt seven”; the hypotheses and conclusion in the code panel fix its exact scope. The inverse sparse-slot helper is injective on the active 'κ = 7' slot set.

theorem oneTermRobinGlobalSparseInverseSlot_injective_of_lt_seven
    {s t : Nat} (hs : s < 7) (ht : t < 7)
    (h : oneTermRobinGlobalSparseInverseSlot s =
      oneTermRobinGlobalSparseInverseSlot t) :
    s = t := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “one term robin global sparse address inverse slot address eq”; the hypotheses and conclusion in the code panel fix its exact scope. Global sparse-address roundtrip for the supplied inverse-slot helper.

theorem oneTermRobinGlobalSparseAddress_inverseSlot_address_eq
    {n s i : Nat} (hn : 3 ≤ n) (hs : s < 8) (hi : i < gridSize n) :
    oneTermRobinGlobalSparseAddress n (oneTermRobinGlobalSparseInverseSlot s)
        (oneTermRobinGlobalSparseAddress n s i) = i := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “one term robin global sparse offset lt grid size of lt seven”; the hypotheses and conclusion in the code panel fix its exact scope. Every active global sparse-slot offset is an 'n'-bit address when '3 ≤ n'.

theorem oneTermRobinGlobalSparseOffset_lt_gridSize_of_lt_seven
    {n s : Nat} (hn : 3 ≤ n) (hs : s < 7) :
    oneTermRobinGlobalSparseOffset n s < gridSize n := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “one term robin global sparse address comp eq mod offset sum”; the hypotheses and conclusion in the code panel fix its exact scope. Composing two global sparse-slot addresses is addition by the sum of their global offsets modulo the grid size.

theorem oneTermRobinGlobalSparseAddress_comp_eq_mod_offset_sum
    {n s t i : Nat} :
    oneTermRobinGlobalSparseAddress n t
        (oneTermRobinGlobalSparseAddress n s i) =
      (((oneTermRobinGlobalSparseOffset n t +
          oneTermRobinGlobalSparseOffset n s) % gridSize n) + i) %
        gridSize n := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “one term robin global sparse offset sum mod eq zero unique of lt seven”; the hypotheses and conclusion in the code panel fix its exact scope. If two active global sparse-slot offsets sum to zero modulo the grid, the first slot is the reverse slot of the second.

theorem oneTermRobinGlobalSparseOffset_sum_mod_eq_zero_unique_of_lt_seven
    {n s t : Nat} (hn : 3 ≤ n) (hs : s < 7) (ht : t < 7)
    (hzero :
      (oneTermRobinGlobalSparseOffset n t +
          oneTermRobinGlobalSparseOffset n s) % gridSize n = 0) :
    t = oneTermRobinGlobalSparseInverseSlot s := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “one term robin global sparse address inverse slot unique of lt seven”; the hypotheses and conclusion in the code panel fix its exact scope. Uniqueness of the reverse sparse slot for the corrected global-slot address.

theorem oneTermRobinGlobalSparseAddress_inverseSlot_unique_of_lt_seven
    {n s t i : Nat} (hn : 3 ≤ n) (hs : s < 7) (ht : t < 7)
    (hi : i < gridSize n)
    (h :
      oneTermRobinGlobalSparseAddress n t
          (oneTermRobinGlobalSparseAddress n s i) = i) :
    t = oneTermRobinGlobalSparseInverseSlot s := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “one term robin global sparse address same row injective of lt seven”; the hypotheses and conclusion in the code panel fix its exact scope. For a fixed in-range row, the corrected seven-slot global address table is injective in the sparse slot.

theorem oneTermRobinGlobalSparseAddress_same_row_injective_of_lt_seven
    {n s t i : Nat} (hn : 3 ≤ n) (hs : s < 7) (ht : t < 7)
    (hi : i < gridSize n)
    (h :
      oneTermRobinGlobalSparseAddress n s i =
        oneTermRobinGlobalSparseAddress n t i) :
    s = t := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “robin sparse column branch valid”. Row-dependent sparse-branch domain for the executable one-term Robin stencil.

def robinSparseColumnBranchValid (n s i : Nat) : Bool :=
  let N := gridSize n
  if 2 ≤ i ∧ i ≤ N - 3 then
    decide (s < 5)
  else if i = 0 then
    decide (s < 3)
  else if i = 1 then
    decide (s < 4)
  else if i = N - 2 then
    decide (s < 4)
  else if i = N - 1 then

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “robin sparse column branch valid boundary unused n 3”; the hypotheses and conclusion in the code panel fix its exact scope. The proposed valid-branch predicate separates the boundary unused branch that caused the recorded 'n = 3' collision, while the current executable map still sends both branches to the same address.

theorem robinSparseColumnBranchValid_boundaryUnused_n3 :
    robinSparseColumnBranchValid 3 0 0 = true ∧
      robinSparseColumnBranchValid 3 3 0 = false ∧
      robinSparseColumnMap 3 0 0 = robinSparseColumnMap 3 3 0 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “robin sparse column map lt grid size of row lt”; the hypotheses and conclusion in the code panel fix its exact scope. Proof-DAG block for the Lemma 1 address-range route.

theorem robinSparseColumnMap_lt_gridSize_of_row_lt
    {n s i : Nat} (hn : 2 ≤ n) (hi : i < gridSize n) :
    robinSparseColumnMap n s i < gridSize n := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “robin sparse reverse column index”. Candidate reverse sparse index for the one-term Robin stencil.

def robinSparseReverseColumnIndex (n target row : Nat) : Nat :=
  let N := gridSize n
  if row = 0 then target
  else if row = 1 then target
  else if 2 ≤ row ∧ row ≤ N - 3 then target + 2 - row
  else if row = N - 2 then target - (N - 4)
  else if row = N - 1 then target - (N - 3)
  else target

/-- Normal form for the leftmost row of the executable Robin sparse map. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “robin sparse column map zero”; the hypotheses and conclusion in the code panel fix its exact scope. Normal form for the leftmost row of the executable Robin sparse map.

@[simp] theorem robinSparseColumnMap_zero (n s : Nat) :
    robinSparseColumnMap n s 0 = if s < 3 then s else 0 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “robin sparse column map one”; the hypotheses and conclusion in the code panel fix its exact scope. Normal form for the second row of the executable Robin sparse map.

@[simp] theorem robinSparseColumnMap_one (n s : Nat) :
    robinSparseColumnMap n s 1 = if s < 4 then s else 1 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “robin sparse column map bulk”; the hypotheses and conclusion in the code panel fix its exact scope. Normal form for a bulk row of the executable Robin sparse map.

theorem robinSparseColumnMap_bulk (n s i : Nat)
    (hbulk : 2 ≤ i ∧ i ≤ gridSize n - 3) :
    robinSparseColumnMap n s i = if s < 5 then i - 2 + s else i := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “robin sparse column map right boundary prev”; the hypotheses and conclusion in the code panel fix its exact scope. Normal form for the penultimate row of the executable Robin sparse map.

theorem robinSparseColumnMap_rightBoundaryPrev {n s : Nat} (hn : 3 ≤ n) :
    robinSparseColumnMap n s (gridSize n - 2) =
      if s < 4 then gridSize n - 4 + s else gridSize n - 2 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “robin sparse column map right boundary last”; the hypotheses and conclusion in the code panel fix its exact scope. Normal form for the last row of the executable Robin sparse map.

theorem robinSparseColumnMap_rightBoundaryLast {n s : Nat} (hn : 3 ≤ n) :
    robinSparseColumnMap n s (gridSize n - 1) =
      if s < 3 then gridSize n - 3 + s else gridSize n - 1 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “robin sparse reverse column index zero”; the hypotheses and conclusion in the code panel fix its exact scope. Reverse-index normal form for row zero.

@[simp] theorem robinSparseReverseColumnIndex_zero (n target : Nat) :
    robinSparseReverseColumnIndex n target 0 = target := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “robin sparse reverse column index one”; the hypotheses and conclusion in the code panel fix its exact scope. Reverse-index normal form for row one.

@[simp] theorem robinSparseReverseColumnIndex_one (n target : Nat) :
    robinSparseReverseColumnIndex n target 1 = target := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “robin sparse reverse column index bulk”; the hypotheses and conclusion in the code panel fix its exact scope. Reverse-index normal form for a bulk row.

theorem robinSparseReverseColumnIndex_bulk (n target row : Nat)
    (hbulk : 2 ≤ row ∧ row ≤ gridSize n - 3) :
    robinSparseReverseColumnIndex n target row = target + 2 - row := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “robin sparse reverse column index right boundary prev”; the hypotheses and conclusion in the code panel fix its exact scope. Reverse-index normal form for the penultimate row.

theorem robinSparseReverseColumnIndex_rightBoundaryPrev
    {n target : Nat} (hn : 3 ≤ n) :
    robinSparseReverseColumnIndex n target (gridSize n - 2) =
      target - (gridSize n - 4) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “robin sparse reverse column index right boundary last”; the hypotheses and conclusion in the code panel fix its exact scope. Reverse-index normal form for the last row.

theorem robinSparseReverseColumnIndex_rightBoundaryLast
    {n target : Nat} (hn : 3 ≤ n) :
    robinSparseReverseColumnIndex n target (gridSize n - 1) =
      target - (gridSize n - 3) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “robin sparse reverse column roundtrip of lt eight”; the hypotheses and conclusion in the code panel fix its exact scope. The reverse sparse-index candidate is a left inverse for the executable one-term Robin column map on the three-bit sparse-index range used by the current one-term parameter family.

theorem robinSparseReverseColumnRoundtrip_of_lt_eight
    {n s i : Nat} (hn : 3 <= n) (hs : s < 8) (hi : i < gridSize n) :
    robinSparseColumnMap n
      (robinSparseReverseColumnIndex n i (robinSparseColumnMap n s i))
      (robinSparseColumnMap n s i) = i := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “robin sparse reverse column index lt eight of column map”; the hypotheses and conclusion in the code panel fix its exact scope. The reverse-index candidate stays inside the three-bit sparse register for columns produced by the executable one-term Robin map.

theorem robinSparseReverseColumnIndex_lt_eight_of_columnMap
    {n s i : Nat} (hn : 3 <= n) (hs : s < 8) (hi : i < gridSize n) :
    robinSparseReverseColumnIndex n i (robinSparseColumnMap n s i) < 8 := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “robin sparse reverse column roundtrip check”. Executable finite audit for the reverse-index candidate.

def robinSparseReverseColumnRoundtripCheck (n sparseBound : Nat) : Bool :=
  (List.range sparseBound).all (fun s =>
    (List.range (gridSize n)).all (fun i =>
      robinSparseColumnMap n
          (robinSparseReverseColumnIndex n i (robinSparseColumnMap n s i))
          (robinSparseColumnMap n s i) == i))

/--
Register values used by the faithful Lemma 1 `O_D^BS` contract.

The current compound-index convention stores the row register in bits

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “banded sparse access paper registers”. A proposition-valued field is a requirement until a constructor supplies it. Register values used by the faithful Lemma 1 'O_D^BS' contract.

structure BandedSparseAccessPaperRegisters where
  odRegisterValue : Nat
  paddedZeroValue : Nat
  sparseIndexValue : Nat
  rowValue : Nat
deriving Repr, DecidableEq

/--
Extract the Lemma 1 padded sparse-address and row registers from a compound
basis index.  This is a source-contract skeleton only; it does not alter the
interim `bandedSparseAccessMatrix` helper and does not prove unitarity.

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “banded sparse access paper registers”. Extract the Lemma 1 padded sparse-address and row registers from a compound basis index.

def bandedSparseAccessPaperRegisters (p : OneTermRobinParameters) (j : Nat) :
    BandedSparseAccessPaperRegisters :=
  let n := p.n
  let κbits := clog2 p.kappa
  let odPure := n - κbits
  let nMask := (1 <<< n) - 1
  let zeroMask := (1 <<< odPure) - 1
  let sparseMask := (1 <<< κbits) - 1
  let odValue := (j >>> (1 + n)) &&& nMask
  {
    odRegisterValue := odValue

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper registers row lt grid size”; the hypotheses and conclusion in the code panel fix its exact scope. The row field extracted for Lemma 1 is always an 'n'-bit row value.

theorem bandedSparseAccessPaperRegisters_row_lt_gridSize
    (p : OneTermRobinParameters) (j : Nat) :
    (bandedSparseAccessPaperRegisters p j).rowValue < gridSize p.n := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper registers sparse index value eq”; the hypotheses and conclusion in the code panel fix its exact scope. The sparse-index field is the high sparse slice of the full O_D register.

theorem bandedSparseAccessPaperRegisters_sparseIndexValue_eq
    (p : OneTermRobinParameters) (j : Nat) :
    (bandedSparseAccessPaperRegisters p j).sparseIndexValue =
      (((bandedSparseAccessPaperRegisters p j).odRegisterValue >>>
          (p.n - clog2 p.kappa)) &&& ((1 <<< clog2 p.kappa) - 1)) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper registers padded zero value eq”; the hypotheses and conclusion in the code panel fix its exact scope. The padded-zero field is the low padded slice of the full O_D register.

theorem bandedSparseAccessPaperRegisters_paddedZeroValue_eq
    (p : OneTermRobinParameters) (j : Nat) :
    (bandedSparseAccessPaperRegisters p j).paddedZeroValue =
      ((bandedSparseAccessPaperRegisters p j).odRegisterValue &&&
        ((1 <<< (p.n - clog2 p.kappa)) - 1)) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper registers sparse index lt”; the hypotheses and conclusion in the code panel fix its exact scope. The extracted sparse-index field always fits in its declared bit width.

theorem bandedSparseAccessPaperRegisters_sparseIndex_lt
    (p : OneTermRobinParameters) (j : Nat) :
    (bandedSparseAccessPaperRegisters p j).sparseIndexValue <
      (1 <<< clog2 p.kappa) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper registers od register value lt”; the hypotheses and conclusion in the code panel fix its exact scope. The extracted O_D register value always fits in its declared 'n'-bit block.

theorem bandedSparseAccessPaperRegisters_odRegisterValue_lt
    (p : OneTermRobinParameters) (j : Nat) :
    (bandedSparseAccessPaperRegisters p j).odRegisterValue < (1 <<< p.n) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “banded sparse access row dependent paper address”. Rejected row-dependent paper-address helper.

def bandedSparseAccessRowDependentPaperAddress
    (p : OneTermRobinParameters) (j : Nat) : Nat :=
  let regs := bandedSparseAccessPaperRegisters p j
  robinSparseColumnMap p.n regs.sparseIndexValue regs.rowValue

/--
Paper address value `r_si` for the one-term Robin sparse-access oracle.

The active address follows the global sparse-slot formula
`r_si = r_s0 + i mod 2^n`.  Boundary or zero-amplitude slots remain present in
the sparse register; the coefficient layer supplies zero values where needed.

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “banded sparse access paper address”. Paper address value 'r_si' for the one-term Robin sparse-access oracle.

def bandedSparseAccessPaperAddress (p : OneTermRobinParameters) (j : Nat) : Nat :=
  let regs := bandedSparseAccessPaperRegisters p j
  oneTermRobinGlobalSparseAddress p.n regs.sparseIndexValue regs.rowValue

/-- Executable check that the paper address `r_si` fits in the n-bit address register. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “banded sparse access paper address in range”. Executable check that the paper address 'r_si' fits in the n-bit address register.

def bandedSparseAccessPaperAddressInRange (p : OneTermRobinParameters) (j : Nat) : Bool :=
  decide (bandedSparseAccessPaperAddress p j < (1 <<< p.n))

/-- Boolean form of the executable `O_D^BS` address-range check. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper address in range iff”; the hypotheses and conclusion in the code panel fix its exact scope. Boolean form of the executable 'O_D^BS' address-range check.

theorem bandedSparseAccessPaperAddressInRange_iff
    (p : OneTermRobinParameters) (j : Nat) :
    bandedSparseAccessPaperAddressInRange p j = true ↔
      bandedSparseAccessPaperAddress p j < (1 <<< p.n) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper address lt grid size of two le”; the hypotheses and conclusion in the code panel fix its exact scope. The executable paper address is in range for the fourth-order grid regime '2 <= n'.

theorem bandedSparseAccessPaperAddress_lt_gridSize_of_two_le
    (p : OneTermRobinParameters) (j : Nat) (_hn : 2 ≤ p.n) :
    bandedSparseAccessPaperAddress p j < gridSize p.n := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper address in range eq true of two le”; the hypotheses and conclusion in the code panel fix its exact scope. The executable address-range Boolean evaluates to true for the fourth-order grid regime '2 <= n'.

theorem bandedSparseAccessPaperAddressInRange_eq_true_of_two_le
    (p : OneTermRobinParameters) (j : Nat) (hn : 2 ≤ p.n) :
    bandedSparseAccessPaperAddressInRange p j = true := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “banded sparse access paper image”. Executable Lemma 1 image skeleton for 'O_D^BS'.

def bandedSparseAccessPaperImage (p : OneTermRobinParameters) (j : Nat) : Nat :=
  let lowWidth := 1 + p.n
  let highWidth := 1 + 2 * p.n
  let lowBase := 2 ^ lowWidth
  let highBase := 2 ^ highWidth
  let lowPrefix := j % lowBase
  let highTail := j / highBase
  let address := bandedSparseAccessPaperAddress p j
  lowPrefix + address * lowBase + highTail * highBase

/--

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “banded sparse access row dependent paper image”. Rejected row-dependent image helper corresponding to the old active address.

def bandedSparseAccessRowDependentPaperImage
    (p : OneTermRobinParameters) (j : Nat) : Nat :=
  let lowWidth := 1 + p.n
  let highWidth := 1 + 2 * p.n
  let lowBase := 2 ^ lowWidth
  let highBase := 2 ^ highWidth
  let lowPrefix := j % lowBase
  let highTail := j / highBase
  let address := bandedSparseAccessRowDependentPaperAddress p j
  lowPrefix + address * lowBase + highTail * highBase

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper register value eq mod”; the hypotheses and conclusion in the code panel fix its exact scope. Bit-slice extraction as arithmetic division followed by an 'n'-bit remainder.

theorem bandedSparseAccessPaperRegisterValue_eq_mod
    (x offset n : Nat) :
    ((x >>> offset) &&& ((1 <<< n) - 1)) =
      (x / 2 ^ offset) % 2 ^ n := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper high width le total qubits”; the hypotheses and conclusion in the code panel fix its exact scope. The O_D^BS address block ends before the full one-term Robin basis width.

theorem bandedSparseAccessPaperHighWidth_le_totalQubits
    (p : OneTermRobinParameters) :
    1 + 2 * p.n ≤ oneTermRobinTotalQubits p := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper image low block lt high base of address lt”; the hypotheses and conclusion in the code panel fix its exact scope. The low block of the paper image fits below the high-tail boundary whenever the written O_D^BS address is an n-bit value.

theorem bandedSparseAccessPaperImage_lowBlock_lt_highBase_of_address_lt
    (p : OneTermRobinParameters) (j : Nat)
    (haddr : bandedSparseAccessPaperAddress p j < (1 <<< p.n)) :
    let lowWidth := 1 + p.n
    let highWidth := 1 + 2 * p.n
    let lowBase := 2 ^ lowWidth
    let highBase := 2 ^ highWidth
    let lowPrefix := j % lowBase
    let address := bandedSparseAccessPaperAddress p j
    lowPrefix + address * lowBase < highBase := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper image mod low base”; the hypotheses and conclusion in the code panel fix its exact scope. The paper image preserves the low ancilla-and-row block modulo its width.

theorem bandedSparseAccessPaperImage_mod_lowBase
    (p : OneTermRobinParameters) (j : Nat) :
    bandedSparseAccessPaperImage p j % 2 ^ (1 + p.n) =
      j % 2 ^ (1 + p.n) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper image div low base mod eq”; the hypotheses and conclusion in the code panel fix its exact scope. After shifting past the low block, the paper image exposes the written address modulo the n-bit O_D^BS register.

theorem bandedSparseAccessPaperImage_div_lowBase_mod_eq
    (p : OneTermRobinParameters) (j : Nat)
    (haddr : bandedSparseAccessPaperAddress p j < (1 <<< p.n)) :
    bandedSparseAccessPaperImage p j / 2 ^ (1 + p.n) % 2 ^ p.n =
      bandedSparseAccessPaperAddress p j := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper image lt qubit dim of address lt”; the hypotheses and conclusion in the code panel fix its exact scope. The executable paper image remains inside the full finite basis when the input column is in range and the written O_D^BS address is n-bit.

theorem bandedSparseAccessPaperImage_lt_qubitDim_of_address_lt
    (p : OneTermRobinParameters) (j : Nat)
    (hj : j < qubitDim (oneTermRobinTotalQubits p))
    (haddr : bandedSparseAccessPaperAddress p j < (1 <<< p.n)) :
    bandedSparseAccessPaperImage p j < qubitDim (oneTermRobinTotalQubits p) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “banded sparse access paper image fin”. Finite-basis index for the executable Lemma 1 'O_D^BS' paper image.

def bandedSparseAccessPaperImageFin
    (p : OneTermRobinParameters)
    (j : Fin (qubitDim (oneTermRobinTotalQubits p)))
    (haddr : bandedSparseAccessPaperAddress p j.val < (1 <<< p.n)) :
    Fin (qubitDim (oneTermRobinTotalQubits p)) :=
  ⟨bandedSparseAccessPaperImage p j.val,
    bandedSparseAccessPaperImage_lt_qubitDim_of_address_lt p j.val j.2 haddr⟩

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper image fin val”; the hypotheses and conclusion in the code panel fix its exact scope.

@[simp] theorem bandedSparseAccessPaperImageFin_val
    (p : OneTermRobinParameters)
    (j : Fin (qubitDim (oneTermRobinTotalQubits p)))
    (haddr : bandedSparseAccessPaperAddress p j.val < (1 <<< p.n)) :
    (bandedSparseAccessPaperImageFin p j haddr).val =
      bandedSparseAccessPaperImage p j.val := rfl

/-- Register extraction from the paper image preserves the row register. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper image row value eq”; the hypotheses and conclusion in the code panel fix its exact scope. Register extraction from the paper image preserves the row register.

theorem bandedSparseAccessPaperImage_rowValue_eq
    (p : OneTermRobinParameters) (j : Nat) :
    (bandedSparseAccessPaperRegisters p
      (bandedSparseAccessPaperImage p j)).rowValue =
      (bandedSparseAccessPaperRegisters p j).rowValue := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper image od register value eq”; the hypotheses and conclusion in the code panel fix its exact scope. Register extraction from the paper image reports the written O_D^BS address.

theorem bandedSparseAccessPaperImage_odRegisterValue_eq
    (p : OneTermRobinParameters) (j : Nat)
    (haddr : bandedSparseAccessPaperAddress p j < (1 <<< p.n)) :
    (bandedSparseAccessPaperRegisters p
      (bandedSparseAccessPaperImage p j)).odRegisterValue =
      bandedSparseAccessPaperAddress p j := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “banded sparse access paper high tail”. High signal/workspace bits above the n-bit 'O_D^BS' address register.

def bandedSparseAccessPaperHighTail (p : OneTermRobinParameters) (j : Nat) : Nat :=
  j >>> (1 + 2 * p.n)

/--
The arithmetic register-splice form of `bandedSparseAccessPaperImage` preserves
all bits above the `O_D^BS` address register when the written address is n-bit.

This is a proof-DAG block for Lemma 1 register safety.  It does not promote the
paper-level `noSpill` obligation because the parameter-family side conditions
are still tracked by `defaultBandedSparseAccessPaperContract`.
-/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper image high tail eq of address lt”; the hypotheses and conclusion in the code panel fix its exact scope. The arithmetic register-splice form of 'bandedSparseAccessPaperImage' preserves all bits above the 'O_D^BS' address register when the written address is n-bit.

theorem bandedSparseAccessPaperImage_highTail_eq_of_address_lt
    (p : OneTermRobinParameters) (j : Nat)
    (haddr : bandedSparseAccessPaperAddress p j < (1 <<< p.n)) :
    bandedSparseAccessPaperHighTail p (bandedSparseAccessPaperImage p j) =
      bandedSparseAccessPaperHighTail p j := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “banded sparse access paper image no spill”. Executable check that the paper-image skeleton does not write past the n-bit 'O_D^BS' address register into the indicator or 'm_f' bits above it.

def bandedSparseAccessPaperImageNoSpill (p : OneTermRobinParameters) (j : Nat) : Bool :=
  bandedSparseAccessPaperHighTail p (bandedSparseAccessPaperImage p j) ==
    bandedSparseAccessPaperHighTail p j

/--
Boolean form of the executable high-tail no-spill check.

The high-tail theorem above discharges this Boolean under an n-bit written
address, while the paper-level semantic obligation remains a separate flag.
-/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper image no spill iff”; the hypotheses and conclusion in the code panel fix its exact scope. Boolean form of the executable high-tail no-spill check.

theorem bandedSparseAccessPaperImageNoSpill_iff
    (p : OneTermRobinParameters) (j : Nat) :
    bandedSparseAccessPaperImageNoSpill p j = true ↔
      bandedSparseAccessPaperHighTail p (bandedSparseAccessPaperImage p j) =
        bandedSparseAccessPaperHighTail p j := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper image no spill eq true of address lt”; the hypotheses and conclusion in the code panel fix its exact scope. The no-spill Boolean follows from the executable n-bit address bound.

theorem bandedSparseAccessPaperImageNoSpill_eq_true_of_address_lt
    (p : OneTermRobinParameters) (j : Nat)
    (haddr : bandedSparseAccessPaperAddress p j < (1 <<< p.n)) :
    bandedSparseAccessPaperImageNoSpill p j = true := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper image no spill eq true of two le”; the hypotheses and conclusion in the code panel fix its exact scope. The no-spill Boolean is true in the fourth-order grid regime '2 <= n', reusing the address-range proof-DAG block.

theorem bandedSparseAccessPaperImageNoSpill_eq_true_of_two_le
    (p : OneTermRobinParameters) (j : Nat) (hn : 2 ≤ p.n) :
    bandedSparseAccessPaperImageNoSpill p j = true := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “banded sparse access paper clean input”. Clean-domain predicate for the Lemma 1 'O_D^BS' source equation.

def bandedSparseAccessPaperCleanInput (p : OneTermRobinParameters) (j : Nat) : Bool :=
  (bandedSparseAccessPaperRegisters p j).paddedZeroValue == 0

/--
Faithful sparse-slot range for the Lemma 1 `O_D^BS` source equation.

The paper source domain keeps the global slot `s` whenever `s < kappa`.
Whether a boundary coefficient is zero is handled by the amplitude layer, not
by deleting the sparse-register slot from the index oracle.
-/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “banded sparse access paper sparse index in kappa”. Faithful sparse-slot range for the Lemma 1 'O_D^BS' source equation.

def bandedSparseAccessPaperSparseIndexInKappa
    (p : OneTermRobinParameters) (j : Nat) : Bool :=
  decide ((bandedSparseAccessPaperRegisters p j).sparseIndexValue < p.kappa)

/--
Faithful clean source domain for the active global-slot `O_D^BS` address.

This predicate is the padded clean input from Lemma 1 together with the global
slot range `s < kappa`.  It supersedes the row-dependent nonzero-branch
classifier as the active source-domain contract for `bandedSparseAccessPaperImage`.
-/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “banded sparse access paper global slot source”. Faithful clean source domain for the active global-slot 'O_D^BS' address.

def bandedSparseAccessPaperGlobalSlotSource
    (p : OneTermRobinParameters) (j : Nat) : Bool :=
  bandedSparseAccessPaperCleanInput p j &&
    bandedSparseAccessPaperSparseIndexInKappa p j

/-- A faithful global-slot source column is clean in the padded O_D register. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper global slot source clean input eq true”; the hypotheses and conclusion in the code panel fix its exact scope. A faithful global-slot source column is clean in the padded O_D register.

theorem bandedSparseAccessPaperGlobalSlotSource_cleanInput_eq_true
    (p : OneTermRobinParameters) (j : Nat)
    (h : bandedSparseAccessPaperGlobalSlotSource p j = true) :
    bandedSparseAccessPaperCleanInput p j = true := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper global slot source sparse index lt kappa”; the hypotheses and conclusion in the code panel fix its exact scope. A faithful global-slot source column has sparse index below 'kappa'.

theorem bandedSparseAccessPaperGlobalSlotSource_sparseIndex_lt_kappa
    (p : OneTermRobinParameters) (j : Nat)
    (h : bandedSparseAccessPaperGlobalSlotSource p j = true) :
    (bandedSparseAccessPaperRegisters p j).sparseIndexValue < p.kappa := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper global slot source inverse slot injective”; the hypotheses and conclusion in the code panel fix its exact scope. Global-source wrapper for inverse-slot injectivity.

theorem bandedSparseAccessPaperGlobalSlotSource_inverseSlot_injective
    (p : OneTermRobinParameters) {j₁ j₂ : Nat}
    (hkappa : p.kappa = 7)
    (hsource₁ : bandedSparseAccessPaperGlobalSlotSource p j₁ = true)
    (hsource₂ : bandedSparseAccessPaperGlobalSlotSource p j₂ = true)
    (h :
      oneTermRobinGlobalSparseInverseSlot
          (bandedSparseAccessPaperRegisters p j₁).sparseIndexValue =
        oneTermRobinGlobalSparseInverseSlot
          (bandedSparseAccessPaperRegisters p j₂).sparseIndexValue) :
    (bandedSparseAccessPaperRegisters p j₁).sparseIndexValue =

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper address same row injective of global slot source”; the hypotheses and conclusion in the code panel fix its exact scope. Same-row injectivity of the active paper address on the global-slot source domain.

theorem bandedSparseAccessPaperAddress_same_row_injective_of_globalSlotSource
    (p : OneTermRobinParameters) {j₁ j₂ : Nat}
    (hn : 3 ≤ p.n) (hkappa : p.kappa = 7)
    (hsource₁ : bandedSparseAccessPaperGlobalSlotSource p j₁ = true)
    (hsource₂ : bandedSparseAccessPaperGlobalSlotSource p j₂ = true)
    (hrow :
      (bandedSparseAccessPaperRegisters p j₁).rowValue =
        (bandedSparseAccessPaperRegisters p j₂).rowValue)
    (haddr :
      bandedSparseAccessPaperAddress p j₁ =
        bandedSparseAccessPaperAddress p j₂) :

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “banded sparse access paper valid sparse branch”. Candidate row-dependent sparse-branch domain for a basis column of Lemma 1.

def bandedSparseAccessPaperValidSparseBranch
    (p : OneTermRobinParameters) (j : Nat) : Bool :=
  let regs := bandedSparseAccessPaperRegisters p j
  robinSparseColumnBranchValid p.n regs.sparseIndexValue regs.rowValue

/--
Candidate corrected clean source domain for Lemma 1: padded-zero input plus a
row-dependent valid sparse branch.  This is a rejected-model contract-audit
predicate only.  Use `bandedSparseAccessPaperGlobalSlotSource` for the active
global-slot source contract.
-/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “banded sparse access paper valid clean source”. Candidate corrected clean source domain for Lemma 1: padded-zero input plus a row-dependent valid sparse branch.

def bandedSparseAccessPaperValidCleanSource
    (p : OneTermRobinParameters) (j : Nat) : Bool :=
  bandedSparseAccessPaperCleanInput p j &&
    bandedSparseAccessPaperValidSparseBranch p j

/-- The corrected source-domain candidate implies the original clean input. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper valid clean source clean input eq true”; the hypotheses and conclusion in the code panel fix its exact scope. The corrected source-domain candidate implies the original clean input.

theorem bandedSparseAccessPaperValidCleanSource_cleanInput_eq_true
    (p : OneTermRobinParameters) (j : Nat)
    (h : bandedSparseAccessPaperValidCleanSource p j = true) :
    bandedSparseAccessPaperCleanInput p j = true := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper valid clean source valid sparse branch eq true”; the hypotheses and conclusion in the code panel fix its exact scope. The corrected source-domain candidate implies a valid sparse branch.

theorem bandedSparseAccessPaperValidCleanSource_validSparseBranch_eq_true
    (p : OneTermRobinParameters) (j : Nat)
    (h : bandedSparseAccessPaperValidCleanSource p j = true) :
    bandedSparseAccessPaperValidSparseBranch p j = true := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper valid clean source separates boundary collision n 3”; the hypotheses and conclusion in the code panel fix its exact scope. The row-dependent valid-source audit excludes the concrete unused sparse branch from the recorded 'n = 3', 'kappa = 7' rejected-model collision.

theorem bandedSparseAccessPaperValidCleanSource_separates_boundaryCollision_n3 :
    let p : OneTermRobinParameters :=
      { n := 3, kappa := 7, functionPieces := 1, polynomialDegreeCost := 1 }
    bandedSparseAccessPaperCleanInput p 0 = true ∧
      bandedSparseAccessPaperCleanInput p 48 = true ∧
      bandedSparseAccessPaperValidSparseBranch p 0 = true ∧
      bandedSparseAccessPaperValidSparseBranch p 48 = false ∧
      bandedSparseAccessPaperValidCleanSource p 0 = true ∧
      bandedSparseAccessPaperValidCleanSource p 48 = false ∧
      bandedSparseAccessRowDependentPaperImage p 0 =
        bandedSparseAccessRowDependentPaperImage p 48 ∧

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “banded sparse access paper unused sparse branch”. Classifier for clean padded-register columns whose sparse branch is invalid for the row-dependent Robin stencil.

def bandedSparseAccessPaperUnusedSparseBranch
    (p : OneTermRobinParameters) (j : Nat) : Bool :=
  bandedSparseAccessPaperCleanInput p j &&
    !bandedSparseAccessPaperValidSparseBranch p j

/-- An unused sparse branch is still in the padded clean-input domain. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper unused sparse branch clean input eq true”; the hypotheses and conclusion in the code panel fix its exact scope. An unused sparse branch is still in the padded clean-input domain.

theorem bandedSparseAccessPaperUnusedSparseBranch_cleanInput_eq_true
    (p : OneTermRobinParameters) (j : Nat)
    (h : bandedSparseAccessPaperUnusedSparseBranch p j = true) :
    bandedSparseAccessPaperCleanInput p j = true := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper unused sparse branch valid sparse branch eq false”; the hypotheses and conclusion in the code panel fix its exact scope. An unused sparse branch is outside the row-dependent valid-branch classifier.

theorem bandedSparseAccessPaperUnusedSparseBranch_validSparseBranch_eq_false
    (p : OneTermRobinParameters) (j : Nat)
    (h : bandedSparseAccessPaperUnusedSparseBranch p j = true) :
    bandedSparseAccessPaperValidSparseBranch p j = false := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper clean domain split iff”; the hypotheses and conclusion in the code panel fix its exact scope. The executable clean padded-input domain splits into valid sparse branches and clean unused sparse branches.

theorem bandedSparseAccessPaperCleanDomainSplit_iff
    (p : OneTermRobinParameters) (j : Nat) :
    bandedSparseAccessPaperCleanInput p j = true ↔
      bandedSparseAccessPaperValidCleanSource p j = true ∨
        bandedSparseAccessPaperUnusedSparseBranch p j = true := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper clean domain split disjoint”; the hypotheses and conclusion in the code panel fix its exact scope. The two branches in 'bandedSparseAccessPaperCleanDomainSplit_iff' are disjoint.

theorem bandedSparseAccessPaperCleanDomainSplit_disjoint
    (p : OneTermRobinParameters) (j : Nat) :
    ¬ (bandedSparseAccessPaperValidCleanSource p j = true ∧
        bandedSparseAccessPaperUnusedSparseBranch p j = true) := by

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “banded sparse access unused branch image rule contract”. A proposition-valued field is a requirement until a constructor supplies it. Interface for the missing reversible image rule on clean unused sparse branches.

structure BandedSparseAccessUnusedBranchImageRuleContract where
  sourceAnchor : String
  sourceIndex : Nat
  inputRegisters : BandedSparseAccessPaperRegisters
  activeImageIndex : Nat
  proposedImageIndex : Option Nat
  cleanInput : Bool
  validSparseBranch : Bool
  unusedSparseBranch : Bool
  imageSpecified : ObligationRecord
  imageFinite : ObligationRecord

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “banded sparse access unused branch image rule contract”. Default image-rule interface for one unused-branch source column.

def bandedSparseAccessUnusedBranchImageRuleContract
    (p : OneTermRobinParameters) (j : Nat) :
    BandedSparseAccessUnusedBranchImageRuleContract where
  sourceAnchor := "Guseynov-Huang-Liu 2025, Lemma 1 and one-term Robin zero-branch audit, arXiv:2506.20478"
  sourceIndex := j
  inputRegisters := bandedSparseAccessPaperRegisters p j
  activeImageIndex := bandedSparseAccessPaperImage p j
  proposedImageIndex := none
  cleanInput := bandedSparseAccessPaperCleanInput p j
  validSparseBranch := bandedSparseAccessPaperValidSparseBranch p j
  unusedSparseBranch := bandedSparseAccessPaperUnusedSparseBranch p j

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access unused branch image rule contract flags false”; the hypotheses and conclusion in the code panel fix its exact scope. The unused-branch image-rule interface is obligation-only in Phase 1.

theorem bandedSparseAccessUnusedBranchImageRuleContract_flags_false
    (p : OneTermRobinParameters) (j : Nat) :
    (bandedSparseAccessUnusedBranchImageRuleContract p j).proposedImageIndex = none ∧
      (bandedSparseAccessUnusedBranchImageRuleContract p j).imageSpecified.proved = false ∧
      (bandedSparseAccessUnusedBranchImageRuleContract p j).imageFinite.proved = false ∧
      (bandedSparseAccessUnusedBranchImageRuleContract p j).separatesActiveCollision.proved = false ∧
      (bandedSparseAccessUnusedBranchImageRuleContract p j).validBranchAgreement.proved = false := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access unused branch image rule contract of unused branch”; the hypotheses and conclusion in the code panel fix its exact scope. Classifier bridge for the unused-branch image-rule interface.

theorem bandedSparseAccessUnusedBranchImageRuleContract_of_unusedBranch
    (p : OneTermRobinParameters) (j : Nat)
    (h : bandedSparseAccessPaperUnusedSparseBranch p j = true) :
    (bandedSparseAccessUnusedBranchImageRuleContract p j).cleanInput = true ∧
      (bandedSparseAccessUnusedBranchImageRuleContract p j).validSparseBranch = false ∧
      (bandedSparseAccessUnusedBranchImageRuleContract p j).unusedSparseBranch = true ∧
      (bandedSparseAccessUnusedBranchImageRuleContract p j).proposedImageIndex = none ∧
      (bandedSparseAccessUnusedBranchImageRuleContract p j).imageSpecified.proved = false ∧
      (bandedSparseAccessUnusedBranchImageRuleContract p j).validBranchAgreement.proved = false := by

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “banded sparse access unused branch extension contract”. A proposition-valued field is a requirement until a constructor supplies it. Contract slot for a faithful reversible extension on unused sparse branches.

structure BandedSparseAccessUnusedBranchExtensionContract where
  sourceAnchor : String
  inputRegisters : BandedSparseAccessPaperRegisters
  activeImageIndex : Nat
  cleanInput : Bool
  validSparseBranch : Bool
  unusedSparseBranch : Bool
  unusedBranchImageRuleContract : BandedSparseAccessUnusedBranchImageRuleContract
  paperAgreementOnValidBranches : ObligationRecord
  unusedBranchImageRule : ObligationRecord
  unusedBranchInjective : ObligationRecord

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “banded sparse access unused branch extension contract”. Default unused-branch extension contract for one O_D^BS basis column.

def bandedSparseAccessUnusedBranchExtensionContract
    (p : OneTermRobinParameters) (j : Nat) :
    BandedSparseAccessUnusedBranchExtensionContract where
  sourceAnchor := "Guseynov-Huang-Liu 2025, Lemma 1 and one-term Robin zero-branch audit, arXiv:2506.20478"
  inputRegisters := bandedSparseAccessPaperRegisters p j
  activeImageIndex := bandedSparseAccessPaperImage p j
  cleanInput := bandedSparseAccessPaperCleanInput p j
  validSparseBranch := bandedSparseAccessPaperValidSparseBranch p j
  unusedSparseBranch := bandedSparseAccessPaperUnusedSparseBranch p j
  unusedBranchImageRuleContract :=
    bandedSparseAccessUnusedBranchImageRuleContract p j

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access unused branch extension contract flags false”; the hypotheses and conclusion in the code panel fix its exact scope. The unused-branch extension contract is obligation-only in Phase 1.

theorem bandedSparseAccessUnusedBranchExtensionContract_flags_false
    (p : OneTermRobinParameters) (j : Nat) :
    (bandedSparseAccessUnusedBranchExtensionContract p j).paperAgreementOnValidBranches.proved = false ∧
      (bandedSparseAccessUnusedBranchExtensionContract p j).unusedBranchImageRule.proved = false ∧
      (bandedSparseAccessUnusedBranchExtensionContract p j).unusedBranchInjective.proved = false ∧
      (bandedSparseAccessUnusedBranchExtensionContract p j).fullCleanDomainInjective.proved = false ∧
      (bandedSparseAccessUnusedBranchExtensionContract p j).daggerCleanup.proved = false ∧
      (bandedSparseAccessUnusedBranchExtensionContract p j).unitaryExtension.proved = false := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access unused branch extension contract boundary collision n 3”; the hypotheses and conclusion in the code panel fix its exact scope. The unused-branch contract classifies the recorded row-dependent boundary collision without promoting any O_D^BS semantic proof flag.

theorem bandedSparseAccessUnusedBranchExtensionContract_boundaryCollision_n3 :
    let p : OneTermRobinParameters :=
      { n := 3, kappa := 7, functionPieces := 1, polynomialDegreeCost := 1 }
    bandedSparseAccessPaperValidCleanSource p 0 = true ∧
      bandedSparseAccessPaperUnusedSparseBranch p 48 = true ∧
      bandedSparseAccessRowDependentPaperImage p 0 =
        bandedSparseAccessRowDependentPaperImage p 48 ∧
      bandedSparseAccessPaperImage p 0 ≠ bandedSparseAccessPaperImage p 48 ∧
      (bandedSparseAccessUnusedBranchExtensionContract p 48).unusedBranchInjective.proved = false ∧
      (bandedSparseAccessUnusedBranchExtensionContract p 48).unitaryExtension.proved = false := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access unused branch extension contract of unused branch”; the hypotheses and conclusion in the code panel fix its exact scope. Package the unused-branch classifier with the reversible-extension obligations.

theorem bandedSparseAccessUnusedBranchExtensionContract_of_unusedBranch
    (p : OneTermRobinParameters) (j : Nat)
    (h : bandedSparseAccessPaperUnusedSparseBranch p j = true) :
    (bandedSparseAccessUnusedBranchExtensionContract p j).cleanInput = true ∧
      (bandedSparseAccessUnusedBranchExtensionContract p j).validSparseBranch = false ∧
      (bandedSparseAccessUnusedBranchExtensionContract p j).unusedSparseBranch = true ∧
      (bandedSparseAccessUnusedBranchExtensionContract p j).unusedBranchImageRule.proved = false ∧
      (bandedSparseAccessUnusedBranchExtensionContract p j).unusedBranchInjective.proved = false ∧
      (bandedSparseAccessUnusedBranchExtensionContract p j).fullCleanDomainInjective.proved = false ∧
      (bandedSparseAccessUnusedBranchExtensionContract p j).daggerCleanup.proved = false ∧
      (bandedSparseAccessUnusedBranchExtensionContract p j).unitaryExtension.proved = false := by

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “banded sparse access full clean domain extension contract”. A proposition-valued field is a requirement until a constructor supplies it. Paper-level wrapper for the full clean-domain extension obligation of 'O_D^BS'.

structure BandedSparseAccessFullCleanDomainExtensionContract where
  sourceAnchor : String
  cleanInputPredicate : String
  validSparseBranchPredicate : String
  validCleanSourcePredicate : String
  unusedSparseBranchPredicate : String
  unusedBranchImageRuleContract :
    Nat → BandedSparseAccessUnusedBranchImageRuleContract
  unusedBranchExtensionContract :
    Nat → BandedSparseAccessUnusedBranchExtensionContract
  cleanDomainSplit : ObligationRecord

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “banded sparse access full clean domain extension contract”. Default full clean-domain extension contract for Lemma 1 'O_D^BS'.

def bandedSparseAccessFullCleanDomainExtensionContract
    (p : OneTermRobinParameters) :
    BandedSparseAccessFullCleanDomainExtensionContract where
  sourceAnchor := "Guseynov-Huang-Liu 2025, Lemma 1 and one-term Robin zero-branch audit, arXiv:2506.20478"
  cleanInputPredicate := "bandedSparseAccessPaperCleanInput"
  validSparseBranchPredicate := "bandedSparseAccessPaperValidSparseBranch"
  validCleanSourcePredicate := "bandedSparseAccessPaperValidCleanSource"
  unusedSparseBranchPredicate := "bandedSparseAccessPaperUnusedSparseBranch"
  unusedBranchImageRuleContract := fun j =>
    bandedSparseAccessUnusedBranchImageRuleContract p j
  unusedBranchExtensionContract := fun j =>

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access full clean domain extension contract flags false”; the hypotheses and conclusion in the code panel fix its exact scope. The full clean-domain wrapper is obligation-only in Phase 1.

theorem bandedSparseAccessFullCleanDomainExtensionContract_flags_false
    (p : OneTermRobinParameters) (j : Nat) :
    (bandedSparseAccessFullCleanDomainExtensionContract p).cleanDomainSplit.proved = false ∧
      (bandedSparseAccessFullCleanDomainExtensionContract p).validBranchAgreement.proved = false ∧
      (bandedSparseAccessFullCleanDomainExtensionContract p).unusedBranchImageSpecified.proved = false ∧
      (bandedSparseAccessFullCleanDomainExtensionContract p).unusedBranchImageFinite.proved = false ∧
      (bandedSparseAccessFullCleanDomainExtensionContract p).unusedBranchInjective.proved = false ∧
      (bandedSparseAccessFullCleanDomainExtensionContract p).fullCleanDomainInjective.proved = false ∧
      (bandedSparseAccessFullCleanDomainExtensionContract p).daggerCleanup.proved = false ∧
      (bandedSparseAccessFullCleanDomainExtensionContract p).unitaryExtension.proved = false ∧
      ((bandedSparseAccessFullCleanDomainExtensionContract p).unusedBranchImageRuleContract j).proposedImageIndex = none ∧

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access full clean domain extension contract of unused branch”; the hypotheses and conclusion in the code panel fix its exact scope. The full clean-domain wrapper reuses the existing per-column unused-branch classifier bridge and keeps every extension proof flag false.

theorem bandedSparseAccessFullCleanDomainExtensionContract_of_unusedBranch
    (p : OneTermRobinParameters) (j : Nat)
    (h : bandedSparseAccessPaperUnusedSparseBranch p j = true) :
    ((bandedSparseAccessFullCleanDomainExtensionContract p).unusedBranchImageRuleContract j).cleanInput = true ∧
      ((bandedSparseAccessFullCleanDomainExtensionContract p).unusedBranchImageRuleContract j).validSparseBranch = false ∧
      ((bandedSparseAccessFullCleanDomainExtensionContract p).unusedBranchImageRuleContract j).unusedSparseBranch = true ∧
      ((bandedSparseAccessFullCleanDomainExtensionContract p).unusedBranchImageRuleContract j).proposedImageIndex = none ∧
      (bandedSparseAccessFullCleanDomainExtensionContract p).unusedBranchImageSpecified.proved = false ∧
      (bandedSparseAccessFullCleanDomainExtensionContract p).fullCleanDomainInjective.proved = false ∧
      (bandedSparseAccessFullCleanDomainExtensionContract p).unitaryExtension.proved = false := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access full clean domain extension contract local clean domain split”; the hypotheses and conclusion in the code panel fix its exact scope. Wrapper-facing form of the local clean-domain split audit.

theorem bandedSparseAccessFullCleanDomainExtensionContract_localCleanDomainSplit
    (p : OneTermRobinParameters) (j : Nat) :
    (bandedSparseAccessPaperCleanInput p j = true ↔
      bandedSparseAccessPaperValidCleanSource p j = true ∨
        bandedSparseAccessPaperUnusedSparseBranch p j = true) ∧
      (bandedSparseAccessFullCleanDomainExtensionContract p).cleanDomainSplit.proved =
        false := by

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “banded sparse access unused zero branch source decision”. A proposition-valued field is a requirement until a constructor supplies it. Lean-facing source decision for unused zero-amplitude 'O_D^BS' branches.

structure BandedSparseAccessUnusedZeroBranchSourceDecision where
  sourceAnchor : String
  citedResultKey : String
  paperImageRuleSpecified : Bool
  externalExtensionTheoremAccepted : Bool
  lowerProofSearchAllowed : Bool
  dependency : ObligationRecord
deriving Repr, DecidableEq

/--
Default cycle-14 source decision for unused zero-amplitude sparse branches.

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “banded sparse access unused zero branch source decision”. Default cycle-14 source decision for unused zero-amplitude sparse branches.

def bandedSparseAccessUnusedZeroBranchSourceDecision :
    BandedSparseAccessUnusedZeroBranchSourceDecision where
  sourceAnchor := "Guseynov-Huang-Liu 2025, Lemma 1 and Fig. 1-term Robin, arXiv:2506.20478"
  citedResultKey := "QBE.ODBS.UnusedZeroBranchExtension"
  paperImageRuleSpecified := false
  externalExtensionTheoremAccepted := false
  lowerProofSearchAllowed := false
  dependency := {
    description := "unused zero-amplitude sparse branches need a paper-backed image rule or accepted reversible-extension theorem before O_D^BS injectivity, cleanup, or unitarity proof search"
    source := "research-wiki/cited-results/GHL2025.md: QBE.ODBS.UnusedZeroBranchExtension"
    proved := false

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access unused zero branch source decision flags false”; the hypotheses and conclusion in the code panel fix its exact scope. The cycle-14 source decision is a blocking obligation, not a proof ticket.

theorem bandedSparseAccessUnusedZeroBranchSourceDecision_flags_false :
    bandedSparseAccessUnusedZeroBranchSourceDecision.paperImageRuleSpecified = false ∧
      bandedSparseAccessUnusedZeroBranchSourceDecision.externalExtensionTheoremAccepted = false ∧
      bandedSparseAccessUnusedZeroBranchSourceDecision.lowerProofSearchAllowed = false ∧
      bandedSparseAccessUnusedZeroBranchSourceDecision.dependency.proved = false := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access unused zero branch source decision keeps full domain flags false”; the hypotheses and conclusion in the code panel fix its exact scope. The source decision keeps the full clean-domain wrapper in obligation mode.

theorem bandedSparseAccessUnusedZeroBranchSourceDecision_keepsFullDomainFlagsFalse
    (p : OneTermRobinParameters) :
    bandedSparseAccessUnusedZeroBranchSourceDecision.lowerProofSearchAllowed = false ∧
      (bandedSparseAccessFullCleanDomainExtensionContract p).unusedBranchImageSpecified.proved =
        false ∧
      (bandedSparseAccessFullCleanDomainExtensionContract p).fullCleanDomainInjective.proved =
        false ∧
      (bandedSparseAccessFullCleanDomainExtensionContract p).daggerCleanup.proved =
        false ∧
      (bandedSparseAccessFullCleanDomainExtensionContract p).unitaryExtension.proved =
        false := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access unused zero branch source decision keeps image rule unspecified”; the hypotheses and conclusion in the code panel fix its exact scope. The blocking source decision keeps every unused-branch image slot unspecified.

theorem bandedSparseAccessUnusedZeroBranchSourceDecision_keepsImageRuleUnspecified
    (p : OneTermRobinParameters) (j : Nat) :
    bandedSparseAccessUnusedZeroBranchSourceDecision.lowerProofSearchAllowed = false ∧
      (bandedSparseAccessUnusedBranchImageRuleContract p j).proposedImageIndex = none ∧
      (bandedSparseAccessUnusedBranchImageRuleContract p j).imageSpecified.proved = false ∧
      ((bandedSparseAccessFullCleanDomainExtensionContract p).unusedBranchImageRuleContract
        j).proposedImageIndex = none ∧
      ((bandedSparseAccessFullCleanDomainExtensionContract p).unusedBranchImageRuleContract
        j).imageSpecified.proved = false ∧
      ((bandedSparseAccessFullCleanDomainExtensionContract p).unusedBranchImageRuleContract
        j).separatesActiveCollision.proved = false := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access unused zero branch source decision keeps paper contract flags false”; the hypotheses and conclusion in the code panel fix its exact scope. The blocking source decision also keeps the paper-level O_D^BS contract obligations false.

theorem bandedSparseAccessUnusedZeroBranchSourceDecision_keepsPaperContractFlagsFalse
    (p : OneTermRobinParameters) :
    bandedSparseAccessUnusedZeroBranchSourceDecision.lowerProofSearchAllowed = false ∧
      (defaultBandedSparseAccessPaperContract p).forwardCorrect.proved = false ∧
      (defaultBandedSparseAccessPaperContract p).daggerCleanup.proved = false ∧
      (defaultBandedSparseAccessPaperContract p).unitaryExtension.proved = false := by

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “banded sparse access robin zero inclusion source contract”. A proposition-valued field is a requirement until a constructor supplies it. Source transcript for the Robin zero-inclusion sentence near Theorem 1.

structure BandedSparseAccessRobinZeroInclusionSourceContract where
  sourceAnchor : String
  zeroInclusionAnchor : String
  equationAnchor : String
  sparseIndexRange : String
  zerosIncludedInSparseEnumeration : Bool
  paperImageEquation : String
  unusedBranchImageRule : Option String
  unusedBranchImageIndex : Option Nat
  reversibleExtensionTheorem : Option String
  closesUnusedZeroBranchExtension : Bool

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “banded sparse access robin zero inclusion source contract”. Default transcript of the GHL2025 Robin zero-inclusion source text.

def bandedSparseAccessRobinZeroInclusionSourceContract :
    BandedSparseAccessRobinZeroInclusionSourceContract where
  sourceAnchor :=
    "Guseynov-Huang-Liu 2025, one-term Robin construction, arXiv:2506.20478"
  zeroInclusionAnchor :=
    "text before Theorem 1-term Robin: zeros can be included in the set of non-zero elements"
  equationAnchor :=
    "Lemma 1 and Eq. ROBIN clarified, arXiv:2506.20478"
  sparseIndexRange := "s = 0, ..., kappa - 1"
  zerosIncludedInSparseEnumeration := true
  paperImageEquation := "O_D^BS |0>^(n-l)|s>^l|i>^n = |r_si>^n|i>^n"

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access robin zero inclusion source contract blocks unused zero branch”; the hypotheses and conclusion in the code panel fix its exact scope. The Robin zero-inclusion source transcript keeps the unused-branch route blocked.

theorem bandedSparseAccessRobinZeroInclusionSourceContract_blocks_unusedZeroBranch :
    bandedSparseAccessRobinZeroInclusionSourceContract.zerosIncludedInSparseEnumeration =
        true ∧
      bandedSparseAccessRobinZeroInclusionSourceContract.unusedBranchImageRule =
        none ∧
      bandedSparseAccessRobinZeroInclusionSourceContract.unusedBranchImageIndex =
        none ∧
      bandedSparseAccessRobinZeroInclusionSourceContract.reversibleExtensionTheorem =
        none ∧
      bandedSparseAccessRobinZeroInclusionSourceContract.closesUnusedZeroBranchExtension =
        false ∧

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access robin zero inclusion source contract keeps image rule unspecified”; the hypotheses and conclusion in the code panel fix its exact scope. The zero-inclusion transcript does not fill the per-column image-rule slot.

theorem bandedSparseAccessRobinZeroInclusionSourceContract_keepsImageRuleUnspecified
    (p : OneTermRobinParameters) (j : Nat) :
    bandedSparseAccessRobinZeroInclusionSourceContract.zerosIncludedInSparseEnumeration =
        true ∧
      bandedSparseAccessRobinZeroInclusionSourceContract.unusedBranchImageIndex =
        none ∧
      bandedSparseAccessRobinZeroInclusionSourceContract.reversibleExtensionTheorem =
        none ∧
      bandedSparseAccessRobinZeroInclusionSourceContract.lowerProofSearchAllowed =
        false ∧
      (bandedSparseAccessUnusedBranchImageRuleContract p j).proposedImageIndex =

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “banded sparse access prior pde source contract”. A proposition-valued field is a requirement until a constructor supplies it. Source contract imported from the prior PDE block-encoding paper.

structure BandedSparseAccessPriorPDESourceContract where
  sourceAnchor : String
  definitionAnchor : String
  lemmaAnchor : String
  appendixAnchor : String
  oracleEquation : String
  circuitDecomposition : String
  resourceClaim : ObligationRecord
  robinUnusedBranchImageRule : Option String
  closesUnusedZeroBranchExtension : Bool
  lowerProofSearchAllowed : Bool

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “banded sparse access prior pde source contract”. Default transcript of arXiv:2405.12855v3 Definition 6, Lemma 1, and the appendix construction for 'O_A^BS'.

def bandedSparseAccessPriorPDESourceContract :
    BandedSparseAccessPriorPDESourceContract where
  sourceAnchor :=
    "Guseynov-Huang-Liu 2024, arXiv:2405.12855v3, Definition 6, Lemma 1, Appendix Banded-sparse-access"
  definitionAnchor := "Definition 6: Banded-sparse-access"
  lemmaAnchor := "Lemma 1: Banded-sparse-access resource bound"
  appendixAnchor := "Appendix: Explicit quantum circuit construction for O_A^BS"
  oracleEquation := "O_A^BS |0>^(n-l)|s>^l|i>^n = |r_si>^n|i>^n"
  circuitDecomposition := "O_A^BS = U^SUM (U_A^(l) tensor I^n)"
  resourceClaim := {
    description := "transcribe the prior-paper gate and pure-ancilla resource counts for the padded banded-sparse-access primitive"

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “robin banded sparse access citation chain”. The explicit citation chain for the displayed Robin sparse-address equation.

def robinBandedSparseAccessCitationChain : List String := [
  "Guseynov-Huang-Liu 2025, arXiv:2506.20478, Lemma 2",
  "Guseynov-Huang-Liu 2024, arXiv:2405.12855v3, Lemma 1"
]

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “robin banded sparse access citation chain eq”; the hypotheses and conclusion in the code panel fix its exact scope.

@[simp] theorem robinBandedSparseAccessCitationChain_eq :
    robinBandedSparseAccessCitationChain = [
      "Guseynov-Huang-Liu 2025, arXiv:2506.20478, Lemma 2",
      "Guseynov-Huang-Liu 2024, arXiv:2405.12855v3, Lemma 1"
    ] := rfl

/--
The prior PDE source does not unblock the QBE unused-zero-branch extension.

This is the compiled guard for the source audit: the cited theorem is recorded,
but lower proof search for Robin unused-branch injectivity, cleanup, and

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access prior pde source contract blocks unused zero branch”; the hypotheses and conclusion in the code panel fix its exact scope. The prior PDE source does not unblock the QBE unused-zero-branch extension.

theorem bandedSparseAccessPriorPDESourceContract_blocks_unusedZeroBranch :
    bandedSparseAccessPriorPDESourceContract.robinUnusedBranchImageRule = none ∧
      bandedSparseAccessPriorPDESourceContract.closesUnusedZeroBranchExtension = false ∧
      bandedSparseAccessPriorPDESourceContract.lowerProofSearchAllowed = false ∧
      bandedSparseAccessUnusedZeroBranchSourceDecision.lowerProofSearchAllowed = false := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access prior pde source contract oracle equation”; the hypotheses and conclusion in the code panel fix its exact scope. The prior PDE source contract records the exact sparse-access equation.

theorem bandedSparseAccessPriorPDESourceContract_oracleEquation :
    bandedSparseAccessPriorPDESourceContract.oracleEquation =
      "O_A^BS |0>^(n-l)|s>^l|i>^n = |r_si>^n|i>^n" := rfl

/-- The prior PDE resource claim remains an external obligation in QBE. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access prior pde source contract resource unproved”; the hypotheses and conclusion in the code panel fix its exact scope. The prior PDE resource claim remains an external obligation in QBE.

theorem bandedSparseAccessPriorPDESourceContract_resource_unproved :
    bandedSparseAccessPriorPDESourceContract.resourceClaim.proved = false := rfl

/--
Boolean form of the Lemma 1 clean-input domain.

The executable predicate is exactly the statement that the padded part of the
`O_D^BS` sparse-address register is zero.  This only classifies columns; it
does not prove the clean-input source equation or a unitary extension.
-/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper clean input iff”; the hypotheses and conclusion in the code panel fix its exact scope. Boolean form of the Lemma 1 clean-input domain.

theorem bandedSparseAccessPaperCleanInput_iff
    (p : OneTermRobinParameters) (j : Nat) :
    bandedSparseAccessPaperCleanInput p j = true ↔
      (bandedSparseAccessPaperRegisters p j).paddedZeroValue = 0 := by

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “banded sparse access paper column contract”. A proposition-valued field is a requirement until a constructor supplies it. Per-column audit record for the executable Lemma 1 paper image.

structure BandedSparseAccessPaperColumnContract where
  sourceAnchor : String
  inputRegisters : BandedSparseAccessPaperRegisters
  cleanInput : Bool
  imageIndex : Nat
  imageRegisters : BandedSparseAccessPaperRegisters
  rowPreserved : Bool
  addressWritten : Bool
  addressInRange : Bool
  imageNoSpill : Bool
  cleanInputDomain : ObligationRecord

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “banded sparse access paper column contract”. Default per-column contract for the 'O_D^BS' paper image skeleton.

def bandedSparseAccessPaperColumnContract
    (p : OneTermRobinParameters) (j : Nat) :
    BandedSparseAccessPaperColumnContract :=
  let regs := bandedSparseAccessPaperRegisters p j
  let image := bandedSparseAccessPaperImage p j
  let imageRegs := bandedSparseAccessPaperRegisters p image
  let paperContract := defaultBandedSparseAccessPaperContract p
  {
    sourceAnchor := paperContract.sourceAnchor
    inputRegisters := regs
    cleanInput := bandedSparseAccessPaperCleanInput p j

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper column contract input registers eq”; the hypotheses and conclusion in the code panel fix its exact scope. The per-column contract uses the shared Lemma 1 register extractor.

theorem bandedSparseAccessPaperColumnContract_inputRegisters_eq
    (p : OneTermRobinParameters) (j : Nat) :
    (bandedSparseAccessPaperColumnContract p j).inputRegisters =
      bandedSparseAccessPaperRegisters p j := rfl

/-- The per-column clean-domain flag is the executable padded-zero predicate. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper column contract clean input eq”; the hypotheses and conclusion in the code panel fix its exact scope. The per-column clean-domain flag is the executable padded-zero predicate.

theorem bandedSparseAccessPaperColumnContract_cleanInput_eq
    (p : OneTermRobinParameters) (j : Nat) :
    (bandedSparseAccessPaperColumnContract p j).cleanInput =
      bandedSparseAccessPaperCleanInput p j := rfl

/--
The per-column clean-domain flag is true exactly on Lemma 1 clean columns.

Columns with a nonzero padded register are still covered only by the explicit
unitary-extension obligation.
-/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper column contract clean input iff”; the hypotheses and conclusion in the code panel fix its exact scope. The per-column clean-domain flag is true exactly on Lemma 1 clean columns.

theorem bandedSparseAccessPaperColumnContract_cleanInput_iff
    (p : OneTermRobinParameters) (j : Nat) :
    (bandedSparseAccessPaperColumnContract p j).cleanInput = true ↔
      (bandedSparseAccessPaperRegisters p j).paddedZeroValue = 0 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper column contract unitary extension proved eq false”; the hypotheses and conclusion in the code panel fix its exact scope. The per-column audit keeps the full-space unitary extension as an open obligation for every column, including non-clean padded-register inputs.

theorem bandedSparseAccessPaperColumnContract_unitaryExtension_proved_eq_false
    (p : OneTermRobinParameters) (j : Nat) :
    (bandedSparseAccessPaperColumnContract p j).unitaryExtension.proved = false := rfl

/-- The per-column contract records the same image index as the paper-image skeleton. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper column contract image index eq”; the hypotheses and conclusion in the code panel fix its exact scope. The per-column contract records the same image index as the paper-image skeleton.

theorem bandedSparseAccessPaperColumnContract_imageIndex_eq
    (p : OneTermRobinParameters) (j : Nat) :
    (bandedSparseAccessPaperColumnContract p j).imageIndex =
      bandedSparseAccessPaperImage p j := rfl

/-- The per-column contract records the executable n-bit address range check. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper column contract address in range eq”; the hypotheses and conclusion in the code panel fix its exact scope. The per-column contract records the executable n-bit address range check.

theorem bandedSparseAccessPaperColumnContract_addressInRange_eq
    (p : OneTermRobinParameters) (j : Nat) :
    (bandedSparseAccessPaperColumnContract p j).addressInRange =
      bandedSparseAccessPaperAddressInRange p j := rfl

/-- The per-column contract records the executable high-bit no-spill check. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper column contract image no spill eq”; the hypotheses and conclusion in the code panel fix its exact scope. The per-column contract records the executable high-bit no-spill check.

theorem bandedSparseAccessPaperColumnContract_imageNoSpill_eq
    (p : OneTermRobinParameters) (j : Nat) :
    (bandedSparseAccessPaperColumnContract p j).imageNoSpill =
      bandedSparseAccessPaperImageNoSpill p j := rfl

/--
The per-column audit records that the paper image preserves the row register.

This is an executable register-safety fact for the Phase 1 skeleton; it does
not promote the paper-level `forwardCorrect` obligation.
-/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper column contract row preserved eq true”; the hypotheses and conclusion in the code panel fix its exact scope. The per-column audit records that the paper image preserves the row register.

theorem bandedSparseAccessPaperColumnContract_rowPreserved_eq_true
    (p : OneTermRobinParameters) (j : Nat) :
    (bandedSparseAccessPaperColumnContract p j).rowPreserved = true := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper column contract address written eq true of address lt”; the hypotheses and conclusion in the code panel fix its exact scope. The per-column audit records that the paper image writes the O_D register to the computed address whenever that address is an n-bit value.

theorem bandedSparseAccessPaperColumnContract_addressWritten_eq_true_of_address_lt
    (p : OneTermRobinParameters) (j : Nat)
    (haddr : bandedSparseAccessPaperAddress p j < (1 <<< p.n)) :
    (bandedSparseAccessPaperColumnContract p j).addressWritten = true := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper column contract address in range eq true of address lt”; the hypotheses and conclusion in the code panel fix its exact scope. The per-column address-range audit Boolean follows from the address bound.

theorem bandedSparseAccessPaperColumnContract_addressInRange_eq_true_of_address_lt
    (p : OneTermRobinParameters) (j : Nat)
    (haddr : bandedSparseAccessPaperAddress p j < (1 <<< p.n)) :
    (bandedSparseAccessPaperColumnContract p j).addressInRange = true := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper column contract image no spill eq true of address lt”; the hypotheses and conclusion in the code panel fix its exact scope. The per-column no-spill audit Boolean follows from the address bound.

theorem bandedSparseAccessPaperColumnContract_imageNoSpill_eq_true_of_address_lt
    (p : OneTermRobinParameters) (j : Nat)
    (haddr : bandedSparseAccessPaperAddress p j < (1 <<< p.n)) :
    (bandedSparseAccessPaperColumnContract p j).imageNoSpill = true := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper column contract register safety of address lt”; the hypotheses and conclusion in the code panel fix its exact scope. Reusable per-column register-safety package for the active Lemma 1 image skeleton.

theorem bandedSparseAccessPaperColumnContract_registerSafety_of_address_lt
    (p : OneTermRobinParameters) (j : Nat)
    (haddr : bandedSparseAccessPaperAddress p j < (1 <<< p.n)) :
    (bandedSparseAccessPaperColumnContract p j).rowPreserved = true ∧
      (bandedSparseAccessPaperColumnContract p j).addressWritten = true ∧
      (bandedSparseAccessPaperColumnContract p j).addressInRange = true ∧
      (bandedSparseAccessPaperColumnContract p j).imageNoSpill = true := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “banded sparse access paper matrix”. Matrix entries for the faithful Lemma 1 'O_D^BS' paper-image skeleton.

def bandedSparseAccessPaperMatrix (p : OneTermRobinParameters) :
    Matrix (qubitDim (oneTermRobinTotalQubits p)) (qubitDim (oneTermRobinTotalQubits p)) Coeff :=
  fun i j =>
    if i.val = bandedSparseAccessPaperImage p j.val then Coeff.rat 1 else Coeff.rat 0

/-- The paper-image matrix entry is governed by `bandedSparseAccessPaperImage`. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper matrix eq image”; the hypotheses and conclusion in the code panel fix its exact scope. The paper-image matrix entry is governed by 'bandedSparseAccessPaperImage'.

theorem bandedSparseAccessPaperMatrix_eq_image (p : OneTermRobinParameters)
    (i j : Fin (qubitDim (oneTermRobinTotalQubits p))) :
    bandedSparseAccessPaperMatrix p i j =
      if i.val = bandedSparseAccessPaperImage p j.val then Coeff.rat 1 else Coeff.rat 0 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper matrix image fin eq one”; the hypotheses and conclusion in the code panel fix its exact scope. Forward paper-image matrix entry at the finite image column.

theorem bandedSparseAccessPaperMatrix_imageFin_eq_one
    (p : OneTermRobinParameters)
    (j : Fin (qubitDim (oneTermRobinTotalQubits p)))
    (haddr : bandedSparseAccessPaperAddress p j.val < (1 <<< p.n)) :
    bandedSparseAccessPaperMatrix p (bandedSparseAccessPaperImageFin p j haddr) j =
      Coeff.rat 1 := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “banded sparse access paper dagger matrix”. Transpose-style matrix for the faithful Lemma 1 'O_D^BS' paper-image skeleton.

def bandedSparseAccessPaperDaggerMatrix (p : OneTermRobinParameters) :
    Matrix (qubitDim (oneTermRobinTotalQubits p)) (qubitDim (oneTermRobinTotalQubits p)) Coeff :=
  fun i j =>
    if j.val = bandedSparseAccessPaperImage p i.val then Coeff.rat 1 else Coeff.rat 0

/-- The paper-image dagger matrix is the transpose-style matrix for the image skeleton. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper dagger matrix eq image”; the hypotheses and conclusion in the code panel fix its exact scope. The paper-image dagger matrix is the transpose-style matrix for the image skeleton.

theorem bandedSparseAccessPaperDaggerMatrix_eq_image (p : OneTermRobinParameters)
    (i j : Fin (qubitDim (oneTermRobinTotalQubits p))) :
    bandedSparseAccessPaperDaggerMatrix p i j =
      if j.val = bandedSparseAccessPaperImage p i.val then Coeff.rat 1 else Coeff.rat 0 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper dagger matrix image fin eq one”; the hypotheses and conclusion in the code panel fix its exact scope. Transpose-style paper-image matrix entry paired with the finite forward image.

theorem bandedSparseAccessPaperDaggerMatrix_imageFin_eq_one
    (p : OneTermRobinParameters)
    (j : Fin (qubitDim (oneTermRobinTotalQubits p)))
    (haddr : bandedSparseAccessPaperAddress p j.val < (1 <<< p.n)) :
    bandedSparseAccessPaperDaggerMatrix p j (bandedSparseAccessPaperImageFin p j haddr) =
      Coeff.rat 1 := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “robin sparse amplitude value”. Sparse amplitude value: the s-th nonzero stencil coefficient of row i in the Robin derivative matrix, returned as a Coeff value.

def robinSparseAmplitudeValue (n s i : Nat) : Coeff :=
  let N := gridSize n
  let K1 := 2
  let K2 := N - 3
  if K1 ≤ i ∧ i ≤ K2 then
    match s with
    | 0 => Coeff.rat ((-1 : Rat) / 12)
    | 1 => Coeff.rat ((4 : Rat) / 3)
    | 2 => Coeff.rat ((-5 : Rat) / 2)
    | 3 => Coeff.rat ((4 : Rat) / 3)
    | 4 => Coeff.rat ((-1 : Rat) / 12)

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “robin global sparse amplitude value”. Global sparse-slot coefficient source for the one-term Robin table.

def robinGlobalSparseAmplitudeValue (n s i : Nat) : Coeff :=
  let N := gridSize n
  let K1 := 2
  let K2 := N - 3
  if K1 ≤ i ∧ i ≤ K2 then
    match s with
    | 0 => Coeff.rat ((-1 : Rat) / 12)
    | 1 => Coeff.rat ((4 : Rat) / 3)
    | 2 => Coeff.rat ((-5 : Rat) / 2)
    | 3 => Coeff.rat ((4 : Rat) / 3)
    | 4 => Coeff.rat ((-1 : Rat) / 12)

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “robin global sparse amplitude value boundary slot 2 row 0 n 3”; the hypotheses and conclusion in the code panel fix its exact scope. Focused boundary regression: global slot '2' is the row-'0' diagonal.

theorem robinGlobalSparseAmplitudeValue_boundarySlot2_row0_n3 :
    robinGlobalSparseAmplitudeValue 3 2 0 =
      Coeff.add (Coeff.rat ((-5 : Rat) / 2))
        (Coeff.mul (Coeff.rat ((7 : Rat) / 3)) (Coeff.symbol "A1*dx")) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “robin global sparse amplitude value boundary slot 2 differs row local n 3”; the hypotheses and conclusion in the code panel fix its exact scope. The focused global slot is not the old row-local sparse entry.

theorem robinGlobalSparseAmplitudeValue_boundarySlot2_differs_rowLocal_n3 :
    robinGlobalSparseAmplitudeValue 3 2 0 ≠
      robinSparseAmplitudeValue 3 2 0 := by

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “derivative normalizer nd contract”. A proposition-valued field is a requirement until a constructor supplies it. Shared Phase-1 contract for every paper route that uses the normalized derivative coefficient 'D_j^(s) / N_D'.

structure DerivativeNormalizerNDContract where
  sourceAnchor : String
  rowValue : Nat
  sparseIndexValue : Nat
  coefficient : Coeff
  normalizerND : Coeff
  normalizedCoefficient : Coeff
  normalizedCoefficientFormula : String
  nonzeroNormalizer : ObligationRecord
  divisionSemantics : ObligationRecord
  coefficientBound : ObligationRecord

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “derivative normalizer nd contract”. Default shared 'N_D' normalizer contract for one Robin coefficient.

def derivativeNormalizerNDContract
    (p : OneTermRobinParameters) (row sparse : Nat) :
    DerivativeNormalizerNDContract where
  sourceAnchor := "Guseynov-Huang-Liu 2025, Lemma 3, Eq. (20), Fig. 1-term Robin, and boundary Ry equations, arXiv:2506.20478"
  rowValue := row
  sparseIndexValue := sparse
  coefficient := robinGlobalSparseAmplitudeValue p.n sparse row
  normalizerND := Coeff.symbol "N_D"
  normalizedCoefficient :=
    Coeff.mul (robinGlobalSparseAmplitudeValue p.n sparse row) (Coeff.symbol "N_D_inv")
  normalizedCoefficientFormula := "D_j^(s) / N_D"

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “derivative normalizer nd contract coefficient”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem derivativeNormalizerNDContract_coefficient
    (p : OneTermRobinParameters) (row sparse : Nat) :
    (derivativeNormalizerNDContract p row sparse).coefficient =
      robinGlobalSparseAmplitudeValue p.n sparse row := rfl

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “derivative normalizer nd contract normalizer nd”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem derivativeNormalizerNDContract_normalizerND
    (p : OneTermRobinParameters) (row sparse : Nat) :
    (derivativeNormalizerNDContract p row sparse).normalizerND =
      Coeff.symbol "N_D" := rfl

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “derivative normalizer nd contract normalized coefficient”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem derivativeNormalizerNDContract_normalizedCoefficient
    (p : OneTermRobinParameters) (row sparse : Nat) :
    (derivativeNormalizerNDContract p row sparse).normalizedCoefficient =
      Coeff.mul (robinGlobalSparseAmplitudeValue p.n sparse row) (Coeff.symbol "N_D_inv") := rfl

/--
Phase-1 source/bound view for the shared `N_D` normalizer contract.

This does not prove the analytic inequality.  It only packages the exact
coefficient source and the paper normalizer symbol used by the future bound
obligation, so `O_DT^S` and `Ry_boundary` can point to the same fixed

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “derivative normalizer nd source bound”. A proposition-valued field is a requirement until a constructor supplies it. Phase-1 source/bound view for the shared 'N_D' normalizer contract.

structure DerivativeNormalizerNDSourceBound where
  sourceAnchor : String
  rowValue : Nat
  sparseIndexValue : Nat
  sourceCoefficient : Coeff
  normalizerND : Coeff
  boundFormula : String
  coefficientBound : ObligationRecord
deriving Repr, DecidableEq

/--

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “derivative normalizer nd source bound”. Default source/bound interface for the paper statement '|D_j^(s)| <= N_D'.

def derivativeNormalizerNDSourceBound
    (p : OneTermRobinParameters) (row sparse : Nat) :
    DerivativeNormalizerNDSourceBound :=
  let nd := derivativeNormalizerNDContract p row sparse
  {
    sourceAnchor := nd.sourceAnchor
    rowValue := nd.rowValue
    sparseIndexValue := nd.sparseIndexValue
    sourceCoefficient := nd.coefficient
    normalizerND := nd.normalizerND
    boundFormula := "|D_j^(s)| <= N_D"

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “derivative normalizer nd source bound source coefficient”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem derivativeNormalizerNDSourceBound_sourceCoefficient
    (p : OneTermRobinParameters) (row sparse : Nat) :
    (derivativeNormalizerNDSourceBound p row sparse).sourceCoefficient =
      robinGlobalSparseAmplitudeValue p.n sparse row := rfl

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “derivative normalizer nd source bound normalizer nd”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem derivativeNormalizerNDSourceBound_normalizerND
    (p : OneTermRobinParameters) (row sparse : Nat) :
    (derivativeNormalizerNDSourceBound p row sparse).normalizerND =
      Coeff.symbol "N_D" := rfl

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “derivative normalizer nd source bound bound formula”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem derivativeNormalizerNDSourceBound_boundFormula
    (p : OneTermRobinParameters) (row sparse : Nat) :
    (derivativeNormalizerNDSourceBound p row sparse).boundFormula =
      "|D_j^(s)| <= N_D" := rfl

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “derivative normalizer nd source bound coefficient bound”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem derivativeNormalizerNDSourceBound_coefficientBound
    (p : OneTermRobinParameters) (row sparse : Nat) :
    (derivativeNormalizerNDSourceBound p row sparse).coefficientBound =
      (derivativeNormalizerNDContract p row sparse).coefficientBound := rfl

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “derivative normalizer nd source bound coefficient bound false”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem derivativeNormalizerNDSourceBound_coefficientBound_false
    (p : OneTermRobinParameters) (row sparse : Nat) :
    (derivativeNormalizerNDSourceBound p row sparse).coefficientBound.proved =
      false := rfl

/--
Honest U_indic matrix: controlled-X on the indicator qubit, conditioned on
the system register being in the bulk window [K1, K2].
For each basis state |j⟩:
  - Extract systemVal = bits [1, 1+n) of j
  - If K1 ≤ systemVal ≤ K2 (bulk row): flip indicator bit

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “indicator oracle matrix”. Honest U_indic matrix: controlled-X on the indicator qubit, conditioned on the system register being in the bulk window [K1, K2].

def indicatorOracleMatrix (p : OneTermRobinParameters) :
    Matrix (qubitDim (oneTermRobinTotalQubits p)) (qubitDim (oneTermRobinTotalQubits p)) Coeff :=
  fun i j =>
    let n := p.n
    let indPos := robinIndicatorBitPosition p
    let systemVal := (j.val >>> 1) &&& ((1 <<< n) - 1)
    let K1 := 2
    let K2 := gridSize n - 3
    let isBulk := if K1 ≤ systemVal ∧ systemVal ≤ K2 then (1 : Nat) else 0
    let expectedImage := j.val ^^^ (isBulk <<< indPos)
    if i.val = expectedImage then Coeff.rat 1 else Coeff.rat 0

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gate u indic”. Gate matrix for U_indic using the honest permutation matrix.

def oneTermRobinGate_U_indic (p : OneTermRobinParameters) : GateMatrix Coeff (oneTermRobinTotalQubits p) where
  gate := Gate.oracleCall "U_indic"
  matrix := indicatorOracleMatrix p
  unitary := {
    description := "U_indic(K1,K2) permutation matrix: unitarity proved via indicatorOracleMatrix_is_permutation"
    source := "main.tex:1088-1099"
    proved := true
  }

/--
Theorem-facing Hermitian-conjugate slot for `U_indic`.

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gate u indic dagger”. Theorem-facing Hermitian-conjugate slot for 'U_indic'.

def oneTermRobinGate_U_indic_dagger (p : OneTermRobinParameters) :
    GateMatrix Coeff (oneTermRobinTotalQubits p) where
  gate := Gate.oracleCall "U_indic^dagger"
  matrix := indicatorOracleMatrix p
  unitary := {
    description := "U_indic^dagger uses the same self-inverse indicator permutation matrix as U_indic"
    source := "GHL2025 Fig. 1-term Robin transcript slot; self-inverse bridge from indicatorOracleImage_self_inverse"
    proved := true
  }

/--

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “one term robin gate u indic dagger matrix eq”; the hypotheses and conclusion in the code panel fix its exact scope. The theorem-facing 'U_indic^dagger' slot has the same matrix as 'U_indic'.

theorem oneTermRobinGate_U_indic_dagger_matrix_eq
    (p : OneTermRobinParameters) :
    (oneTermRobinGate_U_indic_dagger p).matrix =
      (oneTermRobinGate_U_indic p).matrix := rfl

/--
Honest O_DT^S diagonal matrix: encodes the sparse amplitude data on the diagonal
for bulk rows (indicator=1) and acts as identity for boundary rows (indicator=0).

For each compound basis state |j⟩:
  - If indicator bit = 0 (boundary row): diagonal entry = Coeff.rat 1 (identity)

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “sparse amplitude oracle dt matrix”. Honest O_DT^S diagonal matrix: encodes the sparse amplitude data on the diagonal for bulk rows (indicator=1) and acts as identity for boundary rows (indicator=0).

def sparseAmplitudeOracleDTMatrix (p : OneTermRobinParameters) :
    Matrix (qubitDim (oneTermRobinTotalQubits p)) (qubitDim (oneTermRobinTotalQubits p)) Coeff :=
  fun i j =>
    if i.val ≠ j.val then Coeff.rat 0
    else
      let n := p.n
      let indPos := robinIndicatorBitPosition p
      let indBit := (j.val >>> indPos) &&& 1
      if indBit = 0 then
        Coeff.rat 1
      else

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “sparse amplitude oracle dt paper registers”. A proposition-valued field is a requirement until a constructor supplies it. Register values used by the faithful Lemma 3 'O_DT^S' contract.

structure SparseAmplitudeOracleDTPaperRegisters where
  ancillaBit : Nat
  indicatorBit : Nat
  rowValue : Nat
  sparseIndexValue : Nat
  nonAncillaValue : Nat
deriving Repr, DecidableEq

/--
Extract the Lemma 3 sparse-amplitude oracle registers from a compound basis
index.  This is a source-contract skeleton for the paper's controlled rotation

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “sparse amplitude oracle dt paper registers”. Extract the Lemma 3 sparse-amplitude oracle registers from a compound basis index.

def sparseAmplitudeOracleDTPaperRegisters (p : OneTermRobinParameters) (j : Nat) :
    SparseAmplitudeOracleDTPaperRegisters :=
  let n := p.n
  let indPos := robinIndicatorBitPosition p
  let κbits := clog2 p.kappa
  let odPure := n - κbits
  let sysMask := (1 <<< n) - 1
  let sparseStart := 1 + n + odPure
  let sparseMask := (1 <<< κbits) - 1
  {
    ancillaBit := j &&& 1

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “sparse amplitude oracle dt cos half”. Symbolic cosine half-angle entry for the Lemma 3 O_DT^S rotation.

def sparseAmplitudeOracleDTCosHalf (row sparse : Nat) : Coeff :=
  Coeff.symbol s!"odts_cos_half_{row}_{sparse}"

/-- Symbolic sine half-angle entry for the Lemma 3 O_DT^S rotation. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “sparse amplitude oracle dt sin half”. Symbolic sine half-angle entry for the Lemma 3 O_DT^S rotation.

def sparseAmplitudeOracleDTSinHalf (row sparse : Nat) : Coeff :=
  Coeff.symbol s!"odts_sin_half_{row}_{sparse}"

/--
Explicit unresolved source obligation for the symbolic entries in the Lemma 3
`O_DT^S` rotation skeleton.

Equation (20) of Guseynov-Huang-Liu 2025 maps `|0>|s>` to an amplitude whose
`|0>` component is `D^(s) / N_D` and whose complementary component is the
square-root normalizer term.  The Lean symbols
`sparseAmplitudeOracleDTCosHalf row sparse` and

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “sparse amplitude oracle dt coefficient normalizer obligation”. Explicit unresolved source obligation for the symbolic entries in the Lemma 3 'O_DT^S' rotation skeleton.

def sparseAmplitudeOracleDTCoefficientNormalizerObligation : ObligationRecord := {
  description := "O_DT^S symbolic rotation entries match Eq. (20): D^(s)/N_D amplitude and complementary normalizer term"
  source := "Guseynov-Huang-Liu 2025, Lemma 3, Eq. (20), arXiv:2506.20478"
  proved := false
}

/--
Typed Eq. (20) coefficient-normalizer contract for one `O_DT^S` rotation block.

This binds the symbolic rotation entries to the concrete Robin sparse
coefficient data and the paper's `N_D` normalizer without proving the analytic

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “sparse amplitude oracle dt coefficient normalizer contract”. A proposition-valued field is a requirement until a constructor supplies it. Typed Eq.

structure SparseAmplitudeOracleDTCoefficientNormalizerContract where
  sourceAnchor : String
  rowValue : Nat
  sparseIndexValue : Nat
  coefficient : Coeff
  normalizerND : Coeff
  ketZeroEntry : Coeff
  ketOneEntry : Coeff
  ketZeroFormula : String
  ketOneFormula : String
  coefficientRelation : ObligationRecord

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “sparse amplitude oracle dt coefficient normalizer contract”. Default Eq.

def sparseAmplitudeOracleDTCoefficientNormalizerContract
    (p : OneTermRobinParameters) (row sparse : Nat) :
    SparseAmplitudeOracleDTCoefficientNormalizerContract where
  sourceAnchor := "Guseynov-Huang-Liu 2025, Lemma 3, Eq. (20), arXiv:2506.20478"
  rowValue := row
  sparseIndexValue := sparse
  coefficient := robinGlobalSparseAmplitudeValue p.n sparse row
  normalizerND := Coeff.symbol "N_D"
  ketZeroEntry := sparseAmplitudeOracleDTCosHalf row sparse
  ketOneEntry := sparseAmplitudeOracleDTSinHalf row sparse
  ketZeroFormula := "D_j^(s) / N_D"

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “sparse amplitude oracle dt normalized coefficient”. Symbolic stand-in for the Lemma 3 normalized coefficient 'D_j^(s) / N_D'.

def sparseAmplitudeOracleDTNormalizedCoefficient
    (p : OneTermRobinParameters) (row sparse : Nat) : Coeff :=
  Coeff.mul (robinGlobalSparseAmplitudeValue p.n sparse row) (Coeff.symbol "N_D_inv")

/--
Refined proof route for the `odts_coeff_normalizer` block.

This record separates the typed Eq. (20) data from the analytic obligations:
division by `N_D`, the paper's normalizer bound, the absolute-square term, the
complementary square root, and the two-by-two unitarity identity.  All proof
obligations stay false in Phase 1.

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “sparse amplitude oracle dt coefficient normalizer proof route”. A proposition-valued field is a requirement until a constructor supplies it. Refined proof route for the 'odts_coeff_normalizer' block.

structure SparseAmplitudeOracleDTCoefficientNormalizerProofRoute where
  sourceAnchor : String
  rowValue : Nat
  sparseIndexValue : Nat
  coefficient : Coeff
  normalizerND : Coeff
  normalizedCoefficient : Coeff
  normalizedCoefficientFormula : String
  ketZeroEntry : Coeff
  ketOneEntry : Coeff
  ketZeroFormula : String

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “sparse amplitude oracle dt coefficient normalizer proof route”. Default refined proof route for one 'O_DT^S' Eq.

def sparseAmplitudeOracleDTCoefficientNormalizerProofRoute
    (p : OneTermRobinParameters) (row sparse : Nat) :
    SparseAmplitudeOracleDTCoefficientNormalizerProofRoute :=
  let c := sparseAmplitudeOracleDTCoefficientNormalizerContract p row sparse
  let nd := derivativeNormalizerNDContract p row sparse
  {
    sourceAnchor := c.sourceAnchor
    rowValue := c.rowValue
    sparseIndexValue := c.sparseIndexValue
    coefficient := c.coefficient
    normalizerND := nd.normalizerND

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “sparse amplitude oracle dt coefficient normalizer proof route coefficient”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem sparseAmplitudeOracleDTCoefficientNormalizerProofRoute_coefficient
    (p : OneTermRobinParameters) (row sparse : Nat) :
    (sparseAmplitudeOracleDTCoefficientNormalizerProofRoute p row sparse).coefficient =
      (sparseAmplitudeOracleDTCoefficientNormalizerContract p row sparse).coefficient := rfl

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “sparse amplitude oracle dt coefficient normalizer proof route normalizer nd”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem sparseAmplitudeOracleDTCoefficientNormalizerProofRoute_normalizerND
    (p : OneTermRobinParameters) (row sparse : Nat) :
    (sparseAmplitudeOracleDTCoefficientNormalizerProofRoute p row sparse).normalizerND =
      (sparseAmplitudeOracleDTCoefficientNormalizerContract p row sparse).normalizerND := rfl

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “sparse amplitude oracle dt coefficient normalizer proof route normalized coefficient”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem sparseAmplitudeOracleDTCoefficientNormalizerProofRoute_normalizedCoefficient
    (p : OneTermRobinParameters) (row sparse : Nat) :
    (sparseAmplitudeOracleDTCoefficientNormalizerProofRoute p row sparse).normalizedCoefficient =
      sparseAmplitudeOracleDTNormalizedCoefficient p row sparse := rfl

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “sparse amplitude oracle dt coefficient normalizer proof route shared nd”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem sparseAmplitudeOracleDTCoefficientNormalizerProofRoute_sharedND
    (p : OneTermRobinParameters) (row sparse : Nat) :
    (sparseAmplitudeOracleDTCoefficientNormalizerProofRoute p row sparse).normalizerBound =
      (derivativeNormalizerNDContract p row sparse).coefficientBound ∧
    (sparseAmplitudeOracleDTCoefficientNormalizerProofRoute p row sparse).coefficientDivision =
      (derivativeNormalizerNDContract p row sparse).divisionSemantics ∧
    (sparseAmplitudeOracleDTCoefficientNormalizerProofRoute p row sparse).absSquareSemantics =
      (derivativeNormalizerNDContract p row sparse).absSquareSemantics ∧
    (sparseAmplitudeOracleDTCoefficientNormalizerProofRoute p row sparse).sqrtComplementSemantics =
      (derivativeNormalizerNDContract p row sparse).sqrtComplementSemantics := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “sparse amplitude oracle dt coefficient normalizer proof route source bound”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem sparseAmplitudeOracleDTCoefficientNormalizerProofRoute_sourceBound
    (p : OneTermRobinParameters) (row sparse : Nat) :
    (sparseAmplitudeOracleDTCoefficientNormalizerProofRoute p row sparse).coefficient =
      (derivativeNormalizerNDSourceBound p row sparse).sourceCoefficient ∧
    (sparseAmplitudeOracleDTCoefficientNormalizerProofRoute p row sparse).normalizerND =
      (derivativeNormalizerNDSourceBound p row sparse).normalizerND ∧
    (sparseAmplitudeOracleDTCoefficientNormalizerProofRoute p row sparse).normalizerBound =
      (derivativeNormalizerNDSourceBound p row sparse).coefficientBound := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “sparse amplitude oracle dt coefficient normalizer proof route ket zero entry”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem sparseAmplitudeOracleDTCoefficientNormalizerProofRoute_ketZeroEntry
    (p : OneTermRobinParameters) (row sparse : Nat) :
    (sparseAmplitudeOracleDTCoefficientNormalizerProofRoute p row sparse).ketZeroEntry =
      (sparseAmplitudeOracleDTCoefficientNormalizerContract p row sparse).ketZeroEntry := rfl

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “sparse amplitude oracle dt coefficient normalizer proof route ket one entry”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem sparseAmplitudeOracleDTCoefficientNormalizerProofRoute_ketOneEntry
    (p : OneTermRobinParameters) (row sparse : Nat) :
    (sparseAmplitudeOracleDTCoefficientNormalizerProofRoute p row sparse).ketOneEntry =
      (sparseAmplitudeOracleDTCoefficientNormalizerContract p row sparse).ketOneEntry := rfl

/--
Faithful Lemma 3 controlled-rotation skeleton for `O_DT^S`.

For columns whose indicator bit is 0, the matrix acts as identity.  For columns
whose indicator bit is 1, it preserves every non-ancilla bit and applies a
symbolic two-by-two rotation on ancilla bit 0.  The symbols are indexed by the

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “sparse amplitude oracle dt rotation matrix”. Faithful Lemma 3 controlled-rotation skeleton for 'O_DT^S'.

def sparseAmplitudeOracleDTRotationMatrix (p : OneTermRobinParameters) :
    Matrix (qubitDim (oneTermRobinTotalQubits p)) (qubitDim (oneTermRobinTotalQubits p)) Coeff :=
  fun i j =>
    let regs := sparseAmplitudeOracleDTPaperRegisters p j.val
    if regs.indicatorBit = 0 then
      if i.val = j.val then Coeff.rat 1 else Coeff.rat 0
    else if i.val >>> 1 ≠ regs.nonAncillaValue then
      Coeff.rat 0
    else
      let cosHalf := sparseAmplitudeOracleDTCosHalf regs.rowValue regs.sparseIndexValue
      let sinHalf := sparseAmplitudeOracleDTSinHalf regs.rowValue regs.sparseIndexValue

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gate o dt s”. Gate matrix for O_DT^S using the faithful controlled-rotation skeleton.

def oneTermRobinGate_O_DT_S (p : OneTermRobinParameters) : GateMatrix Coeff (oneTermRobinTotalQubits p) where
  gate := Gate.oracleCall "O_DT^S"
  matrix := sparseAmplitudeOracleDTRotationMatrix p
  unitary := {
    description := "O_DT^S controlled-rotation skeleton on ancilla bit: unitarity and normalizer bound not yet proved"
    source := "Guseynov-Huang-Liu 2025, Lemma 3, arXiv:2506.20478"
    proved := false
  }

/--
Register values used by the faithful `Ry_boundary` source contract.

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “boundary rotation paper registers”. A proposition-valued field is a requirement until a constructor supplies it. Register values used by the faithful 'Ry_boundary' source contract.

structure BoundaryRotationPaperRegisters where
  ancillaBit : Nat
  indicatorBit : Nat
  rowValue : Nat
  sparseIndexValue : Nat
  nonAncillaValue : Nat
deriving Repr, DecidableEq

/--
Extract the `Ry_boundary` register fields from a compound basis index.
This is a source-contract skeleton; it does not prove the angle identities or

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “boundary rotation paper registers”. Extract the 'Ry_boundary' register fields from a compound basis index.

def boundaryRotationPaperRegisters (p : OneTermRobinParameters) (j : Nat) :
    BoundaryRotationPaperRegisters :=
  let n := p.n
  let indPos := robinIndicatorBitPosition p
  let κbits := clog2 p.kappa
  let odPure := n - κbits
  let sysMask := (1 <<< n) - 1
  let sparseStart := 1 + n + odPure
  let sparseMask := (1 <<< κbits) - 1
  {
    ancillaBit := j &&& 1

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “boundary rotation cos half”. Symbolic cosine half-angle entry for the 'Ry_boundary' rotation.

def boundaryRotationCosHalf (row sparse : Nat) : Coeff :=
  Coeff.symbol s!"boundary_cos_half_{row}_{sparse}"

/-- Symbolic sine half-angle entry for the `Ry_boundary` rotation. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “boundary rotation sin half”. Symbolic sine half-angle entry for the 'Ry_boundary' rotation.

def boundaryRotationSinHalf (row sparse : Nat) : Coeff :=
  Coeff.symbol s!"boundary_sin_half_{row}_{sparse}"

/--
Explicit unresolved source obligation for the `Ry_boundary` angle/normalizer
relation.

The paper uses angles `theta_j^s = arccos(D_j^(s) / N_D)` for boundary rows.
The Lean symbols `boundaryRotationCosHalf row sparse` and
`boundaryRotationSinHalf row sparse` are placeholders until the half-angle
identities and the two-by-two unitarity relation are formalized.

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “boundary rotation angle normalizer obligation”. Explicit unresolved source obligation for the 'Ry_boundary' angle/normalizer relation.

def boundaryRotationAngleNormalizerObligation : ObligationRecord := {
  description := "Ry_boundary symbolic entries match theta_j^s = arccos(D_j^(s) / N_D) and the half-angle formulas"
  source := "Guseynov-Huang-Liu 2025, Fig. 1-term Robin and Eq. angles for Ry, arXiv:2506.20478"
  proved := false
}

/--
Typed angle/normalizer contract for one `Ry_boundary` rotation block.

This binds the symbolic half-angle entries used by `boundaryRotationMatrix` to
the Robin sparse coefficient source and the paper normalizer `N_D`.  It records

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “boundary rotation angle normalizer contract”. A proposition-valued field is a requirement until a constructor supplies it. Typed angle/normalizer contract for one 'Ry_boundary' rotation block.

structure BoundaryRotationAngleNormalizerContract where
  sourceAnchor : String
  rowValue : Nat
  sparseIndexValue : Nat
  coefficient : Coeff
  normalizerND : Coeff
  thetaFormula : String
  cosHalfEntry : Coeff
  sinHalfEntry : Coeff
  cosHalfFormula : String
  sinHalfFormula : String

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “boundary rotation angle normalizer contract”. Default 'Ry_boundary' angle/normalizer contract for one Robin row and global sparse slot.

def boundaryRotationAngleNormalizerContract
    (p : OneTermRobinParameters) (row sparse : Nat) :
    BoundaryRotationAngleNormalizerContract where
  sourceAnchor := "Guseynov-Huang-Liu 2025, Fig. 1-term Robin and Eq. angles for Ry, arXiv:2506.20478"
  rowValue := row
  sparseIndexValue := sparse
  coefficient := robinGlobalSparseAmplitudeValue p.n sparse row
  normalizerND := Coeff.symbol "N_D"
  thetaFormula := "theta_j^s = arccos(D_j^(s) / N_D)"
  cosHalfEntry := boundaryRotationCosHalf row sparse
  sinHalfEntry := boundaryRotationSinHalf row sparse

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “boundary rotation angle normalizer contract coefficient”; the hypotheses and conclusion in the code panel fix its exact scope. The coefficient source of the 'Ry_boundary' angle contract is definitionally the Robin global sparse-slot amplitude data layer.

theorem boundaryRotationAngleNormalizerContract_coefficient
    (p : OneTermRobinParameters) (row sparse : Nat) :
    (boundaryRotationAngleNormalizerContract p row sparse).coefficient =
      robinGlobalSparseAmplitudeValue p.n sparse row := rfl

/--
Symbolic stand-in for the paper argument `D_j^(s) / N_D`.

The factor `Coeff.symbol "N_D_inv"` is not a proof that `N_D` is invertible.
It only records the intended normalized coefficient while the required division
semantics and nonzero normalizer condition remain explicit obligations.

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “boundary rotation normalized coefficient”. Symbolic stand-in for the paper argument 'D_j^(s) / N_D'.

def boundaryRotationNormalizedCoefficient
    (p : OneTermRobinParameters) (row sparse : Nat) : Coeff :=
  Coeff.mul (robinGlobalSparseAmplitudeValue p.n sparse row) (Coeff.symbol "N_D_inv")

/--
Refined proof route for the `ryb_angle_normalizer` block.

This record separates the typed data already present in
`BoundaryRotationAngleNormalizerContract` from the missing analytic semantics:
division by `N_D`, real arccos, square roots, the paper's normalizer bound, and
the resulting two-by-two unitarity identity.  All proof obligations stay false

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “boundary rotation angle normalizer proof route”. A proposition-valued field is a requirement until a constructor supplies it. Refined proof route for the 'ryb_angle_normalizer' block.

structure BoundaryRotationAngleNormalizerProofRoute where
  sourceAnchor : String
  rowValue : Nat
  sparseIndexValue : Nat
  coefficient : Coeff
  normalizerND : Coeff
  arccosArgument : Coeff
  arccosArgumentFormula : String
  thetaFormula : String
  cosHalfEntry : Coeff
  sinHalfEntry : Coeff

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “boundary rotation angle normalizer proof route”. Default refined proof route for one 'Ry_boundary' angle-normalizer block.

def boundaryRotationAngleNormalizerProofRoute
    (p : OneTermRobinParameters) (row sparse : Nat) :
    BoundaryRotationAngleNormalizerProofRoute :=
  let c := boundaryRotationAngleNormalizerContract p row sparse
  let nd := derivativeNormalizerNDContract p row sparse
  {
    sourceAnchor := c.sourceAnchor
    rowValue := c.rowValue
    sparseIndexValue := c.sparseIndexValue
    coefficient := c.coefficient
    normalizerND := nd.normalizerND

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “boundary rotation angle normalizer proof route coefficient”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem boundaryRotationAngleNormalizerProofRoute_coefficient
    (p : OneTermRobinParameters) (row sparse : Nat) :
    (boundaryRotationAngleNormalizerProofRoute p row sparse).coefficient =
      (boundaryRotationAngleNormalizerContract p row sparse).coefficient := rfl

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “boundary rotation angle normalizer proof route arccos argument”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem boundaryRotationAngleNormalizerProofRoute_arccosArgument
    (p : OneTermRobinParameters) (row sparse : Nat) :
    (boundaryRotationAngleNormalizerProofRoute p row sparse).arccosArgument =
      boundaryRotationNormalizedCoefficient p row sparse := rfl

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “boundary rotation angle normalizer proof route shared nd”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem boundaryRotationAngleNormalizerProofRoute_sharedND
    (p : OneTermRobinParameters) (row sparse : Nat) :
    (boundaryRotationAngleNormalizerProofRoute p row sparse).normalizerBound =
      (derivativeNormalizerNDContract p row sparse).coefficientBound ∧
    (boundaryRotationAngleNormalizerProofRoute p row sparse).coefficientDivision =
      (derivativeNormalizerNDContract p row sparse).divisionSemantics ∧
    (boundaryRotationAngleNormalizerProofRoute p row sparse).realArccosSemantics =
      (derivativeNormalizerNDContract p row sparse).arccosSemantics := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “boundary rotation angle normalizer proof route source bound”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem boundaryRotationAngleNormalizerProofRoute_sourceBound
    (p : OneTermRobinParameters) (row sparse : Nat) :
    (boundaryRotationAngleNormalizerProofRoute p row sparse).coefficient =
      (derivativeNormalizerNDSourceBound p row sparse).sourceCoefficient ∧
    (boundaryRotationAngleNormalizerProofRoute p row sparse).normalizerND =
      (derivativeNormalizerNDSourceBound p row sparse).normalizerND ∧
    (boundaryRotationAngleNormalizerProofRoute p row sparse).normalizerBound =
      (derivativeNormalizerNDSourceBound p row sparse).coefficientBound := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “derivative normalizer nd source bound shared routes”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem derivativeNormalizerNDSourceBound_sharedRoutes
    (p : OneTermRobinParameters) (row sparse : Nat) :
    (sparseAmplitudeOracleDTCoefficientNormalizerProofRoute p row sparse).coefficient =
      (boundaryRotationAngleNormalizerProofRoute p row sparse).coefficient ∧
    (sparseAmplitudeOracleDTCoefficientNormalizerProofRoute p row sparse).normalizerND =
      (boundaryRotationAngleNormalizerProofRoute p row sparse).normalizerND ∧
    (sparseAmplitudeOracleDTCoefficientNormalizerProofRoute p row sparse).normalizerBound =
      (boundaryRotationAngleNormalizerProofRoute p row sparse).normalizerBound := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “robin global sparse amplitude value shared normalizer routes”; the hypotheses and conclusion in the code panel fix its exact scope. Bridge showing that the shared 'N_D' route is now sourced from the active global sparse-slot coefficient table.

theorem robinGlobalSparseAmplitudeValue_sharedNormalizerRoutes
    (p : OneTermRobinParameters) (row sparse : Nat) :
    (derivativeNormalizerNDSourceBound p row sparse).sourceCoefficient =
      robinGlobalSparseAmplitudeValue p.n sparse row ∧
    (sparseAmplitudeOracleDTCoefficientNormalizerProofRoute p row sparse).coefficient =
      robinGlobalSparseAmplitudeValue p.n sparse row ∧
    (boundaryRotationAngleNormalizerProofRoute p row sparse).coefficient =
      robinGlobalSparseAmplitudeValue p.n sparse row ∧
    (sparseAmplitudeOracleDTCoefficientNormalizerProofRoute p row sparse).coefficient =
      (boundaryRotationAngleNormalizerProofRoute p row sparse).coefficient := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “boundary rotation matrix”. Honest Ry_boundary matrix: controlled R_y rotation on the ancilla qubit (bit 0), conditioned on the indicator bit being 0 (boundary row).

def boundaryRotationMatrix (p : OneTermRobinParameters) :
    Matrix (qubitDim (oneTermRobinTotalQubits p)) (qubitDim (oneTermRobinTotalQubits p)) Coeff :=
  fun i j =>
    let n := p.n
    let indPos := robinIndicatorBitPosition p
    let indBit_j := (j.val >>> indPos) &&& 1
    if indBit_j = 1 then
      if i.val = j.val then Coeff.rat 1 else Coeff.rat 0
    else
      let anc_j := j.val &&& 1
      let anc_i := i.val &&& 1

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gate ry boundary”. Gate matrix for Ry_boundary using the honest controlled rotation matrix.

def oneTermRobinGate_Ry_boundary (p : OneTermRobinParameters) : GateMatrix Coeff (oneTermRobinTotalQubits p) where
  gate := Gate.oracleCall "Ry_boundary"
  matrix := boundaryRotationMatrix p
  unitary := {
    description := "Ry_boundary honest controlled rotation matrix: unitarity not yet proved"
    source := "Guseynov-Huang-Liu 2025, Fig. 1-term Robin and Eq. angles for Ry, arXiv:2506.20478"
    proved := false
  }

/--
Guard for the shared `N_D` Phase-1 route.

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “derivative normalizer nd shared route flags false”; the hypotheses and conclusion in the code panel fix its exact scope. Guard for the shared 'N_D' Phase-1 route.

theorem derivativeNormalizerNDSharedRoute_flags_false
    (p : OneTermRobinParameters) (row sparse : Nat) :
    (derivativeNormalizerNDContract p row sparse).nonzeroNormalizer.proved = false ∧
    (derivativeNormalizerNDContract p row sparse).divisionSemantics.proved = false ∧
    (derivativeNormalizerNDContract p row sparse).coefficientBound.proved = false ∧
    (derivativeNormalizerNDContract p row sparse).absSquareSemantics.proved = false ∧
    (derivativeNormalizerNDContract p row sparse).sqrtComplementSemantics.proved = false ∧
    (derivativeNormalizerNDContract p row sparse).arccosSemantics.proved = false ∧
    (derivativeNormalizerNDContract p row sparse).twoByTwoUnitary.proved = false ∧
    (sparseAmplitudeOracleDTCoefficientNormalizerProofRoute p row sparse).coefficientDivision.proved = false ∧
    (sparseAmplitudeOracleDTCoefficientNormalizerProofRoute p row sparse).normalizerBound.proved = false ∧

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “derivative normalizer nd shared route source bound and flags”; the hypotheses and conclusion in the code panel fix its exact scope. Combined Phase-1 guard for the shared 'N_D' route.

theorem derivativeNormalizerNDSharedRoute_sourceBoundAndFlags
    (p : OneTermRobinParameters) (row sparse : Nat) :
    ((sparseAmplitudeOracleDTCoefficientNormalizerProofRoute p row sparse).coefficient =
        (derivativeNormalizerNDSourceBound p row sparse).sourceCoefficient ∧
      (sparseAmplitudeOracleDTCoefficientNormalizerProofRoute p row sparse).normalizerND =
        (derivativeNormalizerNDSourceBound p row sparse).normalizerND ∧
      (sparseAmplitudeOracleDTCoefficientNormalizerProofRoute p row sparse).normalizerBound =
        (derivativeNormalizerNDSourceBound p row sparse).coefficientBound) ∧
    ((boundaryRotationAngleNormalizerProofRoute p row sparse).coefficient =
        (derivativeNormalizerNDSourceBound p row sparse).sourceCoefficient ∧
      (boundaryRotationAngleNormalizerProofRoute p row sparse).normalizerND =

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “banded sparse access matrix”. Interim O_D^BS column-map helper, not the faithful Lemma 1 paper oracle.

def bandedSparseAccessMatrix (p : OneTermRobinParameters) :
    Matrix (qubitDim (oneTermRobinTotalQubits p)) (qubitDim (oneTermRobinTotalQubits p)) Coeff :=
  fun i j =>
    let n := p.n
    let kappa := p.kappa
    let κbits := clog2 kappa
    let odPure := n - κbits
    let sysMask := (1 <<< n) - 1
    let sysVal := (j.val >>> 1) &&& sysMask
    let sparseStart := 1 + n + odPure
    let sparseMask := (1 <<< κbits) - 1

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gate o d bs”. Gate record for the faithful Lemma 1 O_D^BS paper-image matrix skeleton.

def oneTermRobinGate_O_D_BS (p : OneTermRobinParameters) : GateMatrix Coeff (oneTermRobinTotalQubits p) where
  gate := Gate.oracleCall "O_D^BS"
  matrix := bandedSparseAccessPaperMatrix p
  unitary := {
    description := "O_D^BS paper-image matrix skeleton: unitarity and cleanup not yet proved"
    source := "Guseynov-Huang-Liu 2025, Lemma 1, arXiv:2506.20478"
    proved := false
  }

/-- Active forward `O_D^BS` gate entry at the finite paper image. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “one term robin gate o d bs image fin eq one”; the hypotheses and conclusion in the code panel fix its exact scope. Active forward 'O_D^BS' gate entry at the finite paper image.

theorem oneTermRobinGate_O_D_BS_imageFin_eq_one
    (p : OneTermRobinParameters)
    (j : Fin (qubitDim (oneTermRobinTotalQubits p)))
    (haddr : bandedSparseAccessPaperAddress p j.val < (1 <<< p.n)) :
    (oneTermRobinGate_O_D_BS p).matrix
        (bandedSparseAccessPaperImageFin p j haddr) j =
      Coeff.rat 1 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “one term robin gate o d bs contract drift column 8 n 3”; the hypotheses and conclusion in the code panel fix its exact scope. Concrete contract-drift guard separating the active Lemma 1 paper-image matrix from the legacy sparse-column helper.

theorem oneTermRobinGate_O_D_BS_contractDrift_column8_n3 :
    let p : OneTermRobinParameters :=
      { n := 3, kappa := 7, functionPieces := 1, polynomialDegreeCost := 1 }
    bandedSparseAccessPaperImage p 8 = 40 ∧
      (oneTermRobinGate_O_D_BS p).matrix
          ⟨40, by native_decide⟩ ⟨8, by native_decide⟩ = Coeff.rat 1 ∧
      (oneTermRobinGate_O_D_BS p).matrix
          ⟨4, by native_decide⟩ ⟨8, by native_decide⟩ = Coeff.rat 0 ∧
      (bandedSparseAccessMatrix p)
          ⟨4, by native_decide⟩ ⟨8, by native_decide⟩ = Coeff.rat 1 ∧
      (oneTermRobinGate_O_D_BS p).unitary.proved = false := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “one term robin gate o d bs boundary unused sparse collision n 3”; the hypotheses and conclusion in the code panel fix its exact scope. Concrete rejected-model collision for the old row-dependent 'O_D^BS' address.

theorem oneTermRobinGate_O_D_BS_boundaryUnusedSparseCollision_n3 :
    let p : OneTermRobinParameters :=
      { n := 3, kappa := 7, functionPieces := 1, polynomialDegreeCost := 1 }
    bandedSparseAccessPaperCleanInput p 0 = true ∧
      bandedSparseAccessPaperCleanInput p 48 = true ∧
      (bandedSparseAccessPaperRegisters p 0).rowValue = 0 ∧
      (bandedSparseAccessPaperRegisters p 48).rowValue = 0 ∧
      (bandedSparseAccessPaperRegisters p 0).sparseIndexValue = 0 ∧
      (bandedSparseAccessPaperRegisters p 48).sparseIndexValue = 3 ∧
      bandedSparseAccessRowDependentPaperAddress p 0 = 0 ∧
      bandedSparseAccessRowDependentPaperAddress p 48 = 0 ∧

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “one term robin gate o d bs global sparse boundary no collision n 3”; the hypotheses and conclusion in the code panel fix its exact scope. Concrete regression that the corrected active global-slot image separates the old boundary unused-sparse collision columns.

theorem oneTermRobinGate_O_D_BS_globalSparseBoundaryNoCollision_n3 :
    let p : OneTermRobinParameters :=
      { n := 3, kappa := 7, functionPieces := 1, polynomialDegreeCost := 1 }
    bandedSparseAccessPaperCleanInput p 0 = true ∧
      bandedSparseAccessPaperCleanInput p 48 = true ∧
      bandedSparseAccessPaperAddress p 0 = 6 ∧
      bandedSparseAccessPaperAddress p 48 = 1 ∧
      bandedSparseAccessPaperImage p 0 = 96 ∧
      bandedSparseAccessPaperImage p 48 = 16 ∧
      bandedSparseAccessPaperImage p 0 ≠ bandedSparseAccessPaperImage p 48 ∧
      (oneTermRobinGate_O_D_BS p).matrix

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper global slot source boundary columns n 3”; the hypotheses and conclusion in the code panel fix its exact scope. The old boundary collision columns are both in the faithful global-slot source domain even though one of them is outside the rejected row-dependent nonzero-branch classifier.

theorem bandedSparseAccessPaperGlobalSlotSource_boundaryColumns_n3 :
    let p : OneTermRobinParameters :=
      { n := 3, kappa := 7, functionPieces := 1, polynomialDegreeCost := 1 }
    bandedSparseAccessPaperGlobalSlotSource p 0 = true ∧
      bandedSparseAccessPaperGlobalSlotSource p 48 = true ∧
      bandedSparseAccessPaperValidCleanSource p 48 = false ∧
      bandedSparseAccessPaperImage p 0 ≠ bandedSparseAccessPaperImage p 48 ∧
      (oneTermRobinGate_O_D_BS p).unitary.proved = false := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper global slot source encoded out of range n 3”; the hypotheses and conclusion in the code panel fix its exact scope. Encoded sparse value '7' is the first out-of-range slot for the one-term 'kappa = 7' contract.

theorem bandedSparseAccessPaperGlobalSlotSource_encodedOutOfRange_n3 :
    let p : OneTermRobinParameters :=
      { n := 3, kappa := 7, functionPieces := 1, polynomialDegreeCost := 1 }
    bandedSparseAccessPaperCleanInput p 112 = true ∧
      (bandedSparseAccessPaperRegisters p 112).sparseIndexValue = 7 ∧
      bandedSparseAccessPaperSparseIndexInKappa p 112 = false ∧
      bandedSparseAccessPaperGlobalSlotSource p 112 = false ∧
      (oneTermRobinGate_O_D_BS p).unitary.proved = false := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “robin function value”. Symbolic function value at grid point j.

def robinFunctionValue (n i : Nat) : Coeff :=
  Coeff.symbol s!"f_{n}_{i}"

/--
Register values used by the paper-level function oracle `O_f` contract.

The compound-index convention stores the system row in bits `[1, 1+n)` and
stores the `m_f` function-oracle workspace immediately above the indicator bit,
starting at `robinIndicatorBitPosition p + 1`.  This record is a source-contract
skeleton for the paper's clean-workspace equation; it does not assert the
amplitude relation or workspace cleanup.

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “function oracle paper registers”. A proposition-valued field is a requirement until a constructor supplies it. Register values used by the paper-level function oracle 'O_f' contract.

structure FunctionOraclePaperRegisters where
  systemValue : Nat
  mfWorkspaceValue : Nat
  nonMFValue : Nat
  cleanWorkspace : Bool
deriving Repr, DecidableEq

/--
Extract the system register and the `m_f` function workspace from a compound
basis index for the `O_f` source contract.

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “function oracle paper registers”. Extract the system register and the 'm_f' function workspace from a compound basis index for the 'O_f' source contract.

def functionOraclePaperRegisters (p : OneTermRobinParameters) (j : Nat) :
    FunctionOraclePaperRegisters :=
  let n := p.n
  let rp := defaultRobinRegisterPartition p
  let sysMask := (1 <<< n) - 1
  let mfStart := robinIndicatorBitPosition p + 1
  let mfMask := (1 <<< rp.mfQubits) - 1
  let mfValue := (j >>> mfStart) &&& mfMask
  {
    systemValue := (j >>> 1) &&& sysMask
    mfWorkspaceValue := mfValue

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “function oracle normalized value”. Symbolic normalized clean-branch amplitude for the paper's function oracle.

def functionOracleNormalizedValue (p : OneTermRobinParameters) (i : Nat) : Coeff :=
  Coeff.mul (robinFunctionValue p.n i) (Coeff.symbol "N_f_inv")

/--
Paper-image source contract for one column of the function oracle `O_f`.

The clean branch records the displayed paper component
`(f(x_i)/N_f)|0>^mf|i>`.  The orthogonal component and all analytic side
conditions are tracked as false obligations; this record is not a matrix proof
and does not promote the current diagonal helper to a faithful oracle.
-/

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “function oracle paper image”. A proposition-valued field is a requirement until a constructor supplies it. Paper-image source contract for one column of the function oracle 'O_f'.

structure FunctionOraclePaperImage where
  sourceAnchor : String
  inputRegisters : FunctionOraclePaperRegisters
  cleanBranchBasisIndex : Nat
  cleanBranchSystemValue : Nat
  cleanBranchWorkspaceValue : Nat
  cleanBranchAmplitude : Coeff
  orthogonalComponent : String
  systemPreserved : Bool
  cleanWorkspaceBranch : Bool
  normalizedAmplitudeCorrect : ObligationRecord

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “function oracle paper image”. Build the paper-level 'O_f' image contract for one compound basis column.

def functionOraclePaperImage (p : OneTermRobinParameters) (j : Nat) :
    FunctionOraclePaperImage :=
  let regs := functionOraclePaperRegisters p j
  {
    sourceAnchor := "Guseynov-Huang-Liu 2025, function oracle O_f, arXiv:2506.20478"
    inputRegisters := regs
    cleanBranchBasisIndex := regs.nonMFValue
    cleanBranchSystemValue := regs.systemValue
    cleanBranchWorkspaceValue := 0
    cleanBranchAmplitude := functionOracleNormalizedValue p regs.systemValue
    orthogonalComponent := s!"orth_f_{p.n}_{regs.systemValue}"

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “function oracle paper image input registers eq”; the hypotheses and conclusion in the code panel fix its exact scope. Bridge lemma: the 'O_f' paper image uses the shared register extractor.

theorem functionOraclePaperImage_inputRegisters_eq
    (p : OneTermRobinParameters) (j : Nat) :
    (functionOraclePaperImage p j).inputRegisters =
      functionOraclePaperRegisters p j := rfl

/-- Bridge lemma: the clean `O_f` branch clears only the `m_f` workspace bits. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “function oracle paper image clean branch basis index eq”; the hypotheses and conclusion in the code panel fix its exact scope. Bridge lemma: the clean 'O_f' branch clears only the 'm_f' workspace bits.

theorem functionOraclePaperImage_cleanBranchBasisIndex_eq
    (p : OneTermRobinParameters) (j : Nat) :
    (functionOraclePaperImage p j).cleanBranchBasisIndex =
      (functionOraclePaperRegisters p j).nonMFValue := rfl

/-- Bridge lemma: the clean `O_f` branch preserves the extracted system value. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “function oracle paper image clean branch system value eq”; the hypotheses and conclusion in the code panel fix its exact scope. Bridge lemma: the clean 'O_f' branch preserves the extracted system value.

theorem functionOraclePaperImage_cleanBranchSystemValue_eq
    (p : OneTermRobinParameters) (j : Nat) :
    (functionOraclePaperImage p j).cleanBranchSystemValue =
      (functionOraclePaperRegisters p j).systemValue := rfl

/-- Bridge lemma: the clean `O_f` branch has zero `m_f` workspace value. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “function oracle paper image clean branch workspace value eq”; the hypotheses and conclusion in the code panel fix its exact scope. Bridge lemma: the clean 'O_f' branch has zero 'm_f' workspace value.

theorem functionOraclePaperImage_cleanBranchWorkspaceValue_eq
    (p : OneTermRobinParameters) (j : Nat) :
    (functionOraclePaperImage p j).cleanBranchWorkspaceValue = 0 := rfl

/--
Bridge lemma: the clean `O_f` branch amplitude is the normalized function value
at the system value extracted from the same column.
-/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “function oracle paper image clean branch amplitude eq”; the hypotheses and conclusion in the code panel fix its exact scope. Bridge lemma: the clean 'O_f' branch amplitude is the normalized function value at the system value extracted from the same column.

theorem functionOraclePaperImage_cleanBranchAmplitude_eq
    (p : OneTermRobinParameters) (j : Nat) :
    (functionOraclePaperImage p j).cleanBranchAmplitude =
      functionOracleNormalizedValue p (functionOraclePaperRegisters p j).systemValue := rfl

/-- Bridge lemma: the clean-workspace branch flag is inherited from the extractor. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “function oracle paper image clean workspace branch eq”; the hypotheses and conclusion in the code panel fix its exact scope. Bridge lemma: the clean-workspace branch flag is inherited from the extractor.

theorem functionOraclePaperImage_cleanWorkspaceBranch_eq
    (p : OneTermRobinParameters) (j : Nat) :
    (functionOraclePaperImage p j).cleanWorkspaceBranch =
      (functionOraclePaperRegisters p j).cleanWorkspace := rfl

/--
External source transcript for the O_f amplitude-oracle theorem cited by
GHL2025.

This records the theorem and coordinate-oracle equation used as a source
contract for the function oracle.  It does not formalize the cited theorem and

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “function oracle external amplitude source contract”. A proposition-valued field is a requirement until a constructor supplies it. External source transcript for the O_f amplitude-oracle theorem cited by GHL2025.

structure FunctionOracleExternalAmplitudeSourceContract where
  sourceAnchor : String
  theoremAnchor : String
  coordinateOracleAnchor : String
  citedSourceAnchor : String
  cleanBranchFormula : String
  normalizerNf : Coeff
  resourceClaim : ObligationRecord
  externalTheoremFormalized : ObligationRecord
  nonzeroNormalizer : ObligationRecord
  divisionSemantics : ObligationRecord

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “function oracle external amplitude source contract”. Default source transcript for GHL2025's function-oracle dependency.

def functionOracleExternalAmplitudeSourceContract :
    FunctionOracleExternalAmplitudeSourceContract where
  sourceAnchor :=
    "GHL2025 Theorem 'Amplitude-oracle for piece-wise polynomial function' and Eq. 'coordinate oracle', arXiv:2506.20478; cited source arXiv:2411.01131"
  theoremAnchor :=
    "GHL2025 Theorem 'Amplitude-oracle for piece-wise polynomial function'"
  coordinateOracleAnchor := "GHL2025 Eq. 'coordinate oracle'"
  citedSourceAnchor :=
    "Guseynov-Liu 2024, arXiv:2411.01131, Theorem 5"
  cleanBranchFormula := "f(x_i) / N_f"
  normalizerNf := Coeff.symbol "N_f"

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “function oracle external amplitude source contract source anchor”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem functionOracleExternalAmplitudeSourceContract_sourceAnchor :
    functionOracleExternalAmplitudeSourceContract.sourceAnchor =
      "GHL2025 Theorem 'Amplitude-oracle for piece-wise polynomial function' and Eq. 'coordinate oracle', arXiv:2506.20478; cited source arXiv:2411.01131" := rfl

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “function oracle external amplitude source contract flags false”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem functionOracleExternalAmplitudeSourceContract_flags_false :
    functionOracleExternalAmplitudeSourceContract.resourceClaim.proved = false ∧
      functionOracleExternalAmplitudeSourceContract.externalTheoremFormalized.proved = false ∧
      functionOracleExternalAmplitudeSourceContract.nonzeroNormalizer.proved = false ∧
      functionOracleExternalAmplitudeSourceContract.divisionSemantics.proved = false ∧
      functionOracleExternalAmplitudeSourceContract.theoremAmplitudeCorrect.proved = false ∧
      functionOracleExternalAmplitudeSourceContract.closesNormalizerBound = false ∧
      functionOracleExternalAmplitudeSourceContract.closesOrthogonalCompletion = false ∧
      functionOracleExternalAmplitudeSourceContract.closesUnitaryCompletion = false ∧
      functionOracleExternalAmplitudeSourceContract.closesFunctionOracleContract = false := by

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “function oracle amplitude proof route”. A proposition-valued field is a requirement until a constructor supplies it. Refined proof route for the 'of_nf_amplitude_route' block.

structure FunctionOracleAmplitudeProofRoute where
  sourceAnchor : String
  systemValue : Nat
  sourceFunctionValue : Coeff
  normalizerNf : Coeff
  normalizedAmplitude : Coeff
  normalizedAmplitudeFormula : String
  cleanBranchAmplitude : Coeff
  cleanBranchBasisIndex : Nat
  cleanWorkspaceBranch : Bool
  theoremNormalizer : Coeff

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “function oracle amplitude proof route”. Default O_f amplitude-route contract for one compound basis column.

def functionOracleAmplitudeProofRoute
    (p : OneTermRobinParameters) (j : Nat) :
    FunctionOracleAmplitudeProofRoute :=
  let image := functionOraclePaperImage p j
  let source := functionOracleExternalAmplitudeSourceContract
  {
    sourceAnchor := source.sourceAnchor
    systemValue := image.cleanBranchSystemValue
    sourceFunctionValue := robinFunctionValue p.n image.cleanBranchSystemValue
    normalizerNf := source.normalizerNf
    normalizedAmplitude := functionOracleNormalizedValue p image.cleanBranchSystemValue

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “function oracle amplitude proof route source anchor”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem functionOracleAmplitudeProofRoute_sourceAnchor
    (p : OneTermRobinParameters) (j : Nat) :
    (functionOracleAmplitudeProofRoute p j).sourceAnchor =
      "GHL2025 Theorem 'Amplitude-oracle for piece-wise polynomial function' and Eq. 'coordinate oracle', arXiv:2506.20478; cited source arXiv:2411.01131" := rfl

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “function oracle amplitude proof route source function value”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem functionOracleAmplitudeProofRoute_sourceFunctionValue
    (p : OneTermRobinParameters) (j : Nat) :
    (functionOracleAmplitudeProofRoute p j).sourceFunctionValue =
      robinFunctionValue p.n (functionOraclePaperRegisters p j).systemValue := rfl

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “function oracle amplitude proof route normalizer nf”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem functionOracleAmplitudeProofRoute_normalizerNf
    (p : OneTermRobinParameters) (j : Nat) :
    (functionOracleAmplitudeProofRoute p j).normalizerNf =
      Coeff.symbol "N_f" := rfl

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “function oracle amplitude proof route normalized amplitude”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem functionOracleAmplitudeProofRoute_normalizedAmplitude
    (p : OneTermRobinParameters) (j : Nat) :
    (functionOracleAmplitudeProofRoute p j).normalizedAmplitude =
      functionOracleNormalizedValue p (functionOraclePaperRegisters p j).systemValue := rfl

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “function oracle amplitude proof route paper image”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem functionOracleAmplitudeProofRoute_paperImage
    (p : OneTermRobinParameters) (j : Nat) :
    (functionOracleAmplitudeProofRoute p j).cleanBranchAmplitude =
      (functionOraclePaperImage p j).cleanBranchAmplitude ∧
    (functionOracleAmplitudeProofRoute p j).cleanBranchBasisIndex =
      (functionOraclePaperImage p j).cleanBranchBasisIndex ∧
    (functionOracleAmplitudeProofRoute p j).cleanWorkspaceBranch =
      (functionOraclePaperImage p j).cleanWorkspaceBranch := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “function oracle amplitude proof route obligations reuse paper image”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem functionOracleAmplitudeProofRoute_obligations_reuse_paperImage
    (p : OneTermRobinParameters) (j : Nat) :
    (functionOracleAmplitudeProofRoute p j).normalizedAmplitudeCorrect =
      (functionOraclePaperImage p j).normalizedAmplitudeCorrect ∧
    (functionOracleAmplitudeProofRoute p j).normalizerBound =
      (functionOraclePaperImage p j).normalizerBound ∧
    (functionOracleAmplitudeProofRoute p j).orthogonalComponentCorrect =
      (functionOraclePaperImage p j).orthogonalComponentCorrect ∧
    (functionOracleAmplitudeProofRoute p j).unitaryCompletion =
      (functionOraclePaperImage p j).unitaryCompletion := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “function oracle amplitude proof route external source contract”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem functionOracleAmplitudeProofRoute_externalSourceContract
    (p : OneTermRobinParameters) (j : Nat) :
    (functionOracleAmplitudeProofRoute p j).sourceAnchor =
      functionOracleExternalAmplitudeSourceContract.sourceAnchor ∧
    (functionOracleAmplitudeProofRoute p j).normalizerNf =
      functionOracleExternalAmplitudeSourceContract.normalizerNf ∧
    (functionOracleAmplitudeProofRoute p j).normalizedAmplitudeFormula =
      functionOracleExternalAmplitudeSourceContract.cleanBranchFormula ∧
    (functionOracleAmplitudeProofRoute p j).nonzeroNormalizer =
      functionOracleExternalAmplitudeSourceContract.nonzeroNormalizer ∧
    (functionOracleAmplitudeProofRoute p j).divisionSemantics =

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “function oracle amplitude proof route flags false”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem functionOracleAmplitudeProofRoute_flags_false
    (p : OneTermRobinParameters) (j : Nat) :
    (functionOracleAmplitudeProofRoute p j).normalizedAmplitudeCorrect.proved = false ∧
    (functionOracleAmplitudeProofRoute p j).nonzeroNormalizer.proved = false ∧
    (functionOracleAmplitudeProofRoute p j).divisionSemantics.proved = false ∧
    (functionOracleAmplitudeProofRoute p j).normalizerBound.proved = false ∧
    (functionOracleAmplitudeProofRoute p j).orthogonalComponentCorrect.proved = false ∧
    (functionOracleAmplitudeProofRoute p j).unitaryCompletion.proved = false ∧
    (functionOracleAmplitudeProofRoute p j).theoremAmplitudeCorrect.proved = false := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “function oracle amplitude proof route external source and flags”; the hypotheses and conclusion in the code panel fix its exact scope. Combined Phase-1 guard for the 'O_f' external-source route.

theorem functionOracleAmplitudeProofRoute_externalSourceAndFlags
    (p : OneTermRobinParameters) (j : Nat) :
    ((functionOracleAmplitudeProofRoute p j).sourceAnchor =
        functionOracleExternalAmplitudeSourceContract.sourceAnchor ∧
      (functionOracleAmplitudeProofRoute p j).normalizerNf =
        functionOracleExternalAmplitudeSourceContract.normalizerNf ∧
      (functionOracleAmplitudeProofRoute p j).normalizedAmplitudeFormula =
        functionOracleExternalAmplitudeSourceContract.cleanBranchFormula ∧
      (functionOracleAmplitudeProofRoute p j).nonzeroNormalizer =
        functionOracleExternalAmplitudeSourceContract.nonzeroNormalizer ∧
      (functionOracleAmplitudeProofRoute p j).divisionSemantics =

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “function oracle orthogonal entry”. Symbolic matrix entry for the unresolved orthogonal component of 'O_f'.

def functionOracleOrthogonalEntry
    (p : OneTermRobinParameters) (systemValue row col : Nat) : Coeff :=
  Coeff.symbol s!"orth_f_entry_{p.n}_{systemValue}_{row}_{col}"

/--
Faithful Phase 1 matrix skeleton for the paper-level function oracle `O_f`.

For each clean-workspace input column, the clean `m_f` branch entry is the
normalized amplitude recorded by `functionOraclePaperImage`, namely
`f(x_i) / N_f` represented as `functionOracleNormalizedValue`.  Other
clean-workspace output rows are zero, matching the paper statement that the

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “function oracle paper matrix”. Faithful Phase 1 matrix skeleton for the paper-level function oracle 'O_f'.

def functionOraclePaperMatrix (p : OneTermRobinParameters) :
    Matrix (qubitDim (oneTermRobinTotalQubits p)) (qubitDim (oneTermRobinTotalQubits p)) Coeff :=
  fun i j =>
    let image := functionOraclePaperImage p j.val
    if image.cleanWorkspaceBranch then
      if i.val = image.cleanBranchBasisIndex then
        image.cleanBranchAmplitude
      else if (functionOraclePaperRegisters p i.val).mfWorkspaceValue = 0 then
        Coeff.rat 0
      else
        functionOracleOrthogonalEntry p image.cleanBranchSystemValue i.val j.val

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “function oracle paper matrix clean branch entry”; the hypotheses and conclusion in the code panel fix its exact scope. The 'O_f' paper matrix exposes the clean branch amplitude for clean input columns.

theorem functionOraclePaperMatrix_cleanBranch_entry
    (p : OneTermRobinParameters)
    (i j : Fin (qubitDim (oneTermRobinTotalQubits p)))
    (hClean : (functionOraclePaperImage p j.val).cleanWorkspaceBranch = true)
    (h : i.val = (functionOraclePaperImage p j.val).cleanBranchBasisIndex) :
    functionOraclePaperMatrix p i j =
      (functionOraclePaperImage p j.val).cleanBranchAmplitude := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “function oracle paper matrix clean workspace off branch zero”; the hypotheses and conclusion in the code panel fix its exact scope. Other clean-workspace rows have zero 'O_f' orthogonal-completion entry.

theorem functionOraclePaperMatrix_cleanWorkspace_offBranch_zero
    (p : OneTermRobinParameters)
    (i j : Fin (qubitDim (oneTermRobinTotalQubits p)))
    (hInputClean : (functionOraclePaperImage p j.val).cleanWorkspaceBranch = true)
    (hBranch : i.val ≠ (functionOraclePaperImage p j.val).cleanBranchBasisIndex)
    (hClean : (functionOraclePaperRegisters p i.val).mfWorkspaceValue = 0) :
    functionOraclePaperMatrix p i j = Coeff.rat 0 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “function oracle paper matrix non clean input entry”; the hypotheses and conclusion in the code panel fix its exact scope. Non-clean input columns are left in the symbolic 'O_f' completion branch.

theorem functionOraclePaperMatrix_nonCleanInput_entry
    (p : OneTermRobinParameters)
    (i j : Fin (qubitDim (oneTermRobinTotalQubits p)))
    (hInputNonClean : (functionOraclePaperImage p j.val).cleanWorkspaceBranch = false) :
    functionOraclePaperMatrix p i j =
      functionOracleOrthogonalEntry p
        (functionOraclePaperImage p j.val).cleanBranchSystemValue i.val j.val := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “function oracle matrix”. Helper-only O_f diagonal matrix: records function values f(x_j) on the diagonal.

def functionOracleMatrix (p : OneTermRobinParameters) :
    Matrix (qubitDim (oneTermRobinTotalQubits p)) (qubitDim (oneTermRobinTotalQubits p)) Coeff :=
  fun i j =>
    if i.val = j.val then
      let n := p.n
      let sysMask := (1 <<< n) - 1
      let sysVal := (j.val >>> 1) &&& sysMask
      robinFunctionValue n sysVal
    else Coeff.rat 0

/--

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gate o f”. Gate matrix for 'O_f' using the faithful paper-image matrix skeleton.

def oneTermRobinGate_O_f (p : OneTermRobinParameters) : GateMatrix Coeff (oneTermRobinTotalQubits p) where
  gate := Gate.oracleCall "O_f"
  matrix := functionOraclePaperMatrix p
  unitary := {
    description := "O_f paper-image matrix skeleton: clean branch wired, orthogonal completion and unitarity not yet proved"
    source := "Guseynov-Huang-Liu 2025, Theorem amplitude-oracle for piece-wise polynomial function and Fig. 1-term Robin, arXiv:2506.20478"
    proved := false
  }

/--
Honest SWAP matrix: permutation matrix swapping the system register

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “swap oracle matrix”. Honest SWAP matrix: permutation matrix swapping the system register (n qubits at bits [1, 1+n)) with the O_D^BS register (n qubits at bits [1+n, 1+2n)).

def swapOracleMatrix (p : OneTermRobinParameters) :
    Matrix (qubitDim (oneTermRobinTotalQubits p)) (qubitDim (oneTermRobinTotalQubits p)) Coeff :=
  fun i j =>
    let n := p.n
    let blockMask := (1 <<< n) - 1
    let block1 := (j.val >>> 1) &&& blockMask
    let block2 := (j.val >>> (1 + n)) &&& blockMask
    let diff := block1 ^^^ block2
    let swapped := j.val ^^^ (diff <<< 1) ^^^ (diff <<< (1 + n))
    if i.val = swapped then Coeff.rat 1 else Coeff.rat 0

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “swap oracle image”. Image function for the SWAP oracle: swaps two n-qubit register blocks.

def swapOracleImage (p : OneTermRobinParameters) (j : Nat) : Nat :=
  let n := p.n
  let blockMask := (1 <<< n) - 1
  let block1 := (j >>> 1) &&& blockMask
  let block2 := (j >>> (1 + n)) &&& blockMask
  let diff := block1 ^^^ block2
  j ^^^ (diff <<< 1) ^^^ (diff <<< (1 + n))

/--
The n-bit XOR difference between the two register blocks exchanged by SWAP.

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “swap oracle diff”. The n-bit XOR difference between the two register blocks exchanged by SWAP.

def swapOracleDiff (p : OneTermRobinParameters) (j : Nat) : Nat :=
  let n := p.n
  let blockMask := (1 <<< n) - 1
  let block1 := (j >>> 1) &&& blockMask
  let block2 := (j >>> (1 + n)) &&& blockMask
  block1 ^^^ block2

/-- The SWAP image is the source index XORed by the same difference in both blocks. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “swap oracle image eq xor diff”; the hypotheses and conclusion in the code panel fix its exact scope. The SWAP image is the source index XORed by the same difference in both blocks.

theorem swapOracleImage_eq_xor_diff (p : OneTermRobinParameters) (j : Nat) :
    swapOracleImage p j =
      j ^^^ (swapOracleDiff p j <<< 1) ^^^
        (swapOracleDiff p j <<< (1 + p.n)) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “swap oracle matrix eq image”; the hypotheses and conclusion in the code panel fix its exact scope. swapOracleMatrix entry equals image function check.

theorem swapOracleMatrix_eq_image (p : OneTermRobinParameters)
    (i j : Fin (qubitDim (oneTermRobinTotalQubits p))) :
    swapOracleMatrix p i j =
      if i.val = swapOracleImage p j.val then Coeff.rat 1 else Coeff.rat 0 := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gate swap”. Gate matrix for SWAP using the honest permutation matrix.

def oneTermRobinGate_SWAP (p : OneTermRobinParameters) : GateMatrix Coeff (oneTermRobinTotalQubits p) where
  gate := Gate.swap 0 0
  matrix := swapOracleMatrix p
  unitary := {
    description := "SWAP permutation matrix: unitarity backed by swapOracleMatrix_is_permutation"
    source := "Guseynov-Huang-Liu 2025, Fig. 1-term Robin SWAP operation, arXiv:2506.20478"
    proved := true
  }

/--
Transpose-style matrix for O_D^BS, sharing the forward sparse-access image map.

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “banded sparse access dagger matrix”. Transpose-style matrix for O_D^BS, sharing the forward sparse-access image map.

def bandedSparseAccessDaggerMatrix (p : OneTermRobinParameters) :
    Matrix (qubitDim (oneTermRobinTotalQubits p)) (qubitDim (oneTermRobinTotalQubits p)) Coeff :=
  fun i j =>
    let n := p.n
    let kappa := p.kappa
    let κbits := clog2 kappa
    let odPure := n - κbits
    let sysMask := (1 <<< n) - 1
    let sysVal := (i.val >>> 1) &&& sysMask
    let sparseStart := 1 + n + odPure
    let sparseMask := (1 <<< κbits) - 1

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gate o d bs dagger”. Gate matrix for '(O_D^BS)^†' using the transpose-style paper-image matrix.

def oneTermRobinGate_O_D_BS_dagger (p : OneTermRobinParameters) : GateMatrix Coeff (oneTermRobinTotalQubits p) where
  gate := Gate.oracleCall "(O_D^BS)^†"
  matrix := bandedSparseAccessPaperDaggerMatrix p
  unitary := {
    description := "(O_D^BS)^† paper-image transpose matrix: cleanup and unitarity not yet proved"
    source := "Guseynov-Huang-Liu 2025, Fig. 1-term Robin and Lemma 1, arXiv:2506.20478"
    proved := false
  }

/-- Active `(O_D^BS)^†` gate entry paired with the finite forward image. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “one term robin gate o d bs dagger image fin eq one”; the hypotheses and conclusion in the code panel fix its exact scope. Active '(O_D^BS)^†' gate entry paired with the finite forward image.

theorem oneTermRobinGate_O_D_BS_dagger_imageFin_eq_one
    (p : OneTermRobinParameters)
    (j : Fin (qubitDim (oneTermRobinTotalQubits p)))
    (haddr : bandedSparseAccessPaperAddress p j.val < (1 <<< p.n)) :
    (oneTermRobinGate_O_D_BS_dagger p).matrix j
        (bandedSparseAccessPaperImageFin p j haddr) =
      Coeff.rat 1 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “one term robin gate o d bs dagger post swap entry of preimage”; the hypotheses and conclusion in the code panel fix its exact scope. Post-SWAP dagger entry from an explicitly supplied paper-image preimage.

theorem oneTermRobinGate_O_D_BS_dagger_postSwap_entry_of_preimage
    (p : OneTermRobinParameters)
    (source post pre : Fin (qubitDim (oneTermRobinTotalQubits p)))
    (hpost : post.val =
      swapOracleImage p
        (bandedSparseAccessPaperImage p source.val))
    (hpre : post.val = bandedSparseAccessPaperImage p pre.val) :
    (oneTermRobinGate_O_D_BS_dagger p).matrix pre post = Coeff.rat 1 := by

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “banded sparse access post swap cleanup”. A proposition-valued field is a requirement until a constructor supplies it. Proof-carrying interface for a supplied post-SWAP cleanup preimage.

structure BandedSparseAccessPostSwapCleanup
    (p : OneTermRobinParameters)
    (source post pre : Fin (qubitDim (oneTermRobinTotalQubits p))) where
  postSwap :
    post.val = swapOracleImage p (bandedSparseAccessPaperImage p source.val)
  preimage : post.val = bandedSparseAccessPaperImage p pre.val
  preCleanInput : bandedSparseAccessPaperCleanInput p pre.val = true
  preAddressBound : bandedSparseAccessPaperAddress p pre.val < (1 <<< p.n)
  daggerEntry : (oneTermRobinGate_O_D_BS_dagger p).matrix pre post = Coeff.rat 1
  preRowPreserved :
    (bandedSparseAccessPaperColumnContract p pre.val).rowPreserved = true

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “banded sparse access post swap cleanup of preimage”. Build the post-SWAP cleanup witness from an explicitly supplied preimage.

def bandedSparseAccessPostSwapCleanup_of_preimage
    (p : OneTermRobinParameters)
    (source post pre : Fin (qubitDim (oneTermRobinTotalQubits p)))
    (hpost : post.val =
      swapOracleImage p
        (bandedSparseAccessPaperImage p source.val))
    (hpre : post.val = bandedSparseAccessPaperImage p pre.val)
    (hclean : bandedSparseAccessPaperCleanInput p pre.val = true)
    (haddr : bandedSparseAccessPaperAddress p pre.val < (1 <<< p.n)) :
    BandedSparseAccessPostSwapCleanup p source post pre := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “one term robin gate o d bs image fin entry safety”; the hypotheses and conclusion in the code panel fix its exact scope. Reusable image witness for the active Lemma 1 'O_D^BS' gate pair.

theorem oneTermRobinGate_O_D_BS_imageFin_entrySafety
    (p : OneTermRobinParameters)
    (j : Fin (qubitDim (oneTermRobinTotalQubits p)))
    (haddr : bandedSparseAccessPaperAddress p j.val < (1 <<< p.n)) :
    (oneTermRobinGate_O_D_BS p).matrix
        (bandedSparseAccessPaperImageFin p j haddr) j = Coeff.rat 1 ∧
      (oneTermRobinGate_O_D_BS_dagger p).matrix j
        (bandedSparseAccessPaperImageFin p j haddr) = Coeff.rat 1 ∧
      (bandedSparseAccessPaperRegisters p
        (bandedSparseAccessPaperImage p j.val)).rowValue =
          (bandedSparseAccessPaperRegisters p j.val).rowValue ∧

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “one term robin gate o d bs global slot source entry safety”; the hypotheses and conclusion in the code panel fix its exact scope. Global-source specialization of the active Lemma 1 'O_D^BS' entry witness.

theorem oneTermRobinGate_O_D_BS_globalSlotSource_entrySafety
    (p : OneTermRobinParameters)
    (j : Fin (qubitDim (oneTermRobinTotalQubits p)))
    (hn : 2 ≤ p.n)
    (hsource : bandedSparseAccessPaperGlobalSlotSource p j.val = true) :
    bandedSparseAccessPaperCleanInput p j.val = true ∧
      (bandedSparseAccessPaperRegisters p j.val).sparseIndexValue < p.kappa ∧
      ∃ image : Fin (qubitDim (oneTermRobinTotalQubits p)),
        image.val = bandedSparseAccessPaperImage p j.val ∧
          (oneTermRobinGate_O_D_BS p).matrix image j = Coeff.rat 1 ∧
          (oneTermRobinGate_O_D_BS_dagger p).matrix j image = Coeff.rat 1 ∧

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gate matrix placeholders”. List of all 7 gate matrix placeholders for the one-term Robin circuit, in the same order as 'oneTermRobinCircuit'.

def oneTermRobinGateMatrixPlaceholders (p : OneTermRobinParameters) :
    List (GateMatrix Coeff (oneTermRobinTotalQubits p)) :=
  [ oneTermRobinGate_U_indic p
  , oneTermRobinGate_O_DT_S p
  , oneTermRobinGate_Ry_boundary p
  , oneTermRobinGate_O_D_BS p
  , oneTermRobinGate_O_f p
  , oneTermRobinGate_SWAP p
  , oneTermRobinGate_O_D_BS_dagger p
  ]

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “one term robin placeholders match”; the hypotheses and conclusion in the code panel fix its exact scope. The placeholder gate matrices match the circuit gate labels.

theorem oneTermRobinPlaceholdersMatch (p : OneTermRobinParameters) :
    gateMatricesMatchCircuit oneTermRobinCircuit (oneTermRobinGateMatrixPlaceholders p) = true := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “one term robin gate matrix placeholders gate list”; the hypotheses and conclusion in the code panel fix its exact scope. The active matrix placeholder list uses the same gate order as Fig.

theorem oneTermRobinGateMatrixPlaceholders_gateList
    (p : OneTermRobinParameters) :
    (oneTermRobinGateMatrixPlaceholders p).map
        (fun gateMatrix => gateMatrix.gate) =
      oneTermRobinCircuit := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “one term robin gate matrix placeholders unitary flags”; the hypotheses and conclusion in the code panel fix its exact scope. The active seven-gate matrix list keeps only the locally certified indicator and SWAP gates marked as proved.

theorem oneTermRobinGateMatrixPlaceholders_unitaryFlags
    (p : OneTermRobinParameters) :
    (oneTermRobinGateMatrixPlaceholders p).map
        (fun gateMatrix => gateMatrix.unitary.proved) =
      [true, false, false, false, false, true, false] := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “indicator oracle image”. Indicator oracle image function: for each basis state j, computes the image by XORing the indicator bit at position indPos when the system register value is in the bulk window [K1, K2].

def indicatorOracleImage (p : OneTermRobinParameters) (j : Nat) : Nat :=
  let n := p.n
  let indPos := robinIndicatorBitPosition p
  let systemVal := (j >>> 1) &&& ((1 <<< n) - 1)
  let K1 := 2
  let K2 := gridSize n - 3
  let isBulk := if K1 ≤ systemVal ∧ systemVal ≤ K2 then (1 : Nat) else 0
  j ^^^ (isBulk <<< indPos)

/--
The indicator oracle matrix entry is 1 exactly when i = indicatorOracleImage j.

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “indicator oracle matrix eq image”; the hypotheses and conclusion in the code panel fix its exact scope. The indicator oracle matrix entry is 1 exactly when i = indicatorOracleImage j.

theorem indicatorOracleMatrix_eq_image (p : OneTermRobinParameters)
    (i j : Fin (qubitDim (oneTermRobinTotalQubits p))) :
    indicatorOracleMatrix p i j =
      if i.val = indicatorOracleImage p j.val then Coeff.rat 1 else Coeff.rat 0 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “indicator oracle image self inverse n 1”; the hypotheses and conclusion in the code panel fix its exact scope. Self-inverse property for n=1: applying indicatorOracleImage twice returns the original value for all j in Fin domain (128 elements).

theorem indicatorOracleImage_self_inverse_n1 :
    ∀ j : Fin (qubitDim (oneTermRobinTotalQubits
      { n := 1, kappa := 1, functionPieces := 1, polynomialDegreeCost := 1 })),
      indicatorOracleImage
        { n := 1, kappa := 1, functionPieces := 1, polynomialDegreeCost := 1 }
        (indicatorOracleImage
          { n := 1, kappa := 1, functionPieces := 1, polynomialDegreeCost := 1 } j) = j := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “indicator oracle image self inverse n 3”; the hypotheses and conclusion in the code panel fix its exact scope. Self-inverse property for n=3: applying indicatorOracleImage twice returns the original value for all j in Fin domain (8192 elements).

theorem indicatorOracleImage_self_inverse_n3 :
    ∀ j : Fin (qubitDim (oneTermRobinTotalQubits
      { n := 3, kappa := 7, functionPieces := 1, polynomialDegreeCost := 1 })),
      indicatorOracleImage
        { n := 3, kappa := 7, functionPieces := 1, polynomialDegreeCost := 1 }
        (indicatorOracleImage
          { n := 3, kappa := 7, functionPieces := 1, polynomialDegreeCost := 1 } j) = j := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “indicator oracle image injective n 1”; the hypotheses and conclusion in the code panel fix its exact scope. Injectivity for n=1: derived from self-inverse property.

theorem indicatorOracleImage_injective_n1 {j₁ j₂ : Fin (qubitDim (oneTermRobinTotalQubits
      { n := 1, kappa := 1, functionPieces := 1, polynomialDegreeCost := 1 }))}
    (h : indicatorOracleImage
        { n := 1, kappa := 1, functionPieces := 1, polynomialDegreeCost := 1 } j₁ =
      indicatorOracleImage
        { n := 1, kappa := 1, functionPieces := 1, polynomialDegreeCost := 1 } j₂) :
    j₁ = j₂ := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “indicator oracle image injective n 3”; the hypotheses and conclusion in the code panel fix its exact scope. Injectivity for n=3: derived from self-inverse property.

theorem indicatorOracleImage_injective_n3 {j₁ j₂ : Fin (qubitDim (oneTermRobinTotalQubits
      { n := 3, kappa := 7, functionPieces := 1, polynomialDegreeCost := 1 }))}
    (h : indicatorOracleImage
        { n := 3, kappa := 7, functionPieces := 1, polynomialDegreeCost := 1 } j₁ =
      indicatorOracleImage
        { n := 3, kappa := 7, functionPieces := 1, polynomialDegreeCost := 1 } j₂) :
    j₁ = j₂ := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “shift left land mask eq zero”; the hypotheses and conclusion in the code panel fix its exact scope. Cycle 12 helper: (b <<< pos) &&& ((1 <<< n) - 1) = 0 when pos >= n, because b <<< pos has all zeros in bits [0, pos) >= [0, n).

theorem shiftLeft_land_mask_eq_zero (b pos n : Nat) (h : pos ≥ n) :
    (b <<< pos) &&& ((1 <<< n) - 1) = 0 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “xor shift preserve low”; the hypotheses and conclusion in the code panel fix its exact scope. Cycle 12 helper: XOR with a value shifted left by 'pos' preserves the low 'n' bits when 'pos >= n'.

theorem xor_shift_preserve_low (x b pos n : Nat) (h : pos ≥ n) :
    (x ^^^ (b <<< pos)) &&& ((1 <<< n) - 1) = x &&& ((1 <<< n) - 1) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “xor shift preserve shift low”; the hypotheses and conclusion in the code panel fix its exact scope. Cycle 12 helper: XOR with a high-shifted value preserves low bits after right-shifting.

theorem xor_shift_preserve_shift_low (x b pos n : Nat) (h : pos ≥ 1 + n) :
    ((x ^^^ (b <<< pos)) >>> 1) &&& ((1 <<< n) - 1) =
    (x >>> 1) &&& ((1 <<< n) - 1) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “swap oracle diff lt two pow”; the hypotheses and conclusion in the code panel fix its exact scope. SWAP proof-DAG helper: the XOR difference between the two n-bit blocks is itself an n-bit value.

theorem swapOracleDiff_lt_two_pow (p : OneTermRobinParameters) (j : Nat) :
    let n := p.n
    let blockMask := (1 <<< n) - 1
    let block1 := (j >>> 1) &&& blockMask
    let block2 := (j >>> (1 + n)) &&& blockMask
    block1 ^^^ block2 < 2 ^ n := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “swap oracle diff shift right eq zero”; the hypotheses and conclusion in the code panel fix its exact scope. SWAP proof-DAG helper: right-shifting the n-bit block difference by n removes it.

theorem swapOracleDiff_shiftRight_eq_zero (p : OneTermRobinParameters) (j : Nat) :
    let n := p.n
    let blockMask := (1 <<< n) - 1
    let block1 := (j >>> 1) &&& blockMask
    let block2 := (j >>> (1 + n)) &&& blockMask
    let diff := block1 ^^^ block2
    diff >>> n = 0 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “swap oracle diff shift left mask eq zero”; the hypotheses and conclusion in the code panel fix its exact scope. SWAP proof-DAG helper: shifting the block difference into the high block leaves zero in the low n-bit mask.

theorem swapOracleDiff_shiftLeft_mask_eq_zero (p : OneTermRobinParameters) (j : Nat) :
    let n := p.n
    let blockMask := (1 <<< n) - 1
    let block1 := (j >>> 1) &&& blockMask
    let block2 := (j >>> (1 + n)) &&& blockMask
    let diff := block1 ^^^ block2
    (diff <<< n) &&& blockMask = 0 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “shift left lt two pow of lt”; the hypotheses and conclusion in the code panel fix its exact scope. Shifting a bounded value into a register block keeps it inside the total basis width.

theorem shiftLeft_lt_two_pow_of_lt
    {x width shift total : Nat}
    (hx : x < 2 ^ width) (hblock : width + shift ≤ total) :
    x <<< shift < 2 ^ total := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “swap oracle image lt qubit dim”; the hypotheses and conclusion in the code panel fix its exact scope. SWAP proof-DAG range block: the image of the register-block SWAP stays inside the same full finite basis.

theorem swapOracleImage_lt_qubitDim
    (p : OneTermRobinParameters) {j : Nat}
    (hj : j < qubitDim (oneTermRobinTotalQubits p)) :
    swapOracleImage p j < qubitDim (oneTermRobinTotalQubits p) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “swap oracle image block 1 eq block 2”; the hypotheses and conclusion in the code panel fix its exact scope. SWAP proof-DAG block: after 'swapOracleImage', the low n-bit register equals the old high n-bit register.

theorem swapOracleImage_block1_eq_block2 (p : OneTermRobinParameters) (j : Nat) :
    let n := p.n
    let blockMask := (1 <<< n) - 1
    ((swapOracleImage p j) >>> 1) &&& blockMask =
      (j >>> (1 + n)) &&& blockMask := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “swap oracle image block 2 eq block 1”; the hypotheses and conclusion in the code panel fix its exact scope. SWAP proof-DAG block: after 'swapOracleImage', the high n-bit register equals the old low n-bit register.

theorem swapOracleImage_block2_eq_block1 (p : OneTermRobinParameters) (j : Nat) :
    let n := p.n
    let blockMask := (1 <<< n) - 1
    ((swapOracleImage p j) >>> (1 + n)) &&& blockMask =
      (j >>> 1) &&& blockMask := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “swap oracle diff preserved”; the hypotheses and conclusion in the code panel fix its exact scope. SWAP proof-DAG block: the XOR difference between the two exchanged registers is preserved by one SWAP application.

theorem swapOracleDiff_preserved (p : OneTermRobinParameters) (j : Nat) :
    swapOracleDiff p (swapOracleImage p j) = swapOracleDiff p j := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “xor two shifted masks cancel”; the hypotheses and conclusion in the code panel fix its exact scope. XORing the same two shifted masks twice cancels them bitwise.

theorem xor_two_shifted_masks_cancel (j diff n : Nat) :
    (j ^^^ (diff <<< 1) ^^^ (diff <<< (1 + n))) ^^^
        (diff <<< 1) ^^^ (diff <<< (1 + n)) = j := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “swap oracle image self inverse”; the hypotheses and conclusion in the code panel fix its exact scope. SWAP proof-DAG block: the image function is self-inverse.

theorem swapOracleImage_self_inverse (p : OneTermRobinParameters) (j : Nat) :
    swapOracleImage p (swapOracleImage p j) = j := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “swap oracle image injective”; the hypotheses and conclusion in the code panel fix its exact scope. SWAP proof-DAG block: injectivity of the image function, derived from the self-inverse arithmetic block without opening the bit-slice proof again.

theorem swapOracleImage_injective (p : OneTermRobinParameters) {j₁ j₂ : Nat}
    (h : swapOracleImage p j₁ = swapOracleImage p j₂) :
    j₁ = j₂ := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “swap oracle image bijective”; the hypotheses and conclusion in the code panel fix its exact scope. SWAP proof-DAG block: bijectivity of 'swapOracleImage' on the finite full Hilbert-space basis.

theorem swapOracleImage_bijective (p : OneTermRobinParameters) :
    (∀ (a b : Fin (qubitDim (oneTermRobinTotalQubits p))),
        (⟨swapOracleImage p a.val, swapOracleImage_lt_qubitDim p a.2⟩ :
          Fin (qubitDim (oneTermRobinTotalQubits p))) =
        ⟨swapOracleImage p b.val, swapOracleImage_lt_qubitDim p b.2⟩ →
        a = b) ∧
    ∀ (y : Fin (qubitDim (oneTermRobinTotalQubits p))),
      ∃ (x : Fin (qubitDim (oneTermRobinTotalQubits p))),
        (⟨swapOracleImage p x.val, swapOracleImage_lt_qubitDim p x.2⟩ :
          Fin (qubitDim (oneTermRobinTotalQubits p))) = y := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “swap oracle matrix col has one”; the hypotheses and conclusion in the code panel fix its exact scope. For each SWAP matrix column, the row indexed by 'swapOracleImage' contains the unique '1' entry.

theorem swapOracleMatrix_col_has_one (p : OneTermRobinParameters)
    (j : Fin (qubitDim (oneTermRobinTotalQubits p))) :
    swapOracleMatrix p
      (⟨swapOracleImage p j.val, swapOracleImage_lt_qubitDim p j.2⟩ :
        Fin (qubitDim (oneTermRobinTotalQubits p))) j = Coeff.rat 1 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “swap oracle matrix col unique”; the hypotheses and conclusion in the code panel fix its exact scope. For each SWAP matrix column, any '1' entry must occur at the row indexed by 'swapOracleImage'.

theorem swapOracleMatrix_col_unique (p : OneTermRobinParameters)
    (i j : Fin (qubitDim (oneTermRobinTotalQubits p)))
    (h : swapOracleMatrix p i j = Coeff.rat 1) :
    i = ⟨swapOracleImage p j.val, swapOracleImage_lt_qubitDim p j.2⟩ := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “swap oracle matrix row has one”; the hypotheses and conclusion in the code panel fix its exact scope. Every SWAP matrix row has a '1' entry, by finite surjectivity.

theorem swapOracleMatrix_row_has_one (p : OneTermRobinParameters)
    (i : Fin (qubitDim (oneTermRobinTotalQubits p))) :
    ∃ (j : Fin (qubitDim (oneTermRobinTotalQubits p))),
      swapOracleMatrix p i j = Coeff.rat 1 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “swap oracle matrix row unique”; the hypotheses and conclusion in the code panel fix its exact scope. Every SWAP matrix row has a unique '1' entry, by finite injectivity.

theorem swapOracleMatrix_row_unique (p : OneTermRobinParameters)
    (i : Fin (qubitDim (oneTermRobinTotalQubits p)))
    (j₁ j₂ : Fin (qubitDim (oneTermRobinTotalQubits p)))
    (h₁ : swapOracleMatrix p i j₁ = Coeff.rat 1)
    (h₂ : swapOracleMatrix p i j₂ = Coeff.rat 1) :
    j₁ = j₂ := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “swap oracle matrix is permutation”; the hypotheses and conclusion in the code panel fix its exact scope. SWAP matrix is a finite permutation matrix: every row and column has exactly one entry equal to '1'.

theorem swapOracleMatrix_is_permutation (p : OneTermRobinParameters) :
    (∀ (i : Fin (qubitDim (oneTermRobinTotalQubits p))),
      ∃ (j : Fin (qubitDim (oneTermRobinTotalQubits p))),
        swapOracleMatrix p i j = Coeff.rat 1 ∧
        ∀ (j' : Fin (qubitDim (oneTermRobinTotalQubits p))),
          swapOracleMatrix p i j' = Coeff.rat 1 → j' = j) ∧
    (∀ (j : Fin (qubitDim (oneTermRobinTotalQubits p))),
      ∃ (i : Fin (qubitDim (oneTermRobinTotalQubits p))),
        swapOracleMatrix p i j = Coeff.rat 1 ∧
        ∀ (i' : Fin (qubitDim (oneTermRobinTotalQubits p))),
          swapOracleMatrix p i' j = Coeff.rat 1 → i' = i) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper post swap row value eq address”; the hypotheses and conclusion in the code panel fix its exact scope. After the active Lemma 1 paper image and the SWAP gate, the system-row register contains the paper address 'r_si'.

theorem bandedSparseAccessPaperPostSwap_rowValue_eq_address
    (p : OneTermRobinParameters) (j : Nat)
    (haddr : bandedSparseAccessPaperAddress p j < (1 <<< p.n)) :
    (bandedSparseAccessPaperRegisters p
      (swapOracleImage p (bandedSparseAccessPaperImage p j))).rowValue =
      bandedSparseAccessPaperAddress p j := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper post swap od register value eq row value”; the hypotheses and conclusion in the code panel fix its exact scope. After the active Lemma 1 paper image and the SWAP gate, the O_D register contains the original row value.

theorem bandedSparseAccessPaperPostSwap_odRegisterValue_eq_rowValue
    (p : OneTermRobinParameters) (j : Nat) :
    (bandedSparseAccessPaperRegisters p
      (swapOracleImage p (bandedSparseAccessPaperImage p j))).odRegisterValue =
      (bandedSparseAccessPaperRegisters p j).rowValue := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper post swap image lt qubit dim of address lt”; the hypotheses and conclusion in the code panel fix its exact scope. After the active paper image and SWAP, the post-SWAP column is still a finite basis index whenever the source column is finite and the written paper address is n-bit.

theorem bandedSparseAccessPaperPostSwapImage_lt_qubitDim_of_address_lt
    (p : OneTermRobinParameters)
    (source : Fin (qubitDim (oneTermRobinTotalQubits p)))
    (haddr : bandedSparseAccessPaperAddress p source.val < (1 <<< p.n)) :
    swapOracleImage p (bandedSparseAccessPaperImage p source.val) <
      qubitDim (oneTermRobinTotalQubits p) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “banded sparse access paper splice od register”. Replace the 'O_D^BS' n-bit register of a compound index while preserving the low ancilla/system block and all high-tail bits.

def bandedSparseAccessPaperSpliceODRegister
    (p : OneTermRobinParameters) (j odValue : Nat) : Nat :=
  let lowWidth := 1 + p.n
  let highWidth := 1 + 2 * p.n
  let lowBase := 2 ^ lowWidth
  let highBase := 2 ^ highWidth
  j % lowBase + odValue * lowBase + (j / highBase) * highBase

/-- The paper image is the O_D-register splice with the computed paper address. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper image eq splice”; the hypotheses and conclusion in the code panel fix its exact scope. The paper image is the O_D-register splice with the computed paper address.

theorem bandedSparseAccessPaperImage_eq_splice
    (p : OneTermRobinParameters) (j : Nat) :
    bandedSparseAccessPaperImage p j =
      bandedSparseAccessPaperSpliceODRegister p j
        (bandedSparseAccessPaperAddress p j) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper splice od register low block lt high base of od value lt”; the hypotheses and conclusion in the code panel fix its exact scope. The spliced low-and-O_D block fits below the high-tail boundary for n-bit O_D values.

theorem bandedSparseAccessPaperSpliceODRegister_lowBlock_lt_highBase_of_odValue_lt
    (p : OneTermRobinParameters) (j odValue : Nat)
    (hod : odValue < (1 <<< p.n)) :
    let lowWidth := 1 + p.n
    let highWidth := 1 + 2 * p.n
    let lowBase := 2 ^ lowWidth
    let highBase := 2 ^ highWidth
    let lowPrefix := j % lowBase
    lowPrefix + odValue * lowBase < highBase := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper splice od register mod low base”; the hypotheses and conclusion in the code panel fix its exact scope. Splicing an O_D value preserves the low ancilla-and-row block.

theorem bandedSparseAccessPaperSpliceODRegister_mod_lowBase
    (p : OneTermRobinParameters) (j odValue : Nat) :
    bandedSparseAccessPaperSpliceODRegister p j odValue % 2 ^ (1 + p.n) =
      j % 2 ^ (1 + p.n) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper splice od register div low base mod eq”; the hypotheses and conclusion in the code panel fix its exact scope. Splicing an n-bit O_D value exposes that value when the O_D register is extracted.

theorem bandedSparseAccessPaperSpliceODRegister_div_lowBase_mod_eq
    (p : OneTermRobinParameters) (j odValue : Nat)
    (hod : odValue < (1 <<< p.n)) :
    bandedSparseAccessPaperSpliceODRegister p j odValue / 2 ^ (1 + p.n) %
        2 ^ p.n =
      odValue := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper splice od register row value eq”; the hypotheses and conclusion in the code panel fix its exact scope. Splicing preserves the row field.

theorem bandedSparseAccessPaperSpliceODRegister_rowValue_eq
    (p : OneTermRobinParameters) (j odValue : Nat) :
    (bandedSparseAccessPaperRegisters p
      (bandedSparseAccessPaperSpliceODRegister p j odValue)).rowValue =
      (bandedSparseAccessPaperRegisters p j).rowValue := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper splice od register od register value eq”; the hypotheses and conclusion in the code panel fix its exact scope. Splicing an n-bit value into the O_D block makes that value the extracted O_D register.

theorem bandedSparseAccessPaperSpliceODRegister_odRegisterValue_eq
    (p : OneTermRobinParameters) (j odValue : Nat)
    (hod : odValue < (1 <<< p.n)) :
    (bandedSparseAccessPaperRegisters p
      (bandedSparseAccessPaperSpliceODRegister p j odValue)).odRegisterValue =
      odValue := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper splice od register div high base eq of od value lt”; the hypotheses and conclusion in the code panel fix its exact scope. Splicing an n-bit O_D value preserves all bits above the O_D register.

theorem bandedSparseAccessPaperSpliceODRegister_div_highBase_eq_of_odValue_lt
    (p : OneTermRobinParameters) (j odValue : Nat)
    (hod : odValue < (1 <<< p.n)) :
    bandedSparseAccessPaperSpliceODRegister p j odValue / 2 ^ (1 + 2 * p.n) =
      j / 2 ^ (1 + 2 * p.n) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper splice od register lt qubit dim of od value lt”; the hypotheses and conclusion in the code panel fix its exact scope. Splicing an n-bit O_D value into a finite compound basis index preserves the full finite-basis range.

theorem bandedSparseAccessPaperSpliceODRegister_lt_qubitDim_of_odValue_lt
    (p : OneTermRobinParameters) (j odValue : Nat)
    (hj : j < qubitDim (oneTermRobinTotalQubits p))
    (hod : odValue < (1 <<< p.n)) :
    bandedSparseAccessPaperSpliceODRegister p j odValue <
      qubitDim (oneTermRobinTotalQubits p) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper splice od register splice of od value lt”; the hypotheses and conclusion in the code panel fix its exact scope. Replacing the O_D block twice is the same as keeping the second replacement.

theorem bandedSparseAccessPaperSpliceODRegister_splice_of_odValue_lt
    (p : OneTermRobinParameters) (j odValue newODValue : Nat)
    (hod : odValue < (1 <<< p.n)) :
    bandedSparseAccessPaperSpliceODRegister p
        (bandedSparseAccessPaperSpliceODRegister p j odValue) newODValue =
      bandedSparseAccessPaperSpliceODRegister p j newODValue := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper splice od register self”; the hypotheses and conclusion in the code panel fix its exact scope. Reconstructing an index from its low, O_D, and high blocks gives the same index.

theorem bandedSparseAccessPaperSpliceODRegister_self
    (p : OneTermRobinParameters) (j : Nat) :
    bandedSparseAccessPaperSpliceODRegister p j
      (bandedSparseAccessPaperRegisters p j).odRegisterValue = j := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “banded sparse access paper clean od value”. Clean 'O_D^BS' register value whose padded-low part is zero and sparse part is 'sparseValue'.

def bandedSparseAccessPaperCleanODValue
    (p : OneTermRobinParameters) (sparseValue : Nat) : Nat :=
  sparseValue <<< (p.n - clog2 p.kappa)

/-- The clean O_D value has zeroes in the padded low slice. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper clean od value padded zero eq zero”; the hypotheses and conclusion in the code panel fix its exact scope. The clean O_D value has zeroes in the padded low slice.

theorem bandedSparseAccessPaperCleanODValue_paddedZero_eq_zero
    (p : OneTermRobinParameters) (sparseValue : Nat) :
    bandedSparseAccessPaperCleanODValue p sparseValue &&&
        ((1 <<< (p.n - clog2 p.kappa)) - 1) = 0 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper clean od value lt two pow of sparse lt”; the hypotheses and conclusion in the code panel fix its exact scope. A clean sparse value fits in the n-bit O_D register when the sparse width fits in n.

theorem bandedSparseAccessPaperCleanODValue_lt_two_pow_of_sparse_lt
    (p : OneTermRobinParameters) {sparseValue : Nat}
    (hwidth : clog2 p.kappa ≤ p.n)
    (hsparse : sparseValue < 2 ^ clog2 p.kappa) :
    bandedSparseAccessPaperCleanODValue p sparseValue < (1 <<< p.n) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper clean od value sparse index eq”; the hypotheses and conclusion in the code panel fix its exact scope. Extracting the sparse slice from a clean O_D value recovers the sparse value.

theorem bandedSparseAccessPaperCleanODValue_sparseIndex_eq
    (p : OneTermRobinParameters) {sparseValue : Nat}
    (hsparse : sparseValue < 2 ^ clog2 p.kappa) :
    ((bandedSparseAccessPaperCleanODValue p sparseValue >>>
          (p.n - clog2 p.kappa)) &&& ((1 <<< clog2 p.kappa) - 1)) =
      sparseValue := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper clean input od register value eq clean od value”; the hypotheses and conclusion in the code panel fix its exact scope. On a clean Lemma 1 source column, the extracted O_D register is exactly the canonical clean sparse-register value for its sparse slot.

theorem bandedSparseAccessPaperCleanInput_odRegisterValue_eq_cleanODValue
    (p : OneTermRobinParameters) (j : Nat)
    (hwidth : clog2 p.kappa ≤ p.n)
    (hclean : bandedSparseAccessPaperCleanInput p j = true) :
    (bandedSparseAccessPaperRegisters p j).odRegisterValue =
      bandedSparseAccessPaperCleanODValue p
        (bandedSparseAccessPaperRegisters p j).sparseIndexValue := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper image injective on global slot source”; the hypotheses and conclusion in the code panel fix its exact scope. The corrected active 'O_D^BS' paper image is injective on the faithful global-slot clean source domain.

theorem bandedSparseAccessPaperImage_injective_on_globalSlotSource
    (p : OneTermRobinParameters)
    (j₁ j₂ : Fin (qubitDim (oneTermRobinTotalQubits p)))
    (hn : 3 ≤ p.n) (hkappa : p.kappa = 7) (hκbits : clog2 p.kappa = 3)
    (hsource₁ : bandedSparseAccessPaperGlobalSlotSource p j₁.val = true)
    (hsource₂ : bandedSparseAccessPaperGlobalSlotSource p j₂.val = true)
    (himage :
      bandedSparseAccessPaperImage p j₁.val =
        bandedSparseAccessPaperImage p j₂.val) :
    j₁ = j₂ := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper post swap reverse sparse lt two pow”; the hypotheses and conclusion in the code panel fix its exact scope. The reverse sparse index used by the post-SWAP cleanup candidate fits in the three-bit sparse register for the one-term Robin parameter family.

theorem bandedSparseAccessPaperPostSwapReverseSparse_lt_two_pow
    (p : OneTermRobinParameters) (source : Nat)
    (hn : 3 ≤ p.n) (hκbits : clog2 p.kappa = 3) :
    oneTermRobinGlobalSparseInverseSlot
        (bandedSparseAccessPaperRegisters p source).sparseIndexValue <
      2 ^ clog2 p.kappa := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper post swap clean od value lt two pow”; the hypotheses and conclusion in the code panel fix its exact scope. The clean O_D register value spliced into the post-SWAP preimage candidate is n-bit for the one-term Robin parameter family.

theorem bandedSparseAccessPaperPostSwapCleanODValue_lt_two_pow
    (p : OneTermRobinParameters) (source : Nat)
    (hn : 3 ≤ p.n) (hκbits : clog2 p.kappa = 3) :
    bandedSparseAccessPaperCleanODValue p
        (oneTermRobinGlobalSparseInverseSlot
          (bandedSparseAccessPaperRegisters p source).sparseIndexValue) <
      (1 <<< p.n) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “banded sparse access paper post swap preimage candidate”. Candidate clean preimage for the column reached by 'O_D^BS', SWAP, and then '(O_D^BS)^dagger'.

def bandedSparseAccessPaperPostSwapPreimageCandidate
    (p : OneTermRobinParameters) (source : Nat) : Nat :=
  let regs := bandedSparseAccessPaperRegisters p source
  let post := swapOracleImage p (bandedSparseAccessPaperImage p source)
  let reverseSparse := oneTermRobinGlobalSparseInverseSlot regs.sparseIndexValue
  bandedSparseAccessPaperSpliceODRegister p post
    (bandedSparseAccessPaperCleanODValue p reverseSparse)

/--
Executable audit for the post-SWAP preimage candidate.

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “banded sparse access paper post swap preimage candidate checks”. Executable audit for the post-SWAP preimage candidate.

def bandedSparseAccessPaperPostSwapPreimageCandidateChecks
    (p : OneTermRobinParameters) (source : Nat) : Bool :=
  let post := swapOracleImage p (bandedSparseAccessPaperImage p source)
  let pre := bandedSparseAccessPaperPostSwapPreimageCandidate p source
  (bandedSparseAccessPaperImage p pre == post) &&
    bandedSparseAccessPaperCleanInput p pre &&
    bandedSparseAccessPaperAddressInRange p pre

/--
The post-SWAP preimage candidate passes the executable image, clean-domain, and
address-range checks for clean one-term Robin source columns.

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper post swap preimage candidate checks of clean source”; the hypotheses and conclusion in the code panel fix its exact scope. The post-SWAP preimage candidate passes the executable image, clean-domain, and address-range checks for clean one-term Robin source columns.

theorem bandedSparseAccessPaperPostSwapPreimageCandidateChecks_of_cleanSource
    (p : OneTermRobinParameters) (source : Nat)
    (hn : 3 ≤ p.n) (hkappa : p.kappa = 7) (hκbits : clog2 p.kappa = 3)
    (hsource : source < qubitDim (oneTermRobinTotalQubits p))
    (hclean : bandedSparseAccessPaperCleanInput p source = true) :
    bandedSparseAccessPaperPostSwapPreimageCandidateChecks p source = true := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper post swap preimage candidate lt qubit dim of clean source”; the hypotheses and conclusion in the code panel fix its exact scope. The clean post-SWAP preimage candidate is a finite basis index for finite clean one-term Robin source columns.

theorem bandedSparseAccessPaperPostSwapPreimageCandidate_lt_qubitDim_of_cleanSource
    (p : OneTermRobinParameters)
    (source : Fin (qubitDim (oneTermRobinTotalQubits p)))
    (hn : 3 ≤ p.n) (hkappa : p.kappa = 7) (hκbits : clog2 p.kappa = 3)
    (hclean : bandedSparseAccessPaperCleanInput p source.val = true) :
    bandedSparseAccessPaperPostSwapPreimageCandidate p source.val <
      qubitDim (oneTermRobinTotalQubits p) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access post swap cleanup of clean source candidate”; the hypotheses and conclusion in the code panel fix its exact scope. Instantiate the conditional post-SWAP cleanup witness with the clean-source preimage candidate.

theorem bandedSparseAccessPostSwapCleanup_of_cleanSourceCandidate
    (p : OneTermRobinParameters)
    (source : Fin (qubitDim (oneTermRobinTotalQubits p)))
    (hn : 3 <= p.n) (hkappa : p.kappa = 7) (hκbits : clog2 p.kappa = 3)
    (hclean : bandedSparseAccessPaperCleanInput p source.val = true)
    (hpostRange :
      swapOracleImage p (bandedSparseAccessPaperImage p source.val) <
        qubitDim (oneTermRobinTotalQubits p))
    (hpreRange :
      bandedSparseAccessPaperPostSwapPreimageCandidate p source.val <
        qubitDim (oneTermRobinTotalQubits p)) :

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access post swap cleanup of clean source candidate no range”; the hypotheses and conclusion in the code panel fix its exact scope. Instantiate the clean-source post-SWAP cleanup witness without caller-supplied finite-range premises.

theorem bandedSparseAccessPostSwapCleanup_of_cleanSourceCandidate_noRange
    (p : OneTermRobinParameters)
    (source : Fin (qubitDim (oneTermRobinTotalQubits p)))
    (hn : 3 <= p.n) (hkappa : p.kappa = 7) (hκbits : clog2 p.kappa = 3)
    (hclean : bandedSparseAccessPaperCleanInput p source.val = true) :
    BandedSparseAccessPostSwapCleanup p source
      ⟨swapOracleImage p (bandedSparseAccessPaperImage p source.val),
        by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access post swap cleanup of valid clean source candidate no range”; the hypotheses and conclusion in the code panel fix its exact scope. Feed the row-dependent valid-clean-source predicate into the existing post-SWAP cleanup candidate wrapper.

theorem bandedSparseAccessPostSwapCleanup_of_validCleanSourceCandidate_noRange
    (p : OneTermRobinParameters)
    (source : Fin (qubitDim (oneTermRobinTotalQubits p)))
    (hn : 3 <= p.n) (hkappa : p.kappa = 7) (hκbits : clog2 p.kappa = 3)
    (hvalid : bandedSparseAccessPaperValidCleanSource p source.val = true) :
    BandedSparseAccessPostSwapCleanup p source
      ⟨swapOracleImage p (bandedSparseAccessPaperImage p source.val),
        by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access post swap cleanup of global slot source candidate no range”; the hypotheses and conclusion in the code panel fix its exact scope. Feed the faithful global-slot source predicate into the existing post-SWAP cleanup candidate wrapper.

theorem bandedSparseAccessPostSwapCleanup_of_globalSlotSourceCandidate_noRange
    (p : OneTermRobinParameters)
    (source : Fin (qubitDim (oneTermRobinTotalQubits p)))
    (hn : 3 <= p.n) (hkappa : p.kappa = 7) (hκbits : clog2 p.kappa = 3)
    (hsource : bandedSparseAccessPaperGlobalSlotSource p source.val = true) :
    BandedSparseAccessPostSwapCleanup p source
      ⟨swapOracleImage p (bandedSparseAccessPaperImage p source.val),
        by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper post swap preimage candidate checks of global slot source”; the hypotheses and conclusion in the code panel fix its exact scope. The post-SWAP preimage candidate audit is available on the active global-slot source domain.

theorem bandedSparseAccessPaperPostSwapPreimageCandidateChecks_of_globalSlotSource
    (p : OneTermRobinParameters) (source : Nat)
    (hn : 3 <= p.n) (hkappa : p.kappa = 7) (hκbits : clog2 p.kappa = 3)
    (hsourceFinite : source < qubitDim (oneTermRobinTotalQubits p))
    (hsource : bandedSparseAccessPaperGlobalSlotSource p source = true) :
    bandedSparseAccessPaperPostSwapPreimageCandidateChecks p source = true := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper post swap preimage candidate lt qubit dim of global slot source”; the hypotheses and conclusion in the code panel fix its exact scope. The global-source post-SWAP preimage candidate is a finite basis index.

theorem bandedSparseAccessPaperPostSwapPreimageCandidate_lt_qubitDim_of_globalSlotSource
    (p : OneTermRobinParameters)
    (source : Fin (qubitDim (oneTermRobinTotalQubits p)))
    (hn : 3 <= p.n) (hkappa : p.kappa = 7) (hκbits : clog2 p.kappa = 3)
    (hsource : bandedSparseAccessPaperGlobalSlotSource p source.val = true) :
    bandedSparseAccessPaperPostSwapPreimageCandidate p source.val <
      qubitDim (oneTermRobinTotalQubits p) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper post swap preimage candidate sparse index eq”; the hypotheses and conclusion in the code panel fix its exact scope. The post-SWAP preimage candidate has the reverse sparse slot in its extracted clean O_D register.

theorem bandedSparseAccessPaperPostSwapPreimageCandidate_sparseIndex_eq
    (p : OneTermRobinParameters) (source : Nat)
    (hn : 3 <= p.n) (hκbits : clog2 p.kappa = 3) :
    (bandedSparseAccessPaperRegisters p
      (bandedSparseAccessPaperPostSwapPreimageCandidate p source)).sparseIndexValue =
      oneTermRobinGlobalSparseInverseSlot
        (bandedSparseAccessPaperRegisters p source).sparseIndexValue := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper post swap preimage candidate global slot source of global slot source”; the hypotheses and conclusion in the code panel fix its exact scope. The post-SWAP preimage candidate is itself an active global-slot source.

theorem bandedSparseAccessPaperPostSwapPreimageCandidate_globalSlotSource_of_globalSlotSource
    (p : OneTermRobinParameters)
    (source : Fin (qubitDim (oneTermRobinTotalQubits p)))
    (hn : 3 <= p.n) (hkappa : p.kappa = 7) (hκbits : clog2 p.kappa = 3)
    (hsource : bandedSparseAccessPaperGlobalSlotSource p source.val = true) :
    bandedSparseAccessPaperGlobalSlotSource p
      (bandedSparseAccessPaperPostSwapPreimageCandidate p source.val) = true := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access paper post swap preimage candidate unique on global slot source”; the hypotheses and conclusion in the code panel fix its exact scope. Uniqueness of the active global-slot clean preimage for the post-SWAP target.

theorem bandedSparseAccessPaperPostSwapPreimageCandidate_unique_on_globalSlotSource
    (p : OneTermRobinParameters)
    (source pre : Fin (qubitDim (oneTermRobinTotalQubits p)))
    (hn : 3 <= p.n) (hkappa : p.kappa = 7) (hκbits : clog2 p.kappa = 3)
    (hsource : bandedSparseAccessPaperGlobalSlotSource p source.val = true)
    (hpreSource : bandedSparseAccessPaperGlobalSlotSource p pre.val = true)
    (hpreImage :
      bandedSparseAccessPaperImage p pre.val =
        swapOracleImage p (bandedSparseAccessPaperImage p source.val)) :
    pre.val =
      bandedSparseAccessPaperPostSwapPreimageCandidate p source.val := by

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “banded sparse access global slot inverse on range contract”. A proposition-valued field is a requirement until a constructor supplies it. Proof-obligation interface for the active global-slot inverse-on-range route.

structure BandedSparseAccessGlobalSlotInverseOnRangeContract where
  sourceAnchor : String
  sourcePredicate : String
  imageFunction : String
  preimageCandidate : String
  sourceIndex : Nat
  sourceRegisters : BandedSparseAccessPaperRegisters
  sourceInGlobalDomain : Bool
  postSwapImageIndex : Nat
  candidatePreimageIndex : Nat
  candidateChecks : Bool

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “banded sparse access global slot inverse on range contract”. Default global-source inverse-on-range contract for one 'O_D^BS' source column.

def bandedSparseAccessGlobalSlotInverseOnRangeContract
    (p : OneTermRobinParameters) (source : Nat) :
    BandedSparseAccessGlobalSlotInverseOnRangeContract where
  sourceAnchor := "Guseynov-Huang-Liu 2025, Lemma 1 and Fig. 1-term Robin, arXiv:2506.20478"
  sourcePredicate := "bandedSparseAccessPaperGlobalSlotSource"
  imageFunction := "bandedSparseAccessPaperImage"
  preimageCandidate := "bandedSparseAccessPaperPostSwapPreimageCandidate"
  sourceIndex := source
  sourceRegisters := bandedSparseAccessPaperRegisters p source
  sourceInGlobalDomain := bandedSparseAccessPaperGlobalSlotSource p source
  postSwapImageIndex := swapOracleImage p (bandedSparseAccessPaperImage p source)

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access global slot inverse on range contract flags false”; the hypotheses and conclusion in the code panel fix its exact scope. The global-source inverse-on-range contract is obligation-only in Phase 1.

theorem bandedSparseAccessGlobalSlotInverseOnRangeContract_flags_false
    (p : OneTermRobinParameters) (source : Nat) :
    (bandedSparseAccessGlobalSlotInverseOnRangeContract p source).inverseOnRange.proved =
        false ∧
      (bandedSparseAccessGlobalSlotInverseOnRangeContract p source).uniquePreimage.proved =
        false ∧
      (bandedSparseAccessGlobalSlotInverseOnRangeContract p source).imageInjectiveOnGlobalSource.proved =
        false ∧
      (bandedSparseAccessGlobalSlotInverseOnRangeContract p source).daggerCleanup.proved =
        false ∧
      (bandedSparseAccessGlobalSlotInverseOnRangeContract p source).unitaryExtension.proved =

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access global slot inverse on range contract of global slot source”; the hypotheses and conclusion in the code panel fix its exact scope. Global-source columns feed the fixed inverse-on-range interface and satisfy the executable candidate audit.

theorem bandedSparseAccessGlobalSlotInverseOnRangeContract_of_globalSlotSource
    (p : OneTermRobinParameters) (source : Nat)
    (hn : 3 <= p.n) (hkappa : p.kappa = 7) (hκbits : clog2 p.kappa = 3)
    (hsourceFinite : source < qubitDim (oneTermRobinTotalQubits p))
    (hsource : bandedSparseAccessPaperGlobalSlotSource p source = true) :
    (bandedSparseAccessGlobalSlotInverseOnRangeContract p source).sourceInGlobalDomain =
        true ∧
      (bandedSparseAccessGlobalSlotInverseOnRangeContract p source).candidateChecks =
        true ∧
      (bandedSparseAccessGlobalSlotInverseOnRangeContract p source).inverseOnRange.proved =
        false ∧

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access global slot inverse on range contract unique preimage bridge”; the hypotheses and conclusion in the code panel fix its exact scope. Record-level bridge from the compiled post-SWAP unique-preimage theorem to the global-slot inverse-on-range contract.

theorem bandedSparseAccessGlobalSlotInverseOnRangeContract_uniquePreimageBridge
    (p : OneTermRobinParameters)
    (source pre : Fin (qubitDim (oneTermRobinTotalQubits p)))
    (hn : 3 <= p.n) (hkappa : p.kappa = 7) (hκbits : clog2 p.kappa = 3)
    (hsource : bandedSparseAccessPaperGlobalSlotSource p source.val = true)
    (hpreSource : bandedSparseAccessPaperGlobalSlotSource p pre.val = true)
    (hpreImage :
      bandedSparseAccessPaperImage p pre.val =
        (bandedSparseAccessGlobalSlotInverseOnRangeContract p
          source.val).postSwapImageIndex) :
    pre.val =

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access global slot inverse on range contract dagger cleanup bridge”; the hypotheses and conclusion in the code panel fix its exact scope. Bridge the global-slot inverse-on-range contract to the concrete post-SWAP dagger cleanup witness.

theorem bandedSparseAccessGlobalSlotInverseOnRangeContract_daggerCleanupBridge
    (p : OneTermRobinParameters)
    (source : Fin (qubitDim (oneTermRobinTotalQubits p)))
    (hn : 3 <= p.n) (hkappa : p.kappa = 7) (hκbits : clog2 p.kappa = 3)
    (hsource : bandedSparseAccessPaperGlobalSlotSource p source.val = true) :
    ∃ (post pre : Fin (qubitDim (oneTermRobinTotalQubits p))),
      BandedSparseAccessPostSwapCleanup p source post pre ∧
        post.val =
          (bandedSparseAccessGlobalSlotInverseOnRangeContract p
            source.val).postSwapImageIndex ∧
        pre.val =

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access global slot inverse on range contract cleanup contract map”; the hypotheses and conclusion in the code panel fix its exact scope. Reviewed cleanup-contract map for the active global-slot 'O_D^BS' route.

theorem bandedSparseAccessGlobalSlotInverseOnRangeContract_cleanupContractMap
    (p : OneTermRobinParameters)
    (source : Fin (qubitDim (oneTermRobinTotalQubits p)))
    (hn : 3 <= p.n) (hkappa : p.kappa = 7) (hκbits : clog2 p.kappa = 3)
    (hsource : bandedSparseAccessPaperGlobalSlotSource p source.val = true) :
    ∃ (post pre : Fin (qubitDim (oneTermRobinTotalQubits p))),
      BandedSparseAccessPostSwapCleanup p source post pre ∧
        post.val =
          (bandedSparseAccessGlobalSlotInverseOnRangeContract p
            source.val).postSwapImageIndex ∧
        pre.val =

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “default banded sparse access paper contract cleanup route bridge”; the hypotheses and conclusion in the code panel fix its exact scope. Default-paper-contract cleanup-route bridge for the active global-slot 'O_D^BS' route.

theorem defaultBandedSparseAccessPaperContract_cleanupRouteBridge
    (p : OneTermRobinParameters)
    (source : Fin (qubitDim (oneTermRobinTotalQubits p)))
    (hn : 3 <= p.n) (hkappa : p.kappa = 7) (hκbits : clog2 p.kappa = 3)
    (hsource : bandedSparseAccessPaperGlobalSlotSource p source.val = true) :
    ∃ (post pre : Fin (qubitDim (oneTermRobinTotalQubits p))),
      BandedSparseAccessPostSwapCleanup p source post pre ∧
        post.val =
          (bandedSparseAccessGlobalSlotInverseOnRangeContract p
            source.val).postSwapImageIndex ∧
        pre.val =

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access global slot inverse on range contract dagger off candidate zero”; the hypotheses and conclusion in the code panel fix its exact scope. Off-candidate dagger entries are zero on the active global-slot source domain.

theorem bandedSparseAccessGlobalSlotInverseOnRangeContract_daggerOffCandidate_zero
    (p : OneTermRobinParameters)
    (source other post : Fin (qubitDim (oneTermRobinTotalQubits p)))
    (hn : 3 <= p.n) (hkappa : p.kappa = 7) (hκbits : clog2 p.kappa = 3)
    (hsource : bandedSparseAccessPaperGlobalSlotSource p source.val = true)
    (hotherSource : bandedSparseAccessPaperGlobalSlotSource p other.val = true)
    (hpost :
      post.val =
        (bandedSparseAccessGlobalSlotInverseOnRangeContract p
          source.val).postSwapImageIndex)
    (hne :

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access global slot inverse on range contract restricted dagger column cleanup”; the hypotheses and conclusion in the code panel fix its exact scope. Restricted active-domain dagger-column cleanup for the global-slot route.

theorem bandedSparseAccessGlobalSlotInverseOnRangeContract_restrictedDaggerColumnCleanup
    (p : OneTermRobinParameters)
    (source : Fin (qubitDim (oneTermRobinTotalQubits p)))
    (hn : 3 <= p.n) (hkappa : p.kappa = 7) (hκbits : clog2 p.kappa = 3)
    (hsource : bandedSparseAccessPaperGlobalSlotSource p source.val = true) :
    ∃ (post pre : Fin (qubitDim (oneTermRobinTotalQubits p))),
      BandedSparseAccessPostSwapCleanup p source post pre ∧
        post.val =
          (bandedSparseAccessGlobalSlotInverseOnRangeContract p
            source.val).postSwapImageIndex ∧
        pre.val =

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access global slot inverse on range contract restricted dagger column indicator”; the hypotheses and conclusion in the code panel fix its exact scope. Indicator form of the restricted active-domain dagger column.

theorem bandedSparseAccessGlobalSlotInverseOnRangeContract_restrictedDaggerColumnIndicator
    (p : OneTermRobinParameters)
    (source : Fin (qubitDim (oneTermRobinTotalQubits p)))
    (hn : 3 <= p.n) (hkappa : p.kappa = 7) (hκbits : clog2 p.kappa = 3)
    (hsource : bandedSparseAccessPaperGlobalSlotSource p source.val = true) :
    ∃ (post pre : Fin (qubitDim (oneTermRobinTotalQubits p))),
      BandedSparseAccessPostSwapCleanup p source post pre ∧
        post.val =
          (bandedSparseAccessGlobalSlotInverseOnRangeContract p
            source.val).postSwapImageIndex ∧
        pre.val =

commit-pinned source · Verso Blueprint panel

This type lists the allowed alternatives for “banded sparse access cleanup scope”; its constructors are the cases that downstream code must handle. Allowed scopes for the next 'O_D^BS' cleanup theorem packet.

inductive BandedSparseAccessCleanupScope where
  | activeGlobalSource
  | fullCleanDomain
  | fullSpace
deriving Repr, DecidableEq

/--
Non-promoting decision for the next `O_D^BS` cleanup theorem domain.

The current compiled matrix-entry theorem is restricted to active global-source
rows.  Full clean-domain cleanup still needs a reversible image rule for every

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “banded sparse access cleanup scope decision”. A proposition-valued field is a requirement until a constructor supplies it. Non-promoting decision for the next 'O_D^BS' cleanup theorem domain.

structure BandedSparseAccessCleanupScopeDecision where
  sourceAnchor : String
  selectedScope : BandedSparseAccessCleanupScope
  selectedPredicate : String
  selectedEvidence : String
  fullCleanDomainSelected : Bool
  fullSpaceSelected : Bool
  semanticCleanupPromotionAllowed : Bool
  paperContractCleanup : ObligationRecord
  fullCleanDomainCleanup : ObligationRecord
  fullSpaceUnitaryExtension : ObligationRecord

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “banded sparse access cleanup scope decision”. Default cleanup-scope decision after the restricted dagger-column indicator.

def bandedSparseAccessCleanupScopeDecision
    (p : OneTermRobinParameters) :
    BandedSparseAccessCleanupScopeDecision where
  sourceAnchor := "Guseynov-Huang-Liu 2025, Lemma 1 and Fig. 1-term Robin, arXiv:2506.20478"
  selectedScope := BandedSparseAccessCleanupScope.activeGlobalSource
  selectedPredicate := "bandedSparseAccessPaperGlobalSlotSource"
  selectedEvidence :=
    "bandedSparseAccessGlobalSlotInverseOnRangeContract_restrictedDaggerColumnIndicator"
  fullCleanDomainSelected := false
  fullSpaceSelected := false
  semanticCleanupPromotionAllowed := false

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access cleanup scope decision active global source”; the hypotheses and conclusion in the code panel fix its exact scope. The cleanup-scope decision selects the active global-source theorem and keeps all broader cleanup/unitarity obligations closed to proof-flag promotion.

theorem bandedSparseAccessCleanupScopeDecision_activeGlobalSource
    (p : OneTermRobinParameters) :
    (bandedSparseAccessCleanupScopeDecision p).selectedScope =
        BandedSparseAccessCleanupScope.activeGlobalSource ∧
      (bandedSparseAccessCleanupScopeDecision p).selectedPredicate =
        "bandedSparseAccessPaperGlobalSlotSource" ∧
      (bandedSparseAccessCleanupScopeDecision p).selectedEvidence =
        "bandedSparseAccessGlobalSlotInverseOnRangeContract_restrictedDaggerColumnIndicator" ∧
      (bandedSparseAccessCleanupScopeDecision p).fullCleanDomainSelected =
        false ∧
      (bandedSparseAccessCleanupScopeDecision p).fullSpaceSelected = false ∧

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access cleanup scope decision prior pde source transcript guard”; the hypotheses and conclusion in the code panel fix its exact scope. The cleanup-scope decision does not accept the prior PDE sparse-access transcript as a full-space unitary-extension proof.

theorem bandedSparseAccessCleanupScopeDecision_priorPDESourceTranscriptGuard
    (p : OneTermRobinParameters) :
    (bandedSparseAccessCleanupScopeDecision p).selectedScope =
        BandedSparseAccessCleanupScope.activeGlobalSource ∧
      (bandedSparseAccessCleanupScopeDecision p).fullSpaceSelected = false ∧
      (bandedSparseAccessCleanupScopeDecision p).fullSpaceUnitaryExtension.proved =
        false ∧
      bandedSparseAccessPriorPDESourceContract.oracleEquation =
        "O_A^BS |0>^(n-l)|s>^l|i>^n = |r_si>^n|i>^n" ∧
      bandedSparseAccessPriorPDESourceContract.resourceClaim.proved = false ∧
      bandedSparseAccessPriorPDESourceContract.robinUnusedBranchImageRule =

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “banded sparse access cleanup scope decision full clean domain image rule blocked”; the hypotheses and conclusion in the code panel fix its exact scope. The cleanup-scope decision keeps the full clean-domain image-rule slot blocked.

theorem bandedSparseAccessCleanupScopeDecision_fullCleanDomainImageRuleBlocked
    (p : OneTermRobinParameters) (j : Nat) :
    (bandedSparseAccessCleanupScopeDecision p).selectedScope =
        BandedSparseAccessCleanupScope.activeGlobalSource ∧
      (bandedSparseAccessCleanupScopeDecision p).fullCleanDomainSelected =
        false ∧
      (bandedSparseAccessCleanupScopeDecision p).semanticCleanupPromotionAllowed =
        false ∧
      (bandedSparseAccessCleanupScopeDecision p).fullCleanDomainCleanup.proved =
        false ∧
      bandedSparseAccessUnusedZeroBranchSourceDecision.lowerProofSearchAllowed =

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “default banded sparse access paper contract cleanup route bridge boundary column n 3”; the hypotheses and conclusion in the code panel fix its exact scope. Concrete boundary-source regression for the default paper-contract cleanup route.

theorem defaultBandedSparseAccessPaperContract_cleanupRouteBridge_boundaryColumn_n3 :
    let p : OneTermRobinParameters :=
      { n := 3, kappa := 7, functionPieces := 1, polynomialDegreeCost := 1 }
    let source : Fin (qubitDim (oneTermRobinTotalQubits p)) :=
      ⟨48, by native_decide⟩
    ∃ (post pre : Fin (qubitDim (oneTermRobinTotalQubits p))),
      BandedSparseAccessPostSwapCleanup p source post pre ∧
        post.val =
          (bandedSparseAccessGlobalSlotInverseOnRangeContract p
            source.val).postSwapImageIndex ∧
        pre.val =

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “robin indicator bit position ge”; the hypotheses and conclusion in the code panel fix its exact scope. Cycle 12: robinIndicatorBitPosition = 1 + 2*p.n, hence >= 1 + p.n.

theorem robinIndicatorBitPosition_ge (p : OneTermRobinParameters) :
    robinIndicatorBitPosition p ≥ 1 + p.n := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “indicator oracle image system val preserved”; the hypotheses and conclusion in the code panel fix its exact scope. Cycle 12: The system register value is preserved by indicatorOracleImage.

theorem indicatorOracleImage_systemVal_preserved (p : OneTermRobinParameters) (j : Nat) :
    ((indicatorOracleImage p j) >>> 1) &&& ((1 <<< p.n) - 1) =
    (j >>> 1) &&& ((1 <<< p.n) - 1) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “indicator oracle image is bulk preserved”; the hypotheses and conclusion in the code panel fix its exact scope. Cycle 12: The isBulk predicate gives the same result for j and indicatorOracleImage p j, because isBulk only depends on the system register value, which is preserved.

theorem indicatorOracleImage_isBulk_preserved (p : OneTermRobinParameters) (j : Nat) :
    (if (2 : Nat) ≤ ((indicatorOracleImage p j) >>> 1) &&& ((1 <<< p.n) - 1) ∧
        ((indicatorOracleImage p j) >>> 1) &&& ((1 <<< p.n) - 1) ≤ gridSize p.n - 3
     then (1 : Nat) else 0) =
    (if (2 : Nat) ≤ (j >>> 1) &&& ((1 <<< p.n) - 1) ∧
        (j >>> 1) &&& ((1 <<< p.n) - 1) ≤ gridSize p.n - 3
     then (1 : Nat) else 0) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “indicator oracle image self inverse”; the hypotheses and conclusion in the code panel fix its exact scope. Cycle 12: General self-inverse property for indicatorOracleImage.

theorem indicatorOracleImage_self_inverse (p : OneTermRobinParameters) (j : Nat) :
    indicatorOracleImage p (indicatorOracleImage p j) = j := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “one term robin gate u indic dagger self inverse bridge”; the hypotheses and conclusion in the code panel fix its exact scope. Source-facing bridge for the explicit 'U_indic^dagger' transcript slot.

theorem oneTermRobinGate_U_indic_dagger_selfInverseBridge
    (p : OneTermRobinParameters) :
    (oneTermRobinGate_U_indic_dagger p).matrix =
        (oneTermRobinGate_U_indic p).matrix ∧
      (∀ j : Nat, indicatorOracleImage p (indicatorOracleImage p j) = j) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “indicator oracle image injective”; the hypotheses and conclusion in the code panel fix its exact scope. Cycle 12: General injectivity for indicatorOracleImage, derived from self-inverse.

theorem indicatorOracleImage_injective (p : OneTermRobinParameters) {j₁ j₂ : Nat}
    (h : indicatorOracleImage p j₁ = indicatorOracleImage p j₂) :
    j₁ = j₂ := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “robin indicator bit position lt total qubits”; the hypotheses and conclusion in the code panel fix its exact scope. Cycle 12: robinIndicatorBitPosition is strictly below oneTermRobinTotalQubits.

theorem robinIndicatorBitPosition_lt_totalQubits (p : OneTermRobinParameters) :
    robinIndicatorBitPosition p < oneTermRobinTotalQubits p := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “indicator oracle image lt”; the hypotheses and conclusion in the code panel fix its exact scope. Cycle 12: indicatorOracleImage preserves the qubitDim bound.

theorem indicatorOracleImage_lt (p : OneTermRobinParameters) {j : Nat}
    (hj : j < qubitDim (oneTermRobinTotalQubits p)) :
    indicatorOracleImage p j < qubitDim (oneTermRobinTotalQubits p) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “indicator oracle image bijective”; the hypotheses and conclusion in the code panel fix its exact scope. Cycle 12: Bijectivity of indicatorOracleImage on the Fin domain.

theorem indicatorOracleImage_bijective (p : OneTermRobinParameters) :
    (∀ (a b : Fin (qubitDim (oneTermRobinTotalQubits p))),
        (⟨indicatorOracleImage p a.val, indicatorOracleImage_lt p a.2⟩ :
          Fin (qubitDim (oneTermRobinTotalQubits p))) =
        ⟨indicatorOracleImage p b.val, indicatorOracleImage_lt p b.2⟩ →
        a = b) ∧
    ∀ (y : Fin (qubitDim (oneTermRobinTotalQubits p))),
      ∃ (x : Fin (qubitDim (oneTermRobinTotalQubits p))),
        (⟨indicatorOracleImage p x.val, indicatorOracleImage_lt p x.2⟩ :
          Fin (qubitDim (oneTermRobinTotalQubits p))) = y := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “indicator oracle matrix col has one”; the hypotheses and conclusion in the code panel fix its exact scope. Cycle 12: For each column j, there is exactly one row i with M[i][j] = 1, namely i = ⟨indicatorOracleImage p j.val, ...⟩.

theorem indicatorOracleMatrix_col_has_one (p : OneTermRobinParameters)
    (j : Fin (qubitDim (oneTermRobinTotalQubits p))) :
    indicatorOracleMatrix p
      (⟨indicatorOracleImage p j.val, indicatorOracleImage_lt p j.2⟩ :
        Fin (qubitDim (oneTermRobinTotalQubits p))) j = Coeff.rat 1 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “indicator oracle matrix col unique”; the hypotheses and conclusion in the code panel fix its exact scope. Cycle 12: For each column j, any row i with M[i][j] = 1 must equal ⟨indicatorOracleImage p j.val, ...⟩, so the 1-entry is unique per column.

theorem indicatorOracleMatrix_col_unique (p : OneTermRobinParameters)
    (i j : Fin (qubitDim (oneTermRobinTotalQubits p)))
    (h : indicatorOracleMatrix p i j = Coeff.rat 1) :
    i = ⟨indicatorOracleImage p j.val, indicatorOracleImage_lt p j.2⟩ := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “indicator oracle matrix row has one”; the hypotheses and conclusion in the code panel fix its exact scope. Cycle 12: For each row i, there exists a column j with M[i][j] = 1, from surjectivity of indicatorOracleImage.

theorem indicatorOracleMatrix_row_has_one (p : OneTermRobinParameters)
    (i : Fin (qubitDim (oneTermRobinTotalQubits p))) :
    ∃ (j : Fin (qubitDim (oneTermRobinTotalQubits p))),
      indicatorOracleMatrix p i j = Coeff.rat 1 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “indicator oracle matrix row unique”; the hypotheses and conclusion in the code panel fix its exact scope. Cycle 12: For each row i, the column j with M[i][j] = 1 is unique, from injectivity of indicatorOracleImage.

theorem indicatorOracleMatrix_row_unique (p : OneTermRobinParameters)
    (i : Fin (qubitDim (oneTermRobinTotalQubits p)))
    (j₁ j₂ : Fin (qubitDim (oneTermRobinTotalQubits p)))
    (h₁ : indicatorOracleMatrix p i j₁ = Coeff.rat 1)
    (h₂ : indicatorOracleMatrix p i j₂ = Coeff.rat 1) :
    j₁ = j₂ := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “indicator oracle matrix is permutation”; the hypotheses and conclusion in the code panel fix its exact scope. Cycle 12: indicatorOracleMatrix is a permutation matrix: each row has exactly one entry equal to 1, and each column has exactly one entry equal to 1.

theorem indicatorOracleMatrix_is_permutation (p : OneTermRobinParameters) :
    (∀ (i : Fin (qubitDim (oneTermRobinTotalQubits p))),
      ∃ (j : Fin (qubitDim (oneTermRobinTotalQubits p))),
        indicatorOracleMatrix p i j = Coeff.rat 1 ∧
        ∀ (j' : Fin (qubitDim (oneTermRobinTotalQubits p))),
          indicatorOracleMatrix p i j' = Coeff.rat 1 → j' = j) ∧
    (∀ (j : Fin (qubitDim (oneTermRobinTotalQubits p))),
      ∃ (i : Fin (qubitDim (oneTermRobinTotalQubits p))),
        indicatorOracleMatrix p i j = Coeff.rat 1 ∧
        ∀ (i' : Fin (qubitDim (oneTermRobinTotalQubits p))),
          indicatorOracleMatrix p i' j = Coeff.rat 1 → i' = i) := by

commit-pinned source · Verso Blueprint panel