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.24 · 16 September 2026