CounterexampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-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.

A boundary mode has a different concentration rate

Statement refuted

Every $C^{2}$ function $h$ on $[0, 1]$ with a unique maximizer at the boundary point $0$ and $h^{''} (0) < 0$ satisfies the interior Gaussian formula $\int_{0}^{1} e^{n h (x)} d x \sim e^{n h (0)} \sqrt{\frac{2 π}{n (- h^{''} (0))}} .$

Facts & Assumptions

Given: The phase $h (x) : = - x - x^{2}$ on $[0, 1]$ and the integral $I_{n} : = \int_{0}^{1} e^{n h (x)} d x$ for integers $n \geq 1$ .

[F1]

Higher derivatives and the classes $C^{k}$ and $C^{\infty}$ : a $C^{2}$ function has continuous first and second derivatives on its interval.

[F2]

The exponential function is strictly increasing and The exponential is positive and satisfies $\exp (- x) = 1 / \exp (x)$ : the real exponential is increasing and positive.

[F3]

A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion: a continuous function on $[0, 1]$ is bounded and Riemann integrable.

[F4]

If $f \leq g$ on $[a, b]$ and both are integrable then $\int_{a}^{b} f \leq \int_{a}^{b} g$ ; and $m (b - a) \leq \int_{a}^{b} f \leq M (b - a)$ : pointwise inequalities between integrable functions on an increasing interval pass to their integrals.

[F5]

Newton–Leibniz needs only continuity on $[a, b]$ , differentiability on $(a, b)$ , and a Riemann-integrable extension of the interior derivative: if $G$ is continuous on $[a, b]$ , differentiable on $(a, b)$ , and $G^{'}$ has a Riemann-integrable extension, then $\int_{a}^{b} G^{'} = G (b) - G (a)$ .

[F6]

The exponential function is smooth and $(\exp)^{'} = \exp$ : the real exponential is differentiable with derivative $\exp$ .

Counterexample

1.1givenF1algebra

The phase is $C^{2}$ , satisfies $h (0) = 0$ , $h (x) < 0$ for every $x \in (0, 1]$ , and $h^{''} (0) = - 2$ . Thus its unique maximizer is the boundary point $0$ , and the refuted formula predicts $\sqrt{π / n}$ .

1.2givenF2F3F4F5F6algebra

For $x \in [0, 1]$ , $h (x) = - x - x^{2} \leq - x$ , so [F2] and [F4] give $0 \leq I_{n} \leq \int_{0}^{1} e^{- n x} d x$ . The antiderivative $G (x) = - e^{- n x} / n$ has derivative $e^{- n x}$ by [F6]; [F3, F5] evaluate the latter integral as $(1 - e^{- n}) / n \leq 1 / n$ .

2.1givenF2F3F4step 1.2algebra

On $[0, 1 / n]$ with $n \geq 1$ , $n (x + x^{2}) \leq 1 + 1 / n \leq 2$ . Thus $e^{n h (x)} \geq e^{- 2}$ there and [F3, F4] give $I_{n} \geq e^{- 2} / n$ . Together with step 1.2, this proves $e^{- 2} / n \leq I_{n} \leq 1 / n$ , so the boundary contribution has order $n^{- 1}$ .

3.1step 1.1step 1.2algebra∎

Consequently $0 \leq I_{n} / \sqrt{π / n} \leq 1 / \sqrt{π n} \to 0$ . The ratio required by the refuted asymptotic formula therefore tends to $0$ , not $1$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

47 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

NIST Digital Library of Mathematical Functions, §2.3(iii), Laplace's Method (standard reference, not scraped)
Laplace method for integrals, PHYS 2400, University of Connecticut (standard reference, not scraped)