Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: Literature-sourcedPipeline-generatedprecheck passjudge 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.

The standard seven-sphere as the (1,0) quaternionic Hopf sphere bundle

Example

Assume the Axiom of Choice. The (1,0) Milnor sphere bundle is diffeomorphic to the standard S7, and its disk filling has q=4, σ=1 and λ=0(mod7).

Facts & Assumptions

[F1]

The quaternionic clutching is upper-to-lower (a,v)+∼(a,av)− for (h,j)=(1,0) (The Milnor sphere and disk bundles Mh,j and Wh,j).

[F3]

The filling-independent invariant is λ=2q−σ(mod7) (The Milnor lambda invariant is well defined modulo seven).

Verification

Given: AC and the sphere S7={(q0,q1)∈H2:∣q0∣2+∣q1∣2=1}, with the projection onto right quaternionic lines.

1.1F1givenconstruct

On the base chart q0≠0, put z=q1q0−1 and write (q0,q1)=(1,z)λ/1+∣z∣2, with unit λ=q0/∣q0∣. On q1≠0, put w=q0q1−1=z−1 and write (q0,q1)=(w,1)λ′/1+∣w∣2, with λ′=q1/∣q1∣. These formulas and their inverses are smooth. The base is the one-point compactification of H; replacing the second coordinate w by wˉ gives the usual stereographic transition z↦z/∣z∣2, hence its smooth structure is that of S4. On the equator ∣z∣=1 set a=z; the fibre transition is λ′=aλ, since quaternionic multiplication has the displayed order. Thus the two hemisphere product charts of S7 glue by precisely [F1], giving M1,0≅S7.

2.1step 1.1F2F3algebra∎

By [F2], q(W1,0)=4 and σ(W1,0)=1. Therefore [F3] gives λ(M1,0)=2⋅4−1=7≡0(mod7), agreeing with the standard sphere's disk filling.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

28 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