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.

Latitude and meridian intersections on the torus

Example

Let T2=Q×Q with Q=R/Z (The two-dimensional torus T2=(R/Z)2) carry the product smooth structure and product orientation (Products of smooth manifolds have a canonical product smooth structure, Product orientations). Let A:=Q×{[0]} be the latitude circle and B:={[0]}×Q the meridian circle, both embedded oriented circles cutting out by the coordinate projections (A regular level set is an embedded submanifold). They meet transversely in the single point ([0],[0]); with the product orientation and the first-factor-first convention of The local oriented intersection sign the local sign is +1, so I(A,B)=1, while I(B,A)=−1; the mod 2 number is I2(A,B)=I2(B,A)=1 and can be computed without orientations. Perturbing B to Bε={[t]}×Q for a fixed nonzero class [t] leaves the mod 2 number equal to 1 as long as the trace stays transverse to A.

Facts & Assumptions

Given: T2=Q×Q with the product smooth structure and product orientation, the latitude A=Q×{[0]} oriented by ∂x and the meridian B={[0]}×Q oriented by ∂y in the positive product frame (∂x,∂y).

[F1]

Give Q=R/Z its standard quotient smooth structure: the projection is a diffeomorphism on sufficiently short intervals, and the overlap transitions are integer translations. The projection of [0,1] covers Q, so it is compact. These local coordinates orient Q by the increasing real coordinate, and T2=Q×Q has the product smooth structure (The circle as S1=R/Z with basepoint [0], The two-dimensional torus T2=(R/Z)2, Products of smooth manifolds have a canonical product smooth structure).

[F2]

The coordinate circles are regular level sets of the coordinate projections, hence embedded submanifolds, and the tangent bundle of the product splits canonically as T(x,y)T2=TxQ⊕TyQ with the positive product frame (∂x,∂y) (A regular level set is an embedded submanifold, Canonical tangent and cotangent splittings for products, Product orientations).

[F3]

The local sign compares (TpA,TpB) in that order with the orientation of TpT2, and the intersection number is the sum of the local signs over the finite transverse intersection (The local oriented intersection sign, The oriented intersection number, Transverse complementary-dimensional intersection sets).

[F4]

The mod 2 intersection number is the cardinality of a transverse intersection modulo two and needs no orientation (The mod 2 intersection number); under ACω it is invariant under homotopies of the map (The mod 2 intersection number is homotopy invariant).

Verification

1.1F2F3givenalgebra

By [F2] the sets A and B are embedded circles, and A∩B={([0],[0])}: a point of A has second coordinate [0], a point of B has first coordinate [0]. At that point TpA=R∂x and TpB=R∂y, and (∂x,∂y) is the positive product frame, so A and B are transverse and the local sign is +1 by [F3]. Hence I(A,B)=1; with the factors exchanged the ordered basis (∂y,∂x) is negative, so I(B,A)=−1.

2.1F1F4step 1.1algebra∎

The same computation counts mod two: the transverse intersection has one point, so I2(A,B)=I2(B,A)=1 by [F4], and no orientation hypothesis was used. For the perturbation, each Bt:={[t]}×Q with t∈R is again a meridian circle with TpBt=R∂y at its unique intersection point ([t],[0]) with A, so the intersection is transverse with one point and I2(A,Bt)=1 for every t; the explicit family t↦{[t]}×Q thus has constant mod 2 count by this direct computation. Thus the example realizes the source's count I2=1 and the sign asymmetry I(A,B)=−I(B,A); no choice principle is used: the circles, the product structure and the perturbation are explicit, the perturbation count is computed directly for every t, without selecting a homotopy or applying classification.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

55 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