Alphabeta Math
ExampleConstruction: AI-adaptedVerification: AI-generatedSession-authored (Fable 5 assisted)precheck passaudited 2026-07-31verified 2026-08-08 (gpt-5.6-terra-codex-subscription)
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.

Two paths with the same endpoints in a convex subset of Rn\mathbb{R}^n are path homotopic relative to their endpoints

Example

Let C⊆RnC\subseteq\mathbb R^n be convex, with n≥1n\ge1, and let α,β:I→C\alpha,\beta:I\to C be paths with the same initial and terminal points. Then

H(s,t)=(1−t)α(s)+tβ(s)H(s,t)=(1-t)\alpha(s)+t\beta(s)

is a path homotopy from α\alpha to β\beta relative to the endpoints.

Facts & Assumptions

Given: A convex C⊆RnC\subseteq\mathbb R^n and paths α,β:I→C\alpha,\beta:I\to C with α(0)=β(0)\alpha(0)=\beta(0) and α(1)=β(1)\alpha(1)=\beta(1).

[L1]

The straight-line formula defines a continuous map H:I×I→CH:I\times I\to C (For continuous maps into a convex subset of Rn\mathbb{R}^n, the straight-line formula defines a continuous homotopy).

[A1]

A path homotopy relative endpoints is a homotopy H:I×I→CH:I\times I\to C with the path parameter on the first coordinate and with H(0,t)H(0,t) and H(1,t)H(1,t) fixed (Homotopies of continuous maps, homotopies relative to a subspace, and path homotopies relative to the endpoints).

Verification

technique · direct
1.1

The map HH is continuous by [L1].

L1
1.2

One has H(s,0)=α(s)H(s,0)=\alpha(s) and H(s,1)=β(s)H(s,1)=\beta(s). At the endpoints, H(0,t)=(1−t)α(0)+tβ(0)=α(0)H(0,t)=(1-t)\alpha(0)+t\beta(0)=\alpha(0) and H(1,t)=(1−t)α(1)+tβ(1)=α(1)H(1,t)=(1-t)\alpha(1)+t\beta(1)=\alpha(1).

algebra
2.1

Thus HH satisfies all clauses of [A1], so it is a path homotopy from α\alpha to β\beta relative to the endpoints.

step 1.1step 1.2A1∎

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: 64 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