vibe-qc/Documentation

AICCM finite-torus RHF: derivation and proof bridge

AICCM/CCM remains experimental. This tranche proves 27 finite mathematical claims in VibeQCAICCM, extending the 58-claim stage-1 audit to 85 claims. It covers supplied real fitted integrals through the reported per-cell RHF energy and its density derivative. It does not prove the continuum torus construction, all of the manuscript’s equivalence theorem, or the production engine. The manuscript inventory is theory/formalization/equations.json in the AICCM article sources; stable labels below refer to Paper 1 and its SI.

Definitions, physical inputs and units

Let AO be the finite set of supercell real atomic orbitals and Aux the finite retained auxiliary set. Write

[ V_{ij,kl}=\sum_P B_{Pij}B_{Pkl},\quad J_{ij}(D)=\sum_{kl}V_{ij,kl}D_{kl},\quad K_{ij}(D)=\sum_{kl}V_{ik,jl}D_{kl}. ]

The factors are supplied data, symmetric in their AO pair. This is a density-fitting approximation to the chosen Hamiltonian, not a theorem that a fit equals the exact torus integrals. In atomic units, S and the spin-summed density D are dimensionless, B has energy dimension to the one-half power, and h, V, J, K and energies are in Hartree. The Coulomb self-potential xi has inverse-length dimension before the atomic-unit Coulomb factor is understood. Lean uses real scalar magnitudes; the units in this paragraph are an external contract, not dimension types.

Let S be symmetric, xi = xi_N the manuscript’s signed supercell self-potential, nuclear the supercell nuclear energy, and n a CellCount with natural-number value Nc > 0. Flatten (i,j) into one finite pair index and use the real component dot product. Define

[ T_{ij,kl}=S_{ik}S_{jl},\qquad A_{ij,kl}=V_{ij,kl}-\tfrac12 V_{ik,jl}+\tfrac{\xi}{2}T_{ij,kl}, ] [ F(D)=h+AD=h+J(D)-\tfrac12K(D)+\tfrac{\xi}{2}SDS, ] [ E_{\rm total}(D)=\langle D,h\rangle+ \tfrac12\langle D,AD\rangle+E_{NN},\qquad E_{\rm cell}=E_{\rm total}/N_c. ]

These are seamKernel, effectiveKernel, totalEnergy and perCell in Energy.lean, reusing VibeQCRHF.rhfKernel, fock and electronicEnergy. They instantiate manuscript eq:energy, eq:fock and eq:seam in the real supercell representation. The model choice to include this exchange seam, the Green function, and the values of B, h, S, xi and E_NN are inputs. There is no embedding term in this route; adding one would require a separate energy and double-counting contract. For the physical instantiation, Nc must equal the cardinality of the translation group and the replication product. CellCount encodes positivity, not a proof that a parsed mesh has that cardinality. This identification is an explicit bridge assumption and is tested for the two-cell fixture below.

Per-claim derivations

All names in this section have prefix VibeQCAICCM.. The exact statements are in formal/rhf/VibeQCAICCM/{Domains,Fitting,Energy}.lean and the complete machine-readable claim list is formal/rhf/claims.json.

Finite class domains and basis changes (7 claims)

These are the finite counting part of Appendix B (eq:class_trace) and parts of eq:identity, not a proof of an infinite image sum.

1. relative_class_sum: in any finite additive commutative group G, b -> b-a is a bijection, so summing f(b-a) over b gives sum_r f(r).

2. pair_class_accounting: sum the preceding equality over a to obtain sum_ab f(b-a) = |G| sum_r f(r). The zero relative class is included. It is a cell-label class, not permission to include singular particle self terms.

3. quartet_class_accounting: the product of three subtraction bijections maps (b,c,d) to (b-a,c-a,d-a) for each a. Summing the unchanged triple sum over the free origin gives |G|, not |G|^2 or |G|^4.

4. common_translation: cancellation in the group gives (b+t)-(a+t)=b-a, and likewise for the other two arguments. This proves invariance of a contribution already defined by relative classes; it does not establish that arbitrary production tensors have that form.

5. contraction_relabel: for a supplied finite equivalence e : I ≃ J, sum_i d(e i) h(e i) = sum_j d(j) h(j). A truncated or weighted selection is not such a bijection.

6. complex_trace_invariant: with complex square matrices and the explicit hypothesis U U† = I, cyclicity gives Tr(U† A U) = Tr(U U† A) = Tr(A).

7. complex_seam_trace_invariant: write D'=U†DU, S'=U†SU. Insert UU†=I between adjacent factors of D'S'D'S', then apply trace cyclicity to obtain Tr(D'S'D'S')=Tr(DSDS). Conjugate transpose is essential.

No character matrix is constructed by these lemmas. For the manuscript’s Bloch formula, a future proof must construct the full normalized BvK matrix, prove unitarity and block structure, and transform the complex two-electron tensor. The generic trace identity alone does not prove those steps.

Fitted interactions (6 claims)

These give finite fitted versions of eq:eriperm, eq:gramN, eq:fit and the real fitted specialization of eq:fock.

8. fitted_pair_swap: commute the two real factors in each summand of V_ij,kl to exchange (ij) and (kl). No AO-pair symmetry is needed here.

9. fitted_first_swap: B_Pij=B_Pji exchanges the first AO pair.

10. fitted_last_swap: the same hypothesis exchanges the second pair.

11. fitted_coulomb_square: expand the contraction, interchange only finite sums and regroup by P: sum_ij D_ij J_ij(D) = sum_P (sum_ij B_Pij D_ij)^2. The proof reuses VibeQCCore.df_staged_equals_dense. No positivity or symmetry of D is required for this real scalar identity.

12. fitted_coulomb_nonnegative: every square in claim 11 is nonnegative. This says nothing about positivity of total HF energy or a raw windowed tensor.

13. fitted_per_cell_derivative: claims 8-10 supply all three ERI symmetries to claim 25 below. Symmetric supplied factors and overlap suffice for the derivative; fitting accuracy and SCF convergence are absent.

Seam, energy ledger and derivative (14 claims)

14. cell_count_nonzero: positivity of the natural count implies its real cast is nonzero. The definition excludes empty physical supercells.

15. recover_total: cancellation gives Nc * (E/Nc) = E using claim 14.

16. normalized_energy_components: division distributes over E_el + E_NN. This reuses VibeQCCore.normalized_components and supplies a single normalization for each extensive term.

17. seam_kernel_symmetric: symmetry of S gives S_ik S_jl = S_ki S_lj, so T is symmetric on flattened pairs.

18. seam_contraction: expand (TD)_ij=sum_kl S_ik S_jl D_kl; use S_jl=S_lj to get (SDS)_ij. No hidden spin factor occurs.

19. seam_quadratic_trace: when D and S are symmetric, expand sum_ij D_ij (SDS)_ij and transpose the contracted indices to get Tr(DSDS). This is the bridge from the component dot product to the manuscript trace, and is not asserted for arbitrary complex matrices.

20. effective_kernel_symmetric: the three real ERI permutation hypotheses make V_ij,kl - V_ik,jl/2 symmetric on pairs (existing RHF result). Add the symmetric seam kernel from claim 17.

21. seam_energy_split: distribute the quadratic form to obtain E_total = E_el,bare + xi/4 <D,TD> + E_NN. With claim 19, the seam is xi Tr(DSDS)/4 for the supercell, and requires division by Nc.

22. corrected_fock: linearity of matrix-vector multiplication gives F_corrected = F_bare + xi TD/2. The energy coefficient 1/4 therefore corresponds to a Fock coefficient 1/2.

23. code_sign_translation: the production parameter is eta=-xi, so K + eta SDS = K - xi SDS. Applying the restricted-spin factor -1/2 to that corrected exchange gives the same Fock correction as claim 22. No sign restriction on either scalar is assumed.

24. total_half_fock: substitute F=h+AD to get E_total = <D,h+F>/2 + E_NN, using the existing RHF theorem. The nuclear term is included once, outside the half-Fock expression.

25. per_cell_directional_derivative: hold h,S,V,xi,E_NN,Nc fixed. Expanding E(D+tX) gives linear coefficient <X,h> + (<X,AD>+<D,AX>)/2. Claim 20 identifies the two mixed terms, giving d E_cell(D+tX)/dt at 0 = <X,F(D)>/Nc. Lean proves HasDerivAt, not a finite-difference approximation. This is an unconstrained density derivative. It is neither a theorem of minimization on the idempotent manifold nor a nuclear-force theorem.

26. idempotent_seam_trace: from the hypothesis DSD=2D, multiply by S and take the trace to obtain Tr(DSDS)=2 Tr(DS).

27. idempotent_seam_per_cell: add the electron-count hypothesis Tr(DS)=Nc Ne, substitute claim 26 and cancel the positive count: xi Tr(DSDS)/(4 Nc) = xi Ne/2. Fractional occupations and arbitrary SCF trial densities need not obey this simplification.

The existing RHF density lemmas derive metric idempotency and electron count from real occupied orbitals with Co^T S Co=I and D=2 Co Co^T. They can supply the last two hypotheses when that representation is given. The present theorem does not assert that a numerical solver enforces them exactly.

Production correspondence and discriminating checks

formal/aiccm_reference.py evaluates independent explicit finite sums using math.fsum, a direct complex Fourier sum and a direct real/reciprocal Ewald cube. It is handwritten reference Python, not extracted verified code. formal/check_aiccm.py compares them with:

Production entry point	Property checked
periodic.ccm.ri.ccm_ri_j_neutral, ccm_ri_k_neutral	Fitted J/K index contractions
periodic.ccm.ri.psd_density_factor	Rejection of an indefinite density
periodic.ccm.direct._k_neutral_fast	Factored exchange, seam sign and density factors
periodic.ccm.direct._rhf_energy_of	Single nuclear term, spin factors, energy/density derivative
periodic.ccm.direct.run_ccm_rhf_direct	Complete two-cell native RHF and returned energy ledger
periodic.ccm.direct.ccm_exchange_q0_madelung	Supercell rather than primitive-cell seam
periodic.ccm.bloch_reference.fold_block_circulant	Non-TRIM complex fold, mesh ordering and normalized trace
madelung.madelung_constant_for_cell	Negative of the signed self-potential

Random fixtures use seed 20261101, unequal entries, noncommuting positive definite D,S, symmetric factors, and separately a nonsymmetric, strided J fixture. Thirteen deliberately wrong evaluations must be distinguished: density transpose, seam sign, missing spin half, exchange as Coulomb, missing or repeated cell normalization, repeated nuclear energy, lost conjugation, reversed Fourier phase, missing Fourier average, dropped zero class, primitive-cell seam and reversed native seam offset. Three invalid cell counts are rejected by the reference, not claimed to test production input admission. The fourth rejection is production’s indefinite-density case.

The completed native run used qualified vibe-qc 0.18.6, source 7c98b77bf5a5f145129cb97a8820120d01e3ed74, native SHA-256 a1221a70e321b8cb4a212e3dcc7ff31c15f0a30cfc66224de0e2a873320bb2f0. Inputs: 6-bohr cubic primitive cell, H at (3,3,2.3) and (3,3,3.7) bohr, replication (2,1,1), STO-3G, neutral singlet, HCORE guess, 60-Hartree fitting cutoff, energy/commutator tolerances 1e-12/1e-9, 150 maximum iterations, stability checking/following disabled. Seam-on/off calculations shared the same (32,4,4) fitting array and each took two iterations.

Observation	Measured value or maximum absolute residual	Tolerance
Seam-on total energy	-2.3890610129143406 Hartree	observation
Seam-on per-cell energy	-1.1945305064571703 Hartree	observation
Seam-off total energy	-1.7871137427635495 Hartree	observation
Code Madelung eta=-xi	0.30097363507539565 a.u.	observation
Independent native Fock reconstruction	3.34e-16 Hartree	2e-8
Independent per-cell energy	2.23e-16 Hartree	2e-9
Metric idempotency	4.45e-16	2e-8
Seam-on/off energy offset	2.23e-16 Hartree	2e-8
On/off density difference	4.45e-16	2e-7
Signed Ewald bridge	1.05e-14 a.u.	2e-10
Synthetic density finite difference	1.37e-9 Hartree	2e-8
Synthetic complex fold	3.80e-16	2e-12

Residuals in this table are rounded upward. The Ewald oracle uses a cube of integer indices [-10,10]^3 at splitting parameters 0.35 and 0.5; their agreement is a numerical check, not a certified tail bound. The synthetic quadratic derivative uses central steps 1e-3 and 1e-4. All 22 residual checks, 13 error controls and four rejection cases passed. Nine of ten recorded function-source hashes matched inspected main 6bc846a3. Main’s driver additionally exposes default-zero Fock mixing and level shift; those new options were not tested by the release-runtime run. The article’s theory/formalization/check-results.json preserves the portable identities, inputs, tolerances and residuals. Raw runtime paths, qualification and scheduler records are private operational evidence.

No matched ORCA/CRYSTAL calculation was established for this finite-torus 60-Hartree fitted Hamiltonian. The independent indexed/Ewald checks address correspondence, not method accuracy. Earlier molecular ORCA evidence and periodic comparisons at different cutoffs retain their original scope.

Reproduction and trust boundary

Keep the pinned Lean 4.35.0 and mathlib v4.35.0 lock files unchanged. Use the existing dependency cache; if absent, lake exe cache get in formal/rhf populates it. From the source root with lake on the path:

python formal/check_proofs.py

The same audit builds both libraries, checks manifest/namespace coverage and inspects every theorem’s transitive axioms. Only propext, Classical.choice and Quot.sound are allowed. There are no admitted claims, custom scientific axioms or compiler-trust proof shortcuts.

Supply check_aiccm.py, aiccm_reference.py, core_reference.py and check_rhf.py as calculation-job inputs. Using the identified qualified runtime interpreter, submit python check_aiccm.py through vq. It writes aiccm-checks.json in the job directory and requires NumPy and the actual native module. Run without assertion-disabling optimization. Keep raw output outside the public checkout because it includes paths. Do not substitute whichever Python happens to be first on the path for the qualified runtime or infer binary identity from a source commit alone.

The finite class group does not specify nearest images. Existing core results establish inverse-multiplicity normalization for a supplied nonempty finite boundary set, and nearest-image rounding only for orthogonal cells. Exact ties, tolerance-selected ties, completeness and general triclinic closest-vector selection are distinct obligations. This tranche does not discharge them by assuming fractional rounding. The separately audited stage-2 extension, landed during this work, supplies exact-rational triclinic certificates and records a production tie-completeness gap. Applying those certificates to actual AICCM selected domains and tolerance policies remains a separate bridge. Its 13 universal claims are not included in the 85-claim audit reported here. There is no nuclear self-energy proof: the supplied E_NN must already exclude point self-interactions and include the intended periodic self images/background. No embedding or correction term may be silently counted twice.

Fixed topology in the derivative includes the lattice/class set, retained basis/auxiliary space, screening and metric thresholds. Geometry derivatives would add integral, overlap, seam, nuclear and possibly selection derivatives. Real-number algebra supplies no floating-point equivalence guarantee and does not verify parsing, native integral kernels, compilers, conditioning, SCF solution selection or physical adequacy.

Literature, findings and next tranche

Relevant primary sources read for this tranche were Peintinger et al., doi:10.1002/jcc.23550, Eqs. 4-24 (the historical windowed model); Sun et al., doi:10.1063/1.4998644, Sec. II A-C (neutral-mode Gaussian/mixed fitting); Weigend, doi:10.1039/B204199P, Eqs. 1-4 (RI-HF); and Helgaker, Jorgensen and Olsen, Molecular Electronic-Structure Theory, Secs. 10.7.1, 10.7.3 and 10.7.8 (density functional, metric idempotency and variation). No separate SI was catalogued for the first three in the consulted library. Sun’s Eq. 24 defines fitting; it is not evidence for this exact signed seam operator. The sign bridge above is derived explicitly from the manuscript and implementation definitions.

Prior formalization includes Bobbin et al., doi:10.1039/D3DD00077J, including its supporting derivations, and Ugwuanyi et al., doi:10.1080/00268976.2025.2539421, Secs. 4.2-4.5, 5.3 and 7 in the available preprint. These provide precedent and explicit limits on physical and executable correctness. No priority claim is made for quantum-chemistry formalization.

The manuscript seam equation needed an explicit mesh average or supercell division by Nc; the sign translation to production also needed to be stated. Those clarifications do not change computed energies. Other inventory findings need author review: unequal main/SI pair-density normalizations; real-only squared MP2 numerators beside a complex formula; an SI positive-definiteness statement that incorrectly includes the Fock matrix; a shape-independent negative-xi assertion; and overbroad charged-cell, finite-radius and broken-symmetry statements. They are not silently promoted to proved claims or corrected by changing numerical data.

The next coherent tranche is explicit finite BvK character orthogonality, the complex four-index Fourier transform and momentum delta, followed by translation-invariant density/energy equivalence with matched retained integral spaces. Separate later work should certify image domains and self-energy subtraction, then geometry derivatives and local-correlation normalizations. A proof of the full manuscript theorem must additionally discharge the analytic periodization and convergence hypotheses.