Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-03
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 fundamental group of the unit interval is trivial at every basepoint

Example

For every x0∈I=[0,1]x_0\in I=[0,1], the fundamental group π1(I,x0)\pi_1(I,x_0) has one element. A loop α\alpha contracts relative to its endpoints by

H(s,t)=(1−t)α(s)+tx0.H(s,t)=(1-t)\alpha(s)+t x_0.

Facts & Assumptions

Given: A basepoint x0∈Ix_0\in I and a based loop α:I→I\alpha:I\to I.

[L1]

The unit interval is convex: if x,y,t∈[0,1]x,y,t\in[0,1], then 0≤(1−t)x+ty≤10\le(1-t)x+ty\le1, so the convex combination remains in [0,1][0,1] (Intervals of R\mathbb{R}: the nine order-convex forms, nondegeneracy, and length, A convex subset of Rm\mathbb{R}^m contains every line segment between two of its points, algebra).

[L2]

Every nonempty convex Euclidean subset is simply connected, with the displayed straight-line endpoint homotopy (Every nonempty convex subset of Rn\mathbb R^n is simply connected).

[L3]

Elements of π1(I,x0)\pi_1(I,x_0) are endpoint-homotopy classes of based loops (Based loops and the fundamental group).

Verification

technique · direct
1.1

By [L1], the interval satisfies the hypotheses of [L2], so the displayed formula is an endpoint-fixed homotopy from α\alpha to the constant loop at x0x_0.

L1L2
2.1

Thus every class in π1(I,x0)\pi_1(I,x_0) equals the constant-loop class, and the group has exactly one element.

step 1.1L3∎

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: 55 results over 15 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