The lattice magnetization as a wired one-point function on the box graph

DefinitionBoolean spin of a two-state color#✓fully proved

The Boolean spin of a two-state color: 0 ↦ true.

def fToB (a : Fin 2) : Bool := a = 0

Used by 2

Used byRestriction of a box coloring to the inner box · Box configurations as box-graph colorings with boundary color \(0\)

DefinitionRestriction of a box coloring to the inner box#✓fully proved

The configuration in Λ_n obtained by restricting a two-state coloring of Λ_{n+1}.

noncomputable def boxToLat (d n : ℕ) (σ : boxVerts d (n + 1) → Fin 2) :
    {x // x ∈ box d n} → Bool :=
  fun x => fToB (σ ⟨x.1, box_subset_succ d n x.2⟩)

Uses 4 · Used by 1

Statement usesVertices of the box \((-n, n)^d\) · Boolean spin of a two-state color · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byBox configurations as box-graph colorings with boundary color \(0\)

DefinitionBox configurations as box-graph colorings with boundary color \(0\)#✓fully proved

Configurations in Λ_n correspond to two-state colorings of Λ_{n+1} with boundary color 0.

StatMech.IsingFK.hbx_latBoxEquiv · 18 lines

noncomputable def hbx_latBoxEquiv (d n : ℕ) :
    ({x // x ∈ box d n} → Bool) ≃
      {σ : boxVerts d (n + 1) → Fin 2 // BoundaryFixed (boxBoundary d (n + 1)) (0 : Fin 2) σ} where
  toFun τ := ⟨latToBox d n τ, boundaryFixed_latToBox d n τ⟩
  invFun σ := boxToLat d n σ.1
  left_inv τ := by
    funext x
    change boxToLat d n (latToBox d n τ) x = τ x
    unfold boxToLat latToBox
    rw [dite_eq_left x.2, hbx_fToB_bToF]
  right_inv σ := by
    apply Subtype.ext
    funext v
    change latToBox d n (boxToLat d n σ.1) v = σ.1 v
    unfold latToBox boxToLat
    by_cases h : (v : Site d) ∈ box d n
    · rw [dite_eq_left h, hbx_bToF_fToB]
    · rw [dite_eq_right h]; exact (σ.2 v ((hbx_boxBoundary_succ_iff d n v).mpr h)).symm

Uses 10 · Used by 5

Statement usesVertex boundary of a box · Vertices of the box \((-n, n)^d\) · Coloring fixed to a color on the boundary · Two-state color of a Boolean spin · Restriction of a box coloring to the inner box · Boolean spin of a two-state color · Box configuration as a coloring of the next larger box · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Inner vertex boundary of a box

Used byPositive planar percolation at some \(p < 1\) via the Ising model · 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

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.