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.
The logarithm to a positive base other than one
Definition
For with and , define
The denominator is nonzero: would imply by the inverse identities of The natural logarithm as the inverse of the exponential function.
Depends on
Used by
- Every continuous f with f(xy)=f(x)+f(y) is f(x)=c log x for a unique c, including c=0 Corollary
- For fixed H, the log-log scale eventually exceeds every classical scale 2^c√log₂ n Corollary
- Subreciprocal function and ell divisibility Definition
- A lower bound of size 2^c√log₂ n is still subpolynomial in n Example
- A lower bound of size 2^c√log₂ n log₂ log₂ n is still subpolynomial in n Example
- Dropping f(e)=1 leaves the whole family c log, including logarithms to other bases and the zero function Example
- For large n, the Fox–Sudakov choice of x leaves a dense-or-sparse set of order at least √n Example
- For large n, the log-log choice of x still leaves a dense-or-sparse set of order at least √n Example
- The P₃-free case is much stronger than the general lower bounds Example
- Alon–Pach–Solymosi: if H₁ and H₂ have the Erdős–Hajnal property, so does the graph obtained from H₁ by substituting H₂ for a vertex Theorem
- Change of base and inversion of the positive-base real exponential Theorem
- Every H-free graph has a homogeneous set of size at least 2^c√log₂ n Theorem
- Every H-free graph has a homogeneous set of size at least 2^c√log₂ n log₂ log₂ n Theorem
- Every nonempty n-vertex graph satisfies hom(G)≥ 1/2 log₂ n Theorem
- For every n≥16 there is an n-vertex graph with hom(G)<3 log₂ n Theorem
Dependency tree · two levels
2 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
- J. Lebl, Basic Analysis, Logarithm and Exponential (standard reference, not scraped)
- MIT OpenCourseWare 18.100B Real Analysis, Spring 2025 full lecture notes (standard reference, not scraped)