Foundation lesson · do not skip this if you are new
A quantum algorithm is not given a NumPy array for free. Before discussing speedups, we must say how classical data, matrix entries, or a linear operator become quantum operations. State preparation, query oracles, and block encodings are three different access contracts.
Contract. Build a circuit P that creates the input quantum state you actually want to use.
Why it matters. Algorithms that start from amplitude-encoded data need this state before any later quantum subroutine can help. Preparation cost is therefore part of the end-to-end algorithm, not decorative preprocessing.
The Pauli-X and Hadamard cases show the smallest exact examples.
Contract. Ask a reversible black box for a matrix entry encoded in a work register.
Why it matters. Query-complexity theorems often count how many times the oracle is called, but a real fault-tolerant implementation must also build the arithmetic and memory circuit hidden inside that call.
The GHL Robin paper explicitly contrasts this model with its gate-level construction.
Contract. Embed a possibly non-unitary matrix A as the clean ancilla block of a larger unitary U_A.
Why it matters. Quantum hardware applies unitary gates. Block encoding is the interface that lets algorithms such as QSVT and Hamiltonian simulation manipulate a general structured matrix through a unitary circuit.
BE Case 1, the cubic diagonal family, and the Robin case all certify this contract.
How to read a quantum circuit
wireA horizontal wire is one qubit/register. Time flows from left to right.|0>A ket at the left fixes the input state of that wire.H, X, RYA box is a gate. Its matrix acts when the state reaches that box.controlA control dot means another gate acts only when the control condition is satisfied.daggerU† means the inverse/conjugate-transpose circuit; it often uncomputes temporary information.ancillaAn ancilla is workspace. A clean block-encoding proof normally requires selected ancillas to start and end in |0>.measurementMeasurement converts quantum amplitudes into classical outcomes; it is different from the coherent unitary part of the circuit.The H-plus-CNOT circuit above prepares the Bell state \((|00\rangle+|11\rangle)/\sqrt2\). The same visual grammar is used in the case studies; larger diagrams only add named registers and uncomputation.
“quantum state vectors are unit vectors with respect to the Euclidean norm.”Quantum circuitsIBM Quantum Learning / John Watrous
“The flow of information along the wires goes from left to right”Lecture Notes on Quantum Algorithms for Scientific ComputationLin Lin
“A more general input model, as will be discussed in this chapter, is called ‘block encoding’.”
New to quantum computing? Start here.
A classical program updates bits. In the circuit model used here, a quantum program applies reversible linear transformations to complex amplitude vectors and reads classical outcomes through measurement.
Textbook / teaching anchor
Standard textbook reference for quantum mechanics, qubits, gates, and the circuit model.
Textbook / teaching anchor
Circuit-first computer-science viewpoint on qubits and quantum information.
Textbook / teaching anchor
Beginner-friendly state-vector, measurement, multi-system, and circuit explanations.
Textbook / teaching anchor
Foundations, entanglement, circuits, algorithms, and error correction.
Guided reading
State Preparation and Block Encoding are the two currently compiled cores. Quantum Information and Representation Theory, and Quantum Algorithms for Scientific Computation, are source-audited peer parts with honest planned status. They reuse shared foundations instead of defining a second state, channel, circuit or block-encoding API.
Reading map
The graph makes State Preparation a reusable subproblem of the broader Block Encoding toolchain without identifying their certificate types. Reverse block-to-state consumption remains a separately typed path.
flowchart TB F["Shared foundations<br/>finite matrices, basis states, circuits"] F --> S1["State preparation"] S1 --> S2["State action and<br/>first-column certificates"] S2 --> S3["Prepared-state routes<br/>and reusable PREPARE components"] F --> B1["Block encoding"] B1 --> B2["Ancillas, register order,<br/>normalization and projection"] B2 --> B3["Composition, dilation,<br/>LCU and QSVT interfaces"] S3 -. "nested PREPARE layer + SELECT + unprepare" .-> B3 B3 -. "downstream consumer only: input + branch + normalization/amplification" .-> S3 S3 --> H["ASPBE search,<br/>verification and exports"] B3 --> H classDef shared fill:#f8f5ee,stroke:#826a32,color:#222222,stroke-width:1.5px; classDef state fill:#edf5f1,stroke:#2f7355,color:#18382b,stroke-width:1.5px; classDef block fill:#eef3f7,stroke:#49677d,color:#1f2e39,stroke-width:1.5px; classDef system fill:#ffffff,stroke:#64747a,color:#222222,stroke-width:1.25px; class F shared; class S1,S2,S3 state; class B1,B2,B3 block; class H system;
One book map · explicit proof status
Chapters 1–2 are shared foundations authored once and reused by Block Encoding; Chapters 3–4 specialize them to preparation certificates.
Block Encoding reuses the same finite-matrix and circuit nodes, then adds projected-block, composition, resource and proof-gated construction obligations.
Leditzky's representation-theoretic QIT notes organize one shared state/channel foundation followed by symmetry, Schur–Weyl and information-theoretic applications.
Lin–Wiebe's scientific-computing progression reuses Part II Block Encoding and adds transforms, simulation, estimation and application contracts.
Choose what to learn
Find a chapter, its reading source and the exact upstream memory assigned to it. Compiled means the listed local core, not a completed source book; Partial route and Planned keep their open boundaries.
23 chapter entries. All visible without JavaScript.
No matching chapter. Try a broader term or reset the filters.
Part I · State Preparation
Normalized targets, unitary candidates, first-column semantics and exact finite witnesses.
Efficient Quantum State Preparation with Walsh Series · Efficient Quantum Circuits for Non-Unitary and Unitary Diagonal Operators with Space-Time-Accuracy trade-offs
These are reading anchors, not a claim that every source theorem is formalized.
Part I · State Preparation
Walsh phase synthesis, controlled constant mode, interference, postselection, infidelity and successful-preparation cost.
Efficient Quantum State Preparation with Walsh Series · Efficient Quantum Circuits for Non-Unitary and Unitary Diagonal Operators with Space-Time-Accuracy trade-offs
These are reading anchors, not a claim that every source theorem is formalized.
OpenAI Math snapshot adc7f1241b42 · upstream Lean 4.34.1 · local migration target 4.33.0.
Source placement does not certify an adapter, the whole chapter, or an SP/BE construction.
InformationTheory/QuantumCircuit
Candidate circuit-model and resource adapter.
Upstream evidence: comparator-backed. adapter-backed. Not local admission.
Next boundary: A local semantic adapter and independent publication review are still required.
Part I · State Preparation
Apply a unitary or dilated non-unitary diagonal to a charged input, then account for normalization, success and finite precision.
Efficient Quantum State Preparation with Walsh Series · Efficient Quantum Circuits for Non-Unitary and Unitary Diagonal Operators with Space-Time-Accuracy trade-offs
These are reading anchors, not a claim that every source theorem is formalized.
Part II · Block Encoding
Clean-block extraction, LCU/product routes, sparse access, resource records and finite certified cases.
Efficient Quantum Circuits for Non-Unitary and Unitary Diagonal Operators with Space-Time-Accuracy trade-offs · Quantum Algorithms for Scientific Computation
These are reading anchors, not a claim that every source theorem is formalized.
Part II · Block Encoding
Separate phase operators from dilated filters and prove matched space–time–accuracy contracts, including cleanup and error-scale adapters.
Efficient Quantum Circuits for Non-Unitary and Unitary Diagonal Operators with Space-Time-Accuracy trade-offs · Quantum Algorithms for Scientific Computation
These are reading anchors, not a claim that every source theorem is formalized.
OpenAI Math snapshot adc7f1241b42 · upstream Lean 4.34.1 · local migration target 4.33.0.
Source placement does not certify an adapter, the whole chapter, or an SP/BE construction.
preprints/Polynomial-Time-Unitary-Synthesis-from-a-Boolean-Oracle-October-5-2026
oracle-assisted unitary synthesis frontier directly relevant to ASPBE synthesis semantics
Upstream evidence: manuscript-only-in-current-audit. benchmark-only. Not local admission.
Next boundary: compare target/operator/oracle/resource contract with the ASPBE synthesis API before formal route creation
Part II · Block Encoding
Connect exact Fourier circuit resources and structured operator descriptions to the shared circuit and block interfaces without treating either as an automatic block encoding.
Efficient Quantum Circuits for Non-Unitary and Unitary Diagonal Operators with Space-Time-Accuracy trade-offs · Quantum Algorithms for Scientific Computation
These are reading anchors, not a claim that every source theorem is formalized.
OpenAI Math snapshot adc7f1241b42 · upstream Lean 4.34.1 · local migration target 4.33.0.
Source placement does not certify an adapter, the whole chapter, or an SP/BE construction.
exact Fourier-circuit construction and resource theorem; supplier to Fourier/QPE chapters after circuit-model adaptation
Upstream evidence: comparator-backed. source-route. Not local admission.
Next boundary: compare circuit ordering, gate set and cost tuple with the local circuit/resource API; do not present the Fourier result as a block encoding or QPE certificate
Part III · Quantum Information and Representation Theory
Choose one canonical finite-dimensional state, positive-operator, Born-rule and POVM layer before importing downstream results.
Representation-theoretic methods in quantum information theory
These are reading anchors, not a claim that every source theorem is formalized.
OpenAI Math snapshot adc7f1241b42 · upstream Lean 4.34.1 · local migration target 4.33.0.
Source placement does not certify an adapter, the whole chapter, or an SP/BE construction.
InformationTheory/Entanglement
candidate foundational QIT spine; declaration-by-declaration admission only
Upstream evidence: lean-present-not-single-comparator-audited. adapter-backed. Not local admission.
Next boundary: A local semantic adapter and independent publication review are still required.
Part III · Quantum Information and Representation Theory
Freeze subsystem order and tensor conventions; purification and dilation remain non-unique representative constructions.
Representation-theoretic methods in quantum information theory
These are reading anchors, not a claim that every source theorem is formalized.
OpenAI Math snapshot adc7f1241b42 · upstream Lean 4.34.1 · local migration target 4.33.0.
Source placement does not certify an adapter, the whole chapter, or an SP/BE construction.
InformationTheory/Entanglement
candidate foundational QIT spine; declaration-by-declaration admission only
Upstream evidence: lean-present-not-single-comparator-audited. adapter-backed. Not local admission.
Next boundary: A local semantic adapter and independent publication review are still required.
Part III · Quantum Information and Representation Theory
Completely positive maps, Kraus/Choi representations, trace/fidelity conventions and contractivity become shared nodes.
Representation-theoretic methods in quantum information theory
These are reading anchors, not a claim that every source theorem is formalized.
OpenAI Math snapshot adc7f1241b42 · upstream Lean 4.34.1 · local migration target 4.33.0.
Source placement does not certify an adapter, the whole chapter, or an SP/BE construction.
InformationTheory/AmplitudeDamping
quantum channel, entropy, Holevo information, and operational capacity
Upstream evidence: comparator-backed. source-route. Not local admission.
Next boundary: A local semantic adapter and independent publication review are still required.
InformationTheory/Entanglement
candidate foundational QIT spine; declaration-by-declaration admission only
Upstream evidence: lean-present-not-single-comparator-audited. adapter-backed. Not local admission.
Next boundary: A local semantic adapter and independent publication review are still required.
CP/PPT/trace-preserving/entanglement-breaking channel geometry and an explicit PPT-square counterexample route
Upstream evidence: lean-present-not-comparator-audited. adapter-backed. Not local admission.
Next boundary: admit only after canonical CP, PPT, trace-preserving, Choi and entanglement-breaking adapters are fixed
Part III · Quantum Information and Representation Theory
Group actions, representations, characters, averaging and fixed spaces are admitted only after manuscript-specific namespaces are purified.
Representation-theoretic methods in quantum information theory
These are reading anchors, not a claim that every source theorem is formalized.
OpenAI Math snapshot adc7f1241b42 · upstream Lean 4.34.1 · local migration target 4.33.0.
Source placement does not certify an adapter, the whole chapter, or an SP/BE construction.
RepresentationTheory/Young · RepresentationTheory/YoungSymmetry · RepresentationTheory/FiniteUnitary
Young/Specht and finite-unitary representation ingredients relevant to Schur-Weyl prerequisites
Upstream evidence: lean-present-not-comparator-audited. adapter-backed. Not local admission.
Next boundary: purify manuscript-specific namespaces and assumptions, then admit only source-independent declarations with a real textbook consumer
Part III · Quantum Information and Representation Theory
Build the symmetric-group/unitary-group bridge needed by the quantum method of types; advanced Saxl and Foulkes–Howe results remain extensions, not prerequisites.
Representation-theoretic methods in quantum information theory
These are reading anchors, not a claim that every source theorem is formalized.
OpenAI Math snapshot adc7f1241b42 · upstream Lean 4.34.1 · local migration target 4.33.0.
Source placement does not certify an adapter, the whole chapter, or an SP/BE construction.
RepresentationTheory/Young · RepresentationTheory/YoungSymmetry · RepresentationTheory/FiniteUnitary
Young/Specht and finite-unitary representation ingredients relevant to Schur-Weyl prerequisites
Upstream evidence: lean-present-not-comparator-audited. adapter-backed. Not local admission.
Next boundary: purify manuscript-specific namespaces and assumptions, then admit only source-independent declarations with a real textbook consumer
advanced symmetric-group and Specht-module route, not a prerequisite for Schur-Weyl
Upstream evidence: comparator-backed. source-route. Not local admission.
Next boundary: A local semantic adapter and independent publication review are still required.
RepresentationTheory/FoulkesHowe
advanced plethysm/Foulkes-Howe route, not a prerequisite for quantum representation theory
Upstream evidence: comparator-backed. source-route. Not local admission.
Next boundary: A local semantic adapter and independent publication review are still required.
Part III · Quantum Information and Representation Theory
Consume the shared QIT and representation layers without turning conceptual symmetry correspondences into Lean dependencies.
Representation-theoretic methods in quantum information theory
These are reading anchors, not a claim that every source theorem is formalized.
Part III · Quantum Information and Representation Theory
Amplitude-damping capacity, entangled games and dimension-ten zero-key constructions are source routes above canonical state/channel adapters.
Representation-theoretic methods in quantum information theory
These are reading anchors, not a claim that every source theorem is formalized.
OpenAI Math snapshot adc7f1241b42 · upstream Lean 4.34.1 · local migration target 4.33.0.
Source placement does not certify an adapter, the whole chapter, or an SP/BE construction.
InformationTheory/AmplitudeDamping
quantum channel, entropy, Holevo information, and operational capacity
Upstream evidence: comparator-backed. source-route. Not local admission.
Next boundary: A local semantic adapter and independent publication review are still required.
finite-dimensional entangled-game, measurement, purification and repeated-game information route
Upstream evidence: comparator-backed. adapter-backed. Not local admission.
Next boundary: reuse only after state/measurement/trace-distance adapters are canonical
advanced QIT / private-key route after foundation adapters
Upstream evidence: lean-present-not-comparator-audited. source-route. Not local admission.
Next boundary: A local semantic adapter and independent publication review are still required.
InformationTheory/DimensionTen
companion density-state, entanglement, Choi-transfer and finite readout/key construction above the DimensionTen and SecretKey layers
Upstream evidence: lean-present-not-comparator-audited. source-route. Not local admission.
Next boundary: keep this as a downstream consumer; do not promote its local density or separability wrappers as the shared QIT foundation
classical information-theory candidate substrate, not quantum-labelled by default
Upstream evidence: comparator-backed. canonical-leaf. Not local admission.
Next boundary: A local semantic adapter and independent publication review are still required.
Part III · Quantum Information and Representation Theory
Photon-number entropy, PPT-square phenomena and explicit channel geometry are advanced consumers, not foundational definitions.
Representation-theoretic methods in quantum information theory
These are reading anchors, not a claim that every source theorem is formalized.
OpenAI Math snapshot adc7f1241b42 · upstream Lean 4.34.1 · local migration target 4.33.0.
Source placement does not certify an adapter, the whole chapter, or an SP/BE construction.
InformationTheory/PhotonNumber
quantum optics and entropy photon-number route
Upstream evidence: comparator-backed. source-route. Not local admission.
Next boundary: A local semantic adapter and independent publication review are still required.
CP/PPT/trace-preserving/entanglement-breaking channel geometry and an explicit PPT-square counterexample route
Upstream evidence: lean-present-not-comparator-audited. adapter-backed. Not local admission.
Next boundary: admit only after canonical CP, PPT, trace-preserving, Choi and entanglement-breaking adapters are fixed
quantum-channel existence and geometry route
Upstream evidence: comparator-backed. source-route. Not local admission.
Next boundary: A local semantic adapter and independent publication review are still required.
Part IV · Quantum Algorithms for Scientific Computation
Share QIT states/channels/distances and make query construction, precision and readout costs explicit.
Quantum Algorithms for Scientific Computation
These are reading anchors, not a claim that every source theorem is formalized.
OpenAI Math snapshot adc7f1241b42 · upstream Lean 4.34.1 · local migration target 4.33.0.
Source placement does not certify an adapter, the whole chapter, or an SP/BE construction.
InformationTheory/Entanglement
candidate foundational QIT spine; declaration-by-declaration admission only
Upstream evidence: lean-present-not-single-comparator-audited. adapter-backed. Not local admission.
Next boundary: A local semantic adapter and independent publication review are still required.
preprints/A-Nearly-Quartic-Separation-Between-Randomized-and-Quantum-Query-Complexity-October-5-2026
quantum query-complexity frontier
Upstream evidence: manuscript-only-in-current-audit. benchmark-only. Not local admission.
Next boundary: locate exact formalization/comparator mapping before any Lean-status claim; then connect to query/oracle complexity graph
Part IV · Quantum Algorithms for Scientific Computation
Point back to Part II and add adapters only where the source notation or error convention differs.
Quantum Algorithms for Scientific Computation
These are reading anchors, not a claim that every source theorem is formalized.
Part IV · Quantum Algorithms for Scientific Computation
Separate polynomial/signal-transform correctness from phase synthesis and finite-gate compilation.
Quantum Algorithms for Scientific Computation
These are reading anchors, not a claim that every source theorem is formalized.
Part IV · Quantum Algorithms for Scientific Computation
Compose access, block/qubitization suppliers, approximation and successful execution under one resource tier.
Quantum Algorithms for Scientific Computation
These are reading anchors, not a claim that every source theorem is formalized.
Part IV · Quantum Algorithms for Scientific Computation
Use the Comparator-backed exact Fourier route as an external resource theorem after circuit-model adaptation; it does not itself certify QPE.
Quantum Algorithms for Scientific Computation
These are reading anchors, not a claim that every source theorem is formalized.
OpenAI Math snapshot adc7f1241b42 · upstream Lean 4.34.1 · local migration target 4.33.0.
Source placement does not certify an adapter, the whole chapter, or an SP/BE construction.
exact Fourier-circuit construction and resource theorem; supplier to Fourier/QPE chapters after circuit-model adaptation
Upstream evidence: comparator-backed. source-route. Not local admission.
Next boundary: compare circuit ordering, gate set and cost tuple with the local circuit/resource API; do not present the Fourier result as a block encoding or QPE certificate
Part IV · Quantum Algorithms for Scientific Computation
Charge trial-state preparation, overlap, gap, precision, amplification and final classical output.
Quantum Algorithms for Scientific Computation
These are reading anchors, not a claim that every source theorem is formalized.
Part IV · Quantum Algorithms for Scientific Computation
Reuse block/channel nodes and expose input, condition-number, success and readout assumptions rather than hiding them in an oracle.
Quantum Algorithms for Scientific Computation
These are reading anchors, not a claim that every source theorem is formalized.
OpenAI Math snapshot adc7f1241b42 · upstream Lean 4.34.1 · local migration target 4.33.0.
Source placement does not certify an adapter, the whole chapter, or an SP/BE construction.
InformationTheory/AmplitudeDamping
quantum channel, entropy, Holevo information, and operational capacity
Upstream evidence: comparator-backed. source-route. Not local admission.
Next boundary: A local semantic adapter and independent publication review are still required.
Part IV · Quantum Algorithms for Scientific Computation
Exact factoring, shallow-circuit parity and oracle-assisted unitary synthesis extend the computing curriculum without counting as SP/BE successes.
Quantum Algorithms for Scientific Computation
These are reading anchors, not a claim that every source theorem is formalized.
OpenAI Math snapshot adc7f1241b42 · upstream Lean 4.34.1 · local migration target 4.33.0.
Source placement does not certify an adapter, the whole chapter, or an SP/BE construction.
InformationTheory/QuantumCircuit
Candidate circuit-model and resource adapter.
Upstream evidence: comparator-backed. adapter-backed. Not local admission.
Next boundary: A local semantic adapter and independent publication review are still required.
Computability/QuantumFactoring
full quantum algorithm/circuit/compiler route with arithmetic, oracle and resource semantics
Upstream evidence: comparator-backed. source-route. Not local admission.
Next boundary: mine circuit/compiler/resource primitives that can share with ASPBE before exposing the factoring endpoint
preprints/Polynomial-Time-Unitary-Synthesis-from-a-Boolean-Oracle-October-5-2026
oracle-assisted unitary synthesis frontier directly relevant to ASPBE synthesis semantics
Upstream evidence: manuscript-only-in-current-audit. benchmark-only. Not local admission.
Next boundary: compare target/operator/oracle/resource contract with the ASPBE synthesis API before formal route creation
Part IV · Quantum Algorithms for Scientific Computation
The Comparator-backed Laughlin route is a model-side spectral target and reusable mathematical substrate, not evidence of a quantum algorithm or simulator.
Quantum Algorithms for Scientific Computation
These are reading anchors, not a claim that every source theorem is formalized.
OpenAI Math snapshot adc7f1241b42 · upstream Lean 4.34.1 · local migration target 4.33.0.
Source placement does not certify an adapter, the whole chapter, or an SP/BE construction.
many-body model-side mathematical target; not a quantum-algorithm or simulator certificate
Upstream evidence: comparator-backed. source-route. Not local admission.
Next boundary: A local semantic adapter and independent publication review are still required.
One navigation level · distinct proof status
This catalog is a textbook placement map. A listed source, upstream Lean cluster, or extended chapter is not a local ASPBE theorem unless an exact compiled declaration is linked separately.
flowchart TB
accTitle: QuantumComputinglib textbooks and shared Lean foundations
accDescr: External Lean references enter shared foundations only through reviewed reuse or narrow adapters. The textbooks reuse these foundations. State Preparation and Block Encoding are the current core; Quantum Information and Scientific Computing are planned extensions. Conditional algorithm and theory support lead into Scientific Computing. These are curriculum relationships, not Lean theorem implications.
EXT["External Lean references<br/>Mathlib · attributed quantum Lean libraries<br/>upstream references, not automatic local proofs"]
CORE["Shared Lean foundations<br/>Reviewed building blocks reused across textbooks<br/>linear algebra · states/tensors · operators<br/>circuits/registers · norms · resource interfaces"]
subgraph TEXTBOOK["QuantumComputinglib textbooks"]
direction TB
subgraph CURRENT["Current core · compiled guided chapters"]
direction LR
SP["Part I · State Preparation<br/>U|0^n⟩ = |ψ⟩"]
BE["Part II · Block Encoding<br/>‖A - αΠUΠ†‖ ≤ ε"]
end
subgraph PLANNED["Planned extensions · local chapter admission required"]
direction TB
QIT["Planned Part III · Quantum Information<br/>and Representation Theory<br/>symmetry · Schur–Weyl · de Finetti"]
SCI["Planned Part IV · Quantum Scientific Computing<br/>QSP/QSVT · simulation · estimation<br/>linear systems · dynamics · open systems"]
end
end
EXT -. "reviewed reuse / narrow adapters" .-> CORE
CORE -->|common foundation| TEXTBOOK
BE -. "algorithm support" .-> SCI
QIT -. "theoretical support" .-> SCI
classDef core fill:#f8f5ee,stroke:#826a32,color:#222222,stroke-width:1.5px;
classDef state fill:#edf5f1,stroke:#2f7355,color:#18382b,stroke-width:1.5px;
classDef block fill:#eef3f7,stroke:#49677d,color:#1f2e39,stroke-width:1.5px;
classDef future fill:#f7f4fb,stroke:#735a8f,color:#2f2440,stroke-width:1.5px;
classDef external fill:#ffffff,stroke:#64747a,color:#222222,stroke-width:1.25px;
class CORE core;
class SP state;
class BE block;
class QIT,SCI future;
class EXT external;
Part I · Partial route
The compiled preparation contract and finite examples are joined by source-audited routes for structured, scalable state loading.
Part II · Partial route
The compiled clean-block API and construction rules are extended by source-faithful diagonal, compiler and resource routes.
Part III · Planned
Leditzky's representation-theoretic QIT notes organize one shared state/channel foundation followed by symmetry, Schur–Weyl and information-theoretic applications.
Part IV · Planned
Lin–Wiebe's scientific-computing progression reuses Part II Block Encoding and adds transforms, simulation, estimation and application contracts.