Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-sol)
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.

A quadratic norm-one torus and its sign action

Example

Assume the Axiom of Choice. Let k have characteristic different from 2, and let d∈k× be a nonsquare. The affine group T=Spec⁡k[x,y]/(x2−dy2−1), with product (x,y)(x′,y′)=(xx′+dyy′,xy′+yx′), is a nonsplit torus. Its character module is Z, on which the nontrivial automorphism of k(d)/k acts by n↦−n. For k=R and d=−1, this is the circle group x2+y2=1, as an algebraic group over R.

Facts & Assumptions

[A1]

Assume The Axiom of Choice; it is used through the general multiplicative-type classification, whose affineness interface uses fpqc submersiveness.

[F2]

Classification by Galois modules is Multiplicative type groups and Galois character modules.

Verification

Given: char⁡k≠2 and nonsquare d∈k×.

1.1F1algebra

The displayed multiplication is multiplication of x+yd; the norm x2−dy2 multiplies, so it preserves the equation. The identity is (1,0) and the inverse is (x,−y), and associative multiplication follows by direct expansion in the basis 1,d. This gives an affine group by F1. Over L=k(d) put t=x+d y. Then t−1=x−d y, and x=(t+t−1)/2, y=(t−t−1)/(2d) give inverse algebra maps with L[t,t−1]. They preserve multiplication, so TL≅Gm.

2.1A1F2F3step 1.1algebra∎

The nontrivial σ∈Gal⁡(L/k) sends t to t−1, so it sends tn to t−n. F2 gives the sign action on Z; F3 makes T a torus. It cannot be split: a split rank-one torus has trivial action, and no isomorphism of abelian groups Z→Z intertwines the sign action with the trivial action (its nonzero generator would have to equal its negative). For d=−1 over R the equation and product are exactly those of unit complex numbers.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

14 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