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.
Accessibility Foundation — Examples
1 · Prerequisites
- Absolute and Conditional Convergence; Rearrangement; Products
- Accessibility Foundation
- 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
- Foundations of the Real Numbers for Analysis
- 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
- 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
- Power Series and Real-Analytic Functions
- 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
- 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 Total Derivative in ℝᵐ → ℝⁿ
- The ZFC Axioms and the Basic Set Constructions
- Thermodynamic Framework
- Topology of ℝ
- Vector Spaces, Linear Subspaces, Span and Direct Sums
2 · Summary
These leaf cases show that the adopted contact assumptions have a nondegenerate logarithmic consistency witness and that a degenerate thermometer can satisfy a simple one-system order while failing T4 and product comparison. Both are constructed mathematical models; neither is an experimental observation or a universal claim about real materials.
3 · Logical flowchart
4 · Definitions, postulates, theorems and proofs
None yet.
5 · Examples, experiments and counterexamples
Positive logarithmic contact model as a consistency witness
A calculated mathematical model showing compatibility of the stated accessibility and contact assumptions for positive-coordinate systems; it is not an experiment or evidence that real materials obey the assumptions.
Example
Take finitely many tagged simple types , each with positive dimensionless coordinates , where for internal energy measured in joules and is the numerical work coordinate in its declared fixed unit. Choose dimensionless constants , positive dimensionless reference values , and dimensionless offsets , and define
For a scaled tag , set its coefficients to and its reference coordinates to , so . For every finite compound of declared primitive, scaled, or recursively joined tags, assign the sum of the constituent state entropies and declare exactly when this sum for is no greater than this sum for , on equal-formal-mass pairs. For a thermal join of , define the joined entropy at as the maximum of over with . Use the same entropy comparison for the separated-pair and joined encodings, which have the same formal composition: the pair accesses the join exactly when its entropy is at most the joined entropy, and the join accesses the pair exactly when the reverse inequality holds. Thus contact equilibrium is equivalent to equality with the maximum. For a positive scaled copy of a join, scale all coordinates by and set ; this is consistent with the maximum because scaling by bijects the splits of with the splits of . For nested joins, use the same maximum construction recursively, with the same positive-scaling rule.
To realize every stated comparison, explicitly declare a formal channel for each ordered pair of endpoint types of equal formal mass, including pairs with different primitive compositions. Let be their domains, let be the entropy specified above, and let be the energy map (sum over separated factors, or the single summed energy for a join). The configuration space is the disjoint union , with initial and final equilibrium subsets the two summands and endpoint maps , . Fix singleton protocol and outer-boundary record sets and the transfer-record set . For endpoints the one-second record is , where and for ; no path regularity is asserted. Let its transfer record supply for every , with numerical values in joules. These nonnegative, nondecreasing maps start at zero and specify no thermal transfer across the selected outer boundary. Deleting the fixed outer-boundary field gives a bijection from these seven-field records to the six-field records of Tagged scaled systems and separated products, preserving endpoints, controls, transfers and admission; for one-factor channels use these same records as the single-system model. Permutation and reassociation transport the endpoint tuples and the path labels together; their inverse transports give record bijections, preserving entropy sums, total energy and the zero thermal histories. Assign from these histories and . Admit exactly these records with ; their declared balance is and equal formal mass. Accessibility is existence of one of these admitted records. Thus the entropy order, including the cross-composition comparisons, has explicit witnesses, rather than being inferred from equal mass. Primitive composition here is a formal label, not a mole vector; no chemical or material conservation model, actual apparatus, or realization of these discontinuous paths is asserted. The empty type has its sole state, energy zero and entropy zero, and has its identity record.
This formal model explicitly declares each equilibrium endpoint domain to be the stated positive numerical orthant, with endpoint coordinate map the identity and accessibility the entropy-sum relation above. Its fixed unit map assigns and each work coordinate for a fixed positive unit ; this bookkeeping supplies no material realization. Each primitive tag has a fixed formal composition, while the joined endpoint space is the positive orthant in summed energy and retained work coordinates with the summed composition. A scaled copy transports these coordinates and that composition and retains its distinct tag, exactly as in the declared join interface. This provides a nondegenerate consistency witness for the order, geometric, contact, T5, and C1 assumptions on this positive-coordinate family. It supplies no measured parameter values or empirical claim.
Facts & Assumptions
Given: Positive coordinates; fixed , reference values and constants; tagged scaling as stated; accessibility on separated, joined, and mixed contact encodings is the stated total-entropy comparison; join entropy is the constrained maximum.
Thermal joins and thermal equivalence: a join retains component work coordinates and sums the energy coordinate.
Accessibility axioms A1–A6: A1–A6 are the order conditions to be checked for the example relation.
Simple-system geometric axioms: A7 and S1–S3 are the geometric conditions to be checked.
Thermal-contact axioms T1–T4: T1–T4 are the contact conditions to be checked.
Universal thermal-equilibrium range T5 and Equilibrium-join coherence C1: T5 and C1 are separate conditions to be checked.
The two-point convexity inequality for the exponential function: for and , ; for , equality holds exactly when .
Real powers for positive bases, with the zero-base positive-exponent convention and Continuity and derivatives of positive-base real powers: for and , is differentiable for with derivative .
The mean value theorem, as the case of Cauchy's: for continuous on with and differentiable on there is with : if is continuous on a closed interval and differentiable inside, its endpoint slope equals at some interior point.
Verification
Given: [F1]–[F5] and the construction in the Example.
For , apply [F6] to , then use [F7] and monotonicity of , to obtain for . Apply this inequality to the energy ratios and to the work ratios ; multiplying by and adding proves concavity of . This verifies the convex-combination accessibility condition. Since is strictly increasing, raising at fixed gives a strict successor, proving S1.
The boundary equation rearranges to , where and . By [F8], and . Thus is increasing by [F9]. For , the mean value theorem on the interval between them and the monotonicity of give : when , both the derivative comparison and the sign of reverse. Hence the forward sector lies above the tangent support . A vertical line cannot support this sector because its work coordinate varies on both sides at an interior boundary point. If a nonvertical line with slope parameter supports there, its inequality on graph points gives for both signs of ; dividing by that difference and taking limits forces . This proves uniqueness and gives . On any closed rectangle with and , , so the slope is locally Lipschitz. The graph over is arcwise connected, proving S3.
Put . For any split , [F6] with weights , followed by [F7], gives with equality exactly when . Since , that equality forces the unique split . Multiply by and add the constants ; the resulting inequality is exactly the pair entropy bounded by its value at that split. By the declared total-entropy comparison, this proves T1 and shows that the maximizing split is reversible with the join, establishing the join-splitting clause of T2. For the equal-state scaled split, tagged extensivity gives and , so the pair is reversible with by the example order. The maximizing-split criterion also applies to the two scaled types: their energy coefficients are , and their energy-to-coefficient ratios both equal . Their join is therefore reversible with the pair, which is precisely the scaled-join clause of T2. The binary join entropy is for a constant ; its energy-to-coefficient ratio is at the maximizing split.
By the declared total-entropy comparison, every finite product has a real-valued order. Reflexivity and transitivity follow from the real order; adding the same spectator adds the same number to both sides; positive scaling multiplies the sums by a positive coefficient; and reversible splitting preserves the extensive sum. If , then . Taking yields and hence . This verifies the six adopted order conditions.
For a single system the entropy has the displayed logarithmic form. If a nested join has energy coefficient and is joined with a system of coefficient , the maximum calculation of step 1.3 gives the unique maximizing split at equal energy-to-coefficient ratios; substitution adds to the energy coefficient and adds the new work term. Induction over the finite joins therefore gives coefficient and entropy for the positive work coordinates . Its boundary is with . Direct differentiation gives, for any vector , Thus along each segment in the positive work orthant, the derivative of is nondecreasing by [F9], and the mean value theorem gives . The forward sector lies above this tangent support; uniqueness follows by applying the support inequality to graph points in each direction and , which forces the support functional to equal . Its finite slope components are ; on rectangles bounded away from all coordinate axes, the quotient estimate from step 1.2 applies to each component and proves local Lipschitz regularity. The positive orthant and its graph are arcwise connected. Increasing gives S1, and the coordinatewise concavity argument of step 1.1 gives the convex-combination accessibility condition. Hence each join satisfies the same simple-system geometry.
Applying the two-weight maximum calculation of steps 1.3 and 2.2 to any two primitive or recursively joined types shows that and are thermally equivalent exactly when , where are their energy coefficients. Equality of ratios is transitive, proving T3. For any such simple type with coefficient and at least one work coordinate , fix a state and choose , keeping and all other coordinates fixed. The entropy formula of step 2.2 strictly increases with , so . Both outer states have the same ratio and hence are thermally equivalent. This proves T4 for primitive and recursively joined simple types.
Let be any primitive or recursively joined simple types, with energy coefficients . Given and any allowed work-coordinate vector , choose . The two-weight maximum calculation in steps 1.3 and 2.2 makes thermally equivalent to , proving T5. For any equilibrated pair , the same calculation gives . Their joined state has energy coefficient and energy , so its ratio equals the common ratio; the two-weight maximum criterion therefore makes that joined state thermally equivalent to , and likewise to . This proves C1 for every admitted join.
Remarks
The coefficients are chosen mathematical parameters. Their existence checks compatibility of the postulates but does not report measurements, determine SI entropy units, or prove the assumptions for a real substance.
Degenerate thermometers can fail product comparison
An abstract positive-energy thermometer model showing failure of T4 and the comparison hypothesis for products; it is not a measured thermometer or a claim about ordinary thermodynamic bodies.
Statement refuted
Let be an internal-energy value measured in joules, and use the dimensionless numerical coordinate , so , as in SI quantities and unit conventions. The one-system order relation on the degenerate thermometer state space , together with the thermal equilibration operation described below, need not satisfy T4 or the comparison hypothesis on products. Consequently, a monotone entropy on the single-system space need not represent product accessibility.
Facts & Assumptions
Given: A state is a positive dimensionless energy coordinate as defined in the Statement. For one copy, accessibility is . Thermal equilibrium of scaled copies holds exactly when their normalized coordinates . For two unit copies starting at , put , let
and define the product forward sector as , where is the set of all finite convex combinations with , , and . describes componentwise energy increase and thermal equilibration followed by energy increase, as in Lieb–Yngvason §IV.C. To respect the permutation identification in [F1], a two-copy state here is the class of under swapping its coordinates. Define exactly when some representative of belongs to , where are the displayed sets for the initial representative . This explicitly declares the permutation-compatible version of the source construction; its independence of the initial representative is checked below.
To realize these relations by formal process records, use for one copy and for two ordered copies. In the latter case admit endpoint pairs exactly when under the displayed sector relation; in the former admit exactly . For either domain, put , take identity endpoint maps, a singleton control set, transfer-record set , and a fixed outer boundary. For each admitted pair use exactly the one-second record , where for and . Its transfer record supplies for every , with numerical values in joules, so . Define for one copy and for two, and assign . The same one-copy construction applies to a scaled copy using its actual energy coordinate . Permuting initial and final representatives transports their endpoint labels and the corresponding path labels; the inverse permutations give record bijections preserving boundary, thermal histories, total energies and admission by the representative invariance checked in step 1.1 below. Quotienting therefore gives exactly the stated class relation while retaining both factors up to permutation. These are formal records without auxiliaries, path regularity, core-class membership or material realization asserted; their zero histories are explicit data, not an inference from zero net heat.
Tagged scaled systems and separated products: product states are tagged scaled copies and product comparison is the declared relation, not coordinate addition.
Thermal-contact axioms T1–T4: T4 requires a thermal-equilibrium class crossing strictly below and above every state.
Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm: the real natural logarithm is strictly increasing on positive reals, has , and satisfies .
SI quantities and unit conventions: energy is measured in joules, and numerical energy coordinates are divided by their displayed units before they are used as Euclidean coordinates.
Counterexample
Given: [F1]–[F4] and the product sector specified above.
Let . Then and , since the mean is unchanged; linearity of also gives . Thus the declared relation is independent of the representative of ; target representatives are already quantified over, and reflexivity follows from . Consider the distinct classes and . From , every point of has coordinate sum at least , and every point of has both coordinates at least , hence sum at least . Finite convex combinations preserve this sum bound. Every representative of has sum , so .
In the one-system space, strict accessibility is exactly strict increase of , while thermal equilibrium is equality of normalized energies. If , then , so and the two cannot be thermally equivalent. Thus T4 fails.
From , both and consist of points whose two coordinates are at least ; finite convex combinations preserve both inequalities. Every representative of has a coordinate equal to . Therefore . Together with step 1.1, this proves incomparability of distinct product states and failure of the comparison hypothesis.
By [F4], is dimensionless, so the single-system function is well-defined; it is strictly increasing and represents . If its additive sum represented product accessibility, the states and would have equal summed entropy , forcing accessibility both ways. Step 1.1 and step 2.1 show neither direction holds. Therefore this single-system entropy does not represent the product relation. Since the example fails T4 by step 1.2, it does not satisfy the hypotheses of a product-comparison result that includes T4.
Remarks
The example concerns the formal order model and shows why a product theorem must retain T4 or provide another adequate thermal partner. Lieb–Yngvason’s subsequent Theorem 4.9 treats entropy construction without T4 only when the degenerate type is joined to a system satisfying the appropriate contact conditions.
Sources
- Lieb and Yngvason, The Physics and Mathematics of the Second Law of Thermodynamics, §§III.B–IV.A
- André Thess, The Lieb–Yngvason Machine: A didactical tool for the definition of entropy in classical thermodynamics, §§2–4
- Lieb and Yngvason, The Physics and Mathematics of the Second Law of Thermodynamics, §IV.C, pp. 59–60
- André Thess, The Lieb–Yngvason Machine: A didactical tool for the definition of entropy in classical thermodynamics, §2
- Goddard, The second law of thermodynamics as variation on a theme of Carathéodory, §3