A finite formalization of the finite part of the hard-sphere NBC proof. points is a finite configuration ledger, trees is a finite list of candidate spanning trees, and region t x is the NBC ownership test.

The central theorem is a literal finite Tonelli/double-counting proof:

  sum_x weight(x) * NBCMultiplicity(x)
    = sum_t NBCRegionWeight(t).

No measure theorem, graph theorem, or opaque assumption is imported here. The continuous hard-sphere interpretation is obtained by replacing the finite weight sum with Lebesgue integration after this algebraic identity.

def HsVirial.sumNat (xs : List ℕ) : ℕ

Compatibility name for the standard sum of a list of natural numbers.

Equations

• HsVirial.sumNat xs = xs.sum

theorem HsVirial.sumNat_map_congr {X : Type} {xs : List X} {f g : X → ℕ} (h : ∀ (x : X), f x = g x) : sumNat (List.map f xs) = sumNat (List.map g xs)

theorem HsVirial.list_map_map {X Y Z : Type} (xs : List X) (f : X → Y) (g : Y → Z) : List.map g (List.map f xs) = List.map (fun (x : X) => g (f x)) xs

theorem HsVirial.mul_sumNat {xs : List ℕ} (a : ℕ) : a * sumNat xs = sumNat (List.map (fun (b : ℕ) => a * b) xs)

theorem HsVirial.sumNat_swap {X Y : Type} (xs : List X) (ys : List Y) (f : X → Y → ℕ) : sumNat (List.map (fun (x : X) => sumNat (List.map (f x) ys)) xs) = sumNat (List.map (fun (y : Y) => sumNat (List.map (fun (x : X) => f x y) xs)) ys)

def HsVirial.indicator (p : Bool) (a : ℕ) : ℕ

Keep a natural-number weight exactly when the Boolean predicate holds.

Equations

• HsVirial.indicator p a = if p = true then a else 0

def HsVirial.nbcMultiplicity {X T : Type} (trees : List T) (region : T → X → Bool) (x : X) : ℕ

Count the listed tree regions containing the point, including repeated tree entries.

Equations

• HsVirial.nbcMultiplicity trees region x = HsVirial.sumNat (List.map (fun (t : T) => HsVirial.indicator (region t x) 1) trees)

def HsVirial.nbcRegionWeight {X T : Type} (points : List X) (weight : X → ℕ) (region : T → X → Bool) (t : T) : ℕ

Sum point weights over one tree region.

Equations

• HsVirial.nbcRegionWeight points weight region t = HsVirial.sumNat (List.map (fun (x : X) => HsVirial.indicator (region t x) (weight x)) points)

def HsVirial.pointwiseNbcWeight {X T : Type} (points : List X) (trees : List T) (weight : X → ℕ) (region : T → X → Bool) : ℕ

Sum point weights multiplied by the number of tree regions containing the point.

Equations

• HsVirial.pointwiseNbcWeight points trees weight region = HsVirial.sumNat (List.map (fun (x : X) => weight x * HsVirial.nbcMultiplicity trees region x) points)

def HsVirial.nbcVolumeSum {X T : Type} (points : List X) (trees : List T) (weight : X → ℕ) (region : T → X → Bool) : ℕ

Sum the weighted sizes of all listed tree regions.

Equations

• HsVirial.nbcVolumeSum points trees weight region = HsVirial.sumNat (List.map (HsVirial.nbcRegionWeight points weight region) trees)

theorem HsVirial.indicator_mul_one (p : Bool) (a : ℕ) : a * indicator p 1 = indicator p a

theorem HsVirial.nbc_volume_identity {X T : Type} (points : List X) (trees : List T) (weight : X → ℕ) (region : T → X → Bool) : pointwiseNbcWeight points trees weight region = nbcVolumeSum points trees weight region

def HsVirial.sumInt (xs : List ℤ) : ℤ

Compatibility name for the standard sum of a list of integers.

Equations

• HsVirial.sumInt xs = xs.sum

def HsVirial.paritySign : ℕ → ℤ

The alternating integer sign associated with a natural-number size.

Equations

• HsVirial.paritySign = HsVirial.matroidParitySign

This is the finite active-graph restriction used before the NBC step. The list graphs represents the complete finite list of edge subsets. A Mayer term is zero unless every edge is active; otherwise its product is the parity sign of the number of edges.

def HsVirial.allActive {E : Type} (active : E → Bool) : List E → Bool

Check that every edge in a list is active.

Equations

• HsVirial.allActive active [] = true
• HsVirial.allActive active (e :: es) = if active e = true then HsVirial.allActive active es else false

def HsVirial.signedMayerTerm {E : Type} (connected : List E → Bool) (active : E → Bool) (edges : List E) : ℤ

The parity contribution of a connected edge list with every edge active.

Equations

• HsVirial.signedMayerTerm connected active edges = if connected edges = true then if HsVirial.allActive active edges = true then HsVirial.paritySign edges.length else 0 else 0

def HsVirial.signedMayerSum {E : Type} (graphs : List (List E)) (connected : List E → Bool) (active : E → Bool) : ℤ

Sum signed Mayer terms over a list of candidate edge sets.

Equations

• HsVirial.signedMayerSum graphs connected active = HsVirial.sumInt (List.map (HsVirial.signedMayerTerm connected active) graphs)

def HsVirial.activeGraphSum {E : Type} (graphs : List (List E)) (connected : List E → Bool) (active : E → Bool) : ℤ

Restrict the graph list to active edge sets before summing connected contributions.

Equations

• One or more equations did not get rendered due to their size.

theorem HsVirial.signed_mayer_restriction {E : Type} (graphs : List (List E)) (connected : List E → Bool) (active : E → Bool) : signedMayerSum graphs connected active = activeGraphSum graphs connected active

The next block formalizes the sign-reversing part independently of graph representation. For a fixed ordered graph, all is the finite list of connected edge sets, good is the finite list of NBC trees, and badPairs is produced by the least broken-circuit toggle described in the TeX proof. The theorem checks, in the kernel, that every paired bad contribution disappears.

def HsVirial.signedList {A : Type} (xs : List A) (size : A → ℕ) : ℤ

The sum of parity signs for the sizes of a list of objects.

Equations

• HsVirial.signedList xs size = HsVirial.sumInt (List.map (fun (a : A) => HsVirial.paritySign (size a)) xs)

theorem HsVirial.sumInt_append {as bs : List ℤ} : sumInt (as ++ bs) = sumInt as + sumInt bs

theorem HsVirial.signedList_eq_constant {A : Type} (xs : List A) (size : A → ℕ) (rank : ℕ) (same_sign : ∀ a ∈ xs, paritySign (size a) = paritySign rank) : signedList xs size = sumInt (List.map (fun (x : A) => paritySign rank) xs)

theorem HsVirial.sumInt_pair_zero {A : Type} (pairs : List (A × A)) (size : A → ℕ) (opposite : ∀ p ∈ pairs, paritySign (size p.1) + paritySign (size p.2) = 0) : sumInt (List.flatMap (fun (p : A × A) => [paritySign (size p.1), paritySign (size p.2)]) pairs) = 0

structure HsVirial.NBCPairing (A : Type) : Type

A decomposition into surviving objects and pairs with opposite parity contributions.

• all : List A

  The full list before cancellation.

• good : List A

  The surviving list of no-broken-circuit objects.

• badPairs : List (A × A)

  Pairs whose signed contributions cancel.

• size : A → ℕ

  The size determining the parity sign of each object.

• rank : ℕ

  The common size of the surviving objects.

• decomposition : self.all = self.good ++ List.flatMap (fun (p : A × A) => [p.1, p.2]) self.badPairs
• opposite (p : A × A) : p ∈ self.badPairs → paritySign (self.size p.1) + paritySign (self.size p.2) = 0
• goodParity (a : A) : a ∈ self.good → paritySign (self.size a) = paritySign self.rank

theorem HsVirial.signed_sum_of_nbc_pairing {A : Type} (P : NBCPairing A) : signedList P.all P.size = signedList P.good P.size