Completely monotone and Bernstein functions in Lean 4: a kernel-checked library with a general subordination theorem, applied to planar universal optimality

A small Lean 4 library of completely monotone (CM) and Bernstein functions on (0,∞), built to re-derive and extend the admissibility results needed for planar universal optimality (bilayer dipolar exciton, Yukawa, Rytova–Keldysh). Every claim is filed in an Elenchus claim ledger with tiers A (kernel-checked Lean), L (cited literature, quoted verbatim), C (human argument, not machine-checked) and X (floating-point exploration or tool measurement, which never supports a claim). Tier A (Lean 4.34.1, pinned openai/math and Mathlib; axioms within propext, Classical.choice, Quot.sound; planted sorry and planted-axiom controls caught): 130 theorems in 10 modules, each with a recorded #print axioms line. The CM definition is proved equivalent to upstream's AdmissiblePotential. Closure under positive combinations, products, translations and differences of translates; a locally uniform limit theorem with derived smoothness of the limit; a Laplace-mixture theorem under a weaker integrability hypothesis than the earlier lemma; and the general subordination theorem (f CM, ψ Bernstein with ψ > 0 implies fˆψ CM) by strong induction without the Faà di Bruno formula. Negative controls show that each of the listed hypotheses is needed. New consequences: soft-core Yukawa, stretched exponential, a Yukawa-screened bilayer exciton, continuous Yukawa mixtures, and the interaction of two aligned +1,−2,+1 quadrupoles; the field of ONE such quadrupole on a test charge (its potential energy) is proved NOT completely monotone for every layer spacing. An additive Mathlib-only core (8 Mathlib imports) re-proves the main ingredients. Honest accounting. The library does not shorten the earlier proofs end to end: for H1, H2 and H3 together the measured dependency closure grows from 406 to 505 source lines; only the marginal cost of a new potential is small. Mathlib already contains the sign-free mirror notion (AbsolutelyMonotoneOn), so this is not a Mathlib-ready contribution; no pull request was opened. Not done: the hard direction of Bernstein–Widder, pointwise limits without smoothness, mixtures of arbitrary CM families, Stieltjes mixtures and the Fourier criterion. No rusty-SUNDIALS or LeanFlow change was made in this lane. All triangular-lattice optimality corollaries are conditional on the upstream openai/math theorem, which is AI-generated and not peer reviewed, and on the fidelity of its definitions. Tier C: the step-by-step human demonstration and the quadrupole pair counting. Tier X: a 60-digit numerical screen with positive and negative controls, the proof-length measurement with its reading, and the figures. Against the preregistration: core closure and composition with Bernstein functions done; Fourier criterion not attempted; Stieltjes mixtures not done; the Mathlib-PR-ready branch goal was not met. No novelty is claimed and no literature search for novelty was made. The Elenchus ledger gate reports 0 blocking findings and 20 flags (exit code 1), one for each Tier A row whose statement adequacy no human has audited. The work was produced by AI agents (Claude) under the author's direction; the author is responsible for the content. An independent AI audit by a separate agent (verdict ACCEPT_WITH_CORRECTIONS; corrections applied in this version) rebuilt all 11 Lean files and the 5 repository prerequisites from source with the producer's olean directory off LEAN_PATH, enumerated axioms with Lean.collectAxioms over all 167 library constants (0 outside the allowlist), and caught its own planted sorry, axiom and transitive-sorry controls while a clean control passed; it did not rebuild the upstream openai/math or Mathlib oleans. There has been NO human audit of the statements or proofs, and the 20 unaudited-Tier-A flags remain open.