Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + claude-sonnet-5)audited 2026-08-17
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 geometric loops t(cos2πnt,sin2πnt) have degree n

Example

For every integer n, the based geometric loop

γn(t)=(cos2πnt,sin2πnt)

has degree n, where degree is transported from the quotient-circle model by the based homeomorphism.

Facts & Assumptions

Given: An integer n and the quotient-circle dictionary.

[L1]

[t](cos2πt,sin2πt) is a homeomorphism from R/Z to the unit circle and sends [0] to (1,0) ([t](cos2πt,sin2πt) is a homeomorphism from R/Z to the unit circle).

[L2]

deg(ωn)=n for every integer n (deg(ωn)=n for every integer n).

[L3]

For every integer n, ωn(t)=[nt] (The standard circle loops ωn(t)=[nt] for nZ).

Verification

technique · direct
1.1

Under the homeomorphism of [L1], the loop in [L3] has image t(cos(2πnt),sin(2πnt))=γn(t).

L1L3algebra
2.1

The quotient loop has degree n by [L2], so the transported degree of its geometric image γn is also n. At n=0 this is the constant loop, and the same computation covers every negative n.

step 1.1L2

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: 123 results over 19 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