# AI provenance: Ghosts in Poisson Brane Gases

Authors: Deep Bhattacharjee (corresponding author, ORCID 0000-0003-0466-750X)
and Ushashi Bhattacharya (ORCID 0009-0002-2254-3914).

- Paper: https://github.com/creelie/brane-cluster-gases/blob/main/preprintGhostsBraneGases/GhostsBraneGases.pdf
- Lean formalisation and code: Zenodo, release 3.0.0, https://doi.org/10.5281/zenodo.23449534 (all versions: https://doi.org/10.5281/zenodo.22866290)
- Repository: https://github.com/creelie/brane-cluster-gases (folder `ghosts/`)

## Result

A Poisson gas of branes with intensity ν dresses the graviton propagator by
the random entire function F(z) = ∏(1 + z/t_k). The paper proves that the gas
average of the propagator is E[1/(zF(z))] = e^{−φ(z)}/z, where
φ(z) = ∫ z ν(dt)/(z + t) is a complete Bernstein function, and not
1/(z E F(z)) as the two earlier manuscripts of the repository assumed. The
massive states then carry total weight e^{−ν(0,∞)} − 1 < 0, so the average
has no positive Källén–Lehmann representation. For ν = λ(t) dt/t the averaged
massive spectrum consists of ghosts alone exactly when λ ≤ 1, and every
average with a finite four-dimensional tadpole has states of both signs. A
frozen gas has residues of alternating sign.

## Who did what

Deep Bhattacharjee chose the problem, directed the work, set the format and
the target, and ran the computations. Claude (Anthropic), used through Claude
Code under his direction, produced the following:

- the proofs of the theorems, in particular the exact averaging formula, the
  ghost threshold λ ≤ 1 through Plemelj–Privalov boundary values, and the
  trade-off between a finite tadpole and positivity;
- the Lean 4 formalisation;
- the checking programs in Python, C and Julia;
- the figures;
- the LaTeX text of the paper.

No other AI system took part.

## How the result is checked

- **Lean 4.33.0 with Mathlib.** Thirteen theorems in `ghosts/lean/BraneGhosts.lean`
  prove the sign of the residues, the sum rule, the elementary inequalities of
  Appendix A, the bound Im φ ≤ π, the sign of the spectral density in the two
  windows and a partial fraction. Each one depends only on propext,
  Classical.choice and Quot.sound. There is no `sorry`, `admit`,
  `native_decide` or added axiom. The analytic steps are proved in the paper
  and are not formalised.
- **Independent programs.** Python (19 checks), C (5) and Julia (9) programs
  recheck the averaging formula by simulation and the other formulas
  numerically. No statement rests on a floating-point computation.

## What is not claimed

The paper does not prove ultraviolet finiteness or completeness of
perturbative quantum gravity. Its Theorem D shows that for this averaged
model a finite four-dimensional tadpole and a positive spectrum cannot both
hold.

## Text and references

The paper is written in one analytical flow. Its bibliography contains,
besides the works it builds on, five self-citations of the authors placed
where they bear on the text. Every entry was checked against its Crossref
record or the arXiv listing, and none comes from TechRxiv, Qeios, Authorea or
EasyChair.