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.
Perron Inversion and the Explicit Formula — Examples
1 · Prerequisites
- Absolute and Conditional Convergence; Rearrangement; Products
- Analyticity of Holomorphic Functions; Liouville and Morera
- Approximation and Compactness in C(K)
- Arc Length and Rectifiable Curves
- Areas of Elementary Plane Figures
- Arithmetic Functions and Dirichlet Convolution
- Binary Operations, Monoids, Groups and Subgroups
- Bounded Variation and the Riemann–Stieltjes Integral
- Chebyshev Bounds and Mertens Theorems
- Compactness
- Compactness in Metric Spaces
- Completeness, Completion, and Uniform Continuity
- Complex Coordinate and Path Transport
- Complex Differentiability and the Cauchy–Riemann Equations
- Complex Lp Spaces and Test-Function Conventions
- Complex Power Series and Analytic Functions
- 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
- Contour Integration
- Cosets, Index and Lagrange's Theorem
- Countability and Uncountability
- Countability Axioms and Cardinal Functions
- Darboux, L'Hôpital, and Taylor's Theorem
- Density Separability and Convolution in Lᵖ
- Determinants of Matrices over a Commutative Ring
- Dirichlet Series and Euler Products
- Divisibility, Euclidean Domains, Principal Ideal Domains and Unique Factorisation
- Divisibility, Greatest Common Divisors and Bézout's Identity
- Equivalent Forms of Completeness
- Filters and Ultrafilters
- Finite Counting, Factorials and Binomial Coefficients
- Finite Probability and the Probabilistic Method
- Foundations of the Real Numbers for Analysis
- Fourier Transform Convolution and Approximate Identities
- Fubini and Change of Variables
- Function Space Topologies and the Exponential Law
- Fundamental Trigonometric Identities
- Gaussian Elimination, Elementary Matrices and Reduced Row Echelon Form
- Goursat's Theorem and Cauchy's Theorem in a Convex Domain
- Group Actions, Orbits, Stabilisers and Cayley's Theorem
- Ideals, Quotient Rings and the Isomorphism Theorems for Rings
- Improper and Parameter-Dependent Multiple Integrals
- Improper Integrals
- Incidence Algebras and Möbius Inversion
- Infinite Products and the Weierstrass Factorisation Theorem
- Isolated Singularities and Laurent Series
- Lebesgue Measure on Euclidean Space
- Limits of Real Functions
- limsup, liminf, and Subsequential Limits
- Line Integrals and the Gradient Theorem
- 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
- Mixed Partials, Taylor Formulae, and Extrema
- Monotone Functions, Discontinuities, and Continuity Sets
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Normal Subgroups and Quotient Groups
- Order, Zorn's Lemma, and the Axiom of Choice
- Outer Measure and the Caratheodory Extension Theorem
- Partitions of Unity and Paracompactness
- Perron Inversion and the Explicit Formula
- pi: the Equivalent Characterizations
- Pointwise Extended-Real Function Products
- Polynomial Rings, the Division Algorithm and Roots
- Power Series and Real-Analytic Functions
- Primes, Euclid's Lemma and the Fundamental Theorem of Arithmetic
- Product Measures and the Fubini Tonelli Theorems
- Properties of the Integral and the Working FTC
- Relations, Functions, and Quotients
- Rings, Subrings, Integral Domains and Fields
- Rⁿ as a Normed Space; Vector-Valued Functions
- Roots, Rational Powers, and Classical Inequalities
- Schwartz Space and the Plancherel Theorem
- 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
- Stone–Weierstrass in General
- Subspaces, Products, and Quotients
- Suprema and Infima
- Symmetric Groups, Cycle Decomposition and the Sign Homomorphism
- The Argument Principle and Rouché's 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 Exponential Function
- The Fundamental Theorems of Calculus
- The Gamma Function
- The Identity Theorem, the Maximum Principle and the Open Mapping Theorem
- The Inverse and Implicit Function Theorems
- The Lebesgue and Riemann Integrals Compared
- The Lebesgue Integral and the Convergence Theorems
- The Logarithm and General Powers
- The Lᵖ Spaces Holder Minkowski and Riesz Fischer
- The Real Gamma and Beta Functions
- The Residue Theorem and the Evaluation of Real Integrals
- The Riemann Integral in Rᵐ and Jordan Content
- The Riemann Integral: Definition and Integrability
- The Riemann Zeta Function
- The Topology of Euclidean Space
- The Total Derivative in ℝᵐ → ℝⁿ
- The Winding Number and the Global Cauchy Theorem
- The ZFC Axioms and the Basic Set Constructions
- Topological Spaces and Continuity
- Topology of ℝ
- Triangularisation, Generalised Eigenspaces and Jordan Canonical Form
- Vector Spaces, Linear Subspaces, Span and Direct Sums
2 · Summary
These calculations isolate the half-jump, the four residue families, and the ordering convention that a sharp zero sum requires. The global sharp and smoothed formula examples inherit countable choice from their supplying theorems.
3 · Logical flowchart
4 · Definitions, theorems and proofs
None yet.
5 · Examples, counterexamples and false statements
Perron's kernel at and away from its jump
Example
At , the limiting kernels for are respectively .
Verification
Given: the symmetric and truncated Perron kernel formulas.
Substitute in the three branches of the symmetric kernel.
The truncated estimate has the separate branch only at , exhibiting why the half value cannot be merged into either away-from-jump estimate.
Perron inversion for a finite Dirichlet polynomial
Example
For , Perron's integral is for , for , and for .
Verification
Given: the Perron formula for finite sums.
Termwise inversion gives ; for , the first term is .
The second term is according as , proving all three values without a limit interchange.
The von Mangoldt residue table
Example
Assume countable choice.
For , the contour integrand has contributions at , at a nontrivial zero, from all negative even zeros, and at .
Verification
Given: Countable choice, and the residue ledger.
The pole at and each nontrivial zero have the listed local residues, with zero multiplicity multiplying the second entry.
Summing the geometric-logarithmic trivial family and retaining the independent pole of at gives the remaining two entries.
Smoothed versus sharp explicit formulas
Example
Assume countable choice.
The linear cutoff equals through and fades to on , whereas the sharp formula evaluates and gives half weight at a prime power.
Verification
Given: Countable choice and the smoothed and sharp formulas.
The two integrations by parts in the smoothed formula supply Mellin decay, hence a declared convergent zero sum.
The sharp formula instead has a finite ordinate sum and an error containing ; at a jump its left hand side is explicitly half-weighted.
Selecting an admissible contour height
Example
Assume countable choice. For , one can choose with distance at least from every zero ordinate in , for an absolute .
Verification
Given: Countable choice and the unit-interval zero count.
The three adjacent unit-interval bounds show that the number of relevant ordinates is at most after enlarging an absolute constant to cover . Around each such ordinate remove an interval of radius , where .
The total removed length inside is at most . Consequently some remains in that interval, and by construction its distance from every relevant ordinate is at least .
An unordered infinite zero sum is not an explicit formula
Statement refuted
For , the bare unordered expression is a defined quantity equal to the sharp explicit-formula zero contribution.
Counterexample
Given: Countable choice and the sharp and smoothed explicit formulas.
The sharp formula asserts only finite sums and specifies an error before any limit is taken.
The smoothed formula supplies a different convergence mechanism through its Mellin decay. Neither result assigns a value to the displayed unordered bare sum, so the asserted equality has no defined left side.
Right-continuous psi has the wrong Perron endpoint
Statement refuted
At every prime power , the right-continuous equals the Perron endpoint value.
Counterexample
Given: and the definitions of and .
The right-continuous sum includes the full last term: .
Perron's endpoint is , so the two values differ by .