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.
Finite reduced dynamics, memory and quantum trajectories — Examples
1 · Prerequisites
- Absolute and Conditional Convergence; Rearrangement; Products
- 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
- 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
- Cosets, Index and Lagrange's Theorem
- Countability and Uncountability
- Divisibility, Euclidean Domains, Principal Ideal Domains and Unique Factorisation
- Dual Spaces, Bilinear and Quadratic Forms, and Sylvester's Law of Inertia
- Filters and Ultrafilters
- Finite completely positive trace-preserving maps
- Finite Counting, Factorials and Binomial Coefficients
- Finite Dimensional Normed Spaces and Riesz Lemma
- Finite reduced dynamics, memory and quantum trajectories
- Foundations of the Real Numbers for Analysis
- Free Modules, Exact Sequences, Projective and Injective Modules
- Fundamental Trigonometric Identities
- 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
- Metric Spaces
- Modules, Submodules, Quotient Modules and the Isomorphism Theorems
- Monotone Functions, Discontinuities, and Continuity Sets
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Normal density states and spectral moments
- 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
- Properties of the Integral and the Working FTC
- 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
- Strongly Continuous Semigroups and Hille Yosida
- Subspaces, Products, and Quotients
- Suprema and Infima
- Tensor Products of Modules
- The Complex Exponential and Euler's Formula
- The Derivative and the Mean Value Theorems
- The Exponential Function
- The Fundamental Theorems of Calculus
- The Riemann Integral: Definition and Integrability
- The Topology of Euclidean Space
- The ZFC Axioms and the Basic Set Constructions
- Topological Spaces and Continuity
- Topology of ℝ
- Trace-class bounded-observable response
- Vector Spaces, Linear Subspaces, Span and Direct Sums
2 · Summary
3 · Logical flowchart
4 · Definitions, postulates, theorems and proofs
None yet.
5 · Examples, experiments and counterexamples
A finite bath revives coherence
A conditional two-qubit finite-environment unitary model with fixed product preparation. The coherence revival is an exact model prediction, not a reported experiment or a general claim about finite reservoirs.
Example
For , , in , and in joule-seconds, choose , , and the fixed environment state with in the displayed environment eigenbasis. Here coherence means an off-diagonal matrix entry in the displayed system basis. The reduced map leaves the system populations unchanged and multiplies each coherence by . At a positive time where the multiplier is zero, it erases the distinction between the two eigenstates; at it restores them with their signs exchanged. Thus this finite reduced family is neither a semigroup nor CP-divisible.
Example references
Facts & Assumptions
Given: The two-qubit model, , , and the definitions of channel semigroup and CP-divisibility.
The two-qubit calculation in Product-state reduced evolution is a channel uses this exact Hamiltonian and environment state; it defines the matrix exponential by its power series, derives with , and obtains the reduced channel's coherence multiplier .
Finite channel families, semigroups, and CP-divisibility: the semigroup law is with , and CP-divisibility requires a channel for every with .
is a bijection from onto the real unit circle: some satisfies .
, , and : for real .
, and the complex exponential extends the real exponential: for complex .
The complex exponential by its power series: and is the scalar exponential power series.
Finite matrix spectral and state calculus: every finite Hermitian matrix has an orthonormal eigenbasis with real eigenvalues; for a real-valued function on its finite spectrum, the corresponding spectral operator is basis-independent.
Verification
The Hermitian matrix has the orthonormal eigenbasis of product eigenvectors and eigenvalues by direct multiplication, consistent with [F7]. For this exact matrix and environment preparation, [F1] defines the matrix exponential by its power series and derives , where . By [F4], each diagonal phase has modulus one, so these blocks and are unitary. The environment state has equal weight on , so the reduced map is ; multiplying the two diagonal matrices shows that the off-diagonal entries are multiplied by , while the diagonal entries are unchanged.
By [F3] choose with and , and put . Then [F4] gives , while [F5] and [F6] with give ; another application of [F5] yields and .
Let and . Since , , and , each is a positive trace-one matrix. Steps 1.1 and 1.2 give , but and . Thus , so the semigroup law in [F2] fails. If a channel satisfied , it would map the equal intermediate states to equal outputs, contradicting their distinct final states; by [F1], every is a channel, so the family is not CP-divisible by [F2].
Single excitation jump law
An ideal trajectory-ensemble calculation for an undriven qubit in the finite amplitude-damping GKSL model. It predicts a model waiting-time law and state update; it is not a reported detector observation.
Example
In the normalized jump-branch ensemble for the finite amplitude-damping model, let be in and take the initial qubit state . The no-jump survival weight at time is . If , the ensemble assigns the first-jump time density and post-jump state ; because there is no drive and , there are no later jumps. If , no jump occurs and the survival weight is one. This is a model branch distribution, not a detector observation.
Example references
Facts & Assumptions
Given: The qubit amplitude-damping model, initial state , and the finite jump-trajectory branch definition.
Amplitude damping with operational time units: for and , the excited-state population obeys with measured in seconds.
Finite GKSL jump-trajectory branches: the no-jump operator is with , and a one-jump branch at time has operator . Its branch-weight density is the real scalar trace of the branch state, integrated by the ordinary scalar Riemann integral; a degenerate interval has integral zero.
Finite jump expansion and ensemble equation: the branch weights in the finite expansion form a normalized ensemble for each .
, and the complex exponential extends the real exponential: on real arguments, the complex exponential used in the model formulas agrees with the real exponential .
Verification
For , the no-jump generator is . Hence and . For the initial state , the no-jump branch weight is , equal to the excited population in [F1].
For and a one-jump history at , , since and . Its branch-weight density from [F2] is . Because and , every branch with at least two jumps has zero weight. The normalized ensemble [F3] therefore gives : the only nonzero contributions are the no-jump weight from step 1.1 and the one-jump integral. Letting , [F4] identifies this as the real exponential and [F5] gives because ; hence the first-jump density has total mass one. Each first jump leaves the normalized state . If , then , all positive-jump branches vanish, and the no-jump weight is one.