Hypercubic lattice graphs

AbbreviationSite of the hypercubic lattice#✓fully proved

A site of the d-dimensional hypercubic lattice ℤ^d, encoded as an integer vector.

abbrev Site (d : ℕ) : Type := Fin d → ℤ

Used by 1,200

Used byBase point of the exterior of a box · Box \((-n, n)^d\) in the hypercubic lattice · Size of the vertex boundary of the box \((-n, n)^d\) · Box \((-n, n)^d\) as a finite set of sites · Number of nearest-neighbour pairs inside the box \((-n, n)^d\) · Nearest-neighbour pairs inside the box \((-n, n)^d\) · Box sites with a forward neighbour in the box · Vertex boundary of the box \((-n, n)^d\) as a finite set · Nearest neighbours of a lattice site · Neighbour of a site in a coordinate direction · Edge boundary of a set of sites · Exterior of a box in \(\mathbb{Z}^d\) · Every finite set of sites lies in a box · Hypercubic lattice \(\mathbb{Z}^d\) · Square lattice is connected · \(\ell^1\) distance on \(\mathbb{Z}^d\) · Nearest neighbours in \(\mathbb{Z}^d\) · First index where a walk reaches a coordinate value · Changing one coordinate stays in the same component · Increasing one coordinate stays in the same component · Setting a set of coordinates of a lattice site · Shift of a site along a coordinate · Complement of a finite set in \(\mathbb{Z}^d\) has one infinite component · Inner vertex boundary of a box · Total turning of a boundary orbit is bounded by its length · Boundary indicator of an edge · Lattice connectivity in the complement implies king connectivity · King-move graph on the complement of a set · Cumulative turn along a boundary-tracing orbit · Dart of the square lattice · Successor of a boundary dart · Next boundary dart direction is rotated by the turn · Successor map on boundary darts · Minimal period of a boundary dart · Closed walk around a boundary dart orbit · Successor graph on boundary darts · Direction of a lattice dart · Dart direction after k steps is rotated by the cumulative turn · Base boundary dart of the domino · Domino as a two-site set · Face loop around the domino · Lattice darts agree with graph darts of the square lattice · Dart correspondence respects reversal · Boundary degree of a unit face · Lower left corner of the unit face at \((a, b)\) · Upper left corner of the unit face at \((a, b)\) · Lower right corner of the unit face at \((a, b)\) · Upper right corner of the unit face at \((a, b)\) · Total turning over the minimal period is divisible by four · Total turning of a closed orbit segment is divisible by four · Boundary darts with heads in one component share an orbit · Boundary dart of a set of sites · Inner corner of a boundary dart · King adjacency on the square lattice · Number of convex corners in a boundary orbit · Dart from a site in a unit direction · Face loop left of one period of a boundary orbit · Minimal-period orbit loop as a lattice walk · Closure under the diagonal fill rules · Product set of two coordinate sets in the plane · Star hull of a set of lattice sites · Membership in the star hull · Sublevel set of a separable function · Diagonal touch at a face · Set with no diagonal touches · No diagonal touch along a boundary orbit · Lower left corner of a face \(f\) · Upper left corner of a face \(f\) · Lower right corner of a face \(f\) · Upper right corner of a face \(f\) · King-saturated set · Boundary orbit face loop as a lattice walk · No-pinch condition for a boundary orbit · Orbit saturation by heads connected in the complement · Boundary orbits spread along king moves · Boundary orbit with a full revolution has length at least four · Site reached by a boundary orbit · Orbit saturation at reached sites · Walk along the first iterates of a boundary dart · Reversal of a lattice dart · Number of reflex corners in a boundary orbit · Rotation of \(\mathbb{Z}^2\) by a number of quarter turns · Quarter-turn rotations form an action of \(\mathbb{Z}/4\) · Nontrivial quarter-turn rotations fix no lattice direction · Four quarter turns of the square lattice are the identity · Two darts in the same boundary orbit · Corner balance of a simple lattice polygon · Number of straight steps in a boundary orbit · Total signed turning along a boundary orbit · Quarter turn between consecutive boundary darts modulo 4 · Signed quarter turn between consecutive boundary darts · Boundary orbit making exactly one full revolution · Base boundary dart of the unit cell · Unit cell as a one-site set · Face loop around the unit cell · \(\ell^1\) norm of a vector in \(\mathbb{Z}^2\) · Each face visited once per period by a boundary orbit · Four unit vectors of \(\mathbb{Z}^2\) · Local turn of a boundary orbit at a face · Faces visited by a boundary orbit in one period · \(p_c(\mathbb{Z}^2) < 1\) under a no-pinch hypothesis · Visit times of a boundary orbit to a face · Boundary edge of a set · Bounded regions are the components other than the outer one · Set of sites is the inside of a closed lattice walk · Four unit faces at a lattice site · Number of boundary crossings of a walk · Inside and outside of a closed walk are connected · Box exterior embeds in the region graph · Face-boundary graph of a set · Lattice off a closed walk · Jordan region property off a closed walk · Flood fill avoiding a set of sites · Lattice walk avoiding a set, lifted to the reduced lattice · Square lattice with a set of vertices removed · Geometric count of bounded regions · Image of a planar lattice subgraph in the square lattice · Disconnected sites are joined in the lattice minus a bridged graph · Corners of the unit square in cyclic order · Square lattice minus the edges of a graph · Unit square as a planar lattice subgraph · Quarter-turn isomorphism onto the region graph · Bounded regions of a planar lattice subgraph · Bounded regions indexed by the cycle rank · Two diagonally touching sites · Lattice points around the L-shaped tromino · 8-cycle around the L-tromino as a planar lattice subgraph · Jordan region of the cut lattice · Separating side between inside and outside sites · Vertices of two unit squares sharing a corner · Two corner-sharing unit squares as a planar lattice subgraph · Even-degree subgraphs have as many regions as their face count · Peeling a cycle from an even-degree subgraph · Half-plane below a row · Open vertical crossings separate the sides of a rectangle · Horizontal lattice path rightward · Inside of a closed walk by the even-odd rule · Quadrant below and left of a site · Ray-crossing count of a walk · Ray edges left of a site · Return path around a rectangle · Vertical lattice path upward · Wall-crossing count of a walk · Wall edges below a site · Twelve boundary edges of a 3 by 3 rectangle · Boundary of a 3 by 3 rectangle as a graph · Cut set of a face coloring · Bounded faces of a finite lattice graph are counted by its cycle rank · Lattice graph spanned by an edge set · Pushforward of a subgraph into the square lattice · Pushed-forward subgraphs are locally finite · Interior region of the unit square · Outer face region of a planar lattice subgraph · Whitney cut-cycle duality for a planar lattice subgraph · Exterior of a box maps into the face-region graph · Unit square corners with a pendant site · Unit square with a pendant edge as a planar lattice subgraph · Number of face regions of a subgraph's image · Corners of two distant unit squares · Two disjoint unit squares as a planar lattice subgraph · Nine sites of a 3 by 3 grid · 3 by 3 grid as a planar lattice subgraph · Keep-reconnect residue for finite graphs · Horizontal axis with one edge removed · Adjacency relation of the cut horizontal axis · Region step property for even-degree subgraphs · Veblen step property for even-degree subgraphs · Square lattice with the boundary edges of a set removed · Square lattice with a closed walk's vertices removed · Component off a closed walk containing a seed · Radius of a box containing a planar lattice subgraph · Outer region of the rotated region graph · Planar lattice subgraph of the square lattice · Rotated region graph of a lattice subgraph · Boundary darts of a component off a closed walk · Facial orbit of a boundary dart · Facial orbits cover the components of the complement · Primal edge shared by adjacent faces · Edges of the grid \((-n, n)^2\) · Euler's formula for the grid graph \((-n, n)^2\) · Square lattice induced on the box \((-n, n)^2\) · Vertices of the grid \((-n, n)^2\) · Horizontal edges of the grid \((-n, n)^2\) · Vertical edges of the grid \((-n, n)^2\) · Face-graph adjacency as absence of a walk step between cells · Ray-parity interior equals the bounded face components · Vertex of a walk as a lattice site · Vertices of a simple walk are distinct sites · Consecutive walk vertices are adjacent in the square lattice · Lattice Jordan curve theorem for simple closed walks · Simple closed walk as an embedded cycle graph · Unit cell as a face of the square lattice · Cells of the inner face component · The inner component has finitely many cells · Neighbours in the image graph are walk predecessor and successor · Inner component of the face graph · The inner face component is finite · Face below-left of the inside top corner · Membership in the bounded face · A face far outside the walk has ray parity zero · Face-adjacent cells have the same ray parity · Horizontally face-adjacent cells have the same ray parity · Vertically face-adjacent cells have the same ray parity · Ray parity is constant on face-graph components · Each walk step is an edge of the image graph · Face graph of a closed walk · Vertices of a walk's image graph are adjacent only to walk neighbours · Consecutive left cells on a straight step are face-adjacent · Consecutive left cells have the same ray parity · Left and right cells of a step share that step · Lattice Jordan curve theorem, even-odd form · Bounded face of a simple closed walk has no pinch points · Face-graph component of an interior cell · Three walk edges cannot meet at a vertex · No right cell lies in the bounded face · A side between interior and exterior cells is a walk edge · Cells on either side of a step lie in different faces · Number of cells is at most the nullity of the skeleton · Adjacent cells have connected lower-left corners · 1-skeleton of a cell complex as a planar subgraph · Bounded face formed by a cell · Distinct cells form distinct bounded faces · Face component containing a cell · The face component of a cell is bounded · The face of a cell is enclosed on all four sides · The face of a cell is alone in its component · Cell complex edges lie in the embedded skeleton · Shared side of a cell and an adjacent face is an edge · Interior cells have connected lower-left corners · Hopf's Umlaufsatz · Quarter-turn rotation of unordered site pairs · Bijection between primal and dual edges · Rotated dual configuration · Dual square lattice · Quarter-turn rotation as a permutation · Quarter-turn rotation of the square lattice · Inverse quarter-turn rotation · Quarter-turn rotation as a lattice automorphism · Identity self-duality of the square lattice · Rotational self-duality of the square lattice · Closed contour as an even-degree edge set · Degree of a site in an edge set · Edge flip relation of an edge set · Number of horizontal contour edges below a height · Horizontal edges below a face in its column · Parity coloring changes across vertical contour edges · Four nearest neighbours of a site · Parity coloring of faces by an edge set · Even-degree image of a planar lattice subgraph · Whitney duality in the bridge direction · Closed face walk around a lattice vertex · Cut-flip count along a walk · Chosen lattice walk between two faces · Even-flip condition on closed lattice walks · Cut coloring separating the ends of a dual edge · Cut flip relation of a lattice graph and a dual edge · Number of flips along a lattice walk · Closed walk around a unit square · Symmetry of a flip relation on lattice edges · Face coloring by parity of flips · Whitney's cut–cycle duality · Face-region graph of a square-lattice subgraph · Face coloring compatible with a subgraph · Cut coloring of a subgraph with an extra dual edge · Number of edge crossings of a face walk · Faithful discrete Jordan statement for the face count · Number of bounded faces of a lattice subgraph · Unit square with its bottom edge removed · Primal edge between two faces lies in a subgraph · Face coloring supported at a single face · Support of the first-exit decomposition events · Horizontal and vertical crossings meet · Open cluster inside the overlap rectangle · Every overlap cluster meets every horizontal crossing · Half-plane left of a column · Walk in an induced open subgraph as a lattice walk · Projection of an induced open subgraph to the lattice · Infimum of the box-crossing probabilities · Set of long-direction box-crossing probabilities · Box-crossing property with a given aspect ratio · Agreement of the two critical probabilities · Open cluster of the origin · Event that the origin's cluster is infinite · Agreement of the two percolation events · Percolation probability as an extended real · Translate of a bond configuration · Left–right crossing event of a translated rectangle · Bottom–top crossing event of a translated rectangle · Gluing horizontal crossings through a vertical overlap crossing · Measurability of the overlap connection event · Open connection inside an overlap rectangle · Connection event inside an overlap rectangle · Vertical overlap crossings separate the sides of a rectangle · Vertical overlap crossings meet every horizontal crossing · RSW gluing from side separation · Bottom side of a rectangle at the origin · Open left–right crossing of a rectangle at the origin · Left–right crossing event of a rectangle at the origin · Left side of a rectangle at the origin · Monotonicity of the open subgraph in the plane · Rectangle at the origin in the plane lattice · Right side of a rectangle at the origin · Top side of a rectangle at the origin · Open bottom–top crossing of a rectangle at the origin · Bottom–top crossing event of a rectangle at the origin · Separating set for a lattice rectangle · Open path from the left side of a rectangle to a point · Left half-crossing event · Measurability of the left half-crossing event · Measurability of the right half-crossing event · Open path from a point to the right side of a rectangle · Right half-crossing event · Square annulus in the plane lattice · Existence of an open circuit in an annulus · Open circuit event in an annulus · Open circuit in an annulus centered at the origin · Bottom side of a general lattice rectangle · Left–right crossing event of a box with given aspect ratio · Dual left–right crossing of a rectangle · Dual left–right crossing event · Dual bottom–top crossing of a rectangle · Dual bottom–top crossing event · Open left–right crossing of a general rectangle · Left–right crossing event of a general rectangle · Open circuit lying in an annulus · Left side of a general lattice rectangle · Measurability of connection inside a set · Measurability of the left–right crossing event · Measurability of the bottom–top crossing event · Box-crossing property for a sequence of measures · Uniform two-sided box-crossing property · Integer rectangle in the plane lattice · Right side of a general lattice rectangle · Top side of a general lattice rectangle · Open bottom–top crossing of a general rectangle · Bottom–top crossing event of a general rectangle · Critical bond percolation measure on the square lattice · Russo–Seymour–Welsh theorem · Russo–Seymour–Welsh theorem · Left region of a rectangle cut by an open cluster · Condition that every left-right crossing meets the open cluster · Rectangle lattice with an open cluster removed · Sites reachable from the left side of a rectangle · Anchor sites for dual circuits · Bernoulli box cylinder probability equals its probability on the box · Bernoulli percolation restricted to a box is Bernoulli on the box · Bernoulli percolation restricted to the plane is planar Bernoulli · Event that a dual circuit is closed · Anchored dual cycles of a given length · Step directions of an open walk from the origin · Edges of a lattice path encoded by a step sequence · Positive planar percolation at some \(p < 1\) via the Ising model · Wired \(q = 2\) percolation probability at most the Bernoulli one · Self-avoiding initial segment of an encoded lattice path · Anchored dual-circuit enclosure property · \(p_c(2) < 1\) from anchored dual-circuit enclosure · Positivity of the critical probability (Hammersley's bound) · Plane open connections are open connections in \(\mathbb{Z}^{2+k}\) · Plane embedding on edges · Injectivity of the plane embedding on edges · Percolation in the plane implies percolation in \(\mathbb{Z}^{2+k}\) · Restriction of a configuration to the embedded plane · Plane embedding of \(\mathbb{Z}^2\) into \(\mathbb{Z}^{2+k}\) · Plane embedding preserves and reflects adjacency · First two coordinates of an embedded site are the original ones · Injectivity of the plane embedding · Last \(k\) coordinates of an embedded site vanish · Plane embedding fixes the origin · Primal edges crossed by a dual walk · Monotonicity in \(p\) of the Bernoulli percolation probability · \(\theta_2(p) \le \theta_{2+k}(p)\) for Bernoulli percolation · Vertices of a lattice path encoded by a step sequence · Wired \(q = 2\) origin-to-boundary probability at most Bernoulli · Event that an encoded lattice path is open · Endpoints of a finite edge set · Event of at least two infinite open clusters · Configuration with a finite edge set forced open · Finite energy for opening finite edge sets · Set of infinite open clusters · Measurability of the one-arm event · Configurations with \(k\) infinite clusters, two merged by opening \(F\) · Number of infinite open clusters · Number of infinite clusters is almost surely constant · Zero or one infinite cluster, given ergodicity and \(\mu(N \ge 2) = 0\) · Representative sites of the infinite clusters · Translation of the open subgraph as a graph homomorphism · Inverse translation of the open subgraph · Existence of an anchored dual cycle around the origin cluster · Site on the positive horizontal axis · Boundary edges of a set of sites in \(\mathbb{Z}^2\), as unordered pairs · Canonical contour of a finite origin cluster · Darts of the canonical contour · Canonical contour is longer than the exit index · Closed face walk of the canonical contour · Face walk along the first successors of a boundary dart · Canonical orbit cycle condition · Primal edges of the canonical contour · Event that every edge of the canonical contour is closed · Open cluster maps into the lattice minus its boundary edges · Cut lattice of a set of sites · Dual cycle reaching the left half-plane · Unit face to the left of a dart · Face loop of a boundary orbit in the face-boundary graph · Face walk along a boundary orbit · Undirected lattice edge of a dart · Discrete Jordan separation for finite open clusters · Origin cluster's enclosing contour links the two axis exits · Exit dart of a finite origin cluster · Exit dart on the positive horizontal axis · Left and right exit darts lie in the same boundary orbit · Face below the exit edge · Face above the exit edge · Exit index of a finite origin cluster · Minimal-period face loop of the exit orbit · Face loop of the exit orbit of a finite cluster · Axis site lies outside the origin cluster · Box exterior maps into the lattice minus boundary edges · Inside region of an open cluster in the cut lattice · Site on the negative horizontal axis · Exit dart on the negative horizontal axis · Face below the left exit edge · Face above the left exit edge · Left exit index of a finite cluster · Left exit condition at an axis site · Simplicity of the exit orbit's face walk · Anchored dual cycles give the anchored enclosure property · \(p_c(\mathbb{Z}^2) < 1\) assuming simple exit orbits · \(p_c(\mathbb{Z}^2) < 1\) assuming a canonical orbit cycle · \(p_c(\mathbb{Z}^2) < 1\) via boundary connectivity, assuming linked exits · \(p_c(\mathbb{Z}^2) < 1\) via the canonical contour, assuming anchored cycles · \(p_c(\mathbb{Z}^2) < 1\) via exit dart orbits, assuming linked exits · Set and walk interior share boundary edges · Lattice box as a finite set · Open cluster of a site · Lattice clusters agree with general graph clusters · Connection by an open path · Connection by an open path within a set · Open connection within a set is monotone in the set · Open circuit in a bond configuration · Open lattice edge of a bond configuration · Open subgraph of a bond configuration · Open subgraph induced on a set of sites · Origin of the hypercubic lattice · Percolation event for the origin · Percolation probability of bond percolation · Sites of a box as a finite set · Burton–Keane theorem · Trifurcation point, without requiring infinite branches · Configuration with all edges at a site closed · Number of trifurcation points in a box · Aizenman–Barsky inequality on \(\mathbb{Z}^d\) · Aizenman–Barsky inequality on \(\mathbb{Z}^d\) with neighbour row sum · Box as a finite set of sites · Box-crossing probability · Box-crossing event · Pairs of sites of a lattice box · Pairs of box sites outside a given set · Connection of a site to the box boundary · Box-crossing probability as a polynomial in the density · Duminil-Copin–Tassion differential inequality · Pairs of sites of a finite set · Edges of \(\mathbb{Z}^d\) inside a set · Pivotal edge event · Event that the unconnected set equals a given set · Set of sites not connected to the box boundary · Mean-field lower bound · Event of a connection inside a finite set · Open boundary edge of a cluster · Box edges with no endpoint in a cluster · Event that the cluster of the origin inside a set equals a given set · Open cluster of a site inside a set · One-arm probability · Exponential decay below p̃_c · One-arm event from the origin · One-arm event from a shifted origin · Exploration independence of a cluster inside a set · Edges from a subset into a set · Edges joining a finite set to a region · Crossing inside the box that avoids a cluster · Crossing to the box exterior that avoids a cluster · Exponential decay from a one-step recursion · \(\tilde p_c \le p_c\) if \(\theta = 0\) on the set defining \(\tilde p_c\) · Sharpness of the phase transition, conditional form · Equality of the Duminil-Copin–Tassion threshold and \(p_c\) · Exponential decay of the one-arm probability below the threshold · Sharpness of the phase transition · Positivity of the Duminil-Copin–Tassion threshold · Oriented edge boundary of a finite lattice set · Size bound for the edge boundary · Probability of connection inside a set · Shift of a lattice site in one coordinate · Duminil-Copin–Tassion quantity · Densities with a finite set of small Duminil-Copin–Tassion quantity · Boolean indicator of a set of sites of ℤ² · Bonds inside the box · Bonds touching the box · Ordered nearest-neighbour pairs inside the box · Ordered nearest-neighbour pairs touching the box · Box \((-n, n)^d\) as a finite set of sites · Convexity of the set of DLR states · Existence of infinite-volume states · Free-boundary Ising measure in a box · Infinite-volume free state as a subsequential weak limit · Box energy with a boundary condition · Finite-volume Gibbs measure on configurations of \(\mathbb{Z}^d\) · Finite-volume Gibbs probability with a boundary condition · Finite-volume Gibbs measure as a probability measure · Finite-volume Boltzmann weight with a boundary condition · Finite-volume partition function with a boundary condition · Consistency of the plus measures under the specification · Configuration glued from inside spins and a boundary condition · Uniqueness of the Gibbs state · Infinite-volume state of a sequence of measures · DLR state of the Ising model on \(\mathbb{Z}^d\) · Ising specification in a box · Ising specification as a Markov kernel · Chosen subsequential weak limit of a sequence of measures · All-minus configuration · Minus-boundary Ising measure in a box · Infinite-volume minus state as a subsequential weak limit · Overwriting a configuration on an inner box · All-plus configuration · Plus-boundary Ising measure in a box · Infinite-volume plus state as a subsequential weak limit · The plus state is a Gibbs (DLR) state · Restriction of a configuration to an inner box · Specification applied to a function · Specification applied to a bounded continuous function · Involution swapping inner-box parts of configuration pairs · Edge boundary of a set of sites · Edge with exactly one endpoint in a set · Hypercubic lattice with the edge boundary removed · Anchor row of \(\ell\) sites in \(\mathbb{Z}^2\) · Anchored closed-walk decoding of cluster contours in \(\mathbb{Z}^2\) · Bond configuration open on the edges inside a set · Peierls count of connected clusters by contour length · Rectangle \((0, m) \times (0, n)\) of sites · Frame of faces around a rectangle · Four faces meeting the origin · Injective closed-walk encoding of clusters of contour length \(\ell\) · Connected clusters in a box with contour length \(\ell\) · Sites reachable from the origin after deleting edges · Cluster family: all subsets of the box · Peierls series bound on the cluster-family contour sum · Contour event of a set: opposite spins across every crossing bond · Contour length of a set · Bond variable of a crossing bond · Contour of a set: bonds crossing its boundary · Bond crossing the boundary of a set · Inside configuration with the spins in a set flipped · Flipping spins in a set as an involutive equivalence · Configuration with the spins in a set flipped · Minus cluster of a site · Minus cluster of the origin as a finite set · Nearest-neighbour graph on the minus sites · Set of minus sites · Probability of the contour event of a set · Connected clusters in the box containing the origin · Peierls series bound on the connected-cluster contour sum · Connected cluster through the origin in the nearest-neighbour graph · Nearest-neighbour graph restricted to a set · Two-site set \(\{0, p\}\) · First \(\ell\) sites of the first coordinate axis · Closed-walk decoding of each realised contour from an axis site · Site \((j, 0, \ldots, 0)\) on the first coordinate axis · Closed-walk decoding of each realised contour from an anchor pool · Connected face-boundary graphs at the axis for all connected clusters · Primal edges crossed by a closed dual walk · Two faces flanking a primal edge · Two faces flanking an unordered pair of sites · Connected face-boundary graphs at the axis for all realised contours · Primal edge crossed by a dual edge · Primal edge crossed by an unordered pair of faces · Component of a face in the face-boundary graph · Faces of a set reachable from a face in the face-boundary graph · Tight axis circuit data: contour edges in one axis-face component · Finite face set containing the face-boundary support · Connectedness of the face-boundary graph on a face set · Hole-free clusters with contour length \(\ell\) · Hole-free clusters in the box through the origin · Hole-free connected cluster through the origin · Winding hypothesis for outer contours on \(\mathbb{Z}^2\) · Peierls counting bound on realised contours of length \(\ell\) · Contours of length \(\ell\) realised by connected clusters in a box · Assignment of interiors to closed walks of \(\mathbb{Z}^2\) · Outer contour map: clusters as interiors of boundary circuits · Cycles of length less than \(M\) based near the origin · Boltzmann weight of a closed walk in the circuit sum · Closed-walk encoding of realised contours of length \(\ell\) · Global spin flip of a configuration · Spin flip inside the box · Spin flip inside the box as an involutive equivalence · Finite-volume magnetization at the origin · Origin of \(\mathbb{Z}^d\) · Origin cluster family: finite site sets in the box through the origin · Peierls series bound on the origin-cluster contour sum · Site \(j e_c\) on the \(c\)-th coordinate axis · Support of the face-boundary graph of a finite set · Shift by \((-1, -1)\) as an equivalence of \(\mathbb{Z}^2\) · Shift isomorphism: lattice minus barrier edges to face region graph · Shift by \((-1, -1)\) identifying the double dual with \(\mathbb{Z}^2\) · Face-boundary graph of a finite set as a planar subgraph · Probability that the origin spin is minus · Configuration with only the origin minus · Filled-cluster winding hypothesis · Origin-only minus configuration satisfies the filled-cluster data · Exterior component of the complement of a set · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Set with its holes filled · Filled minus cluster of the origin as a finite set · FK critical point is less than one for \(d \ge 2\), \(q \ge 1\) · Integrability of the spin at a site under finite measures · Inf-based and sup-based Ising critical points agree for \(d \ge 2\) · Sup-based \(\beta_c\) equals \(-\tfrac{1}{2}\log(1 - p_c)\) for \(d \ge 2\) · Existence of the Ising phase transition · Spontaneous magnetization of the Ising model · Measurability of the spin at a site · Peierls' theorem · Spin at a site as a bounded continuous function · Approximation in measure by events measurable outside every box · Cylinder events of the Ising configuration space · σ-algebra generated by the spins in a finite set · Nonvacuity of the a.s.-tail theorem via the all-plus Dirac mass · All-plus Dirac mass gives the all-plus event probability one · Site with its nearest neighbours · Bonds touching a set · Set with its nearest neighbours · Energy on a set with a boundary condition · Configuration glued from a set and a boundary condition · Finite-volume Gibbs measure on a finite set · Overwriting a configuration on an inner set · Finite-volume Gibbs measure with plus boundary condition · Gibbs probability on a set with a boundary condition · Restriction of a configuration to an inner set · Involution swapping inner-set parts of configuration pairs · Unit vector of \(\mathbb{Z}^d\) · Boltzmann weight on a set with a boundary condition · Partition function on a set with a boundary condition · Boundary bond fraction of a box · Boundary influence bound for the minus box measures · Boundary influence bound for the plus box measures · Shift vector \(R e_{i_0}\) · Box sites as a set and as a finite set · Ergodicity of the plus state · Translation invariance of the plus state · Translation as an equivalence onto a translate · Extreme point of the DLR states · Tail event for lattice spin configurations · Extremality of the plus state · Off-centre domination of all-plus events · Asymptotic shift homogeneity of all-plus events in plus boxes · Continuous functions with decaying shifted integrals · All-plus monomial as a bounded continuous function · All-plus monomial as a continuous function · Shift homogeneity of all-plus events in the plus state · Decay of shifted integrals for minus box measures · Shifted minus-boundary box measure · Decay of shifted integrals for plus box measures · Shifted plus-boundary box measure · Plus-spin indicator at a site as a bounded continuous function · Plus-spin indicator at a site as a continuous function · Subalgebra of cylinder functions · Cylinder functions as bounded continuous functions · Difference between an integral and its shifted version · Decay of shifted cylinder integrals for minus box measures · Decay of shifted cylinder integrals for plus box measures · Pointwise convergence of box centered free energies · Box-edge marginal uniqueness off a countable set under tilt data · Edge-marginal uniqueness off a countable set from convex free energy · Collapse of average edge densities to the free density · Left-continuity of the free \(q = 2\) edge density in \(t\) · Free \(q = 2\) edge density is monotone in \(p\) on \((0, 1)\) · Wired \(q = 2\) edge density is monotone in \(t\) · Right-continuity of the wired \(q = 2\) edge density in \(t\) · Ambient tilted log normalizer ignores the decidability instance · Non-bulk edge fraction bound from a boundary bound on their count · Limits of tilted log normalizers on a fixed box are attained · A limit shared with growing boxes is one fixed-box graph's value · Tilted log normalizers on a fixed box take finitely many values · Average wired density collapse at \(q = 2\) · Free percolation probability · Free percolation probability is at most one · Nonnegativity of the free percolation probability · Free and wired measures differ at a first-order transition · Free and wired measures differ at self-dual \(p\) for \(q > 4\) if first order · Free and wired measures differ at \(\sqrt{q}/(1+\sqrt{q})\) for \(q > 4\) if first order · Wired percolation above the random-cluster critical point · Free percolation from domination and free–wired agreement at \(p'\) · Free percolation above \(p_c\) from monotonicity and countable agreement · The percolation event is increasing · Measurability of the percolation event · No percolation below the critical point at \(q = 2\) · Wired box-boundary connection probability is monotone in \(p\) at \(q = 2\) · Monotonicity of \(\theta^1(p, 2)\) in \(p\) · Box edge with a lattice-edge image is a box-graph edge · Open self-avoiding walk in a box gives \(m\) distinct open box edges · Extended box configuration keeps box edge states · Event of an open self-avoiding walk of \(m\) steps · No wired percolation for \(2dp < 1\) and \(q \ge 1\) · Wired percolation bound \(\theta^1(p, q) \le (2dp)^m\) for \(q \ge 1\) · Event of some open self-avoiding walk is clopen · Single-edge open event is clopen · Event that a given walk is open is clopen · Event of some open self-avoiding walk is increasing · Event that a given walk is open is increasing · Bernoulli bound \(p^m\) for a fixed self-avoiding walk in the box · Percolation gives open self-avoiding walks of every length · Open edges of an extended box configuration are box edges · Wired box bound \((2dp)^m\) on the open-walk event for \(q \ge 1\) · Wired box measure as a finite sum over box configurations · Wired random-cluster percolation probability \(\theta(p, q)\) · Closed-circuit event of a dual circuit · Non-percolation means the origin's cluster is finite · Finite cluster in \(\mathbb{Z}^2\) gives a closed lattice circuit · Finite cluster in \(\mathbb{Z}^2\): closed circuit, separated point, odd crossings · Finite subsets of \(\mathbb{Z}^2\) miss far points on each row · Finite cluster in \(\mathbb{Z}^2\) has a reachable point outside it · Finite-cluster event is covered by closed-circuit events · Horizontal lattice walk in \(\mathbb{Z}^2\) · Finite-volume plus-boundary magnetization at the origin · Wired probability that the origin reaches the box boundary · Origin as a vertex of the box graph · Origin lies in every box · Box configuration as a coloring of the next larger box · Restriction of a box coloring to the inner box · Box configurations as box-graph colorings with boundary color \(0\) · Free box measure dominated by the wired one for \(q \ge 1\) · Assumed doubling, boundedness and oscillation data along \(K_j\) · Negative log ambient normalizer of a box · Number of edges of a box · Isomorphism of a box with its translated copy in the predicate part · Isomorphism of a box with its translated copy in the complement part · Isomorphism of translated induced lattice graphs · \(\Lambda_n\) has \(d \cdot 2n(2n+1)^{d-1}\) edges · Dyadic convergence data for the ambient tilted log normalizer · Negative log ambient normalizer of the box \(\Lambda_n\) · Edge count of the box \(\Lambda_n\) · \(\Lambda_n\) has \(4n(2n+1)^{d-1}\) ordered pairs in each direction · \(2n(2n+1)^{d-1}\) sites of \(\Lambda_n\) stay inside after a unit shift · Ordered pairs in different directions are disjoint · Ordered nearest-neighbour pairs of \(\Lambda_n\) in direction \(i\) · Pairs in direction \(i\) are the forward and backward shifts · \(\Lambda_n\) has \(4dn(2n+1)^{d-1}\) ordered nearest-neighbour pairs · Ordered neighbour pairs of \(\Lambda_n\) as a union over directions · Box free-energy doubling bound along \(K_j\) holds for \(d, q \ge 1\) · Doubling bound for the box free energy when \(q \ge 1\) · Van Hove subadditivity of the box free energy for \(q \ge 1\) · Per-edge free energy converges along \(K_j\) for \(d, q \ge 1\) · Edge-normalized box free energy of the random-cluster model · Per-edge box free energy · Van Hove limit · Uniform upper bound on the box free energy for \(d, n, q \ge 1\) · Box free energy \(-\log Z^E\) of the random-cluster model · Forward and backward shift pairs are disjoint · Box Fekete data from a uniform bound and an oscillation bound · Additive doubling bound for \(-\log Z\) of the free \(q = 2\) FK model · The hyperplane block has at most \(2d|J|\) edges · Orthant blocks have the FK partition function of \(\Lambda_K\) · Vertex degrees in a box are at most \(2d\) · Doubling inequality for \(-\log Z\) of the free \(q = 2\) FK model · Orthant tag of a site of \(\Lambda_{2K+1}\) · Coordinate description of the sites with a given orthant tag · Bound on the edge gap \(|E(\Lambda_{2K+1})| - 2^d |E(\Lambda_K)|\) · \(\Lambda_{2K+1}\) has at least \(2^d\) times as many edges as \(\Lambda_K\) · Lower bound \(n(2n+1)^{d-1}\) on the number of edges of \(\Lambda_n\) · Hyperplane set of \(\Lambda_{2K+1}\) · The hyperplane set has at most \(d(4K+3)^{d-1}\) sites · Hyperplane set lies in the union of the coordinate slabs · Coordinate slab of \(\Lambda_{2K+1}\) · A coordinate slab has at most \((4K+3)^{d-1}\) sites · Translation of \(\Lambda_K\) onto an orthant block of \(\Lambda_{2K+1}\) · The all-tag restriction has the partition function of \(\Lambda_{2K+1}\) · At most \(2d|J|\) edges straddle an orthant tag · An edge leaving an orthant ends on a coordinate hyperplane · An edge between differently tagged sites meets a coordinate hyperplane · Edges straddling a tag are incident to the hyperplane set · Summability of doubling corrections relative to edge counts · Untagged sites are exactly those on a coordinate hyperplane · Translation vector onto an orthant of \(\Lambda_{2K+1}\) · A site is adjacent to its unit shift in one coordinate · Sites of \(\Lambda_n\) whose shift in coordinate \(i\) stays in the box · Shift map \(x \mapsto (x, x + b e_i)\) · Injectivity of the shift map · Unit shifts of sites staying in the box are pairs in direction \(i\) · Wired box measure dominates the induced-wiring measure for \(q \ge 1\) · Domain Markov property for the wired measure on nested boxes · Edge product of a glued configuration factorizes · Component decomposition of the wired glued graph · Component map into the wired glued graph · Glued and inner graphs have the same connections on the box · Induced wiring lies below the inner boundary clique · Wired cluster count of a glued configuration splits additively · Outer Bernoulli edge factor of an outer configuration · Gluing a box configuration into an outer configuration · Wired glued open graph is the union of inner and outer graphs · Event that the box origin connects to the box boundary · Box-boundary profile tends to \(\theta(p,2)\) if wired probabilities do · Inner vertex with an outside-graph edge lies on the inner boundary · Lattice inclusion matches induced adjacency · Lattice induced wirings are coarser than the inner boundary clique · Inner wired domination for vertex sets of \(\mathbb{Z}^d\) · Outer wired all-open probability at most the inner wired one · Vertex boundary of a box · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Extension of a box configuration by closed edges · Free random-cluster measure on a box · Free infinite-volume random-cluster measure · Free infinite-volume measure is a subsequential weak limit · Wired random-cluster measure on a box · Wired infinite-volume random-cluster measure · Wired infinite-volume measure is a subsequential weak limit · FKG inequality for free \(q = 2\) box measures on smaller-box events · FKG inequality for the free \(q = 2\) infinite-volume measure · FKG inequality for the wired \(q = 2\) infinite-volume measure · Wired \(q = 2\) measure dominates the free one on increasing cylinders · FKG inequality for wired \(q = 2\) box measures on smaller-box events · Convergence and ordering of free and wired limits at \(q = 2\) · Convergence and ordering at \(q = 2\) in subsequence form · Translation covariance of free box masses · Translation covariance of wired box masses · Wired box measure of an all-open event equals its box mass · Wired all-open probabilities converge to the infinite-volume value · Free box measure of an all-open event equals its box mass · Free all-open probabilities converge to the infinite-volume value · Free translation invariance from free placements of every shift · Equal free probabilities from eventually equal translated masses · Free placement for a shift via eventually equal box masses · Difference of wired all-open masses of an edge set and its translate · Wired translation invariance from wired placements of every shift · Equal wired probabilities from eventually equal translated masses · Wired placement for a shift via eventually equal box masses · Closed annulus plus inner-boundary wiring gives wired \(\Lambda_n\) law · Closed-annulus wired bound on origin-to-\(\partial\Lambda_n\), \(q = 2\) · Common subsequence with free and wired weak limits · Ordered free and wired subsequential limits exist for \(q \ge 1\) · Free limit at most wired limit along a common subsequence, \(q \ge 1\) · Wired probability that the origin connects to the outside of a box · Wired crossing probabilities converge to the percolation probability · Crossing events intersect to the percolation event · Conditional free probabilities depend only on the outer configuration · Domain Markov property · Conditional free measure as an induced-wiring measure · Free \(q=2\) box masses of increasing cylinders tend to infinite volume · Free \(q = 2\) box measures are bounded by the limit value · Free \(q = 2\) box measures of increasing cylinders converge · Free \(q = 2\) infinite-volume mass of increasing cylinders as a box limit · One-step growth of free \(q = 2\) measures of increasing cylinders · Free \(q = 2\) box measures of increasing cylinders are monotone · Limit of free \(q = 2\) box measures of a cylinder event · Fibre-mass factorization of random-cluster probabilities · Conditional free measure dominates the smaller free box for \(q \ge 1\) · Free measure is dominated by induced-wiring measures for \(q \ge 1\) · Random-cluster weight of a glued configuration factorizes · Free box measure of a cylinder event as a finite sum · Free box measures are at most one · Increasing box events gain free \(q = 2\) probability in the next box · Next-box free measure of a cylinder event as a finite sum · Decomposition of the free measure over the outer configuration · One-step box monotonicity of free measures for \(q \ge 1\) · Injectivity of the free cluster map · Surjectivity of the free cluster map · Glued open edges at outer vertices are outer edges · Inner-graph connections are glued-graph connections · Conditional partition function in terms of the induced wiring · Glued connections between inner vertices are inner-graph connections · Outer open connections give connections in the inner graph · Cluster count of a glued configuration splits additively · Glued open graph is the union of inner and outer open edges · Positivity of the outer weight factor · Fibre masses of the free measure sum to one · Secant bound gives free–wired density agreement off a countable set · Off-centre carrier tends to zero · Off-centre carrier vanishes by translation covariance · Free density is at most each translated wired marginal · Translated wired marginals converge to the wired density · Equal wired densities from equal translated marginals · Inclusion of the annulus wiring into the extra-wired graph · Box as an induced subgraph of the next box · Inclusion of box vertices into the next box · Domain Markov property for the wired box measure · Extended-graph components as inner components plus annulus vertices · Extra-wired components as inner plus annulus-wiring components · Extension of a configuration closing the annulus edges · Extended open graph with the inner box boundary wired · Vertex on the boundary of the inner box · Edges of the next box coming from the inner box · Configurations closed off the inner edges as inner-box configurations · Open graph of a box configuration with the box boundary wired · Inclusion of the wired inner graph into the extended wired graph · Inclusion of the wired inner graph into the extra-wired graph · Vertex of the next box lying in the inner box · Number of next-box edges not coming from the inner box · Wired infinite-volume measure as limit on increasing cylinder events · Wired box probabilities of increasing cylinder events converge · Wired \(q = 2\) increasing-event probabilities do not grow with the box · Infimum of wired box probabilities of a box event · Wired infinite-volume probability equals the infimum over boxes · Box-boundary connection probability tends to percolation probability · Event that the open cluster of a site is infinite · A connection to outside the box passes through the box boundary · Crossing probabilities converge to the percolation probability · Joint percolation at most connectivity given no two infinite clusters · Two-point connectivity of a bond measure on \(\mathbb{Z}^d\) · Uniform decay of two-point connectivity without percolation · Two-point lower bound from FKG, invariance, uniqueness and percolation · Disconnected sites in infinite clusters give two infinite clusters · Event that two sites are joined by open edges inside a box · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Free box measure of a box connection event is the two-point function · Free infinite-volume two-point function in a box · Convergence to the free two-point function under stochastic increase · Cylinder events of a box are clopen · Box restriction pulls increasing events back to increasing events · Cylinder events of a box are measurable · Wired infinite-volume two-point function in a box · Convergence to the wired two-point function under stochastic decrease · Outer projection agrees with the configuration off \(\Lambda_n\) · Wired \(q = 2\) percolation probability as the limit of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_n\) · Boundary connection of \(\Lambda_n\) is a \(\Lambda_m\) cylinder event · Boundary connection inside \(\Lambda_n\) reaches outside \(\Lambda_{n-1}\) · Events \(0 \leftrightarrow \partial\Lambda_n\) decrease in \(n \ge 1\) · One-step decrease of the events \(0 \leftrightarrow \partial\Lambda_n\) · Open path from the origin out of \(\Lambda_n\) gives \(0 \leftrightarrow \partial\Lambda_n\) inside \(\Lambda_n\) · Inner vertices next to the annulus lie on \(\partial\Lambda_n\) · Open lattice edges between box vertices are open box edges · Restriction to \(\Lambda_n\) factors through \(\Lambda_m\) · Box inclusion maps the origin to the origin · Inclusion of \(\Lambda_n\) into \(\Lambda_m\) for \(n \le m\) · Conditional wired decrease on inner increasing events for \(q \ge 1\) · Paths to \(\partial\Lambda_{n+1}\) pass through \(\partial\Lambda_n\) · Open connections in a box are open connections in \(\mathbb{Z}^d\) · Leaving \(\Lambda_n\) implies connecting to \(\partial\Lambda_n\) · Edge inclusion into \(\mathbb{Z}^d\) factors through \(\Lambda_m\) · Configurations with a given outer part form its conditioning fibre · Cylinder form of the \(\Lambda_n\) boundary connection is measurable · Open edges of \(\Lambda_n\) are open edges of \(\Lambda_{n+1}\) · Open edges of a box are open edges of \(\mathbb{Z}^d\) · Outer projection closes the edges of \(\Lambda_n\) · Outer projection keeps the edges outside \(\Lambda_n\) · Outer projection is idempotent · Wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_k\) in \(\Lambda_{k+j}\) is nonincreasing in \(j\) · Masses of the conditioning fibres sum to one · Wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_n\) is nonincreasing in \(n\) · Wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_{n+k+1}\) at most in \(\Lambda_{n+k}\) · Infinite-volume limit of the wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_k\) · Wired \(\Lambda_m\) measure of a \(\Lambda_m\) cylinder event as a sum · Wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_{n+1}\) at most in \(\Lambda_n\) · Wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_{m+1}\) at most in \(\Lambda_m\), \(m \ge n\) · Wired box measures decrease on increasing cylinder events at \(q = 2\) · Wired \(\Lambda_{n+1}\) measure of a \(\Lambda_n\) cylinder event as a sum · Wired infinite-volume boundary connection tends to \(\theta^1(p, q)\) · Wired \(\Lambda_{n+1}\) measure decomposed over outer configurations · Wired box measures decrease on inner increasing events for \(q \ge 1\) · Boxes satisfy the additive doubling bound for \(d \ge 1\) · Van Hove tiling bound for the edge partition function · Graph isomorphism between a sub-box and a tiling cell · Translation between a sub-box and a tiling cell · Coordinate index of the tiling cell containing a site · Center of a cell in the tiling of a box by sub-boxes · Per-edge free energy of a box in the tilt variable · Per-edge negative log edge partition function of a box · Per-box \(q = 2\) uniqueness off a countable set of tilts · Convergence of the per-edge free energy of boxes · Per-edge free energy of boxes converges for \(d \ge 1\) · Sub-box as an induced subgraph of a larger box · Membership of a box vertex in a sub-box · Negative log edge partition function of a box · Tiling cell of a box vertex · Wired-marginal difference between a box and its translate · Secant bound gives \(q = 2\) edge-event uniqueness off a countable set · Convex limit of centered tilt free energies of boxes for \(d, q \ge 1\) · Per-box uniqueness of the random-cluster measures off a countable set · Free infinite-volume mass function on a box for \(q \ge 1\) · Free unit-edge marginal at \(0\) on \(\Lambda_{\lfloor\sqrt n\rfloor}\) · Wired unit-edge marginal at \(0\) on \(\Lambda_{\lfloor\sqrt n\rfloor}\) · Wired infinite-volume mass function on a box for \(q \ge 1\) · Countable-exception \(q = 2\) uniqueness from one-sided derivative data · Free average edge density collapse on boxes · Free densities of genuine box edges as left derivatives · Wired average edge density collapse on boxes · Wired densities of genuine box edges as right derivatives · Per-coordinate free energy on a box · Free infinite-volume edge density · Free-energy data give \(q = 2\) box uniqueness off countably many \(t\) · Free \(q = 2\) infinite-volume mass function on a box · Wired \(q = 2\) infinite-volume mass function on a box · Two-sided free \(q = 2\) bulk bounds from the free sandwich · Free \(q = 2\) bulk sandwich from equal free edge densities · Two-sided wired \(q = 2\) bulk bounds from the wired sandwich · Wired \(q = 2\) bulk sandwich from equal wired edge densities · Bulk edges of \(\Lambda_n\) · Shell edge fraction is at most \(4d^2(n-m)/n\) · Adjacent box vertices differ by a signed unit vector · Vanishing shell edge fraction when \((n - m(n))/n \to 0\) · Lower bound on free bulk edge marginals · Free off-centre lower bound by the recentred small-box marginal · Free off-centre sandwich from free rotation residues · Free rotation residue for a box pair · Unit edge \(\{0, \pm e_j\}\) of a box · Free unit-edge marginals converge to the free density · Wired unit-edge marginals converge to the wired density · Free unit-edge marginal in the square-root box · Wired unit-edge marginal in the square-root box · Wired bulk edges of \(\Lambda_n\) · Upper bound on wired bulk edge marginals · Wired off-centre sandwich from wired rotation residues · Wired off-centre upper bound by the recentred small-box marginal · Wired rotation residue for a box pair · Adjacent sites differ by a signed unit vector · Unit edges at the origin have the free density of \(\{0, e_0\}\) · Box symmetries preserve the free \(q = 2\) density of any pair of sites · Every lattice edge has the free \(q = 2\) density of \(\{0, e_0\}\) · All box edges have the same free \(q = 2\) density · Coordinate permutation as a box symmetry · Coordinate permutation of \(\mathbb{Z}^d\) · Reference edge \(\{0, e_0\}\) of \(\mathbb{Z}^d\) · Unit edges at the origin have the wired density of \(\{0, e_0\}\) · Box symmetries preserve the wired \(q = 2\) density of any pair of sites · Every lattice edge has the wired \(q = 2\) density of \(\{0, e_0\}\) · All box edges have the same wired \(q = 2\) density · Average wired \(q = 2\) edge density of a box as a mean of marginals · Free \(q = 2\) edge density lies in \((0, 1)\) · Free growing-box collapse at \(q = 2\) · Free uniform bulk deviation at \(q = 2\) · Wired \(q = 2\) edge density lies in \((0, 1)\) · Wired uniform bulk deviation at \(q = 2\) · Wired infinite-volume edge density · Box symmetry of \(\mathbb{Z}^d\) · Box symmetries preserve the free \(q = 2\) density of box edges · Coordinate reflection as a box symmetry · Reflection of \(\mathbb{Z}^d\) in one coordinate · Box symmetries preserve the wired \(q = 2\) density of box edges · Translation covariance of FK edge marginals on boxes · Translated box in \(\mathbb{Z}^d\) · Vertex boundary of a translated box · Nearest-neighbour graph on a translated box · Some translated box leaves the centered box for \(d \ge 1\) · Vertex type of a translated box · Translation from the centered box onto a translated box · Restriction of a box symmetry to a box · Translation invariance of the free \(q = 2\) infinite-volume measure · Free off-centre sandwich hypothesis · Free \(q = 2\) box edge marginals are at most the free density · Wired off-centre sandwich hypothesis · Wired \(q = 2\) box edge marginals are at least the wired density · Translate of a vertex of \(\Lambda_N\) as a vertex of \(\Lambda_{N+r}\) · Translate of an edge of \(\Lambda_N\) as an edge of \(\Lambda_{N+r}\) · Shift vector moving \(\Lambda_N\) to a disjoint box · Ergodicity of the wired random-cluster measure · Submodule of functions with vanishing free shift decay · Free \(q = 2\) multi-edge homogeneity under a translation · Monomial indicator as a bounded continuous function · Continuous monomial indicator that every edge of a set is open · Event that every edge of a finite set is open · Submodule of functions with vanishing wired shift decay · Wired \(q = 2\) multi-edge homogeneity under a translation · Disjoint-box cap hypothesis for multi-open events · Translated free box measure · Translated wired box measure · Conditional product cap for multi-open events in boxes · Unordered pair of two sites of a box \(\Lambda_N\) · Translation invariance of free and wired densities if marginals merge · An edge and its translate lie in a common centered box · Constant free density gives an upper bound on expected open edges · Free upper bound on expected open edges along a box-symmetry orbit · Equal free densities from merging free marginals · Translation invariance of the free density given merging marginals · A site and its translate lie in a common centered box · Translation of \(\mathbb{Z}^d\) by a vector · Unit translations are not box symmetries · Constant wired density gives a lower bound on expected open edges · Wired lower bound on expected open edges along a box-symmetry orbit · Equal wired densities from merging wired marginals · Translation invariance of the wired density given merging marginals · Inclusion of a subset of sites into a larger one · Box edge set included into \(\Lambda_m\) and translated by \(v\) · Sup norm of a site of \(\mathbb{Z}^d\) · Translation invariance of the wired \(q = 2\) infinite-volume measure · Far-box product domination of multi-open events · Finite-box disjoint product domination of multi-open events · Wired box products approximate infinite-volume products · Every finite family of edge sets is realized in some box · Finite-box product domination from the factorization bound · Realized edge sets stay realized in larger boxes · Upper decorrelation of the wired measure from factorization · Domain monotonicity of wired \(q = 2\) box measures · Domain monotonicity for translated pairs of multi-open events · Disjoint-box factorization bound for box measures · All-open Dirac mass satisfies the factorization bound · Domain monotonicity for edge sets realized in a box · Wired \(q = 2\) measure is ergodic under the factorization bound · Domain monotonicity of wired multi-open probabilities · Edge-open indicator as a bounded continuous function · Edge-open indicator as a continuous function · Cylinder algebra generated by edge indicators · Cylinder algebra as bounded continuous functions · Density of cylinder functions among bounded continuous functions · Cylinder decay along the free box measures · Translation invariance of the free FK measure from cylinder decay · Free box integral of an edge indicator is the free edge marginal · Wired box integral of an edge indicator is the wired edge marginal · Decay of the edge-indicator functional from equal wired densities · Cylinder decay along the wired box measures · Translation invariance of the wired FK measure from cylinder decay · Shift-decay functional of a sequence of measures · Free shift decay on a dense set of test functions · Free translation invariance from decay on a dense set · Shift decay extends from a dense set of test functions · Wired shift decay on a dense set of test functions · Wired translation invariance from decay on a dense set · Free integral shift decay along a box sequence · Identity shift satisfies the free decay hypothesis · Free translation invariance from integral shift decay · Wired integral shift decay along a box sequence · Identity shift satisfies the wired decay hypothesis · Wired translation invariance from integral shift decay · Free translation invariance from the placement hypothesis · Free placement gives shift homogeneity on all-open events · Equal free probabilities for \(t\) and \(v + t\) from matching box limits · Free infinite-volume measure is homogeneous under the identity shift · Free placement hypothesis for a shift via box-mass limits · Identity shift satisfies the free placement hypothesis · Wired all-open probability on a translated box · Translated wired box mass equals the centered box mass · Translated free box mass of an edge set · Translated free box mass equals the centred box probability · Translated free box masses converge to the free infinite-volume value · Translated wired box masses converge to the infinite-volume mass · Edge inclusion of a translated box into \(\mathbb{Z}^d\) · Translated box edges are shifted centered box edges · Images of translated edge sets are shifted images · Wired translation invariance from the placement hypothesis · Wired placement gives shift homogeneity on all-open events · Wired shift invariance of an all-open event from matching limits · Wired shift invariance of an all-open event from decaying differences · Wired infinite-volume measure is homogeneous under the identity shift · Wired placement hypothesis for a shift · Identity shift satisfies the wired placement hypothesis · Boundary covariance error · Box \(\Lambda_n\) as a type · Origin–site covariance in a box · Nearest-neighbour graph on a box · Membership of a larger-box site in a smaller box · Smaller box as a subtype of a larger box · Free-boundary site magnetization in a box · Origin as a site of a box · All sites of a box · Lattice site as a box site, defaulting to the origin · Edge with exactly one endpoint in a cut set · Boundary error of the finite-volume mean-field inequality · Cut mass of a box set rooted at the field ghost · Lattice sites underlying a set of box sites · Identification of a box cut set with its lattice sites · Boundary correlation of an edge crossing a cut · Exterior neighbours of a site · External boundary correlation of a cut, over edges leaving the box · Pairs of a box site and an outside lattice neighbour · Finite-volume mean-field inequality for the Ising model · Field switched off on the outer layer · Origin magnetization with the outer-layer field switched off · Internal boundary correlation of a cut in the box · Minimal origin-to-site magnetization ratio in a box · Mean-field lower bound for the spontaneous magnetization · Oriented cut mass over cuts \(T \ni 0, x\) with \(y \notin T\) · \(\beta\)-derivative of the origin magnetization in a box · Covariance sum over the outer layer · Outer-layer indicator as a field direction · Translation onto a translated box · Translated box \(\Lambda_n - y\) · Nearest-neighbour graph on a translated box · Membership of a doubled-box site in a translated box · Translated box as a subtype of the doubled box · Simon radius of a finite set · Tail set of plus-state correlations · Window sum of plus-state correlations · Supremum of plus-state window sums over windows of at most \(n\) sites · Sharpness of the Ising phase transition on \(\mathbb{Z}^d\), \(d \ge 2\) · Auxiliary critical point \(\tilde\beta_c(d)\) is positive for \(d \ge 2\) · Free origin correlation in a set, extended by zero · Free-boundary zero-field two-point function in a finite set · Induced subgraph of \(\mathbb{Z}^d\) on a finite set · Percolation quantity \(\varphi_p(S)\) at \(p = 1 - e^{-\beta}\) · Duminil-Copin–Tassion quantity \(\varphi_\beta(S)\) for the Ising model · Inverse temperatures with an Ising witness \(\varphi_\beta(S) < 1\) · Inverse temperatures with a percolation witness \(\varphi(S) < 1\) · Boundary edges of a finite volume · Field induced by the plus boundary condition · Plus-state two-point function at zero field · Simon–Lieb inequality in the infinite-volume plus state · Underlying lattice sites of a subset of a volume · Identification of volume sites with lattice sites · Simon–Lieb boundary sum against a measure · Simon–Lieb boundary sum in the plus state · Sites of a volume lying in a set · Spin pair product as a bounded continuous function · Isomorphism of the hypercubic lattice with Physlib's crystal graph · Outer vertex boundary of a box

DefinitionNearest neighbours in \(\mathbb{Z}^d\)#✓fully proved

Two sites are nearest neighbours when their ℓ¹ distance ∑ i, |x i - y i| equals one.

def NearestNeighbour (d : ℕ) (x y : Site d) : Prop :=
  (∑ i, (x i - y i).natAbs) = 1

Uses 1 · Used by 41

Statement usesSite of the hypercubic lattice

Used byHypercubic lattice \(\mathbb{Z}^d\) · Bounded faces of a finite lattice graph are counted by its cycle rank · Pushed-forward subgraphs are locally finite · Anchored dual cycles of a given length · \(p_c(2) < 1\) from anchored dual-circuit enclosure · Finite face set containing the face-boundary support · Support of the face-boundary graph of a finite set · Face-boundary graph of a finite set as a planar subgraph · Origin-only minus configuration satisfies the filled-cluster data · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Inf-based and sup-based Ising critical points agree for \(d \ge 2\) · Peierls' theorem · Bonds touching a set · Translation invariance of the plus state · Finite cluster in \(\mathbb{Z}^2\) gives a closed lattice circuit · Finite cluster in \(\mathbb{Z}^2\): closed circuit, separated point, odd crossings · Vertex degrees in a box are at most \(2d\) · Induced wiring lies below the inner boundary clique · Inner vertex with an outside-graph edge lies on the inner boundary · Lattice induced wirings are coarser than the inner boundary clique · Inner wired domination for vertex sets of \(\mathbb{Z}^d\) · Outer wired all-open probability at most the inner wired one · Open path from the origin out of \(\Lambda_n\) gives \(0 \leftrightarrow \partial\Lambda_n\) inside \(\Lambda_n\) · Inner vertices next to the annulus lie on \(\partial\Lambda_n\) · Per-box uniqueness of the random-cluster measures off a countable set · Free \(q = 2\) bulk sandwich from equal free edge densities · Wired \(q = 2\) bulk sandwich from equal wired edge densities · Shell edge fraction is at most \(4d^2(n-m)/n\) · Adjacent box vertices differ by a signed unit vector · Free off-centre sandwich from free rotation residues · Wired off-centre sandwich from wired rotation residues · Wired off-centre upper bound by the recentred small-box marginal · Adjacent sites differ by a signed unit vector · Ergodicity of the wired random-cluster measure · Translation invariance of the wired \(q = 2\) infinite-volume measure · Exterior neighbours of a site · Mean-field lower bound for the spontaneous magnetization · Sharpness of the Ising phase transition on \(\mathbb{Z}^d\), \(d \ge 2\) · Auxiliary critical point \(\tilde\beta_c(d)\) is positive for \(d \ge 2\) · Simon–Lieb inequality in the infinite-volume plus state

DefinitionHypercubic lattice \(\mathbb{Z}^d\)#✓fully proved

The hypercubic lattice ℤ^d: the simple graph on Site d whose edges join nearest neighbours.

def hypercubicLattice (d : ℕ) : SimpleGraph (Site d) where
  Adj := NearestNeighbour d
  symm := ⟨fun _ _ h => nearestNeighbour_symm d h⟩
  loopless := nearestNeighbour_irrefl d

Uses 2 · Used by 274

Statement usesNearest neighbours in \(\mathbb{Z}^d\) · Site of the hypercubic lattice

Used byEdge boundary of a set of sites · Square lattice is connected · First index where a walk reaches a coordinate value · Changing one coordinate stays in the same component · Increasing one coordinate stays in the same component · Complement of a finite set in \(\mathbb{Z}^d\) has one infinite component · Lattice connectivity in the complement implies king connectivity · Dart of the square lattice · Successor of a boundary dart · Next boundary dart direction is rotated by the turn · Successor map on boundary darts · Face loop around the domino · Lattice darts agree with graph darts of the square lattice · Dart correspondence respects reversal · Boundary darts with heads in one component share an orbit · Dart from a site in a unit direction · Minimal-period orbit loop as a lattice walk · Boundary orbit face loop as a lattice walk · Orbit saturation by heads connected in the complement · Walk along the first iterates of a boundary dart · Reversal of a lattice dart · Nontrivial quarter-turn rotations fix no lattice direction · Face loop around the unit cell · \(p_c(\mathbb{Z}^2) < 1\) under a no-pinch hypothesis · Bounded regions are the components other than the outer one · Set of sites is the inside of a closed lattice walk · Number of boundary crossings of a walk · Inside and outside of a closed walk are connected · Box exterior embeds in the region graph · Face-boundary graph of a set · Lattice off a closed walk · Jordan region property off a closed walk · Lattice walk avoiding a set, lifted to the reduced lattice · Square lattice with a set of vertices removed · Square lattice minus the edges of a graph · Unit square as a planar lattice subgraph · Quarter-turn isomorphism onto the region graph · 8-cycle around the L-tromino as a planar lattice subgraph · Separating side between inside and outside sites · Two corner-sharing unit squares as a planar lattice subgraph · Open vertical crossings separate the sides of a rectangle · Horizontal lattice path rightward · Inside of a closed walk by the even-odd rule · Ray-crossing count of a walk · Return path around a rectangle · Vertical lattice path upward · Wall-crossing count of a walk · Cut set of a face coloring · Bounded faces of a finite lattice graph are counted by its cycle rank · Lattice graph spanned by an edge set · Pushed-forward subgraphs are locally finite · Whitney cut-cycle duality for a planar lattice subgraph · Exterior of a box maps into the face-region graph · Unit square with a pendant edge as a planar lattice subgraph · Two disjoint unit squares as a planar lattice subgraph · 3 by 3 grid as a planar lattice subgraph · Keep-reconnect residue for finite graphs · Horizontal axis with one edge removed · Square lattice with the boundary edges of a set removed · Square lattice with a closed walk's vertices removed · Component off a closed walk containing a seed · Planar lattice subgraph of the square lattice · Rotated region graph of a lattice subgraph · Boundary darts of a component off a closed walk · Facial orbits cover the components of the complement · Square lattice induced on the box \((-n, n)^2\) · Consecutive walk vertices are adjacent in the square lattice · Simple closed walk as an embedded cycle graph · The inner face component is finite · Face-adjacent cells have the same ray parity · Horizontally face-adjacent cells have the same ray parity · Vertically face-adjacent cells have the same ray parity · Consecutive left cells on a straight step are face-adjacent · Left and right cells of a step share that step · Lattice Jordan curve theorem, even-odd form · Bounded face of a simple closed walk has no pinch points · No right cell lies in the bounded face · A side between interior and exterior cells is a walk edge · Cells on either side of a step lie in different faces · Number of cells is at most the nullity of the skeleton · Adjacent cells have connected lower-left corners · 1-skeleton of a cell complex as a planar subgraph · The face of a cell is enclosed on all four sides · Shared side of a cell and an adjacent face is an edge · Interior cells have connected lower-left corners · Hopf's Umlaufsatz · Bijection between primal and dual edges · Dual square lattice · Quarter-turn rotation as a lattice automorphism · Identity self-duality of the square lattice · Rotational self-duality of the square lattice · Whitney duality in the bridge direction · Closed face walk around a lattice vertex · Cut-flip count along a walk · Chosen lattice walk between two faces · Even-flip condition on closed lattice walks · Cut coloring separating the ends of a dual edge · Number of flips along a lattice walk · Closed walk around a unit square · Symmetry of a flip relation on lattice edges · Whitney's cut–cycle duality · Face-region graph of a square-lattice subgraph · Face coloring compatible with a subgraph · Cut coloring of a subgraph with an extra dual edge · Number of edge crossings of a face walk · Walk in an induced open subgraph as a lattice walk · Projection of an induced open subgraph to the lattice · Vertical overlap crossings separate the sides of a rectangle · RSW gluing from side separation · Monotonicity of the open subgraph in the plane · Separating set for a lattice rectangle · Measurability of connection inside a set · Condition that every left-right crossing meets the open cluster · Rectangle lattice with an open cluster removed · Event that a dual circuit is closed · Anchored dual cycles of a given length · Step directions of an open walk from the origin · Positive planar percolation at some \(p < 1\) via the Ising model · \(p_c(2) < 1\) from anchored dual-circuit enclosure · Positivity of the critical probability (Hammersley's bound) · Plane open connections are open connections in \(\mathbb{Z}^{2+k}\) · Plane embedding preserves and reflects adjacency · Primal edges crossed by a dual walk · Measurability of the one-arm event · Number of infinite clusters is almost surely constant · Translation of the open subgraph as a graph homomorphism · Inverse translation of the open subgraph · Face walk along the first successors of a boundary dart · Open cluster maps into the lattice minus its boundary edges · Cut lattice of a set of sites · Face loop of a boundary orbit in the face-boundary graph · Face walk along a boundary orbit · Discrete Jordan separation for finite open clusters · Exit dart on the positive horizontal axis · Box exterior maps into the lattice minus boundary edges · Exit dart on the negative horizontal axis · \(p_c(\mathbb{Z}^2) < 1\) assuming simple exit orbits · \(p_c(\mathbb{Z}^2) < 1\) assuming a canonical orbit cycle · \(p_c(\mathbb{Z}^2) < 1\) via boundary connectivity, assuming linked exits · Set and walk interior share boundary edges · Lattice clusters agree with general graph clusters · Open lattice edge of a bond configuration · Open subgraph of a bond configuration · Aizenman–Barsky inequality on \(\mathbb{Z}^d\) · Aizenman–Barsky inequality on \(\mathbb{Z}^d\) with neighbour row sum · Duminil-Copin–Tassion differential inequality · Mean-field lower bound · Exponential decay below p̃_c · Exploration independence of a cluster inside a set · Sharpness of the phase transition · Ordered nearest-neighbour pairs inside the box · Ordered nearest-neighbour pairs touching the box · The plus state is a Gibbs (DLR) state · Edge boundary of a set of sites · Hypercubic lattice with the edge boundary removed · Anchored closed-walk decoding of cluster contours in \(\mathbb{Z}^2\) · Injective closed-walk encoding of clusters of contour length \(\ell\) · Sites reachable from the origin after deleting edges · Minus cluster of the origin as a finite set · Nearest-neighbour graph on the minus sites · Nearest-neighbour graph restricted to a set · Closed-walk decoding of each realised contour from an axis site · Closed-walk decoding of each realised contour from an anchor pool · Primal edges crossed by a closed dual walk · Finite face set containing the face-boundary support · Assignment of interiors to closed walks of \(\mathbb{Z}^2\) · Outer contour map: clusters as interiors of boundary circuits · Cycles of length less than \(M\) based near the origin · Boltzmann weight of a closed walk in the circuit sum · Closed-walk encoding of realised contours of length \(\ell\) · Support of the face-boundary graph of a finite set · Shift isomorphism: lattice minus barrier edges to face region graph · Face-boundary graph of a finite set as a planar subgraph · Origin-only minus configuration satisfies the filled-cluster data · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Filled minus cluster of the origin as a finite set · FK critical point is less than one for \(d \ge 2\), \(q \ge 1\) · Inf-based and sup-based Ising critical points agree for \(d \ge 2\) · Sup-based \(\beta_c\) equals \(-\tfrac{1}{2}\log(1 - p_c)\) for \(d \ge 2\) · Existence of the Ising phase transition · Peierls' theorem · Bonds touching a set · Ergodicity of the plus state · Translation invariance of the plus state · Extremality of the plus state · The percolation event is increasing · Box edge with a lattice-edge image is a box-graph edge · Open self-avoiding walk in a box gives \(m\) distinct open box edges · Percolation gives open self-avoiding walks of every length · Closed-circuit event of a dual circuit · Finite cluster in \(\mathbb{Z}^2\) gives a closed lattice circuit · Finite cluster in \(\mathbb{Z}^2\): closed circuit, separated point, odd crossings · Finite cluster in \(\mathbb{Z}^2\) has a reachable point outside it · Finite-cluster event is covered by closed-circuit events · Horizontal lattice walk in \(\mathbb{Z}^2\) · Isomorphism of a box with its translated copy in the predicate part · Isomorphism of a box with its translated copy in the complement part · Isomorphism of translated induced lattice graphs · \(\Lambda_n\) has \(d \cdot 2n(2n+1)^{d-1}\) edges · Ordered pairs in different directions are disjoint · Pairs in direction \(i\) are the forward and backward shifts · Ordered neighbour pairs of \(\Lambda_n\) as a union over directions · Vertex degrees in a box are at most \(2d\) · Lower bound \(n(2n+1)^{d-1}\) on the number of edges of \(\Lambda_n\) · An edge leaving an orthant ends on a coordinate hyperplane · A site is adjacent to its unit shift in one coordinate · Unit shifts of sites staying in the box are pairs in direction \(i\) · Edge product of a glued configuration factorizes · Component decomposition of the wired glued graph · Component map into the wired glued graph · Glued and inner graphs have the same connections on the box · Induced wiring lies below the inner boundary clique · Inner vertex with an outside-graph edge lies on the inner boundary · Lattice inclusion matches induced adjacency · Lattice induced wirings are coarser than the inner boundary clique · Inner wired domination for vertex sets of \(\mathbb{Z}^d\) · Outer wired all-open probability at most the inner wired one · Nearest-neighbour graph on a box · Translation covariance of free box masses · Translation covariance of wired box masses · Closed annulus plus inner-boundary wiring gives wired \(\Lambda_n\) law · Inner-graph connections are glued-graph connections · Glued connections between inner vertices are inner-graph connections · Box as an induced subgraph of the next box · Domain Markov property for the wired box measure · Extended-graph components as inner components plus annulus vertices · Extra-wired components as inner plus annulus-wiring components · Inclusion of the wired inner graph into the extended wired graph · Inclusion of the wired inner graph into the extra-wired graph · Open path from the origin out of \(\Lambda_n\) gives \(0 \leftrightarrow \partial\Lambda_n\) inside \(\Lambda_n\) · Inner vertices next to the annulus lie on \(\partial\Lambda_n\) · Open lattice edges between box vertices are open box edges · Open edges of \(\Lambda_n\) are open edges of \(\Lambda_{n+1}\) · Open edges of a box are open edges of \(\mathbb{Z}^d\) · Graph isomorphism between a sub-box and a tiling cell · Per-box \(q = 2\) uniqueness off a countable set of tilts · Per-box uniqueness of the random-cluster measures off a countable set · Countable-exception \(q = 2\) uniqueness from one-sided derivative data · Free \(q = 2\) bulk sandwich from equal free edge densities · Wired \(q = 2\) bulk sandwich from equal wired edge densities · Shell edge fraction is at most \(4d^2(n-m)/n\) · Adjacent box vertices differ by a signed unit vector · Vanishing shell edge fraction when \((n - m(n))/n \to 0\) · Free off-centre lower bound by the recentred small-box marginal · Free off-centre sandwich from free rotation residues · Wired off-centre sandwich from wired rotation residues · Wired off-centre upper bound by the recentred small-box marginal · Adjacent sites differ by a signed unit vector · Every lattice edge has the free \(q = 2\) density of \(\{0, e_0\}\) · All box edges have the same free \(q = 2\) density · Coordinate permutation as a box symmetry · Every lattice edge has the wired \(q = 2\) density of \(\{0, e_0\}\) · All box edges have the same wired \(q = 2\) density · Box symmetry of \(\mathbb{Z}^d\) · Box symmetries preserve the free \(q = 2\) density of box edges · Coordinate reflection as a box symmetry · Box symmetries preserve the wired \(q = 2\) density of box edges · Translation covariance of FK edge marginals on boxes · Nearest-neighbour graph on a translated box · Translation invariance of the free \(q = 2\) infinite-volume measure · Ergodicity of the wired random-cluster measure · Translation invariance of the wired \(q = 2\) infinite-volume measure · Nearest-neighbour graph on a box · Exterior neighbours of a site · Finite-volume mean-field inequality for the Ising model · Mean-field lower bound for the spontaneous magnetization · Nearest-neighbour graph on a translated box · Sharpness of the Ising phase transition on \(\mathbb{Z}^d\), \(d \ge 2\) · Auxiliary critical point \(\tilde\beta_c(d)\) is positive for \(d \ge 2\) · Free-boundary zero-field two-point function in a finite set · Induced subgraph of \(\mathbb{Z}^d\) on a finite set · Simon–Lieb inequality in the infinite-volume plus state · Isomorphism of the hypercubic lattice with Physlib's crystal graph

DefinitionBox \((-n, n)^d\) in the hypercubic lattice#✓fully proved

The box [-n, n]^d of sites whose coordinates all have absolute value at most n.

def box (d n : ℕ) : Set (Site d) := {x | ∀ i, (x i).natAbs ≤ n}

Uses 1 · Used by 430

Statement usesSite of the hypercubic lattice

Used bySize of the vertex boundary of the box \((-n, n)^d\) · Every finite set of sites lies in a box · Complement of a finite set in \(\mathbb{Z}^d\) has one infinite component · Inner vertex boundary of a box · Bounded regions are the components other than the outer one · Box exterior embeds in the region graph · Bounded faces of a finite lattice graph are counted by its cycle rank · Exterior of a box maps into the face-region graph · Radius of a box containing a planar lattice subgraph · Square lattice induced on the box \((-n, n)^2\) · The inner face component is finite · A face far outside the walk has ray parity zero · Lattice Jordan curve theorem, even-odd form · Number of cells is at most the nullity of the skeleton · Hopf's Umlaufsatz · Square annulus in the plane lattice · Bernoulli box cylinder probability equals its probability on the box · Bernoulli percolation restricted to a box is Bernoulli on the box · Positive planar percolation at some \(p < 1\) via the Ising model · Positivity of the critical probability (Hammersley's bound) · Monotonicity in \(p\) of the Bernoulli percolation probability · Wired \(q = 2\) origin-to-boundary probability at most Bernoulli · Measurability of the one-arm event · Number of infinite clusters is almost surely constant · Face loop of a boundary orbit in the face-boundary graph · Discrete Jordan separation for finite open clusters · \(p_c(\mathbb{Z}^2) < 1\) assuming simple exit orbits · \(p_c(\mathbb{Z}^2) < 1\) assuming a canonical orbit cycle · Lattice box as a finite set · Sites of a box as a finite set · Aizenman–Barsky inequality on \(\mathbb{Z}^d\) with neighbour row sum · Box as a finite set of sites · Box-crossing event · Connection of a site to the box boundary · Duminil-Copin–Tassion differential inequality · Mean-field lower bound · Exponential decay below p̃_c · One-arm event from the origin · One-arm event from a shifted origin · Crossing inside the box that avoids a cluster · Crossing to the box exterior that avoids a cluster · Exponential decay from a one-step recursion · Sharpness of the phase transition, conditional form · Equality of the Duminil-Copin–Tassion threshold and \(p_c\) · Exponential decay of the one-arm probability below the threshold · Sharpness of the phase transition · Ordered nearest-neighbour pairs touching the box · Box \((-n, n)^d\) as a finite set of sites · Convexity of the set of DLR states · Box energy with a boundary condition · Finite-volume Gibbs measure on configurations of \(\mathbb{Z}^d\) · Finite-volume Gibbs probability with a boundary condition · Finite-volume Gibbs measure as a probability measure · Finite-volume Boltzmann weight with a boundary condition · Finite-volume partition function with a boundary condition · Configuration glued from inside spins and a boundary condition · Uniqueness of the Gibbs state · DLR state of the Ising model on \(\mathbb{Z}^d\) · Ising specification in a box · Ising specification as a Markov kernel · Overwriting a configuration on an inner box · The plus state is a Gibbs (DLR) state · Restriction of a configuration to an inner box · Specification applied to a bounded continuous function · Involution swapping inner-box parts of configuration pairs · Inside configuration with the spins in a set flipped · Flipping spins in a set as an involutive equivalence · Minus cluster of the origin as a finite set · Probability of the contour event of a set · Connected face-boundary graphs at the axis for all realised contours · Tight axis circuit data: contour edges in one axis-face component · Winding hypothesis for outer contours on \(\mathbb{Z}^2\) · Outer contour map: clusters as interiors of boundary circuits · Spin flip inside the box · Spin flip inside the box as an involutive equivalence · Finite-volume magnetization at the origin · Probability that the origin spin is minus · Configuration with only the origin minus · Filled-cluster winding hypothesis · Origin-only minus configuration satisfies the filled-cluster data · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Filled minus cluster of the origin as a finite set · FK critical point is less than one for \(d \ge 2\), \(q \ge 1\) · Inf-based and sup-based Ising critical points agree for \(d \ge 2\) · Sup-based \(\beta_c\) equals \(-\tfrac{1}{2}\log(1 - p_c)\) for \(d \ge 2\) · Existence of the Ising phase transition · Peierls' theorem · Approximation in measure by events measurable outside every box · Nonvacuity of the a.s.-tail theorem via the all-plus Dirac mass · Box sites as a set and as a finite set · Ergodicity of the plus state · Translation invariance of the plus state · Tail event for lattice spin configurations · Extremality of the plus state · Pointwise convergence of box centered free energies · Collapse of average edge densities to the free density · Left-continuity of the free \(q = 2\) edge density in \(t\) · Free \(q = 2\) edge density is monotone in \(p\) on \((0, 1)\) · Wired \(q = 2\) edge density is monotone in \(t\) · Right-continuity of the wired \(q = 2\) edge density in \(t\) · Ambient tilted log normalizer ignores the decidability instance · Non-bulk edge fraction bound from a boundary bound on their count · Limits of tilted log normalizers on a fixed box are attained · A limit shared with growing boxes is one fixed-box graph's value · Tilted log normalizers on a fixed box take finitely many values · Average wired density collapse at \(q = 2\) · Measurability of the percolation event · Wired box-boundary connection probability is monotone in \(p\) at \(q = 2\) · Box edge with a lattice-edge image is a box-graph edge · Open self-avoiding walk in a box gives \(m\) distinct open box edges · Extended box configuration keeps box edge states · Bernoulli bound \(p^m\) for a fixed self-avoiding walk in the box · Percolation gives open self-avoiding walks of every length · Open edges of an extended box configuration are box edges · Wired box bound \((2dp)^m\) on the open-walk event for \(q \ge 1\) · Wired box measure as a finite sum over box configurations · Wired probability that the origin reaches the box boundary · Origin as a vertex of the box graph · Origin lies in every box · Box configuration as a coloring of the next larger box · Restriction of a box coloring to the inner box · Box configurations as box-graph colorings with boundary color \(0\) · Free box measure dominated by the wired one for \(q \ge 1\) · Assumed doubling, boundedness and oscillation data along \(K_j\) · Negative log ambient normalizer of a box · Number of edges of a box · Isomorphism of a box with its translated copy in the predicate part · Isomorphism of a box with its translated copy in the complement part · \(\Lambda_n\) has \(d \cdot 2n(2n+1)^{d-1}\) edges · Dyadic convergence data for the ambient tilted log normalizer · Negative log ambient normalizer of the box \(\Lambda_n\) · Edge count of the box \(\Lambda_n\) · Box free-energy doubling bound along \(K_j\) holds for \(d, q \ge 1\) · Doubling bound for the box free energy when \(q \ge 1\) · Van Hove subadditivity of the box free energy for \(q \ge 1\) · Per-edge free energy converges along \(K_j\) for \(d, q \ge 1\) · Edge-normalized box free energy of the random-cluster model · Per-edge box free energy · Van Hove limit · Uniform upper bound on the box free energy for \(d, n, q \ge 1\) · Box free energy \(-\log Z^E\) of the random-cluster model · Box Fekete data from a uniform bound and an oscillation bound · Additive doubling bound for \(-\log Z\) of the free \(q = 2\) FK model · The hyperplane block has at most \(2d|J|\) edges · Orthant blocks have the FK partition function of \(\Lambda_K\) · Vertex degrees in a box are at most \(2d\) · Doubling inequality for \(-\log Z\) of the free \(q = 2\) FK model · Orthant tag of a site of \(\Lambda_{2K+1}\) · Coordinate description of the sites with a given orthant tag · Bound on the edge gap \(|E(\Lambda_{2K+1})| - 2^d |E(\Lambda_K)|\) · \(\Lambda_{2K+1}\) has at least \(2^d\) times as many edges as \(\Lambda_K\) · Lower bound \(n(2n+1)^{d-1}\) on the number of edges of \(\Lambda_n\) · Hyperplane set of \(\Lambda_{2K+1}\) · The hyperplane set has at most \(d(4K+3)^{d-1}\) sites · Hyperplane set lies in the union of the coordinate slabs · Coordinate slab of \(\Lambda_{2K+1}\) · A coordinate slab has at most \((4K+3)^{d-1}\) sites · Translation of \(\Lambda_K\) onto an orthant block of \(\Lambda_{2K+1}\) · The all-tag restriction has the partition function of \(\Lambda_{2K+1}\) · At most \(2d|J|\) edges straddle an orthant tag · An edge leaving an orthant ends on a coordinate hyperplane · An edge between differently tagged sites meets a coordinate hyperplane · Edges straddling a tag are incident to the hyperplane set · Summability of doubling corrections relative to edge counts · Untagged sites are exactly those on a coordinate hyperplane · Wired box measure dominates the induced-wiring measure for \(q \ge 1\) · Domain Markov property for the wired measure on nested boxes · Edge product of a glued configuration factorizes · Component decomposition of the wired glued graph · Component map into the wired glued graph · Glued and inner graphs have the same connections on the box · Induced wiring lies below the inner boundary clique · Wired cluster count of a glued configuration splits additively · Outer Bernoulli edge factor of an outer configuration · Gluing a box configuration into an outer configuration · Wired glued open graph is the union of inner and outer graphs · Box-boundary profile tends to \(\theta(p,2)\) if wired probabilities do · Vertex boundary of a box · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Extension of a box configuration by closed edges · Free random-cluster measure on a box · Wired random-cluster measure on a box · FKG inequality for free \(q = 2\) box measures on smaller-box events · FKG inequality for wired \(q = 2\) box measures on smaller-box events · Translation covariance of free box masses · Translation covariance of wired box masses · Wired box measure of an all-open event equals its box mass · Free box measure of an all-open event equals its box mass · Free translation invariance from free placements of every shift · Equal free probabilities from eventually equal translated masses · Free placement for a shift via eventually equal box masses · Difference of wired all-open masses of an edge set and its translate · Wired translation invariance from wired placements of every shift · Equal wired probabilities from eventually equal translated masses · Wired placement for a shift via eventually equal box masses · Closed annulus plus inner-boundary wiring gives wired \(\Lambda_n\) law · Closed-annulus wired bound on origin-to-\(\partial\Lambda_n\), \(q = 2\) · Wired crossing probabilities converge to the percolation probability · Crossing events intersect to the percolation event · Conditional free probabilities depend only on the outer configuration · Domain Markov property · Conditional free measure as an induced-wiring measure · One-step growth of free \(q = 2\) measures of increasing cylinders · Fibre-mass factorization of random-cluster probabilities · Conditional free measure dominates the smaller free box for \(q \ge 1\) · Free measure is dominated by induced-wiring measures for \(q \ge 1\) · Random-cluster weight of a glued configuration factorizes · Free box measure of a cylinder event as a finite sum · Increasing box events gain free \(q = 2\) probability in the next box · Next-box free measure of a cylinder event as a finite sum · Decomposition of the free measure over the outer configuration · One-step box monotonicity of free measures for \(q \ge 1\) · Injectivity of the free cluster map · Surjectivity of the free cluster map · Glued open edges at outer vertices are outer edges · Inner-graph connections are glued-graph connections · Conditional partition function in terms of the induced wiring · Glued connections between inner vertices are inner-graph connections · Outer open connections give connections in the inner graph · Cluster count of a glued configuration splits additively · Glued open graph is the union of inner and outer open edges · Positivity of the outer weight factor · Fibre masses of the free measure sum to one · Secant bound gives free–wired density agreement off a countable set · Off-centre carrier vanishes by translation covariance · Free density is at most each translated wired marginal · Translated wired marginals converge to the wired density · Equal wired densities from equal translated marginals · Inclusion of the annulus wiring into the extra-wired graph · Box as an induced subgraph of the next box · Inclusion of box vertices into the next box · Domain Markov property for the wired box measure · Extended-graph components as inner components plus annulus vertices · Extra-wired components as inner plus annulus-wiring components · Extension of a configuration closing the annulus edges · Extended open graph with the inner box boundary wired · Vertex on the boundary of the inner box · Edges of the next box coming from the inner box · Configurations closed off the inner edges as inner-box configurations · Open graph of a box configuration with the box boundary wired · Inclusion of the wired inner graph into the extended wired graph · Inclusion of the wired inner graph into the extra-wired graph · Vertex of the next box lying in the inner box · Number of next-box edges not coming from the inner box · Wired \(q = 2\) increasing-event probabilities do not grow with the box · A connection to outside the box passes through the box boundary · Crossing probabilities converge to the percolation probability · Uniform decay of two-point connectivity without percolation · Free box measure of a box connection event is the two-point function · Convergence to the free two-point function under stochastic increase · Cylinder events of a box are clopen · Convergence to the wired two-point function under stochastic decrease · Outer projection agrees with the configuration off \(\Lambda_n\) · Boundary connection inside \(\Lambda_n\) reaches outside \(\Lambda_{n-1}\) · Open path from the origin out of \(\Lambda_n\) gives \(0 \leftrightarrow \partial\Lambda_n\) inside \(\Lambda_n\) · Inner vertices next to the annulus lie on \(\partial\Lambda_n\) · Open lattice edges between box vertices are open box edges · Box inclusion maps the origin to the origin · Inclusion of \(\Lambda_n\) into \(\Lambda_m\) for \(n \le m\) · Conditional wired decrease on inner increasing events for \(q \ge 1\) · Paths to \(\partial\Lambda_{n+1}\) pass through \(\partial\Lambda_n\) · Open connections in a box are open connections in \(\mathbb{Z}^d\) · Leaving \(\Lambda_n\) implies connecting to \(\partial\Lambda_n\) · Edge inclusion into \(\mathbb{Z}^d\) factors through \(\Lambda_m\) · Configurations with a given outer part form its conditioning fibre · Cylinder form of the \(\Lambda_n\) boundary connection is measurable · Open edges of \(\Lambda_n\) are open edges of \(\Lambda_{n+1}\) · Open edges of a box are open edges of \(\mathbb{Z}^d\) · Outer projection closes the edges of \(\Lambda_n\) · Outer projection keeps the edges outside \(\Lambda_n\) · Outer projection is idempotent · Masses of the conditioning fibres sum to one · Infinite-volume limit of the wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_k\) · Wired \(\Lambda_m\) measure of a \(\Lambda_m\) cylinder event as a sum · Wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_{n+1}\) at most in \(\Lambda_n\) · Wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_{m+1}\) at most in \(\Lambda_m\), \(m \ge n\) · Wired box measures decrease on increasing cylinder events at \(q = 2\) · Wired \(\Lambda_{n+1}\) measure of a \(\Lambda_n\) cylinder event as a sum · Wired \(\Lambda_{n+1}\) measure decomposed over outer configurations · Wired box measures decrease on inner increasing events for \(q \ge 1\) · Boxes satisfy the additive doubling bound for \(d \ge 1\) · Van Hove tiling bound for the edge partition function · Graph isomorphism between a sub-box and a tiling cell · Translation between a sub-box and a tiling cell · Per-edge free energy of a box in the tilt variable · Per-edge negative log edge partition function of a box · Per-box \(q = 2\) uniqueness off a countable set of tilts · Convergence of the per-edge free energy of boxes · Per-edge free energy of boxes converges for \(d \ge 1\) · Sub-box as an induced subgraph of a larger box · Membership of a box vertex in a sub-box · Negative log edge partition function of a box · Tiling cell of a box vertex · Wired-marginal difference between a box and its translate · Secant bound gives \(q = 2\) edge-event uniqueness off a countable set · Convex limit of centered tilt free energies of boxes for \(d, q \ge 1\) · Per-box uniqueness of the random-cluster measures off a countable set · Free unit-edge marginal at \(0\) on \(\Lambda_{\lfloor\sqrt n\rfloor}\) · Wired unit-edge marginal at \(0\) on \(\Lambda_{\lfloor\sqrt n\rfloor}\) · Countable-exception \(q = 2\) uniqueness from one-sided derivative data · Free average edge density collapse on boxes · Free densities of genuine box edges as left derivatives · Wired average edge density collapse on boxes · Wired densities of genuine box edges as right derivatives · Per-coordinate free energy on a box · Free-energy data give \(q = 2\) box uniqueness off countably many \(t\) · Two-sided free \(q = 2\) bulk bounds from the free sandwich · Free \(q = 2\) bulk sandwich from equal free edge densities · Two-sided wired \(q = 2\) bulk bounds from the wired sandwich · Wired \(q = 2\) bulk sandwich from equal wired edge densities · Bulk edges of \(\Lambda_n\) · Adjacent box vertices differ by a signed unit vector · Vanishing shell edge fraction when \((n - m(n))/n \to 0\) · Lower bound on free bulk edge marginals · Free off-centre lower bound by the recentred small-box marginal · Free off-centre sandwich from free rotation residues · Free rotation residue for a box pair · Unit edge \(\{0, \pm e_j\}\) of a box · Free unit-edge marginals converge to the free density · Wired unit-edge marginals converge to the wired density · Free unit-edge marginal in the square-root box · Wired unit-edge marginal in the square-root box · Wired bulk edges of \(\Lambda_n\) · Upper bound on wired bulk edge marginals · Wired off-centre sandwich from wired rotation residues · Wired off-centre upper bound by the recentred small-box marginal · Wired rotation residue for a box pair · Unit edges at the origin have the free density of \(\{0, e_0\}\) · Box symmetries preserve the free \(q = 2\) density of any pair of sites · All box edges have the same free \(q = 2\) density · Coordinate permutation as a box symmetry · Unit edges at the origin have the wired density of \(\{0, e_0\}\) · Box symmetries preserve the wired \(q = 2\) density of any pair of sites · All box edges have the same wired \(q = 2\) density · Average wired \(q = 2\) edge density of a box as a mean of marginals · Free \(q = 2\) edge density lies in \((0, 1)\) · Free growing-box collapse at \(q = 2\) · Free uniform bulk deviation at \(q = 2\) · Wired \(q = 2\) edge density lies in \((0, 1)\) · Wired uniform bulk deviation at \(q = 2\) · Box symmetry of \(\mathbb{Z}^d\) · Box symmetries preserve the free \(q = 2\) density of box edges · Coordinate reflection as a box symmetry · Box symmetries preserve the wired \(q = 2\) density of box edges · Translation covariance of FK edge marginals on boxes · Translated box in \(\mathbb{Z}^d\) · Some translated box leaves the centered box for \(d \ge 1\) · Translation from the centered box onto a translated box · Restriction of a box symmetry to a box · Translation invariance of the free \(q = 2\) infinite-volume measure · Free off-centre sandwich hypothesis · Free \(q = 2\) box edge marginals are at most the free density · Wired off-centre sandwich hypothesis · Wired \(q = 2\) box edge marginals are at least the wired density · Translate of a vertex of \(\Lambda_N\) as a vertex of \(\Lambda_{N+r}\) · Ergodicity of the wired random-cluster measure · Disjoint-box cap hypothesis for multi-open events · Conditional product cap for multi-open events in boxes · Unordered pair of two sites of a box \(\Lambda_N\) · Translation invariance of free and wired densities if marginals merge · An edge and its translate lie in a common centered box · Constant free density gives an upper bound on expected open edges · Free upper bound on expected open edges along a box-symmetry orbit · Equal free densities from merging free marginals · Translation invariance of the free density given merging marginals · A site and its translate lie in a common centered box · Unit translations are not box symmetries · Constant wired density gives a lower bound on expected open edges · Wired lower bound on expected open edges along a box-symmetry orbit · Equal wired densities from merging wired marginals · Translation invariance of the wired density given merging marginals · Box edge set included into \(\Lambda_m\) and translated by \(v\) · Translation invariance of the wired \(q = 2\) infinite-volume measure · Wired box products approximate infinite-volume products · Every finite family of edge sets is realized in some box · Realized edge sets stay realized in larger boxes · Upper decorrelation of the wired measure from factorization · All-open Dirac mass satisfies the factorization bound · Wired \(q = 2\) measure is ergodic under the factorization bound · Free box integral of an edge indicator is the free edge marginal · Wired box integral of an edge indicator is the wired edge marginal · Free translation invariance from the placement hypothesis · Identity shift satisfies the free placement hypothesis · Wired all-open probability on a translated box · Translated wired box mass equals the centered box mass · Translated free box mass of an edge set · Translated free box mass equals the centred box probability · Translated box edges are shifted centered box edges · Wired translation invariance from the placement hypothesis · Identity shift satisfies the wired placement hypothesis · Boundary covariance error · Box \(\Lambda_n\) as a type · Origin–site covariance in a box · Nearest-neighbour graph on a box · Membership of a larger-box site in a smaller box · Smaller box as a subtype of a larger box · Free-boundary site magnetization in a box · Origin as a site of a box · All sites of a box · Lattice site as a box site, defaulting to the origin · Edge with exactly one endpoint in a cut set · Boundary error of the finite-volume mean-field inequality · Cut mass of a box set rooted at the field ghost · Lattice sites underlying a set of box sites · Identification of a box cut set with its lattice sites · Boundary correlation of an edge crossing a cut · Exterior neighbours of a site · External boundary correlation of a cut, over edges leaving the box · Pairs of a box site and an outside lattice neighbour · Finite-volume mean-field inequality for the Ising model · Field switched off on the outer layer · Origin magnetization with the outer-layer field switched off · Internal boundary correlation of a cut in the box · Minimal origin-to-site magnetization ratio in a box · Mean-field lower bound for the spontaneous magnetization · Oriented cut mass over cuts \(T \ni 0, x\) with \(y \notin T\) · \(\beta\)-derivative of the origin magnetization in a box · Covariance sum over the outer layer · Outer-layer indicator as a field direction · Translation onto a translated box · Translated box \(\Lambda_n - y\) · Membership of a doubled-box site in a translated box · Translated box as a subtype of the doubled box · Sharpness of the Ising phase transition on \(\mathbb{Z}^d\), \(d \ge 2\) · Auxiliary critical point \(\tilde\beta_c(d)\) is positive for \(d \ge 2\) · Simon–Lieb inequality in the infinite-volume plus state · Outer vertex boundary of a box

DefinitionInner vertex boundary of a box#✓fully proved

The inner vertex boundary of box d n: sites of box d n that are not in box d (n - 1).

def vertexBoundary (d n : ℕ) : Set (Site d) := box d n \ box d (n - 1)

Uses 2 · Used by 31

Statement usesSite of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used bySize of the vertex boundary of the box \((-n, n)^d\) · Positive planar percolation at some \(p < 1\) via the Ising model · Box-crossing event · Connection of a site to the box boundary · Duminil-Copin–Tassion differential inequality · Mean-field lower bound · Sharpness of the phase transition · FK critical point is less than one for \(d \ge 2\), \(q \ge 1\) · Inf-based and sup-based Ising critical points agree for \(d \ge 2\) · Sup-based \(\beta_c\) equals \(-\tfrac{1}{2}\log(1 - p_c)\) for \(d \ge 2\) · Existence of the Ising phase transition · Box configurations as box-graph colorings with boundary color \(0\) · Induced wiring lies below the inner boundary clique · Vertex boundary of a box · Translation covariance of wired box masses · Closed-annulus wired bound on origin-to-\(\partial\Lambda_n\), \(q = 2\) · Inclusion of the annulus wiring into the extra-wired graph · Extended-graph components as inner components plus annulus vertices · Extra-wired components as inner plus annulus-wiring components · Vertex on the boundary of the inner box · Inclusion of the wired inner graph into the extended wired graph · Inclusion of the wired inner graph into the extra-wired graph · Boundary connection inside \(\Lambda_n\) reaches outside \(\Lambda_{n-1}\) · Paths to \(\partial\Lambda_{n+1}\) pass through \(\partial\Lambda_n\) · Per-box \(q = 2\) uniqueness off a countable set of tilts · Per-box uniqueness of the random-cluster measures off a countable set · Box symmetries preserve the wired \(q = 2\) density of box edges · Translation covariance of FK edge marginals on boxes · Vertex boundary of a translated box · Ergodicity of the wired random-cluster measure · Outer vertex boundary of a box

DefinitionEdge boundary of a set of sites#✓fully proved

The edge boundary of a set S of sites: ordered nearest-neighbour pairs with exactly one endpoint in S.

def edgeBoundary (d : ℕ) (S : Set (Site d)) : Set (Site d × Site d) :=
  {p | (hypercubicLattice d).Adj p.1 p.2 ∧ (p.1 ∈ S ↔ p.2 ∉ S)}

Uses 2 · Used by 6

Statement usesSite of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\)

Used by\(p_c(2) < 1\) from anchored dual-circuit enclosure · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Peierls' theorem · Finite cluster in \(\mathbb{Z}^2\) gives a closed lattice circuit · Finite cluster in \(\mathbb{Z}^2\): closed circuit, separated point, odd crossings

TheoremEvery finite set of sites lies in a box#✓fully proved

Every finite set of sites lies in some box box d R.

theorem finite_subset_box {d : ℕ} (F : Set (Site d)) (hF : F.Finite) : ∃ R : ℕ, F ⊆ box d R

Uses 2 · Used by 25

Statement usesSite of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byComplement of a finite set in \(\mathbb{Z}^d\) has one infinite component · Bounded regions are the components other than the outer one · Bounded faces of a finite lattice graph are counted by its cycle rank · Radius of a box containing a planar lattice subgraph · The inner face component is finite · A face far outside the walk has ray parity zero · Lattice Jordan curve theorem, even-odd form · Number of cells is at most the nullity of the skeleton · Hopf's Umlaufsatz · Number of infinite clusters is almost surely constant · Discrete Jordan separation for finite open clusters · Mean-field lower bound · Sharpness of the phase transition, conditional form · Equality of the Duminil-Copin–Tassion threshold and \(p_c\) · Exponential decay of the one-arm probability below the threshold · Sharpness of the phase transition · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Inf-based and sup-based Ising critical points agree for \(d \ge 2\) · Peierls' theorem · Measurability of the percolation event · Crossing events intersect to the percolation event · Sharpness of the Ising phase transition on \(\mathbb{Z}^d\), \(d \ge 2\) · Auxiliary critical point \(\tilde\beta_c(d)\) is positive for \(d \ge 2\) · Simon–Lieb inequality in the infinite-volume plus state

TheoremIncreasing one coordinate stays in the same component#✓fully proved

In ℤ², increasing one coordinate by n stays in the same component.

theorem reachable_update_add (x : Site 2) (j : Fin 2) (a : ℤ) (n : ℕ) :
    (hypercubicLattice 2).Reachable (Function.update x j a) (Function.update x j (a + n))

Uses 2 · Used by 1

Statement usesSite of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\)

Used byChanging one coordinate stays in the same component

TheoremChanging one coordinate stays in the same component#✓fully proved

In ℤ², changing one coordinate stays in the same component.

theorem reachable_update (x : Site 2) (j : Fin 2) (a b : ℤ) :
    (hypercubicLattice 2).Reachable (Function.update x j a) (Function.update x j b)

Uses 3 · Used by 1

Statement usesSite of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\)

Proof usesIncreasing one coordinate stays in the same component

Used bySquare lattice is connected

TheoremSquare lattice is connected#✓fully proved

The square lattice ℤ² is connected.

theorem hypercubicLattice_two_reachable (x y : Site 2) : (hypercubicLattice 2).Reachable x y

Uses 3 · Used by 5

Statement usesSite of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\)

Proof usesChanging one coordinate stays in the same component

Used byBounded faces of a finite lattice graph are counted by its cycle rank · Chosen lattice walk between two faces · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Peierls' theorem

DefinitionBox \((-n, n)^d\) as a finite set of sites#✓fully proved

The box [-n, n]^d as a finite set of sites.

noncomputable def boxSV_boxF (d n : ℕ) : Finset (Site d) :=
  Fintype.piFinset (fun _ => Finset.Icc (-(n : ℤ)) n)

Uses 1 · Used by 17

Statement usesSite of the hypercubic lattice

Used byNearest-neighbour pairs inside the box \((-n, n)^d\) · Box sites with a forward neighbour in the box · Vertex boundary of the box \((-n, n)^d\) as a finite set · \(\Lambda_n\) has \(d \cdot 2n(2n+1)^{d-1}\) edges · \(2n(2n+1)^{d-1}\) sites of \(\Lambda_n\) stay inside after a unit shift · Ordered pairs in different directions are disjoint · Pairs in direction \(i\) are the forward and backward shifts · Ordered neighbour pairs of \(\Lambda_n\) as a union over directions · Uniform upper bound on the box free energy for \(d, n, q \ge 1\) · Lower bound \(n(2n+1)^{d-1}\) on the number of edges of \(\Lambda_n\) · Sites of \(\Lambda_n\) whose shift in coordinate \(i\) stays in the box · Unit shifts of sites staying in the box are pairs in direction \(i\) · Per-box \(q = 2\) uniqueness off a countable set of tilts · Per-edge free energy of boxes converges for \(d \ge 1\) · Per-box uniqueness of the random-cluster measures off a countable set · Shell edge fraction is at most \(4d^2(n-m)/n\) · Vanishing shell edge fraction when \((n - m(n))/n \to 0\)

DefinitionVertex boundary of the box \((-n, n)^d\) as a finite set#✓fully proved

The vertex boundary of [-n, n]^d as a finite set of sites.

noncomputable def boxSV_vbF (d n : ℕ) : Finset (Site d) :=
  boxSV_boxF d n \ boxSV_boxF d (n - 1)

Uses 2 · Used by 2

Statement usesSite of the hypercubic lattice · Box \((-n, n)^d\) as a finite set of sites

Used byPer-box \(q = 2\) uniqueness off a countable set of tilts · Per-box uniqueness of the random-cluster measures off a countable set

DefinitionSize of the vertex boundary of the box \((-n, n)^d\)#✓fully proved

The number of sites in the vertex boundary of [-n, n]^d.

noncomputable def boxSV_boundaryCard (d n : ℕ) : ℕ :=
  (vertexBoundary_finite d n).toFinset.card

Uses 3 · Used by 2

Statement usesSite of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Inner vertex boundary of a box

Used byPer-box \(q = 2\) uniqueness off a countable set of tilts · Per-box uniqueness of the random-cluster measures off a countable set

DefinitionNearest-neighbour pairs inside the box \((-n, n)^d\)#✓fully proved

The ordered pairs of nearest-neighbour sites that both lie in [-n, n]^d.

noncomputable def boxSV_edgeF (d n : ℕ) : Finset (Site d × Site d) :=
  ((boxSV_boxF d n) ×ˢ (boxSV_boxF d n)).filter
    (fun p => (∑ i, (p.1 i - p.2 i).natAbs) = 1)

Uses 2 · Used by 13

Statement usesSite of the hypercubic lattice · Box \((-n, n)^d\) as a finite set of sites

Used byNumber of nearest-neighbour pairs inside the box \((-n, n)^d\) · \(\Lambda_n\) has \(d \cdot 2n(2n+1)^{d-1}\) edges · Ordered pairs in different directions are disjoint · Ordered nearest-neighbour pairs of \(\Lambda_n\) in direction \(i\) · Pairs in direction \(i\) are the forward and backward shifts · \(\Lambda_n\) has \(4dn(2n+1)^{d-1}\) ordered nearest-neighbour pairs · Ordered neighbour pairs of \(\Lambda_n\) as a union over directions · Lower bound \(n(2n+1)^{d-1}\) on the number of edges of \(\Lambda_n\) · Unit shifts of sites staying in the box are pairs in direction \(i\) · Per-box \(q = 2\) uniqueness off a countable set of tilts · Per-box uniqueness of the random-cluster measures off a countable set · Shell edge fraction is at most \(4d^2(n-m)/n\) · Vanishing shell edge fraction when \((n - m(n))/n \to 0\)

DefinitionNumber of nearest-neighbour pairs inside the box \((-n, n)^d\)#✓fully proved

The number of ordered nearest-neighbour pairs inside [-n, n]^d.

noncomputable def boxSV_edgeCard (d n : ℕ) : ℕ := (boxSV_edgeF d n).card

Uses 2 · Used by 7

Statement usesSite of the hypercubic lattice · Nearest-neighbour pairs inside the box \((-n, n)^d\)

Used by\(\Lambda_n\) has \(d \cdot 2n(2n+1)^{d-1}\) edges · \(\Lambda_n\) has \(4dn(2n+1)^{d-1}\) ordered nearest-neighbour pairs · Lower bound \(n(2n+1)^{d-1}\) on the number of edges of \(\Lambda_n\) · Per-box \(q = 2\) uniqueness off a countable set of tilts · Per-box uniqueness of the random-cluster measures off a countable set · Shell edge fraction is at most \(4d^2(n-m)/n\) · Vanishing shell edge fraction when \((n - m(n))/n \to 0\)

DefinitionBox sites with a forward neighbour in the box#✓fully proved

Sites of [-n, n]^d whose successor in the first coordinate direction is still in the box.

noncomputable def boxSV_fwdDom (d n : ℕ) (hd : 1 ≤ d) : Finset (Site d) :=
  (boxSV_boxF d n).filter (fun x => x ⟨0, hd⟩ + 1 ∈ Finset.Icc (-(n : ℤ)) n)

Uses 2 · Used by 4

Statement usesSite of the hypercubic lattice · Box \((-n, n)^d\) as a finite set of sites

Used byLower bound \(n(2n+1)^{d-1}\) on the number of edges of \(\Lambda_n\) · Per-box \(q = 2\) uniqueness off a countable set of tilts · Per-box uniqueness of the random-cluster measures off a countable set · Shell edge fraction is at most \(4d^2(n-m)/n\)

DefinitionFirst index where a walk reaches a coordinate value#✓fully proved

The first index at which the walk w has k-th coordinate equal to r.

noncomputable def pvr_firstIdxAtCoord {a b : Site 2} (w : (hypercubicLattice 2).Walk a b)
    (k : Fin 2) (r : ℤ) (h : ∃ i, (w.getVert i) k = r) : ℕ :=
  Nat.find h

Uses 2

Statement usesSite of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\)

DefinitionShift of a site along a coordinate#✓fully proved

The site obtained from x by adding s to its j-th coordinate.

def shift (d : ℕ) (x : Site d) (j : Fin d) (s : ℤ) : Site d :=
  Function.update x j (x j + s)

Uses 1 · Used by 26

Statement usesSite of the hypercubic lattice

Used byNeighbour of a site in a coordinate direction · Bounded faces of a finite lattice graph are counted by its cycle rank · Pushed-forward subgraphs are locally finite · Anchored dual cycles of a given length · \(p_c(2) < 1\) from anchored dual-circuit enclosure · Finite face set containing the face-boundary support · Support of the face-boundary graph of a finite set · Face-boundary graph of a finite set as a planar subgraph · Origin-only minus configuration satisfies the filled-cluster data · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Peierls' theorem · Finite cluster in \(\mathbb{Z}^2\) gives a closed lattice circuit · Finite cluster in \(\mathbb{Z}^2\): closed circuit, separated point, odd crossings · Vertex degrees in a box are at most \(2d\) · Per-box uniqueness of the random-cluster measures off a countable set · Free \(q = 2\) bulk sandwich from equal free edge densities · Wired \(q = 2\) bulk sandwich from equal wired edge densities · Shell edge fraction is at most \(4d^2(n-m)/n\) · Adjacent box vertices differ by a signed unit vector · Free off-centre sandwich from free rotation residues · Wired off-centre sandwich from wired rotation residues · Adjacent sites differ by a signed unit vector · Exterior neighbours of a site · Mean-field lower bound for the spontaneous magnetization · Simon–Lieb inequality in the infinite-volume plus state

DefinitionNeighbour of a site in a coordinate direction#✓fully proved

The neighbour of x in direction j, positive if the flag is true and negative otherwise.

def candMap (d : ℕ) (x : Site d) : Fin d × Bool → Site d :=
  fun p => shift d x p.1 (if p.2 then 1 else -1)

Uses 2 · Used by 35

Statement usesSite of the hypercubic lattice · Shift of a site along a coordinate

Used byNearest neighbours of a lattice site · Bounded faces of a finite lattice graph are counted by its cycle rank · Pushed-forward subgraphs are locally finite · Anchored dual cycles of a given length · \(p_c(2) < 1\) from anchored dual-circuit enclosure · Finite face set containing the face-boundary support · Support of the face-boundary graph of a finite set · Face-boundary graph of a finite set as a planar subgraph · Origin-only minus configuration satisfies the filled-cluster data · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Peierls' theorem · Finite cluster in \(\mathbb{Z}^2\) gives a closed lattice circuit · Finite cluster in \(\mathbb{Z}^2\): closed circuit, separated point, odd crossings · Vertex degrees in a box are at most \(2d\) · Per-box uniqueness of the random-cluster measures off a countable set · Free \(q = 2\) bulk sandwich from equal free edge densities · Wired \(q = 2\) bulk sandwich from equal wired edge densities · Shell edge fraction is at most \(4d^2(n-m)/n\) · Adjacent box vertices differ by a signed unit vector · Lower bound on free bulk edge marginals · Free off-centre sandwich from free rotation residues · Unit edge \(\{0, \pm e_j\}\) of a box · Free unit-edge marginals converge to the free density · Wired unit-edge marginals converge to the wired density · Upper bound on wired bulk edge marginals · Wired off-centre sandwich from wired rotation residues · Adjacent sites differ by a signed unit vector · Unit edges at the origin have the free density of \(\{0, e_0\}\) · Every lattice edge has the free \(q = 2\) density of \(\{0, e_0\}\) · Reference edge \(\{0, e_0\}\) of \(\mathbb{Z}^d\) · Unit edges at the origin have the wired density of \(\{0, e_0\}\) · Every lattice edge has the wired \(q = 2\) density of \(\{0, e_0\}\) · Exterior neighbours of a site · Mean-field lower bound for the spontaneous magnetization

DefinitionNearest neighbours of a lattice site#✓fully proved

The finite set of the 2d nearest neighbours of x.

def candFinset (d : ℕ) (x : Site d) : Finset (Site d) :=
  Finset.univ.image (candMap d x)

Uses 2 · Used by 17

Statement usesSite of the hypercubic lattice · Neighbour of a site in a coordinate direction

Used byBounded faces of a finite lattice graph are counted by its cycle rank · Pushed-forward subgraphs are locally finite · Anchored dual cycles of a given length · \(p_c(2) < 1\) from anchored dual-circuit enclosure · Finite face set containing the face-boundary support · Support of the face-boundary graph of a finite set · Face-boundary graph of a finite set as a planar subgraph · Origin-only minus configuration satisfies the filled-cluster data · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Peierls' theorem · Finite cluster in \(\mathbb{Z}^2\) gives a closed lattice circuit · Finite cluster in \(\mathbb{Z}^2\): closed circuit, separated point, odd crossings · Vertex degrees in a box are at most \(2d\) · Shell edge fraction is at most \(4d^2(n-m)/n\) · Exterior neighbours of a site · Mean-field lower bound for the spontaneous magnetization

Definition\(\ell^1\) distance on \(\mathbb{Z}^d\)#✓fully proved

The ℓ¹ (graph) distance ∑ i, |x i - y i| between two sites.

def l1dist (d : ℕ) (x y : Site d) : ℕ := ∑ i, (x i - y i).natAbs

Uses 1 · Used by 9

Statement usesSite of the hypercubic lattice

Used by\(p_c(\mathbb{Z}^2) < 1\) assuming simple exit orbits · \(p_c(\mathbb{Z}^2) < 1\) assuming a canonical orbit cycle · \(p_c(\mathbb{Z}^2) < 1\) via boundary connectivity, assuming linked exits · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Peierls' theorem · Simon radius of a finite set · Tail set of plus-state correlations · Sharpness of the Ising phase transition on \(\mathbb{Z}^d\), \(d \ge 2\)

DefinitionExterior of a box in \(\mathbb{Z}^d\)#✓fully proved

The exterior of the box [-R, R]^d: sites with some coordinate of absolute value greater than R.

def exterior (d R : ℕ) : Set (Site d) := {x | ∃ i, R < (x i).natAbs}

Uses 1 · Used by 15

Statement usesSite of the hypercubic lattice

Used byComplement of a finite set in \(\mathbb{Z}^d\) has one infinite component · Bounded regions are the components other than the outer one · Box exterior embeds in the region graph · Bounded faces of a finite lattice graph are counted by its cycle rank · Exterior of a box maps into the face-region graph · The inner face component is finite · Lattice Jordan curve theorem, even-odd form · Number of cells is at most the nullity of the skeleton · Hopf's Umlaufsatz · Discrete Jordan separation for finite open clusters · Box exterior maps into the lattice minus boundary edges · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Filled minus cluster of the origin as a finite set · Peierls' theorem

DefinitionSetting a set of coordinates of a lattice site#✓fully proved

The site obtained from p by setting every coordinate in T to v.

def setOn (p : Site d) (T : Finset (Fin d)) (v : ℤ) : Site d :=
  fun k => if k ∈ T then v else p k

Uses 1 · Used by 12

Statement usesSite of the hypercubic lattice

Used byComplement of a finite set in \(\mathbb{Z}^d\) has one infinite component · Bounded regions are the components other than the outer one · Bounded faces of a finite lattice graph are counted by its cycle rank · The inner face component is finite · Lattice Jordan curve theorem, even-odd form · Number of cells is at most the nullity of the skeleton · Hopf's Umlaufsatz · Discrete Jordan separation for finite open clusters · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Filled minus cluster of the origin as a finite set · Peierls' theorem

DefinitionBase point of the exterior of a box#✓fully proved

The site (R + 1, …, R + 1), a fixed base point of the exterior of box d R.

def beacon (d R : ℕ) : Site d := fun _ => (R : ℤ) + 1

Uses 1 · Used by 16

Statement usesSite of the hypercubic lattice

Used byComplement of a finite set in \(\mathbb{Z}^d\) has one infinite component · Bounded regions are the components other than the outer one · Bounded faces of a finite lattice graph are counted by its cycle rank · Outer face region of a planar lattice subgraph · Outer region of the rotated region graph · The inner face component is finite · A face far outside the walk has ray parity zero · Lattice Jordan curve theorem, even-odd form · Number of cells is at most the nullity of the skeleton · Hopf's Umlaufsatz · Discrete Jordan separation for finite open clusters · Exterior component of the complement of a set · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Filled minus cluster of the origin as a finite set · Peierls' theorem

TheoremComplement of a finite set in \(\mathbb{Z}^d\) has one infinite component#✓fully proved

For d ≥ 2, the complement of a finite set of sites of ℤ^d has exactly one infinite connected component.

theorem unique_infinite_component (hd : 2 ≤ d) (F : Set (Site d)) (hF : F.Finite) :
    ∃! C : ((hypercubicLattice d).induce Fᶜ).ConnectedComponent, C.supp.Infinite

Uses 7

Statement usesSite of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\)

Proof usesBase point of the exterior of a box · Box \((-n, n)^d\) in the hypercubic lattice · Exterior of a box in \(\mathbb{Z}^d\) · Every finite set of sites lies in a box · Setting a set of coordinates of a lattice site

25 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.