# Conformal universality for weakly interacting and random-bond Ising models

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [Buffered comparison and stopping-band resolution in critical Ising](../../preprints/Buffered-comparison-and-stopping-band-resolution-in-critical-Ising-September-23-2026/paper.pdf)

## Scope

The formalized result compares conditional Ising probabilities on finite graphs when two boundary mixtures differ but a common set of spins is pinned. If $q_0$ is the associated zero-field Fortuin–Kasteleyn connection probability after deleting the pinned vertices, the likelihood ratio lies between $\exp(-4\mathrm{artanh}\,q_0)$ and $\exp(4\mathrm{artanh}\,q_0)$. The statement allows arbitrary external fields and arbitrary probability mixtures satisfying the stated disjointness conditions. The paper's finite stopping-band approximation theorem is outside this selected statement.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Finite-graph buffered Ising likelihood comparison | [BufferedIsing.lean](../ComparatorChallenges/BufferedIsing.lean) |