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.
Finite target bounds do not supply an infinite target bound
Statement refuted
The implication “ and core bounds entail a bounded core estimate” is false, even with both given constants equal to one. Assume countable choice for the cited Lebesgue measure construction.
Facts & Assumptions
The Lp norms of complex simple functions are given by the integrals of their moduli and their essential bounds Complex Lp classes and Euclidean test-function conventions.
Under countable choice an open interval has measure equal to its length A box in with parameters is Lebesgue measurable of measure , whichever of its faces are included.
Countable choice is assumed for the preceding interval-measure result The Axiom of Countable Choice ().
The complex norm is well-defined on a.e. classes Complex Holder, Minkowski, and the quotient norm.
For every real bound there is a larger natural number Every complete ordered field is Archimedean.
Counterexample
Given: The objects and hypotheses in the statement.
Use Lebesgue measure on (0,1) and let T be the identity on complex finite simple classes. It is complex-linear and has and . Countable choice supplies the stated earlier Lebesgue-measure result, which gives measure one to (0,1) and measure to for each integer .
Define . It is a finite simple function of finite-measure support. Direct integration gives and . Its infinity norm is n: n is a pointwise bound, and every smaller nonnegative bound fails on a set of measure . Thus an bound C would require for every , impossible for finite C.
Depends on
- Complex Lp classes and Euclidean test-function conventions
- Complex Holder, Minkowski, and the quotient norm
- A box in $\mathbb{R}^n$ with parameters $a_i\le b_i$ is Lebesgue measurable of measure $\prod_{i<n}(b_i-a_i)$, whichever of its faces are included
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
- Every complete ordered field is Archimedean
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
50 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
- Laugesen Theorem C.6 and Remark C.7, endpoint parameter scope; explicit witness (standard reference, not scraped)