QuantumBlockEncoding/RobinMatrix.lean

This definition gives the library's named construction or computation for “stencil row coeff”. Coefficient at column 'colIdx' when the stencil 'entries' is applied at row 'rowIdx'.

def stencilRowCoeff (rowIdx colIdx : Nat) (entries : List StencilEntry) : Coeff :=
  match entries.filterMap (fun e =>
    if (rowIdx : Int) + e.offset = (colIdx : Int) then some e.coeff else none) with
  | [] => Coeff.rat 0
  | [c] => c
  | c :: cs => cs.foldl (fun acc b => acc + b) c

/--
Select the stencil entry list for row `i`:
- rows `i < w.lower` use left boundary rows,
- rows `i > w.upper` use right boundary rows,

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “robin row entries”. Select the stencil entry list for row 'i': - rows 'i < w.lower' use left boundary rows, - rows 'i > w.upper' use right boundary rows, - all others use the bulk stencil.

def robinRowEntries (bulkEntries : List StencilEntry)
    (leftRows rightRows : List (List StencilEntry))
    (w : BulkWindow)
    (i : Nat) :
    List StencilEntry :=
  if _h : i < w.lower then
    if hi : i < leftRows.length then leftRows.get ⟨i, hi⟩ else []
  else if _h2 : i > w.upper then
    let idx := i - w.upper - 1
    if hi : idx < rightRows.length then rightRows.get ⟨idx, hi⟩ else []
  else

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “build robin matrix”. Build the full Robin derivative matrix of size 'gridSize n × gridSize n'.

def buildRobinMatrix (n : Nat)
    (bulkEntries : List StencilEntry)
    (leftRows rightRows : List (List StencilEntry))
    (w : BulkWindow) :
    Matrix (gridSize n) (gridSize n) Coeff :=
  fun row col =>
    stencilRowCoeff row.val col.val
      (robinRowEntries bulkEntries leftRows rightRows w row.val)

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “robin derivative matrix”. The concrete Robin derivative matrix for the fourth-order central second-derivative stencil.

def robinDerivativeMatrix (n : Nat) : Matrix (gridSize n) (gridSize n) Coeff :=
  buildRobinMatrix n centralBulkEntries
    [leftBoundaryRow0, leftBoundaryRow1]
    [rightBoundaryRowNm2, rightBoundaryRowNm1]
    (robinWindow n)

/--
The one-term Robin theorem target $A_k$.

Theorem `1 term robin` block-encodes the row-scaled operator
`A_k ~ f(x) d^m/dx^m`; Eq. `ROBIN clarified` carries entries

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin ak matrix”. The one-term Robin theorem target $A_k$.

def oneTermRobinAkMatrix (n : Nat) : Matrix (gridSize n) (gridSize n) Coeff :=
  fun i j => Coeff.mul (GHL2025.robinFunctionValue n i.val) (robinDerivativeMatrix n i j)

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin ak matrix apply”; its local proof does not by itself complete the broader paper route.

@[simp] theorem oneTermRobinAkMatrix_apply
    (n : Nat) (i j : Fin (gridSize n)) :
    oneTermRobinAkMatrix n i j =
      Coeff.mul (GHL2025.robinFunctionValue n i.val)
        (robinDerivativeMatrix n i j) := rfl

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “matrix row abs sum”. Absolute-row-sum for row 'i' of a 'Coeff'-valued matrix, given a symbol environment 'env'.

def matrixRowAbsSum {rows cols : Nat} (mat : Matrix rows cols Coeff)
    (env : String → Rat) (i : Fin rows) : Rat :=
  (List.finRange cols).foldl (fun acc j =>
    let v := Coeff.evalWith env (mat i j)
    acc + if v < 0 then -v else v) 0

/--
Induced matrix 1-norm: the maximum absolute row sum.  Uses `evalWith env`
to convert symbolic `Coeff` entries to concrete `Rat` values.
-/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “matrix one norm”. Induced matrix 1-norm: the maximum absolute row sum.

def matrixOneNorm {rows cols : Nat} (mat : Matrix rows cols Coeff)
    (env : String → Rat) : Rat :=
  (List.finRange rows).foldl (fun acc i =>
    max acc (matrixRowAbsSum mat env i)) 0

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “robin derivative norm”. Numeric 1-norm of the Robin derivative matrix under a symbol environment.

def robinDerivativeNorm (n : Nat) (env : String → Rat) : Rat :=
  matrixOneNorm (robinDerivativeMatrix n) env

/--
Numeric normalizer α = N_D · N_f · κ for the one-term Robin construction.
`nD` is the derivative-stencil normalization (1-norm of the Robin derivative matrix),
`nF` is the function-oracle normalization, and `k` is the Robin-condition bound.
-/

commit-pinned source · Verso Blueprint panel

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

def oneTermRobinNumericNormalizer (nD nF : Rat) (k : Nat) : Rat :=
  nD * nF * k

/--
Proposition: the numeric normalizer α is at least the induced 1-norm of the
Robin derivative matrix, i.e. α ≥ ∥D_Robin∥₁.
Stated via a `Decidable` check so `native_decide` can close concrete instances.
-/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “robin normalizer bound”. Proposition: the numeric normalizer α is at least the induced 1-norm of the Robin derivative matrix, i.e.

def robinNormalizerBound (n : Nat) (env : String → Rat) (nF : Rat) (k : Nat) : Bool :=
  oneTermRobinNumericNormalizer (robinDerivativeNorm n env) nF k ≥
    robinDerivativeNorm n env

/-- Connecting the numeric normalizer to the symbolic GHL2025 normalizer via a
concrete environment mapping the three symbols to their numeric values. -/

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin numeric normalizer eq eval”; its local proof does not by itself complete the broader paper route. Connecting the numeric normalizer to the symbolic GHL2025 normalizer via a concrete environment mapping the three symbols to their numeric values.

theorem oneTermRobinNumericNormalizer_eq_eval (nD nF : Rat) (k : Nat) :
    oneTermRobinNumericNormalizer nD nF k =
      Coeff.evalWith
        (fun s => if s = "N_D" then nD else if s = "N_f" then nF else (k : Rat))
        GHL2025.oneTermRobinNormalizer := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “robin block encoding spec”. Concrete BlockEncodingSpec wiring the Robin derivative matrix into the one-term Robin block encoding framework.

def robinBlockEncodingSpec (n : Nat) : BlockEncodingSpec Coeff (gridSize n) (gridSize n) where
  matrix := robinDerivativeMatrix n
  normalizer := GHL2025.oneTermRobinNormalizer
  error := Coeff.rat 0
  layout := GHL2025.oneTermRobinLayout (oneTermParameters n)
  circuit := GHL2025.oneTermRobinCircuit
  resource := GHL2025.oneTermRobinResource (oneTermParameters n)

/-- The spec's resource pureAncilla matches 2n. -/

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “robin block encoding spec pure ancilla”; its local proof does not by itself complete the broader paper route. The spec's resource pureAncilla matches 2n.

theorem robinBlockEncodingSpec_pureAncilla (n : Nat) :
    (robinBlockEncodingSpec n).resource.pureAncilla = 2 * n := rfl

/-- Concrete derivative oracle resource for the fourth-order Robin stencil.
Uses half-bandwidth l = leftRadius = 2. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “robin derivative oracle resource”. Concrete derivative oracle resource for the fourth-order Robin stencil.

def robinDerivativeOracleResource (n : Nat) : Resource :=
  GHL2025.derivativeOracleResource n fourthOrderSecondDerivative

/-- The Robin derivative oracle resource equals bandedSparseAccessResource n 2. -/

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “robin derivative oracle resource eq”; its local proof does not by itself complete the broader paper route. The Robin derivative oracle resource equals bandedSparseAccessResource n 2.

@[simp] theorem robinDerivativeOracleResource_eq (n : Nat) :
    robinDerivativeOracleResource n = bandedSparseAccessResource n 2 := rfl

/-- The Robin derivative oracle uses n - 1 pure ancillas (from Lemma 1). -/

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “robin derivative oracle resource pure ancilla”; its local proof does not by itself complete the broader paper route. The Robin derivative oracle uses n - 1 pure ancillas (from Lemma 1).

@[simp] theorem robinDerivativeOracleResource_pureAncilla (n : Nat) :
    (robinDerivativeOracleResource n).pureAncilla = n - 1 := rfl

/-! ## Cycle 4: Named proof-obligation Props and oracle composition -/

/-- PO-6: Block-extraction equation for the Robin derivative block encoding.
Records the structural preconditions that are checkable now (normalizer bound,
ancilla count, zero error) and reserves the full equation
  ⟨0^a| ⊗ I) U (|0^a⟩ ⊗ I) = A / α
as an abstract component pending unitary semantics. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “robin block encoding predicate”. PO-6: Block-extraction equation for the Robin derivative block encoding.

def robinBlockEncodingPredicate (n : Nat) : Prop :=
  robinNormalizerBound n (fun _ => 0) 1 (oneTermParameters n).kappa = true ∧
  (robinBlockEncodingSpec n).resource.pureAncilla = 2 * n ∧
  (robinBlockEncodingSpec n).error = Coeff.rat 0

/-- PO-7: Resource bound holds for the Robin block encoding.
Concrete decidable check: pureAncilla = 2n and gate count ≤ paper's formula. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “robin resource bound holds”. PO-7: Resource bound holds for the Robin block encoding.

def robinResourceBoundHolds (n : Nat) : Prop :=
  (robinBlockEncodingSpec n).resource.pureAncilla = 2 * n ∧
  (robinBlockEncodingSpec n).resource.gates ≤
    (oneTermParameters n).polynomialDegreeCost * n * clog2 n + (oneTermParameters n).kappa * n

/-- PO-9: The concrete resource is consistent with the symbolic expression.
Checks the decidable part: pureAncilla = 2n. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin resource consistent”. PO-9: The concrete resource is consistent with the symbolic expression.

def oneTermRobinResourceConsistent (p : GHL2025.OneTermRobinParameters) : Prop :=
  (GHL2025.oneTermRobinResource p).pureAncilla = 2 * p.n

/-- Bundle of oracle contracts and LCU composition obligation for the one-term Robin
construction. Contains:
- derivative oracle O_D (sparse-access for the banded stencil matrix),
- function oracle O_f (amplitude oracle for the coefficient function),
- LCU composition Prop (PO-15: linear combination of unitaries correctness),
- matrix coherence (the oracle's matrix equals the Robin derivative matrix). -/

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “robin oracle composition”. A proposition-valued field is a requirement until a constructor supplies it. Bundle of oracle contracts and LCU composition obligation for the one-term Robin construction.

structure RobinOracleComposition (n : Nat) where
  derivativeOracle : GHL2025.DerivativeOracleContract n
  functionOracle : GHL2025.FunctionOracleContract n
  /-- Obligation: LCU composition of oracle calls yields the correct linear combination.
  figure:1_term_ROBIN, main.tex:1131-1136 --/
  lcuCorrect : GHL2025.ObligationRecord
  matrixCoherence : derivativeOracle.matrix = robinDerivativeMatrix n

/-- PO-13/14/15: Concrete oracle composition for the Robin derivative block encoding.
Instantiates the derivative oracle with the fourth-order stencil, the function oracle
with one piece, and records the LCU composition Prop as an abstract claim. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “robin oracle composition”. PO-13/14/15: Concrete oracle composition for the Robin derivative block encoding.

def robinOracleComposition (n : Nat) : RobinOracleComposition n where
  derivativeOracle := {
    stencil := fourthOrderSecondDerivative
    bandwidth := 5
    matrix := robinDerivativeMatrix n
    sparseCorrect := ⟨"O_D^BS for fourth-order Robin stencil", "main.tex:784-801", false⟩
    bandwidth_eq := rfl
  }
  functionOracle := {
    functionPieces := 1
    normalizerBound := Coeff.symbol "N_f"

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “robin oracle composition bandwidth”; its local proof does not by itself complete the broader paper route.

@[simp] theorem robinOracleComposition_bandwidth (n : Nat) :
    (robinOracleComposition n).derivativeOracle.bandwidth = 5 := rfl

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “robin oracle composition function pieces”; its local proof does not by itself complete the broader paper route.

@[simp] theorem robinOracleComposition_functionPieces (n : Nat) :
    (robinOracleComposition n).functionOracle.functionPieces = 1 := rfl

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “robin oracle composition matrix”; its local proof does not by itself complete the broader paper route.

@[simp] theorem robinOracleComposition_matrix (n : Nat) :
    (robinOracleComposition n).derivativeOracle.matrix = robinDerivativeMatrix n := rfl

/-- Default proof-obligation bundle for the one-term Robin construction.
All obligations are unproved. main.tex:1131-1136 --/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “robin proof obligations”. Default proof-obligation bundle for the one-term Robin construction.

def robinProofObligations : GHL2025.RobinProofObligations := {}

/-! ## Circuit matrix semantics bridge --/

/--
CircuitMatrixSemantics for the one-term Robin circuit using honest gate matrices.
The full-space matrix is the product of the 7 honest gate matrices computed by
`evalGateMatrices`. Unproved gate claims remain in their own
`SemanticObligation` records.
figure:1_term_ROBIN --/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin circuit semantics”. CircuitMatrixSemantics for the one-term Robin circuit using honest gate matrices.

def oneTermRobinCircuitSemantics (n : Nat) :
    CircuitMatrixSemantics Coeff
      (GHL2025.oneTermRobinTotalQubits (oneTermParameters n)) where
  circuit := GHL2025.oneTermRobinCircuit
  gateMatrices := GHL2025.oneTermRobinGateMatrixPlaceholders (oneTermParameters n)
  gateListMatches := GHL2025.oneTermRobinPlaceholdersMatch (oneTermParameters n)
  matrix := evalGateMatrices (GHL2025.oneTermRobinGateMatrixPlaceholders (oneTermParameters n))
  matrix_eq_eval := by intro _ _; rfl

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin circuit dim compat”; its local proof does not by itself complete the broader paper route.

theorem oneTermRobinCircuitDimCompat (n : Nat) :
    qubitDim (GHL2025.oneTermRobinTotalQubits (oneTermParameters n)) =
      qubitDim (GHL2025.effectiveRobinSignalQubits (oneTermParameters n)) *
        gridSize n := by

commit-pinned source · Verso Blueprint panel

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

def oneTermRobinBlockExtractionTarget (n : Nat) :
    BlockExtractionTarget Coeff (gridSize n) (gridSize n)
      (qubitDim (GHL2025.effectiveRobinSignalQubits (oneTermParameters n))) :=
  (oneTermRobinCircuitSemantics n).blockExtractionTarget
    (gridSize n)
    (qubitDim (GHL2025.effectiveRobinSignalQubits (oneTermParameters n)))
    (oneTermRobinCircuitDimCompat n)
    (oneTermRobinAkMatrix n)
    GHL2025.oneTermRobinNormalizer
    ⟨0, by
      show (0 : Nat) < qubitDim (GHL2025.effectiveRobinSignalQubits (oneTermParameters n))

commit-pinned source · Verso Blueprint panel

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

def oneTermRobinCircuitBlockClaim (n : Nat)
    (hDim : qubitDim (GHL2025.oneTermRobinTotalQubits (oneTermParameters n)) =
      qubitDim (GHL2025.effectiveRobinSignalQubits (oneTermParameters n)) *
        gridSize n) :
    CircuitBlockEncodingClaim Coeff
      (GHL2025.oneTermRobinTotalQubits (oneTermParameters n))
      (gridSize n)
      (qubitDim (GHL2025.effectiveRobinSignalQubits (oneTermParameters n))) where
  semantics := oneTermRobinCircuitSemantics n
  target := oneTermRobinBlockExtractionTarget n
  dimCompat := hDim

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “default one term robin circuit block claim”. Default one-term Robin circuit block claim using the reusable dimension compatibility theorem.

def defaultOneTermRobinCircuitBlockClaim (n : Nat) :
    CircuitBlockEncodingClaim Coeff
      (GHL2025.oneTermRobinTotalQubits (oneTermParameters n))
      (gridSize n)
      (qubitDim (GHL2025.effectiveRobinSignalQubits (oneTermParameters n))) :=
  oneTermRobinCircuitBlockClaim n (oneTermRobinCircuitDimCompat n)

/--
Contract-only finite-dimensional LCU/block-composition dependency for the
one-term Robin theorem.

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin finite block composition contract”. Contract-only finite-dimensional LCU/block-composition dependency for the one-term Robin theorem.

def oneTermRobinFiniteBlockCompositionContract (n : Nat) :
    FiniteBlockCompositionContract Coeff
      (GHL2025.oneTermRobinTotalQubits (oneTermParameters n))
      (gridSize n)
      (qubitDim (GHL2025.effectiveRobinSignalQubits (oneTermParameters n))) where
  sourceAnchor :=
    "QBE finite-dimensional LCU/block-composition contract for GHL2025 Theorem one-term block-encoding"
  lcuSourceAnchor :=
    "LCU.StandardBlockEncoding; Childs-Wiebe 2012, arXiv:1202.5822; QBE cited-results row"
  theoremAnchor :=
    "Guseynov-Huang-Liu 2025, Theorem one-term block-encoding and Fig. 1-term Robin, arXiv:2506.20478"

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin finite block composition contract transcript”; its local proof does not by itself complete the broader paper route. The finite block-composition contract is wired to the concrete target.

theorem oneTermRobinFiniteBlockCompositionContract_transcript
    (n : Nat) :
    let contract := oneTermRobinFiniteBlockCompositionContract n
    contract.sourceAnchor =
        "QBE finite-dimensional LCU/block-composition contract for GHL2025 Theorem one-term block-encoding" ∧
      contract.lcuSourceAnchor =
        "LCU.StandardBlockEncoding; Childs-Wiebe 2012, arXiv:1202.5822; QBE cited-results row" ∧
      contract.theoremAnchor =
        "Guseynov-Huang-Liu 2025, Theorem one-term block-encoding and Fig. 1-term Robin, arXiv:2506.20478" ∧
      contract.claim = defaultOneTermRobinCircuitBlockClaim n ∧
      contract.expectedTarget = oneTermRobinBlockExtractionTarget n ∧

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin finite composition exact theorem obligation”. Contract-only interface for the exact finite composition theorem still needed to close the GHL2025 one-term Robin block encoding.

def oneTermRobinFiniteCompositionExactTheoremObligation
    (_n : Nat) : SemanticObligation where
  description :=
    "exact finite theorem: the signal-zero block of the Fig. 1-term Robin gate product equals oneTermRobinAkMatrix n normalized by N_D*N_f*kappa"
  source :=
    "GHL2025 Theorem one-term block-encoding, Eq. ROBIN clarified, Fig. 1-term ROBIN, Definition def:block-encoding; cited-results row LCU.StandardBlockEncoding"
  proved := false

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin finite composition exact theorem obligation transcript”; its local proof does not by itself complete the broader paper route.

theorem oneTermRobinFiniteCompositionExactTheoremObligation_transcript
    (n : Nat) :
    (oneTermRobinFiniteCompositionExactTheoremObligation n).source =
        "GHL2025 Theorem one-term block-encoding, Eq. ROBIN clarified, Fig. 1-term ROBIN, Definition def:block-encoding; cited-results row LCU.StandardBlockEncoding" ∧
      (oneTermRobinFiniteCompositionExactTheoremObligation n).proved =
        false := by

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin block encoding proof route”. A proposition-valued field is a requirement until a constructor supplies it. Phase 1 proof-route contract for the GHL2025 one-term Robin theorem.

structure OneTermRobinBlockEncodingProofRoute (n : Nat) where
  sourceAnchor : String
  parameters : GHL2025.OneTermRobinParameters
  theoremData : GHL2025.OneTermRobinTheoremData
  circuitSemantics :
    CircuitMatrixSemantics Coeff
      (GHL2025.oneTermRobinTotalQubits (oneTermParameters n))
  blockClaim :
    CircuitBlockEncodingClaim Coeff
      (GHL2025.oneTermRobinTotalQubits (oneTermParameters n))
      (gridSize n)

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin block encoding proof route”. Default theorem-level proof route for the one-term Robin block encoding.

def oneTermRobinBlockEncodingProofRoute
    (n : Nat) : OneTermRobinBlockEncodingProofRoute n where
  sourceAnchor :=
    "Guseynov-Huang-Liu 2025, Theorem one-term block-encoding, Fig. 1-term Robin, arXiv:2506.20478"
  parameters := oneTermParameters n
  theoremData := GHL2025.defaultOneTermRobinTheoremData (oneTermParameters n)
  circuitSemantics := oneTermRobinCircuitSemantics n
  blockClaim := defaultOneTermRobinCircuitBlockClaim n
  oracleComposition := robinOracleComposition n
  sparseAccessContract :=
    GHL2025.defaultBandedSparseAccessPaperContract (oneTermParameters n)

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route normalizer”; its local proof does not by itself complete the broader paper route. The proof-route contract links the theorem normalizer to the block target.

theorem oneTermRobinBlockEncodingProofRoute_normalizer
    (n : Nat) :
    (oneTermRobinBlockEncodingProofRoute n).theoremData.alpha =
      (oneTermRobinBlockEncodingProofRoute n).blockClaim.target.normalizer :=
  (oneTermRobinBlockEncodingProofRoute n).theoremNormalizerMatchesTarget

/--
The theorem-level route pins the block target used for the one-term theorem.

This is only a structural guard: it records the signal-index-zero convention,
the Robin target matrix, and the shared circuit semantics object.  It does not

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route block target”; its local proof does not by itself complete the broader paper route. The theorem-level route pins the block target used for the one-term theorem.

theorem oneTermRobinBlockEncodingProofRoute_blockTarget
    (n : Nat) :
    (oneTermRobinBlockEncodingProofRoute n).blockClaim.target =
        oneTermRobinBlockExtractionTarget n ∧
      (oneTermRobinBlockEncodingProofRoute n).blockClaim.semantics =
        (oneTermRobinBlockEncodingProofRoute n).circuitSemantics ∧
      (oneTermRobinBlockEncodingProofRoute n).blockClaim.target.targetMatrix =
        oneTermRobinAkMatrix n ∧
      (oneTermRobinBlockEncodingProofRoute n).blockClaim.target.signalIndex.val =
        0 :=
  ⟨(oneTermRobinBlockEncodingProofRoute n).claimUsesTarget,

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route block projection normalizer audit”; its local proof does not by itself complete the broader paper route. The theorem-level route uses the same block-projection target, normalizer, and open flags as the concrete circuit matrix target.

theorem oneTermRobinBlockEncodingProofRoute_blockProjectionNormalizerAudit
    (n : Nat) :
    (oneTermRobinBlockEncodingProofRoute n).blockClaim.target =
        oneTermRobinBlockExtractionTarget n ∧
      (oneTermRobinBlockEncodingProofRoute n).blockClaim.target.unitaryMatrix =
        cast (by rw [oneTermRobinCircuitDimCompat n])
          (oneTermRobinCircuitSemantics n).matrix ∧
      (oneTermRobinBlockEncodingProofRoute n).blockClaim.target.blockMatrix =
        signalSystemBlockProjection
          (qubitDim (GHL2025.effectiveRobinSignalQubits (oneTermParameters n)))
          (gridSize n)

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route circuit product”; its local proof does not by itself complete the broader paper route. The theorem-level route uses the active seven-gate circuit product.

theorem oneTermRobinBlockEncodingProofRoute_circuitProduct
    (n : Nat) :
    (oneTermRobinBlockEncodingProofRoute n).circuitSemantics.circuit =
        GHL2025.oneTermRobinCircuit ∧
      (oneTermRobinBlockEncodingProofRoute n).circuitSemantics.gateMatrices =
        GHL2025.oneTermRobinGateMatrixPlaceholders (oneTermParameters n) ∧
      (oneTermRobinBlockEncodingProofRoute n).circuitSemantics.gateListMatches =
        GHL2025.oneTermRobinPlaceholdersMatch (oneTermParameters n) ∧
      Matrix.PointwiseEq
        (oneTermRobinBlockEncodingProofRoute n).circuitSemantics.matrix
        (evalGateMatrices

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route gate unitary flags”; its local proof does not by itself complete the broader paper route. The theorem route uses the active seven-gate matrix product with the current gate-level proof flags frozen.

theorem oneTermRobinBlockEncodingProofRoute_gateUnitaryFlags
    (n : Nat) :
    (oneTermRobinBlockEncodingProofRoute n).circuitSemantics.gateMatrices.map
        (fun gateMatrix => gateMatrix.unitary.proved) =
        [true, false, false, false, false, true, false] ∧
      (oneTermRobinBlockEncodingProofRoute n).cleanupScopeDecision.selectedScope =
        GHL2025.BandedSparseAccessCleanupScope.activeGlobalSource ∧
      (oneTermRobinBlockEncodingProofRoute n).cleanupScopeDecision.semanticCleanupPromotionAllowed =
        false ∧
      (oneTermRobinBlockEncodingProofRoute n).theoremData.obligations.circuitUnitary.proved =
        false ∧

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route gate list and flags”; its local proof does not by itself complete the broader paper route. The theorem route keeps the Fig.

theorem oneTermRobinBlockEncodingProofRoute_gateListAndFlags
    (n : Nat) :
    (oneTermRobinBlockEncodingProofRoute n).circuitSemantics.gateMatrices.map
        (fun gateMatrix => gateMatrix.gate) =
        GHL2025.oneTermRobinCircuit ∧
      (oneTermRobinBlockEncodingProofRoute n).circuitSemantics.gateMatrices.map
        (fun gateMatrix => gateMatrix.unitary.proved) =
        [true, false, false, false, false, true, false] ∧
      (oneTermRobinBlockEncodingProofRoute n).cleanupScopeDecision.selectedScope =
        GHL2025.BandedSparseAccessCleanupScope.activeGlobalSource ∧
      (oneTermRobinBlockEncodingProofRoute n).cleanupScopeDecision.semanticCleanupPromotionAllowed =

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route gate projection freeze”; its local proof does not by itself complete the broader paper route. The theorem route keeps the seven-gate order and projection target frozen together.

theorem oneTermRobinBlockEncodingProofRoute_gateProjectionFreeze
    (n : Nat) :
    (oneTermRobinBlockEncodingProofRoute n).circuitSemantics.gateMatrices.map
        (fun gateMatrix => gateMatrix.gate) =
        GHL2025.oneTermRobinCircuit ∧
      (oneTermRobinBlockEncodingProofRoute n).circuitSemantics.gateMatrices.map
        (fun gateMatrix => gateMatrix.unitary.proved) =
        [true, false, false, false, false, true, false] ∧
      (oneTermRobinBlockEncodingProofRoute n).blockClaim.target.normalizer =
        GHL2025.oneTermRobinNormalizer ∧
      (oneTermRobinBlockEncodingProofRoute n).blockClaim.target.signalIndex.val =

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route layout projection audit”; its local proof does not by itself complete the broader paper route. The theorem-level signal and pure-ancilla counts are wired separately from the circuit-level projection dimension.

theorem oneTermRobinBlockEncodingProofRoute_layoutProjectionAudit
    (n : Nat) :
    (oneTermRobinBlockEncodingProofRoute n).theoremData.signalQubits =
        (GHL2025.oneTermRobinLayout (oneTermParameters n)).signalQubits ∧
      (oneTermRobinBlockEncodingProofRoute n).theoremData.pureAncillas =
        (GHL2025.oneTermRobinLayout (oneTermParameters n)).pureAncillas ∧
      (oneTermRobinBlockEncodingProofRoute n).theoremData.pureAncillas =
        (GHL2025.oneTermRobinResource (oneTermParameters n)).pureAncilla ∧
      GHL2025.effectiveRobinSignalQubits (oneTermParameters n) =
        (GHL2025.oneTermRobinLayout (oneTermParameters n)).signalQubits +
          (GHL2025.defaultRobinRegisterPartition

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block extraction target signal zero block indices”; its local proof does not by itself complete the broader paper route. The signal-index-zero Robin target uses the unshifted system row and column indices.

theorem oneTermRobinBlockExtractionTarget_signalZeroBlockIndices
    (n : Nat) (i j : Fin (gridSize n)) :
    signalSystemBlockRowIndex (gridSize n)
        (oneTermRobinBlockExtractionTarget n).signalIndex.val i.val = i.val ∧
      signalSystemBlockColIndex (gridSize n)
        (oneTermRobinBlockExtractionTarget n).signalIndex.val j.val = j.val := by

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route signal zero block indices”; its local proof does not by itself complete the broader paper route. The theorem-level route inherits the signal-index-zero block index convention from 'oneTermRobinBlockExtractionTarget'.

theorem oneTermRobinBlockEncodingProofRoute_signalZeroBlockIndices
    (n : Nat) (i j : Fin (gridSize n)) :
    signalSystemBlockRowIndex (gridSize n)
        (oneTermRobinBlockEncodingProofRoute n).blockClaim.target.signalIndex.val
        i.val = i.val ∧
      signalSystemBlockColIndex (gridSize n)
        (oneTermRobinBlockEncodingProofRoute n).blockClaim.target.signalIndex.val
        j.val = j.val := by

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route claim block correct false”; its local proof does not by itself complete the broader paper route. The theorem-level route keeps the circuit-claim block obligation open.

theorem oneTermRobinBlockEncodingProofRoute_claimBlockCorrectFalse
    (n : Nat) :
    (oneTermRobinBlockEncodingProofRoute n).blockClaim.blockCorrect.proved =
        false ∧
      (oneTermRobinBlockEncodingProofRoute n).blockClaim.target.blockProjection.proved =
        false ∧
      (oneTermRobinBlockEncodingProofRoute n).blockClaim.target.blockCorrect.proved =
        false := by

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route flags false”; its local proof does not by itself complete the broader paper route. The theorem-level route keeps all semantic blockers in obligation mode.

theorem oneTermRobinBlockEncodingProofRoute_flags_false (n : Nat) :
    (oneTermRobinBlockEncodingProofRoute n).blockClaim.target.blockProjection.proved =
        false ∧
      (oneTermRobinBlockEncodingProofRoute n).blockClaim.target.blockCorrect.proved =
        false ∧
      (oneTermRobinBlockEncodingProofRoute n).theoremData.obligations.blockExtraction.proved =
        false ∧
      (oneTermRobinBlockEncodingProofRoute n).theoremData.obligations.circuitUnitary.proved =
        false ∧
      (oneTermRobinBlockEncodingProofRoute n).sparseAccessContract.daggerCleanup.proved =
        false ∧

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route of external source and flags”; its local proof does not by itself complete the broader paper route. The theorem route exposes the 'O_f' external-source transcript and false flags.

theorem oneTermRobinBlockEncodingProofRoute_ofExternalSourceAndFlags
    (n j : Nat) :
    (oneTermRobinBlockEncodingProofRoute n).functionOracleSource =
        GHL2025.functionOracleExternalAmplitudeSourceContract ∧
      (GHL2025.functionOracleAmplitudeProofRoute
        (oneTermParameters n) j).sourceAnchor =
        (oneTermRobinBlockEncodingProofRoute n).functionOracleSource.sourceAnchor ∧
      (GHL2025.functionOracleAmplitudeProofRoute
        (oneTermParameters n) j).normalizerNf =
        (oneTermRobinBlockEncodingProofRoute n).functionOracleSource.normalizerNf ∧
      (GHL2025.functionOracleAmplitudeProofRoute

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route of clean function oracle entry”; its local proof does not by itself complete the broader paper route. The route-level 'O_f' gate exposes the clean-workspace paper branch entry.

theorem oneTermRobinBlockEncodingProofRoute_ofCleanFunctionOracleEntry
    (n : Nat)
    (i j : Fin
      (qubitDim (GHL2025.oneTermRobinTotalQubits (oneTermParameters n))))
    (hClean :
      (GHL2025.functionOraclePaperImage
        (oneTermParameters n) j.val).cleanWorkspaceBranch = true)
    (hBranch :
      i.val =
        (GHL2025.functionOraclePaperImage
          (oneTermParameters n) j.val).cleanBranchBasisIndex) :

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route derivative boundary contract map”; its local proof does not by itself complete the broader paper route. The theorem route exposes the derivative-amplitude and boundary-rotation contracts that share the paper normalizer 'N_D'.

theorem oneTermRobinBlockEncodingProofRoute_derivativeBoundaryContractMap
    (n row sparse : Nat) :
    ((GHL2025.sparseAmplitudeOracleDTCoefficientNormalizerProofRoute
        (oneTermParameters n) row sparse).coefficient =
        (GHL2025.derivativeNormalizerNDSourceBound
          (oneTermParameters n) row sparse).sourceCoefficient ∧
      (GHL2025.sparseAmplitudeOracleDTCoefficientNormalizerProofRoute
        (oneTermParameters n) row sparse).normalizerND =
        (GHL2025.derivativeNormalizerNDSourceBound
          (oneTermParameters n) row sparse).normalizerND ∧
      (GHL2025.sparseAmplitudeOracleDTCoefficientNormalizerProofRoute

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route odts ket zero entry”; its local proof does not by itself complete the broader paper route. The route-level 'O_DT^S' gate exposes the Eq.

theorem oneTermRobinBlockEncodingProofRoute_odtsKetZeroEntry
    (n : Nat)
    (i j : Fin
      (qubitDim (GHL2025.oneTermRobinTotalQubits (oneTermParameters n))))
    (hIndicator :
      (GHL2025.sparseAmplitudeOracleDTPaperRegisters
        (oneTermParameters n) j.val).indicatorBit = 1)
    (hAncilla :
      (GHL2025.sparseAmplitudeOracleDTPaperRegisters
        (oneTermParameters n) j.val).ancillaBit = 0)
    (hRow :

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route boundary ket zero entry”; its local proof does not by itself complete the broader paper route. The route-level 'Ry_boundary' gate exposes the boundary ket-zero entry.

theorem oneTermRobinBlockEncodingProofRoute_boundaryKetZeroEntry
    (n : Nat)
    (i j : Fin
      (qubitDim (GHL2025.oneTermRobinTotalQubits (oneTermParameters n))))
    (hIndicator :
      (GHL2025.boundaryRotationPaperRegisters
        (oneTermParameters n) j.val).indicatorBit = 0)
    (hAncilla :
      (GHL2025.boundaryRotationPaperRegisters
        (oneTermParameters n) j.val).ancillaBit = 0)
    (hRow :

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route odbs active global slot blockers”; its local proof does not by itself complete the broader paper route. The theorem-level route exposes the active global-slot 'O_D^BS' blockers.

theorem oneTermRobinBlockEncodingProofRoute_odbsActiveGlobalSlotBlockers
    (n j : Nat) :
    (oneTermRobinBlockEncodingProofRoute n).cleanupScopeDecision.selectedScope =
        GHL2025.BandedSparseAccessCleanupScope.activeGlobalSource ∧
      (oneTermRobinBlockEncodingProofRoute n).cleanupScopeDecision.selectedPredicate =
        "bandedSparseAccessPaperGlobalSlotSource" ∧
      (oneTermRobinBlockEncodingProofRoute n).cleanupScopeDecision.selectedEvidence =
        "bandedSparseAccessGlobalSlotInverseOnRangeContract_restrictedDaggerColumnIndicator" ∧
      (oneTermRobinBlockEncodingProofRoute n).cleanupScopeDecision.fullCleanDomainSelected =
        false ∧
      (oneTermRobinBlockEncodingProofRoute n).cleanupScopeDecision.fullSpaceSelected =

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route active odbs gate pair blocked”; its local proof does not by itself complete the broader paper route. The theorem-level route keeps the active 'O_D^BS' gate pair in obligation mode.

theorem oneTermRobinBlockEncodingProofRoute_activeOdbsGatePairBlocked
    (n : Nat) :
    (GHL2025.oneTermRobinGate_O_D_BS (oneTermParameters n)).unitary.proved =
        false ∧
      (GHL2025.oneTermRobinGate_O_D_BS_dagger (oneTermParameters n)).unitary.proved =
        false ∧
      (oneTermRobinBlockEncodingProofRoute n).sparseAccessContract.daggerCleanup.proved =
        false ∧
      (oneTermRobinBlockEncodingProofRoute n).sparseAccessContract.unitaryExtension.proved =
        false ∧
      (oneTermRobinBlockEncodingProofRoute n).cleanupScopeDecision.semanticCleanupPromotionAllowed =

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route odbs active scope keeps final flags false”; its local proof does not by itself complete the broader paper route. The active-scope blocker propagates to the final theorem flags.

theorem oneTermRobinBlockEncodingProofRoute_odbsActiveScopeKeepsFinalFlagsFalse
    (n : Nat) :
    (oneTermRobinBlockEncodingProofRoute n).cleanupScopeDecision.semanticCleanupPromotionAllowed =
        false ∧
      (GHL2025.oneTermRobinGate_O_D_BS (oneTermParameters n)).unitary.proved =
        false ∧
      (GHL2025.oneTermRobinGate_O_D_BS_dagger (oneTermParameters n)).unitary.proved =
        false ∧
      (oneTermRobinBlockEncodingProofRoute n).sparseAccessContract.daggerCleanup.proved =
        false ∧
      (oneTermRobinBlockEncodingProofRoute n).theoremData.obligations.circuitUnitary.proved =

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route active odbs gate pair wiring”; its local proof does not by itself complete the broader paper route. The theorem-level route wires the active 'O_D^BS' gate pair at the Fig.

theorem oneTermRobinBlockEncodingProofRoute_activeOdbsGatePairWiring
    (n : Nat) :
    (((oneTermRobinBlockEncodingProofRoute n).circuitSemantics.gateMatrices.get
        ⟨3, by
          simp [oneTermRobinBlockEncodingProofRoute, oneTermRobinCircuitSemantics,
            GHL2025.oneTermRobinGateMatrixPlaceholders]⟩).gate =
        Gate.oracleCall "O_D^BS") ∧
      (((oneTermRobinBlockEncodingProofRoute n).circuitSemantics.gateMatrices.get
        ⟨3, by
          simp [oneTermRobinBlockEncodingProofRoute, oneTermRobinCircuitSemantics,
            GHL2025.oneTermRobinGateMatrixPlaceholders]⟩).matrix =

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route active odbs gate pair public sources”; its local proof does not by itself complete the broader paper route. The active 'O_D^BS' gate pair keeps public source anchors on its obligation records.

theorem oneTermRobinBlockEncodingProofRoute_activeOdbsGatePairPublicSources
    (n : Nat) :
    (GHL2025.oneTermRobinGate_O_D_BS (oneTermParameters n)).unitary.source =
        "Guseynov-Huang-Liu 2025, Lemma 1, arXiv:2506.20478" ∧
      (GHL2025.oneTermRobinGate_O_D_BS_dagger (oneTermParameters n)).unitary.source =
        "Guseynov-Huang-Liu 2025, Fig. 1-term Robin and Lemma 1, arXiv:2506.20478" ∧
      (GHL2025.oneTermRobinGate_O_D_BS (oneTermParameters n)).unitary.proved =
        false ∧
      (GHL2025.oneTermRobinGate_O_D_BS_dagger (oneTermParameters n)).unitary.proved =
        false := by

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route odbs active global slot gate freeze”; its local proof does not by itself complete the broader paper route. The active global-slot gate freeze combines the active matrices, cleanup-scope blocker, block target, and final false flags.

theorem oneTermRobinBlockEncodingProofRoute_odbsActiveGlobalSlotGateFreeze
    (n j : Nat) :
    (oneTermRobinBlockEncodingProofRoute n).cleanupScopeDecision.selectedScope =
        GHL2025.BandedSparseAccessCleanupScope.activeGlobalSource ∧
      ((GHL2025.bandedSparseAccessFullCleanDomainExtensionContract
        (oneTermParameters n)).unusedBranchImageRuleContract
        j).proposedImageIndex = none ∧
      (GHL2025.oneTermRobinGate_O_D_BS
        (oneTermParameters n)).unitary.source =
        "Guseynov-Huang-Liu 2025, Lemma 1, arXiv:2506.20478" ∧
      (GHL2025.oneTermRobinGate_O_D_BS_dagger

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route projection source freeze”; its local proof does not by itself complete the broader paper route. The source-gate freeze keeps the projection target and final theorem flags open under the active global-slot cleanup scope.

theorem oneTermRobinBlockEncodingProofRoute_projectionSourceFreeze
    (n : Nat) :
    (oneTermRobinBlockEncodingProofRoute n).blockClaim.target.normalizer =
        GHL2025.oneTermRobinNormalizer ∧
      (oneTermRobinBlockEncodingProofRoute n).blockClaim.target.signalIndex.val =
        0 ∧
      (oneTermRobinBlockEncodingProofRoute n).blockClaim.target.blockProjection.proved =
        false ∧
      (oneTermRobinBlockEncodingProofRoute n).blockClaim.target.blockCorrect.proved =
        false ∧
      (oneTermRobinBlockEncodingProofRoute n).theoremData.obligations.circuitUnitary.proved =

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route rejected row dependent collision regression n 3”; its local proof does not by itself complete the broader paper route. The old row-dependent collision remains rejected-model regression memory.

theorem oneTermRobinBlockEncodingProofRoute_rejectedRowDependentCollisionRegression_n3 :
    let p := oneTermParameters 3
    GHL2025.bandedSparseAccessRowDependentPaperImage p 0 =
        GHL2025.bandedSparseAccessRowDependentPaperImage p 48 ∧
      GHL2025.bandedSparseAccessPaperImage p 0 ≠
        GHL2025.bandedSparseAccessPaperImage p 48 ∧
      (GHL2025.oneTermRobinGate_O_D_BS p).matrix
          ⟨96, by native_decide⟩ ⟨0, by native_decide⟩ = Coeff.rat 1 ∧
      (GHL2025.oneTermRobinGate_O_D_BS p).matrix
          ⟨16, by native_decide⟩ ⟨48, by native_decide⟩ = Coeff.rat 1 ∧
      (oneTermRobinBlockEncodingProofRoute 3).cleanupScopeDecision.selectedScope =

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route encoded out of range sparse slot n 3”; its local proof does not by itself complete the broader paper route. The theorem route records encoded sparse value '7' as the first out-of-range clean slot for the one-term 'kappa = 7' source domain.

theorem oneTermRobinBlockEncodingProofRoute_encodedOutOfRangeSparseSlot_n3 :
    let p := oneTermParameters 3
    GHL2025.bandedSparseAccessPaperCleanInput p 112 = true ∧
      (GHL2025.bandedSparseAccessPaperRegisters p 112).sparseIndexValue = 7 ∧
      GHL2025.bandedSparseAccessPaperSparseIndexInKappa p 112 = false ∧
      GHL2025.bandedSparseAccessPaperGlobalSlotSource p 112 = false ∧
      (oneTermRobinBlockEncodingProofRoute 3).cleanupScopeDecision.selectedScope =
        GHL2025.BandedSparseAccessCleanupScope.activeGlobalSource ∧
      (oneTermRobinBlockEncodingProofRoute 3).cleanupScopeDecision.semanticCleanupPromotionAllowed =
        false ∧
      (oneTermRobinBlockEncodingProofRoute 3).sparseAccessContract.daggerCleanup.proved =

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route contract drift column 8 blocked n 3”; its local proof does not by itself complete the broader paper route. The theorem route carries the active column-8 'O_D^BS' contract-drift guard.

theorem oneTermRobinBlockEncodingProofRoute_contractDriftColumn8Blocked_n3 :
    let p := oneTermParameters 3
    GHL2025.bandedSparseAccessPaperImage p 8 = 40 ∧
      (((oneTermRobinBlockEncodingProofRoute 3).circuitSemantics.gateMatrices.get
        ⟨3, by
          simp [oneTermRobinBlockEncodingProofRoute, oneTermRobinCircuitSemantics,
            GHL2025.oneTermRobinGateMatrixPlaceholders]⟩).matrix
          ⟨40, by native_decide⟩ ⟨8, by native_decide⟩ = Coeff.rat 1) ∧
      (((oneTermRobinBlockEncodingProofRoute 3).circuitSemantics.gateMatrices.get
        ⟨3, by
          simp [oneTermRobinBlockEncodingProofRoute, oneTermRobinCircuitSemantics,

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route sparse access contract identity”; its local proof does not by itself complete the broader paper route. The theorem-level route uses the default Lemma 1 'O_D^BS' contract object.

theorem oneTermRobinBlockEncodingProofRoute_sparseAccessContractIdentity
    (n : Nat) :
    (oneTermRobinBlockEncodingProofRoute n).sparseAccessContract =
        GHL2025.defaultBandedSparseAccessPaperContract (oneTermParameters n) ∧
      (oneTermRobinBlockEncodingProofRoute n).sparseAccessContract.forwardCorrect.proved =
        false ∧
      (oneTermRobinBlockEncodingProofRoute n).sparseAccessContract.daggerCleanup.proved =
        false ∧
      (oneTermRobinBlockEncodingProofRoute n).sparseAccessContract.unitaryExtension.proved =
        false ∧
      (oneTermRobinBlockEncodingProofRoute n).cleanupScopeDecision.semanticCleanupPromotionAllowed =

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route odbs paper contract transcript”; its local proof does not by itself complete the broader paper route. The theorem-level route carries the Lemma 1 'O_D^BS' paper contract verbatim.

theorem oneTermRobinBlockEncodingProofRoute_odbsPaperContractTranscript
    (n : Nat) :
    (oneTermRobinBlockEncodingProofRoute n).sparseAccessContract.sourceAnchor =
        "Guseynov-Huang-Liu 2025, Lemma 1, arXiv:2506.20478" ∧
      (oneTermRobinBlockEncodingProofRoute n).sparseAccessContract.rowRegisterQubits =
        (oneTermParameters n).n ∧
      (oneTermRobinBlockEncodingProofRoute n).sparseAccessContract.paddedZeroQubits =
        (oneTermParameters n).n - clog2 (oneTermParameters n).kappa ∧
      (oneTermRobinBlockEncodingProofRoute n).sparseAccessContract.sparseIndexQubits =
        clog2 (oneTermParameters n).kappa ∧
      (oneTermRobinBlockEncodingProofRoute n).sparseAccessContract.outputAddressQubits =

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route odbs restricted dagger column indicator”; its local proof does not by itself complete the broader paper route. The theorem-level route exposes the active-domain 'O_D^BS' dagger-column indicator.

theorem oneTermRobinBlockEncodingProofRoute_odbsRestrictedDaggerColumnIndicator
    (n : Nat)
    (source : Fin
      (qubitDim (GHL2025.oneTermRobinTotalQubits (oneTermParameters n))))
    (hn : 3 <= n)
    (hsource : GHL2025.bandedSparseAccessPaperGlobalSlotSource
      (oneTermParameters n) source.val = true) :
    ∃ (post pre : Fin
        (qubitDim (GHL2025.oneTermRobinTotalQubits (oneTermParameters n)))),
      GHL2025.BandedSparseAccessPostSwapCleanup
        (oneTermParameters n) source post pre ∧

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route odbs cleanup scope decision”; its local proof does not by itself complete the broader paper route. The theorem route selects the active global-source domain as the next 'O_D^BS' cleanup theorem scope.

theorem oneTermRobinBlockEncodingProofRoute_odbsCleanupScopeDecision
    (n : Nat) :
    (GHL2025.bandedSparseAccessCleanupScopeDecision
        (oneTermParameters n)).selectedScope =
        GHL2025.BandedSparseAccessCleanupScope.activeGlobalSource ∧
      (GHL2025.bandedSparseAccessCleanupScopeDecision
        (oneTermParameters n)).selectedPredicate =
        "bandedSparseAccessPaperGlobalSlotSource" ∧
      (GHL2025.bandedSparseAccessCleanupScopeDecision
        (oneTermParameters n)).selectedEvidence =
        "bandedSparseAccessGlobalSlotInverseOnRangeContract_restrictedDaggerColumnIndicator" ∧

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route odbs full clean domain image rule blocked”; its local proof does not by itself complete the broader paper route. The theorem route keeps the full clean-domain 'O_D^BS' image-rule slot blocked.

theorem oneTermRobinBlockEncodingProofRoute_odbsFullCleanDomainImageRuleBlocked
    (n j : Nat) :
    (GHL2025.bandedSparseAccessCleanupScopeDecision
        (oneTermParameters n)).selectedScope =
        GHL2025.BandedSparseAccessCleanupScope.activeGlobalSource ∧
      (GHL2025.bandedSparseAccessCleanupScopeDecision
        (oneTermParameters n)).fullCleanDomainSelected = false ∧
      (GHL2025.bandedSparseAccessCleanupScopeDecision
        (oneTermParameters n)).semanticCleanupPromotionAllowed = false ∧
      (GHL2025.bandedSparseAccessCleanupScopeDecision
        (oneTermParameters n)).fullCleanDomainCleanup.proved = false ∧

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route odbs active global source cleanup interface”; its local proof does not by itself complete the broader paper route. The theorem-level route exposes the selected active global-source cleanup interface for 'O_D^BS'.

theorem oneTermRobinBlockEncodingProofRoute_odbsActiveGlobalSourceCleanupInterface
    (n : Nat)
    (source : Fin
      (qubitDim (GHL2025.oneTermRobinTotalQubits (oneTermParameters n))))
    (hn : 3 <= n)
    (hsource : GHL2025.bandedSparseAccessPaperGlobalSlotSource
      (oneTermParameters n) source.val = true) :
    ∃ (post pre : Fin
        (qubitDim (GHL2025.oneTermRobinTotalQubits (oneTermParameters n)))),
      GHL2025.BandedSparseAccessPostSwapCleanup
        (oneTermParameters n) source post pre ∧

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route odbs active global source cleanup contract map”; its local proof does not by itself complete the broader paper route. The theorem-level route exposes the active global-source cleanup contract map.

theorem oneTermRobinBlockEncodingProofRoute_odbsActiveGlobalSourceCleanupContractMap
    (n : Nat)
    (source : Fin
      (qubitDim (GHL2025.oneTermRobinTotalQubits (oneTermParameters n))))
    (hn : 3 <= n)
    (hsource : GHL2025.bandedSparseAccessPaperGlobalSlotSource
      (oneTermParameters n) source.val = true) :
    ∃ (post pre : Fin
        (qubitDim (GHL2025.oneTermRobinTotalQubits (oneTermParameters n)))),
      GHL2025.BandedSparseAccessPostSwapCleanup
        (oneTermParameters n) source post pre ∧

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route theorem transcript dependencies”; its local proof does not by itself complete the broader paper route. The theorem route exposes the source transcript dependencies for Theorem '1 term robin'.

theorem oneTermRobinBlockEncodingProofRoute_theoremTranscriptDependencies
    (n : Nat) :
    (oneTermRobinBlockEncodingProofRoute n).sourceAnchor =
        "Guseynov-Huang-Liu 2025, Theorem one-term block-encoding, Fig. 1-term Robin, arXiv:2506.20478" ∧
      (oneTermRobinBlockEncodingProofRoute n).theoremData.alpha =
        (oneTermRobinBlockEncodingProofRoute n).blockClaim.target.normalizer ∧
      (oneTermRobinBlockEncodingProofRoute n).theoremData.alpha =
        GHL2025.oneTermRobinNormalizer ∧
      (oneTermRobinBlockEncodingProofRoute n).circuitSemantics.gateMatrices.map
        (fun gateMatrix => gateMatrix.gate) =
        GHL2025.oneTermRobinCircuit ∧

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route theorem transcript active cleanup map”; its local proof does not by itself complete the broader paper route. The theorem transcript consumes the active global-source cleanup map.

theorem oneTermRobinBlockEncodingProofRoute_theoremTranscriptActiveCleanupMap
    (n : Nat)
    (source : Fin
      (qubitDim (GHL2025.oneTermRobinTotalQubits (oneTermParameters n))))
    (hn : 3 <= n)
    (hsource : GHL2025.bandedSparseAccessPaperGlobalSlotSource
      (oneTermParameters n) source.val = true) :
    ∃ (post pre : Fin
        (qubitDim (GHL2025.oneTermRobinTotalQubits (oneTermParameters n)))),
      GHL2025.BandedSparseAccessPostSwapCleanup
        (oneTermParameters n) source post pre ∧

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route robin clarified gamma transcript”; its local proof does not by itself complete the broader paper route. The theorem transcript exposes the Eq.

theorem oneTermRobinBlockEncodingProofRoute_robinClarifiedGammaTranscript
    (n : Nat)
    (source : Fin
      (qubitDim (GHL2025.oneTermRobinTotalQubits (oneTermParameters n))))
    (hn : 3 <= n)
    (hsource : GHL2025.bandedSparseAccessPaperGlobalSlotSource
      (oneTermParameters n) source.val = true) :
    let gamma := GHL2025.defaultRobinWavefunctionDecomposition
      (oneTermParameters n)
    ∃ (post pre : Fin
        (qubitDim (GHL2025.oneTermRobinTotalQubits (oneTermParameters n)))),

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route block projection dependency map”; its local proof does not by itself complete the broader paper route. The theorem transcript exposes the dependency map for the final block projection.

theorem oneTermRobinBlockEncodingProofRoute_blockProjectionDependencyMap
    (n : Nat)
    (source : Fin
      (qubitDim (GHL2025.oneTermRobinTotalQubits (oneTermParameters n))))
    (hn : 3 <= n)
    (hsource : GHL2025.bandedSparseAccessPaperGlobalSlotSource
      (oneTermParameters n) source.val = true)
    (i j : Fin (gridSize n)) :
    let gamma := GHL2025.defaultRobinWavefunctionDecomposition
      (oneTermParameters n)
    ∃ (post pre : Fin

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route full gate contract ledger”; its local proof does not by itself complete the broader paper route. The theorem route exposes one ledger for all Fig.

theorem oneTermRobinBlockEncodingProofRoute_fullGateContractLedger
    (n row sparse ofColumn : Nat)
    (source : Fin
      (qubitDim (GHL2025.oneTermRobinTotalQubits (oneTermParameters n))))
    (hn : 3 <= n)
    (hsource : GHL2025.bandedSparseAccessPaperGlobalSlotSource
      (oneTermParameters n) source.val = true) :
    ∃ (post pre : Fin
        (qubitDim (GHL2025.oneTermRobinTotalQubits (oneTermParameters n)))),
      GHL2025.BandedSparseAccessPostSwapCleanup
        (oneTermParameters n) source post pre ∧

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route theorem transcript closure packet”; its local proof does not by itself complete the broader paper route. The theorem-transcript closure packet consumes the current Phase 1 guards.

theorem oneTermRobinBlockEncodingProofRoute_theoremTranscriptClosurePacket
    (n row sparse ofColumn : Nat)
    (source : Fin
      (qubitDim (GHL2025.oneTermRobinTotalQubits (oneTermParameters n))))
    (hn : 3 <= n)
    (hsource : GHL2025.bandedSparseAccessPaperGlobalSlotSource
      (oneTermParameters n) source.val = true)
    (i j : Fin (gridSize n)) :
    let gamma := GHL2025.defaultRobinWavefunctionDecomposition
      (oneTermParameters n)
    ∃ (post pre : Fin

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route finite block composition contract map”; its local proof does not by itself complete the broader paper route. The theorem route now has a typed finite LCU/block-composition contract.

theorem oneTermRobinBlockEncodingProofRoute_finiteBlockCompositionContractMap
    (n row sparse ofColumn : Nat)
    (source : Fin
      (qubitDim (GHL2025.oneTermRobinTotalQubits (oneTermParameters n))))
    (hn : 3 <= n)
    (hsource : GHL2025.bandedSparseAccessPaperGlobalSlotSource
      (oneTermParameters n) source.val = true)
    (i j : Fin (gridSize n)) :
    let contract := oneTermRobinFiniteBlockCompositionContract n
    ∃ (post pre : Fin
        (qubitDim (GHL2025.oneTermRobinTotalQubits (oneTermParameters n)))),

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route finite composition exact theorem interface”; its local proof does not by itself complete the broader paper route. The theorem route exposes the exact finite composition theorem interface.

theorem oneTermRobinBlockEncodingProofRoute_finiteCompositionExactTheoremInterface
    (n row sparse ofColumn : Nat)
    (source : Fin
      (qubitDim (GHL2025.oneTermRobinTotalQubits (oneTermParameters n))))
    (hn : 3 <= n)
    (hsource : GHL2025.bandedSparseAccessPaperGlobalSlotSource
      (oneTermParameters n) source.val = true)
    (i j : Fin (gridSize n)) :
    let contract := oneTermRobinFiniteBlockCompositionContract n
    let exactTheorem := oneTermRobinFiniteCompositionExactTheoremObligation n
    ∃ (post pre : Fin

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 signal block entry obligation”. Contract-only entry obligation connecting Eq.

def oneTermRobinGamma3SignalBlockEntryObligation
    (_n : Nat) : SemanticObligation where
  description :=
    "gamma3-to-signal-zero-block entry theorem: each system entry of the signal-zero projection of the Fig. 1-term Robin circuit product equals the Eq. ROBIN clarified gamma3 clean-branch coefficient, hence oneTermRobinAkMatrix n normalized by N_D*N_f*kappa"
  source :=
    "GHL2025 Eq. ROBIN clarified gamma3 line, Theorem one-term block-encoding, Fig. 1-term ROBIN, Definition def:block-encoding"
  proved := false

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 signal block entry obligation transcript”; its local proof does not by itself complete the broader paper route.

theorem oneTermRobinGamma3SignalBlockEntryObligation_transcript
    (n : Nat) :
    (oneTermRobinGamma3SignalBlockEntryObligation n).source =
        "GHL2025 Eq. ROBIN clarified gamma3 line, Theorem one-term block-encoding, Fig. 1-term ROBIN, Definition def:block-encoding" ∧
      (oneTermRobinGamma3SignalBlockEntryObligation n).proved =
        false := by

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route gamma 3 signal block entry obligation map”; its local proof does not by itself complete the broader paper route. The exact finite-composition interface is refined to the gamma3 entry target.

theorem oneTermRobinBlockEncodingProofRoute_gamma3SignalBlockEntryObligationMap
    (n row sparse ofColumn : Nat)
    (source : Fin
      (qubitDim (GHL2025.oneTermRobinTotalQubits (oneTermParameters n))))
    (hn : 3 <= n)
    (hsource : GHL2025.bandedSparseAccessPaperGlobalSlotSource
      (oneTermParameters n) source.val = true)
    (i j : Fin (gridSize n)) :
    let gamma := GHL2025.defaultRobinWavefunctionDecomposition
      (oneTermParameters n)
    let contract := oneTermRobinFiniteBlockCompositionContract n

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route gamma 3 target entry data”; its local proof does not by itself complete the broader paper route. The gamma3 entry obligation also exposes the concrete target entry.

theorem oneTermRobinBlockEncodingProofRoute_gamma3TargetEntryData
    (n row sparse ofColumn : Nat)
    (source : Fin
      (qubitDim (GHL2025.oneTermRobinTotalQubits (oneTermParameters n))))
    (hn : 3 <= n)
    (hsource : GHL2025.bandedSparseAccessPaperGlobalSlotSource
      (oneTermParameters n) source.val = true)
    (i j : Fin (gridSize n)) :
    let gamma := GHL2025.defaultRobinWavefunctionDecomposition
      (oneTermParameters n)
    let contract := oneTermRobinFiniteBlockCompositionContract n

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route gamma 3 factor entry ledger”; its local proof does not by itself complete the broader paper route. The gamma3 factor-entry ledger joins the existing single-gate transcript bridges.

theorem oneTermRobinBlockEncodingProofRoute_gamma3FactorEntryLedger
    (n row sparse ofColumn : Nat)
    (source : Fin
      (qubitDim (GHL2025.oneTermRobinTotalQubits (oneTermParameters n))))
    (hn : 3 <= n)
    (hsource : GHL2025.bandedSparseAccessPaperGlobalSlotSource
      (oneTermParameters n) source.val = true)
    (i j : Fin (gridSize n))
    (ofRow ofCol odtsRow odtsCol ryRow ryCol : Fin
      (qubitDim (GHL2025.oneTermRobinTotalQubits (oneTermParameters n))))
    (hOfClean :

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route gamma 3 signal block product entry”; its local proof does not by itself complete the broader paper route. The gamma3 signal-block entry is the concrete seven-gate product entry.

theorem oneTermRobinBlockEncodingProofRoute_gamma3SignalBlockProductEntry
    (n row sparse ofColumn : Nat)
    (source : Fin
      (qubitDim (GHL2025.oneTermRobinTotalQubits (oneTermParameters n))))
    (hn : 3 <= n)
    (hsource : GHL2025.bandedSparseAccessPaperGlobalSlotSource
      (oneTermParameters n) source.val = true)
    (i j : Fin (gridSize n))
    (ofRow ofCol odtsRow odtsCol ryRow ryCol : Fin
      (qubitDim (GHL2025.oneTermRobinTotalQubits (oneTermParameters n))))
    (hOfClean :

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route gamma 3 ak coefficient entry contract”; its local proof does not by itself complete the broader paper route. The gamma3 coefficient-entry contract is now tied to the Ak target.

theorem oneTermRobinBlockEncodingProofRoute_gamma3AkCoefficientEntryContract
    (n row sparse ofColumn : Nat)
    (source : Fin
      (qubitDim (GHL2025.oneTermRobinTotalQubits (oneTermParameters n))))
    (hn : 3 <= n)
    (hsource : GHL2025.bandedSparseAccessPaperGlobalSlotSource
      (oneTermParameters n) source.val = true)
    (i j : Fin (gridSize n))
    (ofRow ofCol odtsRow odtsCol ryRow ryCol : Fin
      (qubitDim (GHL2025.oneTermRobinTotalQubits (oneTermParameters n))))
    (hOfClean :

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 product to coefficient obligation”. Named product-to-coefficient obligation for the gamma3 entry.

def oneTermRobinGamma3ProductToCoefficientObligation
    (n : Nat) (_i _j : Fin (gridSize n)) : SemanticObligation where
  description :=
    "gamma3 product-to-coefficient theorem: the projected seven-gate product entry equals the Ak target entry normalized by N_D*N_f*kappa"
  source :=
    "GHL2025 Eq. ROBIN clarified gamma3 line, Theorem one-term block-encoding, Fig. 1-term ROBIN, Definition def:block-encoding; cited-results row LCU.StandardBlockEncoding"
  proved := false

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 product to coefficient obligation transcript”; its local proof does not by itself complete the broader paper route.

theorem oneTermRobinGamma3ProductToCoefficientObligation_transcript
    (n : Nat) (i j : Fin (gridSize n)) :
    (oneTermRobinGamma3ProductToCoefficientObligation n i j).source =
        "GHL2025 Eq. ROBIN clarified gamma3 line, Theorem one-term block-encoding, Fig. 1-term ROBIN, Definition def:block-encoding; cited-results row LCU.StandardBlockEncoding" ∧
      (oneTermRobinGamma3ProductToCoefficientObligation n i j).proved =
        false := by

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route gamma 3 product to coefficient interface”; its local proof does not by itself complete the broader paper route. Interface for the exact finite product-to-coefficient theorem.

theorem oneTermRobinBlockEncodingProofRoute_gamma3ProductToCoefficientInterface
    (n row sparse ofColumn : Nat)
    (source : Fin
      (qubitDim (GHL2025.oneTermRobinTotalQubits (oneTermParameters n))))
    (hn : 3 <= n)
    (hsource : GHL2025.bandedSparseAccessPaperGlobalSlotSource
      (oneTermParameters n) source.val = true)
    (i j : Fin (gridSize n))
    (ofRow ofCol odtsRow odtsCol ryRow ryCol : Fin
      (qubitDim (GHL2025.oneTermRobinTotalQubits (oneTermParameters n))))
    (hOfClean :

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route gamma 3 projection path audit n 3”; its local proof does not by itself complete the broader paper route. Focused path-state audit for the current 'n = 3' gamma3 product attempt.

theorem oneTermRobinBlockEncodingProofRoute_gamma3ProjectionPathAudit_n3 :
    let p := oneTermParameters 3
    let fullDim := qubitDim (GHL2025.oneTermRobinTotalQubits p)
    let sysRow : Fin (gridSize 3) := ⟨2, by native_decide⟩
    let sysCol : Fin (gridSize 3) := ⟨5, by native_decide⟩
    let row2 : Fin fullDim := ⟨2, by native_decide⟩
    let row18 : Fin fullDim := ⟨18, by native_decide⟩
    let row192 : Fin fullDim := ⟨192, by native_decide⟩
    let col2 : Fin fullDim := ⟨2, by native_decide⟩
    let col160 : Fin fullDim := ⟨160, by native_decide⟩
    let col132 : Fin fullDim := ⟨132, by native_decide⟩

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 paper basis index”. Full-basis index for the clean 'gamma3' ket layout in Eq.

def oneTermRobinGamma3PaperBasisIndex
    (p : GHL2025.OneTermRobinParameters) (s j : Nat) : Nat :=
  let odPure := p.n - clog2 p.kappa
  (s <<< (1 + p.n + odPure)) + (j <<< 1)

/--
Layout contract for the next gamma3 path attempt at `n = 3`.

Eq. `ROBIN clarified` places the clean `gamma3` basis states for system entry
`(2, 5)` at full indices `(4, 10)` when the sparse slot is `0`.  The existing
`signalSystemBlockProjection` convention instead selects full indices `(2, 5)`.

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route gamma 3 paper basis layout n 3”; its local proof does not by itself complete the broader paper route. Layout contract for the next gamma3 path attempt at 'n = 3'.

theorem oneTermRobinBlockEncodingProofRoute_gamma3PaperBasisLayout_n3 :
    let p := oneTermParameters 3
    let sysRow : Fin (gridSize 3) := ⟨2, by native_decide⟩
    let sysCol : Fin (gridSize 3) := ⟨5, by native_decide⟩
    let projectedRow :=
      signalSystemBlockRowIndex (gridSize 3)
        (oneTermRobinFiniteBlockCompositionContract 3).expectedTarget.signalIndex.val
        sysRow.val
    let projectedCol :=
      signalSystemBlockColIndex (gridSize 3)
        (oneTermRobinFiniteBlockCompositionContract 3).expectedTarget.signalIndex.val

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route gamma 3 paper basis path audit n 3”; its local proof does not by itself complete the broader paper route. Focused Fig.

theorem oneTermRobinBlockEncodingProofRoute_gamma3PaperBasisPathAudit_n3 :
    let p := oneTermParameters 3
    let fullDim := qubitDim (GHL2025.oneTermRobinTotalQubits p)
    let row4 : Fin fullDim := ⟨4, by native_decide⟩
    let row198 : Fin fullDim := ⟨198, by native_decide⟩
    let col10 : Fin fullDim := ⟨10, by native_decide⟩
    let col138 : Fin fullDim := ⟨138, by native_decide⟩
    let col139 : Fin fullDim := ⟨139, by native_decide⟩
    let col186 : Fin fullDim := ⟨186, by native_decide⟩
    let col187 : Fin fullDim := ⟨187, by native_decide⟩
    let col214 : Fin fullDim := ⟨214, by native_decide⟩

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route gamma 3 sparse slot alignment n 3”; its local proof does not by itself complete the broader paper route. Sparse-slot alignment audit for the focused 'n = 3' gamma3 coefficient 'D_{2,5}'.

theorem oneTermRobinBlockEncodingProofRoute_gamma3SparseSlotAlignment_n3 :
    let p := oneTermParameters 3
    let fullDim := qubitDim (GHL2025.oneTermRobinTotalQubits p)
    let slot0Col := oneTermRobinGamma3PaperBasisIndex p 0 5
    let slot5Row := oneTermRobinGamma3PaperBasisIndex p 5 2
    let slot5Col := oneTermRobinGamma3PaperBasisIndex p 5 5
    let slot5Image := GHL2025.bandedSparseAccessPaperImage p slot5Col
    let row4 : Fin fullDim := ⟨4, by native_decide⟩
    let col214 : Fin fullDim := ⟨214, by native_decide⟩
    GHL2025.oneTermRobinGlobalSparseOffset 3 0 = 6 ∧
      GHL2025.oneTermRobinGlobalSparseAddress 3 0 5 = 3 ∧

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 projection slot convention obligation”. Source-contract obligation for the gamma3 projection-slot convention.

def oneTermRobinGamma3ProjectionSlotConventionObligation
    (n : Nat) (_i _j : Fin (gridSize n)) : SemanticObligation where
  description :=
    "gamma3 projection-slot convention: relate the slot-specific clean branch with r_{s,j}=i to the theorem-level signal-zero block projection or sparse-register summation before applying the seven-gate product equality"
  source :=
    "GHL2025 Eq. ROBIN clarified gamma3 line, Theorem one-term block-encoding, Fig. 1-term ROBIN, Definition def:block-encoding, Lemma Banded-sparse-access-oracle"
  proved := false

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 projection slot convention obligation transcript”; its local proof does not by itself complete the broader paper route.

theorem oneTermRobinGamma3ProjectionSlotConventionObligation_transcript
    (n : Nat) (i j : Fin (gridSize n)) :
    (oneTermRobinGamma3ProjectionSlotConventionObligation n i j).source =
        "GHL2025 Eq. ROBIN clarified gamma3 line, Theorem one-term block-encoding, Fig. 1-term ROBIN, Definition def:block-encoding, Lemma Banded-sparse-access-oracle" ∧
      (oneTermRobinGamma3ProjectionSlotConventionObligation n i j).proved =
        false := by

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route gamma 3 projection slot convention map n 3”; its local proof does not by itself complete the broader paper route. Focused projection-slot contract map for the compiled 'n = 3' gamma3 audit.

theorem oneTermRobinBlockEncodingProofRoute_gamma3ProjectionSlotConventionMap_n3 :
    let p := oneTermParameters 3
    let sysRow : Fin (gridSize 3) := ⟨2, by native_decide⟩
    let sysCol : Fin (gridSize 3) := ⟨5, by native_decide⟩
    let projectionObligation :=
      oneTermRobinGamma3ProjectionSlotConventionObligation 3 sysRow sysCol
    let productObligation :=
      oneTermRobinGamma3ProductToCoefficientObligation 3 sysRow sysCol
    let projectedRow :=
      signalSystemBlockRowIndex (gridSize 3)
        (oneTermRobinFiniteBlockCompositionContract 3).expectedTarget.signalIndex.val

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route gamma 3 slot 5 path audit n 3”; its local proof does not by itself complete the broader paper route. Focused Fig.

theorem oneTermRobinBlockEncodingProofRoute_gamma3Slot5PathAudit_n3 :
    let p := oneTermParameters 3
    let fullDim := qubitDim (GHL2025.oneTermRobinTotalQubits p)
    let sysRow : Fin (gridSize 3) := ⟨2, by native_decide⟩
    let sysCol : Fin (gridSize 3) := ⟨5, by native_decide⟩
    let slot5Row := oneTermRobinGamma3PaperBasisIndex p 5 sysRow.val
    let slot5Col := oneTermRobinGamma3PaperBasisIndex p 5 sysCol.val
    let afterIndic := GHL2025.indicatorOracleImage p slot5Col
    let odtsKetOne := afterIndic + 1
    let afterOdbsKetZero := GHL2025.bandedSparseAccessPaperImage p afterIndic
    let afterOdbsKetOne := GHL2025.bandedSparseAccessPaperImage p odtsKetOne

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 slot 5 projection register audit check n 3”. Executable field check for the slot-'5' gamma3 projection/register audit.

def oneTermRobinGamma3Slot5ProjectionRegisterAuditCheck_n3 : Bool :=
  let p := oneTermParameters 3
  let fullDim := qubitDim (GHL2025.oneTermRobinTotalQubits p)
  let slot5Row := oneTermRobinGamma3PaperBasisIndex p 5 2
  let slot5Col := oneTermRobinGamma3PaperBasisIndex p 5 5
  let afterIndic := GHL2025.indicatorOracleImage p slot5Col
  let afterOdbs := GHL2025.bandedSparseAccessPaperImage p afterIndic
  let afterSwap := GHL2025.swapOracleImage p afterOdbs
  let daggerEndpoint :=
    GHL2025.bandedSparseAccessPaperPostSwapPreimageCandidate p afterIndic
  let row84 : Fin fullDim := ⟨84, by native_decide⟩

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route gamma 3 slot 5 projection register audit n 3”; its local proof does not by itself complete the broader paper route. Projection/register audit for the slot-'5' gamma3 path at 'n = 3'.

theorem oneTermRobinBlockEncodingProofRoute_gamma3Slot5ProjectionRegisterAudit_n3 :
    oneTermRobinGamma3Slot5ProjectionRegisterAuditCheck_n3 = true ∧
      (oneTermRobinGamma3ProjectionSlotConventionObligation
          3 ⟨2, by native_decide⟩ ⟨5, by native_decide⟩).proved =
        false ∧
      (oneTermRobinGamma3ProductToCoefficientObligation
          3 ⟨2, by native_decide⟩ ⟨5, by native_decide⟩).proved =
        false ∧
      (oneTermRobinBlockEncodingProofRoute 3).oracleComposition.lcuCorrect.proved =
        false ∧
      (oneTermRobinBlockEncodingProofRoute 3).blockClaim.target.blockProjection.proved =

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 projection register convention decision”. A proposition-valued field is a requirement until a constructor supplies it. Middle-agent decision record for the blocked gamma3 projection/register convention at 'n = 3'.

structure OneTermRobinGamma3ProjectionRegisterConventionDecision where
  sourceAnchor : String
  cleanEndpoint : Nat
  fullEndpoint : Nat
  firstMismatch : String
  secondaryMismatch : String
  classification : String
  requiredDecision : SemanticObligation
  auditCheck : Bool
  productSearchBlocked : Bool
  projectionSlotConventionProved : Bool

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 projection register convention decision n 3”. The focused gamma3 endpoint mismatch is a source-contract gap, not a finite matrix multiplication target.

def oneTermRobinGamma3ProjectionRegisterConventionDecision_n3 :
    OneTermRobinGamma3ProjectionRegisterConventionDecision where
  sourceAnchor :=
    "GHL2025 Theorem one-term block-encoding, Eq. ROBIN clarified, Fig. 1-term ROBIN, Definition def:block-encoding, arXiv:2506.20478"
  cleanEndpoint := 84
  fullEndpoint := 228
  firstMismatch := "indicator bit: full endpoint has 1, clean endpoint has 0"
  secondaryMismatch := "sparse-index value: full endpoint has 6, clean endpoint has 5"
  classification := "source-contract-gap plus internal-paper-step"
  requiredDecision := {
    description :=

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 projection register convention decision n 3 transcript”; its local proof does not by itself complete the broader paper route. Transcript theorem for the middle decision record.

theorem oneTermRobinGamma3ProjectionRegisterConventionDecision_n3_transcript :
    let decision := oneTermRobinGamma3ProjectionRegisterConventionDecision_n3
    decision.auditCheck = true ∧
      decision.cleanEndpoint = 84 ∧
      decision.fullEndpoint = 228 ∧
      decision.firstMismatch =
        "indicator bit: full endpoint has 1, clean endpoint has 0" ∧
      decision.secondaryMismatch =
        "sparse-index value: full endpoint has 6, clean endpoint has 5" ∧
      decision.classification =
        "source-contract-gap plus internal-paper-step" ∧

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 sparse register summation convention”. A proposition-valued field is a requirement until a constructor supplies it. Chosen theorem-facing convention for the focused 'n = 3' gamma3 entry.

structure OneTermRobinGamma3SparseRegisterSummationConvention where
  sourceAnchor : String
  chosenConvention : String
  summedSlotRange : String
  cleanEndpoint : Nat
  fullEndpoint : Nat
  cleanSystemRow : Nat
  fullSystemRow : Nat
  cleanIndicator : Nat
  fullIndicator : Nat
  cleanSparseIndex : Nat

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 sparse register summation convention n 3”. Sparse-register summation convention selected for the slot-'5' gamma3 audit.

def oneTermRobinGamma3SparseRegisterSummationConvention_n3 :
    OneTermRobinGamma3SparseRegisterSummationConvention :=
  let p := oneTermParameters 3
  let sysRow : Fin (gridSize 3) := ⟨2, by native_decide⟩
  let sysCol : Fin (gridSize 3) := ⟨5, by native_decide⟩
  let cleanEndpoint := oneTermRobinGamma3PaperBasisIndex p 5 sysRow.val
  let cleanColumn := oneTermRobinGamma3PaperBasisIndex p 5 sysCol.val
  let fullEndpoint :=
    GHL2025.bandedSparseAccessPaperPostSwapPreimageCandidate p
      (GHL2025.indicatorOracleImage p cleanColumn)
  {

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 sparse register summation convention n 3 transcript”; its local proof does not by itself complete the broader paper route. Transcript theorem for the selected sparse-register summation convention.

theorem oneTermRobinGamma3SparseRegisterSummationConvention_n3_transcript :
    let convention :=
      oneTermRobinGamma3SparseRegisterSummationConvention_n3
    convention.chosenConvention = "sparse-register summation" ∧
      convention.summedSlotRange = "s = 0..kappa-1" ∧
      convention.sparseRegisterSummationSelected = true ∧
      convention.auditCheck = true ∧
      convention.cleanEndpoint = 84 ∧
      convention.fullEndpoint = 228 ∧
      convention.cleanSystemRow = 2 ∧
      convention.fullSystemRow = 2 ∧

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 sparse register summation indicator gap n 3”; its local proof does not by itself complete the broader paper route. Indicator-field gap after selecting sparse-register summation.

theorem oneTermRobinGamma3SparseRegisterSummation_indicatorGap_n3 :
    let convention :=
      oneTermRobinGamma3SparseRegisterSummationConvention_n3
    convention.chosenConvention = "sparse-register summation" ∧
      convention.indicatorMismatchHandledBySummation = false ∧
      convention.indicatorMismatchObligation.description =
        "indicator-bit mismatch between full endpoint 228 and clean endpoint 84 must be handled by a separate projection/register convention; sparse-register summation alone does not close it" ∧
      convention.indicatorMismatchObligation.source =
        "GHL2025 Eq. ROBIN clarified, Fig. 1-term ROBIN; QBE slot-5 projection/register audit" ∧
      convention.indicatorMismatchObligation.proved = false ∧
      convention.cleanEndpoint = 84 ∧

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 indicator projection convention”. A proposition-valued field is a requirement until a constructor supplies it. Indicator-field projection/register convention for the focused 'n = 3' gamma3 endpoint pair.

structure OneTermRobinGamma3IndicatorProjectionConvention where
  sourceAnchor : String
  cleanEndpoint : Nat
  fullEndpoint : Nat
  cleanIndicator : Nat
  fullIndicator : Nat
  indicatorRelationSpecifiedBySource : Bool
  humanInputRequired : Bool
  requiredConvention : String
  conventionObligation : SemanticObligation
  sparseSummationConvention : OneTermRobinGamma3SparseRegisterSummationConvention

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 indicator projection convention n 3”. The active gamma3 indicator convention is still an explicit source-contract gap.

def oneTermRobinGamma3IndicatorProjectionConvention_n3 :
    OneTermRobinGamma3IndicatorProjectionConvention :=
  let sparseConvention :=
    oneTermRobinGamma3SparseRegisterSummationConvention_n3
  {
    sourceAnchor :=
      "GHL2025 Eq. ROBIN clarified, Fig. 1-term ROBIN, Definition def:block-encoding, arXiv:2506.20478"
    cleanEndpoint := sparseConvention.cleanEndpoint
    fullEndpoint := sparseConvention.fullEndpoint
    cleanIndicator := sparseConvention.cleanIndicator
    fullIndicator := sparseConvention.fullIndicator

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 indicator projection convention n 3 transcript”; its local proof does not by itself complete the broader paper route. Transcript theorem for the active gamma3 indicator convention.

theorem oneTermRobinGamma3IndicatorProjectionConvention_n3_transcript :
    let convention :=
      oneTermRobinGamma3IndicatorProjectionConvention_n3
    convention.cleanEndpoint = 84 ∧
      convention.fullEndpoint = 228 ∧
      convention.cleanIndicator = 0 ∧
      convention.fullIndicator = 1 ∧
      convention.cleanIndicator ≠ convention.fullIndicator ∧
      convention.indicatorRelationSpecifiedBySource = false ∧
      convention.humanInputRequired = true ∧
      convention.requiredConvention =

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 bulk indicator source audit”. A proposition-valued field is a requirement until a constructor supplies it. Focused source audit for the bulk-indicator field in the 'n = 3' gamma3 endpoint pair.

structure OneTermRobinGamma3BulkIndicatorSourceAudit where
  sourceAnchor : String
  focusedSystemColumn : Nat
  K1 : Nat
  K2 : Nat
  isBulkColumn : Bool
  cleanEndpoint : Nat
  fullEndpoint : Nat
  cleanIndicator : Nat
  fullIndicator : Nat
  sourceBulkIndicator : Nat

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 bulk indicator source audit n 3”. Source-backed refinement of the active indicator convention blocker.

def oneTermRobinGamma3BulkIndicatorSourceAudit_n3 :
    OneTermRobinGamma3BulkIndicatorSourceAudit :=
  let p := oneTermParameters 3
  let convention := oneTermRobinGamma3IndicatorProjectionConvention_n3
  {
    sourceAnchor :=
      "GHL2025 U_indic paragraph, Eq. ROBIN clarified, Fig. 1-term ROBIN, Definition def:block-encoding, arXiv:2506.20478"
    focusedSystemColumn := 5
    K1 := 2
    K2 := gridSize p.n - 3
    isBulkColumn := GHL2025.isBulkRow 2 (gridSize p.n - 3) 5

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 bulk indicator source audit n 3 transcript”; its local proof does not by itself complete the broader paper route. Transcript theorem for the bulk-indicator source audit.

theorem oneTermRobinGamma3BulkIndicatorSourceAudit_n3_transcript :
    let p := oneTermParameters 3
    let audit := oneTermRobinGamma3BulkIndicatorSourceAudit_n3
    audit.focusedSystemColumn = 5 ∧
      audit.K1 = 2 ∧
      audit.K2 = 5 ∧
      audit.isBulkColumn = true ∧
      GHL2025.isBulkRow audit.K1 audit.K2 audit.focusedSystemColumn = true ∧
      GHL2025.indicatorOracleImage p
          (oneTermRobinGamma3PaperBasisIndex p 5 audit.focusedSystemColumn) =
        218 ∧

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 branch correct source map”. A proposition-valued field is a requirement until a constructor supplies it. Branch-correct source map for the focused 'n = 3' gamma3 transcript.

structure OneTermRobinGamma3BranchCorrectSourceMap where
  sourceAnchor : String
  K1 : Nat
  K2 : Nat
  boundaryColumn : Nat
  boundaryColumnIsBoundary : Bool
  boundaryColumnIsBulk : Bool
  boundaryEndpoint : Nat
  boundaryAfterIndic : Nat
  boundaryIndicator : Nat
  boundaryBranchIsDisplayed : Bool

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 branch correct source map n 3”. Compiled branch-correct gamma3 transcript for 'n = 3'.

def oneTermRobinGamma3BranchCorrectSourceMap_n3 :
    OneTermRobinGamma3BranchCorrectSourceMap :=
  let p := oneTermParameters 3
  let boundaryRow : Fin (gridSize 3) := ⟨0, by native_decide⟩
  let boundaryCol : Fin (gridSize 3) := ⟨0, by native_decide⟩
  let bulkRow : Fin (gridSize 3) := ⟨2, by native_decide⟩
  let bulkCol : Fin (gridSize 3) := ⟨5, by native_decide⟩
  let boundaryEndpoint := oneTermRobinGamma3PaperBasisIndex p 0 boundaryCol.val
  let boundaryAfterIndic := GHL2025.indicatorOracleImage p boundaryEndpoint
  let bulkAudit := oneTermRobinGamma3BulkIndicatorSourceAudit_n3
  {

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 branch correct source map n 3 transcript”; its local proof does not by itself complete the broader paper route. Transcript theorem for the branch-correct gamma3 source map.

theorem oneTermRobinGamma3BranchCorrectSourceMap_n3_transcript :
    let p := oneTermParameters 3
    let branch := oneTermRobinGamma3BranchCorrectSourceMap_n3
    branch.K1 = 2 ∧
      branch.K2 = 5 ∧
      branch.boundaryColumn = 0 ∧
      GHL2025.isBoundaryRow branch.K1 branch.K2 (gridSize p.n)
        branch.boundaryColumn = true ∧
      branch.boundaryColumnIsBoundary = true ∧
      GHL2025.isBulkRow branch.K1 branch.K2 branch.boundaryColumn = false ∧
      branch.boundaryColumnIsBulk = false ∧

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route gamma 3 boundary branch path audit n 3”; its local proof does not by itself complete the broader paper route. Boundary-focused path audit for the displayed gamma3 branch at 'n = 3'.

theorem oneTermRobinBlockEncodingProofRoute_gamma3BoundaryBranchPathAudit_n3 :
    let p := oneTermParameters 3
    let fullDim := qubitDim (GHL2025.oneTermRobinTotalQubits p)
    let branch := oneTermRobinGamma3BranchCorrectSourceMap_n3
    let sysRow : Fin (gridSize 3) := ⟨0, by native_decide⟩
    let sysCol : Fin (gridSize 3) := ⟨0, by native_decide⟩
    let slot0Col := oneTermRobinGamma3PaperBasisIndex p 0 sysCol.val
    let slot2Col := oneTermRobinGamma3PaperBasisIndex p 2 sysCol.val
    let slot2Row := oneTermRobinGamma3PaperBasisIndex p 2 sysRow.val
    let afterIndic := GHL2025.indicatorOracleImage p slot2Col
    let afterOdbs := GHL2025.bandedSparseAccessPaperImage p afterIndic

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 bulk product interface”. A proposition-valued field is a requirement until a constructor supplies it. Bulk-specific interface for the omitted gamma3 product branch.

structure OneTermRobinGamma3BulkProductInterface where
  sourceAnchor : String
  systemRow : Nat
  systemColumn : Nat
  sparseSlot : Nat
  K1 : Nat
  K2 : Nat
  bulkColumnIsBulk : Bool
  bulkBranchIsOmittedByDisplay : Bool
  fullEndpointUsed : Bool
  cleanBoundaryEndpointComparisonUsed : Bool

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin block encoding proof route gamma 3 bulk product to coefficient interface n 3”. Compiled product interface for the omitted bulk branch at 'n = 3', system entry '(2,5)', and global sparse slot '5'.

def oneTermRobinBlockEncodingProofRoute_gamma3BulkProductToCoefficientInterface_n3 :
    OneTermRobinGamma3BulkProductInterface :=
  let p := oneTermParameters 3
  let sysRow : Fin (gridSize 3) := ⟨2, by native_decide⟩
  let sysCol : Fin (gridSize 3) := ⟨5, by native_decide⟩
  let bulkAudit := oneTermRobinGamma3BulkIndicatorSourceAudit_n3
  let cleanSource := oneTermRobinGamma3PaperBasisIndex p 5 sysCol.val
  let afterIndic := GHL2025.indicatorOracleImage p cleanSource
  let afterOdtsKetOne := afterIndic + 1
  let afterOdbsKetZero := GHL2025.bandedSparseAccessPaperImage p afterIndic
  let afterOdbsKetOne := GHL2025.bandedSparseAccessPaperImage p afterOdtsKetOne

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route gamma 3 bulk product to coefficient interface n 3 transcript”; its local proof does not by itself complete the broader paper route. Transcript theorem for the omitted bulk product interface.

theorem oneTermRobinBlockEncodingProofRoute_gamma3BulkProductToCoefficientInterface_n3_transcript :
    let p := oneTermParameters 3
    let fullDim := qubitDim (GHL2025.oneTermRobinTotalQubits p)
    let interface :=
      oneTermRobinBlockEncodingProofRoute_gamma3BulkProductToCoefficientInterface_n3
    let sysRow : Fin (gridSize 3) := ⟨2, by native_decide⟩
    let sysCol : Fin (gridSize 3) := ⟨5, by native_decide⟩
    let row90 : Fin fullDim := ⟨90, by native_decide⟩
    let row170 : Fin fullDim := ⟨170, by native_decide⟩
    let row171 : Fin fullDim := ⟨171, by native_decide⟩
    let row212 : Fin fullDim := ⟨212, by native_decide⟩

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 boundary product interface”. A proposition-valued field is a requirement until a constructor supplies it. Boundary-specific interface for the next gamma3 product theorem.

structure OneTermRobinGamma3BoundaryProductInterface where
  sourceAnchor : String
  systemRow : Nat
  systemColumn : Nat
  sparseSlot : Nat
  cleanSource : Nat
  afterIndic : Nat
  afterOdtsKetZero : Nat
  afterRyKetZero : Nat
  afterRyKetOne : Nat
  afterOdbsKetZero : Nat

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin block encoding proof route gamma 3 boundary product to coefficient interface n 3”. Compiled boundary product interface for the 'n = 3', '(0,0)', sparse-slot-'2' gamma3 packet.

def oneTermRobinBlockEncodingProofRoute_gamma3BoundaryProductToCoefficientInterface_n3 :
    OneTermRobinGamma3BoundaryProductInterface :=
  let p := oneTermParameters 3
  let sysRow : Fin (gridSize 3) := ⟨0, by native_decide⟩
  let sysCol : Fin (gridSize 3) := ⟨0, by native_decide⟩
  let cleanSource := oneTermRobinGamma3PaperBasisIndex p 2 sysCol.val
  let afterIndic := GHL2025.indicatorOracleImage p cleanSource
  let afterOdbsKetZero := GHL2025.bandedSparseAccessPaperImage p afterIndic
  let afterOdbsKetOne := GHL2025.bandedSparseAccessPaperImage p (afterIndic + 1)
  let afterSwapKetZero := GHL2025.swapOracleImage p afterOdbsKetZero
  let afterSwapKetOne := GHL2025.swapOracleImage p afterOdbsKetOne

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route gamma 3 boundary product to coefficient interface n 3 transcript”; its local proof does not by itself complete the broader paper route. Transcript theorem for the boundary product interface.

theorem oneTermRobinBlockEncodingProofRoute_gamma3BoundaryProductToCoefficientInterface_n3_transcript :
    let p := oneTermParameters 3
    let fullDim := qubitDim (GHL2025.oneTermRobinTotalQubits p)
    let interface :=
      oneTermRobinBlockEncodingProofRoute_gamma3BoundaryProductToCoefficientInterface_n3
    let sysRow : Fin (gridSize 3) := ⟨0, by native_decide⟩
    let sysCol : Fin (gridSize 3) := ⟨0, by native_decide⟩
    let row0 : Fin fullDim := ⟨0, by native_decide⟩
    let row1 : Fin fullDim := ⟨1, by native_decide⟩
    let row32 : Fin fullDim := ⟨32, by native_decide⟩
    let row33 : Fin fullDim := ⟨33, by native_decide⟩

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 boundary unique path support audit”. A proposition-valued field is a requirement until a constructor supplies it. Boundary unique-path support audit for the displayed 'n = 3' gamma3 branch.

structure OneTermRobinGamma3BoundaryUniquePathSupportAudit where
  sourceAnchor : String
  systemRow : Nat
  systemColumn : Nat
  sparseSlot : Nat
  sourceColumn : Nat
  targetRow : Nat
  survivingKetZeroPath : List Nat
  adjacentKetOnePath : List Nat
  odtsKetOneProbeEntry : Coeff
  adjacentOfTargetEntry : Coeff

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin block encoding proof route gamma 3 boundary unique path support audit n 3”. Compiled audit for the first boundary unique-path support packet.

def oneTermRobinBlockEncodingProofRoute_gamma3BoundaryUniquePathSupportAudit_n3 :
    OneTermRobinGamma3BoundaryUniquePathSupportAudit :=
  let p := oneTermParameters 3
  let fullDim := qubitDim (GHL2025.oneTermRobinTotalQubits p)
  let interface :=
    oneTermRobinBlockEncodingProofRoute_gamma3BoundaryProductToCoefficientInterface_n3
  let row0 : Fin fullDim := ⟨0, by native_decide⟩
  let row1 : Fin fullDim := ⟨1, by native_decide⟩
  let row32 : Fin fullDim := ⟨32, by native_decide⟩
  let row33 : Fin fullDim := ⟨33, by native_decide⟩
  {

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route gamma 3 boundary unique path support n 3”; its local proof does not by itself complete the broader paper route. First boundary unique-path support result.

theorem oneTermRobinBlockEncodingProofRoute_gamma3BoundaryUniquePathSupport_n3 :
    let p := oneTermParameters 3
    let fullDim := qubitDim (GHL2025.oneTermRobinTotalQubits p)
    let audit :=
      oneTermRobinBlockEncodingProofRoute_gamma3BoundaryUniquePathSupportAudit_n3
    let row0 : Fin fullDim := ⟨0, by native_decide⟩
    let row1 : Fin fullDim := ⟨1, by native_decide⟩
    let row32 : Fin fullDim := ⟨32, by native_decide⟩
    let row33 : Fin fullDim := ⟨33, by native_decide⟩
    audit.systemRow = 0 ∧
      audit.systemColumn = 0 ∧

commit-pinned source · Verso Blueprint panel

This abbreviation gives a shorter name to the type or expression used for “one term robin gamma 3 boundary prefix parameters n 3”. Parameters for the focused 'n = 3' displayed-boundary gamma3 prefix packet.

abbrev oneTermRobinGamma3BoundaryPrefixParameters_n3 :
    GHL2025.OneTermRobinParameters :=
  oneTermParameters 3

/-- Full matrix dimension for the focused boundary gamma3 prefix packet. -/

commit-pinned source · Verso Blueprint panel

This abbreviation gives a shorter name to the type or expression used for “one term robin gamma 3 boundary prefix dim n 3”. Full matrix dimension for the focused boundary gamma3 prefix packet.

abbrev oneTermRobinGamma3BoundaryPrefixDim_n3 : Nat :=
  qubitDim (GHL2025.oneTermRobinTotalQubits
    oneTermRobinGamma3BoundaryPrefixParameters_n3)

/-- Full source column `32` for the focused boundary gamma3 prefix packet. -/

commit-pinned source · Verso Blueprint panel

This abbreviation gives a shorter name to the type or expression used for “one term robin gamma 3 boundary prefix source n 3”. Full source column '32' for the focused boundary gamma3 prefix packet.

abbrev oneTermRobinGamma3BoundaryPrefixSource_n3 :
    Fin oneTermRobinGamma3BoundaryPrefixDim_n3 :=
  ⟨32, by native_decide⟩

/-- Prefix row `0`, the ket-zero image after the forward `O_D^BS` gate. -/

commit-pinned source · Verso Blueprint panel

This abbreviation gives a shorter name to the type or expression used for “one term robin gamma 3 boundary prefix row 0 n 3”. Prefix row '0', the ket-zero image after the forward 'O_D^BS' gate.

abbrev oneTermRobinGamma3BoundaryPrefixRow0_n3 :
    Fin oneTermRobinGamma3BoundaryPrefixDim_n3 :=
  ⟨0, by native_decide⟩

/-- Prefix row `1`, the adjacent ket-one image after the forward `O_D^BS` gate. -/

commit-pinned source · Verso Blueprint panel

This abbreviation gives a shorter name to the type or expression used for “one term robin gamma 3 boundary prefix row 1 n 3”. Prefix row '1', the adjacent ket-one image after the forward 'O_D^BS' gate.

abbrev oneTermRobinGamma3BoundaryPrefixRow1_n3 :
    Fin oneTermRobinGamma3BoundaryPrefixDim_n3 :=
  ⟨1, by native_decide⟩

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary du prefix matrix n 3”. Two-gate prefix 'O_DT^S * U_indic' for the displayed-boundary gamma3 packet.

def oneTermRobinGamma3BoundaryDUPrefixMatrix_n3 :
    Matrix oneTermRobinGamma3BoundaryPrefixDim_n3
      oneTermRobinGamma3BoundaryPrefixDim_n3 Coeff :=
  let p := oneTermRobinGamma3BoundaryPrefixParameters_n3
  Matrix.mul (GHL2025.sparseAmplitudeOracleDTRotationMatrix p)
    (GHL2025.indicatorOracleMatrix p)

/-- Three-gate prefix `Ry_boundary * O_DT^S * U_indic`. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary rdu prefix matrix n 3”. Three-gate prefix 'Ry_boundary * O_DT^S * U_indic'.

def oneTermRobinGamma3BoundaryRDUPrefixMatrix_n3 :
    Matrix oneTermRobinGamma3BoundaryPrefixDim_n3
      oneTermRobinGamma3BoundaryPrefixDim_n3 Coeff :=
  let p := oneTermRobinGamma3BoundaryPrefixParameters_n3
  Matrix.mul (GHL2025.boundaryRotationMatrix p)
    oneTermRobinGamma3BoundaryDUPrefixMatrix_n3

/-- Four-gate prefix `O_D^BS * Ry_boundary * O_DT^S * U_indic`. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary prefix matrix n 3”. Four-gate prefix 'O_D^BS * Ry_boundary * O_DT^S * U_indic'.

def oneTermRobinGamma3BoundaryPrefixMatrix_n3 :
    Matrix oneTermRobinGamma3BoundaryPrefixDim_n3
      oneTermRobinGamma3BoundaryPrefixDim_n3 Coeff :=
  let p := oneTermRobinGamma3BoundaryPrefixParameters_n3
  Matrix.mul (GHL2025.bandedSparseAccessPaperMatrix p)
    oneTermRobinGamma3BoundaryRDUPrefixMatrix_n3

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary du prefix support n 3”; its local proof does not by itself complete the broader paper route. The two-gate boundary prefix has no evaluated support away from source column '32'.

theorem oneTermRobinGamma3BoundaryDUPrefixSupport_n3
    (env : String → Rat)
    (i : Fin oneTermRobinGamma3BoundaryPrefixDim_n3)
    (hi : i ≠ oneTermRobinGamma3BoundaryPrefixSource_n3) :
    Coeff.evalWith env
      (oneTermRobinGamma3BoundaryDUPrefixMatrix_n3
        i oneTermRobinGamma3BoundaryPrefixSource_n3) = 0 := by

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary rdu prefix support n 3”; its local proof does not by itself complete the broader paper route. The three-gate boundary prefix has evaluated support only in rows '32' and '33'.

theorem oneTermRobinGamma3BoundaryRDUPrefixSupport_n3
    (env : String → Rat)
    (i : Fin oneTermRobinGamma3BoundaryPrefixDim_n3)
    (hi32 : i ≠ oneTermRobinGamma3BoundaryPrefixSource_n3)
    (hi33 : i ≠ oneTermRobinGamma3BoundaryPrefixRow33_n3) :
    Coeff.evalWith env
      (oneTermRobinGamma3BoundaryRDUPrefixMatrix_n3
        i oneTermRobinGamma3BoundaryPrefixSource_n3) = 0 := by

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route gamma 3 boundary prefix support n 3”; its local proof does not by itself complete the broader paper route. Boundary prefix support for the displayed gamma3 branch at 'n = 3'.

theorem oneTermRobinBlockEncodingProofRoute_gamma3BoundaryPrefixSupport_n3
    (env : String → Rat)
    (i : Fin oneTermRobinGamma3BoundaryPrefixDim_n3)
    (hi0 : i ≠ oneTermRobinGamma3BoundaryPrefixRow0_n3)
    (hi1 : i ≠ oneTermRobinGamma3BoundaryPrefixRow1_n3) :
    Coeff.evalWith env
      (oneTermRobinGamma3BoundaryPrefixMatrix_n3
        i oneTermRobinGamma3BoundaryPrefixSource_n3) = 0 := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary of swap matrix n 3”. Two-gate suffix 'SWAP * O_f' for the displayed-boundary gamma3 packet.

def oneTermRobinGamma3BoundaryOfSwapMatrix_n3 :
    Matrix oneTermRobinGamma3BoundaryPrefixDim_n3
      oneTermRobinGamma3BoundaryPrefixDim_n3 Coeff :=
  let p := oneTermRobinGamma3BoundaryPrefixParameters_n3
  Matrix.mul (GHL2025.swapOracleMatrix p) (GHL2025.functionOraclePaperMatrix p)

/-- Three-gate suffix `(O_D^BS)^† * SWAP * O_f`. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary suffix matrix n 3”. Three-gate suffix '(O_D^BS)^† * SWAP * O_f'.

def oneTermRobinGamma3BoundarySuffixMatrix_n3 :
    Matrix oneTermRobinGamma3BoundaryPrefixDim_n3
      oneTermRobinGamma3BoundaryPrefixDim_n3 Coeff :=
  let p := oneTermRobinGamma3BoundaryPrefixParameters_n3
  Matrix.mul (GHL2025.bandedSparseAccessPaperDaggerMatrix p)
    oneTermRobinGamma3BoundaryOfSwapMatrix_n3

/--
Full seven-gate matrix for the focused displayed-boundary gamma3 packet.

This is only the finite matrix product for the branch-correct `n = 3`,

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary seven gate matrix n 3”. Full seven-gate matrix for the focused displayed-boundary gamma3 packet.

def oneTermRobinGamma3BoundarySevenGateMatrix_n3 :
    Matrix oneTermRobinGamma3BoundaryPrefixDim_n3
      oneTermRobinGamma3BoundaryPrefixDim_n3 Coeff :=
  Matrix.mul oneTermRobinGamma3BoundarySuffixMatrix_n3
    oneTermRobinGamma3BoundaryPrefixMatrix_n3

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary of swap row 0 col 1 zero n 3”; its local proof does not by itself complete the broader paper route. After 'O_f' and 'SWAP', the adjacent ket-one column has no evaluated support at row '0'.

theorem oneTermRobinGamma3BoundaryOfSwapRow0Col1_zero_n3
    (env : String → Rat) :
    Coeff.evalWith env
      (oneTermRobinGamma3BoundaryOfSwapMatrix_n3
        oneTermRobinGamma3BoundaryPrefixRow0_n3
        oneTermRobinGamma3BoundaryPrefixRow1_n3) = 0 := by

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary suffix row 32 col 1 zero n 3”; its local proof does not by itself complete the broader paper route. The suffix '(O_D^BS)^† * SWAP * O_f' kills the adjacent row-'1' branch when the target row is the boundary row '32'.

theorem oneTermRobinGamma3BoundarySuffixRow32Col1_zero_n3
    (env : String → Rat) :
    Coeff.evalWith env
      (oneTermRobinGamma3BoundarySuffixMatrix_n3
        oneTermRobinGamma3BoundaryPrefixSource_n3
        oneTermRobinGamma3BoundaryPrefixRow1_n3) = 0 := by

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route gamma 3 boundary seven gate support n 3”; its local proof does not by itself complete the broader paper route. Seven-gate support for the displayed 'n = 3' gamma3 boundary branch.

theorem oneTermRobinBlockEncodingProofRoute_gamma3BoundarySevenGateSupport_n3
    (env : String → Rat)
    (q : Fin oneTermRobinGamma3BoundaryPrefixDim_n3)
    (hq0 : q ≠ oneTermRobinGamma3BoundaryPrefixRow0_n3) :
    Coeff.evalWith env
        (oneTermRobinGamma3BoundarySuffixMatrix_n3
          oneTermRobinGamma3BoundaryPrefixSource_n3 q) *
      Coeff.evalWith env
        (oneTermRobinGamma3BoundaryPrefixMatrix_n3 q
          oneTermRobinGamma3BoundaryPrefixSource_n3) = 0 := by

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route gamma 3 boundary seven gate unique path n 3”; its local proof does not by itself complete the broader paper route. One-step unique-path reduction for the focused seven-gate boundary entry.

theorem oneTermRobinBlockEncodingProofRoute_gamma3BoundarySevenGateUniquePath_n3
    (env : String → Rat) :
    Coeff.evalWith env
      (oneTermRobinGamma3BoundarySevenGateMatrix_n3
        oneTermRobinGamma3BoundaryPrefixSource_n3
        oneTermRobinGamma3BoundaryPrefixSource_n3) =
      Coeff.evalWith env
        (oneTermRobinGamma3BoundarySuffixMatrix_n3
          oneTermRobinGamma3BoundaryPrefixSource_n3
          oneTermRobinGamma3BoundaryPrefixRow0_n3) *
      Coeff.evalWith env

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary du prefix entry eval n 3”; its local proof does not by itself complete the broader paper route. The two-gate 'O_DT^S * U_indic' prefix contributes unit amplitude on the boundary source column '32'.

theorem oneTermRobinGamma3BoundaryDUPrefixEntryEval_n3
    (env : String → Rat) :
    Coeff.evalWith env
      (oneTermRobinGamma3BoundaryDUPrefixMatrix_n3
        oneTermRobinGamma3BoundaryPrefixSource_n3
        oneTermRobinGamma3BoundaryPrefixSource_n3) = 1 := by

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary rdu prefix entry eval n 3”; its local proof does not by itself complete the broader paper route. The three-gate 'Ry_boundary * O_DT^S * U_indic' prefix contributes the boundary half-angle cosine on source column '32'.

theorem oneTermRobinGamma3BoundaryRDUPrefixEntryEval_n3
    (env : String → Rat) :
    Coeff.evalWith env
      (oneTermRobinGamma3BoundaryRDUPrefixMatrix_n3
        oneTermRobinGamma3BoundaryPrefixSource_n3
        oneTermRobinGamma3BoundaryPrefixSource_n3) =
      env "boundary_cos_half_0_2" := by

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary prefix entry eval n 3”; its local proof does not by itself complete the broader paper route. The four-gate prefix entry from source column '32' to row '0' is the boundary half-angle cosine.

theorem oneTermRobinGamma3BoundaryPrefixEntryEval_n3
    (env : String → Rat) :
    Coeff.evalWith env
      (oneTermRobinGamma3BoundaryPrefixMatrix_n3
        oneTermRobinGamma3BoundaryPrefixRow0_n3
        oneTermRobinGamma3BoundaryPrefixSource_n3) =
      env "boundary_cos_half_0_2" := by

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary of swap entry eval n 3”; its local proof does not by itself complete the broader paper route. The 'SWAP * O_f' suffix prefix on row/column '0' contributes the clean function-oracle amplitude 'f_3_0 * N_f_inv'.

theorem oneTermRobinGamma3BoundaryOfSwapEntryEval_n3
    (env : String → Rat) :
    Coeff.evalWith env
      (oneTermRobinGamma3BoundaryOfSwapMatrix_n3
        oneTermRobinGamma3BoundaryPrefixRow0_n3
        oneTermRobinGamma3BoundaryPrefixRow0_n3) =
      env "f_3_0" * env "N_f_inv" := by

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary suffix entry eval n 3”; its local proof does not by itself complete the broader paper route. The three-gate suffix entry from row '32' to the row-'0' intermediate state is the clean function-oracle amplitude.

theorem oneTermRobinGamma3BoundarySuffixEntryEval_n3
    (env : String → Rat) :
    Coeff.evalWith env
      (oneTermRobinGamma3BoundarySuffixMatrix_n3
        oneTermRobinGamma3BoundaryPrefixSource_n3
        oneTermRobinGamma3BoundaryPrefixRow0_n3) =
      env "f_3_0" * env "N_f_inv" := by

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route gamma 3 boundary product entry eval n 3”; its local proof does not by itself complete the broader paper route. Evaluated seven-gate product entry for the displayed boundary 'gamma3' packet.

theorem oneTermRobinBlockEncodingProofRoute_gamma3BoundaryProductEntryEval_n3
    (env : String → Rat) :
    Coeff.evalWith env
      (oneTermRobinGamma3BoundarySevenGateMatrix_n3
        oneTermRobinGamma3BoundaryPrefixSource_n3
        oneTermRobinGamma3BoundaryPrefixSource_n3) =
      (env "f_3_0" * env "N_f_inv") * env "boundary_cos_half_0_2" := by

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary du prefix col 0 support n 3”; its local proof does not by itself complete the broader paper route. Two-gate 'O_DT^S * U_indic' prefix support at column '0'.

theorem oneTermRobinGamma3BoundaryDUPrefixCol0Support_n3
    (env : String → Rat)
    (i : Fin oneTermRobinGamma3BoundaryPrefixDim_n3)
    (hi : i ≠ oneTermRobinGamma3BoundaryPrefixRow0_n3) :
    Coeff.evalWith env
      (oneTermRobinGamma3BoundaryDUPrefixMatrix_n3
        i oneTermRobinGamma3BoundaryPrefixRow0_n3) = 0 := by

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary rdu prefix col 0 support n 3”; its local proof does not by itself complete the broader paper route. Three-gate 'Ry * O_DT^S * U_indic' prefix support at column '0'.

theorem oneTermRobinGamma3BoundaryRDUPrefixCol0Support_n3
    (env : String → Rat)
    (i : Fin oneTermRobinGamma3BoundaryPrefixDim_n3)
    (hi0 : i ≠ oneTermRobinGamma3BoundaryPrefixRow0_n3)
    (hi1 : i ≠ oneTermRobinGamma3BoundaryPrefixRow1_n3) :
    Coeff.evalWith env
      (oneTermRobinGamma3BoundaryRDUPrefixMatrix_n3
        i oneTermRobinGamma3BoundaryPrefixRow0_n3) = 0 := by

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary prefix col 0 support n 3”; its local proof does not by itself complete the broader paper route. Four-gate prefix 'O_D^BS * Ry * O_DT^S * U_indic' support at column '0'.

theorem oneTermRobinGamma3BoundaryPrefixCol0Support_n3
    (env : String → Rat)
    (i : Fin oneTermRobinGamma3BoundaryPrefixDim_n3)
    (hi96 : i.val ≠ 96)
    (hi97 : i.val ≠ 97) :
    Coeff.evalWith env
      (oneTermRobinGamma3BoundaryPrefixMatrix_n3
        i oneTermRobinGamma3BoundaryPrefixRow0_n3) = 0 := by

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary du prefix col 0 entry eval n 3”; its local proof does not by itself complete the broader paper route. The two-gate prefix at column '0' contributes unit amplitude on row '0'.

theorem oneTermRobinGamma3BoundaryDUPrefixCol0EntryEval_n3
    (env : String → Rat) :
    Coeff.evalWith env
      (oneTermRobinGamma3BoundaryDUPrefixMatrix_n3
        oneTermRobinGamma3BoundaryPrefixRow0_n3
        oneTermRobinGamma3BoundaryPrefixRow0_n3) = 1 := by

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary rdu prefix row 0 col 0 eval n 3”; its local proof does not by itself complete the broader paper route. The three-gate column-'0' prefix row '0' is the slot-'0' boundary cosine entry.

theorem oneTermRobinGamma3BoundaryRDUPrefixRow0Col0_eval_n3
    (env : String → Rat) :
    Coeff.evalWith env
      (oneTermRobinGamma3BoundaryRDUPrefixMatrix_n3
        oneTermRobinGamma3BoundaryPrefixRow0_n3
        oneTermRobinGamma3BoundaryPrefixRow0_n3) =
      env "boundary_cos_half_0_0" := by

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary rdu prefix row 1 col 0 eval n 3”; its local proof does not by itself complete the broader paper route. The three-gate column-'0' prefix row '1' is the slot-'0' boundary sine entry.

theorem oneTermRobinGamma3BoundaryRDUPrefixRow1Col0_eval_n3
    (env : String → Rat) :
    Coeff.evalWith env
      (oneTermRobinGamma3BoundaryRDUPrefixMatrix_n3
        oneTermRobinGamma3BoundaryPrefixRow1_n3
        oneTermRobinGamma3BoundaryPrefixRow0_n3) =
      env "boundary_sin_half_0_0" := by

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary prefix row 96 col 0 eval n 3”; its local proof does not by itself complete the broader paper route. The four-gate prefix row '96', column '0' evaluates to the slot-'0' boundary cosine half-angle entry.

theorem oneTermRobinGamma3BoundaryPrefixRow96Col0_eval_n3
    (env : String → Rat) :
    Coeff.evalWith env
      (oneTermRobinGamma3BoundaryPrefixMatrix_n3
        (⟨96, by native_decide⟩ : Fin oneTermRobinGamma3BoundaryPrefixDim_n3)
        oneTermRobinGamma3BoundaryPrefixRow0_n3) =
      env "boundary_cos_half_0_0" := by

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary prefix row 97 col 0 eval n 3”; its local proof does not by itself complete the broader paper route. The four-gate prefix row '97', column '0' evaluates to the slot-'0' boundary sine half-angle entry.

theorem oneTermRobinGamma3BoundaryPrefixRow97Col0_eval_n3
    (env : String → Rat) :
    Coeff.evalWith env
      (oneTermRobinGamma3BoundaryPrefixMatrix_n3
        (⟨97, by native_decide⟩ : Fin oneTermRobinGamma3BoundaryPrefixDim_n3)
        oneTermRobinGamma3BoundaryPrefixRow0_n3) =
      env "boundary_sin_half_0_0" := by

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 boundary col 0 support analysis”. A proposition-valued field is a requirement until a constructor supplies it. QBE-AUTO-002 column-'0' support analysis record for the '[0,0]' entry.

structure OneTermRobinGamma3BoundaryCol0SupportAnalysis where
  sourceAnchor : String
  prefixColumn : Nat
  indicatorSupportRows : List Nat
  odtsSupportRows : List Nat
  duSupportRows : List Nat
  rySupportRows : List Nat
  rduSupportRows : List Nat
  odbsImage0 : Nat
  odbsImage1 : Nat
  prefixSupportRows : List Nat

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary col 0 support analysis n 3”. Compiled column-'0' support analysis for the '[0,0]' seven-gate entry.

def oneTermRobinGamma3BoundaryCol0SupportAnalysis_n3 :
    OneTermRobinGamma3BoundaryCol0SupportAnalysis where
  sourceAnchor :=
    "QBE-AUTO-002 column-0 support analysis for sevenGateMatrix[0,0]"
  prefixColumn := 0
  indicatorSupportRows := [0]
  odtsSupportRows := [0]
  duSupportRows := [0]
  rySupportRows := [0, 1]
  rduSupportRows := [0, 1]
  odbsImage0 := 96

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route gamma 3 boundary seven gate two path n 3”; its local proof does not by itself complete the broader paper route. Two-path reduction for the '[0,0]' entry of the seven-gate boundary matrix.

theorem oneTermRobinBlockEncodingProofRoute_gamma3BoundarySevenGateTwoPath_n3
    (env : String → Rat) :
    Coeff.evalWith env
        (oneTermRobinGamma3BoundarySevenGateMatrix_n3
          oneTermRobinGamma3BoundaryPrefixRow0_n3
          oneTermRobinGamma3BoundaryPrefixRow0_n3) =
      Coeff.evalWith env
        (oneTermRobinGamma3BoundarySuffixMatrix_n3
          oneTermRobinGamma3BoundaryPrefixRow0_n3
          (⟨96, by native_decide⟩ : Fin oneTermRobinGamma3BoundaryPrefixDim_n3)) *
      Coeff.evalWith env

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 boundary ry coefficient bridge”. A proposition-valued field is a requirement until a constructor supplies it. Focused false bridge for the displayed boundary 'gamma3' branch.

structure OneTermRobinGamma3BoundaryRyCoefficientBridge where
  sourceAnchor : String
  systemRow : Nat
  systemColumn : Nat
  sparseSlot : Nat
  cosHalfEntry : Coeff
  normalizedCoefficient : Coeff
  normalizedCoefficientFormula : String
  thetaFormula : String
  cosHalfFormula : String
  angleConventionObligation : SemanticObligation

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary ry coefficient bridge n 3”. Compiled focused bridge for the 'n = 3', row-'0', column-'0', global-slot-'2' boundary branch.

def oneTermRobinGamma3BoundaryRyCoefficientBridge_n3 :
    OneTermRobinGamma3BoundaryRyCoefficientBridge :=
  let p := oneTermParameters 3
  let sysRow : Fin (gridSize 3) := ⟨0, by native_decide⟩
  let sysCol : Fin (gridSize 3) := ⟨0, by native_decide⟩
  let angleRoute := GHL2025.boundaryRotationAngleNormalizerProofRoute p 0 2
  {
    sourceAnchor :=
      "GHL2025 Eq. angles for Ry, Eq. ROBIN clarified, Fig. 1-term ROBIN, arXiv:2506.20478"
    systemRow := sysRow.val
    systemColumn := sysCol.val

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary ry coefficient bridge n 3 transcript”; its local proof does not by itself complete the broader paper route. Transcript theorem for the focused boundary 'R_y' coefficient bridge.

theorem oneTermRobinGamma3BoundaryRyCoefficientBridge_n3_transcript :
    let p := oneTermParameters 3
    let bridge := oneTermRobinGamma3BoundaryRyCoefficientBridge_n3
    bridge.sourceAnchor =
        "GHL2025 Eq. angles for Ry, Eq. ROBIN clarified, Fig. 1-term ROBIN, arXiv:2506.20478" ∧
      bridge.systemRow = 0 ∧
      bridge.systemColumn = 0 ∧
      bridge.sparseSlot = 2 ∧
      bridge.cosHalfEntry = Coeff.symbol "boundary_cos_half_0_2" ∧
      bridge.normalizedCoefficient =
        GHL2025.boundaryRotationNormalizedCoefficient p 0 2 ∧

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 boundary ry angle convention decision”. A proposition-valued field is a requirement until a constructor supplies it. Human/source decision packet for the boundary 'R_y' angle convention.

structure OneTermRobinGamma3BoundaryRyAngleConventionDecision where
  sourceAnchor : String
  bridge : OneTermRobinGamma3BoundaryRyCoefficientBridge
  standardRyMatrixConvention : String
  paperCoefficientNeed : String
  sourceSpecifiesDirectHalfAngleCoefficientRule : Bool
  humanInputRequired : Bool
  acceptedSourceBackedOptions : String
  productSearchBlocked : Bool
  decisionObligation : SemanticObligation
  angleConventionObligationProved : Bool

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary ry angle convention decision n 3”. Compiled decision packet for the focused boundary branch at 'n = 3'.

def oneTermRobinGamma3BoundaryRyAngleConventionDecision_n3 :
    OneTermRobinGamma3BoundaryRyAngleConventionDecision :=
  let bridge := oneTermRobinGamma3BoundaryRyCoefficientBridge_n3
  {
    sourceAnchor :=
      "GHL2025 Eq. angles for Ry, Eq. ROBIN clarified, Fig. 1-term ROBIN, arXiv:2506.20478"
    bridge := bridge
    standardRyMatrixConvention :=
      "boundary_cos_half_0_2 is the cos(theta_0^2 / 2) matrix entry"
    paperCoefficientNeed :=
      "the displayed gamma3 coefficient uses D_0^(2) / N_D"

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary ry angle convention decision n 3 transcript”; its local proof does not by itself complete the broader paper route. Transcript theorem for the boundary 'R_y' angle-convention decision packet.

theorem oneTermRobinGamma3BoundaryRyAngleConventionDecision_n3_transcript :
    let p := oneTermParameters 3
    let decision := oneTermRobinGamma3BoundaryRyAngleConventionDecision_n3
    decision.sourceAnchor =
        "GHL2025 Eq. angles for Ry, Eq. ROBIN clarified, Fig. 1-term ROBIN, arXiv:2506.20478" ∧
      decision.bridge = oneTermRobinGamma3BoundaryRyCoefficientBridge_n3 ∧
      decision.bridge.cosHalfEntry = Coeff.symbol "boundary_cos_half_0_2" ∧
      decision.bridge.normalizedCoefficient =
        GHL2025.boundaryRotationNormalizedCoefficient p 0 2 ∧
      decision.bridge.normalizedCoefficient =
        Coeff.mul (GHL2025.robinGlobalSparseAmplitudeValue 3 2 0)

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 boundary ry lower packet guard”. A proposition-valued field is a requirement until a constructor supplies it. Lower-packet guard for the boundary 'R_y' decision freeze.

structure OneTermRobinGamma3BoundaryRyLowerPacketGuard where
  sourceAnchor : String
  decision : OneTermRobinGamma3BoundaryRyAngleConventionDecision
  lowerProductProofPacketAllowed : Bool
  sourceBackedConventionPacketAllowed : Bool
  reviewerAuditAllowed : Bool
  guardReason : String
  bridgeObligationProved : Bool
  decisionObligationProved : Bool
  boundaryHalfAngleSemanticsProved : Bool
  productToCoefficientProved : Bool

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary ry lower packet guard n 3”. Compiled lower-packet guard for the focused 'n = 3' boundary branch.

def oneTermRobinGamma3BoundaryRyLowerPacketGuard_n3 :
    OneTermRobinGamma3BoundaryRyLowerPacketGuard :=
  let decision := oneTermRobinGamma3BoundaryRyAngleConventionDecision_n3
  {
    sourceAnchor := decision.sourceAnchor
    decision := decision
    lowerProductProofPacketAllowed := false
    sourceBackedConventionPacketAllowed := true
    reviewerAuditAllowed := true
    guardReason :=
      "product-to-coefficient search is blocked until the boundary Ry angle convention has source-backed or human input"

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary ry lower packet guard n 3 transcript”; its local proof does not by itself complete the broader paper route. Transcript theorem for the lower-packet guard.

theorem oneTermRobinGamma3BoundaryRyLowerPacketGuard_n3_transcript :
    let guard := oneTermRobinGamma3BoundaryRyLowerPacketGuard_n3
    guard.sourceAnchor =
        "GHL2025 Eq. angles for Ry, Eq. ROBIN clarified, Fig. 1-term ROBIN, arXiv:2506.20478" ∧
      guard.decision =
        oneTermRobinGamma3BoundaryRyAngleConventionDecision_n3 ∧
      guard.decision.humanInputRequired = true ∧
      guard.decision.productSearchBlocked = true ∧
      guard.lowerProductProofPacketAllowed = false ∧
      guard.sourceBackedConventionPacketAllowed = true ∧
      guard.reviewerAuditAllowed = true ∧

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 boundary ry corrected angle source decision”. A proposition-valued field is a requirement until a constructor supplies it. Source-backed correction decision for the focused boundary 'R_y' route.

structure OneTermRobinGamma3BoundaryRyCorrectedAngleSourceDecision where
  sourceAnchor : String
  localPaperFormula : String
  priorPaperFormula : String
  companionCodeFormula : String
  standardRyConventionSource : String
  correctedThetaFormula : String
  bridge : OneTermRobinGamma3BoundaryRyCoefficientBridge
  correctedAngleSourceBacked : Bool
  useStandardRyMatrixConvention : Bool
  directCoefficientEntryAllowed : Bool

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary ry corrected angle source decision n 3”. Compiled corrected-angle decision for the 'n = 3', row-'0', slot-'2' boundary branch.

def oneTermRobinGamma3BoundaryRyCorrectedAngleSourceDecision_n3 :
    OneTermRobinGamma3BoundaryRyCorrectedAngleSourceDecision :=
  let bridge := oneTermRobinGamma3BoundaryRyCoefficientBridge_n3
  let sysRow : Fin (gridSize 3) := ⟨0, by native_decide⟩
  let sysCol : Fin (gridSize 3) := ⟨0, by native_decide⟩
  {
    sourceAnchor :=
      "GHL2025 Eq. angles for Ry, Fig. 1-term ROBIN, arXiv:2506.20478; GHL 2024 arXiv:2405.12855 Appendix O_p^S; companion repository Hamiltonian_of_1D_Heat_Equation.py"
    localPaperFormula :=
      "theta_j^s = arccos(D_j^(s) / N_D)"
    priorPaperFormula :=

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary ry corrected angle source decision n 3 transcript”; its local proof does not by itself complete the broader paper route. Transcript theorem for the corrected-angle source decision.

theorem oneTermRobinGamma3BoundaryRyCorrectedAngleSourceDecision_n3_transcript :
    let decision := oneTermRobinGamma3BoundaryRyCorrectedAngleSourceDecision_n3
    decision.localPaperFormula =
        "theta_j^s = arccos(D_j^(s) / N_D)" ∧
      decision.priorPaperFormula =
        "theta_s = 2 arccos((p^m)^(s) / sqrt(N_p^m)) for the standard Ry sparse-amplitude oracle" ∧
      decision.companionCodeFormula =
        "theta = 2 * np.arccos(boundary_coefficient / normalizer)" ∧
      decision.standardRyConventionSource =
        "companion repository README and fundamental_gates_unitary.py define ry(parameter) with cos(parameter/2) and sin(parameter/2)" ∧
      decision.correctedThetaFormula =

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 boundary corrected coefficient interface”. A proposition-valued field is a requirement until a constructor supplies it. Corrected-angle coefficient interface for the focused boundary branch.

structure OneTermRobinGamma3BoundaryCorrectedCoefficientInterface where
  sourceAnchor : String
  decision : OneTermRobinGamma3BoundaryRyCorrectedAngleSourceDecision
  productEntryFactor : Coeff
  normalizedCoefficient : Coeff
  correctedEntryHypothesis : SemanticObligation
  productObligation : SemanticObligation
  correctedAngleSourceBacked : Bool
  coefficientInterfaceCompiled : Bool
  productToCoefficientProved : Bool
  lcuCorrectProved : Bool

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary corrected coefficient interface n 3”. Compiled interface for replacing the boundary free factor by the corrected normalized coefficient in the 'n = 3', row-'0', column-'0', slot-'2' branch.

def oneTermRobinGamma3BoundaryCorrectedCoefficientInterface_n3 :
    OneTermRobinGamma3BoundaryCorrectedCoefficientInterface :=
  let decision := oneTermRobinGamma3BoundaryRyCorrectedAngleSourceDecision_n3
  let sysRow : Fin (gridSize 3) := ⟨0, by native_decide⟩
  let sysCol : Fin (gridSize 3) := ⟨0, by native_decide⟩
  {
    sourceAnchor := decision.sourceAnchor
    decision := decision
    productEntryFactor := Coeff.symbol "boundary_cos_half_0_2"
    normalizedCoefficient :=
      GHL2025.boundaryRotationNormalizedCoefficient (oneTermParameters 3) 0 2

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary corrected coefficient interface n 3 transcript”; its local proof does not by itself complete the broader paper route. Transcript theorem for the corrected-angle coefficient interface.

theorem oneTermRobinGamma3BoundaryCorrectedCoefficientInterface_n3_transcript :
    let interface := oneTermRobinGamma3BoundaryCorrectedCoefficientInterface_n3
    interface.decision =
        oneTermRobinGamma3BoundaryRyCorrectedAngleSourceDecision_n3 ∧
      interface.productEntryFactor = Coeff.symbol "boundary_cos_half_0_2" ∧
      interface.normalizedCoefficient =
        GHL2025.boundaryRotationNormalizedCoefficient (oneTermParameters 3) 0 2 ∧
      interface.normalizedCoefficient =
        Coeff.mul (GHL2025.robinGlobalSparseAmplitudeValue 3 2 0)
          (Coeff.symbol "N_D_inv") ∧
      interface.correctedEntryHypothesis.proved = false ∧

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route gamma 3 boundary product entry eval corrected angle n 3”; its local proof does not by itself complete the broader paper route. Conditional evaluated-product interface for the corrected boundary angle.

theorem oneTermRobinBlockEncodingProofRoute_gamma3BoundaryProductEntryEval_correctedAngle_n3
    (env : String → Rat)
    (hentry :
      env "boundary_cos_half_0_2" =
        Coeff.evalWith env
          (GHL2025.boundaryRotationNormalizedCoefficient
            (oneTermParameters 3) 0 2)) :
    Coeff.evalWith env
      (oneTermRobinGamma3BoundarySevenGateMatrix_n3
        oneTermRobinGamma3BoundaryPrefixSource_n3
        oneTermRobinGamma3BoundaryPrefixSource_n3) =

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin block encoding proof route gamma 3 boundary product entry eval corrected coefficient expanded n 3”; its local proof does not by itself complete the broader paper route. Expanded corrected-angle product entry for the displayed boundary branch.

theorem oneTermRobinBlockEncodingProofRoute_gamma3BoundaryProductEntryEval_correctedCoefficientExpanded_n3
    (env : String → Rat)
    (hentry :
      env "boundary_cos_half_0_2" =
        Coeff.evalWith env
          (GHL2025.boundaryRotationNormalizedCoefficient
            (oneTermParameters 3) 0 2)) :
    Coeff.evalWith env
      (oneTermRobinGamma3BoundarySevenGateMatrix_n3
        oneTermRobinGamma3BoundaryPrefixSource_n3
        oneTermRobinGamma3BoundaryPrefixSource_n3) =

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary ak entry matches global slot 2 n 3”; its local proof does not by itself complete the broader paper route. The focused boundary target entry uses the same global slot-'2' coefficient.

theorem oneTermRobinGamma3BoundaryAkEntry_matches_globalSlot2_n3 :
    let sysRow : Fin (gridSize 3) := ⟨0, by native_decide⟩
    let sysCol : Fin (gridSize 3) := ⟨0, by native_decide⟩
    oneTermRobinAkMatrix 3 sysRow sysCol =
      Coeff.mul (GHL2025.robinFunctionValue 3 0)
        (GHL2025.robinGlobalSparseAmplitudeValue 3 2 0) := by

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 boundary product to coefficient obstruction”. A proposition-valued field is a requirement until a constructor supplies it. Precise remaining obstruction for the focused boundary product-to-coefficient route.

structure OneTermRobinGamma3BoundaryProductToCoefficientObstruction where
  sourceAnchor : String
  productEntryFormula : String
  akEntryFormula : String
  correctedEntryHypothesis : SemanticObligation
  normalizedQuotientConvention : SemanticObligation
  sparseRegisterProjectionConvention : SemanticObligation
  productObligation : SemanticObligation
  productEntryExpanded : Bool
  akEntryMatched : Bool
  productToCoefficientProved : Bool

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary product to coefficient obstruction n 3”. Compiled obstruction packet for 'oneTermRobinGamma3ProductToCoefficientObligation 3 0 0'.

def oneTermRobinGamma3BoundaryProductToCoefficientObstruction_n3 :
    OneTermRobinGamma3BoundaryProductToCoefficientObstruction :=
  let sysRow : Fin (gridSize 3) := ⟨0, by native_decide⟩
  let sysCol : Fin (gridSize 3) := ⟨0, by native_decide⟩
  let interface := oneTermRobinGamma3BoundaryCorrectedCoefficientInterface_n3
  {
    sourceAnchor :=
      "GHL2025 Eq. ROBIN clarified displayed gamma3 boundary branch, Theorem one-term block-encoding, Fig. 1-term ROBIN, and Definition def:block-encoding, arXiv:2506.20478"
    productEntryFormula :=
      "under the corrected-entry hypothesis, product[32,32] = (f_3_0 * N_f_inv) * (D_0^(2) * N_D_inv)"
    akEntryFormula :=

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary product to coefficient obstruction n 3 transcript”; its local proof does not by itself complete the broader paper route. Transcript theorem for the focused boundary product-to-coefficient obstruction.

theorem oneTermRobinGamma3BoundaryProductToCoefficientObstruction_n3_transcript :
    let obstruction :=
      oneTermRobinGamma3BoundaryProductToCoefficientObstruction_n3
    obstruction.productEntryFormula =
        "under the corrected-entry hypothesis, product[32,32] = (f_3_0 * N_f_inv) * (D_0^(2) * N_D_inv)" ∧
      obstruction.akEntryFormula =
        "(oneTermRobinAkMatrix 3)[0,0] = f_3_0 * D_0^(2)" ∧
      obstruction.correctedEntryHypothesis.proved = false ∧
      obstruction.normalizedQuotientConvention.proved = false ∧
      obstruction.sparseRegisterProjectionConvention.proved = false ∧
      obstruction.productObligation.proved = false ∧

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 boundary normalizer projection convention”. A proposition-valued field is a requirement until a constructor supplies it. Theorem-level normalizer/projection convention packet for the focused boundary 'gamma3' product route.

structure OneTermRobinGamma3BoundaryNormalizerProjectionConvention where
  sourceAnchor : String
  obstruction : OneTermRobinGamma3BoundaryProductToCoefficientObstruction
  branchLocalProduct : Coeff
  targetEntry : Coeff
  targetEntryLocalFormula : Coeff
  theoremNormalizer : Coeff
  finiteCompositionNormalizer : Coeff
  normalizerFormula : String
  quotientConventionFormula : String
  sparseProjectionFormula : String

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary normalizer projection convention n 3”. Compiled normalizer/projection convention interface for 'oneTermRobinGamma3ProductToCoefficientObligation 3 0 0'.

def oneTermRobinGamma3BoundaryNormalizerProjectionConvention_n3 :
    OneTermRobinGamma3BoundaryNormalizerProjectionConvention :=
  let p := oneTermParameters 3
  let sysRow : Fin (gridSize 3) := ⟨0, by native_decide⟩
  let sysCol : Fin (gridSize 3) := ⟨0, by native_decide⟩
  let obstruction := oneTermRobinGamma3BoundaryProductToCoefficientObstruction_n3
  let contract := oneTermRobinFiniteBlockCompositionContract 3
  {
    sourceAnchor :=
      "GHL2025 Eq. ROBIN clarified displayed gamma3 boundary branch, Theorem one-term block-encoding, Definition def:block-encoding, and Fig. 1-term ROBIN, arXiv:2506.20478"
    obstruction := obstruction

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary normalizer projection convention n 3 transcript”; its local proof does not by itself complete the broader paper route. Transcript theorem for the focused normalizer/projection convention packet.

theorem oneTermRobinGamma3BoundaryNormalizerProjectionConvention_n3_transcript :
    let p := oneTermParameters 3
    let convention :=
      oneTermRobinGamma3BoundaryNormalizerProjectionConvention_n3
    let sysRow : Fin (gridSize 3) := ⟨0, by native_decide⟩
    let sysCol : Fin (gridSize 3) := ⟨0, by native_decide⟩
    convention.sourceAnchor =
        "GHL2025 Eq. ROBIN clarified displayed gamma3 boundary branch, Theorem one-term block-encoding, Definition def:block-encoding, and Fig. 1-term ROBIN, arXiv:2506.20478" ∧
      convention.obstruction =
        oneTermRobinGamma3BoundaryProductToCoefficientObstruction_n3 ∧
      convention.branchLocalProduct =

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 boundary normalizer split target”. A proposition-valued field is a requirement until a constructor supplies it. Middle-agent split target for the next focused boundary 'gamma3' packet.

structure OneTermRobinGamma3BoundaryNormalizerSplitTarget where
  sourceAnchor : String
  convention : OneTermRobinGamma3BoundaryNormalizerProjectionConvention
  symbolicInverseFormula : String
  kappaProjectionFormula : String
  symbolicInverseObligation : SemanticObligation
  kappaProjectionObligation : SemanticObligation
  finiteCompositionNormalizedEquality : SemanticObligation
  productObligation : SemanticObligation
  branchLocalProduct : Coeff
  targetEntry : Coeff

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary normalizer split target n 3”. Lean-facing lower packet target after the boundary normalizer/projection convention compiled.

def oneTermRobinGamma3BoundaryNormalizerSplitTarget_n3 :
    OneTermRobinGamma3BoundaryNormalizerSplitTarget :=
  let convention := oneTermRobinGamma3BoundaryNormalizerProjectionConvention_n3
  {
    sourceAnchor :=
      "GHL2025 Eq. ROBIN clarified gamma3 denominator N_D*N_f*kappa and Definition def:block-encoding, arXiv:2506.20478"
    convention := convention
    symbolicInverseFormula :=
      "N_D_inv and N_f_inv supply only the N_D*N_f inverse factors in the corrected boundary product"
    kappaProjectionFormula :=
      "the sparse-register projection/summation supplies the separate 1/kappa factor for the focused slot-2 branch"

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary normalizer split target n 3 transcript”; its local proof does not by itself complete the broader paper route. Transcript theorem for the split target.

theorem oneTermRobinGamma3BoundaryNormalizerSplitTarget_n3_transcript :
    let target := oneTermRobinGamma3BoundaryNormalizerSplitTarget_n3
    target.sourceAnchor =
        "GHL2025 Eq. ROBIN clarified gamma3 denominator N_D*N_f*kappa and Definition def:block-encoding, arXiv:2506.20478" ∧
      target.convention =
        oneTermRobinGamma3BoundaryNormalizerProjectionConvention_n3 ∧
      target.symbolicInverseFormula =
        "N_D_inv and N_f_inv supply only the N_D*N_f inverse factors in the corrected boundary product" ∧
      target.kappaProjectionFormula =
        "the sparse-register projection/summation supplies the separate 1/kappa factor for the focused slot-2 branch" ∧
      target.symbolicInverseObligation =

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary symbolic inverse eval n 3”; its local proof does not by itself complete the broader paper route. Conditional symbolic-inverse evaluation for the focused boundary branch.

theorem oneTermRobinGamma3BoundarySymbolicInverseEval_n3
    (env : String → Rat)
    (hND : env "N_D_inv" * env "N_D" = 1)
    (hNF : env "N_f_inv" * env "N_f" = 1) :
    Coeff.evalWith env
        oneTermRobinGamma3BoundaryNormalizerSplitTarget_n3.branchLocalProduct *
      (env "N_D" * env "N_f") =
    Coeff.evalWith env
        oneTermRobinGamma3BoundaryNormalizerSplitTarget_n3.targetEntry := by

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 boundary symbolic inverse semantics”. A proposition-valued field is a requirement until a constructor supplies it. Transcript packet for the symbolic-inverse half of the boundary split target.

structure OneTermRobinGamma3BoundarySymbolicInverseSemantics where
  sourceAnchor : String
  splitTarget : OneTermRobinGamma3BoundaryNormalizerSplitTarget
  normalizerPartFormula : String
  ndInverseHypothesis : String
  nfInverseHypothesis : String
  conditionalEvalLemma : String
  symbolicInverseObligation : SemanticObligation
  kappaProjectionObligation : SemanticObligation
  finiteCompositionNormalizedEquality : SemanticObligation
  productObligation : SemanticObligation

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary symbolic inverse semantics n 3”. Compiled symbolic-inverse packet for the focused boundary branch.

def oneTermRobinGamma3BoundarySymbolicInverseSemantics_n3 :
    OneTermRobinGamma3BoundarySymbolicInverseSemantics :=
  let target := oneTermRobinGamma3BoundaryNormalizerSplitTarget_n3
  {
    sourceAnchor :=
      "GHL2025 Eq. ROBIN clarified gamma3 denominator N_D*N_f*kappa, arXiv:2506.20478"
    splitTarget := target
    normalizerPartFormula :=
      "branchLocalProduct * (N_D*N_f) = targetEntry under N_D_inv*N_D=1 and N_f_inv*N_f=1"
    ndInverseHypothesis := "env N_D_inv * env N_D = 1"
    nfInverseHypothesis := "env N_f_inv * env N_f = 1"

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary symbolic inverse semantics n 3 transcript”; its local proof does not by itself complete the broader paper route. Transcript theorem for the symbolic-inverse packet.

theorem oneTermRobinGamma3BoundarySymbolicInverseSemantics_n3_transcript :
    let semantics :=
      oneTermRobinGamma3BoundarySymbolicInverseSemantics_n3
    let target := oneTermRobinGamma3BoundaryNormalizerSplitTarget_n3
    semantics.sourceAnchor =
        "GHL2025 Eq. ROBIN clarified gamma3 denominator N_D*N_f*kappa, arXiv:2506.20478" ∧
      semantics.splitTarget = target ∧
      semantics.normalizerPartFormula =
        "branchLocalProduct * (N_D*N_f) = targetEntry under N_D_inv*N_D=1 and N_f_inv*N_f=1" ∧
      semantics.ndInverseHypothesis = "env N_D_inv * env N_D = 1" ∧
      semantics.nfInverseHypothesis = "env N_f_inv * env N_f = 1" ∧

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary uniform sparse register preparation obligation n 3”. Uniform sparse-register preparation obligation for the focused boundary 'gamma3' route.

def oneTermRobinGamma3BoundaryUniformSparseRegisterPreparationObligation_n3 :
    SemanticObligation where
  description :=
    "uniform sparse-register preparation/projection supplies the remaining 1/kappa factor for the focused gamma3 boundary slot"
  source :=
    "GHL2025 Eq. arbitrary sparcity, Eq. ROBIN clarified, Fig. 1-term ROBIN; Shukla-Vedula 2024 uniform superposition state preparation cited for implementation cost"
  proved := false

/--
Middle-agent packet target for the sparse-register `kappa` projection factor.

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 boundary kappa projection target”. A proposition-valued field is a requirement until a constructor supplies it. Middle-agent packet target for the sparse-register 'kappa' projection factor.

structure OneTermRobinGamma3BoundaryKappaProjectionTarget where
  sourceAnchor : String
  splitTarget : OneTermRobinGamma3BoundaryNormalizerSplitTarget
  symbolicInverseSemantics : OneTermRobinGamma3BoundarySymbolicInverseSemantics
  citedResultId : String
  hWFormula : String
  preparationAmplitudeFormula : String
  projectionAmplitudeFormula : String
  productProjectionFormula : String
  focusedKappa : Nat
  focusedSparseSlot : Nat

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary kappa projection target n 3”. Compiled sparse-register 'kappa' projection target for the focused boundary entry '(0,0)' and global sparse slot '2'.

def oneTermRobinGamma3BoundaryKappaProjectionTarget_n3 :
    OneTermRobinGamma3BoundaryKappaProjectionTarget :=
  let p := oneTermParameters 3
  let splitTarget := oneTermRobinGamma3BoundaryNormalizerSplitTarget_n3
  let inverseSemantics := oneTermRobinGamma3BoundarySymbolicInverseSemantics_n3
  let sourceIndex := oneTermRobinGamma3PaperBasisIndex p 2 0
  {
    sourceAnchor :=
      "GHL2025 Eq. arbitrary sparcity, Eq. ROBIN clarified gamma3 boundary summand, Fig. 1-term ROBIN, and Definition def:block-encoding, arXiv:2506.20478"
    splitTarget := splitTarget
    symbolicInverseSemantics := inverseSemantics

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary kappa projection target n 3 transcript”; its local proof does not by itself complete the broader paper route. Transcript theorem for the sparse-register 'kappa' projection target.

theorem oneTermRobinGamma3BoundaryKappaProjectionTarget_n3_transcript :
    let target := oneTermRobinGamma3BoundaryKappaProjectionTarget_n3
    target.sourceAnchor =
        "GHL2025 Eq. arbitrary sparcity, Eq. ROBIN clarified gamma3 boundary summand, Fig. 1-term ROBIN, and Definition def:block-encoding, arXiv:2506.20478" ∧
      target.splitTarget =
        oneTermRobinGamma3BoundaryNormalizerSplitTarget_n3 ∧
      target.symbolicInverseSemantics =
        oneTermRobinGamma3BoundarySymbolicInverseSemantics_n3 ∧
      target.citedResultId =
        "ShuklaVedula2024.HWkappaUniformSuperposition" ∧
      target.hWFormula =

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary kappa projection eval n 3”; its local proof does not by itself complete the broader paper route. Conditional sparse-register 'kappa' projection evaluation for the focused boundary branch.

theorem oneTermRobinGamma3BoundaryKappaProjectionEval_n3
    (env : String → Rat)
    (hND : env "N_D_inv" * env "N_D" = 1)
    (hNF : env "N_f_inv" * env "N_f" = 1)
    (hkappa : env "kappa_inv" * env "kappa" = 1) :
    Coeff.evalWith env
        (Coeff.mul
          oneTermRobinGamma3BoundaryKappaProjectionTarget_n3.splitTarget.branchLocalProduct
          (Coeff.symbol "kappa_inv")) *
      Coeff.evalWith env
        oneTermRobinGamma3BoundaryKappaProjectionTarget_n3.theoremNormalizer =

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 boundary kappa projection semantics”. A proposition-valued field is a requirement until a constructor supplies it. Compiled packet for the conditional 'kappa_inv' projection evaluation.

structure OneTermRobinGamma3BoundaryKappaProjectionSemantics where
  sourceAnchor : String
  projectionTarget : OneTermRobinGamma3BoundaryKappaProjectionTarget
  projectedBranchProduct : Coeff
  projectionFactor : Coeff
  kappaInverseHypothesis : String
  conditionalEvalLemma : String
  uniformPreparationObligation : SemanticObligation
  kappaProjectionObligation : SemanticObligation
  finiteCompositionNormalizedEquality : SemanticObligation
  productObligation : SemanticObligation

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary kappa projection semantics n 3”. Boundary 'gamma3' sparse-register projection packet for 'n = 3'.

def oneTermRobinGamma3BoundaryKappaProjectionSemantics_n3 :
    OneTermRobinGamma3BoundaryKappaProjectionSemantics :=
  let target := oneTermRobinGamma3BoundaryKappaProjectionTarget_n3
  {
    sourceAnchor :=
      "GHL2025 Eq. arbitrary sparcity, Eq. ROBIN clarified gamma3 denominator N_D*N_f*kappa, Fig. 1-term ROBIN, and Definition def:block-encoding, arXiv:2506.20478"
    projectionTarget := target
    projectedBranchProduct :=
      Coeff.mul target.splitTarget.branchLocalProduct (Coeff.symbol "kappa_inv")
    projectionFactor := Coeff.symbol "kappa_inv"
    kappaInverseHypothesis := "env kappa_inv * env kappa = 1"

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary kappa projection semantics n 3 transcript”; its local proof does not by itself complete the broader paper route. Transcript theorem for the conditional sparse-register projection packet.

theorem oneTermRobinGamma3BoundaryKappaProjectionSemantics_n3_transcript :
    let semantics := oneTermRobinGamma3BoundaryKappaProjectionSemantics_n3
    let target := oneTermRobinGamma3BoundaryKappaProjectionTarget_n3
    semantics.sourceAnchor =
        "GHL2025 Eq. arbitrary sparcity, Eq. ROBIN clarified gamma3 denominator N_D*N_f*kappa, Fig. 1-term ROBIN, and Definition def:block-encoding, arXiv:2506.20478" ∧
      semantics.projectionTarget = target ∧
      semantics.projectedBranchProduct =
        Coeff.mul target.splitTarget.branchLocalProduct
          (Coeff.symbol "kappa_inv") ∧
      semantics.projectionFactor = Coeff.symbol "kappa_inv" ∧
      semantics.kappaInverseHypothesis =

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 boundary projection source contract”. A proposition-valued field is a requirement until a constructor supplies it. Source-backed projection contract for the inserted 'kappa_inv' factor.

structure OneTermRobinGamma3BoundaryProjectionSourceContract where
  sourceAnchor : String
  kappaSemantics : OneTermRobinGamma3BoundaryKappaProjectionSemantics
  citedResultId : String
  preparationFormula : String
  preparationAmplitudeFormula : String
  projectionAmplitudeFormula : String
  combinedProjectionFormula : String
  focusedKappa : Nat
  focusedSparseSlot : Nat
  sourceBasisIndex : Nat

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary projection source contract n 3”. Compiled source/projection contract for the focused boundary branch.

def oneTermRobinGamma3BoundaryProjectionSourceContract_n3 :
    OneTermRobinGamma3BoundaryProjectionSourceContract :=
  let semantics := oneTermRobinGamma3BoundaryKappaProjectionSemantics_n3
  let target := semantics.projectionTarget
  {
    sourceAnchor :=
      "GHL2025 Eq. arbitrary sparcity, Eq. ROBIN clarified gamma3 denominator N_D*N_f*kappa, Fig. 1-term ROBIN, Definition def:block-encoding, and Shukla-Vedula 2024, arXiv:2506.20478"
    kappaSemantics := semantics
    citedResultId := target.citedResultId
    preparationFormula := target.hWFormula
    preparationAmplitudeFormula := target.preparationAmplitudeFormula

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary projection source contract n 3 transcript”; its local proof does not by itself complete the broader paper route. Transcript theorem for the boundary projection source contract.

theorem oneTermRobinGamma3BoundaryProjectionSourceContract_n3_transcript :
    let contract := oneTermRobinGamma3BoundaryProjectionSourceContract_n3
    let semantics := oneTermRobinGamma3BoundaryKappaProjectionSemantics_n3
    contract.kappaSemantics = semantics ∧
      contract.citedResultId =
        "ShuklaVedula2024.HWkappaUniformSuperposition" ∧
      contract.preparationFormula =
        "H_W^(kappa)|0>^ceil(log2 kappa) = (1/sqrt(kappa)) * sum_{s=0}^{kappa-1} |s>" ∧
      contract.preparationAmplitudeFormula = "1/sqrt(kappa)" ∧
      contract.projectionAmplitudeFormula = "1/sqrt(kappa)" ∧
      contract.combinedProjectionFormula = "1/kappa" ∧

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary projection factor index n 3”; its local proof does not by itself complete the broader paper route. Finite index check for the boundary projection-factor packet.

theorem oneTermRobinGamma3BoundaryProjectionFactorIndex_n3 :
    let p := oneTermParameters 3
    let contract := oneTermRobinGamma3BoundaryProjectionSourceContract_n3
    contract.focusedSparseSlot = 2 ∧
      contract.sourceBasisIndex = oneTermRobinGamma3PaperBasisIndex p 2 0 ∧
      contract.targetBasisIndex = oneTermRobinGamma3PaperBasisIndex p 2 0 ∧
      contract.sourceBasisIndex = contract.targetBasisIndex ∧
      contract.sourceBasisIndex = 32 ∧
      contract.targetBasisIndex = 32 ∧
      contract.projectionFactor = Coeff.symbol "kappa_inv" ∧
      contract.projectedBranchProduct =

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 boundary projection factor semantics”. A proposition-valued field is a requirement until a constructor supplies it. Finite projection-factor interface for the inserted 'kappa_inv' factor.

structure OneTermRobinGamma3BoundaryProjectionFactorSemantics where
  sourceAnchor : String
  sourceContract : OneTermRobinGamma3BoundaryProjectionSourceContract
  finiteIndexLemma : String
  preparedSparseSlot : Nat
  projectedSparseSlot : Nat
  preparedBasisIndex : Nat
  projectedBasisIndex : Nat
  preparedAndProjectedSlotAgree : Bool
  preparedAndProjectedBasisAgree : Bool
  preparationAmplitudeFormula : String

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary projection factor semantics n 3”. Compiled finite projection-factor interface for the focused boundary branch.

def oneTermRobinGamma3BoundaryProjectionFactorSemantics_n3 :
    OneTermRobinGamma3BoundaryProjectionFactorSemantics :=
  let contract := oneTermRobinGamma3BoundaryProjectionSourceContract_n3
  {
    sourceAnchor :=
      "GHL2025 Eq. arbitrary sparcity, Eq. ROBIN clarified gamma3 boundary branch, Definition def:block-encoding, and Shukla-Vedula 2024, arXiv:2506.20478"
    sourceContract := contract
    finiteIndexLemma :=
      "oneTermRobinGamma3BoundaryProjectionFactorIndex_n3"
    preparedSparseSlot := contract.focusedSparseSlot
    projectedSparseSlot := contract.focusedSparseSlot

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary projection factor semantics n 3 transcript”; its local proof does not by itself complete the broader paper route. Transcript theorem for the finite projection-factor interface.

theorem oneTermRobinGamma3BoundaryProjectionFactorSemantics_n3_transcript :
    let factor := oneTermRobinGamma3BoundaryProjectionFactorSemantics_n3
    let contract := oneTermRobinGamma3BoundaryProjectionSourceContract_n3
    factor.sourceAnchor =
        "GHL2025 Eq. arbitrary sparcity, Eq. ROBIN clarified gamma3 boundary branch, Definition def:block-encoding, and Shukla-Vedula 2024, arXiv:2506.20478" ∧
      factor.sourceContract = contract ∧
      factor.finiteIndexLemma =
        "oneTermRobinGamma3BoundaryProjectionFactorIndex_n3" ∧
      factor.preparedSparseSlot = 2 ∧
      factor.projectedSparseSlot = 2 ∧
      factor.preparedBasisIndex = 32 ∧

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 boundary projection factor obstruction”. A proposition-valued field is a requirement until a constructor supplies it. Smallest current obstruction for proving the focused projection factor.

structure OneTermRobinGamma3BoundaryProjectionFactorObstruction where
  sourceAnchor : String
  factorSemantics : OneTermRobinGamma3BoundaryProjectionFactorSemantics
  citedUniformPreparationId : String
  citedUniformPreparationNeed : String
  matchingProjectionNeed : String
  symbolicFactorNeed : String
  uniformPreparationObligation : SemanticObligation
  matchingProjectionObligation : SemanticObligation
  factorSemanticsObligation : SemanticObligation
  finiteCompositionNormalizedEquality : SemanticObligation

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary projection factor obstruction n 3”. Compiled obstruction packet for the projection-factor semantics of the focused boundary branch.

def oneTermRobinGamma3BoundaryProjectionFactorObstruction_n3 :
    OneTermRobinGamma3BoundaryProjectionFactorObstruction :=
  let factor := oneTermRobinGamma3BoundaryProjectionFactorSemantics_n3
  {
    sourceAnchor :=
      "GHL2025 Eq. arbitrary sparcity, Eq. ROBIN clarified gamma3 boundary branch, Definition def:block-encoding, and Shukla-Vedula 2024, arXiv:2506.20478"
    factorSemantics := factor
    citedUniformPreparationId := factor.sourceContract.citedResultId
    citedUniformPreparationNeed :=
      "formalize or contract-map the H_W^(kappa) per-slot amplitude 1/sqrt(kappa) for focused sparse slot 2"
    matchingProjectionNeed :=

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary projection factor obstruction n 3 transcript”; its local proof does not by itself complete the broader paper route. Transcript theorem for the projection-factor obstruction packet.

theorem oneTermRobinGamma3BoundaryProjectionFactorObstruction_n3_transcript :
    let obstruction :=
      oneTermRobinGamma3BoundaryProjectionFactorObstruction_n3
    let factor := oneTermRobinGamma3BoundaryProjectionFactorSemantics_n3
    obstruction.factorSemantics = factor ∧
      obstruction.citedUniformPreparationId =
        "ShuklaVedula2024.HWkappaUniformSuperposition" ∧
      obstruction.citedUniformPreparationNeed =
        "formalize or contract-map the H_W^(kappa) per-slot amplitude 1/sqrt(kappa) for focused sparse slot 2" ∧
      obstruction.matchingProjectionNeed =
        "state the QBE block-projection convention that the bra onto the same sparse slot contributes the second 1/sqrt(kappa) factor" ∧

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 boundary matching projection convention”. A proposition-valued field is a requirement until a constructor supplies it. Local matching-projection convention for the focused boundary branch.

structure OneTermRobinGamma3BoundaryMatchingProjectionConvention where
  sourceAnchor : String
  obstruction : OneTermRobinGamma3BoundaryProjectionFactorObstruction
  sourceContract : OneTermRobinGamma3BoundaryProjectionSourceContract
  factorSemantics : OneTermRobinGamma3BoundaryProjectionFactorSemantics
  focusedSparseSlot : Nat
  preparedBasisIndex : Nat
  projectedBasisIndex : Nat
  projectionBraFormula : String
  projectionKetFormula : String
  matchingProjectionNeed : String

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary matching projection convention n 3”. Compiled local matching-projection convention for sparse slot '2'.

def oneTermRobinGamma3BoundaryMatchingProjectionConvention_n3 :
    OneTermRobinGamma3BoundaryMatchingProjectionConvention :=
  let obstruction := oneTermRobinGamma3BoundaryProjectionFactorObstruction_n3
  let factor := oneTermRobinGamma3BoundaryProjectionFactorSemantics_n3
  {
    sourceAnchor :=
      "GHL2025 Definition def:block-encoding, Eq. arbitrary sparcity, Eq. ROBIN clarified boundary branch, arXiv:2506.20478"
    obstruction := obstruction
    sourceContract := factor.sourceContract
    factorSemantics := factor
    focusedSparseSlot := factor.projectedSparseSlot

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary matching projection convention n 3 transcript”; its local proof does not by itself complete the broader paper route. Transcript theorem for the matching-projection convention packet.

theorem oneTermRobinGamma3BoundaryMatchingProjectionConvention_n3_transcript :
    let convention :=
      oneTermRobinGamma3BoundaryMatchingProjectionConvention_n3
    let obstruction :=
      oneTermRobinGamma3BoundaryProjectionFactorObstruction_n3
    let factor := oneTermRobinGamma3BoundaryProjectionFactorSemantics_n3
    convention.sourceAnchor =
        "GHL2025 Definition def:block-encoding, Eq. arbitrary sparcity, Eq. ROBIN clarified boundary branch, arXiv:2506.20478" ∧
      convention.obstruction = obstruction ∧
      convention.sourceContract =
        oneTermRobinGamma3BoundaryProjectionSourceContract_n3 ∧

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary projection factor product eval n 3”; its local proof does not by itself complete the broader paper route. Symbolic product check for the two sparse-register amplitude factors.

theorem oneTermRobinGamma3BoundaryProjectionFactorProductEval_n3
    (env : String → Rat)
    (hkappaSqrt :
      env "sqrt_kappa_inv" * env "sqrt_kappa_inv" =
        env "kappa_inv") :
    Coeff.evalWith env
        (Coeff.mul (Coeff.symbol "sqrt_kappa_inv")
          (Coeff.symbol "sqrt_kappa_inv")) =
      Coeff.evalWith env (Coeff.symbol "kappa_inv") := by

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 boundary matching projection amplitude obstruction”. A proposition-valued field is a requirement until a constructor supplies it. Smallest current obstruction for the matching-projection amplitude packet.

structure OneTermRobinGamma3BoundaryMatchingProjectionAmplitudeObstruction where
  sourceAnchor : String
  matchingConvention : OneTermRobinGamma3BoundaryMatchingProjectionConvention
  preparationAmplitudeFormula : String
  matchingProjectionAmplitudeFormula : String
  combinedProjectionFormula : String
  symbolicProductFormula : String
  preparationAmplitudeFactor : Coeff
  matchingProjectionAmplitudeFactor : Coeff
  combinedAmplitudeFactor : Coeff
  expectedProjectionFactor : Coeff

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary matching projection amplitude obstruction n 3”. Compiled obstruction packet for the focused matching-projection amplitude.

def oneTermRobinGamma3BoundaryMatchingProjectionAmplitudeObstruction_n3 :
    OneTermRobinGamma3BoundaryMatchingProjectionAmplitudeObstruction :=
  let convention := oneTermRobinGamma3BoundaryMatchingProjectionConvention_n3
  let halfFactor := Coeff.symbol "sqrt_kappa_inv"
  {
    sourceAnchor :=
      "GHL2025 Definition def:block-encoding, Eq. arbitrary sparcity, Eq. ROBIN clarified boundary branch, Fig. 1-term ROBIN, and Shukla-Vedula 2024, arXiv:2506.20478"
    matchingConvention := convention
    preparationAmplitudeFormula :=
      convention.sourceContract.preparationAmplitudeFormula
    matchingProjectionAmplitudeFormula :=

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary matching projection amplitude obstruction n 3 transcript”; its local proof does not by itself complete the broader paper route. Transcript theorem for the matching-projection amplitude obstruction.

theorem oneTermRobinGamma3BoundaryMatchingProjectionAmplitudeObstruction_n3_transcript :
    let obstruction :=
      oneTermRobinGamma3BoundaryMatchingProjectionAmplitudeObstruction_n3
    let convention :=
      oneTermRobinGamma3BoundaryMatchingProjectionConvention_n3
    obstruction.matchingConvention = convention ∧
      obstruction.preparationAmplitudeFormula = "1/sqrt(kappa)" ∧
      obstruction.matchingProjectionAmplitudeFormula = "1/sqrt(kappa)" ∧
      obstruction.combinedProjectionFormula = "1/kappa" ∧
      obstruction.symbolicProductFormula =
        "sqrt_kappa_inv * sqrt_kappa_inv = kappa_inv" ∧

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 boundary matching projection amplitude contract”. A proposition-valued field is a requirement until a constructor supplies it. Focused contract for the bra-side matching projection amplitude.

structure OneTermRobinGamma3BoundaryMatchingProjectionAmplitudeContract where
  sourceAnchor : String
  amplitudeObstruction :
    OneTermRobinGamma3BoundaryMatchingProjectionAmplitudeObstruction
  matchingConvention : OneTermRobinGamma3BoundaryMatchingProjectionConvention
  focusedSparseSlot : Nat
  preparedBasisIndex : Nat
  projectedBasisIndex : Nat
  projectionBraFormula : String
  expectedBraAmplitudeFormula : String
  matchingProjectionAmplitudeFactor : Coeff

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary matching projection amplitude contract n 3”. Compiled bra-side projection-amplitude contract for the focused boundary route.

def oneTermRobinGamma3BoundaryMatchingProjectionAmplitudeContract_n3 :
    OneTermRobinGamma3BoundaryMatchingProjectionAmplitudeContract :=
  let obstruction :=
    oneTermRobinGamma3BoundaryMatchingProjectionAmplitudeObstruction_n3
  let convention := obstruction.matchingConvention
  {
    sourceAnchor :=
      "GHL2025 Definition def:block-encoding, Eq. arbitrary sparcity, Eq. ROBIN clarified boundary branch, and Fig. 1-term ROBIN, arXiv:2506.20478"
    amplitudeObstruction := obstruction
    matchingConvention := convention
    focusedSparseSlot := convention.focusedSparseSlot

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary matching projection amplitude contract n 3 transcript”; its local proof does not by itself complete the broader paper route. Transcript theorem for the focused bra-side projection-amplitude contract.

theorem oneTermRobinGamma3BoundaryMatchingProjectionAmplitudeContract_n3_transcript :
    let contract :=
      oneTermRobinGamma3BoundaryMatchingProjectionAmplitudeContract_n3
    let obstruction :=
      oneTermRobinGamma3BoundaryMatchingProjectionAmplitudeObstruction_n3
    let convention :=
      oneTermRobinGamma3BoundaryMatchingProjectionConvention_n3
    contract.amplitudeObstruction = obstruction ∧
      contract.matchingConvention = convention ∧
      contract.focusedSparseSlot = 2 ∧
      contract.preparedBasisIndex = 32 ∧

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 boundary projection amplitude semantics”. A proposition-valued field is a requirement until a constructor supplies it. Phase-1 projection-amplitude semantics for the focused boundary branch.

structure OneTermRobinGamma3BoundaryProjectionAmplitudeSemantics where
  sourceAnchor : String
  amplitudeContract :
    OneTermRobinGamma3BoundaryMatchingProjectionAmplitudeContract
  citedUniformPreparationId : String
  focusedSparseSlot : Nat
  cleanBasisIndex : Nat
  ketAmplitudeFormula : String
  braAmplitudeFormula : String
  symbolicProductFormula : String
  ketAmplitudeFactor : Coeff

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary projection amplitude semantics n 3”. Compiled projection-amplitude semantics packet for the focused 'gamma3' boundary branch.

def oneTermRobinGamma3BoundaryProjectionAmplitudeSemantics_n3 :
    OneTermRobinGamma3BoundaryProjectionAmplitudeSemantics :=
  let contract := oneTermRobinGamma3BoundaryMatchingProjectionAmplitudeContract_n3
  let obstruction := contract.amplitudeObstruction
  {
    sourceAnchor :=
      "GHL2025 Definition def:block-encoding, Eq. arbitrary sparcity, Eq. ROBIN clarified boundary branch, Fig. 1-term ROBIN, and Shukla-Vedula 2024, arXiv:2506.20478"
    amplitudeContract := contract
    citedUniformPreparationId :=
      contract.matchingConvention.sourceContract.citedResultId
    focusedSparseSlot := contract.focusedSparseSlot

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary projection amplitude contract product eval n 3”; its local proof does not by itself complete the broader paper route. Conditional product evaluation for the accepted sparse-register amplitude contracts.

theorem oneTermRobinGamma3BoundaryProjectionAmplitudeContractProductEval_n3
    (env : String → Rat)
    (hkappaSqrt :
      env "sqrt_kappa_inv" * env "sqrt_kappa_inv" =
        env "kappa_inv") :
    let semantics :=
      oneTermRobinGamma3BoundaryProjectionAmplitudeSemantics_n3
    Coeff.evalWith env semantics.combinedAmplitudeFactor =
      Coeff.evalWith env semantics.expectedProjectionFactor := by

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary projection amplitude semantics n 3 transcript”; its local proof does not by itself complete the broader paper route. Transcript theorem for the projection-amplitude semantics packet.

theorem oneTermRobinGamma3BoundaryProjectionAmplitudeSemantics_n3_transcript :
    let semantics :=
      oneTermRobinGamma3BoundaryProjectionAmplitudeSemantics_n3
    let contract :=
      oneTermRobinGamma3BoundaryMatchingProjectionAmplitudeContract_n3
    semantics.amplitudeContract = contract ∧
      semantics.citedUniformPreparationId =
        "ShuklaVedula2024.HWkappaUniformSuperposition" ∧
      semantics.focusedSparseSlot = 2 ∧
      semantics.cleanBasisIndex = 32 ∧
      semantics.ketAmplitudeFormula = "1/sqrt(kappa)" ∧

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary projection amplitude factor eval n 3”; its local proof does not by itself complete the broader paper route. Conditional factor-semantics evaluation for the accepted sparse-register amplitude contracts.

theorem oneTermRobinGamma3BoundaryProjectionAmplitudeFactorEval_n3
    (env : String → Rat)
    (hND : env "N_D_inv" * env "N_D" = 1)
    (hNF : env "N_f_inv" * env "N_f" = 1)
    (hkappa : env "kappa_inv" * env "kappa" = 1)
    (hkappaSqrt :
      env "sqrt_kappa_inv" * env "sqrt_kappa_inv" =
        env "kappa_inv") :
    let semantics :=
      oneTermRobinGamma3BoundaryProjectionAmplitudeSemantics_n3
    Coeff.evalWith env

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 boundary projection amplitude factor semantics”. A proposition-valued field is a requirement until a constructor supplies it. Compiled packet for the conditional factor-semantics bridge.

structure OneTermRobinGamma3BoundaryProjectionAmplitudeFactorSemantics where
  sourceAnchor : String
  projectionAmplitudeSemantics :
    OneTermRobinGamma3BoundaryProjectionAmplitudeSemantics
  projectedBranchProduct : Coeff
  expectedTargetEntry : Coeff
  theoremNormalizer : Coeff
  factorHypothesisFormula : String
  conditionalFactorEvalLemma : String
  productEvalLemma : String
  kappaProjectionEvalLemma : String

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary projection amplitude factor semantics n 3”. Factor-semantics bridge for the focused boundary 'gamma3' packet.

def oneTermRobinGamma3BoundaryProjectionAmplitudeFactorSemantics_n3 :
    OneTermRobinGamma3BoundaryProjectionAmplitudeFactorSemantics :=
  let semantics := oneTermRobinGamma3BoundaryProjectionAmplitudeSemantics_n3
  let target := oneTermRobinGamma3BoundaryKappaProjectionTarget_n3
  {
    sourceAnchor :=
      "GHL2025 Eq. arbitrary sparcity, Eq. ROBIN clarified gamma3 denominator N_D*N_f*kappa, Definition def:block-encoding, Fig. 1-term ROBIN, and Shukla-Vedula 2024, arXiv:2506.20478"
    projectionAmplitudeSemantics := semantics
    projectedBranchProduct :=
      Coeff.mul target.splitTarget.branchLocalProduct
        semantics.combinedAmplitudeFactor

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary projection amplitude factor semantics n 3 transcript”; its local proof does not by itself complete the broader paper route. Transcript theorem for the conditional factor-semantics bridge.

theorem oneTermRobinGamma3BoundaryProjectionAmplitudeFactorSemantics_n3_transcript :
    let factor :=
      oneTermRobinGamma3BoundaryProjectionAmplitudeFactorSemantics_n3
    let semantics :=
      oneTermRobinGamma3BoundaryProjectionAmplitudeSemantics_n3
    let target := oneTermRobinGamma3BoundaryKappaProjectionTarget_n3
    factor.projectionAmplitudeSemantics = semantics ∧
      factor.projectedBranchProduct =
        Coeff.mul target.splitTarget.branchLocalProduct
          semantics.combinedAmplitudeFactor ∧
      factor.expectedTargetEntry = target.splitTarget.targetEntry ∧

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 boundary factor semantics contract map”. A proposition-valued field is a requirement until a constructor supplies it. Source-backed contract map for the factor-semantics obligation.

structure OneTermRobinGamma3BoundaryFactorSemanticsContractMap where
  sourceAnchor : String
  factorBridge : OneTermRobinGamma3BoundaryProjectionAmplitudeFactorSemantics
  projectedBranchProduct : Coeff
  expectedTargetEntry : Coeff
  theoremNormalizer : Coeff
  conditionalFactorEvalLemma : String
  productEvalLemma : String
  kappaProjectionEvalLemma : String
  ketAmplitudeObligation : SemanticObligation
  braAmplitudeObligation : SemanticObligation

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary factor semantics contract map n 3”. Compiled contract map for the focused boundary factor-semantics obligation.

def oneTermRobinGamma3BoundaryFactorSemanticsContractMap_n3 :
    OneTermRobinGamma3BoundaryFactorSemanticsContractMap :=
  let factor :=
    oneTermRobinGamma3BoundaryProjectionAmplitudeFactorSemantics_n3
  {
    sourceAnchor :=
      "GHL2025 Eq. arbitrary sparcity, Eq. ROBIN clarified boundary branch, Definition def:block-encoding, Fig. 1-term ROBIN, and Shukla-Vedula 2024, arXiv:2506.20478"
    factorBridge := factor
    projectedBranchProduct := factor.projectedBranchProduct
    expectedTargetEntry := factor.expectedTargetEntry
    theoremNormalizer := factor.theoremNormalizer

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary factor semantics contract map eval n 3”; its local proof does not by itself complete the broader paper route. Conditional evaluation through the contract-map fields.

theorem oneTermRobinGamma3BoundaryFactorSemanticsContractMapEval_n3
    (env : String → Rat)
    (hND : env "N_D_inv" * env "N_D" = 1)
    (hNF : env "N_f_inv" * env "N_f" = 1)
    (hkappa : env "kappa_inv" * env "kappa" = 1)
    (hkappaSqrt :
      env "sqrt_kappa_inv" * env "sqrt_kappa_inv" =
        env "kappa_inv") :
    let contract :=
      oneTermRobinGamma3BoundaryFactorSemanticsContractMap_n3
    Coeff.evalWith env contract.projectedBranchProduct *

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary factor semantics contract map n 3 transcript”; its local proof does not by itself complete the broader paper route. Transcript theorem for the focused factor-semantics contract map.

theorem oneTermRobinGamma3BoundaryFactorSemanticsContractMap_n3_transcript :
    let contract :=
      oneTermRobinGamma3BoundaryFactorSemanticsContractMap_n3
    let factor :=
      oneTermRobinGamma3BoundaryProjectionAmplitudeFactorSemantics_n3
    contract.sourceAnchor =
        "GHL2025 Eq. arbitrary sparcity, Eq. ROBIN clarified boundary branch, Definition def:block-encoding, Fig. 1-term ROBIN, and Shukla-Vedula 2024, arXiv:2506.20478" ∧
      contract.factorBridge = factor ∧
      contract.projectedBranchProduct = factor.projectedBranchProduct ∧
      contract.expectedTargetEntry = factor.expectedTargetEntry ∧
      contract.theoremNormalizer = factor.theoremNormalizer ∧

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 boundary bra projection amplitude source map”. A proposition-valued field is a requirement until a constructor supplies it. Source map for the remaining bra-side projection-amplitude obstruction.

structure OneTermRobinGamma3BoundaryBraProjectionAmplitudeSourceMap where
  sourceAnchor : String
  amplitudeContract :
    OneTermRobinGamma3BoundaryMatchingProjectionAmplitudeContract
  factorContractMap : OneTermRobinGamma3BoundaryFactorSemanticsContractMap
  focusedSparseSlot : Nat
  cleanBasisIndex : Nat
  projectionBraEntryFormula : String
  requiredSemanticObject : String
  requiredAdjointEntry : String
  expectedBraAmplitudeFactor : Coeff

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary bra projection amplitude source map n 3”. Compiled source map for the focused bra-side amplitude packet.

def oneTermRobinGamma3BoundaryBraProjectionAmplitudeSourceMap_n3 :
    OneTermRobinGamma3BoundaryBraProjectionAmplitudeSourceMap :=
  let amplitudeContract :=
    oneTermRobinGamma3BoundaryMatchingProjectionAmplitudeContract_n3
  let factorContract :=
    oneTermRobinGamma3BoundaryFactorSemanticsContractMap_n3
  {
    sourceAnchor :=
      "GHL2025 Definition def:block-encoding, Eq. arbitrary sparcity, Eq. ROBIN clarified boundary branch, Fig. 1-term ROBIN, and Shukla-Vedula 2024, arXiv:2506.20478"
    amplitudeContract := amplitudeContract
    factorContractMap := factorContract

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary bra projection amplitude source map n 3 transcript”; its local proof does not by itself complete the broader paper route. Transcript theorem for the bra-side projection-amplitude source map.

theorem oneTermRobinGamma3BoundaryBraProjectionAmplitudeSourceMap_n3_transcript :
    let sourceMap :=
      oneTermRobinGamma3BoundaryBraProjectionAmplitudeSourceMap_n3
    let amplitudeContract :=
      oneTermRobinGamma3BoundaryMatchingProjectionAmplitudeContract_n3
    let factorContract :=
      oneTermRobinGamma3BoundaryFactorSemanticsContractMap_n3
    sourceMap.amplitudeContract = amplitudeContract ∧
      sourceMap.factorContractMap = factorContract ∧
      sourceMap.focusedSparseSlot = 2 ∧
      sourceMap.cleanBasisIndex = 32 ∧

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 boundary hw kappa dagger projection entry contract”. A proposition-valued field is a requirement until a constructor supplies it. Typed contract for the focused 'H_W^(kappa)' dagger projection entry.

structure OneTermRobinGamma3BoundaryHWKappaDaggerProjectionEntryContract where
  sourceAnchor : String
  braSourceMap : OneTermRobinGamma3BoundaryBraProjectionAmplitudeSourceMap
  factorContractMap : OneTermRobinGamma3BoundaryFactorSemanticsContractMap
  focusedSparseSlot : Nat
  cleanBasisIndex : Nat
  sparseRegisterBra : Nat
  sparseRegisterKet : Nat
  entryFormula : String
  embeddedEntryFormula : String
  expectedEntry : Coeff

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary hw kappa dagger projection entry contract n 3”. Compiled Phase-1 contract for the focused bra projection entry.

def oneTermRobinGamma3BoundaryHWKappaDaggerProjectionEntryContract_n3 :
    OneTermRobinGamma3BoundaryHWKappaDaggerProjectionEntryContract :=
  let sourceMap :=
    oneTermRobinGamma3BoundaryBraProjectionAmplitudeSourceMap_n3
  let factorMap :=
    oneTermRobinGamma3BoundaryFactorSemanticsContractMap_n3
  {
    sourceAnchor :=
      "GHL2025 Eq. arbitrary sparcity, Definition def:block-encoding, Eq. ROBIN clarified boundary branch, Fig. 1-term ROBIN, and Shukla-Vedula 2024, arXiv:2506.20478"
    braSourceMap := sourceMap
    factorContractMap := factorMap

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary hw kappa dagger projection entry contract n 3 transcript”; its local proof does not by itself complete the broader paper route. Transcript theorem for the focused 'H_W^(kappa)' dagger entry contract.

theorem oneTermRobinGamma3BoundaryHWKappaDaggerProjectionEntryContract_n3_transcript :
    let entry :=
      oneTermRobinGamma3BoundaryHWKappaDaggerProjectionEntryContract_n3
    let sourceMap :=
      oneTermRobinGamma3BoundaryBraProjectionAmplitudeSourceMap_n3
    let factorMap :=
      oneTermRobinGamma3BoundaryFactorSemanticsContractMap_n3
    entry.braSourceMap = sourceMap ∧
      entry.factorContractMap = factorMap ∧
      entry.focusedSparseSlot = 2 ∧
      entry.cleanBasisIndex = 32 ∧

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 boundary hw kappa dagger embedded entry interface”. A proposition-valued field is a requirement until a constructor supplies it. Embedded-entry interface for the focused 'H_W^(kappa)^dagger' contract.

structure OneTermRobinGamma3BoundaryHWKappaDaggerEmbeddedEntryInterface where
  sourceAnchor : String
  entryContract : OneTermRobinGamma3BoundaryHWKappaDaggerProjectionEntryContract
  focusedSparseSlot : Nat
  focusedKappa : Nat
  sparseRegisterQubits : Nat
  sparseRegisterDimension : Nat
  localBraIndex : Nat
  localKetIndex : Nat
  ambientCleanBasisIndex : Nat
  localEntryFormula : String

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary hw kappa dagger embedded entry interface n 3”. Compiled embedded-entry interface for the focused boundary branch.

def oneTermRobinGamma3BoundaryHWKappaDaggerEmbeddedEntryInterface_n3 :
    OneTermRobinGamma3BoundaryHWKappaDaggerEmbeddedEntryInterface :=
  let p := oneTermParameters 3
  let entry :=
    oneTermRobinGamma3BoundaryHWKappaDaggerProjectionEntryContract_n3
  {
    sourceAnchor :=
      "GHL2025 Eq. arbitrary sparcity, Definition def:block-encoding, Eq. ROBIN clarified boundary branch, Fig. 1-term ROBIN, and Shukla-Vedula 2024, arXiv:2506.20478"
    entryContract := entry
    focusedSparseSlot := entry.focusedSparseSlot
    focusedKappa := p.kappa

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary hw kappa dagger embedded entry interface n 3 transcript”; its local proof does not by itself complete the broader paper route. Transcript theorem for the embedded-entry interface.

theorem oneTermRobinGamma3BoundaryHWKappaDaggerEmbeddedEntryInterface_n3_transcript :
    let interface :=
      oneTermRobinGamma3BoundaryHWKappaDaggerEmbeddedEntryInterface_n3
    let entry :=
      oneTermRobinGamma3BoundaryHWKappaDaggerProjectionEntryContract_n3
    let p := oneTermParameters 3
    interface.entryContract = entry ∧
      interface.focusedSparseSlot = 2 ∧
      interface.focusedKappa = 7 ∧
      interface.sparseRegisterQubits = 3 ∧
      interface.sparseRegisterDimension = 8 ∧

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary hw kappa dagger entry from uniform column n 3”; its local proof does not by itself complete the broader paper route. Conditional adjoint-entry lemma for the focused 'H_W^(kappa)' slot.

theorem oneTermRobinGamma3BoundaryHWKappaDaggerEntryFromUniformColumn_n3
    (H Hdagger : Matrix 8 8 Coeff)
    (hUniform :
      H ⟨2, by native_decide⟩ ⟨0, by native_decide⟩ =
        Coeff.symbol "sqrt_kappa_inv")
    (hAdjoint :
      Hdagger ⟨0, by native_decide⟩ ⟨2, by native_decide⟩ =
        H ⟨2, by native_decide⟩ ⟨0, by native_decide⟩) :
    Hdagger ⟨0, by native_decide⟩ ⟨2, by native_decide⟩ =
      Coeff.symbol "sqrt_kappa_inv" := by

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 boundary hw kappa dagger uniform column contract”. A proposition-valued field is a requirement until a constructor supplies it. Uniform-column and adjoint-entry contract split for the focused dagger entry.

structure OneTermRobinGamma3BoundaryHWKappaDaggerUniformColumnContract where
  sourceAnchor : String
  embeddedInterface :
    OneTermRobinGamma3BoundaryHWKappaDaggerEmbeddedEntryInterface
  focusedSparseSlot : Nat
  focusedKappa : Nat
  sparseRegisterDimension : Nat
  uniformColumnRowIndex : Nat
  uniformColumnColIndex : Nat
  daggerRowIndex : Nat
  daggerColIndex : Nat

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary hw kappa dagger uniform column contract n 3”. Compiled contract split for row '0', column '2' of 'H_W^(kappa)^dagger'.

def oneTermRobinGamma3BoundaryHWKappaDaggerUniformColumnContract_n3 :
    OneTermRobinGamma3BoundaryHWKappaDaggerUniformColumnContract :=
  let interface :=
    oneTermRobinGamma3BoundaryHWKappaDaggerEmbeddedEntryInterface_n3
  {
    sourceAnchor :=
      "GHL2025 Eq. arbitrary sparcity, Definition def:block-encoding, Eq. ROBIN clarified boundary branch, Fig. 1-term ROBIN, and Shukla-Vedula 2024, arXiv:2506.20478"
    embeddedInterface := interface
    focusedSparseSlot := interface.focusedSparseSlot
    focusedKappa := interface.focusedKappa
    sparseRegisterDimension := interface.sparseRegisterDimension

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary hw kappa dagger uniform column contract n 3 transcript”; its local proof does not by itself complete the broader paper route. Transcript theorem for the uniform-column contract split.

theorem oneTermRobinGamma3BoundaryHWKappaDaggerUniformColumnContract_n3_transcript :
    let contract :=
      oneTermRobinGamma3BoundaryHWKappaDaggerUniformColumnContract_n3
    let interface :=
      oneTermRobinGamma3BoundaryHWKappaDaggerEmbeddedEntryInterface_n3
    contract.embeddedInterface = interface ∧
      contract.focusedSparseSlot = 2 ∧
      contract.focusedKappa = 7 ∧
      contract.sparseRegisterDimension = 8 ∧
      contract.uniformColumnRowIndex = 2 ∧
      contract.uniformColumnColIndex = 0 ∧

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary hw kappa dagger transpose matrix n 3”. Local transpose-style dagger for the focused symbolic 'H_W^(kappa)' matrix.

def oneTermRobinGamma3BoundaryHWKappaDaggerTransposeMatrix_n3
    (H : Matrix 8 8 Coeff) : Matrix 8 8 Coeff :=
  fun row col => H col row

/--
Focused adjoint-entry convention for the boundary `H_W^(kappa)` packet.

This proves only the matrix-interface convention
`H_W^(kappa)^dagger[0,2] = H_W^(kappa)[2,0]` for the local transpose-style
dagger.  It does not provide the cited clean-column amplitude.
-/

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary hw kappa dagger transpose entry convention n 3”; its local proof does not by itself complete the broader paper route. Focused adjoint-entry convention for the boundary 'H_W^(kappa)' packet.

theorem oneTermRobinGamma3BoundaryHWKappaDaggerTransposeEntryConvention_n3
    (H : Matrix 8 8 Coeff) :
    oneTermRobinGamma3BoundaryHWKappaDaggerTransposeMatrix_n3 H
        ⟨0, by native_decide⟩ ⟨2, by native_decide⟩ =
      H ⟨2, by native_decide⟩ ⟨0, by native_decide⟩ :=
  rfl

/--
Focused dagger-entry theorem under the external uniform-column contract.

The adjoint-entry convention is now supplied by the local transpose-style

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary hw kappa dagger entry from transpose uniform column n 3”; its local proof does not by itself complete the broader paper route. Focused dagger-entry theorem under the external uniform-column contract.

theorem oneTermRobinGamma3BoundaryHWKappaDaggerEntryFromTransposeUniformColumn_n3
    (H : Matrix 8 8 Coeff)
    (hUniform :
      H ⟨2, by native_decide⟩ ⟨0, by native_decide⟩ =
        Coeff.symbol "sqrt_kappa_inv") :
    oneTermRobinGamma3BoundaryHWKappaDaggerTransposeMatrix_n3 H
        ⟨0, by native_decide⟩ ⟨2, by native_decide⟩ =
      Coeff.symbol "sqrt_kappa_inv" :=
  oneTermRobinGamma3BoundaryHWKappaDaggerEntryFromUniformColumn_n3 H
    (oneTermRobinGamma3BoundaryHWKappaDaggerTransposeMatrix_n3 H)
    hUniform

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 boundary hw kappa dagger adjoint entry convention”. A proposition-valued field is a requirement until a constructor supplies it. Adjoint-entry convention packet for the focused 'H_W^(kappa)' dagger entry.

structure OneTermRobinGamma3BoundaryHWKappaDaggerAdjointEntryConvention where
  sourceAnchor : String
  uniformColumnContract :
    OneTermRobinGamma3BoundaryHWKappaDaggerUniformColumnContract
  focusedSparseSlot : Nat
  focusedKappa : Nat
  sparseRegisterDimension : Nat
  uniformColumnRowIndex : Nat
  uniformColumnColIndex : Nat
  daggerRowIndex : Nat
  daggerColIndex : Nat

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary hw kappa dagger adjoint entry convention n 3”. Compiled local adjoint-entry convention for the focused boundary branch.

def oneTermRobinGamma3BoundaryHWKappaDaggerAdjointEntryConvention_n3 :
    OneTermRobinGamma3BoundaryHWKappaDaggerAdjointEntryConvention :=
  let contract :=
    oneTermRobinGamma3BoundaryHWKappaDaggerUniformColumnContract_n3
  {
    sourceAnchor :=
      "GHL2025 Eq. arbitrary sparcity, Definition def:block-encoding, Eq. ROBIN clarified boundary branch, Fig. 1-term ROBIN, and QBE transpose-style symbolic matrix convention"
    uniformColumnContract := contract
    focusedSparseSlot := contract.focusedSparseSlot
    focusedKappa := contract.focusedKappa
    sparseRegisterDimension := contract.sparseRegisterDimension

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary hw kappa dagger adjoint entry convention n 3 transcript”; its local proof does not by itself complete the broader paper route. Transcript theorem for the local adjoint-entry convention packet.

theorem oneTermRobinGamma3BoundaryHWKappaDaggerAdjointEntryConvention_n3_transcript :
    let convention :=
      oneTermRobinGamma3BoundaryHWKappaDaggerAdjointEntryConvention_n3
    let contract :=
      oneTermRobinGamma3BoundaryHWKappaDaggerUniformColumnContract_n3
    convention.uniformColumnContract = contract ∧
      convention.focusedSparseSlot = 2 ∧
      convention.focusedKappa = 7 ∧
      convention.sparseRegisterDimension = 8 ∧
      convention.uniformColumnRowIndex = 2 ∧
      convention.uniformColumnColIndex = 0 ∧

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 boundary hw kappa clean column contract”. A proposition-valued field is a requirement until a constructor supplies it. External clean-column contract bridge for the focused 'H_W^(kappa)' entry.

structure OneTermRobinGamma3BoundaryHWKappaCleanColumnContract where
  sourceAnchor : String
  adjointConvention :
    OneTermRobinGamma3BoundaryHWKappaDaggerAdjointEntryConvention
  citedResultId : String
  focusedSparseSlot : Nat
  focusedKappa : Nat
  sparseRegisterDimension : Nat
  uniformColumnRowIndex : Nat
  uniformColumnColIndex : Nat
  daggerRowIndex : Nat

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary hw kappa clean column contract n 3”. Compiled clean-column contract bridge for the focused boundary branch.

def oneTermRobinGamma3BoundaryHWKappaCleanColumnContract_n3 :
    OneTermRobinGamma3BoundaryHWKappaCleanColumnContract :=
  let convention :=
    oneTermRobinGamma3BoundaryHWKappaDaggerAdjointEntryConvention_n3
  {
    sourceAnchor :=
      "GHL2025 Eq. arbitrary sparcity and Fig. 1-term ROBIN; cited-results row ShuklaVedula2024.HWkappaUniformSuperposition; arXiv:2506.20478"
    adjointConvention := convention
    citedResultId := "ShuklaVedula2024.HWkappaUniformSuperposition"
    focusedSparseSlot := convention.focusedSparseSlot
    focusedKappa := convention.focusedKappa

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary hw kappa clean column contract feeds transpose bridge n 3”; its local proof does not by itself complete the broader paper route. The clean-column contract is exactly the hypothesis consumed by the transpose dagger bridge.

theorem oneTermRobinGamma3BoundaryHWKappaCleanColumnContract_feedsTransposeBridge_n3
    (H : Matrix 8 8 Coeff)
    (hUniform :
      H ⟨oneTermRobinGamma3BoundaryHWKappaCleanColumnContract_n3.uniformColumnRowIndex,
          by native_decide⟩
        ⟨oneTermRobinGamma3BoundaryHWKappaCleanColumnContract_n3.uniformColumnColIndex,
          by native_decide⟩ =
        oneTermRobinGamma3BoundaryHWKappaCleanColumnContract_n3.expectedUniformColumnEntry) :
    oneTermRobinGamma3BoundaryHWKappaDaggerTransposeMatrix_n3 H
        ⟨oneTermRobinGamma3BoundaryHWKappaCleanColumnContract_n3.daggerRowIndex,
          by native_decide⟩

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary hw kappa clean column contract n 3 transcript”; its local proof does not by itself complete the broader paper route. Transcript theorem for the clean-column contract bridge.

theorem oneTermRobinGamma3BoundaryHWKappaCleanColumnContract_n3_transcript :
    let bridge :=
      oneTermRobinGamma3BoundaryHWKappaCleanColumnContract_n3
    let convention :=
      oneTermRobinGamma3BoundaryHWKappaDaggerAdjointEntryConvention_n3
    bridge.adjointConvention = convention ∧
      bridge.citedResultId =
        "ShuklaVedula2024.HWkappaUniformSuperposition" ∧
      bridge.focusedSparseSlot = 2 ∧
      bridge.focusedKappa = 7 ∧
      bridge.sparseRegisterDimension = 8 ∧

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 boundary clean column bra route contract”. A proposition-valued field is a requirement until a constructor supplies it. Route contract from the accepted clean-column input to the existing bra amplitude and factor-semantics obligations.

structure OneTermRobinGamma3BoundaryCleanColumnBraRouteContract where
  sourceAnchor : String
  cleanColumnContract : OneTermRobinGamma3BoundaryHWKappaCleanColumnContract
  braSourceMap : OneTermRobinGamma3BoundaryBraProjectionAmplitudeSourceMap
  factorContractMap : OneTermRobinGamma3BoundaryFactorSemanticsContractMap
  citedResultId : String
  focusedSparseSlot : Nat
  focusedKappa : Nat
  sparseRegisterDimension : Nat
  cleanBasisIndex : Nat
  uniformColumnRowIndex : Nat

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary clean column bra route contract n 3”. Compiled clean-column to bra-route contract for the focused boundary branch.

def oneTermRobinGamma3BoundaryCleanColumnBraRouteContract_n3 :
    OneTermRobinGamma3BoundaryCleanColumnBraRouteContract :=
  let cleanColumn :=
    oneTermRobinGamma3BoundaryHWKappaCleanColumnContract_n3
  let sourceMap :=
    oneTermRobinGamma3BoundaryBraProjectionAmplitudeSourceMap_n3
  let factorMap :=
    oneTermRobinGamma3BoundaryFactorSemanticsContractMap_n3
  {
    sourceAnchor :=
      "GHL2025 Eq. arbitrary sparcity, Definition def:block-encoding, Eq. ROBIN clarified boundary branch, Fig. 1-term ROBIN, and Shukla-Vedula 2024, arXiv:2506.20478"

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary clean column bra route contract feeds bra amplitude n 3”; its local proof does not by itself complete the broader paper route. The clean-column bridge feeds the expected bra-amplitude factor conditionally.

theorem oneTermRobinGamma3BoundaryCleanColumnBraRouteContract_feedsBraAmplitude_n3
    (H : Matrix 8 8 Coeff)
    (hUniform :
      H ⟨oneTermRobinGamma3BoundaryCleanColumnBraRouteContract_n3.uniformColumnRowIndex,
          by native_decide⟩
        ⟨oneTermRobinGamma3BoundaryCleanColumnBraRouteContract_n3.uniformColumnColIndex,
          by native_decide⟩ =
        oneTermRobinGamma3BoundaryCleanColumnBraRouteContract_n3.expectedUniformColumnEntry) :
    oneTermRobinGamma3BoundaryHWKappaDaggerTransposeMatrix_n3 H
        ⟨oneTermRobinGamma3BoundaryCleanColumnBraRouteContract_n3.daggerRowIndex,
          by native_decide⟩

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary clean column bra route contract n 3 transcript”; its local proof does not by itself complete the broader paper route. Transcript theorem for the clean-column to bra-route contract.

theorem oneTermRobinGamma3BoundaryCleanColumnBraRouteContract_n3_transcript :
    let route :=
      oneTermRobinGamma3BoundaryCleanColumnBraRouteContract_n3
    let cleanColumn :=
      oneTermRobinGamma3BoundaryHWKappaCleanColumnContract_n3
    let sourceMap :=
      oneTermRobinGamma3BoundaryBraProjectionAmplitudeSourceMap_n3
    let factorMap :=
      oneTermRobinGamma3BoundaryFactorSemanticsContractMap_n3
    route.cleanColumnContract = cleanColumn ∧
      route.braSourceMap = sourceMap ∧

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 boundary clean column factor semantics route”. A proposition-valued field is a requirement until a constructor supplies it. Under-contract route from the clean-column bra factor to factor semantics.

structure OneTermRobinGamma3BoundaryCleanColumnFactorSemanticsRoute where
  sourceAnchor : String
  cleanColumnRoute : OneTermRobinGamma3BoundaryCleanColumnBraRouteContract
  factorContractMap : OneTermRobinGamma3BoundaryFactorSemanticsContractMap
  focusedSparseSlot : Nat
  cleanBasisIndex : Nat
  uniformColumnRowIndex : Nat
  uniformColumnColIndex : Nat
  daggerRowIndex : Nat
  daggerColIndex : Nat
  expectedUniformColumnEntry : Coeff

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary clean column factor semantics route n 3”. Compiled clean-column to factor-semantics route for the focused boundary branch.

def oneTermRobinGamma3BoundaryCleanColumnFactorSemanticsRoute_n3 :
    OneTermRobinGamma3BoundaryCleanColumnFactorSemanticsRoute :=
  let cleanRoute :=
    oneTermRobinGamma3BoundaryCleanColumnBraRouteContract_n3
  let factorMap :=
    oneTermRobinGamma3BoundaryFactorSemanticsContractMap_n3
  {
    sourceAnchor :=
      "GHL2025 Eq. arbitrary sparcity, Definition def:block-encoding, Eq. ROBIN clarified boundary branch, Fig. 1-term ROBIN, and Shukla-Vedula 2024, arXiv:2506.20478"
    cleanColumnRoute := cleanRoute
    factorContractMap := factorMap

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary clean column factor semantics route eval n 3”; its local proof does not by itself complete the broader paper route. Conditional evaluation for the clean-column to factor-semantics route.

theorem oneTermRobinGamma3BoundaryCleanColumnFactorSemanticsRouteEval_n3
    (env : String → Rat)
    (H : Matrix 8 8 Coeff)
    (hUniform :
      H
        ⟨oneTermRobinGamma3BoundaryCleanColumnFactorSemanticsRoute_n3.uniformColumnRowIndex,
          by native_decide⟩
        ⟨oneTermRobinGamma3BoundaryCleanColumnFactorSemanticsRoute_n3.uniformColumnColIndex,
          by native_decide⟩ =
        oneTermRobinGamma3BoundaryCleanColumnFactorSemanticsRoute_n3.expectedUniformColumnEntry)
    (hND : env "N_D_inv" * env "N_D" = 1)

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary clean column factor semantics route n 3 transcript”; its local proof does not by itself complete the broader paper route. Transcript theorem for the clean-column to factor-semantics route.

theorem oneTermRobinGamma3BoundaryCleanColumnFactorSemanticsRoute_n3_transcript :
    let route :=
      oneTermRobinGamma3BoundaryCleanColumnFactorSemanticsRoute_n3
    let cleanRoute :=
      oneTermRobinGamma3BoundaryCleanColumnBraRouteContract_n3
    let factorMap :=
      oneTermRobinGamma3BoundaryFactorSemanticsContractMap_n3
    route.cleanColumnRoute = cleanRoute ∧
      route.factorContractMap = factorMap ∧
      route.focusedSparseSlot = 2 ∧
      route.cleanBasisIndex = 32 ∧

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 boundary product under contracts route”. A proposition-valued field is a requirement until a constructor supplies it. Product-under-contracts route for the focused boundary branch.

structure OneTermRobinGamma3BoundaryProductUnderContractsRoute where
  sourceAnchor : String
  cleanColumnFactorRoute :
    OneTermRobinGamma3BoundaryCleanColumnFactorSemanticsRoute
  focusedSystemRow : Nat
  focusedSystemColumn : Nat
  focusedSparseSlot : Nat
  cleanBasisIndex : Nat
  expectedBraAmplitudeFactor : Coeff
  projectedBranchProduct : Coeff
  expectedTargetEntry : Coeff

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary product under contracts route n 3”. Compiled product-under-contracts route for 'oneTermRobinGamma3ProductToCoefficientObligation 3 0 0'.

def oneTermRobinGamma3BoundaryProductUnderContractsRoute_n3 :
    OneTermRobinGamma3BoundaryProductUnderContractsRoute :=
  let route := oneTermRobinGamma3BoundaryCleanColumnFactorSemanticsRoute_n3
  {
    sourceAnchor :=
      "GHL2025 Eq. ROBIN clarified boundary gamma3 branch, Theorem one-term block-encoding, Definition def:block-encoding, Fig. 1-term ROBIN, and cited LCU.StandardBlockEncoding"
    cleanColumnFactorRoute := route
    focusedSystemRow := 0
    focusedSystemColumn := 0
    focusedSparseSlot := route.focusedSparseSlot
    cleanBasisIndex := route.cleanBasisIndex

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary product under contracts eval n 3”; its local proof does not by itself complete the broader paper route. Conditional product-under-contracts evaluation for the focused boundary route.

theorem oneTermRobinGamma3BoundaryProductUnderContractsEval_n3
    (env : String → Rat)
    (H : Matrix 8 8 Coeff)
    (hUniform :
      H
        ⟨oneTermRobinGamma3BoundaryProductUnderContractsRoute_n3.cleanColumnFactorRoute.uniformColumnRowIndex,
          by native_decide⟩
        ⟨oneTermRobinGamma3BoundaryProductUnderContractsRoute_n3.cleanColumnFactorRoute.uniformColumnColIndex,
          by native_decide⟩ =
        oneTermRobinGamma3BoundaryProductUnderContractsRoute_n3.cleanColumnFactorRoute.expectedUniformColumnEntry)
    (hND : env "N_D_inv" * env "N_D" = 1)

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary product under contracts route n 3 transcript”; its local proof does not by itself complete the broader paper route. Transcript theorem for the product-under-contracts route.

theorem oneTermRobinGamma3BoundaryProductUnderContractsRoute_n3_transcript :
    let productRoute :=
      oneTermRobinGamma3BoundaryProductUnderContractsRoute_n3
    let factorRoute :=
      oneTermRobinGamma3BoundaryCleanColumnFactorSemanticsRoute_n3
    productRoute.cleanColumnFactorRoute = factorRoute ∧
      productRoute.focusedSystemRow = 0 ∧
      productRoute.focusedSystemColumn = 0 ∧
      productRoute.focusedSparseSlot = 2 ∧
      productRoute.cleanBasisIndex = 32 ∧
      productRoute.expectedBraAmplitudeFactor =

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary finite projection block entry index n 3”; its local proof does not by itself complete the broader paper route. Finite signal-block index lemma for the focused product/projection bridge.

theorem oneTermRobinGamma3BoundaryFiniteProjectionBlockEntryIndex_n3 :
    let p := oneTermParameters 3
    let contract := oneTermRobinFiniteBlockCompositionContract 3
    let sysRow : Fin (gridSize 3) := ⟨0, by native_decide⟩
    let sysCol : Fin (gridSize 3) := ⟨0, by native_decide⟩
    let blockRow : Fin
        (qubitDim (GHL2025.effectiveRobinSignalQubits p) * gridSize 3) :=
      ⟨signalSystemBlockRowIndex (gridSize 3)
          contract.expectedTarget.signalIndex.val sysRow.val,
        signalSystemBlockRowIndex_lt
          contract.expectedTarget.signalIndex sysRow⟩

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 boundary finite projection product bridge”. A proposition-valued field is a requirement until a constructor supplies it. Finite projection/product bridge packet for the focused boundary branch.

structure OneTermRobinGamma3BoundaryFiniteProjectionProductBridge where
  sourceAnchor : String
  productRoute : OneTermRobinGamma3BoundaryProductUnderContractsRoute
  focusedSystemRow : Nat
  focusedSystemColumn : Nat
  focusedSparseSlot : Nat
  signalIndexValue : Nat
  signalBlockRowIndex : Nat
  signalBlockColumnIndex : Nat
  branchBasisIndex : Nat
  signalBlockEntryFormula : String

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary finite projection product bridge n 3”. Compiled finite projection/product bridge for 'oneTermRobinGamma3ProductToCoefficientObligation 3 0 0'.

def oneTermRobinGamma3BoundaryFiniteProjectionProductBridge_n3 :
    OneTermRobinGamma3BoundaryFiniteProjectionProductBridge :=
  let p := oneTermParameters 3
  let productRoute :=
    oneTermRobinGamma3BoundaryProductUnderContractsRoute_n3
  let contract := oneTermRobinFiniteBlockCompositionContract 3
  {
    sourceAnchor :=
      "GHL2025 Definition def:block-encoding, Eq. ROBIN clarified boundary gamma3 branch, Fig. 1-term ROBIN, and LCU.StandardBlockEncoding cited-results row"
    productRoute := productRoute
    focusedSystemRow := 0

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary finite projection product bridge n 3 transcript”; its local proof does not by itself complete the broader paper route. Transcript theorem for the finite projection/product bridge packet.

theorem oneTermRobinGamma3BoundaryFiniteProjectionProductBridge_n3_transcript :
    let bridge :=
      oneTermRobinGamma3BoundaryFiniteProjectionProductBridge_n3
    let productRoute :=
      oneTermRobinGamma3BoundaryProductUnderContractsRoute_n3
    bridge.productRoute = productRoute ∧
      bridge.focusedSystemRow = 0 ∧
      bridge.focusedSystemColumn = 0 ∧
      bridge.focusedSparseSlot = 2 ∧
      bridge.signalIndexValue = 0 ∧
      bridge.signalBlockRowIndex = 0 ∧

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 boundary branch decomposition slot 2”. A proposition-valued field is a requirement until a constructor supplies it. Branch-decomposition interface for the focused slot-'2' boundary product.

structure OneTermRobinGamma3BoundaryBranchDecompositionSlot2 where
  sourceAnchor : String
  finiteBridge : OneTermRobinGamma3BoundaryFiniteProjectionProductBridge
  focusedSystemRow : Nat
  focusedSystemColumn : Nat
  focusedSparseSlot : Nat
  signalBlockRowIndex : Nat
  signalBlockColumnIndex : Nat
  branchRowIndex : Nat
  branchColumnIndex : Nat
  signalBlockEntryFormula : String

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary branch decomposition slot 2 n 3”. Compiled branch-decomposition interface for the fixed boundary branch.

def oneTermRobinGamma3BoundaryBranchDecompositionSlot2_n3 :
    OneTermRobinGamma3BoundaryBranchDecompositionSlot2 :=
  let bridge := oneTermRobinGamma3BoundaryFiniteProjectionProductBridge_n3
  {
    sourceAnchor :=
      "GHL2025 Eq. ROBIN clarified boundary gamma3 branch, Definition def:block-encoding, Fig. 1-term ROBIN, and QBE finite projection/summation interface"
    finiteBridge := bridge
    focusedSystemRow := bridge.focusedSystemRow
    focusedSystemColumn := bridge.focusedSystemColumn
    focusedSparseSlot := bridge.focusedSparseSlot
    signalBlockRowIndex := bridge.signalBlockRowIndex

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary branch decomposition slot 2 n 3 transcript”; its local proof does not by itself complete the broader paper route. Transcript theorem for the slot-'2' branch-decomposition interface.

theorem oneTermRobinGamma3BoundaryBranchDecompositionSlot2_n3_transcript :
    let packet :=
      oneTermRobinGamma3BoundaryBranchDecompositionSlot2_n3
    let bridge :=
      oneTermRobinGamma3BoundaryFiniteProjectionProductBridge_n3
    packet.finiteBridge = bridge ∧
      packet.focusedSystemRow = 0 ∧
      packet.focusedSystemColumn = 0 ∧
      packet.focusedSparseSlot = 2 ∧
      packet.signalBlockRowIndex = 0 ∧
      packet.signalBlockColumnIndex = 0 ∧

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 boundary projection summation target”. A proposition-valued field is a requirement until a constructor supplies it. Typed projection-summation target for the focused slot-'2' boundary packet.

structure OneTermRobinGamma3BoundaryProjectionSummationTarget where
  sourceAnchor : String
  branchPacket : OneTermRobinGamma3BoundaryBranchDecompositionSlot2
  focusedSystemRow : Nat
  focusedSystemColumn : Nat
  focusedSparseSlot : Nat
  signalBlockRowIndex : Nat
  signalBlockColumnIndex : Nat
  branchRowIndex : Nat
  branchColumnIndex : Nat
  signalBlockEntry : Coeff

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary projection summation target n 3”. Compiled typed target for the missing branch projection/summation theorem.

def oneTermRobinGamma3BoundaryProjectionSummationTarget_n3 :
    OneTermRobinGamma3BoundaryProjectionSummationTarget :=
  let packet := oneTermRobinGamma3BoundaryBranchDecompositionSlot2_n3
  let p := oneTermParameters 3
  let contract := oneTermRobinFiniteBlockCompositionContract 3
  let sysRow : Fin (gridSize 3) := ⟨0, by native_decide⟩
  let sysCol : Fin (gridSize 3) := ⟨0, by native_decide⟩
  let blockRow : Fin
      (qubitDim (GHL2025.effectiveRobinSignalQubits p) * gridSize 3) :=
    ⟨signalSystemBlockRowIndex (gridSize 3)
        contract.expectedTarget.signalIndex.val sysRow.val,

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary projection summation target n 3 transcript”; its local proof does not by itself complete the broader paper route. Transcript theorem for the typed projection-summation target.

theorem oneTermRobinGamma3BoundaryProjectionSummationTarget_n3_transcript :
    let target :=
      oneTermRobinGamma3BoundaryProjectionSummationTarget_n3
    let packet :=
      oneTermRobinGamma3BoundaryBranchDecompositionSlot2_n3
    target.branchPacket = packet ∧
      target.focusedSystemRow = packet.focusedSystemRow ∧
      target.focusedSystemColumn = packet.focusedSystemColumn ∧
      target.focusedSparseSlot = packet.focusedSparseSlot ∧
      target.signalBlockEntryFormula =
        "contract.expectedTarget.blockMatrix[0,0]" ∧

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 boundary branch entry selection”. A proposition-valued field is a requirement until a constructor supplies it. Conditional branch-entry selection packet for the focused slot-'2' boundary target.

structure OneTermRobinGamma3BoundaryBranchEntrySelection where
  sourceAnchor : String
  projectionTarget : OneTermRobinGamma3BoundaryProjectionSummationTarget
  focusedSparseSlot : Nat
  branchRowIndex : Nat
  branchColumnIndex : Nat
  projectionAmplitudeFactor : Coeff
  selectedBranchEntryFormula : String
  routeProjectedProductFormula : String
  correctedEntryHypothesis : SemanticObligation
  ketAmplitudeObligation : SemanticObligation

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary branch entry selection n 3”. Compiled branch-entry selection interface for the focused projection target.

def oneTermRobinGamma3BoundaryBranchEntrySelection_n3 :
    OneTermRobinGamma3BoundaryBranchEntrySelection :=
  let target := oneTermRobinGamma3BoundaryProjectionSummationTarget_n3
  let amplitude := oneTermRobinGamma3BoundaryProjectionAmplitudeSemantics_n3
  let corrected := oneTermRobinGamma3BoundaryCorrectedCoefficientInterface_n3
  {
    sourceAnchor :=
      "GHL2025 Eq. ROBIN clarified boundary gamma3 branch, Eq. arbitrary sparcity, Definition def:block-encoding, Fig. 1-term ROBIN, and Shukla-Vedula contract row"
    projectionTarget := target
    focusedSparseSlot := target.focusedSparseSlot
    branchRowIndex := target.branchRowIndex

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary branch entry selection eval n 3”; its local proof does not by itself complete the broader paper route. Conditional branch-entry selection for the focused projection target.

theorem oneTermRobinGamma3BoundaryBranchEntrySelectionEval_n3
    (env : String → Rat)
    (hentry :
      env "boundary_cos_half_0_2" =
        Coeff.evalWith env
          (GHL2025.boundaryRotationNormalizedCoefficient
            (oneTermParameters 3) 0 2)) :
    let selection := oneTermRobinGamma3BoundaryBranchEntrySelection_n3
    Coeff.evalWith env
        (Coeff.mul
          (oneTermRobinGamma3BoundarySevenGateMatrix_n3

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary branch entry selection n 3 transcript”; its local proof does not by itself complete the broader paper route. Transcript theorem for the branch-entry selection packet.

theorem oneTermRobinGamma3BoundaryBranchEntrySelection_n3_transcript :
    let selection := oneTermRobinGamma3BoundaryBranchEntrySelection_n3
    let target := oneTermRobinGamma3BoundaryProjectionSummationTarget_n3
    selection.projectionTarget = target ∧
      selection.focusedSparseSlot = 2 ∧
      selection.branchRowIndex = 32 ∧
      selection.branchColumnIndex = 32 ∧
      selection.projectionAmplitudeFactor =
        oneTermRobinGamma3BoundaryProjectionAmplitudeSemantics_n3.combinedAmplitudeFactor ∧
      selection.projectionAmplitudeFactor =
        Coeff.mul (Coeff.symbol "sqrt_kappa_inv")

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 boundary projection summation obstruction”. A proposition-valued field is a requirement until a constructor supplies it. Typed obstruction for the remaining finite projection/summation step.

structure OneTermRobinGamma3BoundaryProjectionSummationObstruction where
  sourceAnchor : String
  branchEntrySelection : OneTermRobinGamma3BoundaryBranchEntrySelection
  projectionTarget : OneTermRobinGamma3BoundaryProjectionSummationTarget
  slotDomain : List Nat
  slotDomainCardinality : Nat
  focusedSparseSlot : Nat
  focusedSlotInDomain : Bool
  signalBlockEntry : Coeff
  selectedBranchEntry : Coeff
  projectionAmplitudeFactor : Coeff

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary projection summation obstruction n 3”. Compiled typed obstruction for the focused boundary projection/summation bridge.

def oneTermRobinGamma3BoundaryProjectionSummationObstruction_n3 :
    OneTermRobinGamma3BoundaryProjectionSummationObstruction :=
  let selection := oneTermRobinGamma3BoundaryBranchEntrySelection_n3
  let target := oneTermRobinGamma3BoundaryProjectionSummationTarget_n3
  let slots := [0, 1, 2, 3, 4, 5, 6]
  {
    sourceAnchor :=
      "GHL2025 Definition def:block-encoding, Eq. ROBIN clarified boundary gamma3 branch, Fig. 1-term ROBIN, and QBE finite projection/summation interface"
    branchEntrySelection := selection
    projectionTarget := target
    slotDomain := slots

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary projection summation obstruction selected slot eval n 3”; its local proof does not by itself complete the broader paper route. The new obstruction reuses the accepted branch-entry selection lemma.

theorem oneTermRobinGamma3BoundaryProjectionSummationObstruction_selectedSlotEval_n3
    (env : String → Rat)
    (hentry :
      env "boundary_cos_half_0_2" =
        Coeff.evalWith env
          (GHL2025.boundaryRotationNormalizedCoefficient
            (oneTermParameters 3) 0 2)) :
    let obstruction :=
      oneTermRobinGamma3BoundaryProjectionSummationObstruction_n3
    Coeff.evalWith env obstruction.selectedSlotContribution =
      Coeff.evalWith env obstruction.projectionTarget.projectedBranchProduct := by

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary projection summation obstruction n 3 transcript”; its local proof does not by itself complete the broader paper route. Transcript theorem for the typed projection/summation obstruction.

theorem oneTermRobinGamma3BoundaryProjectionSummationObstruction_n3_transcript :
    let obstruction :=
      oneTermRobinGamma3BoundaryProjectionSummationObstruction_n3
    let selection := oneTermRobinGamma3BoundaryBranchEntrySelection_n3
    let target := oneTermRobinGamma3BoundaryProjectionSummationTarget_n3
    obstruction.branchEntrySelection = selection ∧
      obstruction.projectionTarget = target ∧
      obstruction.slotDomain = [0, 1, 2, 3, 4, 5, 6] ∧
      obstruction.slotDomainCardinality = 7 ∧
      obstruction.focusedSparseSlot = 2 ∧
      obstruction.focusedSlotInDomain = true ∧

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary branch contribution focused slot”. Focused sparse slot for the branch-contribution interface.

def oneTermRobinGamma3BoundaryBranchContributionFocusedSlot : Fin 7 :=
  ⟨2, by native_decide⟩

/--
Typed sparse-branch sum over the seven one-term Robin sparse slots.

This is intentionally a project-local `List.finRange` fold instead of a
`Finset.sum`, because `Coeff` is a syntactic coefficient language rather than
an additive commutative monoid.  It provides the Lean type that the missing
projection/summation theorem must target.
-/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary branch contribution sum”. Typed sparse-branch sum over the seven one-term Robin sparse slots.

def oneTermRobinGamma3BoundaryBranchContributionSum
    (branchContribution : Fin 7 → Coeff) : Coeff :=
  (List.finRange 7).foldl (fun acc s => acc + branchContribution s) 0

/--
Placeholder branch-contribution family for the focused projection/summation
interface.

Only slot `2` is identified with the already compiled selected contribution.
The other slots remain opaque symbolic placeholders; this definition does not
assert that their sum is the signal-zero block entry.

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary branch contribution placeholder n 3”. Placeholder branch-contribution family for the focused projection/summation interface.

def oneTermRobinGamma3BoundaryBranchContributionPlaceholder_n3
    (obstruction : OneTermRobinGamma3BoundaryProjectionSummationObstruction) :
    Fin 7 → Coeff :=
  fun s =>
    if s = oneTermRobinGamma3BoundaryBranchContributionFocusedSlot then
      obstruction.selectedSlotContribution
    else
      Coeff.symbol "gamma3_boundary_other_branch"

/--
Typed branch-contribution family required by the finite projection/summation

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 boundary branch contribution family”. A proposition-valued field is a requirement until a constructor supplies it. Typed branch-contribution family required by the finite projection/summation bridge.

structure OneTermRobinGamma3BoundaryBranchContributionFamily where
  sourceAnchor : String
  projectionObstruction :
    OneTermRobinGamma3BoundaryProjectionSummationObstruction
  branchContribution : Fin 7 → Coeff
  focusedSparseSlot : Fin 7
  selectedSlotContribution : Coeff
  selectedSlotStatement : Prop
  signalBlockEntry : Coeff
  branchContributionSum : Coeff
  projectionSummationStatement : Prop

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary branch contribution family n 3”. Compiled branch-contribution family for the focused 'n = 3' boundary branch.

def oneTermRobinGamma3BoundaryBranchContributionFamily_n3 :
    OneTermRobinGamma3BoundaryBranchContributionFamily :=
  let obstruction :=
    oneTermRobinGamma3BoundaryProjectionSummationObstruction_n3
  let branchContribution :=
    oneTermRobinGamma3BoundaryBranchContributionPlaceholder_n3 obstruction
  let focusedSlot :=
    oneTermRobinGamma3BoundaryBranchContributionFocusedSlot
  let branchSum :=
    oneTermRobinGamma3BoundaryBranchContributionSum branchContribution
  {

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary branch contribution selected slot n 3”; its local proof does not by itself complete the broader paper route. The typed branch-contribution family selects the accepted slot-'2' contribution.

theorem oneTermRobinGamma3BoundaryBranchContribution_selectedSlot_n3 :
    oneTermRobinGamma3BoundaryBranchContributionFamily_n3.selectedSlotStatement := by

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 boundary branch contribution obstruction”. A proposition-valued field is a requirement until a constructor supplies it. Typed obstruction after introducing the branch-contribution family.

structure OneTermRobinGamma3BoundaryBranchContributionObstruction where
  sourceAnchor : String
  family : OneTermRobinGamma3BoundaryBranchContributionFamily
  projectionObstruction :
    OneTermRobinGamma3BoundaryProjectionSummationObstruction
  selectedSlotTheorem : String
  projectionSummationTheoremTarget : String
  branchContributionFamilyAvailable : Bool
  selectedSlotTheoremCompiled : Bool
  projectionSummationStatementTyped : Bool
  projectionSummationTheoremAvailable : Bool

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary branch contribution obstruction n 3”. Current obstruction for the focused projection/summation bridge after the branch-contribution family has been made a typed Lean interface.

def oneTermRobinGamma3BoundaryBranchContributionObstruction_n3 :
    OneTermRobinGamma3BoundaryBranchContributionObstruction :=
  let family := oneTermRobinGamma3BoundaryBranchContributionFamily_n3
  {
    sourceAnchor :=
      "GHL2025 Definition def:block-encoding, Eq. ROBIN clarified boundary gamma3 branch, and QBE finite sparse-branch summation interface"
    family := family
    projectionObstruction :=
      oneTermRobinGamma3BoundaryProjectionSummationObstruction_n3
    selectedSlotTheorem := family.selectedSlotTheorem
    projectionSummationTheoremTarget :=

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary branch contribution obstruction n 3 transcript”; its local proof does not by itself complete the broader paper route. Transcript theorem for the branch-contribution-family obstruction.

theorem oneTermRobinGamma3BoundaryBranchContributionObstruction_n3_transcript :
    let obstruction :=
      oneTermRobinGamma3BoundaryBranchContributionObstruction_n3
    let family :=
      oneTermRobinGamma3BoundaryBranchContributionFamily_n3
    obstruction.family = family ∧
      family.projectionObstruction =
        oneTermRobinGamma3BoundaryProjectionSummationObstruction_n3 ∧
      family.focusedSparseSlot =
        oneTermRobinGamma3BoundaryBranchContributionFocusedSlot ∧
      family.focusedSparseSlot.val = 2 ∧

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary backend branch contribution predicate n 3”. Predicate that a backend-sourced sparse-branch contribution family must satisfy for the focused boundary projection/summation theorem.

def oneTermRobinGamma3BoundaryBackendBranchContributionPredicate_n3
    (branchContribution : Fin 7 → Coeff) : Prop :=
  branchContribution oneTermRobinGamma3BoundaryBranchContributionFocusedSlot =
      oneTermRobinGamma3BoundaryProjectionSummationObstruction_n3.selectedSlotContribution ∧
    oneTermRobinGamma3BoundaryProjectionSummationObstruction_n3.signalBlockEntry =
      oneTermRobinGamma3BoundaryBranchContributionSum branchContribution

/--
Smallest backend field still missing from the focused projection bridge.

The previous packet supplied a placeholder `branchContribution` family so Lean

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 boundary backend projection summation field target”. A proposition-valued field is a requirement until a constructor supplies it. Smallest backend field still missing from the focused projection bridge.

structure OneTermRobinGamma3BoundaryBackendProjectionSummationFieldTarget where
  sourceAnchor : String
  family : OneTermRobinGamma3BoundaryBranchContributionFamily
  projectionObstruction :
    OneTermRobinGamma3BoundaryProjectionSummationObstruction
  projectionTarget : OneTermRobinGamma3BoundaryProjectionSummationTarget
  backendBranchContributionPredicate : (Fin 7 → Coeff) → Prop
  backendFieldExpectedOwner : String
  backendFieldLeanType : String
  requiredSelectedSlotTheorem : String
  requiredProjectionSummationTheorem : String

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary backend projection summation field target n 3”. Concrete backend-field target for the focused 'n = 3' boundary branch.

def oneTermRobinGamma3BoundaryBackendProjectionSummationFieldTarget_n3 :
    OneTermRobinGamma3BoundaryBackendProjectionSummationFieldTarget :=
  let family := oneTermRobinGamma3BoundaryBranchContributionFamily_n3
  let obstruction := oneTermRobinGamma3BoundaryProjectionSummationObstruction_n3
  {
    sourceAnchor :=
      "GHL2025 Definition def:block-encoding, Eq. ROBIN clarified boundary gamma3 branch, Fig. 1-term ROBIN, and QBE BlockExtractionTarget projection backend"
    family := family
    projectionObstruction := obstruction
    projectionTarget := obstruction.projectionTarget
    backendBranchContributionPredicate :=

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary block extraction branch contribution target n 3”. Generic block-extraction branch-contribution target for the focused boundary entry.

def oneTermRobinGamma3BoundaryBlockExtractionBranchContributionTarget_n3 :
    BlockExtractionBranchContributionTarget Coeff
      (gridSize 3) (gridSize 3)
      (qubitDim (GHL2025.effectiveRobinSignalQubits (oneTermParameters 3)))
      7 :=
  let contract := oneTermRobinFiniteBlockCompositionContract 3
  let family := oneTermRobinGamma3BoundaryBranchContributionFamily_n3
  let sysRow : Fin (gridSize 3) := ⟨0, by native_decide⟩
  let sysCol : Fin (gridSize 3) := ⟨0, by native_decide⟩
  {
    extractionTarget := contract.expectedTarget

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 boundary block extraction backend gap”. A proposition-valued field is a requirement until a constructor supplies it. Smallest obstruction after inspecting the current 'BlockExtractionTarget' backend.

structure OneTermRobinGamma3BoundaryBlockExtractionBackendGap where
  sourceAnchor : String
  backendFieldTarget :
    OneTermRobinGamma3BoundaryBackendProjectionSummationFieldTarget
  expectedTarget :
    BlockExtractionTarget Coeff (gridSize 3) (gridSize 3)
      (qubitDim (GHL2025.effectiveRobinSignalQubits (oneTermParameters 3)))
  signalBlockEntry : Coeff
  unitaryEntry : Coeff
  blockProjectionObligation : SemanticObligation
  blockCorrectObligation : SemanticObligation

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary block extraction backend gap n 3”. Concrete backend gap for the focused 'n = 3' boundary branch.

def oneTermRobinGamma3BoundaryBlockExtractionBackendGap_n3 :
    OneTermRobinGamma3BoundaryBlockExtractionBackendGap :=
  let backendTarget :=
    oneTermRobinGamma3BoundaryBackendProjectionSummationFieldTarget_n3
  let contract := oneTermRobinFiniteBlockCompositionContract 3
  {
    sourceAnchor :=
      "GHL2025 Definition def:block-encoding, Eq. ROBIN clarified boundary gamma3 branch, and QBE BlockExtractionTarget fields"
    backendFieldTarget := backendTarget
    expectedTarget := contract.expectedTarget
    signalBlockEntry := backendTarget.projectionTarget.signalBlockEntry

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary block extraction backend gap n 3 transcript”; its local proof does not by itself complete the broader paper route. Transcript theorem for the block-extraction backend gap.

theorem oneTermRobinGamma3BoundaryBlockExtractionBackendGap_n3_transcript :
    let gap := oneTermRobinGamma3BoundaryBlockExtractionBackendGap_n3
    let backendTarget :=
      oneTermRobinGamma3BoundaryBackendProjectionSummationFieldTarget_n3
    let contract := oneTermRobinFiniteBlockCompositionContract 3
    gap.backendFieldTarget = backendTarget ∧
      gap.expectedTarget = contract.expectedTarget ∧
      gap.signalBlockEntry = backendTarget.projectionTarget.signalBlockEntry ∧
      gap.unitaryEntry = backendTarget.projectionTarget.signalUnitaryEntry ∧
      gap.signalBlockEntry = gap.unitaryEntry ∧
      gap.blockProjectionObligation =

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary backend branch full index n 3”. Full-basis branch index map for the focused 'n = 3' boundary backend packet.

def oneTermRobinGamma3BoundaryBackendBranchFullIndex_n3
    (s : Fin 7) :
    Fin (qubitDim (GHL2025.oneTermRobinTotalQubits (oneTermParameters 3))) :=
  ⟨oneTermRobinGamma3PaperBasisIndex (oneTermParameters 3) s.val 0, by
    have hs : s.val <= 6 := Nat.le_of_lt_succ s.isLt
    have hbasis :
        oneTermRobinGamma3PaperBasisIndex (oneTermParameters 3) s.val 0 =
          s.val * 16 := by

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary backend branch full index selected n 3”; its local proof does not by itself complete the broader paper route. The backend branch-index map sends the focused slot '2' to the accepted clean branch basis index '32'.

theorem oneTermRobinGamma3BoundaryBackendBranchFullIndex_selected_n3 :
    let idx :=
      oneTermRobinGamma3BoundaryBackendBranchFullIndex_n3
        oneTermRobinGamma3BoundaryBranchContributionFocusedSlot
    idx.val = 32 ∧ idx = oneTermRobinGamma3BoundaryPrefixSource_n3 := by

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary backend branch full index slot zero n 3”; its local proof does not by itself complete the broader paper route. The backend branch-index map sends sparse slot '0' to the active signal-zero full basis index '0'.

theorem oneTermRobinGamma3BoundaryBackendBranchFullIndex_slotZero_n3 :
    let idx :=
      oneTermRobinGamma3BoundaryBackendBranchFullIndex_n3
        ⟨0, by native_decide⟩
    idx.val = 0 ∧ idx = oneTermRobinGamma3BoundaryPrefixRow0_n3 := by

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary backend branch full index value n 3”; its local proof does not by itself complete the broader paper route. The all-slot backend branch-index map embeds sparse slot 's' at full basis index '16 * s'.

theorem oneTermRobinGamma3BoundaryBackendBranchFullIndex_value_n3
    (s : Fin 7) :
    (oneTermRobinGamma3BoundaryBackendBranchFullIndex_n3 s).val =
      s.val * 16 := by

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary backend branch full index injective n 3”; its local proof does not by itself complete the broader paper route. The seven backend sparse slots occupy distinct full-basis indices.

theorem oneTermRobinGamma3BoundaryBackendBranchFullIndex_injective_n3 :
    Function.Injective oneTermRobinGamma3BoundaryBackendBranchFullIndex_n3 := by

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary backend slot one dagger after swap zero n 3”; its local proof does not by itself complete the broader paper route. Slot-'1' clean path support mismatch for the backend diagonal branch.

theorem oneTermRobinGamma3BoundaryBackendSlotOneDaggerAfterSwap_zero_n3 :
    let p := oneTermRobinGamma3BoundaryPrefixParameters_n3
    let slotOne :=
      oneTermRobinGamma3BoundaryBackendBranchFullIndex_n3
        ⟨1, by native_decide⟩
    let afterForward : Fin oneTermRobinGamma3BoundaryPrefixDim_n3 :=
      ⟨112, by native_decide⟩
    let afterSwap : Fin oneTermRobinGamma3BoundaryPrefixDim_n3 :=
      ⟨14, by native_decide⟩
    slotOne.val = 16 ∧
      GHL2025.bandedSparseAccessPaperImage p slotOne.val =

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary backend selected branch summand formula n 3”; its local proof does not by itself complete the broader paper route. The selected contribution in the generic branch target is the already compiled slot-'2' seven-gate summand formula.

theorem oneTermRobinGamma3BoundaryBackendSelectedBranchSummandFormula_n3 :
    let target :=
      oneTermRobinGamma3BoundaryBlockExtractionBranchContributionTarget_n3
    target.selectedContribution =
      Coeff.mul
        (oneTermRobinGamma3BoundarySevenGateMatrix_n3
          oneTermRobinGamma3BoundaryPrefixSource_n3
          oneTermRobinGamma3BoundaryPrefixSource_n3)
        oneTermRobinGamma3BoundaryBranchEntrySelection_n3.projectionAmplitudeFactor := by

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 boundary backend branch index map obstruction”. A proposition-valued field is a requirement until a constructor supplies it. Narrow obstruction after adding the branch-to-full-index map.

structure OneTermRobinGamma3BoundaryBackendBranchIndexMapObstruction where
  sourceAnchor : String
  backendGap : OneTermRobinGamma3BoundaryBlockExtractionBackendGap
  branchContributionTarget :
    BlockExtractionBranchContributionTarget Coeff
      (gridSize 3) (gridSize 3)
      (qubitDim (GHL2025.effectiveRobinSignalQubits (oneTermParameters 3)))
      7
  branchFullIndex :
    Fin 7 →
      Fin (qubitDim (GHL2025.oneTermRobinTotalQubits (oneTermParameters 3)))

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary backend branch index map obstruction n 3”. Focused 'n = 3' backend branch-index map obstruction.

def oneTermRobinGamma3BoundaryBackendBranchIndexMapObstruction_n3 :
    OneTermRobinGamma3BoundaryBackendBranchIndexMapObstruction :=
  let gap := oneTermRobinGamma3BoundaryBlockExtractionBackendGap_n3
  let selected :=
    oneTermRobinGamma3BoundaryBranchContributionFocusedSlot
  {
    sourceAnchor :=
      "GHL2025 Definition def:block-encoding, Eq. ROBIN clarified boundary gamma3 branch, Fig. 1-term ROBIN, and QBE finite projection backend branch-index map"
    backendGap := gap
    branchContributionTarget := gap.branchContributionTarget
    branchFullIndex :=

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary backend branch contribution n 3”. All-slot backend summand formula for the focused 'n = 3' boundary packet.

def oneTermRobinGamma3BoundaryBackendBranchContribution_n3
    (s : Fin 7) : Coeff :=
  Coeff.mul
    (oneTermRobinGamma3BoundarySevenGateMatrix_n3
      (oneTermRobinGamma3BoundaryBackendBranchFullIndex_n3 s)
      (oneTermRobinGamma3BoundaryBackendBranchFullIndex_n3 s))
    oneTermRobinGamma3BoundaryBranchEntrySelection_n3.projectionAmplitudeFactor

/--
The all-slot backend summand formula selects the accepted slot-`2`
contribution.

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary backend branch contribution selected n 3”; its local proof does not by itself complete the broader paper route. The all-slot backend summand formula selects the accepted slot-'2' contribution.

theorem oneTermRobinGamma3BoundaryBackendBranchContribution_selected_n3 :
    oneTermRobinGamma3BoundaryBackendBranchContribution_n3
        oneTermRobinGamma3BoundaryBranchContributionFocusedSlot =
      oneTermRobinGamma3BoundaryProjectionSummationObstruction_n3.selectedSlotContribution := by

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary backend branch contribution slot zero n 3”; its local proof does not by itself complete the broader paper route. The slot-'0' backend summand is the active '[0,0]' seven-gate diagonal multiplied by the sparse-register projection amplitude factor.

theorem oneTermRobinGamma3BoundaryBackendBranchContribution_slotZero_n3 :
    oneTermRobinGamma3BoundaryBackendBranchContribution_n3
        ⟨0, by native_decide⟩ =
      Coeff.mul
        (oneTermRobinGamma3BoundarySevenGateMatrix_n3
          oneTermRobinGamma3BoundaryPrefixRow0_n3
          oneTermRobinGamma3BoundaryPrefixRow0_n3)
        oneTermRobinGamma3BoundaryBranchEntrySelection_n3.projectionAmplitudeFactor := by

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary backend branch contribution slot zero eval zero n 3”; its local proof does not by itself complete the broader paper route. The slot-'0' backend branch contribution vanishes after coefficient evaluation.

theorem oneTermRobinGamma3BoundaryBackendBranchContribution_slotZeroEval_zero_n3
    (env : String → Rat) :
    Coeff.evalWith env
      (oneTermRobinGamma3BoundaryBackendBranchContribution_n3
        ⟨0, by native_decide⟩) = 0 := by

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary backend branch contribution slot one eval zero n 3”; its local proof does not by itself complete the broader paper route. The slot-'1' backend branch contribution vanishes after coefficient evaluation.

theorem oneTermRobinGamma3BoundaryBackendBranchContribution_slotOneEval_zero_n3
    (env : String → Rat) :
    Coeff.evalWith env
      (oneTermRobinGamma3BoundaryBackendBranchContribution_n3
        ⟨1, by native_decide⟩) = 0 := by

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary backend branch contribution slot three eval zero n 3”; its local proof does not by itself complete the broader paper route. The slot-'3' backend branch contribution vanishes after coefficient evaluation.

theorem oneTermRobinGamma3BoundaryBackendBranchContribution_slotThreeEval_zero_n3
    (env : String → Rat) :
    Coeff.evalWith env
      (oneTermRobinGamma3BoundaryBackendBranchContribution_n3
        ⟨3, by native_decide⟩) = 0 := by

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary backend branch contribution slot four eval zero n 3”; its local proof does not by itself complete the broader paper route. The slot-'4' backend branch contribution vanishes after coefficient evaluation.

theorem oneTermRobinGamma3BoundaryBackendBranchContribution_slotFourEval_zero_n3
    (env : String → Rat) :
    Coeff.evalWith env
      (oneTermRobinGamma3BoundaryBackendBranchContribution_n3
        ⟨4, by native_decide⟩) = 0 := by

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary backend branch contribution slot five eval zero n 3”; its local proof does not by itself complete the broader paper route. The slot-'5' backend branch contribution vanishes after coefficient evaluation.

theorem oneTermRobinGamma3BoundaryBackendBranchContribution_slotFiveEval_zero_n3
    (env : String → Rat) :
    Coeff.evalWith env
      (oneTermRobinGamma3BoundaryBackendBranchContribution_n3
        ⟨5, by native_decide⟩) = 0 := by

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary backend branch contribution slot six eval zero n 3”; its local proof does not by itself complete the broader paper route. The slot-'6' backend branch contribution vanishes after coefficient evaluation.

theorem oneTermRobinGamma3BoundaryBackendBranchContribution_slotSixEval_zero_n3
    (env : String → Rat) :
    Coeff.evalWith env
      (oneTermRobinGamma3BoundaryBackendBranchContribution_n3
        ⟨6, by native_decide⟩) = 0 := by

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary backend branch fold eval eq selected slot contribution n 3”; its local proof does not by itself complete the broader paper route. After the compiled vanish feeders for slots '0', '1', '3', '4', '5', and '6', the evaluated seven-slot backend fold collapses to the selected slot-'2' contribution.

theorem oneTermRobinGamma3BoundaryBackendBranchFoldEval_eq_selectedSlotContribution_n3
    (env : String → Rat) :
    Coeff.evalWith env
      (blockExtractionBranchContributionSum
        oneTermRobinGamma3BoundaryBackendBranchContribution_n3) =
    Coeff.evalWith env
      oneTermRobinGamma3BoundaryProjectionSummationObstruction_n3.selectedSlotContribution := by

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary backend branch fold expanded slot zero n 3”; its local proof does not by itself complete the broader paper route. Concrete seven-summand expansion of the backend branch fold.

theorem oneTermRobinGamma3BoundaryBackendBranchFold_expandedSlotZero_n3 :
    blockExtractionBranchContributionSum
        oneTermRobinGamma3BoundaryBackendBranchContribution_n3 =
      (((((((0 +
        Coeff.mul
          (oneTermRobinGamma3BoundarySevenGateMatrix_n3
            oneTermRobinGamma3BoundaryPrefixRow0_n3
            oneTermRobinGamma3BoundaryPrefixRow0_n3)
          oneTermRobinGamma3BoundaryBranchEntrySelection_n3.projectionAmplitudeFactor) +
        oneTermRobinGamma3BoundaryBackendBranchContribution_n3
          ⟨1, by native_decide⟩) +

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary backend branch fold expanded all slots n 3”; its local proof does not by itself complete the broader paper route. Concrete seven-slot expansion of the backend branch fold.

theorem oneTermRobinGamma3BoundaryBackendBranchFold_expandedAllSlots_n3 :
    blockExtractionBranchContributionSum
        oneTermRobinGamma3BoundaryBackendBranchContribution_n3 =
      (((((((0 +
        Coeff.mul
          (oneTermRobinGamma3BoundarySevenGateMatrix_n3
            oneTermRobinGamma3BoundaryPrefixRow0_n3
            oneTermRobinGamma3BoundaryPrefixRow0_n3)
          oneTermRobinGamma3BoundaryBranchEntrySelection_n3.projectionAmplitudeFactor) +
        Coeff.mul
          (oneTermRobinGamma3BoundarySevenGateMatrix_n3

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary backend branch contribution target n 3”. Backend branch-contribution target using the all-slot summand formula.

def oneTermRobinGamma3BoundaryBackendBranchContributionTarget_n3 :
    BlockExtractionBranchContributionTarget Coeff
      (gridSize 3) (gridSize 3)
      (qubitDim (GHL2025.effectiveRobinSignalQubits (oneTermParameters 3)))
      7 :=
  let contract := oneTermRobinFiniteBlockCompositionContract 3
  let sysRow : Fin (gridSize 3) := ⟨0, by native_decide⟩
  let sysCol : Fin (gridSize 3) := ⟨0, by native_decide⟩
  let branchContribution :=
    oneTermRobinGamma3BoundaryBackendBranchContribution_n3
  let selected :=

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 boundary backend all slot summand formula”. A proposition-valued field is a requirement until a constructor supplies it. Follow-up packet after the branch-index obstruction.

structure OneTermRobinGamma3BoundaryBackendAllSlotSummandFormula where
  sourceAnchor : String
  indexMapObstruction :
    OneTermRobinGamma3BoundaryBackendBranchIndexMapObstruction
  backendBranchTarget :
    BlockExtractionBranchContributionTarget Coeff
      (gridSize 3) (gridSize 3)
      (qubitDim (GHL2025.effectiveRobinSignalQubits (oneTermParameters 3)))
      7
  backendBranchContribution : Fin 7 → Coeff
  selectedBranch : Fin 7

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary backend all slot summand formula n 3”. Concrete all-slot backend summand formula packet for the focused boundary branch.

def oneTermRobinGamma3BoundaryBackendAllSlotSummandFormula_n3 :
    OneTermRobinGamma3BoundaryBackendAllSlotSummandFormula :=
  let obstruction :=
    oneTermRobinGamma3BoundaryBackendBranchIndexMapObstruction_n3
  let target :=
    oneTermRobinGamma3BoundaryBackendBranchContributionTarget_n3
  let selected :=
    oneTermRobinGamma3BoundaryBranchContributionFocusedSlot
  {
    sourceAnchor :=
      "GHL2025 Definition def:block-encoding, Eq. ROBIN clarified boundary gamma3 branch, Fig. 1-term ROBIN, and QBE finite projection backend all-slot summand formula"

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 boundary backend branch sum closure”. A proposition-valued field is a requirement until a constructor supplies it. Final focused obstruction for the current backend branch-sum packet.

structure OneTermRobinGamma3BoundaryBackendBranchSumClosure where
  sourceAnchor : String
  allSlotPacket : OneTermRobinGamma3BoundaryBackendAllSlotSummandFormula
  backendBranchTarget :
    BlockExtractionBranchContributionTarget Coeff
      (gridSize 3) (gridSize 3)
      (qubitDim (GHL2025.effectiveRobinSignalQubits (oneTermParameters 3)))
      7
  backendBranchContribution : Fin 7 → Coeff
  selectedClauseStatement : Prop
  requiredBranchSumStatement : Prop

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary backend branch sum closure n 3”. Concrete branch-sum closure target for the focused 'n = 3' boundary packet.

def oneTermRobinGamma3BoundaryBackendBranchSumClosure_n3 :
    OneTermRobinGamma3BoundaryBackendBranchSumClosure :=
  let packet := oneTermRobinGamma3BoundaryBackendAllSlotSummandFormula_n3
  let target := oneTermRobinGamma3BoundaryBackendBranchContributionTarget_n3
  let branchContribution :=
    oneTermRobinGamma3BoundaryBackendBranchContribution_n3
  {
    sourceAnchor :=
      "GHL2025 Definition def:block-encoding and Eq. ROBIN clarified boundary gamma3 branch; QBE finite projection/summation backend"
    allSlotPacket := packet
    backendBranchTarget := target

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary backend branch sum closure n 3 transcript”; its local proof does not by itself complete the broader paper route. Transcript theorem for the backend branch-sum closure target.

theorem oneTermRobinGamma3BoundaryBackendBranchSumClosure_n3_transcript :
    let closure :=
      oneTermRobinGamma3BoundaryBackendBranchSumClosure_n3
    let packet :=
      oneTermRobinGamma3BoundaryBackendAllSlotSummandFormula_n3
    let target :=
      oneTermRobinGamma3BoundaryBackendBranchContributionTarget_n3
    closure.allSlotPacket = packet ∧
      closure.backendBranchTarget = target ∧
    closure.backendBranchContribution =
        oneTermRobinGamma3BoundaryBackendBranchContribution_n3 ∧

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary backend projection statement signal entry n 3”; its local proof does not by itself complete the broader paper route. The signal entry used in the Robin-local obstruction is the block entry of the generic backend branch-contribution target.

theorem oneTermRobinGamma3BoundaryBackendProjectionStatement_signalEntry_n3 :
    oneTermRobinGamma3BoundaryProjectionSummationObstruction_n3.signalBlockEntry =
      oneTermRobinGamma3BoundaryBackendBranchContributionTarget_n3.blockEntry := by

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 boundary backend projection statement obstruction”. A proposition-valued field is a requirement until a constructor supplies it. Smallest obstruction after attempting the generic projection statement.

structure OneTermRobinGamma3BoundaryBackendProjectionStatementObstruction where
  sourceAnchor : String
  closurePacket : OneTermRobinGamma3BoundaryBackendBranchSumClosure
  branchContributionTarget :
    BlockExtractionBranchContributionTarget Coeff
      (gridSize 3) (gridSize 3)
      (qubitDim (GHL2025.effectiveRobinSignalQubits (oneTermParameters 3)))
      7
  backendBranchContribution : Fin 7 → Coeff
  genericProjectionStatement : Prop
  focusedBranchSumStatement : Prop

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary backend projection statement obstruction n 3”. Compiled obstruction for the current lower target.

def oneTermRobinGamma3BoundaryBackendProjectionStatementObstruction_n3 :
    OneTermRobinGamma3BoundaryBackendProjectionStatementObstruction :=
  let closure := oneTermRobinGamma3BoundaryBackendBranchSumClosure_n3
  let target := oneTermRobinGamma3BoundaryBackendBranchContributionTarget_n3
  let branchContribution :=
    oneTermRobinGamma3BoundaryBackendBranchContribution_n3
  {
    sourceAnchor :=
      "GHL2025 Definition def:block-encoding and Eq. ROBIN clarified boundary gamma3 branch; QBE finite projection/summation backend"
    closurePacket := closure
    branchContributionTarget := target

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 boundary backend expansion bridge”. A proposition-valued field is a requirement until a constructor supplies it. Proof-DAG packet for the remaining backend-expansion theorem.

structure OneTermRobinGamma3BoundaryBackendExpansionBridge where
  sourceAnchor : String
  projectionStatementObstruction :
    OneTermRobinGamma3BoundaryBackendProjectionStatementObstruction
  branchContributionTarget :
    BlockExtractionBranchContributionTarget Coeff
      (gridSize 3) (gridSize 3)
      (qubitDim (GHL2025.effectiveRobinSignalQubits (oneTermParameters 3)))
      7
  backendExpansionStatement : Prop
  projectionSummationStatement : Prop

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary backend expansion bridge n 3”. Compiled backend-expansion bridge packet for the focused boundary branch.

def oneTermRobinGamma3BoundaryBackendExpansionBridge_n3 :
    OneTermRobinGamma3BoundaryBackendExpansionBridge :=
  let obstruction :=
    oneTermRobinGamma3BoundaryBackendProjectionStatementObstruction_n3
  let target :=
    oneTermRobinGamma3BoundaryBackendBranchContributionTarget_n3
  {
    sourceAnchor :=
      "GHL2025 Definition def:block-encoding and Eq. ROBIN clarified boundary gamma3 branch; QBE finite projection/summation backend proof-DAG bridge"
    projectionStatementObstruction := obstruction
    branchContributionTarget := target

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary backend expansion bridge n 3 transcript”; its local proof does not by itself complete the broader paper route. Transcript theorem for the backend-expansion bridge packet.

theorem oneTermRobinGamma3BoundaryBackendExpansionBridge_n3_transcript :
    let bridge :=
      oneTermRobinGamma3BoundaryBackendExpansionBridge_n3
    let obstruction :=
      oneTermRobinGamma3BoundaryBackendProjectionStatementObstruction_n3
    let target :=
      oneTermRobinGamma3BoundaryBackendBranchContributionTarget_n3
    bridge.projectionStatementObstruction = obstruction ∧
      bridge.branchContributionTarget = target ∧
      bridge.backendExpansionStatement = target.backendExpansionStatement ∧
      bridge.projectionSummationStatement = target.projectionSummationStatement ∧

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 boundary backend unitary entry fold target”. A proposition-valued field is a requirement until a constructor supplies it. Smallest current projection-backend target after moving from the cached block entry to the full finite product entry.

structure OneTermRobinGamma3BoundaryBackendUnitaryEntryFoldTarget where
  sourceAnchor : String
  backendExpansionBridge : OneTermRobinGamma3BoundaryBackendExpansionBridge
  branchContributionTarget :
    BlockExtractionBranchContributionTarget Coeff
      (gridSize 3) (gridSize 3)
      (qubitDim (GHL2025.effectiveRobinSignalQubits (oneTermParameters 3)))
      7
  signalBlockEntry : Coeff
  signalUnitaryEntry : Coeff
  backendBranchContribution : Fin 7 → Coeff

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary backend unitary entry fold target n 3”. Concrete unitary-entry fold target for the focused 'n = 3' boundary branch.

def oneTermRobinGamma3BoundaryBackendUnitaryEntryFoldTarget_n3 :
    OneTermRobinGamma3BoundaryBackendUnitaryEntryFoldTarget :=
  let bridge := oneTermRobinGamma3BoundaryBackendExpansionBridge_n3
  let target := oneTermRobinGamma3BoundaryBackendBranchContributionTarget_n3
  let projectionTarget :=
    oneTermRobinGamma3BoundaryProjectionSummationTarget_n3
  let obstruction :=
    oneTermRobinGamma3BoundaryProjectionSummationObstruction_n3
  let branchContribution :=
    oneTermRobinGamma3BoundaryBackendBranchContribution_n3
  {

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 boundary backend unitary entry fold support target”. A proposition-valued field is a requirement until a constructor supplies it. Support packet for the remaining full-unitary entry fold.

structure OneTermRobinGamma3BoundaryBackendUnitaryEntryFoldSupportTarget where
  sourceAnchor : String
  unitaryEntryFoldTarget :
    OneTermRobinGamma3BoundaryBackendUnitaryEntryFoldTarget
  branchContributionTarget :
    BlockExtractionBranchContributionTarget Coeff
      (gridSize 3) (gridSize 3)
      (qubitDim (GHL2025.effectiveRobinSignalQubits (oneTermParameters 3)))
      7
  backendBranchContribution : Fin 7 → Coeff
  foldIndexList : List (Fin 7)

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary backend unitary entry fold support target n 3”. Concrete fold-support target for the focused 'n = 3' boundary branch.

def oneTermRobinGamma3BoundaryBackendUnitaryEntryFoldSupportTarget_n3 :
    OneTermRobinGamma3BoundaryBackendUnitaryEntryFoldSupportTarget :=
  let unitaryTarget :=
    oneTermRobinGamma3BoundaryBackendUnitaryEntryFoldTarget_n3
  let branchTarget :=
    oneTermRobinGamma3BoundaryBackendBranchContributionTarget_n3
  let branchContribution :=
    oneTermRobinGamma3BoundaryBackendBranchContribution_n3
  let selected :=
    oneTermRobinGamma3BoundaryBranchContributionFocusedSlot
  {

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary prepared branch contribution formula n 3”; its local proof does not by itself complete the broader paper route. Every backend sparse-slot contribution is the corresponding branch-diagonal seven-gate entry, multiplied by the two sparse-register projection amplitudes.

theorem oneTermRobinGamma3BoundaryPreparedBranchContribution_formula_n3
    (s : Fin 7) :
    oneTermRobinGamma3BoundaryBackendBranchContribution_n3 s =
      Coeff.mul
        (oneTermRobinGamma3BoundarySevenGateMatrix_n3
          (oneTermRobinGamma3BoundaryBackendBranchFullIndex_n3 s)
          (oneTermRobinGamma3BoundaryBackendBranchFullIndex_n3 s))
        (Coeff.mul (Coeff.symbol "sqrt_kappa_inv")
          (Coeff.symbol "sqrt_kappa_inv")) := by

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 boundary prepared branch expansion target”. A proposition-valued field is a requirement until a constructor supplies it. Typed target for the prepared branch expansion still missing from the focused projection bridge.

structure OneTermRobinGamma3BoundaryPreparedBranchExpansionTarget where
  sourceAnchor : String
  foldSupportTarget :
    OneTermRobinGamma3BoundaryBackendUnitaryEntryFoldSupportTarget
  unitaryEntryFoldTarget :
    OneTermRobinGamma3BoundaryBackendUnitaryEntryFoldTarget
  branchContributionTarget :
    BlockExtractionBranchContributionTarget Coeff
      (gridSize 3) (gridSize 3)
      (qubitDim (GHL2025.effectiveRobinSignalQubits (oneTermParameters 3)))
      7

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary prepared branch expansion target n 3”. Concrete prepared-branch expansion target for the focused 'n = 3' boundary branch.

def oneTermRobinGamma3BoundaryPreparedBranchExpansionTarget_n3 :
    OneTermRobinGamma3BoundaryPreparedBranchExpansionTarget :=
  let support :=
    oneTermRobinGamma3BoundaryBackendUnitaryEntryFoldSupportTarget_n3
  let unitaryTarget :=
    oneTermRobinGamma3BoundaryBackendUnitaryEntryFoldTarget_n3
  let branchTarget :=
    oneTermRobinGamma3BoundaryBackendBranchContributionTarget_n3
  let branchContribution :=
    oneTermRobinGamma3BoundaryBackendBranchContribution_n3
  let branchIndex :=

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary sparse clean index n 3”. Clean sparse-register column index for the focused 'H_W^(kappa)' packet.

def oneTermRobinGamma3BoundarySparseCleanIndex_n3 : Fin 8 :=
  ⟨0, by native_decide⟩

/-- Embed one of the seven paper sparse slots into the eight-dimensional register. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary sparse slot index n 3”. Embed one of the seven paper sparse slots into the eight-dimensional register.

def oneTermRobinGamma3BoundarySparseSlotIndex_n3 (s : Fin 7) : Fin 8 :=
  ⟨s.val, by omega⟩

/--
Focused uniform-column statement for the sparse-register preparation matrix.

This is the exact local shape of the Shukla--Vedula contract needed by the
prepared projection bridge: each of the seven paper slots has clean-column
amplitude `sqrt_kappa_inv`.
-/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary hw kappa uniform column all slots statement n 3”. Focused uniform-column statement for the sparse-register preparation matrix.

def oneTermRobinGamma3BoundaryHWKappaUniformColumnAllSlotsStatement_n3
    (H : Matrix 8 8 Coeff) : Prop :=
  ∀ s : Fin 7,
    H (oneTermRobinGamma3BoundarySparseSlotIndex_n3 s)
        oneTermRobinGamma3BoundarySparseCleanIndex_n3 =
      Coeff.symbol "sqrt_kappa_inv"

/--
Prepared sandwich contribution for one sparse slot.

The expression is the local branch-diagonal seven-gate entry multiplied by the

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary prepared projection sandwich contribution n 3”. Prepared sandwich contribution for one sparse slot.

def oneTermRobinGamma3BoundaryPreparedProjectionSandwichContribution_n3
    (H : Matrix 8 8 Coeff) (s : Fin 7) : Coeff :=
  Coeff.mul
    (oneTermRobinGamma3BoundarySevenGateMatrix_n3
      (oneTermRobinGamma3BoundaryBackendBranchFullIndex_n3 s)
      (oneTermRobinGamma3BoundaryBackendBranchFullIndex_n3 s))
    (Coeff.mul
      (H (oneTermRobinGamma3BoundarySparseSlotIndex_n3 s)
        oneTermRobinGamma3BoundarySparseCleanIndex_n3)
      (oneTermRobinGamma3BoundaryHWKappaDaggerTransposeMatrix_n3 H
        oneTermRobinGamma3BoundarySparseCleanIndex_n3

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary prepared projection sandwich sum n 3”. Fold the prepared sandwich contributions over the seven paper sparse slots.

def oneTermRobinGamma3BoundaryPreparedProjectionSandwichSum_n3
    (H : Matrix 8 8 Coeff) : Coeff :=
  blockExtractionBranchContributionSum
    (oneTermRobinGamma3BoundaryPreparedProjectionSandwichContribution_n3 H)

/--
The prepared sandwich contribution specializes to the backend branch summand
under the uniform-column contract for `H_W^(kappa)`.

This proves the amplitude side of the prepared projection bridge.  It does not
prove that the raw signal-zero unitary entry is this prepared sandwich fold.

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 boundary prepared projection sandwich backend target”. A proposition-valued field is a requirement until a constructor supplies it. Smallest prepared-projection backend field still missing from the current matrix semantics.

structure OneTermRobinGamma3BoundaryPreparedProjectionSandwichBackendTarget where
  sourceAnchor : String
  preparedBranchExpansionTarget :
    OneTermRobinGamma3BoundaryPreparedBranchExpansionTarget
  cleanColumnContract : OneTermRobinGamma3BoundaryHWKappaCleanColumnContract
  sparseCleanIndex : Nat
  sparseSlotDomain : List Nat
  sparsePreparationMatrixType : String
  sparseDaggerMatrixType : String
  preparedSandwichContributionFormula : String
  preparedSandwichSumFormula : String

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary prepared projection sandwich backend target n 3”. Concrete prepared-sandwich backend target for the focused 'n = 3' boundary branch.

def oneTermRobinGamma3BoundaryPreparedProjectionSandwichBackendTarget_n3 :
    OneTermRobinGamma3BoundaryPreparedProjectionSandwichBackendTarget :=
  let target := oneTermRobinGamma3BoundaryPreparedBranchExpansionTarget_n3
  let cleanColumn := oneTermRobinGamma3BoundaryHWKappaCleanColumnContract_n3
  {
    sourceAnchor :=
      "GHL2025 Definition def:block-encoding, Eq. ROBIN clarified boundary gamma3 branch, Eq. arbitrary sparcity, Fig. 1-term ROBIN, and QBE prepared projection sandwich backend"
    preparedBranchExpansionTarget := target
    cleanColumnContract := cleanColumn
    sparseCleanIndex := oneTermRobinGamma3BoundarySparseCleanIndex_n3.val
    sparseSlotDomain := [0, 1, 2, 3, 4, 5, 6]

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 boundary raw entry prepared sandwich circuit field”. A proposition-valued field is a requirement until a constructor supplies it. Typed raw-entry field needed by the prepared-sandwich backend.

structure OneTermRobinGamma3BoundaryRawEntryPreparedSandwichCircuitField where
  sourceAnchor : String
  preparedSandwichBackendTarget :
    OneTermRobinGamma3BoundaryPreparedProjectionSandwichBackendTarget
  sparsePreparationMatrix : Matrix 8 8 Coeff
  rawUnitaryEntry : Coeff
  preparedSandwichSum : Coeff
  uniformColumnStatement : Prop
  rawEntryPreparedSandwichStatement : Prop
  preferredUnitaryEntryFoldStatement : Prop
  rawCircuitSemanticsEntryFormula : String

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary raw entry prepared sandwich circuit field n 3”. Concrete raw-entry prepared-sandwich field for the focused boundary packet.

def oneTermRobinGamma3BoundaryRawEntryPreparedSandwichCircuitField_n3
    (H : Matrix 8 8 Coeff) :
    OneTermRobinGamma3BoundaryRawEntryPreparedSandwichCircuitField :=
  let backend := oneTermRobinGamma3BoundaryPreparedProjectionSandwichBackendTarget_n3
  {
    sourceAnchor :=
      "GHL2025 Definition def:block-encoding, Eq. arbitrary sparcity, Eq. ROBIN clarified, Fig. 1-term ROBIN, and QBE CircuitMatrixSemantics raw-entry backend"
    preparedSandwichBackendTarget := backend
    sparsePreparationMatrix := H
    rawUnitaryEntry :=
      oneTermRobinGamma3BoundaryProjectionSummationTarget_n3.signalUnitaryEntry

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary raw unitary entry contract matrix n 3”; its local proof does not by itself complete the broader paper route. The raw entry in the focused packet is the active seven-gate circuit product entry selected by the finite block-extraction contract.

theorem oneTermRobinGamma3BoundaryRawUnitaryEntry_contractMatrix_n3 :
    oneTermRobinGamma3BoundaryProjectionSummationTarget_n3.signalUnitaryEntry =
      (oneTermRobinFiniteBlockCompositionContract 3).expectedTarget.unitaryMatrix
        ⟨0, by native_decide⟩ ⟨0, by native_decide⟩ := by

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary sparse preparation gates absent n 3”; its local proof does not by itself complete the broader paper route. The active Fig.

theorem oneTermRobinGamma3BoundarySparsePreparationGates_absent_n3 :
    Gate.oracleCall "H_W^(kappa)" ∉
        (GHL2025.oneTermRobinGateMatrixPlaceholders
          (oneTermParameters 3)).map (fun gateMatrix => gateMatrix.gate) ∧
      Gate.oracleCall "(H_W^(kappa))^dagger" ∉
        (GHL2025.oneTermRobinGateMatrixPlaceholders
          (oneTermParameters 3)).map (fun gateMatrix => gateMatrix.gate) := by

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 boundary prepared circuit semantics gap”. A proposition-valued field is a requirement until a constructor supplies it. Smallest prepared-circuit semantics gap after exposing the raw entry.

structure OneTermRobinGamma3BoundaryPreparedCircuitSemanticsGap where
  sourceAnchor : String
  rawEntryField : OneTermRobinGamma3BoundaryRawEntryPreparedSandwichCircuitField
  rawUnitaryEntryContractStatementName : String
  sparsePreparationGateAbsentStatementName : String
  sparsePreparationDaggerGateAbsentStatementName : String
  rawUnitaryEntryContractLemma : String
  sparsePreparationAbsenceLemma : String
  requiredPreparedCircuitSemantics : String
  missingPreparedMatrixField : String
  rawEntryContractProved : Bool

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary prepared circuit semantics gap n 3”. Compiled prepared-circuit semantics gap for the focused 'n = 3' boundary packet.

def oneTermRobinGamma3BoundaryPreparedCircuitSemanticsGap_n3
    (H : Matrix 8 8 Coeff) :
    OneTermRobinGamma3BoundaryPreparedCircuitSemanticsGap :=
  let field :=
    oneTermRobinGamma3BoundaryRawEntryPreparedSandwichCircuitField_n3 H
  {
    sourceAnchor :=
      "GHL2025 Definition def:block-encoding, Eq. arbitrary sparcity, Eq. ROBIN clarified, Fig. 1-term ROBIN, and QBE CircuitMatrixSemantics active seven-gate product"
    rawEntryField := field
    rawUnitaryEntryContractStatementName :=
      "field.rawUnitaryEntry = oneTermRobinFiniteBlockCompositionContract 3 expectedTarget.unitaryMatrix[0,0]"

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary prepared circuit sparse matrix n 3”. Compressed prepared sparse-register sandwich matrix for the focused boundary branch.

def oneTermRobinGamma3BoundaryPreparedCircuitSparseMatrix_n3
    (H : Matrix 8 8 Coeff) : Matrix 8 8 Coeff :=
  fun row col =>
    blockExtractionBranchContributionSum (fun s : Fin 7 =>
      Coeff.mul
        (oneTermRobinGamma3BoundarySevenGateMatrix_n3
          (oneTermRobinGamma3BoundaryBackendBranchFullIndex_n3 s)
          (oneTermRobinGamma3BoundaryBackendBranchFullIndex_n3 s))
        (Coeff.mul
          (H (oneTermRobinGamma3BoundarySparseSlotIndex_n3 s) col)
          (oneTermRobinGamma3BoundaryHWKappaDaggerTransposeMatrix_n3 H row

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary prepared composite gate n 3”. Composite prepared sparse-register gate for the focused boundary packet.

def oneTermRobinGamma3BoundaryPreparedCompositeGate_n3
    (H : Matrix 8 8 Coeff) : GateMatrix Coeff 3 where
  gate :=
    Gate.oracleCall
      "H_W^(kappa)^dagger * U_gamma3_boundary * H_W^(kappa)"
  matrix := oneTermRobinGamma3BoundaryPreparedCircuitSparseMatrix_n3 H
  unitary := {
    description :=
      "prepared sparse-register composite gate for H_W^(kappa)^dagger * U_gamma3_boundary * H_W^(kappa)"
    source :=
      "GHL2025 Eq. arbitrary sparcity, Eq. ROBIN clarified boundary gamma3 branch, and Fig. 1-term ROBIN"

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary prepared composite circuit n 3”. Singleton circuit for the prepared sparse-register composite gate.

def oneTermRobinGamma3BoundaryPreparedCompositeCircuit_n3 : Circuit :=
  [Gate.oracleCall
    "H_W^(kappa)^dagger * U_gamma3_boundary * H_W^(kappa)"]

/-- The prepared composite gate matrix matches its singleton circuit label. -/

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary prepared composite gate matches circuit n 3”; its local proof does not by itself complete the broader paper route. The prepared composite gate matrix matches its singleton circuit label.

theorem oneTermRobinGamma3BoundaryPreparedCompositeGateMatchesCircuit_n3
    (H : Matrix 8 8 Coeff) :
    gateMatricesMatchCircuit
        oneTermRobinGamma3BoundaryPreparedCompositeCircuit_n3
        [oneTermRobinGamma3BoundaryPreparedCompositeGate_n3 H] =
      true := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary prepared composite circuit semantics n 3”. Circuit-matrix semantics for the prepared sparse-register composite.

def oneTermRobinGamma3BoundaryPreparedCompositeCircuitSemantics_n3
    (H : Matrix 8 8 Coeff) : CircuitMatrixSemantics Coeff 3 :=
  CircuitMatrixSemantics.ofGateMatrices
    oneTermRobinGamma3BoundaryPreparedCompositeCircuit_n3
    [oneTermRobinGamma3BoundaryPreparedCompositeGate_n3 H]
    (oneTermRobinGamma3BoundaryPreparedCompositeGateMatchesCircuit_n3 H)

/--
The prepared composite circuit semantics evaluates to the prepared sparse
matrix at the clean-clean entry.

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 boundary prepared circuit matrix interface”. A proposition-valued field is a requirement until a constructor supplies it. Prepared-circuit matrix interface for the current projection backend.

structure OneTermRobinGamma3BoundaryPreparedCircuitMatrixInterface where
  sourceAnchor : String
  preparedCircuitGap : OneTermRobinGamma3BoundaryPreparedCircuitSemanticsGap
  sparsePreparationMatrix : Matrix 8 8 Coeff
  preparedSparseMatrix : Matrix 8 8 Coeff
  preparedCompositeSemantics : CircuitMatrixSemantics Coeff 3
  cleanRow : Fin 8
  cleanColumn : Fin 8
  cleanEntry : Coeff
  preparedCompositeCleanEntry : Coeff
  preparedSandwichSum : Coeff

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary prepared circuit matrix interface n 3”. Concrete prepared-circuit matrix interface for the focused 'n = 3' boundary branch.

def oneTermRobinGamma3BoundaryPreparedCircuitMatrixInterface_n3
    (H : Matrix 8 8 Coeff) :
    OneTermRobinGamma3BoundaryPreparedCircuitMatrixInterface :=
  let gap := oneTermRobinGamma3BoundaryPreparedCircuitSemanticsGap_n3 H
  let preparedMatrix :=
    oneTermRobinGamma3BoundaryPreparedCircuitSparseMatrix_n3 H
  let preparedSemantics :=
    oneTermRobinGamma3BoundaryPreparedCompositeCircuitSemantics_n3 H
  let clean := oneTermRobinGamma3BoundarySparseCleanIndex_n3
  {
    sourceAnchor :=

commit-pinned source · Verso Blueprint panel

This abbreviation gives a shorter name to the type or expression used for “one term robin gamma 3 boundary active full dim n 3”. Full active matrix dimension for the focused 'n = 3' boundary packet.

abbrev oneTermRobinGamma3BoundaryActiveFullDim_n3 : Nat :=
  qubitDim (GHL2025.effectiveRobinSignalQubits (oneTermParameters 3)) *
    gridSize 3

/-- Clean active full-basis index for the focused signal-zero/system-zero entry. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary active clean index n 3”. Clean active full-basis index for the focused signal-zero/system-zero entry.

def oneTermRobinGamma3BoundaryActiveCleanIndex_n3 :
    Fin oneTermRobinGamma3BoundaryActiveFullDim_n3 :=
  ⟨0, by native_decide⟩

/--
The focused signal-zero entry is the active seven-gate circuit-matrix entry.

This removes one layer from the evaluated backend-fold target: the remaining
projection theorem can work directly against the active `CircuitMatrixSemantics`
matrix instead of the finite block-composition contract wrapper.
-/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary active prepared entry target n 3”. Typed active-entry/prepared-entry target for the focused boundary branch.

def oneTermRobinGamma3BoundaryActivePreparedEntryTarget_n3
    (H : Matrix 8 8 Coeff) :
    PreparedCircuitEntryTarget Coeff
      oneTermRobinGamma3BoundaryActiveFullDim_n3 8 :=
  let contract := oneTermRobinFiniteBlockCompositionContract 3
  let active : Matrix oneTermRobinGamma3BoundaryActiveFullDim_n3
      oneTermRobinGamma3BoundaryActiveFullDim_n3 Coeff :=
    contract.expectedTarget.unitaryMatrix
  let activeClean : Fin oneTermRobinGamma3BoundaryActiveFullDim_n3 :=
    ⟨0, by native_decide⟩
  let prepared :=

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 boundary active prepared composition field target”. A proposition-valued field is a requirement until a constructor supplies it. Smallest prepared-composition field target now missing from the matrix backend.

structure OneTermRobinGamma3BoundaryActivePreparedCompositionFieldTarget where
  sourceAnchor : String
  preparedMatrixInterface :
    OneTermRobinGamma3BoundaryPreparedCircuitMatrixInterface
  entryTarget :
    PreparedCircuitEntryTarget Coeff
      oneTermRobinGamma3BoundaryActiveFullDim_n3 8
  activeEntryStatement : Prop
  matrixEntryStatement : Prop
  interfaceStatement : Prop
  genericEntryTarget : String

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary active prepared composition field target n 3”. Concrete prepared-composition field target for the focused 'n = 3' boundary branch.

def oneTermRobinGamma3BoundaryActivePreparedCompositionFieldTarget_n3
    (H : Matrix 8 8 Coeff) :
    OneTermRobinGamma3BoundaryActivePreparedCompositionFieldTarget :=
  let interface :=
    oneTermRobinGamma3BoundaryPreparedCircuitMatrixInterface_n3 H
  let entryTarget :=
    oneTermRobinGamma3BoundaryActivePreparedEntryTarget_n3 H
  {
    sourceAnchor :=
      "GHL2025 Definition def:block-encoding, Eq. arbitrary sparcity, Fig. 1-term ROBIN, and QBE PreparedCircuitEntryTarget"
    preparedMatrixInterface := interface

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary active prepared composite eval statement n 3”. Evaluation-level active/prepared composite entry statement.

def oneTermRobinGamma3BoundaryActivePreparedCompositeEvalStatement_n3
    (H : Matrix 8 8 Coeff) (env : String → Rat) : Prop :=
  Coeff.evalWith env
      oneTermRobinGamma3BoundaryProjectionSummationTarget_n3.signalUnitaryEntry =
    Coeff.evalWith env
      ((oneTermRobinGamma3BoundaryPreparedCompositeCircuitSemantics_n3 H).matrix
        oneTermRobinGamma3BoundarySparseCleanIndex_n3
        oneTermRobinGamma3BoundarySparseCleanIndex_n3)

/--
Uncast active-entry form of the active/prepared singleton statement.

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary uncast active prepared composite eval statement n 3”. Uncast active-entry form of the active/prepared singleton statement.

def oneTermRobinGamma3BoundaryUncastActivePreparedCompositeEvalStatement_n3
    (H : Matrix 8 8 Coeff) (env : String → Rat) : Prop :=
  Coeff.evalWith env
      ((evalGateMatrices
        (GHL2025.oneTermRobinGateMatrixPlaceholders
          (oneTermParameters 3)))
        oneTermRobinGamma3BoundaryPrefixRow0_n3
        oneTermRobinGamma3BoundaryPrefixRow0_n3) =
    Coeff.evalWith env
      ((oneTermRobinGamma3BoundaryPreparedCompositeCircuitSemantics_n3 H).matrix
        oneTermRobinGamma3BoundarySparseCleanIndex_n3

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary active prepared sparse eval statement n 3”. Evaluation-level active/prepared sparse-matrix entry statement.

def oneTermRobinGamma3BoundaryActivePreparedSparseEvalStatement_n3
    (H : Matrix 8 8 Coeff) (env : String → Rat) : Prop :=
  Coeff.evalWith env
      oneTermRobinGamma3BoundaryProjectionSummationTarget_n3.signalUnitaryEntry =
    Coeff.evalWith env
      (oneTermRobinGamma3BoundaryPreparedCircuitSparseMatrix_n3 H
        oneTermRobinGamma3BoundarySparseCleanIndex_n3
        oneTermRobinGamma3BoundarySparseCleanIndex_n3)

/--
The prepared singleton semantics and prepared sparse matrix expose the same

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary uncast prepared sandwich eval statement n 3”. Named evaluated target for the current prepared-sandwich equality.

def oneTermRobinGamma3BoundaryUncastPreparedSandwichEvalStatement_n3
    (H : Matrix 8 8 Coeff) (env : String → Rat) : Prop :=
  Coeff.evalWith env
      ((evalGateMatrices
        (GHL2025.oneTermRobinGateMatrixPlaceholders
          (oneTermParameters 3)))
        oneTermRobinGamma3BoundaryPrefixRow0_n3
        oneTermRobinGamma3BoundaryPrefixRow0_n3) =
    Coeff.evalWith env
      (oneTermRobinGamma3BoundaryPreparedProjectionSandwichSum_n3 H)

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary active prepared circuit labels distinct n 3”; its local proof does not by itself complete the broader paper route. The active seven-gate circuit and the prepared singleton circuit have distinct gate labels.

theorem oneTermRobinGamma3BoundaryActivePreparedCircuitLabels_distinct_n3
    (H : Matrix 8 8 Coeff) :
    (oneTermRobinCircuitSemantics 3).circuit ≠
      (oneTermRobinGamma3BoundaryPreparedCompositeCircuitSemantics_n3 H).circuit := by

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 boundary active prepared circuit field target”. A proposition-valued field is a requirement until a constructor supplies it. Circuit-semantics field target for the active/prepared clean-entry bridge.

structure OneTermRobinGamma3BoundaryActivePreparedCircuitFieldTarget where
  sourceAnchor : String
  activeSemantics :
    CircuitMatrixSemantics Coeff
      (GHL2025.oneTermRobinTotalQubits (oneTermParameters 3))
  preparedSemantics : CircuitMatrixSemantics Coeff 3
  entryTarget :
    PreparedCircuitEntryTarget Coeff
      oneTermRobinGamma3BoundaryActiveFullDim_n3 8
  activeCircuit : Circuit
  preparedCircuit : Circuit

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary active prepared circuit field target n 3”. Concrete active/prepared circuit-semantics field target.

def oneTermRobinGamma3BoundaryActivePreparedCircuitFieldTarget_n3
    (H : Matrix 8 8 Coeff) (env : String → Rat) :
    OneTermRobinGamma3BoundaryActivePreparedCircuitFieldTarget :=
  let active := oneTermRobinCircuitSemantics 3
  let prepared :=
    oneTermRobinGamma3BoundaryPreparedCompositeCircuitSemantics_n3 H
  let clean := oneTermRobinGamma3BoundarySparseCleanIndex_n3
  let entryTarget := oneTermRobinGamma3BoundaryActivePreparedEntryTarget_n3 H
  {
    sourceAnchor :=
      "GHL2025 Definition def:block-encoding, Eq. arbitrary sparcity, Eq. ROBIN clarified boundary gamma3 branch, Fig. 1-term ROBIN, and QBE CircuitMatrixSemantics comparison"

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 boundary source prepared projection target”. A proposition-valued field is a requirement until a constructor supplies it. Theorem-facing prepared projection target for the focused boundary branch.

structure OneTermRobinGamma3BoundarySourcePreparedProjectionTarget where
  sourceAnchor : String
  activePreparedCircuitField :
    OneTermRobinGamma3BoundaryActivePreparedCircuitFieldTarget
  sparsePreparationMatrix : Matrix 8 8 Coeff
  preparedSemantics : CircuitMatrixSemantics Coeff 3
  cleanIndex : Fin 8
  preparedProjectionEntry : Coeff
  preparedSparseEntry : Coeff
  backendBranchFold : Coeff
  uniformColumnStatement : Prop

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary source prepared projection target n 3”. Concrete theorem-facing prepared projection target for 'n = 3'.

def oneTermRobinGamma3BoundarySourcePreparedProjectionTarget_n3
    (H : Matrix 8 8 Coeff) (env : String → Rat) :
    OneTermRobinGamma3BoundarySourcePreparedProjectionTarget :=
  let field :=
    oneTermRobinGamma3BoundaryActivePreparedCircuitFieldTarget_n3 H env
  let prepared :=
    oneTermRobinGamma3BoundaryPreparedCompositeCircuitSemantics_n3 H
  let clean := oneTermRobinGamma3BoundarySparseCleanIndex_n3
  let backendFold :=
    blockExtractionBranchContributionSum
      oneTermRobinGamma3BoundaryBackendBranchContribution_n3

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary source prepared projection to backend fold n 3”; its local proof does not by itself complete the broader paper route. Named lower2 leaf from the source-prepared projection entry to the backend fold.

theorem oneTermRobinGamma3BoundarySourcePreparedProjection_to_backendFold_n3
    (H : Matrix 8 8 Coeff) (env : String → Rat)
    (hUniform :
      oneTermRobinGamma3BoundaryHWKappaUniformColumnAllSlotsStatement_n3 H) :
    Coeff.evalWith env
      (oneTermRobinGamma3BoundarySourcePreparedProjectionTarget_n3
        H env).preparedProjectionEntry =
    Coeff.evalWith env
      (oneTermRobinGamma3BoundarySourcePreparedProjectionTarget_n3
        H env).backendBranchFold := by

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary backend fold to slot 2 projected product n 3”; its local proof does not by itself complete the broader paper route. Named lower2 bridge from the backend fold to the focused slot-'2' projected branch product.

theorem oneTermRobinGamma3BoundaryBackendFold_to_slot2ProjectedProduct_n3
    (env : String → Rat)
    (hentry :
      env "boundary_cos_half_0_2" =
        Coeff.evalWith env
          (GHL2025.boundaryRotationNormalizedCoefficient
            (oneTermParameters 3) 0 2)) :
    Coeff.evalWith env
      (blockExtractionBranchContributionSum
        oneTermRobinGamma3BoundaryBackendBranchContribution_n3) =
    Coeff.evalWith env

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary source prepared projection slot 2 to projected branch product n 3”; its local proof does not by itself complete the broader paper route. Named composite lower2 leaf from the source-prepared projection entry to the focused slot-'2' projected branch product.

theorem oneTermRobinGamma3BoundarySourcePreparedProjection_slot2_to_projectedBranchProduct_n3
    (H : Matrix 8 8 Coeff) (env : String → Rat)
    (hUniform :
      oneTermRobinGamma3BoundaryHWKappaUniformColumnAllSlotsStatement_n3 H)
    (hentry :
      env "boundary_cos_half_0_2" =
        Coeff.evalWith env
          (GHL2025.boundaryRotationNormalizedCoefficient
            (oneTermParameters 3) 0 2)) :
    Coeff.evalWith env
      (oneTermRobinGamma3BoundarySourcePreparedProjectionTarget_n3

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary evaluated backend fold statement n 3”. Evaluation-level backend-fold statement for the focused boundary branch.

def oneTermRobinGamma3BoundaryEvaluatedBackendFoldStatement_n3
    (env : String → Rat) : Prop :=
  Coeff.evalWith env
      oneTermRobinGamma3BoundaryProjectionSummationTarget_n3.signalUnitaryEntry =
    Coeff.evalWith env
      (blockExtractionBranchContributionSum
        oneTermRobinGamma3BoundaryBackendBranchContribution_n3)

/--
The evaluated backend-fold statement is exactly the active seven-gate
`evalGateMatrices` entry evaluation compared with the seven-slot backend fold.

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary selected slot contribution all one nonzero n 3”; its local proof does not by itself complete the broader paper route. Concrete obstruction witness for the retired all-environment H-free backend fold.

theorem oneTermRobinGamma3BoundarySelectedSlotContribution_allOne_nonzero_n3 :
    let env : String → Rat :=
      fun name =>
        if name = "f_3_0" then 1
        else if name = "N_f_inv" then 1
        else if name = "boundary_cos_half_0_2" then 1
        else if name = "sqrt_kappa_inv" then 1
        else 0
    Coeff.evalWith env
      oneTermRobinGamma3BoundaryProjectionSummationObstruction_n3.selectedSlotContribution =
      1 := by

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary active selected slot index split n 3”; its local proof does not by itself complete the broader paper route. Index split for the active strict-feeder frontier.

theorem oneTermRobinGamma3BoundaryActiveSelectedSlotIndexSplit_n3 :
    let active := oneTermRobinGamma3BoundaryPrefixRow0_n3
    let selected :=
      oneTermRobinGamma3BoundaryBackendBranchFullIndex_n3
        oneTermRobinGamma3BoundaryBranchContributionFocusedSlot
    active.val = 0 ∧
      selected.val = 32 ∧
      active ≠ selected ∧
      oneTermRobinGamma3BoundaryProjectionSummationObstruction_n3.focusedSparseSlot =
        2 ∧
      oneTermRobinGamma3BoundaryProjectionSummationObstruction_n3.selectedSlotContribution =

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary backend expansion statement not n 3”; its local proof does not by itself complete the broader paper route. No-go guard for the current backend-expansion statement.

theorem oneTermRobinGamma3BoundaryBackendExpansionStatement_not_n3 :
    ¬ oneTermRobinGamma3BoundaryBackendBranchContributionTarget_n3.backendExpansionStatement := by

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary backend projection summation statement not n 3”; its local proof does not by itself complete the broader paper route. No-go guard for the generic projection-summation surface.

theorem oneTermRobinGamma3BoundaryBackendProjectionSummationStatement_not_n3 :
    ¬ oneTermRobinGamma3BoundaryBackendBranchContributionTarget_n3.projectionSummationStatement := by

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 boundary evaluated backend fold target”. A proposition-valued field is a requirement until a constructor supplies it. Smallest current evaluated projection-backend target.

structure OneTermRobinGamma3BoundaryEvaluatedBackendFoldTarget where
  sourceAnchor : String
  sourcePreparedProjectionTarget :
    OneTermRobinGamma3BoundarySourcePreparedProjectionTarget
  activeSignalEntry : Coeff
  backendBranchFold : Coeff
  evaluatedBackendFoldStatement : Prop
  activePreparedEvalStatement : Prop
  equivalenceLemma : String
  requiredEvaluationTheorem : String
  missingFiniteProjectionField : String

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary evaluated backend fold target n 3”. Concrete evaluated backend-fold target for 'n = 3'.

def oneTermRobinGamma3BoundaryEvaluatedBackendFoldTarget_n3
    (H : Matrix 8 8 Coeff) (env : String → Rat) :
    OneTermRobinGamma3BoundaryEvaluatedBackendFoldTarget :=
  let preparedTarget :=
    oneTermRobinGamma3BoundarySourcePreparedProjectionTarget_n3 H env
  let backendFold :=
    blockExtractionBranchContributionSum
      oneTermRobinGamma3BoundaryBackendBranchContribution_n3
  {
    sourceAnchor :=
      "GHL2025 Definition def:block-encoding, Eq. ROBIN clarified boundary gamma3 branch, Eq. arbitrary sparcity, and QBE evaluated finite projection backend"

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 boundary source prepared product projection obligation”. A proposition-valued field is a requirement until a constructor supplies it. Source-prepared product/projection proof-DAG packet for the focused boundary leaf.

structure OneTermRobinGamma3BoundarySourcePreparedProductProjectionObligation where
  sourceAnchor : String
  sourceTarget : OneTermRobinGamma3BoundarySourcePreparedProjectionTarget
  productRoute : OneTermRobinGamma3BoundaryProductUnderContractsRoute
  productBridge : OneTermRobinGamma3BoundaryFiniteProjectionProductBridge
  preparedBackendEvalStatement : Prop
  fixedProductObligation : SemanticObligation
  forbiddenBackendExpansionParent : Bool
  preparedBackendEvalCompiled : Bool
  productRouteConsumed : Bool
  normalizedBlockEqualityProved : Bool

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary source prepared product projection obligation n 3”. Concrete 'n = 3' source-prepared product/projection packet.

def oneTermRobinGamma3BoundarySourcePreparedProductProjectionObligation_n3
    (H : Matrix 8 8 Coeff) (env : String → Rat) :
    OneTermRobinGamma3BoundarySourcePreparedProductProjectionObligation :=
  let sourceTarget :=
    oneTermRobinGamma3BoundarySourcePreparedProjectionTarget_n3 H env
  {
    sourceAnchor :=
      "2026-06-15 source-prepared product/projection packet: full prepared sandwich clean projection feeding fixed gamma3 boundary product obligation"
    sourceTarget := sourceTarget
    productRoute := oneTermRobinGamma3BoundaryProductUnderContractsRoute_n3
    productBridge := oneTermRobinGamma3BoundaryFiniteProjectionProductBridge_n3

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 boundary source prepared normalized projection bridge”. A proposition-valued field is a requirement until a constructor supplies it. Source-prepared finite normalized-projection bridge packet for the focused boundary branch.

structure OneTermRobinGamma3BoundarySourcePreparedNormalizedProjectionBridge where
  sourceAnchor : String
  sourcePreparedPacket :
    OneTermRobinGamma3BoundarySourcePreparedProductProjectionObligation
  finiteProjectionBridge :
    OneTermRobinGamma3BoundaryFiniteProjectionProductBridge
  fixedProductObligation : SemanticObligation
  finiteBlockNormalizer : Coeff
  finiteBlockNormalizedEquality : SemanticObligation
  finiteBlockProjectionObligation : SemanticObligation
  finiteBlockLCUCompositionObligation : SemanticObligation

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary source prepared normalized projection bridge n 3”. Concrete 'n = 3' source-prepared finite normalized-projection packet.

def oneTermRobinGamma3BoundarySourcePreparedNormalizedProjectionBridge_n3
    (H : Matrix 8 8 Coeff) (env : String → Rat) :
    OneTermRobinGamma3BoundarySourcePreparedNormalizedProjectionBridge :=
  let packet :=
    oneTermRobinGamma3BoundarySourcePreparedProductProjectionObligation_n3
      H env
  let finiteBridge :=
    oneTermRobinGamma3BoundaryFiniteProjectionProductBridge_n3
  let contract :=
    oneTermRobinFiniteBlockCompositionContract 3
  {

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “one term robin gamma 3 boundary theorem facing finite block contract audit”. A proposition-valued field is a requirement until a constructor supplies it. Theorem-facing finite block-contract audit for the focused boundary branch.

structure OneTermRobinGamma3BoundaryTheoremFacingFiniteBlockContractAudit where
  sourceAnchor : String
  theoremFacingCircuit : Circuit
  activeBackendCircuit : Circuit
  activeSemantics :
    CircuitMatrixSemantics Coeff
      (GHL2025.oneTermRobinTotalQubits (oneTermParameters 3))
  finiteBlockContract :
    FiniteBlockCompositionContract Coeff
      (GHL2025.oneTermRobinTotalQubits (oneTermParameters 3))
      (gridSize 3)

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary theorem facing finite block contract audit n 3”. Concrete 'n = 3' theorem-facing finite block-contract audit packet.

def oneTermRobinGamma3BoundaryTheoremFacingFiniteBlockContractAudit_n3
    (H : Matrix 8 8 Coeff) (env : String → Rat) :
    OneTermRobinGamma3BoundaryTheoremFacingFiniteBlockContractAudit :=
  let contract := oneTermRobinFiniteBlockCompositionContract 3
  let bridge :=
    oneTermRobinGamma3BoundarySourcePreparedNormalizedProjectionBridge_n3
      H env
  let active := oneTermRobinCircuitSemantics 3
  {
    sourceAnchor :=
      "2026-06-15 theorem-facing finite block contract audit: Fig. 4 transcript is distinct from the active seven-gate backend wired into oneTermRobinFiniteBlockCompositionContract 3"

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “one term robin gamma 3 boundary theorem facing finite block projection interface n 3”. Concrete 'n = 3' theorem-facing finite block/projection interface packet.

def oneTermRobinGamma3BoundaryTheoremFacingFiniteBlockProjectionInterface_n3
    (H : Matrix 8 8 Coeff) (env : String → Rat) :
    OneTermRobinGamma3BoundaryTheoremFacingFiniteBlockProjectionInterface :=
  let sourceTarget :=
    oneTermRobinGamma3BoundarySourcePreparedProjectionTarget_n3 H env
  let contract := oneTermRobinFiniteBlockCompositionContract 3
  let audit :=
    oneTermRobinGamma3BoundaryTheoremFacingFiniteBlockContractAudit_n3
      H env
  {
    sourceAnchor :=

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary evaluated backend fold statement diagnostic n 3”; its local proof does not by itself complete the broader paper route. Diagnostic/H-free route: the evaluated backend fold follows from the raw Coeff equality 'signalUnitaryEntry = blockExtractionBranchContributionSum' via the bridge theorem.

theorem oneTermRobinGamma3BoundaryEvaluatedBackendFoldStatement_diagnostic_n3
    (env : String → Rat)
    (hRaw :
      oneTermRobinGamma3BoundaryProjectionSummationTarget_n3.signalUnitaryEntry =
        blockExtractionBranchContributionSum
          oneTermRobinGamma3BoundaryBackendBranchContribution_n3) :
    oneTermRobinGamma3BoundaryEvaluatedBackendFoldStatement_n3 env :=
  oneTermRobinGamma3BoundaryEvaluatedBackendFold_of_unitaryEntryFold_n3 env hRaw

/--
The historical H-free raw fold is false for the current symbolic target.

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary unitary entry ne backend fold n 3”; its local proof does not by itself complete the broader paper route. The historical H-free raw fold is false for the current symbolic target.

theorem oneTermRobinGamma3BoundaryUnitaryEntry_ne_backendFold_n3 :
    oneTermRobinGamma3BoundaryProjectionSummationTarget_n3.signalUnitaryEntry ≠
      blockExtractionBranchContributionSum
        oneTermRobinGamma3BoundaryBackendBranchContribution_n3 := by

commit-pinned source · Verso Blueprint panel

Lean checks the research-module proposition indexed as “one term robin gamma 3 boundary gate matrix list n 3”; its local proof does not by itself complete the broader paper route. The seven active gate matrices have the exact paper-facing order recorded by the circuit semantics layer.

theorem oneTermRobinGamma3BoundaryGateMatrixList_n3 :
    (GHL2025.oneTermRobinGateMatrixPlaceholders
      (oneTermParameters 3)).map (fun gateMatrix => gateMatrix.matrix) =
      [ GHL2025.indicatorOracleMatrix (oneTermParameters 3)
      , GHL2025.sparseAmplitudeOracleDTRotationMatrix (oneTermParameters 3)
      , GHL2025.boundaryRotationMatrix (oneTermParameters 3)
      , GHL2025.bandedSparseAccessPaperMatrix (oneTermParameters 3)
      , GHL2025.functionOraclePaperMatrix (oneTermParameters 3)
      , GHL2025.swapOracleMatrix (oneTermParameters 3)
      , GHL2025.bandedSparseAccessPaperDaggerMatrix (oneTermParameters 3)
      ] := by

commit-pinned source · Verso Blueprint panel