Independent researcher

John Fairfax-Ball

Independent mathematical research in discrete mathematics, computational mathematics and formal verification.

This site collects active projects, completed results, formal proofs and independently verified artefacts. Technical repositories remain the source of truth; this is the readable research index.

View research

Selected work

Research

All projects →

2026

Greedy Uniformity on Trees: Exact Obstruction and Near-Uniform Spiders

arXiv preprint

Random-order greedy maximal independent sets are exactly uniform on a finite tree only for K₁ and K₂, while explicit spiders approach uniformity.

For a uniformly random ordering of the vertices of a finite tree, this project compares the greedy maximal-independent-set law with the uniform law on maximal independent sets. It proves exact uniformity iff the tree is K₁ or K₂, and gives an explicit mixed-spider family $T_{k,2^k-k}$ with positive total-variation bias $O(\sqrt{k}/4^k)=O(\sqrt{\log n_k}/n_k^2)$ along $n_k=2^k+k+1$ . The frozen A+B package is formalised in Lean and registered with Palomar; the all- $n$ extremal minimisation problem and optimality of the construction remain open. The literature audit supports only “plausibly new with bounded uncertainty”, not an unconditional historical-priority claim.

Combinatorics
Graph theory
Probability
Greedy algorithms
Maximal independent sets
Trees
Lean 4
Mathlib

Date: 2026-10-05
Formalisation: Lean 4.35.0-rc3 / Mathlib v4.35.0-rc3
Verification: Lean 4.35.0-rc3 / Mathlib commit c55e6e786f49471c72fbddbec5415808896aec1e machine-checks the exact finite-law bridge, both final Theorem A declarations and all seven final Theorem B checkpoints; axiom checks report only propext, Classical.choice and Quot.sound, with no project-specific axioms or sorry/admit/native_decide in the project Lean sources. GitHub Actions passed the complete Lean build and 5 Python regression tests, while exact computation checks all 436 nonisomorphic unlabeled trees on 1–11 vertices and targeted local proof certificates. Palomar entry PALOMAR-2026-10-01-000003, version 1, is registered with high trust from immutable source commit 1733c29a5165148d71a2f0bd1ed2dcd7c35309ce. Lean and Palomar verify the formal statements and package integrity; they are not peer review or novelty certification.
Palomar: PALOMAR-2026-10-01-000003
arXiv: 2610.02276
DOI: 10.48550/arXiv.2610.02276

Attribution: John Fairfax-Ball is the author and repository maintainer. The random-order greedy maximal-independent-set / iid-priority / random-sequential-adsorption process is established prior art; Gadouleau–Kutner already exhibit the unequal P₃ permutation fibres, and Sagan–Vatter provide standard maximal-independent-set counting machinery used as background. This project’s audited contribution is the exact finite-tree obstruction and the explicit near-uniform mixed-spider family; Mathlib supplies foundational library results and Palomar supplies an external registry/verification record. The literature search supports only “plausibly new with bounded uncertainty”.

Prior / source research: John Fairfax-Ball, “Greedy Uniformity on Trees: Exact Obstruction and Near-Uniform Spiders”, arXiv:2610.02276 (2026). Relevant prior context includes Michael Krivelevich, Tamás Mészáros, Peleg Michaeli and Clara Shikhelman, “Greedy maximal independent sets via local limits”, arXiv:1907.07216 / Random Structures & Algorithms; Ivan Kryven, Rik Versendaal and Mike de Vries, “Unified framework for asymptotically uniform iterative construction of generalised random graphs with local constraints”, arXiv:2608.07239v1 (2026); and Maximilien Gadouleau and David C. Kutner, “Generalising the maximum independent set algorithm via Boolean networks”, Information and Computation 303 (2025), 105266.

GitHub Palomar Paper arXiv DOI Literature / novelty audit Lean formalisation Computational verification results

2026

Pascal Extremes

arXiv preprint

Sharp p-adic extrema and least extremal rows for restricted binomial GCDs are Lean-verified and public as arXiv:2610.01328.

This project studies sharp p-adic valuations of restricted binomial GCDs G(N;m), where lower indices are multiples of m. It proves that for every prime p with p∤m the maximum valuation over admissible rows is exactly r_p(m), constructs an attaining row, and for m=p^a+1 with a≥2 proves the exact least extremal row $T_p(p^a+1)=p^{3a}+1$ ; no general closed formula for T_p(m) is claimed. All stated target theorems are formally verified in Lean, with finite experiments retained only as independent checks. A documented literature audit located no equivalent theorem for the remaining general results beyond attributed prior subcases, but this is a negative-search finding and theorem-level non-overlap with Chung–Yang (2026) remains unresolved because its full text was not openly inspectable.

Number theory
Binomial coefficients
Greatest common divisors
p-adic valuations
Extremal problems
Lean 4
Mathlib

Date: 2026-10-01
Formalisation: Lean 4 / Mathlib
Verification: Lean 4 / Mathlib formalises Target A's universal upper bound, constructive attainment and exact maximum, establishes existence and minimality of the least extremal row T, and formalises Target B's target-row valuation plus strict lower-row non-attainment, yielding T p (p^a+1) = p^(3a)+1 for every prime p and a≥2. Repository CI builds the project from a fresh checkout and rejects sorry/admit in project Lean sources. Palomar entry PALOMAR-2026-09-30-000033, version 1, registered the advertised Target-A/Target-B theorem surface after successful Comparator and kernel verification. The Stage-2 seven-case pilot was independently checked by a Kummer carry/borrow DP against direct Legendre and integer binomial/GCD implementations; those computations are finite evidence only and remain outside the proof and formal trust boundary.
Palomar: PALOMAR-2026-09-30-000033
arXiv: 2610.01328

Attribution: John Fairfax-Ball is the author of the project, paper and Lean formalisation. Chai Wah Wu's 2026 work defines the exact selected-binomial-GCD family, while Carl McTague's work contains the p≡1 (mod m) Target-A subcase and the known (p,m,N)=(2,3,6) case; Kummer's theorem and Mathlib's p-adic/digit infrastructure are prior tools. Compatible low-level Lean infrastructure was adapted with attribution from the Apache-2.0 Pascal Minus-One predecessor. The documented September 2026 literature audit located no equivalent result for the remaining general Target-A theorem or Target B, subject to the unresolved Chung–Yang 2026 full-text caveat; this is not an unconditional historical-priority claim.

Prior / source research: Research continuation of John Fairfax-Ball's Pascal Minus-One GCD project (2026). Core prior mathematical context: Chai Wah Wu, “Computing the Greatest Common Divisor of Binomial Coefficients C(mn,mk)”, arXiv:2606.20940v2 (2026), defines exactly the selected-GCD family; Carl McTague, “On the Greatest Common Divisor of Binomial Coefficients C(n,q), C(n,2q), C(n,3q), ...”, American Mathematical Monthly 124(4) (2017), 353–356, corrected arXiv:1510.06696v5, contains the p≡1 (mod m) overlap and the (2,3,6) example.

GitHub Palomar Paper arXiv Literature / novelty audit Predecessor project: Pascal Minus-One GCD McTague prior work Wu prior work Chung–Yang 2026 adjacent work

2026

ProbStack — Random Stacking on Trees

arXiv preprint

A proved fixed-offset threshold theorem for random stackability on paths, with key finite deterministic interfaces formalised in Lean 4 and a public arXiv preprint.

ProbStack studies support-collapse stackability for uniformly random weak compositions of pebbles on paths and trees. For paths, the project proves a two-sided fixed-offset threshold centred at $\sqrt{\log_2 n}-\tfrac12\log_2\log_2 n+\log_2(3e)$ , with no claim at zero offset. The full asymptotic argument remains paper mathematics; Lean 4 formalises the exact finite TreeStack/path interfaces and the P6 deep-message necessity theorem, including the fixed-total $-(2\mu-1)$ corollary.

Probabilistic combinatorics
Graph pebbling
Random structures
Threshold phenomena
Trees and paths
Lean 4
Mathlib

Date: 2026-09-30
Formalisation: Lean 4 / Mathlib
Verification: The finite P6 necessity theorem and its exact fixed-total corollary are Lean-formalised without project sorry or axiom declarations in the ProbStack proof development and are publicly registered with Palomar as PALOMAR-2026-09-30-000023, version 1. Exhaustive and regression checks support the finite interfaces. The full random asymptotic threshold theorem is not part of the Palomar registration and is not fully Lean-formalised.
Palomar: PALOMAR-2026-09-30-000023
arXiv: 2609.39633
DOI: 10.48550/arXiv.2609.39633

Attribution: John Fairfax-Ball developed and maintains ProbStack and its Lean formalisation. The project uses TreeStack's deterministic structural stackability certificate as an input; Csernák and Soukup provide the support-collapse stacking context, and Bushaw and Kettle provide closely related random-pebbling path asymptotics for the different solvability event. A substantial 2026 public-record prior-art audit found no exact match in the searched sources for ProbStack's random fixed-total support-collapse stackability theorem on paths. Classical ingredients and the closest related results are explicitly attributed; this is a public-record originality finding rather than an unconditional historical-priority claim.

Prior / source research: TreeStack — Structural Certificates for Stacking on Trees (John Fairfax-Ball), together with the graph-pebbling background cited in formalization.yaml: Tamás Csernák and Lajos Soukup, “Stacking and clearing in graph pebbling” (arXiv:2604.22341), and Neal Bushaw and Nathan Kettle, “Thresholds for pebbling on grids” (arXiv:2309.01762).

GitHub Palomar Paper DOI

2026

Pascal Minus-One GCD

arXiv preprint

Lean/Mathlib formalisation complete, Palomar verified, and the research paper is public as arXiv:2609.37754 [math.NT].

This project studies $G(N;m)=\gcd\{\binom Nk:0<k<N,\ m\mid k\}$ . It formally proves the $p\equiv-1\pmod m$ valuation theorem, the complementary $p\equiv1\pmod m$ branch, a prime-power scaling theorem and complete prime-by-prime valuation corollaries for $m=3,4,6$ . A source-level audit through 25 September 2026 located no equivalent prior theorem for the full minus-one classification; this is a negative-search statement rather than an unconditional historical-priority claim. The research paper is public as arXiv:2609.37754 [math.NT], v1 submitted 29 September 2026.

Number theory
Binomial coefficients
Greatest common divisors
p-adic valuations
Lean 4
Mathlib

Date: 2026-09-29
Formalisation: Lean 4 / Mathlib
Verification: Lean-verified theorem layer: minus-one valuation, plus-one valuation, scaling, and complete modulus 3, 4 and 6 valuation corollaries. CI checks the build, regression tests, reference sweep and zero-sorry gate. Palomar registry entry: PALOMAR-2026-09-25-000017, version 1. Research paper: arXiv:2609.37754 [math.NT], v1 submitted 29 September 2026.
Palomar: PALOMAR-2026-09-25-000017
arXiv: 2609.37754

Attribution: John Fairfax-Ball maintains the repository and its Lean formalisation. Mathlib supplies Kummer's theorem and supporting digit machinery. McTague's work gives the plus-one theorem and strict subfamilies of the minus-one side; the September 2026 audit located no equivalent prior theorem for the full minus-one classification.

Prior / source research: Carl McTague, “On the Greatest Common Divisor of Binomial Coefficients C(n,q), C(n,2q), C(n,3q), ...”, American Mathematical Monthly 124(4) (2017), 353–356, corrected arXiv:1510.06696v5. Chai Wah Wu, “Computing the Greatest Common Divisor of Binomial Coefficients C(mn,mk)”, arXiv:2606.20940v2 (2026), is also directly relevant.

GitHub Palomar Paper arXiv McTague prior work Literature / novelty audit

2026

TreeStack — Structural Certificates for Stacking on Trees

arXiv preprint

A Lean 4 proof of the corrected nontrivial-tree form of the Csernák–Soukup tree-stacking estimator conjecture.

For every finite tree $T$ with at least two vertices, this project proves $\operatorname{stack}(T)=\operatorname{estim}(T)$ , the corrected nontrivial-tree form of the Csernák–Soukup estimator conjecture. The result is machine-checked end to end in Lean 4 and publicly registered after Palomar mechanical verification and automated review. The standalone research article is publicly available as arXiv:2609.31811 [math.CO].

Graph theory
Graph pebbling
Formal verification

Date: 2026-09-21
Formalisation: Lean 4
Verification: The Lean 4 formalisation machine-checks the main theorem end to end. Palomar mechanical verification and automated review passed for revision 4d4969703a9f0ca7a51cbe7edf0f0338cc95cafb; the result is publicly registered as PALOMAR-2026-09-25-000010, version 1.
Palomar: PALOMAR-2026-09-25-000010
arXiv: 2609.31811

Attribution: Original conjecture and estimator: Tamás Csernák and Lajos Soukup. Proof, Lean 4 formalisation, computational validation and research article: John Fairfax-Ball, with extensive AI assistance documented in the repository.

Prior / source research: Tamás Csernák and Lajos Soukup, “Stacking and clearing in graph pebbling”, arXiv:2604.22341v1, Conjecture 10.3.

GitHub Palomar Paper arXiv Original problem