vibe-qc/Documentation

Formal verification strategy for the numerical core

Design proposal, 1 November 2026. No production-code change is part of this proposal. The source inventory below was checked against main at 13ac9dc419334fcae41c8771739b9c90c7ab93a7.

Keep Lean 4 as an optional development dependency and build a small verified mathematical core around units, finite tensor sums, lattice geometry and energy accounting. Connect it to existing Python/C++ routes through explicit contracts, small reference evaluators and discriminating implementation checks. Adopt compile-time types at selected C++ boundaries and runtime validation at Python, file and native boundaries incrementally. Do not rewrite the chemistry engine or make a general tensor compiler a prerequisite.

This extends the existing formalization, including the RHF, UHF, density-fitting and MP2 examples. Its 28 registered Lean claims are bounded mathematical results; the native comparisons are numerical evidence. All additional obligations in this proposal are future work. No existing theorem proves the compiled engine, arbitrary triclinic image selection, IEEE-754 execution or physical adequacy of a model.

Literature and reusable software

The following map uses the primary texts, including their equations and stated limitations. The suggested architecture is our inference from those texts and the implementation, rather than a result established by any one paper.

Primary text and passages	Consequence for this design
Bobbin et al., Formalizing chemical physics using the Lean theorem prover, Digital Discovery 3 (2024), 264-280, DOI, sections 2, 3.1-3.3 and 4	Separate model definitions, hypotheses and derived results. Their Langmuir/BET examples expose denominator and convergence assumptions. Reuse that structure for method contracts; these are chemical-theory proofs, not electronic-structure implementation proofs. The paper uses Lean 3.51.1.
Ugwuanyi et al., Benchmarking energy calculations using formal proofs, Molecular Physics 123 (2025), e2539421, DOI, sections 4.2-4.5, 5.1-5.3 and 7	Reuse the separation of algebra, image conventions, pair enumeration and executable checks. Pair-list cardinality alone does not prove uniqueness and completeness. The component-wise box construction is not a general triclinic closest-vector proof. Section 5.3’s parser lost atoms despite the mathematical proofs.
Bobbin et al., Formalizing dimensional analysis using the Lean theorem prover, arXiv:2509.13142v1, sections 3, 4 and 5, derivative appendix	Dimensions as exponent maps and quantities indexed by dimension fit a small unit algebra. Keep unit scales and semantic coordinate tags separate. The LJ example demonstrates dimensional expressions and derivatives, not correctness of conversion constants or floating-point kernels.
Tooby-Smith, Formalization of physics index notation in Lean 4, arXiv:2411.07667v1, sections 2.1-2.4 and 3	Useful architecture: syntax, typed expression tree, mathematical denotation. Index species and contraction legality prevent ambiguous notation. Section 2.4 explicitly says elaboration itself is not formally verified. Start with explicit finite sums; adopt richer notation only when it reduces maintenance.
Ugwuanyi et al., LeanBET, arXiv:2605.16169v1, sections 3.2, 4 and 5.1-5.6	Reuse explicit admissibility predicates and soundness statements for selectors. Section 5.2 separates real-number soundness from floating-point threshold behavior. Shared polymorphic arithmetic is useful for reducing drift; it is not a round-off theorem.
Tooby-Smith, A Perspective on Interactive Theorem Provers in Physics, DOI, sections 2-5, especially 5.1-5.2	Organize APIs around physical structures and retain physical interpretation in theorem documentation. Preserve computable data structures where useful. A correct theorem about the wrong structure remains the wrong scientific specification.
Peintinger and Bredow, The cyclic cluster model at Hartree-Fock level, DOI, two-, three- and four-center sections, equations 4-7, 11-13 and 18-24	Two-center boundary weights do not define every CCM operator. Nuclear attraction uses a union construction, and four-center weights have additional factors. Formalize the selected construction separately from geometric nearest-image selection.

The local library collection records exact PDF filenames and acquisition provenance under collections/formal-verification/. The Bobbin companion is a complete accepted manuscript with its supporting section, not a separate publisher SI. The CCM primary text is catalogued as pbc/2014_peintinger_the-cyclic-cluster-model-at.pdf. No upstream proof project was compiled as part of this design review.

Software metadata was inspected on 1 November 2026. Pin a complete commit and dependency manifest before reuse; paper versions and repository heads differ.

Software	Inspected revision, toolchain and licensing	Recommended use
LeanChemicalTheories	00841fed; Lean 3.51.1, mathlib f2ad3645; no repository license file found	Read for design; do not copy code without resolving permission. Lean 3 source needs porting.
LeanLJ	7ef4fe84; Lean 4.16.0-rc2; Apache-2.0	Candidate small lemmas and pair-enumeration patterns, subject to porting and statement review.
LeanDimensionalAnalysis	de263eed; Lean 4.23.0-rc2; Apache-2.0; paper mentions mathlib 4.23.0-rc1	Compare a small dimension API before importing the whole project.
PhysLean, now physlib	a8823c76; Lean 4.35.0; Apache-2.0	Candidate physics/tensor lemmas; same Lean version does not establish dependency-manifest compatibility.
LeanBET	c0602721; repository Lean 4.27.0-rc1, paper says Lean 4.27.0; no repository license file found	Use its specification/check separation as an architectural example; resolve permission before copying source.
SciLean	95f8119a; Lean 4.28.0-rc1; Apache-2.0	Later experiment for executable scientific kernels and differentiation; not a first-milestone dependency.

Keep the existing Lean 4.35.0/mathlib v4.35.0 environment and its locked manifest. Reuse mathlib finite sums, matrices, real/complex algebra and calculus. Original vibe-qc additions remain MPL-2.0. Preserve upstream notices for any permitted imports, record provenance and dependencies, and keep build caches out of distributions. A paper’s open-access license does not license its repository. Missing license files above mean permission is unresolved, not an assertion that the authors prohibit reuse.

Current code and failure modes

This is a representative inventory of the requested four domains, not a claim to inspect every kernel in the method inventory. Source links identify the implementations; function names remain useful when line numbers change. The listed risks are distinct from reproduced failures.

Domain	Inspected implementation	Contract or concrete failure mode
Input units	molecule.py, from_xyz, ANGSTROM_TO_BOHR; build.py; guess_read.py	XYZ/ASE lengths in Angstrom become internal bohr. The conversion constant is repeated. A second conversion or an omitted conversion has the correct array shape and wrong physics. Preserve the existing CODATA-2018 value during migration.
Lattice conventions	periodic.hpp, periodic.cpp, PeriodicSystem::reciprocal_lattice; CCM system	Native direct and reciprocal matrices have vectors in columns; CCM helpers use rows. Reciprocal native matrix includes 2*pi. Equal dimensions cannot detect transpose or phase-convention errors. Inactive native columns are bookkeeping for dim 1/2, not extra physical periodicity.
Output units and derivatives	ase.py, smearing constants, stress	ASE energy is eV and force is negative gradient times Hartree/Bohr; smearing accepts K/eV/Ry conversions. GPW/GAPW stress is a fixed-density finite difference in Ha/bohr^3, with symmetric-shear factor 4. It is not an analytic relaxed-SCF stress.
Dense Fock	fock.cpp, build_fock_g, build_coulomb, build_exchange; rhf.cpp, uhf.cpp	Real chemists’ ERIs, spin-summed RHF density, J - K/2; UHF separates spin exchange. Wrong exchange permutation or density spin factor can preserve symmetry and still change the energy.
DF	density_fitting.py, build_J, build_K, build_K_density, mo_transform; df.cpp; storage tests	Logical factors B[P,mu,nu] differ from flattened storage. Occupied-orbital K is unweighted, while density K carries density occupations. build_K prose mentions 2J-K, whereas native spin-summed Fock uses J-K/2: document both conventions with their densities. Existing tests cover historical storage/metric defects and retired streaming refusal; do not revive retired paths merely for a proof demo.
Correlation	mp2.cpp, accumulate_incore, accumulate_slab; ccsd.cpp, compute_energy; chi MP2	Real MP2 uses `(ia
Multi-k contractions	multi-k Fock, density, kmesh_address.hpp, bloch.cpp	Cartesian angular wavevectors, complex Bloch phases, weighted densities and exact modular mesh addresses. Mixing preweighted density with another k weight, dropping conjugation or applying 2*pi twice are separate errors.
Wrapping and cutoff domains	ewald.cpp, centered_periodic_representative, for_each_pair_candidate; lattice_sum.cpp, direct_lattice_cells	Ewald wrapping relabels a pair-complete cutoff sum; it does not claim to select the nearest image. A cutoff on `
Nearest images	wigner_seitz.py, _minkowski_reduce, minimum_image; neb.py, _minimum_image_diff	Reduced-basis finite search, not naive rounding. CCM reduction catches import errors and returns the original basis; cached reduced_basis is accepted without verifying its relation to the lattice. The rim check does not itself prove global optimality. These are assurance gaps; this review did not reproduce a normal-path ASE failure.
CCM topology	CCM weights, cell_weight_matrices; padded.py; gradient_analytic.py	A distance tolerance of 1e-6 bohr defines a numerical tie set. Equal weights sum to one even if the wrong images were selected. Three-/four-center constructions, cache validity and topology derivatives are additional obligations. The program-union and printed-eq13 nuclear variants must remain distinct.
Totals and corrections	runner.py, result wrappers; ase.py; CCM SCF, CCMRHFResult	Legacy .energy and corrected .energy_total can mean different quantities. CCM .energy is a total cyclic-cluster energy; divide by n_cells for primitive-cell reporting. Adding dispersion, solvent or correlation twice is a reporting error even with correct individual kernels.
Electrostatics and embedding	ewald.cpp; embedded pieces; Lloyd energy, two-step embedding	Ewald includes real, reciprocal, self and background terms. The real sum skips all distances below 1e-14, so a proof must exclude distinct coincident nuclei, not interpret every skipped term as legitimate self-interaction. Static embedding includes QM-external terms but no external-external energy. Lloyd band-energy change is only one contribution to adsorption energy.

The GPU design is a roadmap, not evidence of shipped GPU verification. Connect future accelerated DF routes to the same logical contractions; record the actual device, precision and backend once implemented. No GPU execution or performance claim is made here.

Architecture and trust boundaries

Use four layers with an explicit bridge between them:

Published formulation and semantic contracts
                 |
Lean definitions -> exact theorems -> audited claim manifest
                 |
Finite reference evaluator + input/output contract
                 |
Named Python/C++ route -> native libraries -> optional device backend
                 |
Recorded numerical comparisons and matched scientific calculations

The downward arrows are not all proofs. Initially the connection from the reference evaluator to production is tested correspondence. Each claim record should hold: definition and theorem names; hypotheses; unit/index/normalization conventions; source symbols and revision; applicable routes; proof status; numerical evidence; external assumptions; and remaining exclusions. A hash detects changed source; it does not establish semantic equivalence.

Extend the existing formal/rhf Lake project first, adding a VibeQCCore namespace with Units, Contractions, Images and Accounting modules. Avoid a second Lean version and avoid renaming the existing project as part of the first milestone. Use the existing axiom audit: no sorry, admit, extra scientific axioms or compiler-trust shortcut. The Lean kernel, foundational axioms and pinned dependency sources remain trusted.

Reference functions should be tiny, finite and deliberately independent of production packing: explicit sums over labelled spaces; exact rational fixtures where possible; high-precision numerical evaluation where square roots or transcendental functions are needed. Lean Real definitions are not executable numerical oracles. If a rational evaluator is written in Lean, prove that its interpretation in Real matches the specification. Python reference evaluators remain tested implementations until a connection is proved.

For a stronger bridge later, verify a checker rather than the entire optimized engine. Production may propose an image set, permutation or pair list; a small checker establishes the relevant finite predicate. Prove the checker’s soundness, and separately connect its executable arithmetic and input decoding to that predicate. An ordinary Python checker or unchecked float comparison is not yet a proof-producing checker. Compiler/FFI/BLAS/GPU assumptions remain visible even for a verified source algorithm.

Units and semantic types

Use Dimension = BaseDimension -> integer exponent initially, extending to rational exponents only when a real use case requires them. A quantity has a dimension and a positive unit scale; coordinates additionally carry a semantic frame. Atomic units simplify numerical values, not dimensions or conventions.

Quantity	Internal contract	Boundary conversion or semantic constraint
Cartesian position and displacement	Length, bohr, finite 3-vector; distinguish point from displacement	Angstrom input converts once. Position minus position gives displacement; adding two positions is not a physical vector operation.
Direct lattice	Length, bohr, columns A; active columns independent	Row-oriented external/CCM view is explicitly A.T. Record periodic mask/dimension and frame identity.
Fractional position/displacement	Dimensionless, tied to a particular direct lattice	r = A f; dimensionlessness does not make it interchangeable with an arbitrary scalar or fractional k coordinate.
Reciprocal lattice/wavevector	Inverse length; distinguish cycles from angular wavevector	B = 2*pi*A^(-T), A.T*B = 2*pi*I; k = B q; k dot r is the phase in radians. A 2*pi-free reciprocal basis has a separate tag.
Energy and temperature width	Energy in Hartree; temperature in K is different	eV/Ry conversion is explicit; k_B T is an energy. Constant provenance and decimal representation are part of the boundary contract.
Gradient and force	Energy/length, Ha/bohr	F = -grad E; ASE force scale is Hartree/Bohr. A sign tag is needed in addition to dimensions.
Stress	Energy/volume, Ha/bohr^3, tensile-positive strain derivative	sigma = (1/V) dE/depsilon; pressure is negative mean normal stress. Specify shear convention and fixed fractional coordinates. For lower-dimensional systems use line/surface quantities or an explicitly chosen reporting thickness, not bookkeeping volume.
Hessian, cutoff and tolerance	E/L^2; L or L^-1 as appropriate	Distance tolerance and squared-distance tolerance are different. An energy cutoff is not an inverse-length cutoff, even when linked by `

First prove conversion composition and inverse laws for positive scales, and derivative conversion: for x = s_L x' and E = s_E E', dE'/dx' = (s_L/s_E) dE/dx. For dimensionless strain, stress scales as s_L^3/s_E. This proves the transformation law, not the measured values of physical constants or exact binary round trips.

At C++ interfaces use lightweight wrappers such as LengthBohr, CartesianDisplacement, DirectLatticeColumns and AngularKVector with explicit constructors. Keep numeric storage compatible with Eigen/BLAS; do not wrap each scalar in a tensor’s inner loops. Distinct index-space tags also prevent mixing equally sized AO and auxiliary spaces. Python uses small validated boundary objects or adapters and explicit names; annotations alone do not enforce NumPy semantics. Runtime validation checks shapes, finite values, positive scales, active rank, dtype, layout and allowed conventions.

Migrate existing raw-array calls through backward-compatible adapters, retain their defaults, and test old/new calls for parity. Deprecate ambiguous entry points only in a separately scheduled API change. Consolidating constants is useful but must not silently update their values or external-format semantics.

Tensor reference layer

Use finite, distinct spaces AO, Aux, Occ, Vir, Spin, KPoint and Cell. A size alone is insufficient: AO and auxiliary spaces of the same dimension are still different. Record scalar field, axis order, strides, flattening maps, occupation convention and conjugation. The initial real finite-basis identities require no general-purpose tensor syntax.

Operation	Specification and assumptions
RHF/UHF J and K	For real D[AO,AO], g[AO,AO,AO,AO] in chemists’ order: J_mu,nu = sum_l,s D_l,s g_mu,nu,l,s; K_mu,nu = sum_l,s D_l,s g_mu,l,nu,s. RHF D=2 Cocc Cocc.T, F=h+J-K/2; UHF F_alpha=h+J[Dalpha+Dbeta]-K[Dalpha]. State ERI symmetries only for claims that need them.
DF J	Real B[Aux,AO,AO]; gtilde_mu,nu,l,s = sum_P B_P,mu,nu B_P,l,s. Prove dense contraction equals the two-stage gamma_P=sum_l,s B_P,l,s D_l,s, J_mu,nu=sum_P B_P,mu,nu gamma_P, by finite-sum interchange. This holds for arbitrary finite real B and D; DF approximation accuracy is separate.
DF K	X_P,mu,i=sum_nu B_P,mu,nu C_nu,i, then K_mu,nu=sum_P,i X_P,mu,i X_P,nu,i. Prove equality to density contraction for D=C C.T; double occupations require the corresponding factor two. The real B symmetry convention must match the density implementation.
Molecular MP2	g[i,a,j,b] shape (no,nv,no,nv), Delta=eps_i+eps_j-eps_a-eps_b != 0. Full ordered sums give E_OS=sum g^2/Delta, E_SS=sum (g^2-g*g_exchange)/Delta. Prove slab packing/reindexing separately from the existing scalar identities. Frozen-core selection is an explicit index injection.
Restricted CCSD energy	T1[no,nv]; flattened T2[i*no+j,a*nv+b]; V[i*nv+a,j*nv+b]; tau=T2+T1*T1 for CCSD. Energy 2 sum f_ia T1_ia + sum tau_ijab (2 V_iajb - V_ibja). Linear/QCI switches omit the quadratic tau term. Verify this contraction before attempting all residual equations.
Complex periodic extension	Explicit bra/ket roles, conjugate transpose, momentum-conserving tuples and k weights. Require P(k)=P(k)^dagger, D(-R)=D(R)^dagger for appropriate transforms and state phase signs. Weighted density is a separate type. Chi MP2’s Nk^-3 applies to its complete uniform-character construction; do not reuse it for an arbitrary irreducible mesh.

For molecular real ERIs, the usual within-pair and pair-exchange symmetries are explicit hypotheses. Complex orbital integrals need different conjugation relations. First prove a generic adjoint/trace identity for complex matrices, then instantiate the actual periodic conventions; do not replace every real transpose by an adjoint mechanically.

Connect CPU/GPU routes with named pack/unpack maps and declared accumulation policies. Prove that flatten/unflatten are inverse bijections and that tiled index sets partition the full domain without overlap or omission. Then compare actual native outputs, not copied production formulas, with the finite-sum reference on nonsymmetric diagnostic tensors and physically symmetric ones. For a future expression tree, include sum, product, permutation and conjugation nodes with a denotation; prove each rewrite preserves that denotation. Generated code still needs a refinement or validation argument.

Floating-point reassociation is a separate obligation. For a specified serial dot product, the familiar target is an absolute forward-error bound of the form gamma_m sum |x_i y_i|, with gamma_m=m*u/(1-m*u) and m*u<1. Derive the correct operation count and hypotheses for the actual implementation, including input error, FMA policy, subnormals, overflow and summation tree. This expression is a proposed proof target here, not a proved bound for BLAS, OpenMP or GPU reductions. Cancellation makes a relative-only tolerance unsafe. Mixed precision and screening add distinct errors. Algebraic equivalence does not bound any of them.

Four distinct periodic operations

Let A contain the d independent active lattice vectors as columns, 0 <= d <= 3, and Lambda={A n : n in Z^d}. A molecule has d=0 and only the zero translation. The core can support left-handed full-rank bases with volume abs(det A) in 3D; any backend requiring positive orientation must say so. Reject nonfinite or rank-deficient active bases. Numerical admission also needs conditioning and work-budget limits, since mathematical invertibility does not imply a stable inverse or affordable enumeration.

1. Wrapping chooses a representative modulo Lambda, for example with fractional coordinates in [-1/2,1/2). Prove lattice equivalence, idempotence and invariance under integer translations. This parallelepiped representative need not be closest to the origin. Existing rint/nearbyint ties-to-even behavior differs at half integers from a half-open convention; preserve the old adapter behavior until a deliberate migration.

2. Nearest-image search returns the minimum squared distance and ideally the complete set M_A(x)={n : ||x-A n||^2 is minimal}. Prove optimality, M_A(x+A m)=M_A(x)+m, and M_A(-x)=-M_A(x). These imply distance translation invariance and symmetry. A single lexicographic tie representative can be deterministic but need not give an odd displacement at a boundary.

3. Cutoff-neighbor enumeration returns all (i,j,n) satisfying ||r_i-r_j-A n|| <= R, with an explicit self policy and pair ownership. Prove soundness, completeness and uniqueness. It is not nearest-image selection: large cutoffs can include several images of the same atom. Equality is included for a closed cutoff; shell ordering is not pair ownership.

4. CCM selection starts with a complete nearest-image set, assigns exact rational weights 1/|M|, and constructs the selected two-/three-/four-center operators. Prove partition of unity and reciprocal pair mappings separately from geometry, then prove each operator’s required symmetries. An orthogonal cell has face/edge/corner multiplicities 2/4/8; arbitrary Voronoi cells must use the actual multiplicity, not those fixed numbers.

Naive fractional rounding has an exact counterexample. Take columns a1=(1,0,0), a2=(9/10,1/10,0), a3=(0,0,1) and f=(49/100,49/100,0). Then x=A f=(931/1000,49/1000,0). Rounding f to zero gives squared distance 434581/500000; choosing image n=(0,1,0) gives 1781/500000, strictly smaller. These two rational values were checked during this design review. This disproves rounding’s general optimality, not the existing reduced-basis normal path.

For orthogonal active vectors, squared distance separates into independent one-dimensional terms, so coordinate-wise nearest integers are optimal. Prove this first, including all ties and the unchanged perpendicular component for dim 1/2.

For triclinic cells, use a complete bounded-search reference. Let L be the left inverse/pseudoinverse of A, s=L x, and let an initial integer candidate n0 give radius R=||x-A n0||. Every candidate at least as good obeys

|n_i-s_i| <= ||row_i(L)|| R.

This follows from L(x-A n)=s-n and Cauchy-Schwarz. Enumerating every integer inside these coordinate bounds therefore contains every minimizer. The same bound with a prescribed cutoff proves neighbor completeness. A rational upper bound on each row norm and R suffices for a conservative exact enclosure; floating inverse/norm evaluation requires outward-certified bounds. Arbitrary padding constants are not such a certificate.

Keep Minkowski reduction as the fast production strategy. Its assurance route needs an integer unimodular transform U, the relation A_reduced=A U (or L_reduced=U L in row convention), a verified reducedness predicate, and a theorem that the chosen finite shell suffices under that predicate. Check transform identity and lattice binding for cached reductions. If these conditions are unavailable, use a complete bounded search or reject the request; silently using an arbitrary unreduced basis cannot inherit the reduced-shell theorem. A selected image away from the search rim is not a completeness certificate.

The current CCM tolerance defines a separate approximate predicate distance <= minimum_distance + tol_bohr. Proving exact partition of unity for its returned set does not prove it is the exact tie set. Proposed future result metadata includes exact/certified/approximate status, tie policy, distance gap or interval, lattice identity and selected construction. Near a boundary, use interval comparison with refinement or explicitly report an unresolved tie. Recompute topology when coordinates, cell, tolerance or CCM construction change; cached weights are not timeless geometry facts.

Multi-k interfaces carry integer mesh addresses, shift parity, reciprocal wraps and Bloch-phase convention alongside Cartesian k. Extend the existing integer kmesh_address design rather than reconstructing addresses by rounded floats. Prove finite-group address bijections and momentum conservation separately from geometry and Fourier normalization. CCM and chi-CCM need construction identities as well as the same finite translation group; matching mesh sizes alone does not prove operator equivalence.

Energy accounting and derivatives

Use a route-specific ledger whose entries have a value, dimension, extent (molecule, cyclic cluster, primitive cell or atom), physical role, provenance, and inclusion status. Include a convention/version key for electrostatic gauge, occupations and CCM construction. The final reporting layer consumes this ledger once. Do not infer inclusion from attribute names or add every quantity containing the word energy.

Route	Accounting contract
Real RHF	E_elec=<D,h> + <D,J[D]>/2 - <D,K[D]>/4, with spin-summed D; E_total=E_elec+E_nn before explicitly selected corrections. Existing half-Fock and derivative identities apply under their stated symmetries.
UHF	E_elec=<Da+Db,h> + <Da+Db,J[Da+Db]>/2 - (<Da,K[Da]>+<Db,K[Db]>)/2. Do not apply the RHF exchange factor to each spin density.
DFT and corrections	One-electron plus Hartree plus XC energy and selected exact exchange, followed by route-specific nuclear, dispersion, solvent and other terms. XC energy is not generally half the density-potential contraction. DFT+U and solvent terms must be marked already included or external. Smearing entropy/free energy has its own reporting and force-consistency contract.
Correlation	Correlated total equals the matching reference total plus the chosen correlation correction. Frozen core, spin scaling and reference identity accompany it. A wrapper’s raw SCF .energy must not be substituted for its correlated .energy_total.
CCM	E_cyclic=E_electronic+E_nuclear; E_per_cell=E_cyclic/n_cells; E_per_atom=E_cyclic/n_atoms. Positive counts and consistent extents are required. ccm_nuclear_repulsion loops over supercell atoms: its reference cell is the cyclic cluster, consistent with the SCF result, not automatically a primitive cell.
Ewald	E=E_real+E_recip+E_self+E_background for the selected finite domains/gauge. Ordered real pairs have factor 1/2; reciprocal zero mode is excluded as specified; point-self subtraction and background are different terms. Finite-cutoff equality to an infinite Coulomb sum needs a separate tail argument. Dim 1/2 electrostatics need their own contracts.
Static embedding	h=T+V_QM+V_ext+V_AIMP; nuclear term is QM-QM plus QM-external. No factor 1/2 on a once-enumerated cross interaction. External-external energy is excluded in this route and must not be silently added or assumed present. Polarizable/self-consistent embedding needs a different functional and response contract.
Green-function embedding	Band-energy or Lloyd band-energy change is not the full total/adsorption energy. Double-counting, electrostatic and reference terms must be supplied by an explicit total-energy definition before claiming total-energy or force consistency.

The first accounting theorem uses a finite pair set and a fixed-point-free involution (i,j,n) -> (j,i,-n). If support and weights are invariant under this involution and pair contributions agree, half the ordered sum equals one representative per orbit. Exclude only the true (i=i,n=0) self term; nonzero periodic self images are generally legitimate. Distinct coincident charged centers are singular and outside the Coulomb domain, not zero-energy pairs. Pair cardinality alone would not establish these facts.

For geometry derivatives, restrict the initial claim to an open neighborhood with constant image/pair support, fixed weights and cutoffs, no collision, and differentiable component kernels. Then a finite energy sum differentiates term by term and F=-grad E. With normalized energy, normalize its gradient by the same fixed count. This statement does not include orbital/basis response: SCF stationarity, occupation stability, Pulay terms and a converged branch need additional hypotheses and proofs. Correlated forces need their response or Lagrangian theory, not the HF stationary argument.

At an image switch the minimum squared distance is continuous but generally not differentiable; a selected displacement can jump. A hard cutoff can make energy discontinuous unless the kernel vanishes at the boundary, and force continuity needs a stronger switching condition. CCM tolerance-band membership and boundary weights can change discretely. Do not claim smoothness there; report topology changes and test each side. A future smooth CCM weighting scheme changes the model and requires a new derivation. Singular configurations, SCF branch changes and occupation crossings remain outside fixed-topology claims. Stress additionally specifies cell deformation, held-fixed variables, volume and shear normalization.

Prioritized proof obligations

All entries below are proposed, not newly proved. Each ID should become a claim-manifest entry with its actual theorem and implementation evidence.

Priority and ID	Precise target	Assumptions and exclusions
P0 U1	convert_c_b(convert_b_a(q))=convert_c_a(q); inverse conversion; derivative scale law above	Positive exact scales, differentiable function. Excludes constant metrology, parser and floating round trips.
P0 T1	DF two-stage J equals the four-index Gram-tensor contraction for every finite B,D; pack/unpack are inverse	Real scalar arithmetic and declared finite spaces. No fitting accuracy or numerical reassociation conclusion.
P0 P1	Orthogonal nearest-image set is complete and optimal; distance translation invariance and symmetry; d=0 is ordinary distance	Independent mutually orthogonal active columns; exact integers/reals and explicit ties. No arbitrary skew-cell assertion.
P0 E1	Half the ordered pair sum equals one sum per reversal orbit; ledger normalization commutes with finite summation	Finite inversion-closed support, symmetric contributions/weights, no fixed points, positive normalization count. No topology derivative yet.
P1 U2	A.T*B=2*pi*I, row/column adapter equivalence and k dot A n=2*pi q dot n	Nonsingular 3D A and declared angular reciprocal convention; active-subspace counterpart for d<3. No numerical inverse bound.
P1 P2	Left-inverse bounds enclose every cutoff neighbor and every nearest minimizer; exact enumeration has no duplicates	Full column rank, finite cutoff, exact/conservatively enclosed arithmetic. Resource exhaustion rejects rather than truncates.
P1 P3	Nonempty complete CCM tie set with weights 1/card has total weight one and reciprocal image covariance	Exact ties; approximate tolerance policy is a different predicate. No implication for three-/four-center operator correctness.
P1 E2	Fixed-topology finite energy derivative equals sum of component derivatives, with sign and normalization	Constant support/weights in an open neighborhood, smooth nonsingular kernels. Excludes switches, SCF response and missing embedding terms.
P1 T2	Molecular MP2 slabs partition the ordered tuple domain and preserve OS/SS energies; CCSD energy packing preserves its explicit formula	Nonzero denominators, specified amplitude/spin convention and active/frozen injections. No amplitude convergence or perturbation validity proof.
P2 P4	Reduced-basis shell search refines P2 and integer mesh operations satisfy group/address laws	Verified reducedness/unimodularity; integer range checks for machine indices. ASE output remains an assumption until certified.
P2 T3	Complex contractions preserve adjoints, momentum support and the specified Fourier/energy normalization	Declared phases, conjugations, mesh weights and symmetry hypotheses; no automatic extension from real molecular proofs.
P2 E3	Selected CCM multi-center operator symmetries and chosen embedding/Ewald component identities	Named construction/gauge and complete finite domains. Model validity and infinite-domain limits remain separate.
P2 N1	A bounded kernel’s IEEE-754 result differs from its exact model by an explicit bound	Concrete rounding mode, reduction order, input ranges, FMA/subnormal policy; no extension to unmodelled vendor/device kernels.

Minimal first milestone and verification plan

Deliver one tractable example per domain in the existing optional formal project, with a derivation, audited theorem and implementation adapter:

Example	Completion criterion and meaningful checks
Units	Prove U1 for length/energy and force conversion. Exercise XYZ to native bohr and ASE energy/force conversion with a nonsymmetric coordinate fixture. Reject wrong dimensions/frames at the new adapter. Include missing conversion, double conversion and force-sign mutations.
Tensor	Prove T1 for finite DF J and its chosen flattening. Compare public Python and resident native J on small factors/densities, including unequal AO/auxiliary sizes, noncontiguous input through supported adapters, and adversarial cancellation. Mutate a permutation, stride map and spin factor. Reuse existing DF storage evidence rather than rerun unrelated chemistry.
Periodic images	Prove P1 for positive orthogonal lengths, including all face/edge/corner ties and partial periodicity. Compare actual CCM/NEB outputs away from ambiguity, test the documented near-tie policy separately, and retain the rational skew counterexample as a negative control. Do not label the triclinic production routine verified at this milestone.
Accounting	Prove E1 and normalization laws. Compare explicit three-particle pair sums and a small fixed-support CCM nuclear ledger; omit the true self term, retain periodic self images where present. Mutate factor 1/2, omit a partner and divide by n_cells twice. Check reported total against components.

Use four complementary evidence categories throughout:

1. Proof: build the locked Lean project and audit transitive axioms and registered statements. Review the specification and hypotheses, not just whether the build succeeds. Compile-failure examples check illegal units and index mixing. Exact rational fixtures check the oracle independently.

2. Numerical correspondence: execute the real public/native route and compare intermediates as well as totals. Record absolute and scaled residuals, native digest, source, dtype, backend, reduction policy and input identity. Start with justified absolute-plus-relative tolerances; mark them as empirical until a bound is proved. A path that falls back must report the resolved path.

3. Metamorphic and boundary tests: integer translation, atom permutation, unimodular rebasing, coordinate rotation, density scaling, basis relabelling, reciprocal-phase periodicity and energy normalization. Include malformed counts, NaN/Inf, singular and ill-conditioned cells, huge indices, empty spaces, noncontiguous arrays and exact/near ties. Exhaustive integer boxes need a completeness bound; a large arbitrary search cube is only a test.

4. Integration/science: use existing matched RHF/UHF/MP2 evidence where the implementation is unchanged. Subsequent production changes get a focused complete calculation through the normal scheduler and matched ORCA/CRYSTAL comparison when applicable. Match basis, spin, frozen core, cell, gauge, k mesh, cutoffs, tolerances and energy extent. Small tensor agreement alone does not establish scientific validity.

Existing tests to extend rather than duplicate include CCM geometry, NEB images, DF storage, lattice cutoff, and stress. Keep the current RHF and extension harnesses. Their previously accepted results remain numerical evidence; this design adds no new native validation claim. No runtime suite or new chemistry calculation is needed to accept this documentation-only proposal.

For force checks, compare analytic components with finite differences over a range of step sizes within a recorded constant-topology neighborhood. Check one-sided behavior separately at switches. For stress, strain both lattice and fixed fractional coordinates consistently, and distinguish fixed-density from reoptimized-SCF comparisons. A good finite-difference match is a test, not a differentiability proof.

Cost, alternatives and staged implementation

These are planning estimates for an engineer comfortable with numerical QC and Lean, not delivery promises. Reassess after the first completed example.

Stage	Scope and exit condition	Estimated effort and runtime impact
0	This design, source map and claim boundaries	Documentation only; no runtime impact.
1	Four first-milestone examples, written derivations, axiom audit, native adapters and negative controls	Roughly 2-4 engineer-weeks, potentially longer while learning Lean. Optional build/test cost; no production hot-loop cost.
2	P2 complete triclinic reference, certified/enclosed bounds, tie policy, lattice/units adapters and energy ledger on one route	Roughly 3-6 additional engineer-weeks. Boundary checks are cheap relative to SCF, but full tensor scans and ill-conditioned lattice enumeration are not. Cache by immutable inputs; enforce budgets.
3	Certify reduced-basis output or add a qualified fallback; multi-k addressing/conjugation; CCM selected operators and fixed-topology derivatives	Several bounded follow-ups, likely months in aggregate. Keep reference search off the hot path unless fallback is needed. Benchmark reduction, checking and cache invalidation separately.
4	Selected floating-point refinement and optional accelerated contraction checks; expand through remaining method inventory	Research-sized work per kernel. No credible fixed date for whole-engine verification. Gate claims on delivered proofs and route evidence.

Lean builds and mathlib caches have nontrivial development disk/time costs; reuse the existing pinned cache and avoid adding several competing toolchains. Phantom/wrapper types can preserve numerical layouts, but measure ABI/inlining and template-build effects before claiming zero cost. Python validators should run once at a boundary rather than inside every SCF contraction. Full finiteness scans are O(tensor size); use debug/admission tiers or immutable validated buffers. Numerical reference evaluation is intentionally slow and restricted to small examples.

The minimal alternative is runtime contracts plus property-based tests with the existing Lean lemmas. It costs less and catches many integration errors, but gives no universal guarantee about geometry or accounting algorithms. That remains a useful fallback if the proof core becomes expensive to maintain.

For a later floating-point kernel, consider Gappa and Flocq as specialist tools rather than asserting that Lean’s real algebra covers rounding. They introduce a Rocq/tool boundary and additional maintenance; Gappa’s tool and proof support libraries have separate licenses, and Flocq is LGPL. Keep any initial experiment external to product runtime packaging. CBMC can address bounded C/C++ index and safety assertions; it requires explicit unwind/range coverage and does not prove arbitrary-size chemistry. Frama-C is an alternative for an isolated C kernel with ACSL contracts, with additional adaptation work for this C++/Python engine. None is a reason to rewrite the application or claim existing code was checked by those tools.

Before stage 2, settle these decisions with concrete prototypes: exact versus approximate tie API; fail-closed versus bounded-search behavior when reduction is unavailable; active-subspace conditioning/work limits; precision policy for near-boundary predicates; constants provenance; and backward-compatible ledger fields. Preserve current defaults until such changes are individually justified. Importing unlicensed code, changing a public API or adding a hard dependency requires its own resolved decision; none is necessary for stage 1.

After the shared core, continue the method inventory by reusing its contracts: finish full UHF/DF/MP2 contraction and derivative obligations, then DFT energy assembly, periodic multi-k and CCM, CCSD energies/residuals, local-correlation screening, multireference methods, response/gradients and dynamics. Each row must distinguish a defined model, proved identity, tested route and remaining approximation. A proof count is not a coverage metric for the engine.

The recommended next implementation is stage 1 in the existing Lean project, followed by the complete triclinic reference and one production boundary at a time. Publish a claim-level account of the results: selected mathematical specifications and proofs connected to tested implementation paths. Do not describe a verified reference model as a verified production engine, and do not make a first-in-quantum-chemistry priority claim without a separate, adequate prior-art investigation.