# Continuum phase transitions for radial pair potentials

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [A continuum temperature singularity for a radial pair potential](../../preprints/A-continuum-temperature-singularity-for-a-radial-pair-potential-September-24-2026/paper.pdf)
- [A radial continuum phase transition with algebraic decay](../../preprints/A-radial-continuum-phase-transition-with-algebraic-decay-September-24-2026/paper.pdf)

## Scope

The formalization constructs one stable radial pair potential in three-dimensional continuum space with a divergent repulsive core and an integrable tail that is $o(r^{-3})$. Its canonical free energy exists for every positive inverse temperature and density. At one inverse temperature $\beta_c\in(1/2,3/2)$, the free energy has a strict finite jump between its one-sided derivatives with respect to inverse temperature, for every density in one nonempty open interval.

The formalization constructs a bounded continuous stable radial pair potential in $\mathbb R^3$ satisfying $|\phi(r)|\le Cr^{-3-1/32}$ for $r\ge1$. There is a nonempty open interval of positive densities around $5p/3$, where $p$ is the unit-separated packing-density limit, on which the canonical free energy exists at every positive inverse temperature and has a strict downward derivative jump at one common $\beta_c\in[7/8,9/8]$.

The earlier fixed-density statement at $5p/3$ is also retained. Both statements concern the derivative with respect to inverse temperature.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Temperature singularity over a density interval | [ContinuumTransition.lean](../ComparatorChallenges/ContinuumTransition.lean) |
| Fixed-density radial continuum phase transition | [RadialTransition.lean](../ComparatorChallenges/RadialTransition.lean) |
| A common radial phase transition over a density interval | [RadialDensityInterval.lean](../ComparatorChallenges/RadialDensityInterval.lean) |