BufferedIsing
DefinitionA finite graph has n vertices and m separately indexed, loop-free edges with nonnegative real couplings Kₑ; parallel edges are allowed and zero couplings may represent absent edges. A spin configuration assigns each vertex a Boolean, interpreted as a spin sᵥ∈{−1,+1}. For arbitrary real fields hᵥ, its energy is E(σ)=∑ₑ Kₑsₗ₍ₑ₎sᵣ₍ₑ₎+∑ᵥ hᵥsᵥ and its weight is exp(E(σ)). Agreement on a vertex set means matching every prescribed spin there, and a constrained sum adds the weights of configurations satisfying a given predicate. For vertex sets I, J, F and prescriptions a, b, τ, conditionalProb is the constrained sum imposing σ_I=a_I, σ_J=b_J, σ_F=τ_F divided by the sum imposing only the latter two conditions. The comparison model deletes F and every incident edge, then identifies all remaining vertices of I together and, separately, all remaining vertices of J together. For an open edge set ω, the equivalence relation generated by these identifications and undirected open-edge adjacency determines its components, whose number is k(ω). With pₑ=1−exp(−2Kₑ), its zero-field random-cluster weight is 2^{k(ω)}∏ₑ pₑ^{1[e∈ω]}(1−pₑ)^{1[e∉ω]}, over retained edges, interpreted by selecting the appropriate factor. For any two retained vertices i,j, qZero is the total weight of open edge subsets connecting i to j divided by the total weight of all open edge subsets. Finally, mixtureProb sums conditionalProb over source prescriptions b with real coefficients mix(b); only their restrictions to J affect the conditional probabilities. These definitions impose no disjointness on I,J,F or probability normalization or nonnegativity on mix; inconsistent conditioning gives a zero denominator, with division interpreted as zero.
-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a
-- Source: lean/ComparatorChallenges/BufferedIsing.lean; bytes 16..4276
-- Kind: block; original declaration names and bodies preserved.
-- Source groups are independent. Target: Lean 4.33.1; see compilation.json.
import Mathlib
namespace OAI
open scoped BigOperators Classical
namespace BufferedIsing
/-- A finite graph given by its edge list. Zero couplings can encode missing edges.
Edges are indexed separately so parallel edges are counted separately. -/
structure FiniteGraph (n m : ℕ) where
left : Fin m → Fin n
right : Fin m → Fin n
coupling : Fin m → ℝ
coupling_nonneg : ∀ e, 0 ≤ coupling e
no_loops : ∀ e, left e ≠ right e
abbrev Spins (n : ℕ) := Fin n → Bool
def spin (b : Bool) : ℝ := if b then 1 else -1
noncomputable def energy {n m : ℕ} (G : FiniteGraph n m)
(h : Fin n → ℝ) (σ : Spins n) : ℝ :=
(∑ e, G.coupling e * spin (σ (G.left e)) * spin (σ (G.right e))) +
∑ v, h v * spin (σ v)
noncomputable def weight {n m : ℕ} (G : FiniteGraph n m)
(h : Fin n → ℝ) (σ : Spins n) : ℝ := Real.exp (energy G h σ)
def AgreesOn {n : ℕ} (S : Finset (Fin n)) (σ τ : Spins n) : Prop :=
∀ v ∈ S, σ v = τ v
noncomputable def constrainedSum {n m : ℕ} (G : FiniteGraph n m)
(h : Fin n → ℝ) (P : Spins n → Prop) : ℝ := by
classical
exact ∑ σ, if P σ then weight G h σ else 0
/-- Conditional probability of σ_I=a, with σ_J=b and σ_F=τ prescribed.
All sums are finite and all fields are finite real numbers. -/
noncomputable def conditionalProb {n m : ℕ} (G : FiniteGraph n m)
(h : Fin n → ℝ) (I J F : Finset (Fin n)) (a b τ : Spins n) : ℝ :=
constrainedSum G h (fun σ => AgreesOn I σ a ∧ AgreesOn J σ b ∧ AgreesOn F σ τ) /
constrainedSum G h (fun σ => AgreesOn J σ b ∧ AgreesOn F σ τ)
/-- Edges remaining after DELETION, not pinning, of F. -/
def keptEdges {n m : ℕ} (G : FiniteGraph n m) (F : Finset (Fin n)) : Finset (Fin m) :=
Finset.univ.filter (fun e => G.left e ∉ F ∧ G.right e ∉ F)
abbrev KeptVertex {n : ℕ} (F : Finset (Fin n)) := {v : Fin n // v ∉ F}
/-- Open-edge adjacency together with the two separate terminal identifications.
No virtual identification of common pins is present: those vertices are absent. -/
def comparisonRel {n m : ℕ} (G : FiniteGraph n m)
(I J F : Finset (Fin n)) (ω : Finset (Fin m)) (u v : KeptVertex F) : Prop :=
(u.val ∈ I ∧ v.val ∈ I) ∨ (u.val ∈ J ∧ v.val ∈ J) ∨
∃ e ∈ ω, (G.left e = u.val ∧ G.right e = v.val) ∨
(G.left e = v.val ∧ G.right e = u.val)
/-- The equivalence closure implements components of the contracted open graph. -/
def comparisonSetoid {n m : ℕ} (G : FiniteGraph n m)
(I J F : Finset (Fin n)) (ω : Finset (Fin m)) : Setoid (KeptVertex F) :=
Relation.EqvGen.setoid (comparisonRel G I J F ω)
noncomputable def clusterCount {n m : ℕ} (G : FiniteGraph n m)
(I J F : Finset (Fin n)) (ω : Finset (Fin m)) : ℕ :=
Nat.card (Quotient (comparisonSetoid G I J F ω))
/-- Zero-field FK weight with q=2 and p_e=1-exp(-2 K_e).
Parallel edges may be retained: the measure after summing them is the measure
for the summed parallel coupling. Loops created by contraction do not change
components and cancel from connection probabilities. -/
noncomputable def fkWeight {n m : ℕ} (G : FiniteGraph n m)
(I J F : Finset (Fin n)) (ω : Finset (Fin m)) : ℝ := by
classical
exact (2 : ℝ) ^ clusterCount G I J F ω *
∏ e ∈ keptEdges G F,
if e ∈ ω then 1 - Real.exp (-2 * G.coupling e) else Real.exp (-2 * G.coupling e)
/-- Choose any i in I and j in J. The terminal connection is independent of
these choices because I and J are each identified. -/
noncomputable def qZero {n m : ℕ} (G : FiniteGraph n m)
(I J F : Finset (Fin n)) (i j : KeptVertex F) : ℝ := by
classical
exact (∑ ω ∈ (keptEdges G F).powerset,
if (comparisonSetoid G I J F ω).r i j then fkWeight G I J F ω else 0) /
∑ ω ∈ (keptEdges G F).powerset, fkWeight G I J F ω
/-- Any probability mixture of source prescriptions. Full configurations
index the mixture, but only their restrictions to J are used. Thus this is
exactly the class of all mixtures on {-1,+1}^J. -/
noncomputable def mixtureProb {n m : ℕ} (G : FiniteGraph n m)
(h : Fin n → ℝ) (I J F : Finset (Fin n)) (a τ : Spins n)
(mix : Spins n → ℝ) : ℝ :=
∑ b, mix b * conditionalProb G h I J F a b τ
end BufferedIsing
end OAI
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.