# Mathematical specifications and implementation checks

This optional development project adds a method inventory and a real
finite-basis RHF pilot. It does not change the calculation engine or add
a runtime dependency. See `docs/formal_verification.md` and
`docs/formal_rhf.md` for scope, derivation and implementation correspondence.

## Inventory

```sh
python formal/check_inventory.py
```

Edit `formal/methods.json` when the method map, feature headings or covered
dispatch registries change. Regenerate the documentation with:

```sh
python formal/check_inventory.py --write
```

An inventory entry records a method and its next proof obligations. Only
the claims listed in the pinned Lean project have Lean proofs.

## Lean environment and proof audit

Install [elan](https://github.com/leanprover/elan), Lean's toolchain manager,
and make its `lake` executable available on PATH. The project pins Lean
4.35.0, mathlib v4.35.0 and all resolved dependencies in `lake-manifest.json`.

```sh
cd formal/rhf
lake exe cache get
python ../check_proofs.py
```

The first cache download needs disk space and network access. Subsequent
checks reuse it. Do not run `lake update` during ordinary reproduction;
that command is for deliberate dependency changes. The `.lake` directory
is a local ignored dependency/build cache.

`check_proofs.py` builds the library and audits every exported theorem's
transitive axioms. Proofs with `sorryAx`, extra axioms or compiler-trust
axioms are rejected. The allowed base is `propext`, `Classical.choice` and
`Quot.sound`. Check both the theorem statements and their physical
interpretation; a kernel-accepted proof does not establish that a model
describes the intended chemistry or that C++ refines it.

## Native implementation checks

Use Python from an existing qualified vibe-qc installation. The script
requires NumPy and the actual `vibeqc._vibeqc_core` module, not a mock.
From the repository root:

```sh
python formal/check_rhf.py --output rhf-synthetic.json
```

For a complete H2O/STO-3G calculation, submit the following command through
the calculation scheduler with that installation's Python:

```sh
python check_rhf.py --molecule --output rhf-checks.json
```

Supply `formal/check_rhf.py` as the job input. Run the matching
`formal/rhf/reference_h2o.inp` with ORCA as an independent calculation.
The returned JSON records the Python/native locations, native SHA-256,
numerical residuals and negative controls. Preserve the scheduler/runtime
identity and reference output alongside it. Keep site-specific paths and
operational records outside the public source tree.

All comparisons use explicit finite tolerances. They do not prove the
compiled program or replace method-level scientific validation. The present
pilot does not establish global SCF convergence, minimum selection,
continuum integral correctness or a floating-point error bound.

## Licenses

The original files here follow vibe-qc's MPL-2.0 license. Lean and mathlib
are separate development dependencies under their upstream licenses. They
are fetched into an ignored cache and are not bundled into vibe-qc's runtime.

## UHF, density-fitting and MP2 extensions

The same pinned project and axiom audit now include `Extensions.lean`.
See `docs/formal_uhf.md`, `docs/formal_density_fitting.md` and
`docs/formal_mp2.md` for the checked claims and remaining obligations.
For numerical reproduction, provide both `check_extensions.py` and
`check_rhf.py` to a scheduler job and run:

```sh
python check_extensions.py
```

The harness exercises native UHF and canonical MP2, native integral generation,
the public Python fitting contractions. Add `--cpp` to require the separate
resident C++ fitting storage bindings (available in the tested 0.18.6 runtime).
It writes `extensions-checks.json`. Reference inputs are
`rhf/reference_oh_uhf.inp` and `rhf/reference_water_mp2.inp`.
This bounded coverage does not establish every variant in a family row.