Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-11
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.

Infinite Ramsey for triples gives a convex or concave subsequence of every real sequence in general position

Example

Let (xn)(x_n) be a real sequence (Sequences of reals: bounded, eventually, frequently, tails, subsequences) such that no three points (i,xi)(i,x_i) are collinear. Then it has an infinite subsequence whose graph is strictly convex or strictly concave: every selected triple has respectively increasing or decreasing secant slopes. All divisions are by positive index differences and use the ordered-field rules of Ordered field.

Facts & Assumptions

Given: Such a sequence (xn)(x_n).

[L1]

Every finite colouring of [N]k[\mathbb N]^k has an infinite monochromatic set, in ZF (Infinite Ramsey theorem on N\mathbb N: every finite colouring of [N]k[\mathbb N]^k has an infinite monochromatic set, in ZF).

Verification

technique · direct
1.1

For i<j<ki<j<k, colour the triple convex when (xj−xi)/(j−i)<(xk−xj)/(k−j)(x_j-x_i)/(j-i)<(x_k-x_j)/(k-j) and concave when the reverse inequality holds. General position excludes equality, so this is a two-colouring. Apply [L1] with k=3k=3.

L1
2.1

On the resulting infinite index set, every ordered triple has the same strict slope comparison. In the convex colour every successive secant slope increases, and in the concave colour every such slope decreases.

step 1.1L1
3.1

Increasing secant slopes are exactly the strict convexity inequality for the selected graph, while decreasing slopes give strict concavity. Thus the increasing enumeration of the homogeneous index set is the required subsequence.

step 2.1algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 43 results over 16 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources