Stage 2: rounding bounds and certified triclinic images¶
This optional extension of the formal core adds two forms of verification: explicit propagation of local floating-point rounding errors through DF contractions, and complete nearest-image certificates for rational triclinic inputs. It uses the existing pinned Lean/mathlib environment. Production kernels and public geometry defaults are unchanged.
The 13 universal proofs and specification are in VibeQCStage2.lean. The independent reference and certificate producer, native checker and proof audit keep mathematical assumptions, Python execution, native observations and kernel-checked certificates distinct. The separate audit entry point lets other method modules evolve concurrently without changing their claim manifests.
DF: from local rounding to a two-stage absolute bound¶
The scope is a real Coulomb contraction using supplied, represented factors B and density D. With AO pair k standing for the full ordered pair of AO indices,
The exact reference is the rational/real value of those supplied finite binary numbers. Errors in integrals, fitting, metric truncation, the density itself or the preceding SCF solution are separate from contraction roundoff.
Local operation contract¶
For an exact intermediate x and represented result y, assume
The absolute allowance covers gradual-underflow rounding. The executable checker uses exact rational u=2^-52 and eta=2^-1074. These are conservative forward allowances, not a redefinition of binary64 unit roundoff u_0=2^-53.
Rump (2010), section 2, equations 2.1-2.4
gives a backward model with u_0 times |y| and half the underflow unit. Since
|y| <= |x|+|y-x| and 0 <= u_0 <= 1/2, it implies the forward allowance with
u=2u_0 and eta equal to the underflow unit. forward_rounding_allowance proves
that implication. It does not prove the IEEE implementation satisfies the
backward premise. The trace checker independently checks each observed operation
against exact operands; it rejects nonfinite results. No overflow, flush-to-zero,
reduced precision or arbitrary compiler transformation is assumed safe.
A trace and its bound¶
DotTrace describes separate multiply/add operations on a finite list of pairs,
processed from the tail. Each constructor carries the actual rounded product,
rounded tail accumulator and rounded sum, plus both local rounding inequalities.
A different reduction order must have its own trace or independently established
stage-error premise. Fused multiply-add is not silently treated as two separate
roundings.
For exact operands a,b and approximate operands ah,bh with errors ea,eb, the triangle inequality gives
rounded_add_error proves this estimate. Let t=a*b be the next exact product,
M the sum of absolute products in the tail and E the tail’s error budget.
Multiplication contributes at most u|t|+eta. Therefore the new budget is
The empty trace has E=M=0. dot_exact_le_mass and dot_trace_bound prove by
induction that the recursively defined dotBudget bounds the actual absolute
error of every trace satisfying its local premises. Cancellation does not
invalidate this bound, although a small result can have a large relative error.
This stage implements this recurrence rather than claiming a sharp gamma_n
bound for every BLAS implementation. All budget arithmetic in the Python bridge
uses Fraction, avoiding an unaccounted downward rounding of the bound itself.
Composition of the DF stages¶
Let e_P bound the first-stage error |rho_hat_P-rho_P|. Let e_out bound the second stage relative to an exact contraction with the rounded first-stage values. Adding and subtracting that intermediate contraction gives
df_two_stage_bound proves this finite-sum inequality; it permits different
ways of establishing the two stage bounds. absolute_error_enclosure converts
an absolute bound into lower and upper limits for the exact result.
df_dense_coulomb_bound connects the bound directly to the stage-1 denseJ
definition using its proved finite contraction identity.
The native checker obtains the resident C++ first stage through
contract_B_with and the final matrix through build_J. The inspected source
uses the same Eigen Frobenius reduction for both first-stage routes. Python
DensityFitting.build_J is also exercised with its explicit einsum first stage.
For every tested entry, the checker evaluates both local stage premises and the
composed bound in exact rational arithmetic. It also checks separate scalar
traces, including cancellation and subnormal multiplication.
The native premises are established for those recorded inputs and outputs. They are not a universal proof that Eigen, BLAS, vectorization, FMA or parallel scheduling implements the scalar trace. A native entry receives an additional Lean-checked rational enclosure. That finite-instance certificate likewise does not establish a compiler refinement theorem or every untested DF route.
Triclinic images: a finite completeness certificate¶
The geometry interface takes a 3 by 3 matrix A with lattice vectors as columns, and Cartesian displacement x, all in one consistent length unit. Finite floating inputs are interpreted as their exact binary rational values. Decimal physical uncertainty and uncertain cell parameters require an interval-input extension. No reduction-quality, orthogonality or fixed-neighbor-shell premise is used.
The producer finds an exact inverse H. The universal Lean theorem more generally allows a left inverse for a full-column-rank active basis. The current Python interface implements full-rank three-dimensional cells; singular inputs fail.
For integer n, define
inverse_residual proves f_i-n_i=sum_a H_ia r_a(n). Choose any integer incumbent
b, including an untrusted production proposal, and a rational R>=0 satisfying
q(b)<=R^2. The producer uses an exact integer ceiling of the square root; it
never computes a floating-point inverse or square root to establish completeness.
If q(n)<=R^2, every |r_a(n)|<=R. Consequently
residual_component_bound and inverse_row_bound prove these inequalities.
Choose integer endpoints satisfying
The producer uses floor and ceiling respectively. sublevel_in_box proves that
every image with squared distance at most R^2 belongs to the finite integer box
product_i [ell_i,h_i]. This deliberately conservative box avoids trusting a
numerical condition estimate or an approximate smallest singular value.
What the certificate checks¶
ValidImageCert checks, in exact rational arithmetic:
The inverse witness HA=I.
R>=0 and q(best)<=R^2.
Every lower/upper completeness inequality.
q(best)<=q(n) for every integer n in the complete box.
image_certificate_sound proves global optimality: an image inside the sublevel
set belongs to the box, while every image outside it is already worse than the
incumbent bound. image_certificate_all_ties proves that filtering the complete
box by equality to the best squared distance gives exactly all global minimizers.
The certificate exporter additionally checks equality with the returned finite
tie set. Optimality of one representative and completeness of all ties are thus
separate checked claims.
The Python producer/checker rejects malformed inverse witnesses, insufficient
bounds, wrong best images and missing or duplicated ties. A configurable maximum
candidate count is checked before enumeration. Exceeding it raises
SearchBudgetExceeded; no partial result is labelled certified. Highly sheared
or ill-conditioned bases can make this conservative method expensive. Supplying
a good incumbent reduces the box, but does not weaken any correctness check.
A certified change of basis or tighter reciprocal-row bounds is future work.
Connection to the current image routines¶
The current CCM minimum_image uses lattice rows, Minkowski reduction and a
fixed shell; NEB _minimum_image_diff uses lattice columns. The native harness
transposes explicitly and checks returned integer image labels against the
exact complete set. NEB returns a Cartesian displacement, so its squared
distance is checked numerically rather than claimed to be an exact integer-label
certificate. Translation and reversal are checked on the exact complete sets.
The certificate path is optional and is not installed in the production hot loop. It can check a production proposal and find a different minimizer if that proposal is wrong. The Python verifier is tested correspondence code; selected exported certificates are additionally replayed by Lean’s kernel. Inputs and outputs are preserved with hashes so a certificate for a different cell cannot be mistaken for evidence about the tested cell.
Exact ties and CCM’s default distance tolerance retain different meanings. The near-boundary fixture records the extra image admitted by the production tolerance. No theorem here certifies that tolerance policy, fractional boundary weights, cutoff-neighbor completeness, multi-k phases or CCM topology changes. Nearest-image sets can have topology-dependent multiplicities; no universal orthogonal face/edge/corner count is imposed on triclinic cells.
A detected production correspondence gap¶
The exact checker exposes a missing tie in minimum_image(..., tol_bohr=0) for
Both integer images (0,-1,0) and (1,0,0) have squared distance 39/32 and
are global minimizers. The tested production routine returns only (0,-1,0).
Consequently its returned weight is 1, whereas the complete exact set assigns
1/2 to each image. The selected image is optimal; exact tie-set completeness
and the resulting exact boundary weights fail on this fixture. Floating-point
distance evaluation cannot be equated with the exact predicate at a boundary.
The harness preserves this counterexample, checks that the native proposals
are genuine minimizers, and reports production_exact_tie_completeness: FAIL.
Its overall status is PASS_WITH_LIMITATION when the certified reference,
rounding checks and expected-counterexample regression succeed. This is not an
unqualified native PASS. The exported certificate proves the complete exact
set, including the image omitted by production. No production tie tolerance or
weight policy was changed to make the comparison pass.
Observed numerical evidence¶
All 13 universal claims and 14 generated certificate claims pass the Lean axiom audit. The final scheduler run completed normally on vibe-qc 0.18.6. All 12 geometry fixtures passed exact verification of the native returned labels’ optimality, and the certified sets passed translation/reversal checks. One fixture failed production exact tie completeness as described above. There were 12 rejected invalid/perturbed cases and three additional discriminating controls.
DF fixture |
Maximum absolute error |
Maximum entrywise error/bound ratio |
|---|---|---|
Synthetic nonsymmetric factors |
1.39e-15 |
0.0249 |
Large signed cancellation |
6.25e-4 |
0.0770 |
Resident native water factors |
2.26e-16 |
0.0194 |
Each error and comparison with its bound was evaluated exactly; the table’s values are rounded for display. The maximum ratio need not occur in the entry with maximum absolute error. Bounds were not tuned to these residuals. The cancellation fixture contains density entries of magnitude 1e12, making an absolute residual alone an inadequate acceptance rule.
The complete conventional H2O/STO-3G RHF calculation gives -74.96033706904934 Hartree, within 1.05e-10 Hartree of the matching existing ORCA 6.1.1 reference. That reference validates the molecular fixture’s energy; it does not establish the rounding model, geometry completeness or DF fitting accuracy. Runtime/source identities and the original failed harness runs are preserved in the private evidence repository. Production DF and CCM image sources under review were unchanged from the inspected runtime source.
Reproduce and audit¶
Use the existing pinned Lean 4.35.0/mathlib project and cache. From the repository
root, with lake on PATH:
python formal/check_stage2_proofs.py
Submit formal/check_stage2.py and formal/stage2_reference.py through the
calculation scheduler using a qualified vibe-qc Python with NumPy, ASE and
resident native DF bindings. Run normal Python with assertions enabled:
python check_stage2.py
The job writes stage2-checks.json, exact native fixture data in
df-native-inputs.npz, and stage2-certificates.lean. Fetch those outputs and
run the independent kernel audit:
python formal/check_stage2_proofs.py --certificates /path/to/stage2-certificates.lean
The audit compiles the universal module, enforces its exact claim manifest and
checks every theorem’s transitive axioms. Generated certificate claims are
checked in the same way. The allowed standard base remains propext,
Classical.choice and Quot.sound. decide +kernel evaluates finite certificates
through Lean’s kernel; compiler-trust evaluation and admitted proofs are rejected.
The source hashes and pinned dependency manifest are recorded. Raw reports can
contain private environment paths and belong outside the public source tree.
The evidence distinguishes universal conditional theorems, kernel-checked finite certificates, exact rational Python checks and tolerance-based native comparisons. The staged implementation adds no production runtime dependency. Original code uses MPL-2.0; Lean and mathlib retain their existing upstream licenses.