Papers With

← All papers
First page of Iterated Graph Systems (II): Bernoulli percolation and critical-exponent universality classes on hierarchical lattices

Iterated Graph Systems (II): Bernoulli percolation and critical-exponent universality classes on hierarchical lattices

Ziyu Neroli

math-ph Oct 7, 2026 · v1 cond-mat.stat-mech math.PR
formalization mathlib probability
Read PDF arXiv abstract Code
TL;DR
Results of Sections 2–5 are formalized in Lean 4 with Mathlib, including kernel-checked certificate identities, assuming only Gelfond–Schneider and the six exponentials theorem.
Abstract
We study Bernoulli percolation and its universality classes on hierarchical lattices generated by edge iterated graph systems (EIGS). By examining eight critical exponents, we prove that no finite family of substitution-multiplicative dimensions completely determines universality, providing a rigorous proof of the failure of dimension-based universality discussed by Hauser and Saxena [Phys. Rev. B 34 (1986), 8193-8195]. Although the six exponentials theorem provides number-theoretic criteria for scale commensurability, we further disprove the conjecture that critical-exponent universality requires commensurate discrete renormalisation scales.
Problem

Hauser and Saxena (1986) questioned whether dimension-based universality holds for percolation on hierarchical lattices. A related conjecture holds that lattices in the same critical-exponent universality class must have commensurate discrete renormalisation scales.

Approach

Bernoulli percolation is studied on hierarchical lattices generated by edge iterated graph systems. Critical clusters are represented as random EIGS, and eight critical exponents are analysed. Four of them define a universality class, and that class is characterised by three critical dimensions. The six exponentials theorem gives number-theoretic commensurability criteria, and explicit Wheatstone-based rule graphs are built with integer certificates. The results are formalized in Lean 4 on Mathlib.

Results

No finite family of substitution-multiplicative dimensions determines the universality class, which settles the Hauser–Saxena question rigorously. The commensurability conjecture is disproved: one universality class is shown to contain infinitely many pairwise incommensurate scales. The proofs are checked by Lean's kernel with no proof placeholders.