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

Formal status. Compiled by the full ASPBE gate in a research-level module. The displayed theorem is checked, but it does not promote a broader paper route or an external oracle contract.

Why it is in this chapter. Compiled Robin-matrix research included in the full ASPBE gate; local results are separated from the broader paper route and external contracts.

Technical source note. Coefficient at column 'colIdx' when the stencil 'entries' is applied at row 'rowIdx'. Only entries whose offset lands on 'colIdx' contribute; the result is the sum of all matching coefficients. Returns bare 'Coeff' (no zero-wrapping) when exactly one entry matches.

Declaration kind. def.

Source: QuantumBlockEncoding/RobinMatrix.lean:21. A commit-pinned external link is added by the publication build when the source exists at the published ref.

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

Formal status. Compiled by the full ASPBE gate in a research-level module. The displayed theorem is checked, but it does not promote a broader paper route or an external oracle contract.

Why it is in this chapter. Compiled Robin-matrix research included in the full ASPBE gate; local results are separated from the broader paper route and external contracts.

Technical source note. Select the stencil entry list for row 'i': - rows 'i < w.lower' use left boundary rows, - rows 'i > w.upper' use right boundary rows, - all others use the bulk stencil. Falls back to the empty list if a boundary row is missing from the supplied data, so the definition is total and does not need index proofs.

Declaration kind. def.

Source: QuantumBlockEncoding/RobinMatrix.lean:37. A commit-pinned external link is added by the publication build when the source exists at the published ref.

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

Formal status. Compiled by the full ASPBE gate in a research-level module. The displayed theorem is checked, but it does not promote a broader paper route or an external oracle contract.

Why it is in this chapter. Compiled Robin-matrix research included in the full ASPBE gate; local results are separated from the broader paper route and external contracts.

Technical source note. Build the full Robin derivative matrix of size 'gridSize n × gridSize n'. The boundary rows come from 'leftRows' and 'rightRows'; the interior uses 'bulkEntries'. The 'BulkWindow w' records where the interior starts and ends.

Declaration kind. def.

Source: QuantumBlockEncoding/RobinMatrix.lean:56. A commit-pinned external link is added by the publication build when the source exists at the published ref.

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

Formal status. Compiled by the full ASPBE gate in a research-level module. The displayed theorem is checked, but it does not promote a broader paper route or an external oracle contract.

Why it is in this chapter. Compiled Robin-matrix research included in the full ASPBE gate; local results are separated from the broader paper route and external contracts.

Technical source note. The concrete Robin derivative matrix for the fourth-order central second-derivative stencil.

Declaration kind. def.

Source: QuantumBlockEncoding/RobinMatrix.lean:68. A commit-pinned external link is added by the publication build when the source exists at the published ref.

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

Formal status. Compiled by the full ASPBE gate in a research-level module. The displayed theorem is checked, but it does not promote a broader paper route or an external oracle contract.

Why it is in this chapter. Compiled Robin-matrix research included in the full ASPBE gate; local results are separated from the broader paper route and external contracts.

Technical source note. The one-term Robin theorem target $A_k$. Theorem '1 term robin' block-encodes the row-scaled operator 'A_k ~ f(x) d^m/dx^m'; Eq. 'ROBIN clarified' carries entries 'f(x_i) D_{ij}' in the 'gamma3' branch.

Declaration kind. def.

Source: QuantumBlockEncoding/RobinMatrix.lean:81. A commit-pinned external link is added by the publication build when the source exists at the published ref.

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

Formal status. Compiled by the full ASPBE gate in a research-level module. The displayed theorem is checked, but it does not promote a broader paper route or an external oracle contract.

Why it is in this chapter. Compiled Robin-matrix research included in the full ASPBE gate; local results are separated from the broader paper route and external contracts.

Technical source note. Absolute-row-sum for row 'i' of a 'Coeff'-valued matrix, given a symbol environment 'env'. This is the building block for the induced 1-norm.

Declaration kind. def.

Source: QuantumBlockEncoding/RobinMatrix.lean:96. A commit-pinned external link is added by the publication build when the source exists at the published ref.

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

Formal status. Compiled by the full ASPBE gate in a research-level module. The displayed theorem is checked, but it does not promote a broader paper route or an external oracle contract.

Why it is in this chapter. Compiled Robin-matrix research included in the full ASPBE gate; local results are separated from the broader paper route and external contracts.

Technical source note. Induced matrix 1-norm: the maximum absolute row sum. Uses 'evalWith env' to convert symbolic 'Coeff' entries to concrete 'Rat' values.

Declaration kind. def.

Source: QuantumBlockEncoding/RobinMatrix.lean:106. A commit-pinned external link is added by the publication build when the source exists at the published ref.

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

Formal status. Compiled by the full ASPBE gate in a research-level module. The displayed theorem is checked, but it does not promote a broader paper route or an external oracle contract.

Why it is in this chapter. Compiled Robin-matrix research included in the full ASPBE gate; local results are separated from the broader paper route and external contracts.

Technical source note. Numeric 1-norm of the Robin derivative matrix under a symbol environment. Returns the maximum absolute row sum as a concrete 'Rat'.

Declaration kind. def.

Source: QuantumBlockEncoding/RobinMatrix.lean:117. A commit-pinned external link is added by the publication build when the source exists at the published ref.

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

Formal status. Compiled by the full ASPBE gate in a research-level module. The displayed theorem is checked, but it does not promote a broader paper route or an external oracle contract.

Why it is in this chapter. Compiled Robin-matrix research included in the full ASPBE gate; local results are separated from the broader paper route and external contracts.

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

Declaration kind. def.

Source: QuantumBlockEncoding/RobinMatrix.lean:125. A commit-pinned external link is added by the publication build when the source exists at the published ref.

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

Formal status. Compiled by the full ASPBE gate in a research-level module. The displayed theorem is checked, but it does not promote a broader paper route or an external oracle contract.

Why it is in this chapter. Compiled Robin-matrix research included in the full ASPBE gate; local results are separated from the broader paper route and external contracts.

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

Declaration kind. def.

Source: QuantumBlockEncoding/RobinMatrix.lean:133. A commit-pinned external link is added by the publication build when the source exists at the published ref.

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

Formal status. Compiled by the full ASPBE gate in a research-level module. The displayed theorem is checked, but it does not promote a broader paper route or an external oracle contract.

Why it is in this chapter. Compiled Robin-matrix research included in the full ASPBE gate; local results are separated from the broader paper route and external contracts.

Technical source note. Concrete BlockEncodingSpec wiring the Robin derivative matrix into the one-term Robin block encoding framework. Uses the fourth-order central stencil with Robin boundary corrections.

Declaration kind. def.

Source: QuantumBlockEncoding/RobinMatrix.lean:149. A commit-pinned external link is added by the publication build when the source exists at the published ref.

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

Formal status. Compiled by the full ASPBE gate in a research-level module. The displayed theorem is checked, but it does not promote a broader paper route or an external oracle contract.

Why it is in this chapter. Compiled Robin-matrix research included in the full ASPBE gate; local results are separated from the broader paper route and external contracts.

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

Declaration kind. def.

Source: QuantumBlockEncoding/RobinMatrix.lean:163. A commit-pinned external link is added by the publication build when the source exists at the published ref.

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

Formal status. Compiled by the full ASPBE gate in a research-level module. The displayed theorem is checked, but it does not promote a broader paper route or an external oracle contract.

Why it is in this chapter. Compiled Robin-matrix research included in the full ASPBE gate; local results are separated from the broader paper route and external contracts.

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

Declaration kind. def.

Source: QuantumBlockEncoding/RobinMatrix.lean:181. A commit-pinned external link is added by the publication build when the source exists at the published ref.

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

Formal status. Compiled by the full ASPBE gate in a research-level module. The displayed theorem is checked, but it does not promote a broader paper route or an external oracle contract.

Why it is in this chapter. Compiled Robin-matrix research included in the full ASPBE gate; local results are separated from the broader paper route and external contracts.

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

Declaration kind. def.

Source: QuantumBlockEncoding/RobinMatrix.lean:188. A commit-pinned external link is added by the publication build when the source exists at the published ref.

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

Formal status. Compiled by the full ASPBE gate in a research-level module. The displayed theorem is checked, but it does not promote a broader paper route or an external oracle contract.

Why it is in this chapter. Compiled Robin-matrix research included in the full ASPBE gate; local results are separated from the broader paper route and external contracts.

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

Declaration kind. def.

Source: QuantumBlockEncoding/RobinMatrix.lean:195. A commit-pinned external link is added by the publication build when the source exists at the published ref.

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

Formal status. Compiled by the full ASPBE gate in a research-level module. The displayed theorem is checked, but it does not promote a broader paper route or an external oracle contract.

Why it is in this chapter. Compiled Robin-matrix research included in the full ASPBE gate; local results are separated from the broader paper route and external contracts.

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

Declaration kind. structure.

Source: QuantumBlockEncoding/RobinMatrix.lean:204. A commit-pinned external link is added by the publication build when the source exists at the published ref.

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

Formal status. Compiled by the full ASPBE gate in a research-level module. The displayed theorem is checked, but it does not promote a broader paper route or an external oracle contract.

Why it is in this chapter. Compiled Robin-matrix research included in the full ASPBE gate; local results are separated from the broader paper route and external contracts.

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

Declaration kind. def.

Source: QuantumBlockEncoding/RobinMatrix.lean:215. A commit-pinned external link is added by the publication build when the source exists at the published ref.

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

Formal status. Compiled by the full ASPBE gate in a research-level module. The displayed theorem is checked, but it does not promote a broader paper route or an external oracle contract.

Why it is in this chapter. Compiled Robin-matrix research included in the full ASPBE gate; local results are separated from the broader paper route and external contracts.

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

Declaration kind. def.

Source: QuantumBlockEncoding/RobinMatrix.lean:242. A commit-pinned external link is added by the publication build when the source exists at the published ref.

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

Formal status. Compiled by the full ASPBE gate in a research-level module. The displayed theorem is checked, but it does not promote a broader paper route or an external oracle contract.

Why it is in this chapter. Compiled Robin-matrix research included in the full ASPBE gate; local results are separated from the broader paper route and external contracts.

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

Declaration kind. def.

Source: QuantumBlockEncoding/RobinMatrix.lean:252. A commit-pinned external link is added by the publication build when the source exists at the published ref.

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

Formal status. Compiled by the full ASPBE gate in a research-level module. The displayed theorem is checked, but it does not promote a broader paper route or an external oracle contract.

Why it is in this chapter. Compiled Robin-matrix research included in the full ASPBE gate; local results are separated from the broader paper route and external contracts.

Technical source note. Block-extraction target for the one-term Robin block encoding. States that the '(0, 0)' block of the circuit matrix should equal 'A_k / (N_D * N_f * kappa)'. The 'unitaryMatrix' and 'blockMatrix' are derived from the real circuit matrix product computed by 'evalGateMatrices' over all 7 honest gate matrices. Block correctness remains unproved. The 'signalDim' is 'qubitDim effectiveRobinSignalQubits' where 'effectiveRobinSignalQubits' counts all non-system qubits. 'systemDim' is 'gridSize n'. figure:1_term_ROBIN, main.tex:1131-1136 -

Declaration kind. def.

Source: QuantumBlockEncoding/RobinMatrix.lean:296. A commit-pinned external link is added by the publication build when the source exists at the published ref.

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

Formal status. Compiled by the full ASPBE gate in a research-level module. The displayed theorem is checked, but it does not promote a broader paper route or an external oracle contract.

Why it is in this chapter. Compiled Robin-matrix research included in the full ASPBE gate; local results are separated from the broader paper route and external contracts.

Technical source note. Circuit block encoding claim for the one-term Robin construction. Connects the circuit matrix semantics to the block extraction target and records the dimension compatibility as a parameter. The caller must supply 'hDim' proving that the total circuit Hilbert space decomposes as signalDim × systemDim. For concrete 'n' (e.g. n = 3) this is provable by 'native_decide'. figure:1_term_ROBIN, main.tex:1131-1136 -

Declaration kind. def.

Source: QuantumBlockEncoding/RobinMatrix.lean:323. A commit-pinned external link is added by the publication build when the source exists at the published ref.

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

Formal status. Compiled by the full ASPBE gate in a research-level module. The displayed theorem is checked, but it does not promote a broader paper route or an external oracle contract.

Why it is in this chapter. Compiled Robin-matrix research included in the full ASPBE gate; local results are separated from the broader paper route and external contracts.

Technical source note. Default one-term Robin circuit block claim using the reusable dimension compatibility theorem. The block-correctness obligation remains unproved.

Declaration kind. def.

Source: QuantumBlockEncoding/RobinMatrix.lean:344. A commit-pinned external link is added by the publication build when the source exists at the published ref.

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

Formal status. Compiled by the full ASPBE gate in a research-level module. The displayed theorem is checked, but it does not promote a broader paper route or an external oracle contract.

Why it is in this chapter. Compiled Robin-matrix research included in the full ASPBE gate; local results are separated from the broader paper route and external contracts.

Technical source note. Contract-only finite-dimensional LCU/block-composition dependency for the one-term Robin theorem. This records the exact circuit claim, target matrix, normalizer, and open matrix obligations that a future finite-dimensional composition theorem must close. It does not promote the current LCU, projection, or extraction flags.

Declaration kind. def.

Source: QuantumBlockEncoding/RobinMatrix.lean:359. A commit-pinned external link is added by the publication build when the source exists at the published ref.

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

Formal status. Compiled by the full ASPBE gate in a research-level module. The displayed theorem is checked, but it does not promote a broader paper route or an external oracle contract.

Why it is in this chapter. Compiled Robin-matrix research included in the full ASPBE gate; local results are separated from the broader paper route and external contracts.

Technical source note. Contract-only interface for the exact finite composition theorem still needed to close the GHL2025 one-term Robin block encoding. This names the missing theorem-facing step without asserting it: the seven-gate matrix product, projected in the Definition 'def:block-encoding' signal-zero convention, must realize the Eq. 'ROBIN clarified' target block 'oneTermRobinAkMatrix n / (N_D N_f kappa)'. The proof flag stays false until that exact finite-dimensional theorem is build-tested.

Declaration kind. def.

Source: QuantumBlockEncoding/RobinMatrix.lean:441. A commit-pinned external link is added by the publication build when the source exists at the published ref.

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

Formal status. Compiled by the full ASPBE gate in a research-level module. The displayed theorem is checked, but it does not promote a broader paper route or an external oracle contract.

Why it is in this chapter. Compiled Robin-matrix research included in the full ASPBE gate; local results are separated from the broader paper route and external contracts.

Technical source note. Phase 1 proof-route contract for the GHL2025 one-term Robin theorem. This record ties the theorem tuple, circuit-matrix semantics, block-projection target, active oracle contracts, and source-route blockers into one Lean object. It is a transcript and obligation map, not a proof that the block encoding is correct.

Declaration kind. structure.

Source: QuantumBlockEncoding/RobinMatrix.lean:467. A commit-pinned external link is added by the publication build when the source exists at the published ref.

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

Formal status. Compiled by the full ASPBE gate in a research-level module. The displayed theorem is checked, but it does not promote a broader paper route or an external oracle contract.

Why it is in this chapter. Compiled Robin-matrix research included in the full ASPBE gate; local results are separated from the broader paper route and external contracts.

Technical source note. Default theorem-level proof route for the one-term Robin block encoding. All unproved semantic obligations are deliberately kept false. The route uses the active seven-gate circuit product, the global-slot 'O_D^BS' cleanup-scope decision, and the external-source transcript for 'O_f'.

Declaration kind. def.

Source: QuantumBlockEncoding/RobinMatrix.lean:531. A commit-pinned external link is added by the publication build when the source exists at the published ref.