CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-sol)

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 continuous function of modulus at most one need not be positive definite

Statement refuted

On $G = R$ let $ϕ$ be the continuous trapezoid function $ϕ (x) = {\begin{cases} 1, & ∣ x ∣ \leq 1, \\ 2 - ∣ x ∣, & 1 \leq ∣ x ∣ \leq 2, \\ 0, & ∣ x ∣ \geq 2, \end{cases}$ so that $ϕ$ is linear on $[1, 2]$ and on $[- 2, - 1]$ and vanishes outside $[- 2, 2]$ . Then $ϕ$ is continuous, $ϕ (0) = 1$ and $∣ ϕ (x) ∣ \leq 1$ for all $x$ , but $ϕ$ is not positive definite (Positive definite functions on an abelian group): for the points $x_{1} = 0, x_{2} = 1, x_{3} = 2$ , the matrix $[ϕ (x_{j} - x_{k})]_{j, k} = (\begin{array}{ccc} 1 & 1 & 0 \\ 1 & 1 & 1 \\ 0 & 1 & 1 \end{array})$ has determinant $- 1 < 0$ , so it is not positive semidefinite and the positive-definiteness inequality fails; explicitly, the coefficients $c = (1, - 2, 1)$ give quadratic form $- 2 < 0$ . Thus boundedness and continuity of a function of modulus at most one do not imply positive definiteness.

Facts & Assumptions

Given: The trapezoid function $ϕ : R \to C$ above.

[F1]

$ϕ : R \to C$ is continuous, $ϕ (0) = 1$ , and $∣ ϕ (x) ∣ \leq 1$ for every $x$ (Continuity of a map of topological spaces at a point and globally, The complex numbers as $R [x] / (x^{2} + 1)$ , with the real embedding and imaginary unit $i$ ): on $[- 1, 1]$ it is the constant $1$ , on $[1, 2]$ and on $[- 2, - 1]$ it is the continuous affine function $2 - ∣ x ∣$ joining the values $1$ and $0$ , and it is $0$ outside $[- 2, 2]$ .

[F2]

$ϕ$ is positive definite exactly when $\sum_{j, k} c_{j} \overline{c_{k}} ϕ (x_{j} - x_{k}) \geq 0$ for every finite family $x_{1}, \dots, x_{n} \in R$ and all $c_{1}, \dots, c_{n} \in C$ (Positive definite functions on an abelian group).

Counterexample

technique · direct

1.1F1algebra

The values of $ϕ$ at the differences of $x_{1} = 0, x_{2} = 1, x_{3} = 2$ are $ϕ (0) = 1$ , $ϕ (\pm 1) = 1$ and $ϕ (\pm 2) = 0$ , so the Hermitian matrix of [F2] is $M = (\begin{array}{ccc} 1 & 1 & 0 \\ 1 & 1 & 1 \\ 0 & 1 & 1 \end{array})$ . Its determinant is $1 \cdot (1 \cdot 1 - 1 \cdot 1) - 1 \cdot (1 \cdot 1 - 1 \cdot 0) + 0 \cdot (1 \cdot 1 - 1 \cdot 0) = - 1 < 0$ . The explicit negative quadratic form in the next step establishes the failure of positive semidefiniteness directly.

2.1F2step 1.1algebra∎

Explicitly, the coefficients $c_{1} = 1, c_{2} = - 2, c_{3} = 1$ give $\sum_{j = 1}^{3} \sum_{k = 1}^{3} c_{j} c_{k} ϕ (x_{j} - x_{k}) = 1 + 4 + 1 + 2 \cdot (- 2) + 2 \cdot (- 2) = - 2 < 0,$ the quadratic form of $M$ being $c_{1}^{2} + c_{2}^{2} + c_{3}^{2} + 2 c_{1} c_{2} + 2 c_{2} c_{3}$ ; hence the defining inequality of [F2] fails for this finite family, and $ϕ$ is not positive definite, even though it is continuous with $ϕ (0) = 1$ and $∣ ϕ (x) ∣ \leq 1$ everywhere.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

11 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

Manfred Einsiedler and Thomas Ward, Ergodic Theory with a View Towards Number Theory, Appendix C.2-C.3 (course-hosted full text) (standard reference, not scraped)
Lynn H. Loomis, Introduction to Abstract Harmonic Analysis, D. Van Nostrand, 1953 (Harvard-hosted full scan) (standard reference, not scraped)