Search every explicit public declaration

QuantumBlockEncoding.AutomationStage

This type lists the allowed alternatives for “automation stage”; its constructors are the cases that downstream code must handle.

QuantumBlockEncoding.TaskKind

This type lists the allowed alternatives for “task kind”; its constructors are the cases that downstream code must handle.

QuantumBlockEncoding.TaskStatus

This type lists the allowed alternatives for “task status”; its constructors are the cases that downstream code must handle.

QuantumBlockEncoding.ArtifactLanguage

This type lists the allowed alternatives for “artifact language”; its constructors are the cases that downstream code must handle.

QuantumBlockEncoding.AgentRole

This type lists the allowed alternatives for “agent role”; its constructors are the cases that downstream code must handle.

QuantumBlockEncoding.AgentBackendKind

This type lists the allowed alternatives for “agent backend kind”; its constructors are the cases that downstream code must handle.

QuantumBlockEncoding.TrialKind

This type lists the allowed alternatives for “trial kind”; its constructors are the cases that downstream code must handle.

QuantumBlockEncoding.TrialStatus

This type lists the allowed alternatives for “trial status”; its constructors are the cases that downstream code must handle.

QuantumBlockEncoding.ArtifactSpec

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

QuantumBlockEncoding.AcceptanceGate

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

QuantumBlockEncoding.AutomationTask

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

QuantumBlockEncoding.AgentContract

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

QuantumBlockEncoding.TrialRecordSpec

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

QuantumBlockEncoding.PostCycleArtifactKind

This type lists the allowed alternatives for “post cycle artifact kind”; its constructors are the cases that downstream code must handle.

QuantumBlockEncoding.PostCycleArtifactSpec

This record groups the data and proof fields needed for “post cycle artifact spec”. A proposition-valued field is a requirement until a constructor supplies it.

QuantumBlockEncoding.WorkflowCheckSpec

This record groups the data and proof fields needed for “workflow check spec”. A proposition-valued field is a requirement until a constructor supplies it.

QuantumBlockEncoding.CandidatePool

This type lists the allowed alternatives for “candidate pool”; its constructors are the cases that downstream code must handle.

QuantumBlockEncoding.LexElimSchedulerMode

This type lists the allowed alternatives for “lex elim scheduler mode”; its constructors are the cases that downstream code must handle.

QuantumBlockEncoding.LexObjectiveClass

This type lists the allowed alternatives for “lex objective class”; its constructors are the cases that downstream code must handle.

QuantumBlockEncoding.LexObjectiveSpec

This record groups the data and proof fields needed for “lex objective spec”. A proposition-valued field is a requirement until a constructor supplies it.

QuantumBlockEncoding.LexElimSchedulerSpec

This record groups the data and proof fields needed for “lex elim scheduler spec”. A proposition-valued field is a requirement until a constructor supplies it.

QuantumBlockEncoding.AgentPanelSizeSpec

This record groups the data and proof fields needed for “agent panel size spec”. A proposition-valued field is a requirement until a constructor supplies it.

QuantumBlockEncoding.AgentBackendProfileSpec

This record groups the data and proof fields needed for “agent backend profile spec”. A proposition-valued field is a requirement until a constructor supplies it.

QuantumBlockEncoding.WorkflowInvariantSpec

This record groups the data and proof fields needed for “workflow invariant spec”. A proposition-valued field is a requirement until a constructor supplies it.

QuantumBlockEncoding.leanBuildGate

This definition gives the library's named construction or computation for “lean build gate”.

QuantumBlockEncoding.noSorryGate

This definition gives the library's named construction or computation for “no sorry gate”.

QuantumBlockEncoding.defaultGates

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

QuantumBlockEncoding.trialRecordSpec

This definition gives the library's named construction or computation for “trial record spec”.

QuantumBlockEncoding.postCycleArtifactSpecs

This definition gives the library's named construction or computation for “post cycle artifact specs”.

QuantumBlockEncoding.workflowCheckSpecs

This definition gives the library's named construction or computation for “workflow check specs”.

QuantumBlockEncoding.blockEncodingLexObjectiveSpecs

This definition gives the library's named construction or computation for “block encoding lex objective specs”.

QuantumBlockEncoding.lexElimSchedulerSpecs

This definition gives the library's named construction or computation for “lex elim scheduler specs”.

QuantumBlockEncoding.agentPanelSizeSpecs

This definition gives the library's named construction or computation for “agent panel size specs”.

QuantumBlockEncoding.agentBackendProfileSpecs

This definition gives the library's named construction or computation for “agent backend profile specs”.

QuantumBlockEncoding.workflowInvariantSpecs

This definition gives the library's named construction or computation for “workflow invariant specs”.

QuantumBlockEncoding.threeLayerAgentContracts

This definition gives the library's named construction or computation for “three layer agent contracts”.

QuantumBlockEncoding.conversionArtifacts

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

QuantumBlockEncoding.seedAutomationTasks

This definition gives the library's named construction or computation for “seed automation tasks”.

QuantumBlockEncoding.automationTaskCount

This definition gives the library's named construction or computation for “automation task count”.

QuantumBlockEncoding.ThreeLayerPhase

This type lists the allowed alternatives for “three layer phase”; its constructors are the cases that downstream code must handle.

QuantumBlockEncoding.ThreeLayerHandoff

This record groups the data and proof fields needed for “three layer handoff”. A proposition-valued field is a requirement until a constructor supplies it.

QuantumBlockEncoding.ThreeLayerHandoff.validFlag

This definition gives the library's named construction or computation for “valid flag”. Executable transition guard.

QuantumBlockEncoding.ThreeLayerHandoff.valid

This definition gives the library's named construction or computation for “valid”. Propositional view of the executable transition guard.

QuantumBlockEncoding.ThreeLayerTrace

This record groups the data and proof fields needed for “three layer trace”. A proposition-valued field is a requirement until a constructor supplies it. One execution trace with an explicit starting phase.

QuantumBlockEncoding.ThreeLayerTrace.advance

This definition gives the library's named construction or computation for “advance”. Follow a handoff only when it starts at the current phase and is valid.

QuantumBlockEncoding.ThreeLayerTrace.finalPhase

This definition gives the library's named construction or computation for “final phase”. Execute a trace left-to-right, rejecting the first invalid handoff.

QuantumBlockEncoding.ThreeLayerTrace.allValid

This definition gives the library's named construction or computation for “all valid”. Every handoff in a trace is locally valid.

QuantumBlockEncoding.threeLayerCanonicalTrace

This definition gives the library's named construction or computation for “three layer canonical trace”. Canonical upper-to-reviewer trace used as the finite teaching witness.

QuantumBlockEncoding.threeLayerCanonicalTrace_allValid

Lean checks the proposition indexed as “three layer canonical trace all valid”; the hypotheses and conclusion in the code panel fix its exact scope.

QuantumBlockEncoding.threeLayerCanonicalTrace_reachesAccepted

Lean checks the proposition indexed as “three layer canonical trace reaches accepted”; the hypotheses and conclusion in the code panel fix its exact scope. The canonical trace reaches acceptance without an external semantic axiom.

QuantumBlockEncoding.threeLayerAccepted_requiresLeanGate

Lean checks the proposition indexed as “three layer accepted requires lean gate”; the hypotheses and conclusion in the code panel fix its exact scope. Any locally valid acceptance transition records a passing Lean gate.

QuantumBlockEncoding.threeLayerAccepted_requiresReviewerApproval

Lean checks the proposition indexed as “three layer accepted requires reviewer approval”; the hypotheses and conclusion in the code panel fix its exact scope. Any locally valid acceptance transition also records reviewer approval.

QuantumBlockEncoding.threeLayerFailedGateTrace

This definition gives the library's named construction or computation for “three layer failed gate trace”. Removing the final Lean gate prevents the same trace from being accepted.

QuantumBlockEncoding.threeLayerFailedGateTrace_notAccepted

Lean checks the proposition indexed as “three layer failed gate trace not accepted”; the hypotheses and conclusion in the code panel fix its exact scope.

QuantumBlockEncoding.BandedSparseAccess.Word

This abbreviation gives a shorter name to the type or expression used for “word”. An 'n'-qubit computational-basis word, represented modulo '2^n'.

QuantumBlockEncoding.BandedSparseAccess.slotWord

This definition gives the library's named construction or computation for “slot word”. The sparse selector embedded in the clean 'n'-qubit address register.

QuantumBlockEncoding.BandedSparseAccess.modularSumEquiv

This definition gives the library's named construction or computation for “modular sum equiv”. Reversible modular SUM: add the second register into the first and preserve the second register.

QuantumBlockEncoding.BandedSparseAccess.liftLoaderEquiv

This definition gives the library's named construction or computation for “lift loader equiv”. Lift a reversible first-row address loader while leaving the row register untouched.

QuantumBlockEncoding.BandedSparseAccess.accessEquiv

This definition gives the library's named construction or computation for “access equiv”. The exact arbitrary-size banded-sparse-access semantics: load 'r_(s,0)', then add the row modulo '2^n'.

QuantumBlockEncoding.BandedSparseAccess.modularSumEquiv_apply

Lean checks the proposition indexed as “modular sum equiv apply”; the hypotheses and conclusion in the code panel fix its exact scope.

QuantumBlockEncoding.BandedSparseAccess.accessEquiv_apply

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

QuantumBlockEncoding.BandedSparseAccess.accessEquiv_clean_slot

Lean checks the proposition indexed as “access equiv clean slot”; the hypotheses and conclusion in the code panel fix its exact scope. Definition 6 action on the clean sparse-selector input.

QuantumBlockEncoding.BandedSparseAccess.accessEquiv_preserves_row

Lean checks the proposition indexed as “access equiv preserves row”; the hypotheses and conclusion in the code panel fix its exact scope. The row register is preserved for every basis input, not only clean sparse selectors.

QuantumBlockEncoding.BandedSparseAccess.accessMatrix

This definition gives the library's named construction or computation for “access matrix”. Exact matrix semantics induced by the reversible access map.

QuantumBlockEncoding.BandedSparseAccess.accessMatrix_unitary

Lean checks the proposition indexed as “access matrix unitary”; the hypotheses and conclusion in the code panel fix its exact scope. The arbitrary-size semantic access construction is unitary.

QuantumBlockEncoding.BandedSparseAccess.paperSingleQubitUpperBound

This definition gives the library's named construction or computation for “paper single qubit upper bound”. Source-facing single-qubit upper bound printed in Lemma 1 of arXiv:2405.12855v3.

QuantumBlockEncoding.BandedSparseAccess.paperCnotUpperBound

This definition gives the library's named construction or computation for “paper cnot upper bound”. Source-facing CNOT upper bound printed in the same lemma.

QuantumBlockEncoding.BandedSparseAccess.paperPureAncillaUpperBound

This definition gives the library's named construction or computation for “paper pure ancilla upper bound”. Source-facing clean-ancilla upper bound printed in the same lemma.

QuantumBlockEncoding.BandedSparseAccess.paperSingleQubitUpperBound_eq

Lean checks the proposition indexed as “paper single qubit upper bound eq”; the hypotheses and conclusion in the code panel fix its exact scope.

QuantumBlockEncoding.BandedSparseAccess.paperCnotUpperBound_eq

Lean checks the proposition indexed as “paper cnot upper bound eq”; the hypotheses and conclusion in the code panel fix its exact scope.

QuantumBlockEncoding.BandedSparseAccess.paperPureAncillaUpperBound_eq

Lean checks the proposition indexed as “paper pure ancilla upper bound eq”; the hypotheses and conclusion in the code panel fix its exact scope.

QuantumBlockEncoding.BandedSparseAccess.primitiveWord3

This definition gives the library's named construction or computation for “primitive word 3”. Decode three little-endian wires as an element of 'Fin 8'.

QuantumBlockEncoding.BandedSparseAccess.primitiveOffset3

This definition gives the library's named construction or computation for “primitive offset 3”. The concrete source loader used by the fixed witness: 's ↦ s XOR 3'.

QuantumBlockEncoding.BandedSparseAccess.primitiveOffset3_table

Lean checks the proposition indexed as “primitive offset 3 table”; the hypotheses and conclusion in the code panel fix its exact scope.

QuantumBlockEncoding.BandedSparseAccess.primitiveAccess3ReversibleProgram

This definition gives the library's named construction or computation for “primitive access 3 reversible program”. Wire order is 'address[0..2], row[0..2], work'.

QuantumBlockEncoding.BandedSparseAccess.primitiveAccess3BasisEquiv

This definition gives the library's named construction or computation for “primitive access 3 basis equiv”. Full-space reversible semantics of the fixed primitive witness.

QuantumBlockEncoding.BandedSparseAccess.primitiveAccess3_cleanAction

Lean checks the proposition indexed as “primitive access 3 clean action”; the hypotheses and conclusion in the code panel fix its exact scope. Exact clean-workspace action of the expanded access circuit.

QuantumBlockEncoding.BandedSparseAccess.primitiveAccess3_preserves_row

Lean checks the proposition indexed as “primitive access 3 preserves row”; the hypotheses and conclusion in the code panel fix its exact scope. The row register is preserved by the primitive witness.

QuantumBlockEncoding.BandedSparseAccess.primitiveAccess3_workspaceClean

Lean checks the proposition indexed as “primitive access 3 workspace clean”; the hypotheses and conclusion in the code panel fix its exact scope. The reusable work qubit is returned to zero.

QuantumBlockEncoding.BandedSparseAccess.primitiveAccess3Program

This definition gives the library's named construction or computation for “primitive access 3 program”. Primitive compilation contains no opaque oracle instruction.

QuantumBlockEncoding.BandedSparseAccess.primitiveAccess3Program_eval

Lean checks the proposition indexed as “primitive access 3 program eval”; the hypotheses and conclusion in the code panel fix its exact scope. Exact matrix refinement from the emitted primitive list to the reversible map.

QuantumBlockEncoding.BandedSparseAccess.primitiveAccess3Program_resource_faithful

Lean checks the proposition indexed as “primitive access 3 program resource faithful”; the hypotheses and conclusion in the code panel fix its exact scope. Resource ownership is definitional: the score is computed from the gate list.

QuantumBlockEncoding.BandedSparseAccess.primitiveAccess3Program_oracleCalls_eq_zero

Lean checks the proposition indexed as “primitive access 3 program oracle calls eq zero”; the hypotheses and conclusion in the code panel fix its exact scope. The expanded witness has zero unresolved oracle calls.

QuantumBlockEncoding.BandedSparseAccess.primitiveAccess3Program_unitary

Lean checks the proposition indexed as “primitive access 3 program unitary”; the hypotheses and conclusion in the code panel fix its exact scope. The primitive matrix is unitary because every emitted instruction is unitary.

QuantumBlockEncoding.RegisterLayout

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

QuantumBlockEncoding.RegisterLayout.auxiliaryQubits

This definition gives the library's named construction or computation for “auxiliary qubits”. The auxiliary qubit count used by the block-encoding score.

QuantumBlockEncoding.BlockEncodingSpec

This record groups the data and proof fields needed for “block encoding spec”. A proposition-valued field is a requirement until a constructor supplies it. A block-encoding candidate before semantic proofs are attached.

QuantumBlockEncoding.BlockEncodingCost

This record groups the data and proof fields needed for “block encoding cost”. A proposition-valued field is a requirement until a constructor supplies it. Resource score for comparing two candidate block encodings of the same operator.

QuantumBlockEncoding.BlockEncodingCost.fromLayoutAndResource

This definition gives the library's named construction or computation for “from layout and resource”.

QuantumBlockEncoding.BlockEncodingCost.fromSpec

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

QuantumBlockEncoding.BlockEncodingCost.betterThan

This definition gives the library's named construction or computation for “better than”. Strict lexicographic improvement used by candidate-population selection.

QuantumBlockEncoding.BlockEncodingCost.noWorseThan

This definition gives the library's named construction or computation for “no worse than”. Non-strict version for accepting a candidate as no worse than a baseline.

QuantumBlockEncoding.QueryOperatorTarget

This record groups the data and proof fields needed for “query operator target”. A proposition-valued field is a requirement until a constructor supplies it. The concrete input ABEIS is meant to solve: a user gives an operator/query oracle target, usually as a finite matrix together with a normalization contract and optional free parameters.

QuantumBlockEncoding.OperatorBlockEncodingCandidate

This record groups the data and proof fields needed for “operator block encoding candidate”. A proposition-valued field is a requirement until a constructor supplies it. A candidate unitary for an 'n'-qubit square operator.

QuantumBlockEncoding.OperatorBlockEncodingCandidate.cost

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

QuantumBlockEncoding.VerifiedOperatorBlockEncoding

This record groups the data and proof fields needed for “verified operator block encoding”. A proposition-valued field is a requirement until a constructor supplies it. A verified candidate with explicit proofs of unitarity and block containment.

QuantumBlockEncoding.ApproximateOperatorBlockEncodingCandidate

This record groups the data and proof fields needed for “approximate operator block encoding candidate”. A proposition-valued field is a requirement until a constructor supplies it. An approximate block-encoding candidate for the same operator-first interface.

QuantumBlockEncoding.VerifiedApproximateOperatorBlockEncoding

This record groups the data and proof fields needed for “verified approximate operator block encoding”. A proposition-valued field is a requirement until a constructor supplies it. A verified approximate block encoding.

QuantumBlockEncoding.VerifiedOperatorBlockEncoding.asZeroErrorApprox

This definition gives the library's named construction or computation for “as zero error approx”. Package an exact certificate as a zero-error approximate certificate when the chosen approximate proposition is the same exact block predicate.

QuantumBlockEncoding.AdaptiveBlockEncodingPolicy

This record groups the data and proof fields needed for “adaptive block encoding policy”. A proposition-valued field is a requirement until a constructor supplies it. User-level stopping and relaxation policy for operator block-encoding search.

QuantumBlockEncoding.BlockEncodingSearchPhase

This type lists the allowed alternatives for “block encoding search phase”; its constructors are the cases that downstream code must handle. High-level phase labels used by the candidate-population ledger.

QuantumBlockEncoding.VerifiedBlockEncoding

This record groups the data and proof fields needed for “verified block encoding”. A proposition-valued field is a requirement until a constructor supplies it. A verified block encoding.

QuantumBlockEncoding.VerifiedBlockEncoding.unitary

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

QuantumBlockEncoding.VerifiedBlockEncoding.correct

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

QuantumBlockEncoding.VerifiedBlockEncoding.resource_ok

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

QuantumBlockEncoding.ConstructionClaim

This record groups the data and proof fields needed for “construction claim”. A proposition-valued field is a requirement until a constructor supplies it. A high-level construction claim imported from a paper or generated by AI.

QuantumBlockEncoding.BlockEncodingClassics.permMatrix

This definition gives the library's named construction or computation for “perm matrix”. Permutation-matrix entries for a finite basis map.

QuantumBlockEncoding.BlockEncodingClassics.columnInner

This definition gives the library's named construction or computation for “column inner”. Column inner products for rational matrix-level orthogonality checks.

QuantumBlockEncoding.BlockEncodingClassics.rowInner

This definition gives the library's named construction or computation for “row inner”. Row inner products for rational matrix-level orthogonality checks.

QuantumBlockEncoding.BlockEncodingClassics.IsRationalOrthogonal

This definition gives the library's named construction or computation for “is rational orthogonal”. Rational orthogonality predicate for real-valued finite matrix backends: 'U^T U = I' and 'U U^T = I', expressed entrywise.

QuantumBlockEncoding.BlockEncodingClassics.cleanBlockBy

This definition gives the library's named construction or computation for “clean block by”. Clean block induced by an embedding of the system basis into a larger basis.

QuantumBlockEncoding.BlockEncodingClassics.productIndex

This definition gives the library's named construction or computation for “product index”. Canonical product-register embedding.

QuantumBlockEncoding.BlockEncodingClassics.cleanBlockProduct

This definition gives the library's named construction or computation for “clean block product”. Clean block for a flattened 'ancilla × system' matrix.

QuantumBlockEncoding.BlockEncodingClassics.cleanBlockBy_permMatrix_entry

Lean checks the proposition indexed as “clean block by perm matrix entry”; the hypotheses and conclusion in the code panel fix its exact scope. Core 'BE.PermMatrix.CleanBlock' leaf: the clean block of a permutation matrix is just the finite image predicate restricted to clean embedded rows and columns.

QuantumBlockEncoding.BlockEncodingClassics.cleanBlockProduct_permMatrix_entry

Lean checks the proposition indexed as “clean block product perm matrix entry”; the hypotheses and conclusion in the code panel fix its exact scope. Product-register version of 'cleanBlockBy_permMatrix_entry'.

QuantumBlockEncoding.BlockEncodingClassics.cleanBlockBy_permMatrix_eq_target_of_entry

Lean checks the proposition indexed as “clean block by perm matrix eq target of entry”; the hypotheses and conclusion in the code panel fix its exact scope. Entrywise bridge from a finite image calculation to an exact clean block.

QuantumBlockEncoding.BlockEncodingClassics.cleanBlockProduct_eq_target_of_entry

Lean checks the proposition indexed as “clean block product eq target of entry”; the hypotheses and conclusion in the code panel fix its exact scope. Pointwise extension principle for product-register clean blocks.

QuantumBlockEncoding.BlockEncodingClassics.kroneckerRat

This definition gives the library's named construction or computation for “kronecker rat”. Kronecker delta over the project-local rational matrix backend.

QuantumBlockEncoding.BlockEncodingClassics.oneSparseMatrix

This definition gives the library's named construction or computation for “one sparse matrix”. Column one-sparse matrix with support map 'c': column 'j' has its possible nonzero entry at row 'c j', with amplitude 'amp j'.

QuantumBlockEncoding.BlockEncodingClassics.oneSparseMatrix_entry_if

Lean checks the proposition indexed as “one sparse matrix entry if”; the hypotheses and conclusion in the code panel fix its exact scope.

QuantumBlockEncoding.BlockEncodingClassics.oneSparse_from_support

Lean checks the proposition indexed as “one sparse from support”; the hypotheses and conclusion in the code panel fix its exact scope. One-sparse reconstruction leaf.

QuantumBlockEncoding.BlockEncodingClassics.OneSparseCertificate

This record groups the data and proof fields needed for “one sparse certificate”. A proposition-valued field is a requirement until a constructor supplies it. Proof-carrying one-sparse certificate.

QuantumBlockEncoding.BlockEncodingClassics.OneSparseCertificate.cleanBlock

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

QuantumBlockEncoding.BlockEncodingClassics.OneSparseCertificate.correct

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

QuantumBlockEncoding.BlockEncodingClassics.sparseColumnCleanEntry

This definition gives the library's named construction or computation for “sparse column clean entry”. Column sparse clean-entry expression: a finite sum over slot indices of value oracle entries times location deltas.

QuantumBlockEncoding.BlockEncodingClassics.permMatrix_columnInner_of_injective

Lean checks the proposition indexed as “perm matrix column inner of injective”; the hypotheses and conclusion in the code panel fix its exact scope. Column Gram entries of a permutation matrix collapse by injectivity.

QuantumBlockEncoding.BlockEncodingClassics.permMatrix_rowInner_of_bijective

Lean checks the proposition indexed as “perm matrix row inner of bijective”; the hypotheses and conclusion in the code panel fix its exact scope. Row Gram entries of a permutation matrix collapse by bijectivity.

QuantumBlockEncoding.BlockEncodingClassics.permMatrix_isRationalOrthogonal_of_bijective

Lean checks the proposition indexed as “perm matrix is rational orthogonal of bijective”; the hypotheses and conclusion in the code panel fix its exact scope. A bijective finite image induces a rational orthogonal permutation matrix.

QuantumBlockEncoding.BlockEncodingClassics.sparseColumnCleanEntry_no_hit

Lean checks the proposition indexed as “sparse column clean entry no hit”; the hypotheses and conclusion in the code panel fix its exact scope.

QuantumBlockEncoding.BlockEncodingClassics.sparseColumnCleanEntry_unique_slot

Lean checks the proposition indexed as “sparse column clean entry unique slot”; the hypotheses and conclusion in the code panel fix its exact scope.

QuantumBlockEncoding.BlockEncodingClassics.rowColumnSparseDeltaEntry

This definition gives the library's named construction or computation for “row column sparse delta entry”. General row/column sparse delta expression.

QuantumBlockEncoding.BlockEncodingClassics.SparseColumnCertificate

This record groups the data and proof fields needed for “sparse column certificate”. A proposition-valued field is a requirement until a constructor supplies it. Proof-carrying sparse-column contract.

QuantumBlockEncoding.BlockEncodingClassics.SparseColumnCertificate.correct

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

QuantumBlockEncoding.BlockEncodingClassics.RowColumnSparseCertificate

This record groups the data and proof fields needed for “row column sparse certificate”. A proposition-valued field is a requirement until a constructor supplies it. Proof-carrying row/column sparse contract for the general sparse route.

QuantumBlockEncoding.BlockEncodingClassics.RowColumnSparseCertificate.correct

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

QuantumBlockEncoding.BlockEncodingClassics.ValueToAmplitudeContract

This record groups the data and proof fields needed for “value to amplitude contract”. A proposition-valued field is a requirement until a constructor supplies it. Value-to-amplitude oracle contract.

QuantumBlockEncoding.BlockEncodingClassics.ValueToAmplitudeContract.correct

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

QuantumBlockEncoding.BlockEncodingClassics.IsSymmetric

This definition gives the library's named construction or computation for “is symmetric”. Symmetric matrix predicate for the rational backend.

QuantumBlockEncoding.BlockEncodingClassics.cleanBlockBy_symmetric_of_symmetric

Lean checks the proposition indexed as “clean block by symmetric of symmetric”; the hypotheses and conclusion in the code panel fix its exact scope. A symmetric full matrix has a symmetric clean block under any embedding.

QuantumBlockEncoding.BlockEncodingClassics.fin2Zero

This definition gives the library's named construction or computation for “fin 2 zero”. Two-by-two scalar dilation block.

QuantumBlockEncoding.BlockEncodingClassics.fin2One

This definition gives the library's named construction or computation for “fin 2 one”.

QuantumBlockEncoding.BlockEncodingClassics.scalarDilation

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

QuantumBlockEncoding.BlockEncodingClassics.scalarDilation_cleanEntry

Lean checks the proposition indexed as “scalar dilation clean entry”; the hypotheses and conclusion in the code panel fix its exact scope.

QuantumBlockEncoding.BlockEncodingClassics.scalarDilation_offdiag01

Lean checks the proposition indexed as “scalar dilation offdiag 01”; the hypotheses and conclusion in the code panel fix its exact scope.

QuantumBlockEncoding.BlockEncodingClassics.scalarDilation_offdiag10

Lean checks the proposition indexed as “scalar dilation offdiag 10”; the hypotheses and conclusion in the code panel fix its exact scope.

QuantumBlockEncoding.BlockEncodingClassics.scalarDilation_diag11

Lean checks the proposition indexed as “scalar dilation diag 11”; the hypotheses and conclusion in the code panel fix its exact scope.

QuantumBlockEncoding.BlockEncodingClassics.scalarDilationRowDot

This definition gives the library's named construction or computation for “scalar dilation row dot”. Two-entry row dot product for the scalar dilation block.

QuantumBlockEncoding.BlockEncodingClassics.scalarDilation_row0_normSq

Lean checks the proposition indexed as “scalar dilation row 0 norm sq”; the hypotheses and conclusion in the code panel fix its exact scope.

QuantumBlockEncoding.BlockEncodingClassics.scalarDilation_row1_normSq

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

QuantumBlockEncoding.BlockEncodingClassics.scalarDilation_row0_unit_norm_of

Lean checks the proposition indexed as “scalar dilation row 0 unit norm of”; the hypotheses and conclusion in the code panel fix its exact scope.

QuantumBlockEncoding.BlockEncodingClassics.scalarDilation_row1_unit_norm_of

Lean checks the proposition indexed as “scalar dilation row 1 unit norm of”; the hypotheses and conclusion in the code panel fix its exact scope.

QuantumBlockEncoding.BlockEncodingClassics.scalarDilation_rows01_orthogonal

Lean checks the proposition indexed as “scalar dilation rows 01 orthogonal”; the hypotheses and conclusion in the code panel fix its exact scope.

QuantumBlockEncoding.BlockEncodingClassics.scalarDilation_rows10_orthogonal

Lean checks the proposition indexed as “scalar dilation rows 10 orthogonal”; the hypotheses and conclusion in the code panel fix its exact scope.

QuantumBlockEncoding.BlockEncodingClassics.chebyshevT

This definition gives the library's named construction or computation for “chebyshev t”. Chebyshev polynomial values, kept as a small executable recurrence.

QuantumBlockEncoding.BlockEncodingClassics.chebyshevT_zero

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

QuantumBlockEncoding.BlockEncodingClassics.chebyshevT_one

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

QuantumBlockEncoding.BlockEncodingClassics.chebyshevT_two

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

QuantumBlockEncoding.BlockEncodingClassics.chebyshevT_succ_succ

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

QuantumBlockEncoding.BlockEncodingClassics.chebyshevT_three_recurrence

Lean checks the proposition indexed as “chebyshev t three recurrence”; the hypotheses and conclusion in the code panel fix its exact scope.

QuantumBlockEncoding.BlockEncodingClassics.chebyshevT_four_recurrence

Lean checks the proposition indexed as “chebyshev t four recurrence”; the hypotheses and conclusion in the code panel fix its exact scope.

QuantumBlockEncoding.BlockEncodingClassics.ExactCleanBlock

This record groups the data and proof fields needed for “exact clean block”. A proposition-valued field is a requirement until a constructor supplies it. Proof-carrying exact clean-block package.

QuantumBlockEncoding.BlockEncodingClassics.ExactCleanBlock.clean

This definition gives the library's named construction or computation for “clean”. The certified clean block associated with a proof-carrying package.

QuantumBlockEncoding.BlockEncodingClassics.ExactCleanBlock.clean_eq_target

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

QuantumBlockEncoding.BlockEncodingClassics.QubitizationChebyshevContract

This record groups the data and proof fields needed for “qubitization chebyshev contract”. A proposition-valued field is a requirement until a constructor supplies it. Qubitization/Chebyshev proof-carrying contract.

QuantumBlockEncoding.BlockEncodingClassics.partialPermutationCertificate

This definition gives the library's named construction or computation for “partial permutation certificate”. Abstract partial-permutation certificate.

QuantumBlockEncoding.BlockEncodingClassics.oneTermLCU

This definition gives the library's named construction or computation for “one term lcu”. One-term LCU leaf.

QuantumBlockEncoding.BlockEncodingClassics.oneTermLCU_cleanBlock

Lean checks the proposition indexed as “one term lcu clean block”; the hypotheses and conclusion in the code panel fix its exact scope.

QuantumBlockEncoding.BlockEncodingClassics.matrixScale

This definition gives the library's named construction or computation for “matrix scale”. Pointwise scalar multiplication for the project-local matrix backend.

QuantumBlockEncoding.BlockEncodingClassics.matrixAdd

This definition gives the library's named construction or computation for “matrix add”. Pointwise addition for the project-local matrix backend.

QuantumBlockEncoding.BlockEncodingClassics.weightedSum2

This definition gives the library's named construction or computation for “weighted sum 2”. Two-term weighted sum, the finite clean-block algebra behind a 2-term LCU.

QuantumBlockEncoding.BlockEncodingClassics.weightedSum2_entry

Lean checks the proposition indexed as “weighted sum 2 entry”; the hypotheses and conclusion in the code panel fix its exact scope.

QuantumBlockEncoding.BlockEncodingClassics.weightedSum2_congr_pointwise

Lean checks the proposition indexed as “weighted sum 2 congr pointwise”; the hypotheses and conclusion in the code panel fix its exact scope.

QuantumBlockEncoding.BlockEncodingClassics.LCUCertificate

This record groups the data and proof fields needed for “lcu certificate”. A proposition-valued field is a requirement until a constructor supplies it. Proof-carrying LCU contract.

QuantumBlockEncoding.BlockEncodingClassics.LCUCertificate.correct

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

QuantumBlockEncoding.BlockEncodingClassics.twoTermLCUCertificate

This definition gives the library's named construction or computation for “two term lcu certificate”. Two-term LCU arithmetic after both selected clean blocks have already been proved.

QuantumBlockEncoding.BlockEncodingClassics.twoTermLCUCertificate_cleanBlock_entry

Lean checks the proposition indexed as “two term lcu certificate clean block entry”; the hypotheses and conclusion in the code panel fix its exact scope.

QuantumBlockEncoding.BlockEncodingClassics.ExactCleanBlock.toLCUCertificate

This definition gives the library's named construction or computation for “to lcu certificate”. Promote an exact clean-block certificate to the LCU-style arithmetic layer.

QuantumBlockEncoding.BlockEncodingClassics.matrix_mul_congr_pointwise

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

QuantumBlockEncoding.BlockEncodingClassics.productCleanBlockCertificate

This definition gives the library's named construction or computation for “product clean block certificate”. Exact product certificate for already-extracted clean blocks.

QuantumBlockEncoding.BlockEncodingClassics.productExactCleanBlockCertificate

This definition gives the library's named construction or computation for “product exact clean block certificate”. Product bridge for exact clean-block certificates via the arithmetic layer.

QuantumBlockEncoding.BlockEncodingClassics.tensorResourceCost

This definition gives the library's named construction or computation for “tensor resource cost”. Tensor-style resource score: parallel depth is the maximum of two depths.

QuantumBlockEncoding.BlockEncodingClassics.tensorResourceCost_gateCount

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

QuantumBlockEncoding.BlockEncodingClassics.tensorResourceCost_depth

Lean checks the proposition indexed as “tensor resource cost depth”; the hypotheses and conclusion in the code panel fix its exact scope.

QuantumBlockEncoding.BlockEncodingClassics.productResourceCost

This definition gives the library's named construction or computation for “product resource cost”. Product-style resource score: sequential depth adds.

QuantumBlockEncoding.BlockEncodingClassics.productResourceCost_depth

Lean checks the proposition indexed as “product resource cost depth”; the hypotheses and conclusion in the code panel fix its exact scope.

QuantumBlockEncoding.BlockEncodingClassics.HermitianDilationContract

This record groups the data and proof fields needed for “hermitian dilation contract”. A proposition-valued field is a requirement until a constructor supplies it. Hermitian-dilation target shape.

QuantumBlockEncoding.BlockEncodingClassics.QSVTConsumerContract

This record groups the data and proof fields needed for “qsvt consumer contract”. A proposition-valued field is a requirement until a constructor supplies it. QSVT consumer contract.

QuantumBlockEncoding.BlockEncodingClassics.ZeroErrorApproxCleanBlock

This record groups the data and proof fields needed for “zero error approx clean block”. A proposition-valued field is a requirement until a constructor supplies it. Zero-error approximate incumbent at the clean-block level.

QuantumBlockEncoding.BlockEncodingClassics.exactAsZeroErrorApproxCleanBlock

This definition gives the library's named construction or computation for “exact as zero error approx clean block”. Any exact clean-block certificate can be used as a zero-error approximate incumbent in the adaptive exact-to-approximate ABEIS policy.

QuantumBlockEncoding.BlockEncodingClassics.exactAsZeroErrorApproxCleanBlock_bound

Lean checks the proposition indexed as “exact as zero error approx clean block bound”; the hypotheses and conclusion in the code panel fix its exact scope.

QuantumBlockEncoding.Gate

This type lists the allowed alternatives for “gate”; its constructors are the cases that downstream code must handle.

QuantumBlockEncoding.Circuit

This abbreviation gives a shorter name to the type or expression used for “circuit”.

QuantumBlockEncoding.Gate.resource

This definition gives the library's named construction or computation for “resource”. Conservative elementary-resource estimate for the current IR.

QuantumBlockEncoding.CircuitLayer

This abbreviation gives a shorter name to the type or expression used for “circuit layer”. A layer is a list of gates intended to be scheduled in parallel.

QuantumBlockEncoding.CircuitLayer.resource

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

QuantumBlockEncoding.LayeredCircuit

This abbreviation gives a shorter name to the type or expression used for “layered circuit”. A layered circuit is the schedule used for depth comparisons.

QuantumBlockEncoding.LayeredCircuit.resource

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

QuantumBlockEncoding.LayeredCircuit.depth

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

QuantumBlockEncoding.Circuit.resource

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

QuantumBlockEncoding.Circuit.resource_nil

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

QuantumBlockEncoding.Circuit.resource_cons

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

QuantumBlockEncoding.Circuit.depth

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

QuantumBlockEncoding.qubitDim

This definition gives the library's named construction or computation for “qubit dim”. A finite-dimensional basis size for an 'n'-qubit register.

QuantumBlockEncoding.SemanticObligation

This record groups the data and proof fields needed for “semantic obligation”. A proposition-valued field is a requirement until a constructor supplies it. Structured semantic obligation for the matrix layer.

QuantumBlockEncoding.GateMatrix

This record groups the data and proof fields needed for “gate matrix”. A proposition-valued field is a requirement until a constructor supplies it. One gate together with its matrix on the full 'qubits'-qubit Hilbert space.

QuantumBlockEncoding.gateMatricesMatchCircuit

This definition gives the library's named construction or computation for “gate matrices match circuit”. Check that a list of gate matrices labels exactly the same circuit gates.

QuantumBlockEncoding.evalGateMatrices

This definition gives the library's named construction or computation for “eval gate matrices”. Evaluate a list of full-space gate matrices to a circuit matrix.

QuantumBlockEncoding.Matrix.evalWith_foldl_add_mul

Lean checks the proposition indexed as “eval with foldl add mul”; the hypotheses and conclusion in the code panel fix its exact scope. Evaluate one symbolic matrix-product entry as a concrete finite Rat fold.

QuantumBlockEncoding.Matrix.evalWith_mul_apply

Lean checks the proposition indexed as “eval with mul apply”; the hypotheses and conclusion in the code panel fix its exact scope. Evaluate one entry of 'Matrix.mul' by evaluating each path contribution.

QuantumBlockEncoding.Matrix.evalWith_mul_eq_zero_of_all_paths_zero

Lean checks the proposition indexed as “eval with mul eq zero of all paths zero”; the hypotheses and conclusion in the code panel fix its exact scope. Evaluate one matrix-product entry as zero when every evaluated path contribution is zero.

QuantumBlockEncoding.Matrix.evalWith_mul_unique_path

Lean checks the proposition indexed as “eval with mul unique path”; the hypotheses and conclusion in the code panel fix its exact scope. Evaluate one matrix-product entry when all evaluated paths except 'k0' vanish.

QuantumBlockEncoding.Matrix.evalWith_mul_two_path

Lean checks the proposition indexed as “eval with mul two path”; the hypotheses and conclusion in the code panel fix its exact scope. Evaluate one matrix-product entry when all evaluated paths except 'k0' and 'k1' vanish.

QuantumBlockEncoding.Matrix.evalWith_mul_identity_right_apply

Lean checks the proposition indexed as “eval with mul identity right apply”; the hypotheses and conclusion in the code panel fix its exact scope. Evaluating a symbolic matrix after multiplying on the right by the identity recovers the evaluated entry.

QuantumBlockEncoding.Matrix.cast_square_apply

Lean checks the proposition indexed as “cast square apply”; the hypotheses and conclusion in the code panel fix its exact scope. Entry-level bridge for square matrix casts along a dimension equality.

QuantumBlockEncoding.evalWith_evalGateMatrices_single

Lean checks the proposition indexed as “eval with eval gate matrices single”; the hypotheses and conclusion in the code panel fix its exact scope. Evaluation-level single-gate reduction for 'evalGateMatrices'.

QuantumBlockEncoding.CircuitMatrixSemantics

This record groups the data and proof fields needed for “circuit matrix semantics”. A proposition-valued field is a requirement until a constructor supplies it. Circuit-level matrix semantics assembled from gate-level matrices.

QuantumBlockEncoding.CircuitMatrixSemantics.ofGateMatrices

This definition gives the library's named construction or computation for “of gate matrices”. Build circuit semantics directly from aligned gate matrices.

QuantumBlockEncoding.PreparedCircuitEntryTarget

This record groups the data and proof fields needed for “prepared circuit entry target”. A proposition-valued field is a requirement until a constructor supplies it. Typed target for relating an active circuit-matrix entry to a prepared composition entry.

QuantumBlockEncoding.PreparedCircuitEntryTarget.entryEqualityStatement

This definition gives the library's named construction or computation for “entry equality statement”. The prepared-composition equality required by the target.

QuantumBlockEncoding.PreparedCircuitEntryTarget.matrixEntryEqualityStatement

This definition gives the library's named construction or computation for “matrix entry equality statement”. The same equality stated directly on the backing matrices.

QuantumBlockEncoding.PreparedCircuitEntryTarget.entryEqualityStatement_iff_matrixEntryEqualityStatement

Lean checks the proposition indexed as “entry equality statement iff matrix entry equality statement”; the hypotheses and conclusion in the code panel fix its exact scope. The cached entry equality is equivalent to the backing matrix-entry equality.

QuantumBlockEncoding.BlockExtractionTarget

This record groups the data and proof fields needed for “block extraction target”. A proposition-valued field is a requirement until a constructor supplies it. A paper-level block-extraction target against a concrete circuit matrix.

QuantumBlockEncoding.blockExtractionBranchContributionSum

This definition gives the library's named construction or computation for “block extraction branch contribution sum”. Fold a finite family of branch contributions into one projected block entry.

QuantumBlockEncoding.BlockExtractionBranchContributionTarget

This record groups the data and proof fields needed for “block extraction branch contribution target”. A proposition-valued field is a requirement until a constructor supplies it. Typed interface for decomposing one block-extracted matrix entry into finite branch contributions.

QuantumBlockEncoding.BlockExtractionBranchContributionTarget.selectedBranchStatement

This definition gives the library's named construction or computation for “selected branch statement”. The selected-branch identity exposed by the target.

QuantumBlockEncoding.BlockExtractionBranchContributionTarget.projectionSummationStatement

This definition gives the library's named construction or computation for “projection summation statement”. The projection/summation theorem still required for the target.

QuantumBlockEncoding.BlockExtractionBranchContributionTarget.backendExpansionStatement

This definition gives the library's named construction or computation for “backend expansion statement”. The backend expansion theorem needed to close 'projectionSummationStatement'.

QuantumBlockEncoding.BlockExtractionBranchContributionTarget.selectedBranchStatement_of_eq

Lean checks the proposition indexed as “selected branch statement of eq”; the hypotheses and conclusion in the code panel fix its exact scope.

QuantumBlockEncoding.BlockExtractionBranchContributionTarget.projectionSummationStatement_iff_backendExpansionStatement

Lean checks the proposition indexed as “projection summation statement iff backend expansion statement”; the hypotheses and conclusion in the code panel fix its exact scope.

QuantumBlockEncoding.BlockExtractionBranchContributionTarget.projectionSummationStatement_of_backendExpansionStatement

Lean checks the proposition indexed as “projection summation statement of backend expansion statement”; the hypotheses and conclusion in the code panel fix its exact scope.

QuantumBlockEncoding.BlockExtractionBranchContributionTarget.backendExpansionStatement_of_projectionSummationStatement

Lean checks the proposition indexed as “backend expansion statement of projection summation statement”; the hypotheses and conclusion in the code panel fix its exact scope.

QuantumBlockEncoding.CircuitBlockEncodingClaim

This record groups the data and proof fields needed for “circuit block encoding claim”. A proposition-valued field is a requirement until a constructor supplies it. A circuit-level block encoding claim bundling a circuit matrix semantics with a block extraction target and a dimension compatibility proof.

QuantumBlockEncoding.FiniteBlockCompositionContract

This record groups the data and proof fields needed for “finite block composition contract”. A proposition-valued field is a requirement until a constructor supplies it. Typed contract for a finite-dimensional LCU/block-composition step.

QuantumBlockEncoding.signalSystemBlockRowIndex

This definition gives the library's named construction or computation for “signal system block row index”. Compound row index for a signal value and a system-row index.

QuantumBlockEncoding.signalSystemBlockColIndex

This definition gives the library's named construction or computation for “signal system block col index”. Compound column index for a signal value and a system-column index.

QuantumBlockEncoding.signalSystemBlockRowIndex_zero

Lean checks the proposition indexed as “signal system block row index zero”; the hypotheses and conclusion in the code panel fix its exact scope.

QuantumBlockEncoding.signalSystemBlockColIndex_zero

Lean checks the proposition indexed as “signal system block col index zero”; the hypotheses and conclusion in the code panel fix its exact scope.

QuantumBlockEncoding.signalSystemBlockRowIndex_lt

Lean checks the proposition indexed as “signal system block row index lt”; the hypotheses and conclusion in the code panel fix its exact scope. The row compound index stays inside a signal × row matrix.

QuantumBlockEncoding.signalSystemBlockColIndex_lt

Lean checks the proposition indexed as “signal system block col index lt”; the hypotheses and conclusion in the code panel fix its exact scope. The column compound index stays inside a signal × column matrix.

QuantumBlockEncoding.signalSystemBlockProjection

This definition gives the library's named construction or computation for “signal system block projection”. Block projection: extract the '(signalIdx, signalIdx)' block from a signal × system matrix.

QuantumBlockEncoding.signalSystemBlockProjection_apply

Lean checks the proposition indexed as “signal system block projection apply”; the hypotheses and conclusion in the code panel fix its exact scope.

QuantumBlockEncoding.totalCircuitQubits

This definition gives the library's named construction or computation for “total circuit qubits”. Total qubits needed for a circuit operating on 'system' system qubits and 'signal' signal qubits.

QuantumBlockEncoding.CircuitMatrixSemantics.blockExtractionTarget

This definition gives the library's named construction or computation for “block extraction target”. Build a BlockExtractionTarget from a CircuitMatrixSemantics by computing the block projection.

QuantumBlockEncoding.coldE1SystemIndex

This definition gives the library's named construction or computation for “cold e 1 system index”. System-register index for one-bit registers ordered as '(T, tau, S)'.

QuantumBlockEncoding.coldE1Target

This definition gives the library's named construction or computation for “cold e 1 target”. The target matrix for 'E_1'.

QuantumBlockEncoding.coldE1QueryTarget

This definition gives the library's named construction or computation for “cold e 1 query target”. Operator-first target metadata for the strict cold-start benchmark.

QuantumBlockEncoding.coldE1SignalIndex

This definition gives the library's named construction or computation for “cold e 1 signal index”. The clean block-selection index for the single signal ancilla.

QuantumBlockEncoding.coldE1BlockProjection

This definition gives the library's named construction or computation for “cold e 1 block projection”. Exact clean-block predicate for a one-signal-qubit candidate matrix.

QuantumBlockEncoding.coldE1ExactNormalizer

This definition gives the library's named construction or computation for “cold e 1 exact normalizer”. Exact normalizer for the requested block encoding.

QuantumBlockEncoding.coldE1ExactError

This definition gives the library's named construction or computation for “cold e 1 exact error”. Exact error for the requested block encoding.

QuantumBlockEncoding.coldE1SourceLayout

This definition gives the library's named construction or computation for “cold e 1 source layout”. Source-facing layout: three system qubits and one clean signal ancilla.

QuantumBlockEncoding.coldE1HighLevelSeedCost

This definition gives the library's named construction or computation for “cold e 1 high level seed cost”. Source-facing seed cost under the high-level reversible-gate convention in the conversion window.

QuantumBlockEncoding.coldE1HighLevelSeedCost_gateCount

Lean checks the proposition indexed as “cold e 1 high level seed cost gate count”; the hypotheses and conclusion in the code panel fix its exact scope.

QuantumBlockEncoding.coldE1HighLevelSeedCost_depth

Lean checks the proposition indexed as “cold e 1 high level seed cost depth”; the hypotheses and conclusion in the code panel fix its exact scope.

QuantumBlockEncoding.coldE1HighLevelSeedCost_auxiliaryQubits

Lean checks the proposition indexed as “cold e 1 high level seed cost auxiliary qubits”; the hypotheses and conclusion in the code panel fix its exact scope.

QuantumBlockEncoding.coldE1HighLevelSeedCost_oracleCalls

Lean checks the proposition indexed as “cold e 1 high level seed cost oracle calls”; the hypotheses and conclusion in the code panel fix its exact scope.

QuantumBlockEncoding.coldE1CandidateImage

This definition gives the library's named construction or computation for “cold e 1 candidate image”. Candidate 'COLD-CLEAN-PERM-001' as a finite image table on '(signal,T,tau,S)' basis states.

QuantumBlockEncoding.coldE1CandidateMatrix

This definition gives the library's named construction or computation for “cold e 1 candidate matrix”. Column-vector permutation matrix for 'COLD-CLEAN-PERM-001'.

QuantumBlockEncoding.coldE1CandidateImage_clean_source_state0

Lean checks the proposition indexed as “cold e 1 candidate image clean source state 0”; the hypotheses and conclusion in the code panel fix its exact scope.

QuantumBlockEncoding.coldE1CandidateImage_clean_source_state1

Lean checks the proposition indexed as “cold e 1 candidate image clean source state 1”; the hypotheses and conclusion in the code panel fix its exact scope.

QuantumBlockEncoding.coldE1CandidateImage_injective_pointwise

Lean checks the proposition indexed as “cold e 1 candidate image injective pointwise”; the hypotheses and conclusion in the code panel fix its exact scope.

QuantumBlockEncoding.coldE1CandidateImage_injective

Lean checks the proposition indexed as “cold e 1 candidate image injective”; the hypotheses and conclusion in the code panel fix its exact scope.

QuantumBlockEncoding.coldE1CandidatePreimage

This definition gives the library's named construction or computation for “cold e 1 candidate preimage”. Explicit inverse image table for the task-local permutation certificate.

QuantumBlockEncoding.coldE1CandidateImage_preimage

Lean checks the proposition indexed as “cold e 1 candidate image preimage”; the hypotheses and conclusion in the code panel fix its exact scope.

QuantumBlockEncoding.coldE1CandidateImage_surjective

Lean checks the proposition indexed as “cold e 1 candidate image surjective”; the hypotheses and conclusion in the code panel fix its exact scope.

QuantumBlockEncoding.coldE1CandidateImage_permutation_certificate

Lean checks the proposition indexed as “cold e 1 candidate image permutation certificate”; the hypotheses and conclusion in the code panel fix its exact scope.

QuantumBlockEncoding.coldE1Target_support_state0

Lean checks the proposition indexed as “cold e 1 target support state 0”; the hypotheses and conclusion in the code panel fix its exact scope.

QuantumBlockEncoding.coldE1Target_support_state1

Lean checks the proposition indexed as “cold e 1 target support state 1”; the hypotheses and conclusion in the code panel fix its exact scope.

QuantumBlockEncoding.coldE1Candidate_blockProjection

Lean checks the proposition indexed as “cold e 1 candidate block projection”; the hypotheses and conclusion in the code panel fix its exact scope.

QuantumBlockEncoding.coldE1QueryTarget_normalizer

Lean checks the proposition indexed as “cold e 1 query target normalizer”; the hypotheses and conclusion in the code panel fix its exact scope.

QuantumBlockEncoding.coldE1SourceLayout_auxiliaryQubits

Lean checks the proposition indexed as “cold e 1 source layout auxiliary qubits”; the hypotheses and conclusion in the code panel fix its exact scope.

QuantumBlockEncoding.ConcreteSemantics.FiniteMatrix

This abbreviation gives a shorter name to the type or expression used for “finite matrix”. A Mathlib finite matrix, definitionally compatible with ABEIS 'Matrix'.

QuantumBlockEncoding.ConcreteSemantics.StateVector

This abbreviation gives a shorter name to the type or expression used for “state vector”. A finite column vector.

QuantumBlockEncoding.ConcreteSemantics.basisKet

This definition gives the library's named construction or computation for “basis ket”. A computational-basis ket in the concrete finite backend.

QuantumBlockEncoding.ConcreteSemantics.zeroKet

This definition gives the library's named construction or computation for “zero ket”. The all-zero computational-basis ket for an 'n'-qubit register.

QuantumBlockEncoding.ConcreteSemantics.applyVec

This definition gives the library's named construction or computation for “apply vec”. Matrix-vector action using Mathlib's finite sum semantics.

QuantumBlockEncoding.ConcreteSemantics.ComplexUnitaryGate

This record groups the data and proof fields needed for “complex unitary gate”. A proposition-valued field is a requirement until a constructor supplies it. A finite complex gate whose unitarity is the standard Mathlib unitary-group predicate rather than an unconstrained proposition.

QuantumBlockEncoding.ConcreteSemantics.applyVec_basisKet

Lean checks the proposition indexed as “apply vec basis ket”; the hypotheses and conclusion in the code panel fix its exact scope. Acting on a basis ket selects the corresponding matrix column.

QuantumBlockEncoding.ConcreteSemantics.applyVec_zeroKet

Lean checks the proposition indexed as “apply vec zero ket”; the hypotheses and conclusion in the code panel fix its exact scope. Acting on the all-zero ket selects column zero.

QuantumBlockEncoding.ConcreteSemantics.firstColumnMatches_iff_applyVec_zeroKet

Lean checks the proposition indexed as “first column matches iff apply vec zero ket”; the hypotheses and conclusion in the code panel fix its exact scope. The ABEIS first-column contract is exactly the state-action equation 'U |0^n> = |psi>' in the concrete finite matrix backend.

QuantumBlockEncoding.ConcreteSemantics.ComplexStatePreparationCertificate

This record groups the data and proof fields needed for “complex state preparation certificate”. A proposition-valued field is a requirement until a constructor supplies it. Concrete state-preparation evidence.

QuantumBlockEncoding.ConcreteSemantics.ComplexStatePreparationCertificate.candidate

This definition gives the library's named construction or computation for “candidate”. Repackage concrete semantics in the existing generic candidate interface.

QuantumBlockEncoding.ConcreteSemantics.ComplexStatePreparationCertificate.verified

This definition gives the library's named construction or computation for “verified”. Promote a concrete certificate to the existing verified wrapper.

QuantumBlockEncoding.ConcreteSemantics.ComplexStatePreparationCertificate.preparesVector

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

QuantumBlockEncoding.ConcreteSemantics.ProductRegisterMatrix

This abbreviation gives a shorter name to the type or expression used for “product register matrix”. A matrix indexed by an explicit signal-register/system-register product.

QuantumBlockEncoding.ConcreteSemantics.flatToProductRegister

This definition gives the library's named construction or computation for “flat to product register”. View a flattened signal-system matrix through explicit product-register indices.

QuantumBlockEncoding.ConcreteSemantics.productRegisterBlockProjection

This definition gives the library's named construction or computation for “product register block projection”. Project one signal branch from an explicit product-register matrix.

QuantumBlockEncoding.ConcreteSemantics.productRegisterBlockProjection_flatToProductRegister

Lean checks the proposition indexed as “product register block projection flat to product register”; the hypotheses and conclusion in the code panel fix its exact scope. Product-register projection after viewing a flat matrix is definitionally the existing ABEIS flattened block projection.

QuantumBlockEncoding.ConcreteSemantics.productIndex_val_eq_signalSystemBlockRowIndex

Lean checks the proposition indexed as “product index val eq signal system block row index”; the hypotheses and conclusion in the code panel fix its exact scope. The classic product index and circuit-semantics row index have the same value.

QuantumBlockEncoding.ConcreteSemantics.signalSystemBlockProjection_eq_cleanBlockProduct

Lean checks the proposition indexed as “signal system block projection eq clean block product”; the hypotheses and conclusion in the code panel fix its exact scope. The classic rational clean block and the generic circuit-semantics projection are the same pointwise matrix under the shared register order.

QuantumBlockEncoding.ConcreteSemantics.cleanBasisActionAmplitude

This definition gives the library's named construction or computation for “clean basis action amplitude”. The clean output amplitude obtained by applying 'operator' to a clean signal-system basis input.

QuantumBlockEncoding.ConcreteSemantics.cleanBasisActionAmplitude_eq_signalSystemBlockProjection

Lean checks the proposition indexed as “clean basis action amplitude eq signal system block projection”; the hypotheses and conclusion in the code panel fix its exact scope. Acting on a clean basis input and reading a clean output is one projected-block entry.

QuantumBlockEncoding.ConcreteSemantics.pointwiseProjection_iff_cleanBasisAction

Lean checks the proposition indexed as “pointwise projection iff clean basis action”; the hypotheses and conclusion in the code panel fix its exact scope. Finite-dimensional bridge between the projected-block definition and the clean-branch action proof.

QuantumBlockEncoding.Matrix

This abbreviation gives a shorter name to the type or expression used for “matrix”. A finite matrix represented by its entries.

QuantumBlockEncoding.Matrix.PointwiseEq

This definition gives the library's named construction or computation for “pointwise eq”. Pointwise equality for finite matrices.

QuantumBlockEncoding.Matrix.zero

This definition gives the library's named construction or computation for “zero”. The zero finite matrix.

QuantumBlockEncoding.Matrix.identity

This definition gives the library's named construction or computation for “identity”. The identity finite matrix.

QuantumBlockEncoding.Matrix.mul

This definition gives the library's named construction or computation for “mul”. Finite matrix multiplication with the project-local 'Matrix' representation.

QuantumBlockEncoding.gridSize

This definition gives the library's named construction or computation for “grid size”. Number of grid points in an 'n'-qubit register.

QuantumBlockEncoding.clog2

This definition gives the library's named construction or computation for “clog 2”. Small ceiling-log helper for resource bookkeeping.

QuantumBlockEncoding.gridSize_zero

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

QuantumBlockEncoding.clog2_zero

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

QuantumBlockEncoding.clog2_one

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

QuantumBlockEncoding.log2_pred_two_pow_succ

Lean checks the proposition indexed as “log 2 pred two pow succ”; the hypotheses and conclusion in the code panel fix its exact scope. 'log2 (2^(n+1)-1) = n', the arithmetic fact behind 'clog2_gridSize'.

QuantumBlockEncoding.clog2_gridSize

Lean checks the proposition indexed as “clog 2 grid size”; the hypotheses and conclusion in the code panel fix its exact scope. The bit-width of an 'n'-qubit grid is 'n'.

QuantumBlockEncoding.BoundaryKind

This type lists the allowed alternatives for “boundary kind”; its constructors are the cases that downstream code must handle. Boundary conditions tracked by this library.

QuantumBlockEncoding.Stencil

This record groups the data and proof fields needed for “stencil”. A proposition-valued field is a requirement until a constructor supplies it. Finite-difference stencil metadata.

QuantumBlockEncoding.Stencil.width

This definition gives the library's named construction or computation for “width”. The number of columns touched by a stencil row before boundary corrections.

QuantumBlockEncoding.Stencil.width_eq

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

QuantumBlockEncoding.BulkWindow

This record groups the data and proof fields needed for “bulk window”. A proposition-valued field is a requirement until a constructor supplies it. A central bulk interval '[lower, upper]' inside the computational basis rows.

QuantumBlockEncoding.BulkWindow.paperBoundaryLines

This definition gives the library's named construction or computation for “paper boundary lines”. Number of boundary-side rows outside the bulk, using the paper's convention.

QuantumBlockEncoding.Coeff

This type lists the allowed alternatives for “coeff”; its constructors are the cases that downstream code must handle. A lightweight symbolic coefficient language for stencil entries.

QuantumBlockEncoding.Coeff.sub

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

QuantumBlockEncoding.Coeff.evalWith

This definition gives the library's named construction or computation for “eval with”. Evaluate a symbolic 'Coeff' to a concrete 'Rat' given an environment.

QuantumBlockEncoding.Coeff.evalWith_rat

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

QuantumBlockEncoding.Coeff.evalWith_symbol

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

QuantumBlockEncoding.Coeff.evalWith_add

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

QuantumBlockEncoding.Coeff.evalWith_mul

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

QuantumBlockEncoding.Coeff.evalWith_neg

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

QuantumBlockEncoding.Coeff.rat_zero

Lean checks the proposition indexed as “rat zero”; the hypotheses and conclusion in the code panel fix its exact scope. Trivial reflexivity lemma for the zero rational coefficient.

QuantumBlockEncoding.Coeff.evalWith_rat_zero

Lean checks the proposition indexed as “eval with rat zero”; the hypotheses and conclusion in the code panel fix its exact scope. Evaluating 'Coeff.rat 0' yields '0' under any environment.

QuantumBlockEncoding.Coeff.evalWith_rat_one

Lean checks the proposition indexed as “eval with rat one”; the hypotheses and conclusion in the code panel fix its exact scope. Evaluating 'Coeff.rat 1' yields '1' under any environment.

QuantumBlockEncoding.Coeff.evalWith_rat_add

Lean checks the proposition indexed as “eval with rat add”; the hypotheses and conclusion in the code panel fix its exact scope. Evaluating 'Coeff.add (Coeff.rat a) (Coeff.rat b)' yields 'a + b'.

QuantumBlockEncoding.Coeff.evalWith_rat_mul

Lean checks the proposition indexed as “eval with rat mul”; the hypotheses and conclusion in the code panel fix its exact scope. Evaluating 'Coeff.mul (Coeff.rat a) (Coeff.rat b)' yields 'a * b'.

QuantumBlockEncoding.Coeff.evalWith_rat_neg

Lean checks the proposition indexed as “eval with rat neg”; the hypotheses and conclusion in the code panel fix its exact scope. Evaluating 'Coeff.neg (Coeff.rat a)' yields '-a'.

QuantumBlockEncoding.Coeff.evalWith_eq_zero_of_rat_zero

Lean checks the proposition indexed as “eval with eq zero of rat zero”; the hypotheses and conclusion in the code panel fix its exact scope. If a Coeff value is 'Coeff.rat 0', it evaluates to '0' under any environment.

QuantumBlockEncoding.Coeff.evalWith_eq_one_of_rat_one

Lean checks the proposition indexed as “eval with eq one of rat one”; the hypotheses and conclusion in the code panel fix its exact scope. If a Coeff value is 'Coeff.rat 1', it evaluates to '1' under any environment.

QuantumBlockEncoding.Coeff.divNat

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

QuantumBlockEncoding.StencilEntry

This record groups the data and proof fields needed for “stencil entry”. A proposition-valued field is a requirement until a constructor supplies it. One symbolic nonzero entry in a finite-difference row.

QuantumBlockEncoding.CubicDiagonalOracle.cubicN2ControlWires

This definition gives the library's named construction or computation for “cubic n 2 control wires”. The first two wires are system controls and wire two is the clean signal.

QuantumBlockEncoding.CubicDiagonalOracle.cubicN2ControlWires_ne_signal

Lean checks the proposition indexed as “cubic n 2 control wires ne signal”; the hypotheses and conclusion in the code panel fix its exact scope.

QuantumBlockEncoding.CubicDiagonalOracle.cubicN2ControlIndex

This definition gives the library's named construction or computation for “cubic n 2 control index”. Decode the two little-endian system controls.

QuantumBlockEncoding.CubicDiagonalOracle.cubicN2Amplitude_abs_le_one

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

QuantumBlockEncoding.CubicDiagonalOracle.cubicN2Angle

This definition gives the library's named construction or computation for “cubic n 2 angle”. Exact standard-RY angle for the selected cubic amplitude.

QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveCircuit

This definition gives the library's named construction or computation for “cubic n 2 primitive circuit”. Four-way uniformly controlled rotation, compiled to primitive gates.

QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveProgram

This definition gives the library's named construction or computation for “cubic n 2 primitive program”.

QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveCircuit_eval

Lean checks the proposition indexed as “cubic n 2 primitive circuit eval”; the hypotheses and conclusion in the code panel fix its exact scope. Exact matrix semantics of the emitted gate list.

QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveProgram_eval

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

QuantumBlockEncoding.CubicDiagonalOracle.cubicN2EncodeBits

This definition gives the library's named construction or computation for “cubic n 2 encode bits”. Encode a signal value and a two-qubit system index into three named wires.

QuantumBlockEncoding.CubicDiagonalOracle.cubicN2EncodeBits_signal

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

QuantumBlockEncoding.CubicDiagonalOracle.cubicN2ControlIndex_encode

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

QuantumBlockEncoding.CubicDiagonalOracle.cubicN2EncodeBits_context_eq_iff

Lean checks the proposition indexed as “cubic n 2 encode bits context eq iff”; the hypotheses and conclusion in the code panel fix its exact scope.

QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveProgram_cleanEntry

Lean checks the proposition indexed as “cubic n 2 primitive program clean entry”; the hypotheses and conclusion in the code panel fix its exact scope. The primitive program's clean signal block is exactly the cubic diagonal.

QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveFlatUnitary

This definition gives the library's named construction or computation for “cubic n 2 primitive flat unitary”. Flat little-endian unitary used by the operator-certificate interface.

QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveFlatUnitary_unitary

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

QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveCleanIndex

This definition gives the library's named construction or computation for “cubic n 2 primitive clean index”.

QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveFlatUnitary_cleanBlock

Lean checks the proposition indexed as “cubic n 2 primitive flat unitary clean block”; the hypotheses and conclusion in the code panel fix its exact scope.

QuantumBlockEncoding.CubicDiagonalOracle.cubicN2ComplexTarget

This definition gives the library's named construction or computation for “cubic n 2 complex target”.

QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitivePresentation

This definition gives the library's named construction or computation for “cubic n 2 primitive presentation”.

QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveResource

This definition gives the library's named construction or computation for “cubic n 2 primitive resource”.

QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveOperatorCandidate

This definition gives the library's named construction or computation for “cubic n 2 primitive operator candidate”.

QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveVerifiedBlockEncoding

This definition gives the library's named construction or computation for “cubic n 2 primitive verified block encoding”. Exact unitarity and clean-block promotion for the finite cubic route.

QuantumBlockEncoding.CubicDiagonalOracle.cubicN2Primitive_oracleCalls_eq_zero

Lean checks the proposition indexed as “cubic n 2 primitive oracle calls eq zero”; the hypotheses and conclusion in the code panel fix its exact scope. No opaque oracle survives in the accepted primitive resource row.

QuantumBlockEncoding.CubicDiagonalOracle.cubicN2Primitive_resource_faithful

Lean checks the proposition indexed as “cubic n 2 primitive resource faithful”; the hypotheses and conclusion in the code panel fix its exact scope. Resource ownership is definitional rather than a handwritten tuple.

QuantumBlockEncoding.CubicStatePreparation.taskId

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

QuantumBlockEncoding.CubicStatePreparation.requestedEpsilon

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

QuantumBlockEncoding.CubicStatePreparation.gridPoint

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

QuantumBlockEncoding.CubicStatePreparation.cubicAmplitude

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

QuantumBlockEncoding.CubicStatePreparation.cubicOperator

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

QuantumBlockEncoding.CubicStatePreparation.cubicNormSq

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

QuantumBlockEncoding.CubicStatePreparation.conservativeNormalizer

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

QuantumBlockEncoding.CubicStatePreparation.cubicTarget

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

QuantumBlockEncoding.CubicStatePreparation.defaultRequiredCost

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

QuantumBlockEncoding.CubicStatePreparation.defaultPolicy

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

QuantumBlockEncoding.CubicStatePreparation.arithmeticCubicDefaultPrecision

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

QuantumBlockEncoding.CubicStatePreparation.arithmeticCubicLayout

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

QuantumBlockEncoding.CubicStatePreparation.arithmeticCubicCircuit

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

QuantumBlockEncoding.CubicStatePreparation.arithmeticCubicResource

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

QuantumBlockEncoding.CubicStatePreparation.arithmeticCubicNormalizer

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

QuantumBlockEncoding.CubicStatePreparation.arithmeticCubicCost

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

QuantumBlockEncoding.CubicStatePreparation.arithmeticCubicResourceTuple

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

QuantumBlockEncoding.CubicStatePreparation.arithmeticCubicResource_eq

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

QuantumBlockEncoding.CubicStatePreparation.arithmeticCubicLayout_auxiliaryQubits

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

QuantumBlockEncoding.CubicStatePreparation.arithmeticCubicClaim

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

QuantumBlockEncoding.CubicStatePreparation.arithmeticRankOneCubicLayout

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

QuantumBlockEncoding.CubicStatePreparation.arithmeticRankOneCubicCircuit

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

QuantumBlockEncoding.CubicStatePreparation.arithmeticRankOneCubicResource

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

QuantumBlockEncoding.CubicStatePreparation.arithmeticRankOneCubicNormalizer

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

QuantumBlockEncoding.CubicStatePreparation.arithmeticRankOneCubicCost

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

QuantumBlockEncoding.CubicStatePreparation.arithmeticRankOneCubicResourceTuple

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

QuantumBlockEncoding.CubicStatePreparation.arithmeticRankOneCubicResource_eq

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

QuantumBlockEncoding.CubicStatePreparation.arithmeticRankOneCubicLayout_auxiliaryQubits

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

QuantumBlockEncoding.CubicStatePreparation.arithmeticRankOneCubicResourceTuple_n2_default

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

QuantumBlockEncoding.CubicStatePreparation.arithmeticRankOneCubicClaim

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

QuantumBlockEncoding.CubicStatePreparation.hadamardCountingCubicWorkspace

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

QuantumBlockEncoding.CubicStatePreparation.hadamardCountingCubicLayout

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

QuantumBlockEncoding.CubicStatePreparation.hadamardCountingCubicCircuit

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

QuantumBlockEncoding.CubicStatePreparation.hadamardCountingCubicCircuit_rejectSignalRepair

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

QuantumBlockEncoding.CubicStatePreparation.hadamardCountingCubicResource

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

QuantumBlockEncoding.CubicStatePreparation.hadamardCountingCubicNormalizer

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

QuantumBlockEncoding.CubicStatePreparation.hadamardCountingCubicCost

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

QuantumBlockEncoding.CubicStatePreparation.hadamardCountingCubicResourceTuple

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

QuantumBlockEncoding.CubicStatePreparation.hadamardCountingCubicResource_eq

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

QuantumBlockEncoding.CubicStatePreparation.hadamardCountingCubicLayout_auxiliaryQubits

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

QuantumBlockEncoding.CubicStatePreparation.hadamardCountingCubicResourceTuple_n2

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

QuantumBlockEncoding.CubicStatePreparation.hadamardCountingCubicClaim

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

QuantumBlockEncoding.CubicStatePreparation.hardModeUpperAgentSchedule

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

QuantumBlockEncoding.CubicStatePreparation.hardModeMiddleAgentSchedule

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

QuantumBlockEncoding.CubicStatePreparation.hardModeLowerAgentSchedule

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

QuantumBlockEncoding.CubicStatePreparation.hardModeExactStallWindow

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

QuantumBlockEncoding.CubicStatePreparation.hardModeConstructionStallWindow

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

QuantumBlockEncoding.CubicStatePreparation.hardModeLevelCycleBudget

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

QuantumBlockEncoding.CubicStatePreparation.relaxedEpsilonLadder

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

QuantumBlockEncoding.CubicStatePreparation.relaxedEpsilonLadder_startsWithRequested

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

QuantumBlockEncoding.CubicStatePreparation.hardModeSchedules_have_four_levels

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

QuantumBlockEncoding.CubicStatePreparation.hardModeLowerAgentSchedule_final

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

QuantumBlockEncoding.CubicStatePreparation.initialExpectedPhase

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

QuantumBlockEncoding.CubicStatePreparation.gridSize_pos

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

QuantumBlockEncoding.CubicStatePreparation.cubicOperator_first_column

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

QuantumBlockEncoding.CubicStatePreparation.cubicOperator_only_first_column

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

QuantumBlockEncoding.CubicStatePreparation.rankOneCleanBlockContract

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

QuantumBlockEncoding.CubicStatePreparation.arithmeticRankOneCubicCleanBlockContract

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

QuantumBlockEncoding.CubicStatePreparation.rankOneCleanBlockContract_pointwise_eq

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

QuantumBlockEncoding.CubicStatePreparation.arithmeticRankOneCubicCleanBlockContract_pointwise_eq

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

QuantumBlockEncoding.CubicStatePreparation.hadamardCountingCubicCleanBlockContract

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

QuantumBlockEncoding.CubicStatePreparation.hadamardCountingCubicCleanBlockContract_pointwise_eq

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

QuantumBlockEncoding.CubicStatePreparation.rat_cube_sq_eq_sixth

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

QuantumBlockEncoding.CubicStatePreparation.cubicAmplitude_sq_eq_gridPoint_sixth

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

QuantumBlockEncoding.CubicStatePreparation.cubicNormSq_sixthPowerFold

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

QuantumBlockEncoding.CubicStatePreparation.gridSize_rat_ne_zero

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

QuantumBlockEncoding.CubicStatePreparation.gridSize_rat_pos

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

QuantumBlockEncoding.CubicStatePreparation.rat_div_cube_div_eq

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

QuantumBlockEncoding.CubicStatePreparation.cubicAmplitude_div_conservativeNormalizer_eq

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

QuantumBlockEncoding.CubicStatePreparation.gridSize_three_mul_eq_cube

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

QuantumBlockEncoding.CubicStatePreparation.gridSize_four_mul_eq_fourth

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

QuantumBlockEncoding.CubicStatePreparation.hadamardCountingCubic_thresholdCountP_finRange

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

QuantumBlockEncoding.CubicStatePreparation.hadamardCountingCubic_thresholdFilterLength

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

QuantumBlockEncoding.CubicStatePreparation.hadamardCountingCubic_threshold_le_pathCapacity

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

QuantumBlockEncoding.CubicStatePreparation.hadamardCountingCubic_thresholdPathCount

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

QuantumBlockEncoding.CubicStatePreparation.gridPoint_nonneg

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

QuantumBlockEncoding.CubicStatePreparation.gridPoint_lt_one

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

QuantumBlockEncoding.CubicStatePreparation.gridPoint_le_one

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

QuantumBlockEncoding.CubicStatePreparation.rat_pow_le_one_of_nonneg_le_one

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

QuantumBlockEncoding.CubicStatePreparation.cubicAmplitude_sq_le_one

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

QuantumBlockEncoding.CubicStatePreparation.foldl_add_le_add_length

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

QuantumBlockEncoding.CubicStatePreparation.cubicNormSq_le_gridSize

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

QuantumBlockEncoding.CubicStatePreparation.gridSize_rat_le_sq

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

QuantumBlockEncoding.CubicStatePreparation.cubicNormSq_le_conservativeNormalizer_sq

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

QuantumBlockEncoding.CubicStatePreparation.cubicNormSq_le_arithmeticCubicNormalizer_sq

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

QuantumBlockEncoding.CubicStatePreparation.cubicNormSq_le_hadamardCountingCubicNormalizer_sq

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

QuantumBlockEncoding.CubicStatePreparation.cubicNormSq_n1

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

QuantumBlockEncoding.CubicStatePreparation.cubicNormSq_n2

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

QuantumBlockEncoding.CubicStatePreparation.cubicNormSq_n3

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

QuantumBlockEncoding.CubicDiagonalOracle.taskId

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

QuantumBlockEncoding.CubicDiagonalOracle.cubicDiagonalOperator

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

QuantumBlockEncoding.CubicDiagonalOracle.exactNormalizer

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

QuantumBlockEncoding.CubicDiagonalOracle.cubicDiagonalTarget

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

QuantumBlockEncoding.CubicDiagonalOracle.linearDiagonalOperator

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

QuantumBlockEncoding.CubicDiagonalOracle.linearDiagonalTarget

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

QuantumBlockEncoding.CubicDiagonalOracle.linearDiagonalCleanBlockContract

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

QuantumBlockEncoding.CubicDiagonalOracle.linearDiagonalCleanBlockContract_pointwise_eq

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

QuantumBlockEncoding.CubicDiagonalOracle.linearDiagonalCleanBlock_eq_target

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

QuantumBlockEncoding.CubicDiagonalOracle.linearDiagonalExactCleanBlockFromPointwise

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

QuantumBlockEncoding.CubicDiagonalOracle.linearDiagonalExactCleanBlockFromPointwise_clean_eq_target

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

QuantumBlockEncoding.CubicDiagonalOracle.LinearDiagonalInputBEContract

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

QuantumBlockEncoding.CubicDiagonalOracle.LinearDiagonalInputBEContract.exactPayload

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

QuantumBlockEncoding.CubicDiagonalOracle.LinearDiagonalInputBEContract.clean_eq_target

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

QuantumBlockEncoding.CubicDiagonalOracle.householderZero

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

QuantumBlockEncoding.CubicDiagonalOracle.dot8

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

QuantumBlockEncoding.CubicDiagonalOracle.householder8E0Minus

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

QuantumBlockEncoding.CubicDiagonalOracle.householder8

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

QuantumBlockEncoding.CubicDiagonalOracle.householder8E0Minus_normSq

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

QuantumBlockEncoding.CubicDiagonalOracle.householder8E0Minus_normSq_ne_zero

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

QuantumBlockEncoding.CubicDiagonalOracle.householder8_clean_entry

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

QuantumBlockEncoding.CubicDiagonalOracle.householder8_isRationalOrthogonal

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

QuantumBlockEncoding.CubicDiagonalOracle.controlledHouseholder8SystemIndex

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

QuantumBlockEncoding.CubicDiagonalOracle.controlledHouseholder8AncillaIndex

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

QuantumBlockEncoding.CubicDiagonalOracle.controlledHouseholder8Embed

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

QuantumBlockEncoding.CubicDiagonalOracle.controlledHouseholder8DirectSum

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

QuantumBlockEncoding.CubicDiagonalOracle.controlledHouseholder8_branchNontrivial_of_clean

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

QuantumBlockEncoding.CubicDiagonalOracle.controlledHouseholder8DirectSum_clean_entry

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

QuantumBlockEncoding.CubicDiagonalOracle.controlledHouseholder8DirectSum_columnInner_eq_identity_of_system_ne

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

QuantumBlockEncoding.CubicDiagonalOracle.controlledHouseholder8DirectSum_columnInner_eq_branch

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

QuantumBlockEncoding.CubicDiagonalOracle.controlledHouseholder8DirectSum_rowInner_eq_branch

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

QuantumBlockEncoding.CubicDiagonalOracle.controlledHouseholder8DirectSum_rowInner_eq_identity_of_system_ne

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

QuantumBlockEncoding.CubicDiagonalOracle.controlledHouseholder8DirectSum_isRationalOrthogonal

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

QuantumBlockEncoding.CubicDiagonalOracle.LinearDiagonalRationalCompletion

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

QuantumBlockEncoding.CubicDiagonalOracle.linearDiagonalFourSquareBranchVector

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

QuantumBlockEncoding.CubicDiagonalOracle.linearDiagonalFourSquareBranchVector_clean

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

QuantumBlockEncoding.CubicDiagonalOracle.linearDiagonalFourSquareBranchVector_unit

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

QuantumBlockEncoding.CubicDiagonalOracle.linearDiagonalRationalCompletion_of_fourSquareWitnesses

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

QuantumBlockEncoding.CubicDiagonalOracle.linearDiagonalRationalCompletion_exists

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

QuantumBlockEncoding.CubicDiagonalOracle.linearDiagonalRationalCompletion_branchData

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

QuantumBlockEncoding.CubicDiagonalOracle.linearDiagonalRationalCompletion_backendSupport

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

QuantumBlockEncoding.CubicDiagonalOracle.linearDiagonalHouseholderCircuit

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

QuantumBlockEncoding.CubicDiagonalOracle.linearDiagonalHouseholderResource

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

QuantumBlockEncoding.CubicDiagonalOracle.linearDiagonalHouseholderResource_eq

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

QuantumBlockEncoding.CubicDiagonalOracle.linearDiagonalHouseholderInputBEContract

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

QuantumBlockEncoding.CubicDiagonalOracle.linearDiagonalHouseholderInputBEContract_clean_eq_target

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

QuantumBlockEncoding.CubicDiagonalOracle.linearDiagonalHouseholderInputBEContract_complete

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

QuantumBlockEncoding.CubicDiagonalOracle.approxDiagonalOperator

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

QuantumBlockEncoding.CubicDiagonalOracle.ratAbs

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

QuantumBlockEncoding.CubicDiagonalOracle.IsDiagonalRatMatrix

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

QuantumBlockEncoding.CubicDiagonalOracle.DiagonalRatOperatorNormBridge

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

QuantumBlockEncoding.CubicDiagonalOracle.ratSquaredEuclideanNorm

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

QuantumBlockEncoding.CubicDiagonalOracle.ratMatrixErrorAction

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

QuantumBlockEncoding.CubicDiagonalOracle.ratEuclideanOperatorNormErrorAtMost

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

QuantumBlockEncoding.CubicDiagonalOracle.ratMatrixErrorAction_eq_diagonal

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

QuantumBlockEncoding.CubicDiagonalOracle.ratAbs_nonneg

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

QuantumBlockEncoding.CubicDiagonalOracle.rat_mul_self_eq_ratAbs_mul_self

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

QuantumBlockEncoding.CubicDiagonalOracle.rat_mul_self_nonneg

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

QuantumBlockEncoding.CubicDiagonalOracle.rat_mul_self_le_of_abs_le

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

QuantumBlockEncoding.CubicDiagonalOracle.rat_mul_self_vector_le_of_abs_le

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

QuantumBlockEncoding.CubicDiagonalOracle.ratEuclideanDiagonalOperatorNormBridge

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

QuantumBlockEncoding.CubicDiagonalOracle.ratEuclideanOperatorNormErrorAtMost_not_vacuous

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

QuantumBlockEncoding.CubicDiagonalOracle.approxDiagonalOperator_isDiagonal

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

QuantumBlockEncoding.CubicDiagonalOracle.cubicDiagonalOperator_isDiagonal

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

QuantumBlockEncoding.CubicDiagonalOracle.approxDiagonalEntrywiseErrorAtMost

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

QuantumBlockEncoding.CubicDiagonalOracle.approxDiagonalOperator_entrywise_error

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

QuantumBlockEncoding.CubicDiagonalOracle.approxDiagonalOperator_operatorNorm_error_of_contract

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

QuantumBlockEncoding.CubicDiagonalOracle.approxDiagonalOperator_operatorNorm_error

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

QuantumBlockEncoding.CubicDiagonalOracle.rationalCircleBranchVector

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

QuantumBlockEncoding.CubicDiagonalOracle.rationalCircleBranchVector_clean

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

QuantumBlockEncoding.CubicDiagonalOracle.rationalCircleBranchVector_unit

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

QuantumBlockEncoding.CubicDiagonalOracle.controlledHouseholder8DirectSum_clean_entry_of_branchValue

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

QuantumBlockEncoding.CubicDiagonalOracle.cubicDiagonalFourSquareBranchVector

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

QuantumBlockEncoding.CubicDiagonalOracle.cubicDiagonalFourSquareBranchVector_clean

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

QuantumBlockEncoding.CubicDiagonalOracle.cubicDiagonalFourSquareBranchVector_unit

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

QuantumBlockEncoding.CubicDiagonalOracle.CubicDiagonalRationalCompletion

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

QuantumBlockEncoding.CubicDiagonalOracle.cubicDiagonalRationalCompletion_of_fourSquareWitnesses

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

QuantumBlockEncoding.CubicDiagonalOracle.cubicDiagonalRationalCompletion_exists

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

QuantumBlockEncoding.CubicDiagonalOracle.cubicAmplitude_lt_one

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

QuantumBlockEncoding.CubicDiagonalOracle.cubicDiagonalRationalCompletion_backendSupport

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

QuantumBlockEncoding.CubicDiagonalOracle.CubicDiagonalExactBEContract

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

QuantumBlockEncoding.CubicDiagonalOracle.cubicDiagonalHouseholderExactBEContract

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

QuantumBlockEncoding.CubicDiagonalOracle.cubicDiagonalHouseholderExactBEContract_clean_eq_target

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

QuantumBlockEncoding.CubicDiagonalOracle.cubicDiagonalHouseholderExactBEContract_complete

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

QuantumBlockEncoding.CubicDiagonalOracle.linearDiagonal_cube_eq_cubicDiagonalOperator

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

QuantumBlockEncoding.CubicDiagonalOracle.linearDiagonalCubicProductCertificate

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

QuantumBlockEncoding.CubicDiagonalOracle.linearDiagonalCubicProductCertificate_target_eq

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

QuantumBlockEncoding.CubicDiagonalOracle.linearDiagonalCubicProductCertificate_clean_eq_target

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

QuantumBlockEncoding.CubicDiagonalOracle.cubicQSVTPolynomial

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

QuantumBlockEncoding.CubicDiagonalOracle.cubicQSVTPolynomial_gridPoint_abs_le_one

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

QuantumBlockEncoding.CubicDiagonalOracle.CubicQSVTLocalSideConditions

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

QuantumBlockEncoding.CubicDiagonalOracle.cubicQSVTLocalSideConditions

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

QuantumBlockEncoding.CubicDiagonalOracle.CubicQSVTExternalSemantics

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

QuantumBlockEncoding.CubicDiagonalOracle.CubicQSVTExternalSemantics.output_eq_cubic_target

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

QuantumBlockEncoding.CubicDiagonalOracle.CubicQSVTExternalSemantics.consumerContract

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

QuantumBlockEncoding.CubicDiagonalOracle.amplitudeOracleLayout

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

QuantumBlockEncoding.CubicDiagonalOracle.amplitudeOracleCircuit

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

QuantumBlockEncoding.CubicDiagonalOracle.amplitudeOracleResource

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

QuantumBlockEncoding.CubicDiagonalOracle.amplitudeOracleCost

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

QuantumBlockEncoding.CubicDiagonalOracle.amplitudeOracleResourceTuple

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

QuantumBlockEncoding.CubicDiagonalOracle.amplitudeOracleResource_eq

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

QuantumBlockEncoding.CubicDiagonalOracle.amplitudeOracleResourceTuple_eq

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

QuantumBlockEncoding.CubicDiagonalOracle.diagonalCleanBlockContract

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

QuantumBlockEncoding.CubicDiagonalOracle.diagonalCleanBlockContract_pointwise_eq

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

QuantumBlockEncoding.CubicDiagonalOracle.primitiveOracleCleanBlock_eq_target

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

QuantumBlockEncoding.CubicDiagonalOracle.cubicAmplitude_le_one

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

QuantumBlockEncoding.CubicDiagonalOracle.cubicAmplitude_nonneg

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

QuantumBlockEncoding.CubicDiagonalOracle.primitiveAmplitudeOracleDimension

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

QuantumBlockEncoding.CubicDiagonalOracle.primitiveAmplitudeOracleUnitary

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

QuantumBlockEncoding.CubicDiagonalOracle.primitiveAmplitudeOracleIsUnitary

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

QuantumBlockEncoding.CubicDiagonalOracle.primitiveAmplitudeOracleCleanBlockExtracts

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

QuantumBlockEncoding.CubicDiagonalOracle.primitiveAmplitudeOracleSemanticContract

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

QuantumBlockEncoding.CubicDiagonalOracle.primitiveAmplitudeOracleSemanticContract_unitary

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

QuantumBlockEncoding.CubicDiagonalOracle.primitiveAmplitudeOracleSemanticContract_cleanBlock_eq_target

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

QuantumBlockEncoding.CubicDiagonalOracle.expandedAmplitudeOracleLayout

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

QuantumBlockEncoding.CubicDiagonalOracle.expandedAmplitudeOracleLayout_auxiliaryQubits

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

QuantumBlockEncoding.CubicDiagonalOracle.expandedAmplitudeOracleNormalizer_eq

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

QuantumBlockEncoding.CubicDiagonalOracle.StandardRyCleanEntryScalarTier

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

QuantumBlockEncoding.CubicDiagonalOracle.expandedRyCleanEntryForCubicAmplitudes

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

QuantumBlockEncoding.CubicDiagonalOracle.expandedRyCleanEntryForCubicAmplitudes_of_standardTier

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

QuantumBlockEncoding.CubicDiagonalOracle.expandedArithmeticComputesCubicAmplitude

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

QuantumBlockEncoding.CubicDiagonalOracle.ExpandedCubicArithmeticBackend

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

QuantumBlockEncoding.CubicDiagonalOracle.symbolicExpandedCubicArithmeticBackend

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

QuantumBlockEncoding.CubicDiagonalOracle.expandedArithmeticBackendComputesCubicAmplitude

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

QuantumBlockEncoding.CubicDiagonalOracle.symbolicExpandedCubicArithmeticBackend_computes

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

QuantumBlockEncoding.CubicDiagonalOracle.expandedArithmeticBackendBridge

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

QuantumBlockEncoding.CubicDiagonalOracle.expandedArithmeticComputesCubicAmplitude_of_backendBridge

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

QuantumBlockEncoding.CubicDiagonalOracle.expandedArithmeticBackendBridge_iff_of_computes

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

QuantumBlockEncoding.CubicDiagonalOracle.expandedArithmeticComputesCubicAmplitude_of_symbolicBackendBridge

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

QuantumBlockEncoding.CubicDiagonalOracle.symbolicExpandedCubicArithmeticBackend_bridge_iff

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

QuantumBlockEncoding.CubicDiagonalOracle.fixedDenomCubicPayload_lt_capacity

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

QuantumBlockEncoding.CubicDiagonalOracle.fixedDenomCubicAmplitude_eq

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

QuantumBlockEncoding.CubicDiagonalOracle.fixedDenomCubicArithmeticBackend

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

QuantumBlockEncoding.CubicDiagonalOracle.fixedDenomCubicArithmeticBackend_computes

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

QuantumBlockEncoding.CubicDiagonalOracle.expandedArithmeticComputesCubicAmplitudeTransparent

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

QuantumBlockEncoding.CubicDiagonalOracle.fixedDenomCubicArithmeticRouteTransparent

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

QuantumBlockEncoding.CubicDiagonalOracle.fixedDenomCubicArithmeticBackend_bridge_iff

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

QuantumBlockEncoding.CubicDiagonalOracle.expandedControlledRyUsesCubicAngle

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

QuantumBlockEncoding.CubicDiagonalOracle.expandedControlledRyUsesCubicAngleTransparent

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

QuantumBlockEncoding.CubicDiagonalOracle.fixedDenomControlledRyRouteTransparent

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

QuantumBlockEncoding.CubicDiagonalOracle.expandedControlledRyBackendBridge

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

QuantumBlockEncoding.CubicDiagonalOracle.expandedControlledRyUsesCubicAngle_of_backendBridge

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

QuantumBlockEncoding.CubicDiagonalOracle.expandedControlledRyBackendBridge_iff_of_standardTier

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

QuantumBlockEncoding.CubicDiagonalOracle.ExpandedControlledRyWorkspaceReadonlyWitness

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

QuantumBlockEncoding.CubicDiagonalOracle.expandedControlledRyWorkspaceReadonlyTransparent

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

QuantumBlockEncoding.CubicDiagonalOracle.expandedWorkspaceCleanUncomputed

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

QuantumBlockEncoding.CubicDiagonalOracle.ExpandedArithmeticCleanUncomputeWitness

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

QuantumBlockEncoding.CubicDiagonalOracle.expandedWorkspaceCleanUncomputedTransparent

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

QuantumBlockEncoding.CubicDiagonalOracle.expandedWorkspaceCleanUncomputedTransparent_of_witness

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

QuantumBlockEncoding.CubicDiagonalOracle.fixedDenomCubicComputeStep

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

QuantumBlockEncoding.CubicDiagonalOracle.fixedDenomCubicUncomputeStep

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

QuantumBlockEncoding.CubicDiagonalOracle.fixedDenomCubicComputeStep_matches_backend_on_clean

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

QuantumBlockEncoding.CubicDiagonalOracle.fixedDenomCubicUncomputeStep_after_compute

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

QuantumBlockEncoding.CubicDiagonalOracle.fixedDenomExpandedArithmeticCleanUncomputeWitness

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

QuantumBlockEncoding.CubicDiagonalOracle.fixedDenomWorkspaceCleanUncomputedTransparent

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

QuantumBlockEncoding.CubicDiagonalOracle.LinearDiagonalValueBackend

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

QuantumBlockEncoding.CubicDiagonalOracle.linearDiagonalValueBackendComputesGridPoint

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

QuantumBlockEncoding.CubicDiagonalOracle.fixedDenomLinearDiagonalValueBackend

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

QuantumBlockEncoding.CubicDiagonalOracle.fixedDenomLinearDiagonalValueBackend_computes

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

QuantumBlockEncoding.CubicDiagonalOracle.LinearDiagonalValueCleanUncomputeWitness

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

QuantumBlockEncoding.CubicDiagonalOracle.linearDiagonalWorkspaceCleanUncomputedTransparent

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

QuantumBlockEncoding.CubicDiagonalOracle.linearDiagonalWorkspaceCleanUncomputedTransparent_of_witness

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

QuantumBlockEncoding.CubicDiagonalOracle.fixedDenomLinearDiagonalComputeStep

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

QuantumBlockEncoding.CubicDiagonalOracle.fixedDenomLinearDiagonalUncomputeStep

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

QuantumBlockEncoding.CubicDiagonalOracle.fixedDenomLinearDiagonalComputeStep_matches_backend_on_clean

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

QuantumBlockEncoding.CubicDiagonalOracle.fixedDenomLinearDiagonalUncomputeStep_after_compute

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

QuantumBlockEncoding.CubicDiagonalOracle.fixedDenomLinearDiagonalCleanUncomputeWitness

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

QuantumBlockEncoding.CubicDiagonalOracle.fixedDenomLinearDiagonalWorkspaceCleanUncomputedTransparent

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

QuantumBlockEncoding.CubicDiagonalOracle.expandedAmplitudeOracleCleanBlockExtracts

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

QuantumBlockEncoding.CubicDiagonalOracle.expandedAmplitudeOracleCleanBlockContract

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

QuantumBlockEncoding.CubicDiagonalOracle.expandedAmplitudeOracleCleanBlockContract_diagonal

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

QuantumBlockEncoding.CubicDiagonalOracle.expandedAmplitudeOracleCleanBlockContract_eq_target

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

QuantumBlockEncoding.CubicDiagonalOracle.expandedAmplitudeOracleSemanticContract

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

QuantumBlockEncoding.CubicDiagonalOracle.expandedAmplitudeOracleSemanticContract_cleanBlock_eq_target

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

QuantumBlockEncoding.CubicDiagonalOracle.primitiveAmplitudeOracleCandidate

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

QuantumBlockEncoding.CubicDiagonalOracle.primitiveAmplitudeOracleCandidate_costTuple_eq

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

QuantumBlockEncoding.CubicDiagonalOracle.primitiveAmplitudeOracleCandidate_unitary_from_contract

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

QuantumBlockEncoding.CubicDiagonalOracle.primitiveAmplitudeOracleCandidate_block_from_contract

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

QuantumBlockEncoding.CubicDiagonalOracle.primitiveAmplitudeOracleVerified

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

QuantumBlockEncoding.CubicDiagonalOracle.amplitudeOracleClaim

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

QuantumBlockEncoding.Examples.RobinHeat.fourthOrderSecondDerivative

This definition gives the library's named construction or computation for “fourth order second derivative”.

QuantumBlockEncoding.Examples.RobinHeat.centralBulkEntries

This definition gives the library's named construction or computation for “central bulk entries”.

QuantumBlockEncoding.Examples.RobinHeat.A1dx

This definition gives the library's named construction or computation for “a 1 dx”.

QuantumBlockEncoding.Examples.RobinHeat.B1dx

This definition gives the library's named construction or computation for “b 1 dx”.

QuantumBlockEncoding.Examples.RobinHeat.leftBoundaryRow0

This definition gives the library's named construction or computation for “left boundary row 0”. First row after eliminating the left Robin ghost points.

QuantumBlockEncoding.Examples.RobinHeat.leftBoundaryRow1

This definition gives the library's named construction or computation for “left boundary row 1”. Second row after eliminating the left Robin ghost points.

QuantumBlockEncoding.Examples.RobinHeat.rightBoundaryRowNm2

This definition gives the library's named construction or computation for “right boundary row nm 2”. Penultimate row after eliminating the right Robin ghost points.

QuantumBlockEncoding.Examples.RobinHeat.rightBoundaryRowNm1

This definition gives the library's named construction or computation for “right boundary row nm 1”. Last row after eliminating the right Robin ghost points.

QuantumBlockEncoding.Examples.RobinHeat.robinWindow

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

QuantumBlockEncoding.Examples.RobinHeat.oneTermParameters

This definition gives the library's named construction or computation for “one term parameters”.

QuantumBlockEncoding.Examples.RobinHeat.fourthOrderStencilWidth

Lean checks the proposition indexed as “fourth order stencil width”; the hypotheses and conclusion in the code panel fix its exact scope.

QuantumBlockEncoding.Examples.RobinHeat.robinHeatAncillas

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

QuantumBlockEncoding.GHL2025.OneTermRobinParameters

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

QuantumBlockEncoding.GHL2025.isBulkRow

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

QuantumBlockEncoding.GHL2025.isBoundaryRow

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

QuantumBlockEncoding.GHL2025.RobinRegisterPartition

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

QuantumBlockEncoding.GHL2025.RobinRegisterPartition.totalQubits

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

QuantumBlockEncoding.GHL2025.defaultRobinRegisterPartition

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

QuantumBlockEncoding.GHL2025.RobinRegisterPartition.totalPureAncillas

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

QuantumBlockEncoding.GHL2025.oneTermRobinResourceExpr

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

QuantumBlockEncoding.GHL2025.deviatingIndices

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

QuantumBlockEncoding.GHL2025.oneTermRobinPreciseResourceExpr

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

QuantumBlockEncoding.GHL2025.deviatingIndices_example

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

QuantumBlockEncoding.GHL2025.oneTermRobinResource

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

QuantumBlockEncoding.GHL2025.oneTermRobin_pureAncilla

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

QuantumBlockEncoding.GHL2025.oneTermRobinLayout

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

QuantumBlockEncoding.GHL2025.oneTermRobinCircuit

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

QuantumBlockEncoding.GHL2025.oneTermRobinTheoremFacingFig4Circuit

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

QuantumBlockEncoding.GHL2025.oneTermRobinTheoremFacingFig4Circuit_gateList

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

QuantumBlockEncoding.GHL2025.oneTermRobinActiveBackendCircuit_gateList

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

QuantumBlockEncoding.GHL2025.oneTermRobinNormalizer

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

QuantumBlockEncoding.GHL2025.oneTermRobinSpec

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

QuantumBlockEncoding.GHL2025.oneTermRobinSpec_ancilla

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

QuantumBlockEncoding.GHL2025.oneTermRobinSpec_circuitCost

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

QuantumBlockEncoding.GHL2025.oneTermRobinNormalizer_eval

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

QuantumBlockEncoding.GHL2025.oneTermRobinClaim

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

QuantumBlockEncoding.GHL2025.oneDimHamiltonianResourceExpr

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

QuantumBlockEncoding.GHL2025.oneDimHamiltonianClaim

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

QuantumBlockEncoding.GHL2025.multiDimHamiltonianResourceExpr

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

QuantumBlockEncoding.GHL2025.multiDimHamiltonianClaim

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

QuantumBlockEncoding.GHL2025.ObligationRecord

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

QuantumBlockEncoding.GHL2025.RobinCircuitSkeleton

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

QuantumBlockEncoding.GHL2025.RobinGamma1

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

QuantumBlockEncoding.GHL2025.RobinGamma2

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

QuantumBlockEncoding.GHL2025.RobinGamma3

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

QuantumBlockEncoding.GHL2025.RobinWavefunctionDecomposition

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

QuantumBlockEncoding.GHL2025.defaultRobinWavefunctionDecomposition

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

QuantumBlockEncoding.GHL2025.RobinProofObligations

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

QuantumBlockEncoding.GHL2025.defaultRobinCircuitSkeleton

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

QuantumBlockEncoding.GHL2025.BandedSparseAccessPaperContract

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

QuantumBlockEncoding.GHL2025.defaultBandedSparseAccessPaperContract

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

QuantumBlockEncoding.GHL2025.DerivativeOracleContract

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

QuantumBlockEncoding.GHL2025.FunctionOracleContract

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

QuantumBlockEncoding.GHL2025.derivativeOracleResource

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

QuantumBlockEncoding.GHL2025.derivativeOracleResource_pureAncilla

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

QuantumBlockEncoding.GHL2025.OneTermRobinTheoremData

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

QuantumBlockEncoding.GHL2025.defaultOneTermRobinTheoremData

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

QuantumBlockEncoding.GHL2025.RobinBoundaryRotationAngle

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

QuantumBlockEncoding.GHL2025.RobinBoundaryRotationSet

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

QuantumBlockEncoding.GHL2025.RobinBoundaryRotationSet.expectedCount

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

QuantumBlockEncoding.GHL2025.importedClaims

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

QuantumBlockEncoding.GHL2025.oneTermRobinTotalQubits

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

QuantumBlockEncoding.GHL2025.effectiveRobinSignalQubits

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

QuantumBlockEncoding.GHL2025.defaultOneTermRobinTheoremData_signalQubits_eq_layout

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

QuantumBlockEncoding.GHL2025.defaultOneTermRobinTheoremData_pureAncillas_eq_layout

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

QuantumBlockEncoding.GHL2025.defaultOneTermRobinTheoremData_pureAncillas_eq_resource

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

QuantumBlockEncoding.GHL2025.effectiveRobinSignalQubits_eq_layout_signal_plus_visibleWorkspace

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

QuantumBlockEncoding.GHL2025.effectiveRobinSignalQubits_eq_theoremData_signal_plus_visibleWorkspace

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

QuantumBlockEncoding.GHL2025.robinIndicatorBitPosition

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

QuantumBlockEncoding.GHL2025.robinSparseColumnMap

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

QuantumBlockEncoding.GHL2025.oneTermRobinGlobalSparseOffset

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

QuantumBlockEncoding.GHL2025.oneTermRobinGlobalSparseAddress

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

QuantumBlockEncoding.GHL2025.oneTermRobinGlobalSparseAddress_lt_gridSize

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

QuantumBlockEncoding.GHL2025.oneTermRobinGlobalSparseInverseSlot

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

QuantumBlockEncoding.GHL2025.oneTermRobinGlobalSparseInverseSlot_lt_eight

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

QuantumBlockEncoding.GHL2025.oneTermRobinGlobalSparseInverseSlot_lt_seven

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

QuantumBlockEncoding.GHL2025.oneTermRobinGlobalSparseInverseSlot_involutive_of_lt_seven

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

QuantumBlockEncoding.GHL2025.oneTermRobinGlobalSparseInverseSlot_injective_of_lt_seven

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

QuantumBlockEncoding.GHL2025.oneTermRobinGlobalSparseAddress_inverseSlot_address_eq

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

QuantumBlockEncoding.GHL2025.oneTermRobinGlobalSparseOffset_lt_gridSize_of_lt_seven

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

QuantumBlockEncoding.GHL2025.oneTermRobinGlobalSparseAddress_comp_eq_mod_offset_sum

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

QuantumBlockEncoding.GHL2025.oneTermRobinGlobalSparseOffset_sum_mod_eq_zero_unique_of_lt_seven

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

QuantumBlockEncoding.GHL2025.oneTermRobinGlobalSparseAddress_inverseSlot_unique_of_lt_seven

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

QuantumBlockEncoding.GHL2025.oneTermRobinGlobalSparseAddress_same_row_injective_of_lt_seven

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

QuantumBlockEncoding.GHL2025.robinSparseColumnBranchValid

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

QuantumBlockEncoding.GHL2025.robinSparseColumnBranchValid_boundaryUnused_n3

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

QuantumBlockEncoding.GHL2025.robinSparseColumnMap_lt_gridSize_of_row_lt

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

QuantumBlockEncoding.GHL2025.robinSparseReverseColumnIndex

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

QuantumBlockEncoding.GHL2025.robinSparseColumnMap_zero

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

QuantumBlockEncoding.GHL2025.robinSparseColumnMap_one

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

QuantumBlockEncoding.GHL2025.robinSparseColumnMap_bulk

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

QuantumBlockEncoding.GHL2025.robinSparseColumnMap_rightBoundaryPrev

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

QuantumBlockEncoding.GHL2025.robinSparseColumnMap_rightBoundaryLast

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

QuantumBlockEncoding.GHL2025.robinSparseReverseColumnIndex_zero

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

QuantumBlockEncoding.GHL2025.robinSparseReverseColumnIndex_one

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

QuantumBlockEncoding.GHL2025.robinSparseReverseColumnIndex_bulk

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

QuantumBlockEncoding.GHL2025.robinSparseReverseColumnIndex_rightBoundaryPrev

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

QuantumBlockEncoding.GHL2025.robinSparseReverseColumnIndex_rightBoundaryLast

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

QuantumBlockEncoding.GHL2025.robinSparseReverseColumnRoundtrip_of_lt_eight

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

QuantumBlockEncoding.GHL2025.robinSparseReverseColumnIndex_lt_eight_of_columnMap

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

QuantumBlockEncoding.GHL2025.robinSparseReverseColumnRoundtripCheck

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

QuantumBlockEncoding.GHL2025.BandedSparseAccessPaperRegisters

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperRegisters

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperRegisters_row_lt_gridSize

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperRegisters_sparseIndexValue_eq

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperRegisters_paddedZeroValue_eq

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperRegisters_sparseIndex_lt

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperRegisters_odRegisterValue_lt

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessRowDependentPaperAddress

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperAddress

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperAddressInRange

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperAddressInRange_iff

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperAddress_lt_gridSize_of_two_le

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperAddressInRange_eq_true_of_two_le

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperImage

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessRowDependentPaperImage

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperRegisterValue_eq_mod

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperHighWidth_le_totalQubits

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperImage_lowBlock_lt_highBase_of_address_lt

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperImage_mod_lowBase

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperImage_div_lowBase_mod_eq

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperImage_lt_qubitDim_of_address_lt

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperImageFin

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperImageFin_val

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperImage_rowValue_eq

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperImage_odRegisterValue_eq

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperHighTail

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperImage_highTail_eq_of_address_lt

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperImageNoSpill

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperImageNoSpill_iff

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperImageNoSpill_eq_true_of_address_lt

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperImageNoSpill_eq_true_of_two_le

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperCleanInput

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperSparseIndexInKappa

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperGlobalSlotSource

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperGlobalSlotSource_cleanInput_eq_true

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperGlobalSlotSource_sparseIndex_lt_kappa

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperGlobalSlotSource_inverseSlot_injective

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperAddress_same_row_injective_of_globalSlotSource

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperValidSparseBranch

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperValidCleanSource

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperValidCleanSource_cleanInput_eq_true

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperValidCleanSource_validSparseBranch_eq_true

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperValidCleanSource_separates_boundaryCollision_n3

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperUnusedSparseBranch

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperUnusedSparseBranch_cleanInput_eq_true

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperUnusedSparseBranch_validSparseBranch_eq_false

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperCleanDomainSplit_iff

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperCleanDomainSplit_disjoint

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

QuantumBlockEncoding.GHL2025.BandedSparseAccessUnusedBranchImageRuleContract

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessUnusedBranchImageRuleContract

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessUnusedBranchImageRuleContract_flags_false

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessUnusedBranchImageRuleContract_of_unusedBranch

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

QuantumBlockEncoding.GHL2025.BandedSparseAccessUnusedBranchExtensionContract

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessUnusedBranchExtensionContract

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessUnusedBranchExtensionContract_flags_false

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessUnusedBranchExtensionContract_boundaryCollision_n3

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessUnusedBranchExtensionContract_of_unusedBranch

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

QuantumBlockEncoding.GHL2025.BandedSparseAccessFullCleanDomainExtensionContract

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessFullCleanDomainExtensionContract

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessFullCleanDomainExtensionContract_flags_false

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessFullCleanDomainExtensionContract_of_unusedBranch

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessFullCleanDomainExtensionContract_localCleanDomainSplit

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

QuantumBlockEncoding.GHL2025.BandedSparseAccessUnusedZeroBranchSourceDecision

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessUnusedZeroBranchSourceDecision

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessUnusedZeroBranchSourceDecision_flags_false

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessUnusedZeroBranchSourceDecision_keepsFullDomainFlagsFalse

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessUnusedZeroBranchSourceDecision_keepsImageRuleUnspecified

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessUnusedZeroBranchSourceDecision_keepsPaperContractFlagsFalse

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

QuantumBlockEncoding.GHL2025.BandedSparseAccessRobinZeroInclusionSourceContract

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessRobinZeroInclusionSourceContract

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessRobinZeroInclusionSourceContract_blocks_unusedZeroBranch

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessRobinZeroInclusionSourceContract_keepsImageRuleUnspecified

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

QuantumBlockEncoding.GHL2025.BandedSparseAccessPriorPDESourceContract

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPriorPDESourceContract

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

QuantumBlockEncoding.GHL2025.robinBandedSparseAccessCitationChain

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

QuantumBlockEncoding.GHL2025.robinBandedSparseAccessCitationChain_eq

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPriorPDESourceContract_blocks_unusedZeroBranch

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPriorPDESourceContract_oracleEquation

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPriorPDESourceContract_resource_unproved

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperCleanInput_iff

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

QuantumBlockEncoding.GHL2025.BandedSparseAccessPaperColumnContract

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperColumnContract

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperColumnContract_inputRegisters_eq

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperColumnContract_cleanInput_eq

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperColumnContract_cleanInput_iff

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperColumnContract_unitaryExtension_proved_eq_false

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperColumnContract_imageIndex_eq

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperColumnContract_addressInRange_eq

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperColumnContract_imageNoSpill_eq

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperColumnContract_rowPreserved_eq_true

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperColumnContract_addressWritten_eq_true_of_address_lt

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperColumnContract_addressInRange_eq_true_of_address_lt

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperColumnContract_imageNoSpill_eq_true_of_address_lt

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperColumnContract_registerSafety_of_address_lt

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperMatrix

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperMatrix_eq_image

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperMatrix_imageFin_eq_one

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperDaggerMatrix

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperDaggerMatrix_eq_image

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

QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperDaggerMatrix_imageFin_eq_one

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

QuantumBlockEncoding.GHL2025.robinSparseAmplitudeValue

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

QuantumBlockEncoding.GHL2025.robinGlobalSparseAmplitudeValue

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

QuantumBlockEncoding.GHL2025.robinGlobalSparseAmplitudeValue_boundarySlot2_row0_n3

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

QuantumBlockEncoding.GHL2025.robinGlobalSparseAmplitudeValue_boundarySlot2_differs_rowLocal_n3

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

QuantumBlockEncoding.GHL2025.DerivativeNormalizerNDContract

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

QuantumBlockEncoding.GHL2025.derivativeNormalizerNDContract

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

QuantumBlockEncoding.GHL2025.derivativeNormalizerNDContract_coefficient

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

QuantumBlockEncoding.GHL2025.derivativeNormalizerNDContract_normalizerND

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

QuantumBlockEncoding.GHL2025.derivativeNormalizerNDContract_normalizedCoefficient

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

QuantumBlockEncoding.GHL2025.DerivativeNormalizerNDSourceBound

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

QuantumBlockEncoding.GHL2025.derivativeNormalizerNDSourceBound

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

QuantumBlockEncoding.GHL2025.derivativeNormalizerNDSourceBound_sourceCoefficient

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

QuantumBlockEncoding.GHL2025.derivativeNormalizerNDSourceBound_normalizerND

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

QuantumBlockEncoding.GHL2025.derivativeNormalizerNDSourceBound_boundFormula

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

QuantumBlockEncoding.GHL2025.derivativeNormalizerNDSourceBound_coefficientBound

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

QuantumBlockEncoding.GHL2025.derivativeNormalizerNDSourceBound_coefficientBound_false

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

QuantumBlockEncoding.GHL2025.indicatorOracleMatrix

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

QuantumBlockEncoding.GHL2025.oneTermRobinGate_U_indic

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

QuantumBlockEncoding.GHL2025.oneTermRobinGate_U_indic_dagger

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

QuantumBlockEncoding.GHL2025.oneTermRobinGate_U_indic_dagger_matrix_eq

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

QuantumBlockEncoding.GHL2025.sparseAmplitudeOracleDTMatrix

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

QuantumBlockEncoding.GHL2025.SparseAmplitudeOracleDTPaperRegisters

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

QuantumBlockEncoding.GHL2025.sparseAmplitudeOracleDTPaperRegisters

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

QuantumBlockEncoding.GHL2025.sparseAmplitudeOracleDTCosHalf

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

QuantumBlockEncoding.GHL2025.sparseAmplitudeOracleDTSinHalf

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

QuantumBlockEncoding.GHL2025.sparseAmplitudeOracleDTCoefficientNormalizerObligation

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

QuantumBlockEncoding.GHL2025.SparseAmplitudeOracleDTCoefficientNormalizerContract

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

QuantumBlockEncoding.GHL2025.sparseAmplitudeOracleDTCoefficientNormalizerContract

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

QuantumBlockEncoding.GHL2025.sparseAmplitudeOracleDTNormalizedCoefficient

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

QuantumBlockEncoding.GHL2025.SparseAmplitudeOracleDTCoefficientNormalizerProofRoute

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

QuantumBlockEncoding.GHL2025.sparseAmplitudeOracleDTCoefficientNormalizerProofRoute

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

QuantumBlockEncoding.GHL2025.sparseAmplitudeOracleDTCoefficientNormalizerProofRoute_coefficient

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

QuantumBlockEncoding.GHL2025.sparseAmplitudeOracleDTCoefficientNormalizerProofRoute_normalizerND

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

QuantumBlockEncoding.GHL2025.sparseAmplitudeOracleDTCoefficientNormalizerProofRoute_normalizedCoefficient

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

QuantumBlockEncoding.GHL2025.sparseAmplitudeOracleDTCoefficientNormalizerProofRoute_sharedND

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

QuantumBlockEncoding.GHL2025.sparseAmplitudeOracleDTCoefficientNormalizerProofRoute_sourceBound

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

QuantumBlockEncoding.GHL2025.sparseAmplitudeOracleDTCoefficientNormalizerProofRoute_ketZeroEntry

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

QuantumBlockEncoding.GHL2025.sparseAmplitudeOracleDTCoefficientNormalizerProofRoute_ketOneEntry

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

QuantumBlockEncoding.GHL2025.sparseAmplitudeOracleDTRotationMatrix

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

QuantumBlockEncoding.GHL2025.oneTermRobinGate_O_DT_S

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

QuantumBlockEncoding.GHL2025.BoundaryRotationPaperRegisters

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

QuantumBlockEncoding.GHL2025.boundaryRotationPaperRegisters

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

QuantumBlockEncoding.GHL2025.boundaryRotationCosHalf

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

QuantumBlockEncoding.GHL2025.boundaryRotationSinHalf

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

QuantumBlockEncoding.GHL2025.boundaryRotationAngleNormalizerObligation

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

QuantumBlockEncoding.GHL2025.BoundaryRotationAngleNormalizerContract

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

QuantumBlockEncoding.GHL2025.boundaryRotationAngleNormalizerContract

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

QuantumBlockEncoding.GHL2025.boundaryRotationAngleNormalizerContract_coefficient

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

QuantumBlockEncoding.GHL2025.boundaryRotationNormalizedCoefficient

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

QuantumBlockEncoding.GHL2025.BoundaryRotationAngleNormalizerProofRoute

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

QuantumBlockEncoding.GHL2025.boundaryRotationAngleNormalizerProofRoute

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

QuantumBlockEncoding.GHL2025.boundaryRotationAngleNormalizerProofRoute_coefficient

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

QuantumBlockEncoding.GHL2025.boundaryRotationAngleNormalizerProofRoute_arccosArgument

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

QuantumBlockEncoding.GHL2025.boundaryRotationAngleNormalizerProofRoute_sharedND

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

QuantumBlockEncoding.GHL2025.boundaryRotationAngleNormalizerProofRoute_sourceBound

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

QuantumBlockEncoding.GHL2025.derivativeNormalizerNDSourceBound_sharedRoutes

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

QuantumBlockEncoding.GHL2025.robinGlobalSparseAmplitudeValue_sharedNormalizerRoutes

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

QuantumBlockEncoding.GHL2025.boundaryRotationMatrix

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

QuantumBlockEncoding.GHL2025.oneTermRobinGate_Ry_boundary

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

QuantumBlockEncoding.GHL2025.derivativeNormalizerNDSharedRoute_flags_false

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

QuantumBlockEncoding.GHL2025.derivativeNormalizerNDSharedRoute_sourceBoundAndFlags