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.
Quantitative DLR uniqueness, concentration and spatial response — Examples
1 · Prerequisites
- Absolute and Conditional Convergence; Rearrangement; Products
- Binary Operations, Monoids, Groups and Subgroups
- Compactness in Metric Spaces
- Completeness, Completion, and Uniform Continuity
- 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
- Countability and Uncountability
- Finite Counting, Factorials and Binomial Coefficients
- Finite-range lattice interaction and conditional energy
- Foundations of the Real Numbers for Analysis
- Limits of Real Functions
- limsup, liminf, and Subsequential Limits
- Measures and Their Basic Properties
- Metric Spaces
- Monotone Functions, Discontinuities, and Continuity Sets
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Order, Zorn's Lemma, and the Axiom of Choice
- Outer Measure and the Caratheodory Extension Theorem
- Power Series and Real-Analytic Functions
- Properties of the Integral and the Working FTC
- Quantitative DLR uniqueness, concentration and spatial response
- Relations, Functions, and Quotients
- Roots, Rational Powers, and Classical Inequalities
- Sequences and Limits
- Sequences and Series of Functions; Uniform Convergence
- Series: Convergence and the Nonnegative Tests
- Sigma Algebras and Borel Sets
- Suprema and Infima
- The Derivative and the Mean Value Theorems
- The Exponential Function
- The Logarithm and General Powers
- The Riemann Integral: Definition and Integrability
- The ZFC Axioms and the Basic Set Constructions
- Topology of ℝ
- 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
Nearest-neighbor Ising influence bound
Example
Assume Countable Choice: every countable family of nonempty sets has a choice function. Let , let with its cylinder-generated Borel -algebra, fix and , and let be a site field. For , put if and otherwise. For a finite and exterior configuration , write for and otherwise, and define
The pair sum is over unordered pairs and is finite because each site has nearest neighbors. For bounded measurable , set
Here denotes the configuration equal to on and to on .
For each field , these kernels are positive normalized probability kernels. They are proper, meaning that they leave every event determined by the exterior spins fixed; consistent, meaning whenever finite ; and finite range, meaning that for every finite and cylinder event , depends on only finitely many exterior coordinates.
For , write for the one-site law and define the influence coefficient
Then when and otherwise. Consequently, if
then every influence row sum is strictly below . More generally, if , then for any two site fields with the same , the matrix defined by when and otherwise is a common finite-range influence envelope with row sums below . Thus, under this inequality, the finite-volume comparison estimate of the Dobrushin comparison theorem applies to and . This is a sufficient criterion; failure of the inequality is not claimed to imply nonuniqueness.
Example references
Facts & Assumptions
Given: Countable Choice, the nearest-neighbor Ising couplings, and one or two site fields as specified in the Statement.
Countable Choice means that every countable family of nonempty sets has a choice function (The Axiom of Countable Choice ()).
For the finite-range Ising conditional energy, changing only boundary spin changes the one-site law at by at most in half-total-variation distance; it gives zero influence when (Ising influence bounded by hyperbolic tangent).
Under Countable Choice, proper consistent finite-range specifications on a finite-alphabet lattice with a uniform finite one-site influence radius and a common nonnegative finite-range influence envelope of supremum row sum below satisfy the finite-volume Dobrushin comparison estimate; each also has a unique DLR state and the stated infinite-volume comparison estimate (Finite-spin Dobrushin comparison and boundary response).
Verification
For finite , the pair sum has at most terms meeting , and the field sum is finite, so every energy is real and the finite partition sum is strictly positive. The kernel is normalized by its definition. For every Borel event, each replacement map is measurable, so the kernel probability is measurable; replacing spins in leaves every exterior-measurable event fixed. For a cylinder event, its kernel probability depends only on its finite support outside and the finitely many exterior neighbors of , so it has finite range.
For each site , exactly sites satisfy . By [F1], each corresponding influence coefficient is at most , while every other coefficient vanishes. Therefore for every .
If finite , split into the pair terms whose support meets and field terms on , which equal , and the remaining terms , which do not depend on . Hence , and . Thus the kernels form the stated proper, consistent, finite-range specification.
If , the matrix in the Statement dominates the influence matrices of both and , has radius in the metric, and has row sums below . The constructed specifications are proper, consistent, and finite range by steps 1.1–1.2. By Countable Choice and [F2], the hypotheses of the comparison theorem hold and its finite-volume comparison estimate applies. The inequality is only sufficient; failure of the bound is not claimed to imply nonuniqueness.