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.
Controlled Gates, Phase, and Entanglement — 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
- Bounded Linear Operators and Quotient Spaces
- 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
- 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
- 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
- Eigenvalues, Eigenvectors and the Characteristic Polynomial
- Filters and Ultrafilters
- Finite Counting, Factorials and Binomial Coefficients
- Finite Dimensional Normed Spaces and Riesz Lemma
- Finite-Dimensional Complex Inner-Product Spaces and Matrix Interfaces
- 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 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
- 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 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
- Vector Spaces, Linear Subspaces, Span and Direct Sums
2 · Summary
Objective
This companion computes a two-qubit witness in which the phase of a target unitary changes a control measurement probability. It assumes the two controlled operations are separately available and makes no access or efficiency inference.
3 · Logical flowchart
4 · Definitions, theorems and proofs
None yet.
5 · Examples, counterexamples and false statements
Controlled Global Phase Changes an X-Outcome
Example
Take the target qubit unitary , control input , and target input . Separately grant controlled access to and . For the finite control effects , where , the plus outcome has probability for and for .
Facts & Assumptions
Given: A control-first two-qubit register, , real , the stated input, separate controlled access to the two specified matrices, and the two control effects in the Example.
A Controlled Global Phase Becomes a Relative Control Phase proves the general eigenvector witness, verifies the finite two-outcome POVM, and computes its plus probability.
Controlled Unitary Access defines the control-first block action and requires each capability to be explicitly granted. Its carrier is present in this batch.
Dirac Notation Conversion defines the Dirac pairing by reversing the root linear-first pairing and defines the corresponding outer product.
A unit-vector outer product is a density operator proves that every unit-vector outer product is a density operator.
Finite POVMs and their outcome law defines the finite POVM outcome weight using the density operator and effect.
Ordered tensor registers, their inner product, and wire permutations defines the control-first tensor order and product inner product. Its current draft proof was read.
The computational basis is orthonormal proves the one-qubit computational basis is orthonormal. Its current draft proof was read.
POVM outcome weights are probabilities proves the finite weights of this POVM form a probability distribution.
, , and : for real , and .
Verification
In the ordered basis , the first controlled block is . It sends the input to . Both factors are unit vectors by [L7], so their product is unit by [L6], and its rank-one projector is a density operator by [L4]. In [L1], specialize , , and ; its verified control POVM then gives plus probability .
The separately granted second block is . It sends the input to , where . By [L3] and [L7], . The phase identity [F1] and orthonormality [L7] give ; then the product pairing [L6] gives . Its projector is a density operator by [L4], so the outcome law [L5] applies and gives , which equals by the derivation in the proof of [L1].
At , the second controlled matrix is and its plus probability is . At , its diagonal is and its plus probability is . The minus probability is the complement by normalization [L8], so these are distinct finite outcome laws under the explicit separate-access assumption.