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.
Periodic finite dynamics, quasienergy and controlled truncation — Examples
1 · Prerequisites
- Absolute and Conditional Convergence; Rearrangement; Products
- Absolute Values Completions and P Adic Numbers
- Algebraic Closure, Embeddings, and Separability
- Algebraic Extensions, Extension Degree, and Finite Fields
- Banach Valued Integration and the Radon Nikodym Property
- Banach-Space Differential Calculus and Banach Manifolds
- Binary Operations, Monoids, Groups and Subgroups
- Bounded Linear Operators and Quotient Spaces
- Compactness in Metric Spaces
- Completeness, Completion, and Uniform Continuity
- Complex Coordinate and Path Transport
- Complex Differentiability and the Cauchy–Riemann Equations
- 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
- Connectedness
- 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
- Cyclic Groups and Direct Products
- Decomposition Inertia and Frobenius
- 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
- Foundations of the Real Numbers for Analysis
- 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
- Measurable Functions and Simple Approximation
- Measures and Their Basic Properties
- Metric Spaces
- Monotone Functions, Discontinuities, and Continuity Sets
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Normal Subgroups and Quotient Groups
- Normed and Banach Spaces
- Norming and Separation under Hahn–Banach
- Order, Zorn's Lemma, and the Axiom of Choice
- Partitions of Unity and Paracompactness
- Periodic finite dynamics, quasienergy and controlled truncation
- 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
- Qm Math Controlled Dynamics
- Relations, Functions, and Quotients
- Rings, Subrings, Integral Domains and Fields
- Rⁿ as a Normed Space; Vector-Valued Functions
- Roots, Rational Powers, and Classical Inequalities
- Separation Axioms: the Hierarchy
- Sequences and Limits
- Sequences and Series of Functions; Uniform Convergence
- Series: Convergence and the Nonnegative Tests
- Sigma Algebras and Borel Sets
- 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
- Subspaces, Products, and Quotients
- Suprema and Infima
- Sylow's Theorems, p-Groups and Nilpotent Groups
- Symmetric Groups, Cycle Decomposition and the Sign Homomorphism
- The Analytic Hahn Banach Theorem
- The Cantor Set, Baire Category, and Measure Zero in ℝ
- 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 Lebesgue Integral and the Convergence Theorems
- The Riemann Integral: Definition and Integrability
- The Spectral Theorem, Positive Operators and Singular Value Decomposition
- The Total Derivative in ℝᵐ → ℝⁿ
- The ZFC Axioms and the Basic Set Constructions
- Topological Spaces and Continuity
- Topology of ℝ
- Triangularisation, Generalised Eigenspaces and Jordan Canonical Form
- Unbounded Self Adjoint Operators and Stones Theorem
- 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
Commuting longitudinal drive
Example
Assume Countable Choice. On let , choose real , and choose , , and . For , the unique propagator from time is One Floquet normal form is and .
Example references
Facts & Assumptions
Given: Countable Choice, , , , , and .
Countable Choice is assumed by the bounded-dynamics theorem used for uniqueness (The Axiom of Countable Choice ()).
The scalar derivatives are and , and sine and cosine have period (The derivatives of sine and cosine are cosine and minus sine, The zero sets of sine and cosine and the least positive common period 2 pi).
Norm Dyson series and uniqueness gives uniqueness for a norm-continuous bounded Hermitian matrix family; Finite-dimensional matrix exponential and Unitarity and differentiation of the finite Hermitian matrix exponential give the finite exponential's definition, derivative, and group law.
Finite Floquet unitary normal form defines the Floquet representation as with unitary and -periodic.
The chain rule and the scalar sine derivative give (The chain rule for total derivatives: , The derivatives of sine and cosine are cosine and minus sine).
Verification
Given: [A1], [F1]–[F4], and the matrices and parameters in the Statement.
Put . By [F1] and [F4], . The diagonal entries of are and ; differentiating them using [F2] gives . At the exponential is , so uniqueness in [F2] identifies it with the propagator.
The finite exponential group law in [F2] splits . Thus and the stated give the required factorization. The matrix exponential is unitary by [F2], and by the period in [F1]. Hence this is a Floquet normal form with quasienergies and , each understood modulo .
Quasienergy has no canonical ground value
Statement refuted
The one-period unitary of a finite-dimensional periodic system determines a distinguished least real quasienergy that is independent of the chosen Hermitian logarithm.
Statement references
Facts & Assumptions
Given: Countable Choice, , , , and the one-dimensional state space .
Countable Choice is assumed by the finite Floquet normal-form result (The Axiom of Countable Choice (), Finite Floquet unitary normal form).
Finite Floquet unitary normal form defines a quasienergy as a real eigenvalue of a chosen Hermitian logarithm of , with representatives taken modulo .
The finite matrix exponential is defined by Finite-dimensional matrix exponential, and equality of scalar exponential values is characterized by , and exactly when .
Norm Dyson series and uniqueness supplies the unique propagator for the constant zero Hamiltonian.
Counterexample
Given: [A1], [F1]–[F3], , , and .
Take the constant zero Hamiltonian on . Its propagator is by [F3]. For each integer , the Hermitian scalar satisfies , so each is a valid logarithm of the same monodromy.
In dimension one the only eigenvalue of , and hence its least quasienergy representative, is . It varies with , while all representatives have the same class modulo by [F1, F2]. Therefore the period unitary determines a quasienergy class but no branch-independent least real quasienergy.