# Lean companion to *Beyond the Bethe Approximation of the Permanent*

[![CI](https://github.com/nimaanari/formalization-beyond-bethe/actions/workflows/ci.yml/badge.svg)](https://github.com/nimaanari/formalization-beyond-bethe/actions/workflows/ci.yml)

This repository contains the Lean 4 formalization accompanying the paper. It
uses Lean `v4.30.0`, Mathlib `v4.30.0`, and a pinned revision of
Complexitylib.

The associated manuscript, *Beyond the Bethe Approximation of the Permanent*,
is being prepared for arXiv. Its permanent identifier will be added here after
posting.

The development has three layers.

1. The mathematical modules define the permanent, the Bethe objective, and
   the stable-polynomial and entropy inequalities used in the proof.
2. The numerical modules prove the bounded epigraph geometry, directed
   rational logarithm and exponential estimates, rounded rational ellipsoid
   method, threshold bisection, and approximate KKT reconstruction.
3. The machine modules implement the complete rational algorithm over a
   canonical ordinary binary encoding and prove that it belongs to
   Complexitylib's class `FP`.

The development reconstructs all four external results used by Theorem 1:
Vontobel's concavity theorem, the sharp Anari--Rezaei one-row inequality, the
upper Bethe bound, and the Anari--Oveis Gharan stable-coefficient inequality.
For the last result, it includes the analytic closure lemmas, the direct
Lieb--Sokal contraction, the bivariate Rayleigh inequality, the multilinear
coefficient-table induction, the passage from approximate witnesses to
capacity, and transport across arbitrary finite coordinate types. The
Gurvits lower Bethe bound is recovered internally as the singleton-cluster
case.

The public theorem is `BeyondBethe.theoremOne` in the module
`BeyondBethe.Main`. It has no hypotheses. It
constructs a fixed rational algorithm, proves the approximation factor with
base strictly below `sqrt 2`, and supplies a deterministic polynomial-time
Turing-machine implementation.

The executable path includes:

- rational normalization, smoothing, support matching, scale restoration,
  and the exact dimensions zero and one;
- structural binary arithmetic, long division, bounded Euclid, signed and
  unreduced rational arithmetic, normalization, comparison, dyadic flooring,
  rational powers, and list/matrix access and mutation;
- directed logarithm and exponential routines with explicit unary work and
  output guards whose polynomial bounds are proved from the source word;
- the bounded regularized-Bethe epigraph oracle, a fixed-precision rounded
  rational ellipsoid loop, threshold bisection, recovery of the Birkhoff
  matrix, and anchored row and column KKT potentials;
- greedy certificate matching, the nearby-Bethe sum, the directed
  exponential certificate, and the complete outer algorithm.

All loops are total on arbitrary bitstrings. Width clamps are part of the
programs, and their correctness theorems prove that the clamps are inactive on
the canonical inputs occurring in the algorithm. In particular, the final
exponential guard is derived from the original normalized-matrix word and a
proved certificate-log magnitude bound; it is not inferred from the possibly
shorter optimizer-output word.

The substantive development and `Solution.lean` contain no `sorry`, `admit`,
project-specific `axiom`, or project-specific optimization interface.
`Challenge.lean` contains the one deliberate theorem hole required by
Palomar. `AxiomAudit.lean` reports only Lean/Mathlib's standard logical axioms
`propext`, `Classical.choice`, and `Quot.sound` for `theoremOne`, the Palomar
solution, and their proof-critical dependencies.

## Project Palomar surface

`Challenge.lean` is a Mathlib-only statement file and `Solution.lean` proves
the same theorem from the full development. The compared declaration is
`Palomar.beyond_bethe_permanent`; `comparator.json` enables NanoDa and permits
only the three standard axioms listed above.

The theorem states polynomial time using a source-stable presentation of
Cobham's bitstring algebra. The formal equivalence
`BeyondBethe.PalomarComplexity.cobhamFP_iff_complexity` identifies it with
Complexitylib's ordinary Cobham class, which Complexitylib in turn proves equal
to its deterministic Turing-machine class `FP`.

On Linux, run the complete pinned Palomar check with:

```sh
./scripts/verify-comparator.sh
```

After the paper and repository metadata are finalized, the reviewed commit can
be submitted through the [Palomar submission form](https://submit.palomar-registry.org/).

## Building

From this directory:

```sh
lake exe cache get
lake build
```

For the final dependency audit:

```sh
lake env lean BeyondBethe/AxiomAudit.lean
```

The command `./scripts/build.sh` performs the build and axiom audit and also
compiles every file in `tests/`; these include small permanent and smoothing
checks and an exhaustive executable comparison of the two matching decisions
on all three-by-three support patterns.

The manuscript correspondence is recorded in
[`notes/paper-map.md`](notes/paper-map.md), and the numerical and finite-word
audit is summarized in
[`notes/numerical-audit.md`](notes/numerical-audit.md).