The bilayer dipolar-exciton interaction is completely monotone in r^2: kernel-checked triangular-lattice corollaries at every density and an exact-Ewald CVODE consistency study
- 1SocrateAI Lab
Abstract
Two rigid, vertically aligned electron–hole dipoles in a bilayer, at layer separation d and in-plane distance r, interact by V(r) = 2(1/r − 1/√(r2+d2)). As a function of t = r2 this is gd(t) = 2(t−1/2 − (t+d2)−1/2). 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, 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): gd satisfies upstream's AdmissiblePotential (smooth, nonnegative, completely monotone), as does the whole family t−s/2 − (t+c)−s/2 for s > 0, c ≥ 0; for c < 0 it fails (negative control); triangular-lattice optimality among locally finite configurations at density one and at every density ρ > 0, obtained from upstream's universal_energy_minimum and a rescaling theorem; for gd (d > 0) only: finiteness of the optimal energy at density one and at every density, so those inequalities are not ⊤ ≤ ⊤ (no finiteness theorem is proved for the rest of the shifted-difference family, which at c = 0 is identically zero); the Step-1 identity gd(r2) = 2(1/r − 1/√(r2+d2)) for r > 0 (the physical pair counting stays Tier C). These corollaries are conditional on the upstream openai/math theorem, which is AI-generated and not peer reviewed (the planar Cohn–Kumar conjecture was stated open in the human literature by Petrache and Serfaty in 2019), and on the fidelity of its definitions. The prior-round theorems were re-checked by a separate AI verifier (ACCEPT_WITH_CORRECTIONS); the every-density and shifted-difference module was re-elaborated from source by a separate AI auditor at the stage-4 audit (rc 0, axioms within the allowlist, planted sorry and planted axiom caught; verdict ACCEPT_WITH_CORRECTIONS, no blocking findings, corrections applied in this version); the small Step-1 module added in this revision is producer-checked only. No human has audited the statements. Tier C: the physics reading (classical, zero-temperature, rigid, unscreened point dipoles) and a step-by-step human demonstration for undergraduates. Complete monotonicity is elementary (Bernstein); the only new item is the explicit kernel-checked corollary. No breakthrough is claimed. Tier X: a new rusty-SUNDIALS module computes exact Ewald energies of the untruncated potential (agreement with an independent Python Ewald sum to about 1e-13; tail-dropping negative control caught). Preregistered CVODE gradient-flow relaxations found 0 of 21 relaxed periodic competitors below the triangular lattice (only 14 of the 21 are open searches; the other 7 are designed negative controls, and two runs end in the same state), with positive and negative controls behaving as designed; the run set is smaller than preregistered, and Ewald energies replace the preregistered truncated sum (a stated deviation). The HuggingFace dataset colabfit/JARVIS_DFT_3D_12_12_2022 (JARVIS-DFT, OptB88vdW; card license ‘unknown’) supplies a homo-stack proxy layer spacing of about 6.6 Å for MoSe2/WSe2, placing experimental exciton densities at d√n ≈ 0.02–0.11; the resulting unscreened square-minus-triangular gaps (about 0.0014 to 0.22 meV per exciton, with the gap taken at the nearest simulated d√n) are about 1.5 to 5 orders of magnitude below moiré trap depths, and real excitons there are a quantum gas. The Elenchus ledger gate reports 0 blocking findings and 14 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.
Related
- The triangular lattice minimises the planar Yukawa energy at every density and for every finite mixture of screening lengths: kernel-checked corollaries of planar universal optimality, a human proof, and an exact-potential CVODE consistency study
- Does the triangular lattice minimise the harmonic zero-point energy? A numerical counterexample for completely monotone potentials, with kernel-checked curvature identities
- An Explicit Family of Log-Concave Counterexamples to the Gaussian Completely Monotone Conjecture
- High-frequency coercivity loss for completely monotone memory on bounded time intervals
- Planar universal optimality, tiered: kernel-checked consequences, a non-uniqueness theorem, and a CVODE N-body consistency check for the Yukawa interaction
BibTeX
@misc{callens2026bilayer,
title = {{The bilayer dipolar-exciton interaction is completely monotone in r^2: kernel-checked triangular-lattice corollaries at every density and an exact-Ewald CVODE consistency study}},
author = {Xavier Callens},
howpublished = {Zenodo (CERN European Organization for Nuclear Research)},
year = {2026},
month = oct,
doi = {10.5281/zenodo.23646102},
url = {https://doi.org/10.5281/zenodo.23646102},
note = {CC BY},
}
RIS
TY - UNPB
TI - The bilayer dipolar-exciton interaction is completely monotone in r^2: kernel-checked triangular-lattice corollaries at every density and an exact-Ewald CVODE consistency study
AU - Xavier Callens
PY - 2026
DA - 2026/10/25
PB - Zenodo (CERN European Organization for Nuclear Research)
DO - 10.5281/zenodo.23646102
UR - https://doi.org/10.5281/zenodo.23646102
AB - Two rigid, vertically aligned electron–hole dipoles in a bilayer, at layer separation d and in-plane distance r, interact by V(r) = 2(1/r − 1/√(r2+d2)). As a function of t = r2 this is gd(t) = 2(t−1/2 − (t+d2)−1/2). 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, 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): gd satisfies upstream's AdmissiblePotential (smooth, nonnegative, completely monotone), as does the whole family t−s/2 − (t+c)−s/2 for s > 0, c ≥ 0; for c < 0 it fails (negative control); triangular-lattice optimality among locally finite configurations at density one and at every density ρ > 0, obtained from upstream's universal_energy_minimum and a rescaling theorem; for gd (d > 0) only: finiteness of the optimal energy at density one and at every density, so those inequalities are not ⊤ ≤ ⊤ (no finiteness theorem is proved for the rest of the shifted-difference family, which at c = 0 is identically zero); the Step-1 identity gd(r2) = 2(1/r − 1/√(r2+d2)) for r > 0 (the physical pair counting stays Tier C). These corollaries are conditional on the upstream openai/math theorem, which is AI-generated and not peer reviewed (the planar Cohn–Kumar conjecture was stated open in the human literature by Petrache and Serfaty in 2019), and on the fidelity of its definitions. The prior-round theorems were re-checked by a separate AI verifier (ACCEPT_WITH_CORRECTIONS); the every-density and shifted-difference module was re-elaborated from source by a separate AI auditor at the stage-4 audit (rc 0, axioms within the allowlist, planted sorry and planted axiom caught; verdict ACCEPT_WITH_CORRECTIONS, no blocking findings, corrections applied in this version); the small Step-1 module added in this revision is producer-checked only. No human has audited the statements. Tier C: the physics reading (classical, zero-temperature, rigid, unscreened point dipoles) and a step-by-step human demonstration for undergraduates. Complete monotonicity is elementary (Bernstein); the only new item is the explicit kernel-checked corollary. No breakthrough is claimed. Tier X: a new rusty-SUNDIALS module computes exact Ewald energies of the untruncated potential (agreement with an independent Python Ewald sum to about 1e-13; tail-dropping negative control caught). Preregistered CVODE gradient-flow relaxations found 0 of 21 relaxed periodic competitors below the triangular lattice (only 14 of the 21 are open searches; the other 7 are designed negative controls, and two runs end in the same state), with positive and negative controls behaving as designed; the run set is smaller than preregistered, and Ewald energies replace the preregistered truncated sum (a stated deviation). The HuggingFace dataset colabfit/JARVIS_DFT_3D_12_12_2022 (JARVIS-DFT, OptB88vdW; card license ‘unknown’) supplies a homo-stack proxy layer spacing of about 6.6 Å for MoSe2/WSe2, placing experimental exciton densities at d√n ≈ 0.02–0.11; the resulting unscreened square-minus-triangular gaps (about 0.0014 to 0.22 meV per exciton, with the gap taken at the nearest simulated d√n) are about 1.5 to 5 orders of magnitude below moiré trap depths, and real excitons there are a quantum gas. The Elenchus ledger gate reports 0 blocking findings and 14 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.
ER -