Alphabeta Math
Pipeline-generated
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

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

ExampleConstruction: AI-adaptedVerification: AI-adaptedverified 2026-10-15 (gpt-6-luna, gpt-6.1-sol, and delegated Codex review/repair agents; see completed run evidence)Open item page →

Positive logarithmic contact model as a consistency witness

Physical scope

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 i, each with positive dimensionless coordinates u>0,v>0, where u=E/(1 J) for internal energy E measured in joules and v is the numerical work coordinate in its declared fixed unit. Choose dimensionless constants ci,ri>0, positive dimensionless reference values u⋆,i,v⋆,i>0, and dimensionless offsets bi∈R, and define

si(u,v)=cilog⁡uu⋆,i+rilog⁡vv⋆,i+bi.

For a scaled tag ti, set its coefficients to tci,tri,tbi and its reference coordinates to tu⋆,i,tv⋆,i, so sti(tu,tv)=t si(u,v). For every finite compound of declared primitive, scaled, or recursively joined tags, assign the sum of the constituent state entropies and declare A≺B exactly when this sum for A is no greater than this sum for B, on equal-formal-mass pairs. For a thermal join of i,j, define the joined entropy at (u,vi,vj) as the maximum of si(ui,vi)+sj(uj,vj) over ui,uj>0 with ui+uj=u. 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 tΔij of a join, scale all coordinates by t and set stΔij(tZ):=tsΔij(Z); this is consistent with the maximum because scaling (ui,uj) by t bijects the splits of u with the splits of tu. 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 T,T′ of equal formal mass, including pairs with different primitive compositions. Let XT,XT′ be their domains, let HT:XT→R be the entropy specified above, and let ET:XT→R J be the energy map (sum over separated factors, or the single summed energy for a join). The configuration space is the disjoint union ZT,T′=({0}×XT)∪({1}×XT′), with initial and final equilibrium subsets the two summands and endpoint maps (0,a)↦a, (1,b)↦b. Fix singleton protocol and outer-boundary record sets {∗} and the transfer-record set RT,T′=XT×XT′. For endpoints (a,b) the one-second record is Pa,b=([0,1],a,b,za,b,∗,∗,(a,b)), where za,b(0)=(0,a) and za,b(t)=(1,b) for 0<t≤1; no path regularity is asserted. Let its transfer record (a,b) supply HPa,bin(t)=HPa,bout(t)=0 for every t∈[0,1], 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 Q(a,b)=0 J from these histories and Won(a,b)=ET′(b)−ET(a). Admit exactly these records with HT(a)≤HT′(b); their declared balance is ΔE=Q+Won 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 E=u(1 J) and each work coordinate Wa=vawa for a fixed positive unit wa; 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 ci,ri>0, 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.

[F1]

Thermal joins and thermal equivalence: a join retains component work coordinates and sums the energy coordinate.

[F2]

Accessibility axioms A1–A6: A1–A6 are the order conditions to be checked for the example relation.

[F3]

Simple-system geometric axioms: A7 and S1–S3 are the geometric conditions to be checked.

[F4]

Thermal-contact axioms T1–T4: T1–T4 are the contact conditions to be checked.

[F5]

Universal thermal-equilibrium range T5 and Equilibrium-join coherence C1: T5 and C1 are separate conditions to be checked.

[F6]

The two-point convexity inequality for the exponential function: for a,b∈R and t∈[0,1], exp⁡((1−t)a+tb)≤(1−t)exp⁡(a)+texp⁡(b); for 0<t<1, equality holds exactly when a=b.

[F7]
[F8]

Real powers for positive bases, with the zero-base positive-exponent convention and Continuity and derivatives of positive-base real powers: for K>0 and α∈R, vα is differentiable for v>0 with derivative αvα−1.

Verification

Given: [F1]–[F5] and the construction in the Example.

1.1F3F6F7algebra

For a,b>0, apply [F6] to log⁡a,log⁡b, then use [F7] and monotonicity of log⁡, to obtain log⁡((1−t)a+tb)≥(1−t)log⁡a+tlog⁡b for 0≤t≤1. Apply this inequality to the energy ratios u/u⋆,i and to the work ratios v/v⋆,i; multiplying by ci,ri>0 and adding bi proves concavity of si. This verifies the convex-combination accessibility condition. Since log⁡ is strictly increasing, raising u at fixed v gives a strict successor, proving S1.

1.2F3F8F9algebra

The boundary equation si(u′,v′)=si(ux,vx) rearranges to u′=g(v′)=K(v′)−α, where K=uxvxα>0 and α=ri/ci>0. By [F8], g′=−αK(v′)−α−1 and g′′=α(α+1)K(v′)−α−2>0. Thus g′ is increasing by [F9]. For v′≠vx, the mean value theorem on the interval between them and the monotonicity of g′ give g(v′)≥g(vx)+g′(vx)(v′−vx): when v′<vx, both the derivative comparison and the sign of v′−vx reverse. Hence the forward sector u′≥g(v′) lies above the tangent support u′−ux+(riux/(civx))(v′−vx)=0. 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 q supports there, its inequality on graph points gives g(v′)−g(vx)+q(v′−vx)≥0 for both signs of v′−vx; dividing by that difference and taking limits forces q=−g′(vx). This proves uniqueness and gives Pi=riux/(civx). On any closed rectangle with u,u~≤u1 and v,v~≥v0>0, ∣u/v−u~/v~∣≤∣u−u~∣/v0+u1∣v−v~∣/v02, so the slope is locally Lipschitz. The graph over v′>0 is arcwise connected, proving S3.

1.3F1F4F6F7givenalgebra

Put C=ci+cj. For any split ui+uj=u, [F6] with weights ci/C,cj/C, followed by [F7], gives ciClog⁡uici+cjClog⁡ujcj≤log⁡uC, with equality exactly when ui/ci=uj/cj. Since ui+uj=u, that equality forces the unique split ui=ciu/C, uj=cju/C. Multiply by C and add the constants cilog⁡(ci/u⋆,i)+cjlog⁡(cj/u⋆,j)+bi+bj+rilog⁡(vi/v⋆,i)+rjlog⁡(vj/v⋆,j); 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 sti(tu,tv)=tsi(u,v) and s(1−t)i((1−t)u,(1−t)v)=(1−t)si(u,v), so the pair is reversible with x by the example order. The maximizing-split criterion also applies to the two scaled types: their energy coefficients are tci,(1−t)ci, and their energy-to-coefficient ratios both equal u/ci. Their join is therefore reversible with the pair, which is precisely the scaled-join clause of T2. The binary join entropy is Clog⁡u+rilog⁡vi+rjlog⁡vj+Cij for a constant Cij; its energy-to-coefficient ratio is u/C=ui/ci=uj/cj at the maximizing split.

2.1F2givenstep 1.1algebra

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 A+ϵnZ0≺B+ϵnZ1, then s(A)−s(B)≤ϵn(s(Z1)−s(Z0)). Taking n→∞ yields s(A)≤s(B) and hence A≺B. This verifies the six adopted order conditions.

2.2F3F8F9givenstep 1.1step 1.2step 1.3algebra

For a single system the entropy has the displayed logarithmic form. If a nested join has energy coefficient C and is joined with a system of coefficient c>0, the maximum calculation of step 1.3 gives the unique maximizing split at equal energy-to-coefficient ratios; substitution adds c to the energy coefficient and adds the new work term. Induction over the finite joins therefore gives coefficient C=∑kck and entropy Clog⁡u+∑krklog⁡vk+C0 for the positive work coordinates v=(v1,…,vm). Its boundary is u=g(v)=K∏kvk−αk with αk=rk/C>0. Direct differentiation gives, for any vector h, D2g(v)[h,h]=g(v)[(∑kαkhkvk)2+∑kαk(hkvk)2]≥0. Thus along each segment in the positive work orthant, the derivative of g is nondecreasing by [F9], and the mean value theorem gives g(v′)≥g(v)+∇g(v)⋅(v′−v). The forward sector u≥g(v) lies above this tangent support; uniqueness follows by applying the support inequality to graph points in each direction h and −h, which forces the support functional to equal ∇g(v). Its finite slope components are Pk=rku/(Cvk); 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 u 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.

3.1F4givenstep 1.3step 2.2algebra

Applying the two-weight maximum calculation of steps 1.3 and 2.2 to any two primitive or recursively joined types A,B shows that x=(uA,vA) and y=(uB,vB) are thermally equivalent exactly when uA/CA=uB/CB, where CA,CB>0 are their energy coefficients. Equality of ratios is transitive, proving T3. For any such simple type with coefficient C and at least one work coordinate vk, fix a state x=(u,v) and choose 0<vk−<vk<vk+, keeping u and all other coordinates fixed. The entropy formula of step 2.2 strictly increases with vk, so x−≺≺x≺≺x+. Both outer states have the same ratio u/C and hence are thermally equivalent. This proves T4 for primitive and recursively joined simple types.

4.1F5givenstep 1.3step 2.2algebra∎

Let A,B be any primitive or recursively joined simple types, with energy coefficients CA,CB>0. Given x=(uA,vA) and any allowed work-coordinate vector vB, choose uB=CBuA/CA. The two-weight maximum calculation in steps 1.3 and 2.2 makes x thermally equivalent to y=(uB,vB), proving T5. For any equilibrated pair x,y, the same calculation gives uA/CA=uB/CB. Their joined state has energy coefficient CA+CB and energy uA+uB, so its ratio equals the common ratio; the two-weight maximum criterion therefore makes that joined state thermally equivalent to x, and likewise to y. 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.

CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedverified 2026-10-15 (gpt-6-luna, gpt-6.1-sol, and delegated Codex review/repair agents; see completed run evidence)Open item page →

Degenerate thermometers can fail product comparison

Physical scope

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 E be an internal-energy value measured in joules, and use the dimensionless numerical coordinate U:=E/(1 J)∈(0,∞), so E=U(1 J), as in SI quantities and unit conventions. The one-system order relation U≤U′ on the degenerate thermometer state space Γ=(0,∞), 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 U as defined in the Statement. For one copy, accessibility is U≤U′. Thermal equilibrium of scaled copies λ1U1,λ2U2 holds exactly when their normalized coordinates U1=U2. For two unit copies starting at (U1,U2), put Uˉ=(U1+U2)/2, let

A={(U1′,U2′):U1′≥U1, U2′≥U2},B={(U1′,U2′):U1′≥Uˉ, U2′≥Uˉ},

and define the product forward sector as conv⁡(A∪B), where conv⁡(C) is the set of all finite convex combinations ∑k=1mtkzk with zk∈C, tk≥0, and ∑ktk=1. A describes componentwise energy increase and B 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 [u] of u=(U1,U2) under swapping its coordinates. Define [u]≺[v] exactly when some representative of [v] belongs to conv⁡(Au∪Bu), where Au,Bu are the displayed sets for the initial representative u. 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 X=Γ for one copy and X=Γ2 for two ordered copies. In the latter case admit endpoint pairs a,b exactly when [a]≺[b] under the displayed sector relation; in the former admit exactly a≤b. For either domain, put Z−=Z+=Z=X, take identity endpoint maps, a singleton control set, transfer-record set X×X, and a fixed outer boundary. For each admitted pair use exactly the one-second record Pa,b=([0,1],a,b,za,b,∗,(a,b)), where za,b(t)=a for 0≤t<1 and za,b(1)=b. Its transfer record supplies HPa,bin(t)=HPa,bout(t)=0 for every t∈[0,1], with numerical values in joules, so Q[Pa,b]=0. Define E(U)=U(1 J) for one copy and E(U1,U2)=(U1+U2)(1 J) for two, and assign Won[Pa,b]=E(b)−E(a). The same one-copy construction applies to a scaled copy using its actual energy coordinate λU. 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.

[F1]

Tagged scaled systems and separated products: product states are tagged scaled copies and product comparison is the declared relation, not coordinate addition.

[F2]

Thermal-contact axioms T1–T4: T4 requires a thermal-equilibrium class crossing strictly below and above every state.

[F3]

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 log⁡1=0, and satisfies log⁡(ab)=log⁡a+log⁡b.

[F4]

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.

1.1givenF1algebra

Let π(U1,U2)=(U2,U1). Then Aπu=πAu and Bπu=πBu, since the mean is unchanged; linearity of π also gives conv⁡(Aπu∪Bπu)=πconv⁡(Au∪Bu). Thus the declared relation is independent of the representative of [u]; target representatives are already quantified over, and reflexivity follows from u∈Au. Consider the distinct classes [(1,4)] and [(2,2)]. From u=(1,4), every point of Au has coordinate sum at least 5, and every point of Bu has both coordinates at least Uˉ=5/2, hence sum at least 5. Finite convex combinations preserve this sum bound. Every representative of [(2,2)] has sum 4, so [(1,4)]⊀[(2,2)].

1.2givenF2algebra

In the one-system space, strict accessibility is exactly strict increase of U, while thermal equilibrium is equality of normalized energies. If U0≺≺U≺≺U1, then U0<U<U1, so U0≠U1 and the two cannot be thermally equivalent. Thus T4 fails.

2.1givenstep 1.1algebra

From u=(2,2), both Au and Bu consist of points whose two coordinates are at least 2; finite convex combinations preserve both inequalities. Every representative of [(1,4)] has a coordinate equal to 1. Therefore [(2,2)]⊀[(1,4)]. Together with step 1.1, this proves incomparability of distinct product states and failure of the comparison hypothesis.

3.1F1F2F3F4step 1.1step 2.1algebra∎

By [F4], U is dimensionless, so the single-system function S(U)=log⁡U is well-defined; it is strictly increasing and represents U≤U′. If its additive sum represented product accessibility, the states [(1,4)] and [(2,2)] would have equal summed entropy log⁡1+log⁡4=2log⁡2=log⁡4, 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