vibe-qcDocumentation

Exact nearest images in production CCM geometry

The stage-2 certificate checks found a real boundary defect: zero-tolerance CCM geometry could return a globally nearest image while omitting another exactly tied image. This follow-up connects the complete rational search to minimum_image(..., tol_bohr=0) and adds proofs of nonempty tie sets and normalized uniform real weights. CCM and AICCM remain experimental.

Contract and corrected example

The public geometry interface accepts Cartesian displacements and a 3 by 3 lattice whose vectors are rows, in the same length unit. It converts inputs to binary64, then treats those finite represented numbers as exact rationals. The internal certificate uses lattice columns, so the wrapper transposes explicitly. This contract concerns the represented inputs after conversion; it does not recover an intended decimal value or physical uncertainty.

For the column-basis matrix and displacement

\[\begin{split} A=\begin{pmatrix}2&-1/2&0\\0&3/2&-1\\0&0&1\end{pmatrix}, \qquad x=(9/8,-5/8,1/4)^T, \end{split}\]

both (0,-1,0) and (1,0,0) minimize the squared distance at 39/32. The old floating-point reconstruction returned only the first image at zero tolerance. The exact path returns both, each with weight 1/2. At one floating-point step away from an orthogonal half-cell boundary, only the genuinely nearest image is returned; the correction does not introduce an epsilon tie rule.

from vibeqc.periodic.ccm.wigner_seitz import minimum_image

rows = [[2., 0., 0.], [-.5, 1.5, 0.], [0., -1., 1.]]
cells, weights = minimum_image(
    [1.125, -.625, .25], rows, tol_bohr=0., max_exact_candidates=100000,
)

Zero tolerance bypasses the reduced basis and fixed shell entirely. Singular cells, nonfinite inputs, invalid budgets and image labels outside the public int64 output range fail explicitly. max_exact_candidates bounds the complete box size per displacement. Exceeding it raises SearchBudgetExceeded, a ValueError subclass, before enumeration; no partial tie set is returned. min_image_multiplicity and CCMSystem(weight_tol_bohr=0) consume the corrected path. The latter currently uses the default work budget. An exceptional cell requiring a larger budget can be queried directly through minimum_image; configurable propagation through the full CCM driver is future work. The full CCM driver still constructs a floating-point reduced basis and selects finite integral images separately. Exact nearest labels do not establish completeness or successful execution of those other steps for every triclinic cell.

Positive finite tol_bohr retains the existing floating-point near-tie policy. It is neither an exact equality predicate nor covered by the completeness proof. Negative and nonfinite tolerances are rejected. The NEB path is unchanged.

Derivation and proofs

Write q(n)=||x-An||^2, with integer image n. The certificate contains an exact left inverse H, an incumbent b, a rational radius R, and integer box endpoints. For HA=I, R>=0 and q(b)<=R^2, any image with q(n)<=R^2 satisfies

\[ | (Hx)_i-n_i | = |\sum_a H_{ia}(x-An)_a| \leq R\sum_a|H_{ia}|. \]

Floor/ceiling of the corresponding endpoints encloses every possible minimizer. Exact enumeration minimizes q over that box. Images outside its sublevel set are worse than the incumbent. Filtering the box by equality to the best cost therefore gives exactly all global minimizers. This argument requires no Minkowski-reduction or neighbor-shell theorem. Component-wise rounding supplies only an incumbent; it is not treated as a nearest-image solution.

image_certificate_sound and image_certificate_all_ties establish these claims in Lean over rational inputs. Two additional theorems close the weight premise:

  • certified_ties_nonempty: a valid certificate’s optimal representative belongs to the complete tie set T, so T is nonempty.

  • certified_weights_sum_one: with m=|T|>0, the uniform real weights satisfy sum(n in T, 1/m)=m/m=1.

The second theorem reuses stage 1’s uniform_boundary_weights. It proves the normalization implied by the two-center prescription in Peintinger and Bredow (2014), equations 4-7. It does not prove the physical adequacy of CCM, the full multi-center weighting scheme, forces across topology changes or floating-point summation of weights. For example, an arbitrary reciprocal multiplicity need not be exactly representable in binary64. The regression’s 1/2 weights are exactly representable.

Mathematical specification and implementation connection

The production module _exact_images.py uses only Python’s standard library. It computes an exact inverse with Fraction, an integer ceiling of the square root, the conservative box, all minimizing labels, and a certificate. Its verifier rechecks the inverse, radius, box inequalities, minimum and complete ordered tie list. The constructor and checker share helpers; they are not independent implementations of every arithmetic operation.

The optional Lean specification is VibeQCStage2.lean. The acceptance script check_exact_images.py exports certificates from the production producer, compares the public wrapper’s image labels and weights, and generates Lean statements for validity, global optimality, complete ties, nonemptiness and normalization. The Lean kernel checks their premises using decide +kernel. The audit rejects admitted proofs and checks transitive axioms against the established standard base.

This gives independent kernel checking of the exported finite certificates. It is not a universal refinement proof of the Python program, NumPy input conversion, integer-output conversion, interpreter, native integrals or SCF. The private evidence records input/output hashes and source/native identities. An explicit Python-only overlay can test these two geometry modules against an existing native installation; that is source-under-test evidence, not evidence that a released installation already contains the change.

Validation and reproduction

The focused geometry suite includes the missed triclinic tie, translation and reversal, exact and one-ULP boundary controls, untrusted reduction/shell inputs, budget exhaustion, singular/nonfinite cells, invalid tolerances and int64 overflow. Existing positive-tolerance random-cell comparisons remain in the same suite. The stage-2 harness now requires zero missing exact ties by default and repeats the DF rounding-bound and native implementation checks.

Submit these files together through the calculation scheduler using a qualified vibe-qc installation with NumPy, ASE and pytest:

  • formal/check_exact_images.py

  • formal/check_stage2.py

  • formal/stage2_reference.py

  • tests/test_ccm_wigner_seitz.py

Run with assertions enabled:

python check_exact_images.py --pytest-file test_ccm_wigner_seitz.py

For a Python-only source test, add --source-overlay /path/to/geometry-sources, containing the proposed wigner_seitz.py and _exact_images.py. The script records this distinction. After collecting its outputs, replay the production certificates in the pinned Lean 4.35.0/mathlib environment:

python formal/check_stage2_proofs.py --certificates /path/to/production-image-certificates.lean

The integration calculation uses a two-hydrogen triclinic cell containing the exact boundary tie, checks its weight matrices and nuclear pair ledger, and compares converged zero/positive-tolerance CCM SCF results when their weights agree. A separate water/STO-3G molecular-limit calculation runs through the same CCM driver and compares with the existing matched ORCA 6.1.1 result. There is no matched external reference for the finite triclinic experimental CCM model; its internal agreement is not labelled external method validation.

Recorded acceptance

The source-overlay run against the qualified 0.18.7 native runtime passed all 19 focused geometry tests and all 12 stage-2 geometry cases, with no missing production exact ties. The DF rounding-bound checks and discriminating controls also passed. Its exported certificate file is byte-identical to the independently audited file: 15 universal claims and 29 generated claims passed Lean’s kernel and transitive-axiom checks.

Calculation or ledger

Result (Hartree)

Triclinic H2 CCM, zero tolerance

-0.7055896471574881

Same CCM, positive tolerance and identical weights

-0.7055896471574881

Triclinic nuclear ledger and exact-distance reference

0.22645540682891913

Water CCM molecular limit, STO-3G

-74.96033706904919

Matched conventional water ORCA 6.1.1

-74.960337068945

The water difference is about 1.04e-10 Hartree, below the declared 2e-8 tolerance. All calculations used closed-shell RHF and converged with the acceptance script’s energy and residual criteria. The triclinic dense SCF call took about 0.22 seconds in this run, after weight construction; that is not a geometry throughput benchmark. Runtime integrity checking and library loading dominated job startup. An initial five-minute attempt timed out before producing test output; its record is retained alongside the successful longer run. These are checked source-overlay results and do not assert deployment of a new release.

Cost and remaining scope

Exact arithmetic and exhaustive enumeration cost more than the vectorized positive-tolerance path. The conservative inverse-row bound can grow sharply for sheared, ill-conditioned or very small cells. The integer radius is chosen for simple exact certification and is not scale-optimal. Each displacement currently recomputes the inverse and checks the box twice, once for construction and once for verification. The explicit budget makes failure visible but does not impose a strict wall-time or rational-bit-complexity bound.

A cached exact inverse, a tighter rational radius and a certified unimodular change of basis can improve throughput while preserving the certificate contract. Those are future optimizations. Interval-valued inputs, cutoff neighbor completeness, multi-k phases, CCM topology changes and a universal floating-point implementation proof remain separate obligations.