A proposed stationary density π and generator L must satisfy L*π=0. Detailed balance is stronger. The same density can support no current or a nonzero stationary circulation.
dX = (−X + ω JX)dt + √(2ε)dW J = [[0, −1], [1, 0]] π(x) ∝ exp[−|x|²/(2ε)] j(x) = ω Jx π(x)
For ε>0 this two-dimensional process has the same Gaussian invariant density for every ω. At ω≠0 the probability current is nonzero. A quasipotential matching the exponent therefore does not prove reversibility. With √ε instead of √(2ε), the variance changes by a factor of two.
Rey-Bellet & Spiliopoulos: irreversible dynamics with a Gibbs measure.
For fixed conditions C and target f, inspect the set {f(x): x∈Ω_C}, after removing physical duplicates. One target value is closure for f; several isolated solutions need not give one value. Minimising a cost introduces an additional selection rule. A saturated bound must be attainable, and every equality case must be retained.
The marginalisation identity below preserves the chosen visible weights with the measure included. It does not restore discarded correlations or determine reduced dynamics. For fixed finite N the minimum limit holds. If N grows while ε shrinks, multiplicity can compete with cost; the order of limits must be specified.
In the exponential theorem below, λ>0 defines ε=1/λ, giving w(S)=exp(−S/ε). The scale has the same units as S. For a nonempty finite set of N real costs with counting measure, let m=minᵢ Sᵢ:
Fε = −ε log Σᵢ exp(−Sᵢ/ε) m − ε log N ≤ Fε ≤ m lim ε→0⁺ Fε = m
Proof: factor out exp(−m/ε); the remaining sum lies between 1 and N. At finite ε>0 every finite cost has positive weight. Tied minima leave more than one winner in the limit. Nonuniform measures and continuous spaces require separate conditions; the Laplace analysis below also shows how the width of minima matters.
Take visible x, hidden y, a fixed product reference measure and ε>0. Where the integral is positive and finite, define:
S_eff(x) = −ε log ∫ exp(−S(x,y)/ε) dν_y(y)
Then exp(−S_eff/ε) is exactly the marginal weight of x. Using the same normalisation preserves expectations of functions of x. Correlations with y are not thereby recovered. The result depends on the measure and need not retain the simple form of S. This static identity alone supplies no dynamics.
Model input Choose x₁,…,x₄,y∈{−1,+1} and S=4|J|−Jy(x₁+x₂+x₃+x₄). The constant makes S nonnegative. Each original interaction couples two variables.
S_eff(x) = 4|J| − ε log[2 cosh(JΣᵢxᵢ/ε)]
For small |J|/ε the expansion contains a four-way term with coefficient 2J⁴/ε³ multiplying x₁x₂x₃x₄, alongside constant and pair terms. This follows from log cosh z=z²/2−z⁴/12+O(z⁶). Marginalising a hidden variable can therefore produce higher couplings without inserting them at the start.
On a finite space, with pᵢ*=exp(−Sᵢ/ε)/Z and any probability distribution p:
F[p] = Σᵢ pᵢ Sᵢ + ε Σᵢ pᵢ log pᵢ F[p] − (−ε log Z) = ε D_KL(p || p*) ≥ 0
Use 0 log 0=0. This is an algebraic identity plus nonnegativity of relative entropy. Identification with thermodynamic free energy requires S to be energy and ε=k_BT in an appropriate equilibrium model. It does not derive thermodynamics from the philosophical core alone.
The original Lean proofs were rebuilt on 16 September 2026: the exponential theorem and four results about derivatives and symmetry pass. This page restores their precise conclusions, written proofs and independently calculated examples.
Choose a configuration space C, composition ⊕ and nonnegative resistance S. For admissible independent composition, assume S(A⊕B)=S(A)+S(B). Separately assume that weight depends only on S: w=φ∘S. These are model choices.
Theorem. If φ:[0,∞)→(0,1] satisfies φ(s+t)=φ(s)φ(t) for every s,t≥0, there is λ≥0 such that:
φ(s) = exp(−λs), s ≥ 0
Positivity and composition already imply φ(0)=1. Continuity need not be assumed. Strictly decreasing weight additionally requires φ(s₀)<1 somewhere; otherwise λ=0 is allowed.
Formal source: Kern.lean · new compilation log. The original Lean source already restricted the claim to s≥0. The old website's statement on all of ℝ did not. Correcting that web statement did not refute the formal proof.
Take C=[0,∞)² with addition, S(x,y)=x and w(x,y)=e−y. S is additive and w multiplicative, yet configurations with equal S can have different weights. Factorisation through S does not follow from those properties alone. Composition must also justify the functional equation on the full stated domain.
Choose a reference measure ν. For ε>0 and measurable S define:
Zε = ∫ exp(−S(C)/ε) dν(C) με(B) = Zε⁻¹ ∫_B exp(−S(C)/ε) dν(C)
This is a probability measure when 0<Zε<∞. In a discrete space, integration becomes summation. A continuous density is not the probability of a single point. The choice of ν helps determine the total weight of regions.
S(x)=½ln(1+x²) is smooth, nonnegative and coercive: S(x)→∞ as |x|→∞. It has a unique nondegenerate minimum. Nevertheless, at ε=1:
Z₁ = ∫ℝ 1/√(1+x²) dx = ∞
Growth to infinity alone is insufficient. It must also compensate for the volume of available configurations.
For one chosen prefix-free description per discrete candidate, with bit length Lᵢ, Kraft gives Σ2−Lᵢ≤1. If Aᵢ≥B and 0<dᵢ≤D, then for ε>0:
0 < Σᵢ dᵢ exp(−Aᵢ/ε) 2^(−Lᵢ) ≤ D exp(−B/ε) < ∞
For example, the words 0, 10, 110, … have lengths 1,2,3,… and weights summing to 1. But if dᵢ=2Lᵢ and Aᵢ=0, every term is 1 and the sum diverges. Bounding the additional factors matters.
The Bayesian accounting also survives. For prior π(M)∝2−L(M) and positive likelihood ℒ(D|M):
−ln P(M|D) = (ln 2)L(M) − ln ℒ(D|M) + constant(D)
This combines description costs and data costs within the chosen prior. The coefficient ln 2 converts bits to natural logarithms; it does not prove that nature chooses this prior. Universal Kolmogorov complexity K also depends on the description language up to an additive constant.
Source for coding conditions: Péter Gács, algorithmic information theory.
Let S and γ be differentiable, with γ(0)=x and S(γ(t))=S(x). The chain rule gives:
dSₓ(γ′(0)) = 0
In an inner product space admitting a gradient, this means ∇S⊥γ′(0). An invertible continuous linear transformation U preserving S maps critical points to critical points. If a curve lies entirely in the critical set and dS is differentiable at x, then:
Hess Sₓ(γ′(0), ·) = 0
These statements and their combination for a family U(t) are the four reverified results. The null direction has no Hessian cross terms with other directions. This does not establish a unique decomposition of the complete resistance as S=A+K+I.
Take S(x,y,z)=(x²+y²−1)²+z². Rotations in the xy-plane preserve S. Their tangent direction is ξ=(−y,x,0). Direct differentiation gives ∇S·ξ=0 everywhere. At the critical point (1,0,0):
∇S = 0, Hess S = diag(8, 0, 2)
The orbit direction (0,1,0) is a null mode. A separate counterexample shows the limit: S=y²+yz+z² is invariant under x-translations but has mixed yz-derivative 1. Symmetry does not decouple arbitrary remaining directions. At a critical point, span(∇S) is also the zero subspace, not a nontrivial time direction.
Orthogonaliteit.lean · new compilation log. The formal statements were checked; broader physical interpretations in historical source comments do not follow automatically.
On ℝⁿ, let S be C² with finitely many isolated global minima x₁,…,xₘ of equal value s*. Assume positive definite Hessians Hᵢ, a positive continuous density r, compact sublevel sets and Zε₀<∞ for some ε₀>0. Laplace asymptotics as ε↓0 gives:
Zε ~ e^(−s*/ε) (2πε)^(n/2) Σᵢ r(xᵢ)/√det Hᵢ pᵢ → [r(xᵢ)/√det Hᵢ] / Σⱼ[r(xⱼ)/√det Hⱼ]
pᵢ is the mass of a fixed small neighbourhood of minimum i. Quadratic approximation supplies the determinant factor. Integrability and compactness control the contribution outside those neighbourhoods. Null modes and continuous sets of minima require a different formula.
S(x)=(x²−1)²(x²+x+1), with r=1, has global minima at −1 and +1. Their Hessians are 8 and 24. The limiting left mass is therefore √3/(1+√3)=0.6339745962. Independent numerical integration gives:
| ε | Mass at x<0 |
|---|---|
| 0.1 | 0.6407736507 |
| 0.02 | 0.6353885314 |
| 0.005 | 0.6343259874 |
| 0.001 | 0.6340447322 |
A broader minimum can carry greater total weight even when the two lowest points have equal resistance.
Let S=aA+bK+cI with a,b,c>0. If candidate X has no greater cost than Y in all three components, and strictly lower cost in at least one, then S(X)<S(Y) for every choice of positive weights.
ΔA ≤ 0, ΔK ≤ 0, ΔI ≤ 0, at least one strict ⇒ aΔA + bΔK + cΔI < 0
This is Pareto dominance. When candidates trade costs against each other, the winner can depend on a,b,c. The old general robustness claim must be restricted to this precise case.
Assume complex amplitudes with quadratic norm, weight depending only on |c|, multiplicative weights and additive weights for orthogonal branches. For positive multiplicative f:(0,1]→(0,1], apply the core theorem to φ(t)=f(e−t):
f(x) = x^p, p ≥ 0
An allowed split c→(c/√2,c/√2) preserves the quadratic norm. If it also preserves total weight, then:
2 (|c|/√2)^p = |c|^p 2^(1−p/2) = 1 ⇒ p = 2
Thus Born weights |c|² follow under these assumptions. Amplitudes, orthogonality, norm and weight conservation are inputs. This does not derive all of quantum theory from Effortless Effect alone.
If a measurable invertible T preserves both S and ν, it also preserves μ, by change of variables in the integral. Invariance of S alone is insufficient: the reference measure must be preserved as well.
A symmetric distribution need not produce symmetric individual outcomes. Equal probability on −1 and +1 is invariant under sign reversal, but neither outcome is. A physical mechanism for spontaneous symmetry breaking requires further dynamics or limits.
These are substantive building blocks. The configuration space, resistance, measure and physical interpretation still need justification. Formal verification establishes the stated implications, not that the world satisfies their assumptions.
Download the verification bundle · Reproduction and scope
Continue with K3, χ=24 and spectral geometry →Results and limits of the verification →
v0.26 · 28 September 2026