Alphabeta Math
ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generatedverified 2026-10-15 (gpt-6-luna, gpt-6.1-sol, and delegated Codex review/repair agents; see completed run evidence)
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.

Logarithmic contact model with coherent joins

Example

Let I be a finite nonempty set of primitive labels, choose ci,ri,ui∗,vi∗>0 and bi∈R for each i∈I, and use the positive state domain Γi=(0,∞)2 with coordinates (U,V). Close these tags under positive scaling, finite separated products, and finite thermal joins, retaining all constituent tags. The reference scales ui∗,vi∗ have the same respective units as U,V; write ln⁡ for the natural logarithm log⁡ of The natural logarithm as the inverse of the exponential function. Thus every logarithm argument is dimensionless. For a unit amount set σi(U,V)=ciln⁡(U/ui∗)+riln⁡(V/vi∗)+bi. For any amount t>0, define on the scaled type ti

σti(U,V)=tciln⁡ ⁣(Utui∗)+triln⁡ ⁣(Vtvi∗)+tbi.

For a separated finite product, add component entropies. For a thermal join of a finite nonempty list of components indexed j=1,…,m, write αj=tjcij, βj=tjrij, dj=tjuij∗, ej=tjvij∗, and C=∑jαj>0. Define its entropy at total energy U>0 and positive work coordinates Vj by

σJ(U,V1,…,Vm)=∑j=1mαjln⁡ ⁣(αjUCdj)+∑j=1mβjln⁡ ⁣(Vjej)+∑j=1mtjbij.

Give each primitive generator its unit amount vector; scaled and joined types retain all primitive amounts, and let wT be their sum, with wtT=twT and joined weight equal to the sum of component weights. Use the represented state JT(x)=wTe(T,x) from Forward-sector hypotheses for a simple state domain. For a finite encoded map c, define its entropy by the finite sum σ(c)=∑(T,x)c(T,x)σT(x)/wT, omitting zero terms. Its aggregate composition is the corresponding amount-vector sum from that supplier. Thus σ(JT(x))=σT(x), while a raw unit point mass has entropy σT(x)/wT. Scaled and joined raw tags are distinct; the displayed formulas make their declared preparation transport entropy-preserving.

On every finite compound of these closed tagged types, define accessibility by nondecrease of this entropy across states of the same composition, including the separated and joined representations of a contact. This is a mathematical consistency model; it is not an observed gas experiment or a universal thermodynamic assertion.

Facts & Assumptions

Given: The positive constants, positive reference scales, finite tagged family, and the entropy and accessibility definitions in the Example.

[F1]

Forward-sector hypotheses for a simple state domain: A1–A7 and S1–S3 specify the relation and simple-domain geometry to be verified.

[F2]

Thermal joins and conditional contact hypotheses: T1–T5 and C1 specify the contact and coherence conditions to be verified.

[F3]

The natural logarithm as the inverse of the exponential function and Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm: log⁡:(0,∞)→R is the natural logarithm, is strictly increasing, and obeys the product and quotient laws.

[F4]

The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t: log⁡ is differentiable on (0,∞) with derivative 1/x.

[F5]

The weighted arithmetic-geometric mean inequality for real weights: for positive rj and positive weights pj summing to one, ∏jrjpj≤∑jpjrj.

[F6]

The two-point convexity inequality for the exponential function: the exponential is strictly convex between distinct real inputs; since log⁡ is its increasing inverse, log⁡ is strictly concave on positive reals.

Verification

Given: The formulas and definitions in the Example, with all ci,ri,ui∗,vi∗>0.

1.1F2F3F5F6givenalgebra

Fix a finite list of scaled components with amounts tj>0 and labels ij∈I. Write αj=tjcij, βj=tjrij, dj=tjuij∗, and ej=tjvij∗, with C=∑jαj>0. For a split of total energy U>0 into positive Uj with ∑jUj=U, put pj=αj/C and rj=Uj/αj. Then ∑jpjrj=U/C. By [F5] and monotonicity of log⁡ from [F3], ∑jαjlog⁡(Uj/dj)=∑jαjlog⁡(αj/dj)+C∑jpjlog⁡rj≤∑jαjlog⁡(αj/dj)+Clog⁡(U/C)=∑jαjlog⁡(αjU/(Cdj)). Equality in the finite weighted Jensen step occurs only when all rj are equal: [F6] gives strict concavity for any unequal pair with positive weights, and grouping terms applies this two-point strict inequality inductively. Since the weighted average is U/C, equality requires rj=U/C, or Uj=αjU/C. This allocation is positive and feasible, so the maximum is attained uniquely. The work-coordinate terms do not depend on the energy split, giving exactly the displayed join entropy. Grouping nested joins is the same finite maximization over all Uj, so the formula is associative under grouping and permutation.

1.2F1F2givenalgebra

On each fixed composition, define accessibility by nondecrease of the displayed entropy. Reflexivity and transitivity follow from the real order. A common spectator adds the same entropy to both sides; positive scaling multiplies each entropy comparison by a positive factor. For a simple scaled type, replacing (U,V,t) by (sU,sV,st) leaves both log ratios unchanged and multiplies their coefficients and constant term by s. In a join, scaling every amount, energy, and work coordinate by s likewise leaves αjU/(Cdj) and Vj/ej unchanged and scales all coefficients and additive constants by s. Extensivity gives σ(s+t)i((s+t)x)=σsi(sx)+σti(tx), proving reversible splitting. For the stability condition, if σ(A)+ϵnσ(Z0)≤σ(B)+ϵnσ(Z1) for all n and ϵn↓0, the four entropies are finite. Moreover, the premise includes equality of aggregate composition: ν(A)−ν(B)=ϵn(ν(Z1)−ν(Z0)) for every n. Choose two different values of ϵn, which exist because the positive sequence tends to zero; subtracting these equalities gives ν(Z1)=ν(Z0), and then ν(A)=ν(B). Taking limits in the entropy inequality gives σ(A)≤σ(B), now with the same-composition condition required by the accessibility definition. This verifies the stated accessibility and stability hypotheses on the declared comparison domains.

1.3F1F3F6givenalgebra

Every simple scaled or finite joined type has entropy of the form f(U,V)=Clog⁡U+∑jβjlog⁡Vj+K, where C,βj>0 and K is constant on that type. Its chart is a nonempty open convex positive orthant. Strict concavity of log⁡ from [F6] gives coordinatewise concavity of f, hence tf(x)+(1−t)f(y)≤f(tx+(1−t)y) for 0<t<1. The two encoded states have the same composition, so the entropy-defined order proves the convex-combination access axiom. Increasing U at fixed work tuple strictly increases f, providing a strict successor and S1 on every such type.

2.1F1F3F4step 1.3givenalgebra

For the type in step 1.3, the forward sector through (U0,V0) is the superlevel set of f, with boundary graph U=U0∏j(Vj/V0,j)−βj/C over the positive work orthant. Differentiation by [F4] gives graph slopes −βjU/(CVj), so put Pj(U,V)=βjU/(CVj). Concavity gives f(y)≤f(x)+Df(x)⋅(y−x); hence f(y)≥f(x) implies Df(x)⋅(y−x)≥0, proving that the tangent plane supports the sector. The energy derivative C/U is nonzero. Any supporting normal annihilates every boundary tangent vector, by testing a graph curve with that tangent for both parameter signs. The tangent space has codimension one, so this supporting plane is unique. On a sufficiently small closed coordinate box inside the positive orthant, the partial derivatives of each rational map Pj are bounded; varying coordinates successively bounds ∥P(y)−P(z)∥ by a fixed multiple of ∥y−z∥. Thus P is locally Lipschitz. A straight segment between distinct work tuples stays in the positive orthant and lifts injectively and continuously to the graph. This proves S2–S3 for simple scaled types and all finite joins.

2.2F1F2F3F5F6step 1.1step 1.2given

Step 1.1 shows that joined entropy is the maximum of separated entropy at its total energy and work tuple. Thus every split compares upward to the join, and the maximizing split compares back, proving T1 and the existence clause of T2. For each simple scaled or finite joined type T let CT>0 be its coefficient of log⁡U and define θT(U,V):=U/CT. For a pair of such types T,R, maximizing over their two energies gives UT/CT=UR/CR, by the same strict-concavity argument of step 1.1. The split is reversible with its join exactly when its entropy reaches this maximum, so x∼Ty if and only if θT(x)=θR(y). Equality of real labels is transitive, proving T3. Positive scaling sends (U,CT) to (sU,sCT) and preserves θ; therefore an equal-state split into any positive scaled copies has equal labels and is reversible with its join, completing T2.

3.1F1F2F3step 1.3step 2.2givenchoose

Fix a state x=(U,V) in any simple scaled or finite joined type T, and any positive work tuple W in any second such type R. Choose Y=(CRU/CT,W). It belongs to the second chart and has θR(Y)=θT(x), so step 2.2 gives x∼TY, proving every ordered-pair instance of T5. For T4 keep U fixed and replace one positive work coordinate Vj by Vj/2 and 2Vj, leaving the others fixed. Its positive coefficient βj makes the resulting states x0≺≺x≺≺x1, while their equal energy gives the same θ and hence x0∼Tx1 by step 2.2. Every type has at least one work coordinate, so this construction applies throughout the join-closed family.

4.1F1F2step 1.1step 2.2∎

If states of any two simple types T,R are thermally equivalent, step 2.2 gives their common label θ and energies UT=CTθ, UR=CRθ. Their join has coefficient CT+CR and energy UT+UR, so its label is also θ. It is therefore thermally equivalent to each constituent by step 2.2, proving C1. Finite grouping preserves this identity by step 1.1. Every logarithm argument is a ratio of like positive quantities, hence dimensionless. The label θ is mathematical; this example asserts no empirical temperature law.

Depends on

Dependency tree · 2 levels

Sources