Metadata

slug: novaes-2023-strong-absorption-spectral-moments
bibkey: novaes2023absorption
doi: 10.1007/s10955-023-03183-7
url: https://arxiv.org/abs/2305.18235
triage: theorem
motivation_gids:
  - D5/S3/Quantum/Transport/StrongAbsorptionMoments.result

Novaes’s strong-absorption spectral and Wigner moment conjectures

Problem

M. Novaes, Time delay statistics for chaotic cavities with absorption, arXiv:2305.18235v1, Section 5, p. 7, states: “We conjecture that $(1/ M) ⟨ Tr (Q^{n})⟩$ is given by” Eq. (54) and that $(1/ M^{n}) ⟨[Tr (Q)]^{n} ⟩$ is given by Eq. (55), for every positive integer $n$ :

$\frac{1}{γ ^{n}} - \frac{n}{γ ^{n + 1}} + \frac{n ^{2}}{γ ^{n + 2}} - \frac{( n + 1 ) ( n ( 5 n - 2 ) M ^{2} + n ( n + 2 ) )}{6 M ^{2} γ ^{n + 3}} + O (γ^{- n - 4}),$

and

$\frac{1}{γ ^{n}} - \frac{n}{γ ^{n + 1}} + \frac{n ( ( n + 1 ) M ^{2} + ( n - 1 ) )}{2 M ^{2} γ ^{n + 2}} + O (γ^{- n - 3}) .$

Here $M \geq 1$ is the channel number, $n \geq 1$ is the order, and the model is the finite-channel $β = 2$ law with uniform absorption. The journal version is Journal of Statistical Physics 190, 182 (2023), DOI 10.1007/s10955-023-03183-7.

Statement echo

Source clause	Formal counterpart
Every positive channel number	`claim54` and `claim55` quantify $M$ with $1 \leq M$ .
Every positive integer order	Both claims quantify $n$ with $1 \leq n$ .
Spectral observable $(1/ M) Tr (Q^{n})$	`traceQPow` is $(M : R)^{- 1} \sum_{i} (γ + p_{1} (i))^{- n}$ .
Wigner observable $(1/ M^{n}) [Tr (Q)]^{n}$	`tauW M γ p ^ n` is the normalized Wigner delay power.
Expectation under the stated law	Both integrals use `law M γ`.
The displayed coefficients and remainder orders	The two absolute remainder inequalities in `claim54` and `claim55` use the literal coefficients and powers.
The same external source conjectures both formulas	`claim` is the conjunction `claim54 ∧ claim55`.

Motivation

D5/S3/Quantum/Transport/StrongAbsorptionMoments.result proves the two conjectured expansions for every $M \geq 1$ and $n \geq 1$ , with constants that may depend on $M$ and $n$ .

Gap

This is the named external conjecture preregistered in #19346. The screened literature records the formulas as conjectures; completeness of that screen is ASSUMED-UNVERIFIED.

Route

The finite-channel law is expanded around the product Laguerre law. The first two cross-density coefficients satisfy $E_{0} [D_{2}] = E_{0} [A D_{2}] = 0$ , while the surviving finite-channel term is fixed by the cubic Laguerre moment $E_{0} [C] = 5 M + 1/ M$ . Polynomial moment jets and finite binomial truncation then control every order $n$ . The spectral and Wigner remainder estimates assemble these identities into the two stated absolute bounds.

Falsifier

The formal claim would fail if some $M \geq 1$ or $n \geq 1$ made either scaled absolute error unbounded as $γ \to \infty$ . A numerical discrepancy alone would require checking the law, units and observable convention. The theorem concerns the stated normalized law and these conventions.

Evidence

The delivered modules are D5/S3/Quantum/Transport/StrongAbsorption/SecondOrderDensity.lean and D5/S3/Quantum/Transport/StrongAbsorptionMoments.lean; the latter’s settling declaration is D5.S3.Quantum.Transport.StrongAbsorptionMoments.result. The supporting frozen owners are the Density, Foundations, LaguerreMoments and StrongAbsorptionCumulants modules. The axiom closure of every public declaration is contained in ${propext, Classical.choice, Quot.sound}$ .

The four-slot escape audit for the newly public supporting theorems is unfinished under #19485; no declared_validated registration is asserted. The missing evidence is the faithful source-family reconstruction, realization bridge, whole-family intervention, sensitivity and observational-dependence evidence.

Experiment

The numerical check is pinned to experiments commit a136bd997edd4f34114b1e7c17fecff5c7c920d1. Command: python3 check.py in that directory; exit 0, RESULT PASS. Script SHA-256: 959e27a9d059f1e44ecee913fbdb09b52df74f466eae7fd9f7bab49d74abe497. The tested scope is exactly Eq. (54) for $M = 1, 2$ with $n \leq 4$ and $M = 3$ with $n \leq 3$ , Eq. (55) for $M \leq 3, n \leq 3$ , and the Eq. (52) comparison at $n = 2$ for every $M < 20$ . These finite computations corroborate the all- $M, n$ Lean result without replacing it.

Triage

What the settlement shows

Target item	Status and evidence
Mechanism: $E_{0} [D_{2}] = E_{0} [A D_{2}] = 0$	Proved in the kernel-checked path through `spectral_moments_low` and the density declarations used by `result`.
Mechanism: cubic Laguerre moment $E_{0} [C] = 5 M + 1/ M$	Proved in the kernel-checked path through `laguerre_cubic_ibp`, `singleBaseExpectation_c`, and `pair_quadratic_sum`.
Escape live path through `result54`, `spectral_normalized_third_order`, `spectral_moments_low`, `baseExpectation_spectral_low`, `singleBaseExpectation_c`, `laguerre_cubic_ibp`, and `pair_quadratic_sum`	Proved: these declarations are used by the delivered settling proof.
Scope: Eqs. (54) and (55) for every $M \geq 1, n \geq 1$	Kernel-checked: `D5.S3.Quantum.Transport.StrongAbsorptionMoments.result`.
Consequence with the pre-existing Eq. (58) settlement	Proved in the stated $β = 2$ model: the spectral and Wigner moment orders are established alongside the cumulant result in `novaes-2023-strong-absorption-cumulants`.
Exact-series checker	Computed: the pinned experiment exits 0 with `RESULT PASS` on the finite scope listed in the experiment entry.
Uniformity of remainder constants as $M$ or $n$ varies	Open; the theorem permits constants depending on $M$ and $n$ .
Higher asymptotic orders	Open; the result stops at the source’s stated orders.
External prior-art completeness	Open and `ASSUMED-UNVERIFIED`; the literature screen does not establish worldwide completeness.

The decisive structure is the cancellation of the first two cross-density coefficients and the cubic Laguerre moment. Finite binomial truncation then propagates the low-degree identities to every positive order. The proof does not claim uniform constants, higher orders, or a settlement for other symmetry classes.

ASSUMED-UNVERIFIED

Literature-search completeness and the correspondence between the normalized law and the physical random-matrix model remain ASSUMED-UNVERIFIED. Numerical quadrature covers only the finite tested scope in the experiment entry. Escape registration remains unfinished under #19485.

Keyboard shortcuts

trureturing — Discovering truth