Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6-luna)
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.

Ising influence bounded by hyperbolic tangent

Statement

Let d≥1, let spins be si∈{−1,+1}, let hi∈R, and let Jij=Jji∈R with Jii=0 and Jij=0 whenever ∥i−j∥∞>R for some finite integer R. No translation invariance is assumed. For finite Λ⊂Zd and exterior η∈{−1,+1}Λc, define s^i=si on Λ and s^i=ηi outside, and use EΛ(sΛ∣η)=−∑{i,j}:{i,j}∩Λ≠∅Jijs^is^j−∑i∈Λhisi, where the pair sum is over unordered distinct pairs and is finite by the range assumption. For site i and exterior spins η∈{−1,+1}Zd∖{i}, the one-site law is explicitly γi(s∣η)=exp⁡ ⁣(β[his+∑k≠iJiksηk])∑u∈{−1,+1}exp⁡ ⁣(β[hiu+∑k≠iJikuηk]),s∈{−1,+1}; the sums are finite by the range condition. For i≠j, define cij:=sup⁡η,η′: ηk=ηk′ (k≠j)12∑s∈{−1,+1}∣γi(s∣η)−γi(s∣η′)∣,cii:=0. Then cij=0 if Jij=0, and otherwise cij≤tanh⁡(β∣Jij∣). In particular, sup⁡i∑jtanh⁡(β∣Jij∣)<1 is a sufficient Dobrushin row-sum bound for every bounded field profile (hi).

Facts & Assumptions

Given: The finite-range Ising pair couplings, field profile, conditional energy, one-site Gibbs laws, and β>0 specified in the Statement.

[F1]

The hyperbolic functions are defined by sinh⁡x=(ex−e−x)/2, cosh⁡x=(ex+e−x)/2, and tanh⁡x=sinh⁡x/cosh⁡x; their addition and product identities include tanh⁡(x+b)−tanh⁡(x−b)=sinh⁡(2b)/(cosh⁡(x+b)cosh⁡(x−b)) and cosh⁡(x+b)cosh⁡(x−b)=(cosh⁡(2x)+cosh⁡(2b))/2 (The six hyperbolic functions and their natural domains, Addition formulas, identities, parity, and derivatives of the hyperbolic functions).

Proof

1.1givenF1algebra

Fix i and all boundary spins except j. Write x=β(hi+∑k∉{i,j}Jikηk) and b=βJij; these sums are finite by the range condition. Direct normalization of the two weights gives γi(+1∣η)=[1+tanh⁡(x+b)]/2 and γi(+1∣η′)=[1+tanh⁡(x−b)]/2.

2.1step 1.1F1algebra

For Bernoulli laws the half-total-variation distance equals the absolute difference of the probabilities of +1. By [F1], cosh⁡(x+b)cosh⁡(x−b)=(cosh⁡(2x)+cosh⁡(2b))/2≥cosh⁡2b, so their difference is at most ∣sinh⁡(2b)∣/(2cosh⁡2b)=tanh⁡∣b∣. If Jij=0, the conditional weights are identical and cij=0.

3.1F1step 2.1∎

Summing the bound in step 2.1 over the finite interaction neighborhood proves the stated sufficient row-sum criterion; the supremum over i is the Dobrushin constant used by the uniqueness theorem.

Depends on

Dependency tree · 2 levels

Sources