===========
Lean proofs
===========


``lean/`` is a Lean 4 (Mathlib) model of
``ring::ringAdjacentCompletion``. The statements live in
``lean/DseamsProofs/Completion.lean``. ``lean/README.org`` lists every
theorem and the ``lake`` build.

The Lean file states that the all-but-one closure is the least fixed
point above the seed, that it is empty on an empty seed, and that
every added vertex sits on a ring whose other vertices are labelled.
It also shows that an edge-sharing rule is not sound on a five-vertex
instance. ``lake`` type-checks that closure on Lean 4.15.0 with Mathlib
v4.15.0 (pins in ``lean-toolchain`` and ``lakefile.toml``). Install
`elan <https://github.com/leanprover/elan>`_ for the toolchain. The
Coq/SymPy suite under ``proofs/`` is a different tree.

.. code:: bash

    cd lean
    lake exe cache get
    lake build

Catch2 (``tests/test_cage_affiliation.cpp``) covers the C++ identity,
vacancy refill, and structural zero of the same all-but-one closure.
The algorithm is
`Ring-adjacent completion <../explanation/ring-completion.rst>`_.