Alphabeta Math
AlgorithmAlgorithm: AI-adaptedProof: Not applicablePipeline-generated
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Finite primitive and contracted Gaussian integral evaluation with certified screening

Definition

Inputs. A finite list of input basis contractions ϕa=∑i=1qadaigai, 1≤a≤n, from Cartesian Gaussian primitives, contractions, and integral conventions, represented by finite dyadic intervals for real centers and positive exponents and finite dyadic intervals or complex rectangles for coefficients; a finite nuclear list ((Cℓ,wℓ))ℓ=1J whose centers and signed real weights are represented by finite dyadic intervals; a requested subset I⊆{S,T,V,G} of integral outputs (overlap, kinetic, nuclear attraction, and Coulomb); and Boolean energy and gradient requests, with a gradient request requiring an energy request. Require at least one requested output. Supply a positive integral tolerance εI for every requested integral and for integrals used internally by an energy request; supply a positive energy tolerance εE when energy is requested and, for a gradient request, an optional positive gradient tolerance defaulting to εE. An optional positive screening tolerance is allowed only for an energy request. Also supply finite positive integer work and precision caps W,P and a dyadic format of precision 2≤p≤P with exponent bounds and fixed elementary truncation index K≥1. A primitive request is the singleton-contraction case. An energy/gradient request additionally requires n,r≥1, real primitive-contraction coefficients dai and real nuclear data, real matrices C∈Rn×r,D∈Rr×r given by dyadic boxes (exact matrices are singleton boxes), and uniform finite bounds B≥sup⁡∥C∥F, MD≥sup⁡∥D∥F from Finite tensor contractions and their variational energy and gradient. Internal primitive labels (a,i) are distinct from the input basis labels a; C is a subsequent transform of the input basis.

Outputs. A status success, inconclusive, domain, or range; outward real intervals or complex rectangles for the integrals in I; an energy interval when energy is requested; a gradient center and Frobenius gradient-error bound when gradient is requested; and a separately accumulated discarded-energy bound when screening is enabled. Success encloses every parameter value in the input boxes. No status declares an omitted integral zero.

Finite calls and accounting. Use Outward-rounded interval, rectangle and ball operations for arithmetic. Every real elementary call means a typed DAG call to Certified range evaluation for elementary real and complex functions at the supplied format and K. Enclose π by the Machin identity in Trigonometric identities, Machin's formula and reduced Taylor tails and the K-term arctangent series with geometric tails from Range-reduced exponential, logarithm and arctangent series have certified tails, using exact rational tail endpoints before final outward conversion. A shared counter charges each conversion, comparison, loop update, arithmetic operation, recurrence update and summand, including every primitive operation executed by a child. Check the counter before executing an operation and interrupt any child at exhaustion. A required Boys call receives remaining work R as its finite work cap, precision cap P, the same format and K, absolute tolerance εI/2 and no relative request; its actual work is charged to the parent. A required child non-success on otherwise valid data or an intermediate overflow makes the current integral evaluation inconclusive; a rounded intermediate failing a domain certification on valid original data is also inconclusive. Return range only when a certified lower bound for a requested exact output component exceeds the largest finite magnitude of the format or a certified upper bound is below its negative. A mere overflow of a conservative intermediate or enclosure endpoint is not enough to claim range. Invalid original inputs return domain; cap exhaustion returns inconclusive. These choices are conservative and need not permit success under every cap or tolerance.

  1. Validate the request specification, positive exponent lower endpoints, finite input boxes, indices in N03, supported format and positive tolerances/caps. Invalid original data return domain. If energy/gradient is requested, verify realness and dimensions and certify the norm bounds by outward Frobenius upper bounds on the complete boxes. If this sufficient norm test cannot certify the supplied bounds, return inconclusive; do not claim that an unknown represented matrix violates its bound. Form finite primitive-pair and quartet lists for the requested integrals and any energy/gradient dependencies, lexicographically. Include all shifted overlap pairs required by the kinetic raising/lowering formula; a negative index contributes zero.

  2. For each ordered primitive pair with exponents a,b, indices α,β and centers A,B, compute p=a+b, P=(aA+bB)/p, and Kab=exp⁡(−ab∥A−B∥2/p) by outward arithmetic and the real elementary call. Compute the Hermite coefficients by Finite Hermite expansion and coefficient recurrences for a Cartesian Gaussian pair, raising the first primitive in x,y,z order and then the second, storing each intermediate degree table until its successors have been formed. The final table has ∏j=13(αj+βj+1) entries; every intermediate table update is also charged. Compute overlap by the finite shifted polynomial expansion and the moments in Cartesian Gaussian moments and exponent-parameter derivatives, and kinetic by Cartesian Gaussian raising, lowering, and kinetic-energy recurrences. Certified square roots and integer powers evaluate all half-integer factors in those moment formulas.

  3. To evaluate an attraction primitive pair, put L=∣α∣+∣β∣ and use exponent η=p and center difference P−Cnuc. To evaluate a primitive Coulomb quartet, including any diagonal self quartet, put L=∣α∣+∣β∣+∣γ∣+∣δ∣, η=pq/(p+q) and center difference P−Q, where the second pair has exponent q. Form the nonnegative Boys argument interval T=η∥P−Q∥2, with the evident attraction substitution, using interval squaring and the positive exponent bounds. Request Boys orders 0,…,L from Finite-budget certified evaluation of Boys function tables. If rounding prevents certification of a required positive denominator, return inconclusive.

  4. Initialize R000j=(−2η)jFj(T) for 0≤j≤L. For total derivative degree d=1,…,L, enumerate (t,u,v) lexicographically with t+u+v=d, choose its first nonzero coordinate in x,y,z order, and apply that coordinate's recurrence in Hermite recurrence formulas for Gaussian nuclear-attraction and two-electron Coulomb integrals for 0≤j≤L−d. Negative-index terms are zero. For example, when t>0, use Rtuvj=(P1−Q1)Rt−1,u,vj+1+(t−1)Rt−2,u,vj+1. Each predecessor is at a smaller derivative degree and within its stored Boys-order range. Contract the finite Hermite sums in that theorem to get each primitive integral.

  5. Contract primitive integrals to input-basis integrals by the finite coefficient sums. For overlap, kinetic and attraction the coefficient is dai‾dbj. For the defined pair-density Coulomb convention, the primitive quartet coefficient is daidbj‾dck‾ddl: expand fab(x)‾fcd(y) in Cartesian Gaussian primitives, contractions, and integral conventions. In the real energy branch these are the four real contraction coefficients. Cache only identical ordered parameter boxes, angular indices, format and truncation context; an R cache record also stores its cutoff L. Reuse a table only if its stored cutoff is at least the needed cutoff; otherwise compute the larger table under the counter.

  6. Optional Coulomb-energy screening applies to whole input-basis quartets, before their off-diagonal primitive quartets are evaluated. First compute every required contracted diagonal Gab,ab without screening by steps 2–5, including all coefficients d. Obtain finite nonnegative upper endpoints Uab from their real projections, justified by Positive Coulomb bilinear form, Cauchy–Schwarz, and screening bound. Form the outward real interval Wab=∑p,qCapDpqCbq and its upper absolute bound Aab=max⁡(∣inf⁡Wab∣,∣sup⁡Wab∣). Compute nonnegative outward upper bounds Qabcd≥UabUcd and wabcd≥12AabAcdQabcd. Enumerate all ordered candidate basis quartets lexicographically, with no unrecorded symmetry compression. Skip a quartet only if the outward accumulated sum after adding wabcd is at most the screening tolerance; otherwise compute its primitive sums. Store a skipped real entry as [−Qabcd,Qabcd] and report the actual accumulated weighted sum. Thus entrywise radius uses Q, while the discarded-energy bound uses w. Even a skipped integral must pass its requested integral-tolerance test. No screening is required or performed when this optional real-energy branch is absent.

  7. If energy or gradient is requested, form the one-body matrix on the input basis by Hab=Tab+∑ℓ=1JwℓVCℓ(ϕa,ϕb), using the supplied signed nuclear weights, and form the Coulomb tensor G on that basis. Use the midpoint tensors H~,G~ and largest entrywise radii ε2,ε4, including every screened interval. Evaluate the finite polynomial E(C;D,H~,G~) by outward arithmetic over the full C,D boxes, and enlarge its interval by δE=MDrnB2ε2+12MD2r2n2B4ε4 from Explicit finite-dimensional contraction error bounds for energy and gradient. If gradient is requested, evaluate every formal partial derivative of this same finite polynomial by differentiating its two and four factors of C and using outward finite sums. If their intervals have midpoints caμ and radii ρaμ, return gradient center c with outward upper Frobenius error bound ∑a,μρaμ2+δ∇, where δ∇=2nrBMDε2+2n2r2B3MD2ε4. This includes uncertainty in C,D as well as integral error; nuclear and contraction-coefficient uncertainty was already included in the integral boxes. Count all these operations. If a final certified bound proves that a requested output range lies wholly outside the finite format, return range; a final endpoint overflow without this proof returns inconclusive. Return success only when every requested integral radius, energy radius and gradient-error bound meets its own declared tolerance; all remaining failures return inconclusive.

An R table with cutoff L stores ∑d=0L(L−d+1)(d+22) entries. All input, pair, primitive-quartet and auxiliary tables are finite. Every update and child evaluation is also subject to the shared finite work counter, so valid inputs may return inconclusive when their tolerance or work requirement cannot be certified.

Depends on

Used by

Dependency tree · two levels

55 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources