How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Computational Problems, Promises, and Cost Models — Examples
1 · Prerequisites
- Absolute and Conditional Convergence; Rearrangement; Products
- Algebraic Closure, Embeddings, and Separability
- Algebraic Extensions, Extension Degree, and Finite Fields
- Binary Operations, Monoids, Groups and Subgroups
- Boolean Circuits and Nonuniform Complexity
- Bounded Linear Operators and Quotient Spaces
- Circuit Syntax, Denotational Semantics, and Measurement
- Clifford+T Exact and Approximate Synthesis
- Compactness in Metric Spaces
- Completeness, Completion, and Uniform Continuity
- Complex Norms and Realification
- Complexification, Realification and Real Structures
- Composition Series, the Jordan–Hölder Theorem and Solvable Groups
- Computational Problems, Promises, and Cost Models
- Congruences, the Integers Modulo n and the Chinese Remainder Theorem
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Continuity, IVT, EVT, and Uniform Continuity
- Continuous-Gate Universality and Exact Synthesis
- Controlled Gates, Phase, and Entanglement
- Cosets, Index and Lagrange's Theorem
- Countability and Uncountability
- Cyclic Groups and Direct Products
- Determinants of Matrices over a Commutative Ring
- Diagonalisation and the Minimal Polynomial
- Divisibility, Euclidean Domains, Principal Ideal Domains and Unique Factorisation
- Divisibility, Greatest Common Divisors and Bézout's Identity
- Dual Spaces, Bilinear and Quadratic Forms, and Sylvester's Law of Inertia
- Effective Numberings, Reductions, Resources, and Randomness
- Eigenvalues, Eigenvectors and the Characteristic Polynomial
- Filters and Ultrafilters
- Finite Counting, Factorials and Binomial Coefficients
- Finite Dimensional Normed Spaces and Riesz Lemma
- Finite Probability Spaces and Random Variables
- Finite-Dimensional Complex Inner-Product Spaces and Matrix Interfaces
- Formal Languages, Encodings, and Decision Problems
- Foundations of the Real Numbers for Analysis
- Free Modules, Exact Sequences, Projective and Injective Modules
- Fundamental Trigonometric Identities
- Group Actions, Orbits, Stabilisers and Cayley's Theorem
- Group Homomorphisms and the Isomorphism Theorems
- Hilbert Space Geometry and Riesz Representation
- Ideals, Quotient Rings and the Isomorphism Theorems for Rings
- Inner Product Spaces, Gram-Schmidt, Projections and Adjoints
- Limits of Real Functions
- limsup, liminf, and Subsequential Limits
- Linear Independence, Bases and Dimension
- Linear Recurrences and Rational Generating Functions
- Linear Transformations, Rank-Nullity and Quotient Spaces
- Matrices, the Matrix of a Linear Map, and Change of Basis
- Measurements, POVMs, and Instruments
- Metric Spaces
- Modules, Submodules, Quotient Modules and the Isomorphism Theorems
- Monotone Functions, Discontinuities, and Continuity Sets
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Normal Subgroups and Quotient Groups
- Normed and Banach Spaces
- Order, Zorn's Lemma, and the Axiom of Choice
- Polynomial Rings, the Division Algorithm and Roots
- Power Series and Real-Analytic Functions
- Primes, Euclid's Lemma and the Fundamental Theorem of Arithmetic
- Properties of the Integral and the Working FTC
- Pure and Mixed States, Ensembles, and Schmidt Decomposition
- Qubits, Bloch Sphere, Pauli Algebra, and One-Qubit Gates
- Registers, Tensor Products, and Partial Trace
- Relations, Functions, and Quotients
- Resource Bounds and Machine Invariance
- Reversible Computation, Ancillas, and Coherent Oracles
- Rings, Subrings, Integral Domains and Fields
- Rⁿ as a Normed Space; Vector-Valued Functions
- Roots, Rational Powers, and Classical Inequalities
- Sequences and Limits
- Sequences and Series of Functions; Uniform Convergence
- Series: Convergence and the Nonnegative Tests
- Simple Field Extensions and the Construction of the Complex Numbers
- Sine, Cosine, and the Definition of Pi
- Splitting Fields
- Strongly Continuous Semigroups and Hille Yosida
- Suprema and Infima
- Sylow's Theorems, p-Groups and Nilpotent Groups
- Symmetric Groups, Cycle Decomposition and the Sign Homomorphism
- Tensor Products of Modules
- The Complex Exponential and Euler's Formula
- The Derivative and the Mean Value Theorems
- The Determinant of a Linear Operator, Cofactors and Cramer's Rule
- The Exponential Function
- The Fundamental Theorem of Algebra
- The Fundamental Theorem of Finite Abelian Groups
- The Galois Correspondence
- The Polynomial Hierarchy and Relativization
- The Riemann Integral: Definition and Integrability
- The Spectral Theorem, Positive Operators and Singular Value Decomposition
- The ZFC Axioms and the Basic Set Constructions
- Topology of ℝ
- Triangularisation, Generalised Eigenspaces and Jordan Canonical Form
- Turing Machines, Configurations, and Computation
- Uniform Circuit Families, Promise Problems, and Complexity
- Vector Spaces, Linear Subspaces, Span and Direct Sums
2 · Summary
This companion gives finite decision and search promises, a promise-preserving map with an explicit witness lift, and a total two-address oracle returning two-bit values. Its resource table separates oracle calls, nonoracle gates, measurement/readout, and classical bit work.
3 · Logical flowchart
4 · Definitions, theorems and proofs
None yet.
5 · Examples, counterexamples and false statements
Promise, query and cost-model examples
Example
Decision reduction. Let the source decision task have and , and let the target task have and . Define the total map by concatenating with itself. Inputs outside either one-bit source promise have no correctness obligation.
Search reduction. Let the source search domain be with relation iff and . Let the target domain be with relation iff and . Define the total instance map and the total witness map .
A total two-bit-output query instance. Write every four-bit instance as , where . Define
This is a total function on both addresses for every . Give it the decision promise and . Instances with or are off-promise.
Use the exact one-query procedure that starts with address and target , calls once, measures the two-bit target in the computational basis, and answers yes exactly when the result is . Compare it with the same procedure preceded by two Hadamard gates on the first target bit. Resource counts for these circuits use the declared QC gate, query, measurement, and classical-readout coordinates.
| Procedure | Oracle queries | Nonoracle quantum gates | Extra clean ancillas | Measurement/readout | Classical bit work |
|---|---|---|---|---|---|
| Decision reduction | 0 | not applicable | not applicable | not applicable | $O( |
| One-query circuit | 1 | 0 | 0 | One computational-basis measurement of the two-bit target; two bits read out | transitions to compare the measured value with and write one output bit |
| Same query with then on target bit 0 | 1 | 2 | 0 | One computational-basis measurement of the two-bit target; two bits read out | transitions to compare the measured value with and write one output bit |
The two query circuits both perform one oracle call even though the reply has two bits. Their gate counts differ while their query count and output law agree.
Facts & Assumptions
Given: The two decision/search task pairs, the maps , and the four-bit query family defined in the Example.
QA task and promise domain: decision tasks require the stated yes/no output only on the disjoint promise pair; search tasks require a witness in the stated relation only on their domain.
Promise query instance and oracle family: each promised instance selects a total function on every address, and one call to its coherent XOR oracle is one query, independent of output width.
Quantum query algorithm: a query circuit applies the specified XOR-oracle calls to its address and target registers.
Exact correctness for promise tasks: exact correctness means the required decision or witness event has probability one on each promised input.
Quantum query complexity: query cost counts designated oracle calls over promised inputs and branches.
Nonoracle quantum gate cost: nonoracle elementary gates are counted separately from black-box oracle calls.
Classical bit-operation cost: address/reply processing and output writing count as Turing transitions, separate from the oracle invocation.
Promise preserving reduction: a total polynomial-time map is a decision promise reduction when it maps source yes-instances to target yes-instances and source no-instances to target no-instances.
Clifford+T gate library and exact matrices: the exact Hadamard matrix is .
Normalized output law for finite quantum query branches: terminal computational-basis weights are finite sums of density-operator diagonal weights over unobserved wires, and the finite branch law is normalized.
Rectangular matrix multiplication and the identity matrix , including zero-sized shapes: matrix products are computed by finite row-by-column sums and the identity matrix acts as the multiplicative identity.
Finite registers and their ordered computational bases and The computational basis is orthonormal give the orthonormal computational basis of each factor. Equip their ordered tensor product with the product inner product of Ordered tensor registers, their inner product, and wire permutations; then The product basis is orthonormal and tensor dimensions multiply makes the bit-string product basis orthonormal.
Dirac Notation Conversion: for the root pairing, linear in its first argument, .
A unit-vector outer product is a density operator: the rank-one projector of a unit vector is a density operator.
Verification
A multitape machine computes by copying twice, using transitions under [F7], so is total and polynomial time. Moreover, and , giving and . Thus is a promise-preserving reduction by [F8]. No image condition is needed for source strings outside .
For the search reduction, the only promised source input is , and . Every valid target witness is , so is either or and satisfies . Both maps are total as defined on all binary strings, even though witness validity is required only on the promise.
For every four-bit , the table assigns one two-bit value to address 0 and one to address 1, so is total on its two-address domain. Starting at target , the oracle call at address 0 returns ; it is one invocation and therefore one query by [F2]–[F3].
The full output state after the oracle call is the basis vector , which is a unit vector by orthonormality [F12]. Its rank-one projector is a density operator by [F14]. For output word and remaining address bit , the product basis is orthonormal by [F12], so exactly when and is zero otherwise. The projector formula [F13] gives ; root first-linearity and conjugate symmetry therefore give . Summing over the unmeasured address bit as in [F10] gives output weight one at and zero elsewhere. If the rule answers yes; if it answers no, so the solver is exact on the promise by [F4]. For off-promise the same rule outputs no, but the decision task imposes no condition there; the two total completions assigning either answer on these inputs agree on .
The matrix in [F9] satisfies by finite row-by-column multiplication [F11]. Therefore the two extra gates in the second circuit return the first target bit to its initial value before the same oracle call. The target entering is again , so both query circuits have the same output law and one query; their nonoracle gate counts are 0 and 2 by [F5]–[F6].
Step 1.1 gives the reduction's linear transition bound in the table. In either query circuit, the fixed two-bit reply and one-bit output rule take transitions. These transition counts are separate from the one oracle query and from the quantum gate counts by [F7].