PhysLean / Physlib formula bridge

Coverage

Inventory

Loading…

Referenced quantities include inputs and related concepts. Compiled subjects are the formula outputs or explicit quantity interpretations covered by a compiled bridge, under its stated conditions. A compiled bridge using lattice thermal conductivity does not prove the formula that computes lattice thermal conductivity.

The upstream counts cover declarations cited here, not all of Physlib. No whole-library percentage is implied.

Dimension checks do not establish formula equivalence. This package uses upstream Dimension ISQDimensionBase with all seven named bases. Opaque fields are listed but not encoded.

The field-by-field dimension inventory lists encoded and opaque fields separately.

OMAI quantities and formulas

Physlib declarations → OMAI

Start from an upstream declaration or module to find the OMAI quantities and operators that cite it. Links work in both directions; they do not assert an inverse formula or a reversible computation.

Harmonic ensemble proofs

The bridge constructs the full nonnegative-integer quantum harmonic ensemble from Physlib's oscillator spectrum. It evaluates the partition sum and energy moment, proves the required finiteness and integrability, and identifies Physlib's free energy, mean energy, entropy and heat capacity with OMAI's single-mode formulas.

The proofs require positive temperature and angular frequency, use the exact upstream constants, and retain zero-point energy. They also establish dF/dT = -S and dU/dT = C at fixed spectrum. The heat-capacity result transfers the proved energy equality on the positive-temperature domain; it does not assume interchange of an infinite sum and a derivative.

Four further proofs identify OMAI's molar contractions with N_A/N_q times the sum of these single-mode Physlib quantities over a finite grid with 3*N_atoms branches. The basis is a mole of primitive cells. A separate proof constructs the heterogeneous joint ensemble, establishes its product partition and actual F/U/S/C, and connects those quantities to all four molar formulas. Molar normalization is applied after evaluating thermodynamics, not inside the Hamiltonian. Every frequency must be strictly positive; zero acoustic modes require a separate treatment.

Volumetric heat capacity is proved as the mode-capacity sum divided by N_q*V_cell, and separately as the joint ensemble capacity with the same normalization. Volume must be positive and refer to the primitive cell. The SI result is J/(m³ K); an ų input requires the exact factor 10^-30. The molar relation is C_vol = C_mol/(N_A*V_cell). The two proofs cover one operator, not two.

Single-mode proofs, molar contraction proofs, joint-ensemble proofs, single-mode volumetric proof, joint volumetric proof, build record and axiom audit.

Reviewed formula contracts: single-mode, molar contractions, joint ensemble, single-mode volumetric, joint volumetric. Formula contracts pin the reviewed endpoints and Lean source; they do not automatically translate formulas into proofs.

Constant-pressure heat capacity

The local static-plus-harmonic bridge proves Cp - Cv = T*V_m*alpha_V^2*K_T on a common primitive-cell molar basis. Cp is defined independently as the temperature derivative of actual ensemble enthalpy along a constant-pressure path. Expansion is V_m'/V_m, and the isothermal bulk modulus is V_m*F_VV for the same molar free energy.

The model attaches the signed static energy N_q*E_0(v) through an actual singleton ensemble, then applies N_A/N_q to the evaluated thermodynamic quantities. Frequencies are positive C2 functions of volume; static energy is C2 and temperature-independent. The reduced-q grid and molar basis stay fixed. The branch must satisfy equilibrium throughout a neighborhood, with positive temperature, volume and curvature at the evaluation point.

A heterogeneous example uses the implicit function theorem to construct a stable branch with nonzero expansion and actual Cp greater than Cv at its reference state. A separate constant-frequency example has zero expansion and Cp equal to Cv. These are exact model examples, not material fits. The result adds one compiled operator/output pair; it does not verify numerical QHA, EOS fits, minimizers, input producers or the sibling compute_heat_capacity_p route.

Inspect the catalog endpoint, actual volume family, two model examples, static ensemble, reviewed endpoint contract, and mapping conditions and sources.

Thermal Grüneisen parameter

The same static-plus-harmonic volume family proves Gamma = alpha_V*K_T/C_V_vol on a local stable constant-pressure branch. Gamma is defined independently as the heat-capacity-weighted mean of mode Grüneisen parameters gamma_i = -v*omega_i'/omega_i, weighted by actual canonical mode heat capacities at the branch volume. Expansion is V_m'(T)/V_m(T) along the branch, the isothermal bulk modulus is V_m*F_VV, and the volumetric heat capacity is sum(c)/(N_q*v), all for the same free energy, temperature and primitive cell.

A supporting result holds at fixed volume without a branch: (dP/dT)_V = Gamma*C_V_vol. The heat-capacity weights use angular SI frequency; mode parameters are logarithmic derivatives and do not depend on a constant frequency scale. Every mode must have positive frequency, so zero acoustic modes need separate treatment. Gamma, the mode parameters and the expansion may be negative, and no statement is made at zero temperature. An adiabatic modulus paired with C_V_vol gives Gamma*(1+alpha_V*Gamma*T), not Gamma.

Exact model examples set the heat-capacity arguments hbar*omega/(kB*T) to 1, 2 and 3 with mode parameters 1, 2 and 3. Gamma then lies strictly between 1 and the arithmetic mean 2: every weight is positive, and the higher-frequency modes, which carry the larger mode parameters, have smaller heat-capacity weights. A negative-rate branch has negative Gamma and negative expansion, and a constant-frequency control with one q point has both equal to zero. These are exact model examples, not material fits. The result adds compiled coverage only for the identity operator and its output; it does not verify FC3 or finite-difference mode-Grüneisen producers, phonopy's fitted thermal-Grüneisen quotient, numerical QHA or input producers. The opaque contract_thermal_gruneisen contraction is covered below, as a corollary of this identity under the quasiharmonic interpretation.

Inspect the catalog endpoint, mode parameters and weights, model examples, actual volume family, reviewed endpoint contract, and mapping conditions and sources.

Quasiharmonic producers

The five quasiharmonic producers are defined from the Gibbs surface of the same static-plus-harmonic ensembles. The Gibbs energy is G(T, p) = inf_V [F(T, V) + p V] over a volume window, the heat capacity is C_P = -T (d2G/dT2)_p, the expansion is alpha_V = (dV/dT)_p / V with V = (dG/dp)_T, the modulus is V (d2F/dV2)_T at that volume, and the thermal Grüneisen contraction is the heat-capacity-weighted mean of the mode parameters.

The C1 implicit-function theorem gives a two-parameter equilibrium family V(T, p) through every stable stationary point. On any volume window across which F + p V is convex, that family is the unique minimizer, so a scan that verifies the convexity of F + p V across its window selects a unique minimizer; the selected volume must lie strictly inside the scanned range, and extrapolation of a fitted equation of state is not covered. The envelope relations give (dG/dT)_p as -(N_A/N_q) times the Physlib ensemble entropy and (dG/dp)_T = V.

C_P equals the enthalpy derivative of the Cp identity above and also C_V + T (dV/dT)_p (dS/dV)_T, the form of phonopy's default polyfit estimator, through the Maxwell relation (dS/dV)_T = -F_TV = alpha_V K_T; C_P > C_V exactly when alpha_V is nonzero. The expansion read off G is -F_TV/(V F_VV), and the modulus at the selected volume equals -V/(dV/dp)_T; its positivity is the stability premise, not a result. It is the modulus along the model's hydrostatic volume coordinate, not the Voigt average that the BulkModulus node defines. The Grüneisen contraction equals alpha_V K_T / C_V_vol with both read off G. Exact witnesses realize positive, negative and zero expansion.

The theorems hold for any T > 0 with F_VV > 0, including temperatures where the quasiharmonic approximation is physically unreliable. Numerical volume scans, equation-of-state fits, minimizers, FC3 and finite-difference Grüneisen producers and phonopy are not verified; producers must reject imaginary modes at every scanned volume and use one cell for the static energy and the phonons. Inspect OMAIPhyslibGibbsBranch.lean, OMAIPhyslibQHA.lean and OMAIPhyslibQHAWitness.lean, and the conditions for compute_qha_gibbs, compute_heat_capacity_p, compute_thermal_expansion, compute_bulk_modulus_qha and contract_thermal_gruneisen.

Linear elasticity (local proofs)

Physlib has no elastic-solid model, so these are local theorems over Mathlib about the catalog's Voigt contractions K = sum C_aabb / 9 and G = -sum C_aabb / 30 + sum C_abab / 10, its Young's modulus and Poisson ratio, and its equation-of-state modulus V0 E''(V0). The stress C : e is tensile-positive, the negative of the catalog's compressive-positive Stress node.

Any stiffness tensor with the first minor symmetry that stores positive energy for every nonzero symmetric strain has positive Voigt moduli, through an orthogonal basis of deviatoric strains, so the catalog's Poisson ratio lies in (-1, 1/2) for every crystal symmetry. For an anisotropic crystal, E and nu computed from the Voigt moduli are Voigt-polycrystal estimates. An isotropic tensor gives the Lame values K = lam + 2 mu / 3 and G = mu, is stable exactly when both are positive, and gives the Lame expressions for E and nu.

For a cubic crystal the contractions give (C11 + 2 C12)/3 and (C11 - C12 + 3 C44)/5. The trace of the stress depends on the strain only through its trace, tr sigma = 3 K tr e, so the Voigt bulk modulus is the stress-controlled one; the Voigt shear modulus is exact only at Zener ratio 1. With C12 <= C11 and C44 >= 0, the energy minimized over cell shape at fixed volume has curvature V0 E''(V0) = K, which relates the equation-of-state modulus to the tensor contraction. Uniform scaling without shape relaxation gives the Voigt K for every tensor. Inspect OMAIElasticity.lean and the conditions for contract_bulk_modulus.

Composites and cure kinetics (local proofs)

Physlib has no effective-medium or polymer-cure model, so these results are local theorems over Mathlib about the catalog's own formulas. They cite no Physlib declaration and are counted apart from the proofs that cite Physlib declarations.

Both closed-form branches of the spheroid depolarization factor and its sphere value equal L33(p) = int_0^1 t^2/(t^2 + p^2 (1 - t^2)) dt. So L33 lies in (0, 1), decreases strictly with the aspect ratio p = d3/d1, is continuous through the sphere p = 1 where it equals 1/3, and tends to 0 for needles and to 1 for disks.

For every spheroid shape the random Nan conductivity exceeds the matrix value by k_m f (2 b11 + b33)/(3 - f (2 L11 b11 + L33 b33)) with a positive denominator, so filler whose interface-corrected conductivities both exceed the matrix raises it. For spheres both Nan formulas reduce to Maxwell-Garnett with the corrected filler conductivity k/(1 + 2k/(G d)), which tends to k as the interface conductance grows. Along the alignment axis the aligned conductivity lies strictly between the series and parallel mixtures and, at fixed d3, rises strictly with the aspect ratio.

The catalog's d is a full particle dimension, a sphere's diameter, while Hasselman-Johnson's a_rad is its radius. The Hasselman-Johnson formula is Maxwell-Garnett at d = 2 a_rad, so putting the radius into d doubles the interface penalty. It exceeds the matrix conductivity exactly above the critical radius (k_m/G) k/(k - k_m). Away from spheres the per-direction interface correction is a slab approximation of unvalidated accuracy.

The Kamal-Sourour cure time increases strictly with conversion below full cure and its derivative is the reciprocal rate. Near every interior time there is an inverse alpha(t) that solves d alpha/dt = (k1 + k2 alpha^m)(1 - alpha)^n throughout a neighbourhood; no global solution is claimed. The DiBenedetto relation, in kelvin, maps conversions [0, 1] one to one onto [T_g0, T_ginf] and lies strictly below the linear interpolation inside the interval for lambda < 1.

Inspect OMAICompositeConductivity.lean and OMAICureKinetics.lean in lean/bridge, and the conditions for depolarization_factors, nan_effective_kappa, nan_effective_kappa_aligned, hasselman_johnson, kamal_cure_conversion and dibenedetto_glass_transition.

Lattice dynamics

Physlib's crystal structure supplies the sites and the translation action; the lattice-dynamics content is OMAI-local. Second-order force constants on crystal sites with equal mixed partials, translation invariance and finite range satisfy the index-permutation symmetry Phi_ij(-R) = Phi_ji(R), and the catalog dynamical matrix D_ij(q) = sum_R e^{i q.R} Phi_ij(R)/sqrt(M_i M_j) is Hermitian at every wavevector. With the acoustic sum rule the Gamma-point matrix has at least three independent zero modes, the mass-weighted rigid translations. The catalog uses the cell-vector phase; phonopy's atom-position phase leaves omega^2 and nondegenerate velocities unchanged but changes the eigenvectors by e^{-i q.tau}, so phonopy eigenvectors must not be fed into the catalog's dD/dq.

Real frequencies need mechanical stability. Folding the force constants into a finite Born-von Karman supercell, Phi_BvK(R) = sum_L Phi(R + L), reproduces the catalog D(q) exactly at every wavevector commensurate with the supercell, and a Bloch-wave argument shows that a stable supercell makes D(q) positive semidefinite there, so omega^2 >= 0. Incommensurate wavevectors are the normal case for BTE (a 4x4x4 force-constant supercell with a 19x19x19 mesh), and Fourier interpolation is exact only at commensurate points; nothing is stated at the others.

On a differentiable eigenvector path, away from Gamma, the catalog group velocity e^dagger (dD/dq) e / (2 omega) is real and equals d omega/dq by the Hellmann-Feynman theorem, with dD/dq the exact derivative of the catalog matrix. Symmetry-enforced degeneracies, such as transverse pairs along Gamma-X and Gamma-L, are generic, and the eigenvector a code returns there is not on such a path. A compiled monatomic chain gives omega^2 = (2K/M)(1 - cos(q a)) and velocity a sqrt(K/M) cos(q a / 2).

With the actual Physlib canonical mode heat capacities at T > 0 and positive half-widths Gamma = Im Sigma (so 1/tau = 2 Gamma), the relaxation-time conductivity is symmetric and positive semidefinite, and positive definite exactly when the group velocities span space. The participation ratio of a normalized mass-weighted mode lies between 1/N and 1, with both equality cases; it is a local proof over Mathlib.

Three catalog formulas were recorded as defects here and are since corrected. The non-analytic correction multiplied the free components q^alpha and q^beta instead of contracting q_gamma, so its q dependence cancelled; it now carries the Gonze-Lee form, whose long-wavelength limit the static-dielectric binding transcribes. The collision matrix of the linearized BTE had the wrong relaxation-time limit and was not symmetric; it is now the symmetric weighting of Chaput's collision matrix, not yet bound. The cumulative conductivity takes the linearized-BTE input, for which it is a signed partial sum, and its description now says so: a compiled three-mode example with one three-phonon process, Casimir boundary scattering and Bose-Einstein weights is not monotone in either the frequency or the mean-free-path binning. Inspect the dynamical matrix, dispersion, group velocity and relaxation-time conductivity conditions and sources.

Stability and CALPHAD equilibrium

These are local proofs over Mathlib: Physlib has no model of convex hulls, slab supercells or assessed Gibbs-energy databases. Most of these catalog producers are opaque code outputs, so each gets an interpreted definition, stated in its binding's conditions. The pymatgen and pycalphad outputs themselves are not verified; the theorems hold for the interpreted definitions.

The energy above the hull, interpreted as the per-atom distance of an entry's formation energy above the lower convex hull of its competing set, is the same for every set of elemental reference energies and is unchanged by any affine function of composition applied to every entry. A supporting affine function that touches the entry certifies a zero distance. The target and its competitors must share one energy model and one correction scheme; the MP2020 corrections are not such a shift across correction classes.

The adsorption energy and the average intercalation voltage are unchanged by every per-element energy offset exactly when the cells conserve atoms. The average voltage -(E_full - E_empty - n mu)/(n q) is the mean of the open-circuit profile -(E'(x) - mu)/q over the ion content, kinks between plateaus included; for an ion of valence z the transferred charge is n z e, while the catalog's n q_e is correct only for monovalent ions. For stoichiometric slabs with energies affine in thickness, the surface and grain-boundary energies are thickness independent exactly when the bulk reference equals the slab slope, and grow without bound otherwise. The catalog's reaction energy, corrected to sum_i c_i N_i Delta H_f,i with N_i the atoms of each formula unit, is independent of the elemental references exactly when the reaction is balanced.

For a binary system the equilibrium molar Gibbs energy, the least energy of any mixture of the assessed phases at the overall composition, is the convex envelope of the phase Gibbs curves. If every phase's Gibbs function is concave in temperature, the equilibrium Gibbs energy at fixed composition is concave in temperature, so the equilibrium entropy and, at nonnegative temperature, the enthalpy are nondecreasing through every phase transition. Differentiable phase curves share the common tangent at a two-phase local extremum (and where the equilibrium envelope follows that chord, its tangent intercepts are the common-tangent intercepts), mass balance fixes the lever-rule phase fractions, and for a unary system or a congruent transformation a Gibbs-energy difference that changes sign with a positive entropy difference has exactly one transition temperature. For an alloy that temperature is T0, not the liquidus, solidus or solvus the catalog's boundary locus returns. All quantities are per mole of atoms at fixed pressure. The formation energy and G = H - T S are definitions with nothing to prove and stay unbound.

Analog devices, Arrhenius diffusion and ionic conduction (local proofs)

Physlib has no device or solid-state diffusion model, so these results are local theorems over Mathlib about the catalog's own formulas. They cite no Physlib declaration and are counted apart from the proofs that cite Physlib declarations.

Every continuous positive drift law that does not depend on the choice of reference time is the catalog's power law, by the multiplicative Cauchy equation; this holds for one device and one level with a fixed exponent, while an array mean over a spread of exponents is not a power law. Conductances that follow the two-dimensional T^(3/2) injection law, inverted with the catalog's T^2 law from two temperatures, return the barrier lowered by k_B T_eff/2, where T_eff, the reciprocal logarithmic mean of 1/T_1 and 1/T_2, lies strictly between the two temperatures. An ensemble with two symmetric sites exchanging at the catalog's retention rate relaxes to one half with time constant tau/2, and no other evolution solves its master equation.

Under a linear ramp the expected hop count from zero bias is exp((V - V*)/b), b = k_B T/alpha_F, minus g_r k_B T/(alpha_F tau_0), with tau_0 the zero-bias lifetime of the unprogrammed state over the SET barrier; it equals the catalog's RetentionTime only for symmetric sites. The first hop then follows a minimum-Gumbel law of total mass one whose mean, through Gamma'(1) = -gamma, is the catalog's set voltage V* - gamma b.

The programming error exceeds c/sqrt(2 n_w) for every kernel and window. For a conductance that changes monotonically during a pulse applied across the same two terminals, the dissipated energy lies between the catalog's pulse energies at the initial and the final conductance. For a channel of segments in series, the catalog conductance with the length-averaged conductivity is an upper bound on the true conductance.

The catalog's weighted Arrhenius fit is the weighted least-squares line of log D against 1/T, and on exact Arrhenius data it returns the activation energy for any positive weights. Fitting the Nernst-Einstein conductivity sigma instead of sigma T in the same way returns E_a - k_B T_eff with T_eff inside the data's temperature range.

The conductance window, the coefficient of variation and the Einstein diffusivity D = slope/(2d) are definitions with nothing non-obvious to prove. The Schottky-Mott barrier is unbound because its validity, the absence of Fermi-level pinning, cannot be established algebraically. Inspect OMAIDeviceMetrology.lean and OMAIMaterialsTransport.lean in lean/bridge, and the conditions for emit_thermionic_conductance, ramp_set_voltage and fit_arrhenius.

Derivatives of an atomistic or cell energy (local proofs)

Physlib has no model of an interatomic potential or a molecular energy surface, so these are local theorems over Mathlib about the catalog's forces, stress, force constants and elastic constants, read as derivatives of one energy, and the molecular frequencies, read as eigenvalues of its mass-weighted Hessian. No theorem verifies a DFT, MLIP, phonopy or finite-strain implementation.

For an energy differentiable at the configuration and invariant under rigid translations of all atoms, the catalog forces F = -dE/dR sum to zero in every direction, and the force constants obey the acoustic sum rules over the sites of one index once the first (second order) or second (third order) derivatives of the potential are differentiable at the reference, as they are for a twice or three times continuously differentiable potential. A real-space grid that breaks translation invariance (the egg-box effect) leaves a nonzero force sum. For an energy invariant under rotations in a plane, as for an isolated molecule but not for atoms rotated inside a fixed periodic lattice, the torque in that plane vanishes. A potential three times continuously differentiable has third-order force constants symmetric under every permutation. A compiled two-atom energy satisfies these hypotheses with a nonzero force and force constant.

The central-difference estimate (F_j(u - h e_i) - F_j(u + h e_i))/(2h) of the finite-displacement force constant is within M h^2 / 6 of the derivative, where M bounds the third derivative of the force along the displacement, the fourth derivative of the potential. When a site symmetry maps the plus displacement onto the minus one, phonopy reconstructs the minus forces by symmetry and the estimate stays the central difference; a truly one-sided difference has an error of order h. Neither case is covered.

For a cell energy of the deformation gradient, differentiable at F and invariant under rotations of the deformed cell, the compressive-positive catalog stress satisfies sum_b sigma_ab F_cb = sum_b sigma_cb F_ab and is symmetric at the reference cell. At a stress-free reference, for an energy twice continuously differentiable there and invariant under rotations of the cells near it, the catalog elastic constants have the major symmetry and both minor symmetries; at a pre-stressed reference the minor symmetries fail by residual-stress terms, and the stress-strain coefficients a code fits there lose the major symmetry as well. A stable stress-free reference then has positive Voigt bulk and shear moduli and a Poisson ratio in (-1, 1/2). The St Venant-Kirchhoff energy of the Green-Lagrange strain is a compiled witness: its catalog elastic constants at the reference are the isotropic tensor (V0/V)(lam delta_ab delta_cd + mu (delta_ac delta_bd + delta_ad delta_bc)), positive definite for lam >= 0, mu > 0 and V = V0 > 0.

Read as the signed square roots of the eigenvalues of the mass-weighted Hessian, the catalog's molecular frequencies have no imaginary mode at a local minimum with positive masses, the catalog's n_imaginary = 0 diagnostic; the converse does not hold. The mass-weighted rigid translations of a translation-invariant potential twice continuously differentiable at the structure are zero modes; rotational zero modes are not covered.

The catalog's mode Grüneisen formula, which contracted the third-order force constants over two Cartesian indices with no eigenvectors, masses, Bloch phases or positions, now carries the Maradudin-Fein contraction; no theorem relates it to the derivative-defined parameter. Inspect OMAIAtomisticDerivatives.lean, OMAICellElasticity.lean and OMAIMolecularModes.lean, and the conditions for compute_forces_hf, compute_stress_cell, compute_force_constants, compute_fc2_finite_displacement, compute_elastic_constants and compute_molecular_frequencies.

Boltzmann electronic transport, carrier statistics and the static dielectric tensor

The electronic transport producers are opaque code outputs, so each gets an interpreted definition stated in its binding. The conductivity, Seebeck coefficient and electronic thermal conductivity are read as BoltzTraP2's Onsager moments L_k = sum_b w_b (E_b - mu)^k of a nonnegative transport window on an energy grid: sigma = e^2 L_0, S = -(L_1/L_0)/(e T) and kappa_e = (L_2 - L_1^2/L_0)/T, one diagonal component at a time, with the scattering model inside the weights. At T > 0 the electronic thermal conductivity is nonnegative and vanishes exactly when the whole window sits at one energy. With L_0 > 0 and any lattice conductivity kappa_l > 0 the coefficients fill a Physlib ThermoelectricMaterial, and, when the window spans more than one energy and L_1 != 0, its figure of merit lies strictly below the Mahan-Sofo bound L_1^2/(L_0 L_2 - L_1^2), the squared mean over the variance of the transport energy, which is approached as the lattice conductivity vanishes. For an energy-independent transport distribution the Fermi-window moments 1, 0 and pi^2/3 give S = 0 and the Sommerfeld Lorenz number, kappa_e = (pi^2/3)(k_B/e)^2 sigma T.

Two local results over Mathlib cover the carrier mobility and the electronic density of states. With scattering rates that add in every state, the mobility is at most the Matthiessen combination of the per-mechanism mobilities amset reports. The density of states of a finite level set with positive degeneracies, integrated against the Fermi function at k_B T > 0, is continuous and strictly increasing in the chemical potential, so every electron count strictly between zero and the number of states fixes exactly one Fermi level; at T = 0 a gap leaves it undetermined.

The static dielectric tensor is read as eps_0 = eps_inf + c Z^T D^-1 Z with D the Gamma-point dynamical matrix on the optical coordinates and Z the mass-weighted Born charges, the mode-oscillator-strength sum in the eigenbasis of D. The ionic term is positive semidefinite and vanishes along a direction exactly when no polar mode couples to it, and the Gonze-Lee long-wavelength correction along u multiplies the product of the squared frequencies by (u eps_0 u)/(u eps_inf u): the generalized Lyddane-Sachs-Teller relation. The catalog's own non-analytic correction, corrected to the Gonze-Lee form, is this term in its long-wavelength limit. Inspect OMAIPhyslibElectronicTransport.lean, OMAISommerfeldTransport.lean, OMAIElectronicStatistics.lean and OMAIStaticDielectric.lean in lean/bridge, and the conditions for compute_seebeck, compute_carrier_mobility and compute_static_dielectric. Physlib supplies the coefficient axioms and the figure of merit; the moment identities are proved locally. No theorem verifies a BoltzTraP2, amset, phonopy, kALDo, GPUMD or LAMMPS implementation; band structures, scattering rates, transmissions and trajectories are inputs.

Molecular-dynamics correlations, the VACF spectrum and the phonon spectrum

Physlib has no model of a molecular-dynamics trajectory, so the correlation estimators are local theorems over Mathlib about the catalog's transcribed formulas. For records periodic over the origin window (the circular correlation of an unpadded FFT) with positions advanced by dt times the stored velocity, the catalog's mean squared displacement is dt^2 [tau Cv(0) + 2 sum_{k<tau} (tau - k) Cv(k)] in terms of the catalog's velocity autocorrelation, so the Einstein and Green-Kubo diffusion estimators are one function of the trajectory. The symmetrized Green-Kubo conductivity at tau_max = m dt, with the trapezoid rule on the sampled autocorrelation, is the central-difference Einstein-Helfand estimator V (Lambda(m + 1) - Lambda(m - 1))/(4 k_B T^2 dt), and the origin-averaged heat-current autocorrelation is the inverse discrete Fourier transform of the cross spectrum of one period. Nothing is claimed about ensemble averages, ergodicity or finite-trajectory bias. The catalog's heat-current formula, which multiplied each atom's total force by its own absolute position, now uses the per-atom virial and is not covered.

For the autocorrelation of lifetime-broadened modes the catalog's cosine transform g(omega) = (6/(pi Cv(0))) int cos(omega tau) Cv(tau) dtau is a sum of Lorentzians at +omega_m and -omega_m with weights 3 A_m/Cv(0), integrates to 6 over the real line and to 3 on positive frequencies for every set of linewidths when Cv(0) != 0, and converges, as the linewidths vanish, to the harmonic delta sum with mode weights 3 A_m/Cv(0). The catalog's g is therefore the density of states per atom, three states on positive frequencies.

On a finite Born-von Kármán crystal of Physlib sites, the catalog density of states taken over every character of the translations has total weight 3 N_cell and, for a harmonic energy that is never negative, second moment sum_i Phi_ii(0)/M_i, by character orthogonality. The catalog's Landauer weight hbar omega dn_BE/dT is the derivative-defined canonical heat capacity of a Physlib quantum oscillator, so the conductance is the transmission-weighted spectral integral of that heat capacity, and with unit transmission it is the thermal conductance quantum pi^2 k_B^2 T/(3h). Inspect OMAIMDCorrelations.lean, OMAIVACFSpectrum.lean and OMAIPhyslibPhononSpectrum.lean in lean/bridge, and the conditions for compute_msd, fourier_to_dos and compute_dos. No theorem verifies a BoltzTraP2, amset, phonopy, kALDo, GPUMD or LAMMPS implementation; band structures, scattering rates, transmissions and trajectories are inputs.

Phonon scattering channels and the relaxation-time mean free path (local proofs)

Physlib has no phonon-scattering model, so these are local theorems over Mathlib about the catalog's transcribed formulas. Every linewidth is the canonical Gamma = Im Sigma = 1/(2 tau) on a Gamma-centred mesh of N_q points. The Tamura isotope linewidth (pi/4N_q) omega^2 sum delta(omega - omega') sum_b g_b |e_b* . e_b'|^2 is nonnegative, and for normalized eigenvectors it is at most (pi/4) omega^2 g_max D(omega), with D the density of states smeared with the isotope kernel. The three-phonon linewidth (pi/2N_q hbar^2) sum |V_3|^2 [(1 + n' + n'') delta(omega - omega' - omega'') + 2 (n' - n'') delta(omega + omega' - omega'')] is nonnegative for a |V_3|^2 symmetric under exchange of the two partner phonons and an even smearing kernel that does not increase with the offset, which covers the catalog's Gaussian. For an arbitrary kernel it is nonnegative when the kernel vanishes at signed offsets above omega_q nu, and a compiled example with an even but non-monotone kernel gives a negative linewidth.

With the Casimir boundary linewidth |v|/(2L) in Matthiessen's sum and nonnegative anharmonic and isotope channels, the relaxation-time mean free displacement F = v/(2 Gamma) never exceeds the boundary length L, with equality exactly when the other channels vanish. The bound holds because the boundary linewidth and the relaxation time carry the same factor 2 of Gamma = 1/(2 tau). No theorem verifies a kALDo, ShengBTE or phono3py implementation. |V_3|^2, frequencies, eigenvectors and mass variances are inputs. Inspect OMAIPhononScattering.lean and the conditions for compute_isotope_scattering, compute_linewidth[channel=anharmonic_3ph], compute_boundary_scattering, sum_linewidths and solve_bte[bte_solver=rta].

The linearized Boltzmann equation and its conductivity (local proofs)

The catalog solves the direct linearized BTE M F = c v with the weighting M = C^(1/2) Omega~ C^(1/2) of Chaput's collision matrix, whose Kronecker term is the scattering rate 2 Gamma and whose kernel carries pi/(N_q hbar^2), |V_3|^2 in the labeling q + q' + q'' = 0, the weight 2 sqrt(n''(n'' + 1)) and three energy channels. For an even smearing kernel and a |V_3|^2 symmetric under exchange of its first two modes on momentum-conserving triples, the collision matrix and its weighting are symmetric. Without the in-scattering kernel the system is solved exactly by the relaxation-time F = v/(2 Gamma), the limit the catalog's former collision matrix violated.

For a symmetric collision matrix the conductivity kappa = sum c v F / (V N_q) of any solution is a symmetric tensor, and if Chaput's matrix is positive semidefinite and every heat capacity is nonnegative, the conductivity is positive semidefinite. For an even smearing kernel the quadratic form of the collision matrix is sum 2 (Gamma - Gamma^db) x^2 plus a sum of squares over momentum-conserving triples, where the detailed-balance linewidth Gamma^db weights each process by s' s''/s with s = sqrt(n(n + 1)), so the matrix is positive semidefinite whenever Gamma >= Gamma^db. With exact energy conservation the catalog's three-phonon linewidth equals Gamma^db. With the nonnegative isotope and boundary linewidths the collision matrix and the conductivity of the catalog chain are then positive semidefinite with no positivity hypothesis. The exact identity, not positivity alone, certifies the kernel constant and the weight relative to Gamma. With Gaussian smearing the matrix can have a negative eigenvalue (issue 221 gives an example), which phono3py's pinv_method=1 drops from the pseudo-inverse. Inspect OMAILinearizedBTE.lean and the conditions for solve_bte[bte_solver=direct_inverse] and contract_kappa[bte_solver=direct_inverse].

Evidence and scope

• Exact definition: the displayed definitions correspond under the specified interpretation. This label alone is not a Lean proof.
• Conditional: a model, units, index or normalization bridge is required. Inspect the remaining obligations.
• Conceptual: a related model or concept, not a formula-equivalence claim.
• Local: a compiled theorem about the OMAI formula itself, over Mathlib, where Physlib has no model for it. It cites no Physlib declaration. Rows it covers show the status Local proof, not Referenced, and the coverage ledger counts them apart from Physlib-anchored results.
• Gap: no correspondence was established in the reviewed source. Other or later developments may supply one.

Scalar thermoelectric results require a common operating point and explicit isotropic interpretation where OMAI carries tensor quantities. Harmonic results require stable positive frequencies, positive temperature, Bose occupation, and the stated per-mode or cell/molar normalization. Zero-point energy contributes to free energy and internal energy. Stored linear THz is not angular frequency: omega_SI = 2*pi*10^12*nu_THz.

Temperature results concern an absolute-temperature representation. The pressure result identifies the signed trace under an inviscid constitutive law; it does not prove a DFT stress formula. Reverse navigation identifies references, not mathematical inverse functions. None of these results certifies finite-precision arithmetic, convergence, physical-model adequacy, or a numerical adapter.

Reproduce and inspect

The machine-readable inventory is generated from the reviewed mapping records shipped with OMAI and its existing scientific identities. Reviewed Lean source and build instructions are in lean/bridge.

python -m omai.formula_bindings --check
python -m omai.formula_bindings --check --physlib-path /path/to/pinned/physlib
bash lean/bridge/check.sh
python -m omai.formula_bindings --check --lean-package lean/bridge

The read-only source check verifies pinned files and declaration lines. The compiled source-reference audit checks upstream names and their defining modules. The package audit also checks the endpoint definitions named in the reviewed formula contracts, including definitions retained in earlier modules. These reference and name checks establish provenance, not formula equivalence. The axiom audit requires every bridge source module to be imported with its private kernel data, and includes module-owned private and generated declarations as well as the bridge namespace. It rejects missing modules, incomplete output and unapproved assumptions. Run check.sh to build with the pinned dependencies and perform the endpoint-name and transitive-axiom audits.