Derivation
Where the settle’s guarantees come from: the closed form the iteration solves for, the round count that follows from it, the floating-point budget the stopping rule respects, the proof assistant the statements mirror, and the social science behind the models. The explanation says what each model means; this page shows why the code may claim what it claims.
The Friedkin-Johnsen step as a contraction#
One round is x(t+1) = (I - S) x0 + S W x(t), with W row-stochastic
and S the diagonal matrix of susceptibilities. Subtracting two
trajectories cancels the anchor term, and a row-stochastic matrix never
stretches the sup norm, so successive differences shrink by max s_i
per round. The fixed point satisfies (I - S W) x* = (I - S) x0, hence
the closed form x* = (I - S W)^{-1} (I - S) x0, which is invertible
exactly when every voter keeps some anchor. The symbolic check is three
lines: expand (I - S W)^{-1} as the Neumann series, multiply by
(I - S) x0, and recover the iteration’s limit term by term. In SymPy:
import sympy as sp
n = 3
S = sp.diag(*sp.symbols('s0:3'))
W = sp.MatrixSymbol('W', n, n)
I = sp.Identity(n)
x0 = sp.MatrixSymbol('x0', n, 1)
xstar = (I - S*W).as_explicit().inv() * (I - S).as_explicit() * x0.as_explicit()
# series: x(t+1) - x(t) = (S W)^t (x(1) - x(0)), so ||.||_inf <= max(s)^t.
The code carries the two consequences as functions, not comments:
fj_contraction_bound returns max s_i over the voters, and
fj_rounds_to_tol turns it into a round count: the first step moves no
row by more than the bound (both W x(0) and x(0) are rows of
distributions, so their sup distance is at most one), and successive
differences shrink by the bound, so err(t) < boundt= and
t > ln(tol)/ln(bound)= suffices, plus the first step. A test holds an
anchored settle to the predicted count. When the bound is not a
contraction (s_i = 1 everywhere, pure DeGroot), the function returns
nothing: there is no round count to guarantee, convergence is asymptotic
under Berger’s closed-group conditions
(doi:10.1080/01621459.1981.10477662), and the iteration budget
(max_iter) decides. That None is the honest boundary between what is
proved and what is budgeted. ljos-consensus rounds prints the bound
and the count for a named panel, or the null count with its reason.
The floating-point budget#
A contraction in the reals still stops in floating point, and the
stopping rule must say what it stopped on. The iteration reports
settled: false when the budget runs out rather than averaging a split,
and the energy engine (fj-energy) reports the largest component of the
energy’s gradient at the point returned as residual: zero when an
engine does not measure it. The settled test there is the tolerance
asked, scaled by the square root of the number of voters so a wide panel
is not held to a tighter bar per voter than a small one, or the floor
floating point sets, whichever is larger: once the decrease a step could
buy, of the order of the squared gradient, is below the energy’s own
rounding, no line search can accept a step, and the point is as settled
as the arithmetic allows. That floor is the part of the routine a
Sollya-style error analysis justifies: bound the rounding of the energy
and its gradient, and the stopping test falls out. The interval half is
done: scripts/verify_fj.py replays an anchored settle in
outward-rounded intervals (mpmath.iv, the same rounding discipline
Sollya certifies) and shows the float stop and the closed form both lie
in an enclosure 5e-16 wide, so stopping at tol 1e-9 is far above the
rounding floor. What remains open is the certificate for the compiled
Rust evaluation order rather than the script’s: a Sollya proof over the
emitted floating-point operations. Until then the claim is the
enclosure, not the certificate, and the page says so.
The Lean correspondence#
The statements above mirror lemmas available in Lean’s Mathlib, and new proof work should target them rather than restating them:
On this page |
In Mathlib |
|---|---|
|
|
the sup norm never grows under a stochastic row |
operator-norm lemmas for stochastic matrices |
the anchored map is a contraction with factor |
the Banach fixed-point theorem ( |
the Neumann series gives the closed form |
|
EigenTrust standing is the principal eigenvector pulled toward pre-trust |
Perron-Frobenius for nonnegative matrices |
Nothing here is a verified proof yet: the table is a map of where the
proofs would land, so a future formalisation starts from named lemmas
rather than from prose. The code’s part is to keep the statements
proof-shaped: pure functions over explicit matrices, bounds returned as
values, and the unproved case (None) distinguished from the proved one.
Reproducing the numbers#
The calibration table on the explanation page regenerates from
examples/synthetic_voters.rs: voters with accuracies drawn uniformly
between 0.35 and 0.95 answer two-way questions under each rule, twenty
seeds, four hundred questions each. The contraction test runs with the
unit tests: cargo test contraction holds the anchored settle inside
the round count the bound predicts. The full derivation is checked
outside Rust too: python3 scripts/verify_fj.py (SymPy; pip install sympy) verifies the exact rational fixed point, the Neumann-series
limit, the per-round contraction, the round-count prediction, and the
shipped ljos-consensus binary’s agreement with the closed form over
eight random panels, and .github/workflows/derive.yml runs it with
cargo test when the library, the derivation, or the script changes.