# Perceptron free energies and microscopic jamming exponents

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

- [The free energy of the Ising random perceptron](../../preprints/The-free-energy-of-the-Ising-random-perceptron-September-24-2026/The-free-energy-of-the-Ising-random-perceptron-September-24-2026.pdf)
- [The free energy of the spherical random perceptron](../../preprints/The-free-energy-of-the-spherical-random-perceptron-September-24-2026/The-free-energy-of-the-spherical-random-perceptron-September-24-2026.pdf)

## Scope

The linked formalization proves finiteness of the variational value used for the Ising random perceptron. For every nonnegative pattern density and every bounded continuous log-potential, the infimum over admissible overlap paths is a finite real number.

This is a supporting well-definedness result. It does not assert convergence of the finite-system pressure or the paper's extension to all bounded Borel log-potentials.

The formalization proves the variational formula for the spherical random perceptron's limiting pressure for every positive pattern density and inverse temperature and every bounded continuous single-pattern potential. It shows that the variational value is finite and that the pressure converges to it both in expectation and in probability.

The linked spherical-field result supplies a supporting dual formula: finite hierarchy field values converge uniformly on compact parameter sets to an attained dual minimum, and the corresponding bounded stationary-field approximation holds for monotone overlap quantiles bounded away from one.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Finiteness of the Ising-perceptron variational value | [IsingFiniteness.lean](../ComparatorChallenges/IsingFiniteness.lean) |
| Variational formula for spherical-perceptron pressure | [PerceptronFreeEnergy.lean](../ComparatorChallenges/PerceptronFreeEnergy.lean) |
| Spherical linear-field dual formula and approximation | [SphericalField.lean](../ComparatorChallenges/SphericalField.lean) |