Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-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 pair of pants is a cobordism realizing addition of circles

Example

Let P={(x,y)∈R2:∥(x,y)∥≤2, ∥(x,y)−(1,0)∥≥12, ∥(x,y)+(1,0)∥≥12}, the closed disk of radius 2 with two disjoint open disks of radius 12 removed. Then P is a compact oriented smooth surface with boundary three circles, and with the outward-normal-first orientation its boundary is −(C1⊔C2)⊔C0, where C0 is the outer circle and C1,C2 are the two inner circles, all three carrying their counterclockwise orientations. Hence P is an oriented bordism from C1⊔C2 to C0 and exhibits in Ω1SO the additive relation [C1]+[C2]=[C0] (Unoriented and oriented bordism groups); all three classes are zero by the disk example (A circle is the boundary of a disk), so the example illustrates disjoint-union addition rather than an independent invariant.

Facts & Assumptions

Given: The set P above, the outer circle C0=S2(0,2), the inner circles C−=S2((1,0),12) and C+=S2((−1,0),12), the standard orientation of R2, and the induced orientation of P and of its boundary.

[F1]

At a boundary point of a planar region where exactly one smooth defining function ρ vanishes and dρ≠0, choose a coordinate whose derivative of ρ is nonzero. Use the other coordinate together with ρ as a local coordinate map. The inverse function theorem gives its C1 inverse, which is smooth by induction from the inverse-derivative formula; restricting to ρ≥0 gives a half-space chart, and ambient smooth transitions give a smooth boundary atlas (The Euclidean inverse function theorem, Euclidean upper half-space and its boundary, Smooth charts, atlases, and structures with boundary, Boundary-defining functions). The interior has Euclidean charts (Euclidean spaces and Euclidean open subsets as smooth manifolds). Euclidean closed balls are compact and closed subsets of compact spaces are compact (For n≥1, every Euclidean closed ball and every Euclidean sphere of positive radius is compact, A closed subspace of a compact space is compact, and a finite union of compact subspaces is compact, Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right).

[F2]

Boundary orientation is outward-normal-first (Induced boundary orientation). If r=p−c is the radial vector of a circle in the standard plane, det⁡(r,Jr)=∣r∣2>0. A normal pointing away from c therefore gives the counterclockwise tangent Jr, while a normal pointing toward c gives the clockwise tangent −Jr (Oriented smooth manifolds and oriented charts, A circle is the boundary of a disk).

[F3]

A bordism from a closed n-manifold M0 to M1 is data with a decomposition of the boundary into open and closed parts and collar embeddings of fixed widths; an oriented bordism additionally requires the induced boundary orientation to be the negative of the source orientation on the incoming face and the target orientation on the outgoing face (Oriented smooth cobordism, Smooth collars of a manifold boundary, Immersions and embeddings for manifolds with boundary).

[F4]

The bordism classes of closed oriented 1-manifolds form the abelian group Ω1SO with [M]+[N]=[M⊔N], and orientation-preserving diffeomorphic circles have equal class (Disjoint union makes bordism classes abelian groups, Smooth cobordism is an equivalence relation, Unoriented and oriented bordism groups, Diffeomorphisms and local diffeomorphisms of manifolds).

Verification

1.1F1

(P is a compact smooth surface with boundary the three circles.) Introduce the smooth functions ρ0(x)=4−∥x∥2, ρ−(x)=∥x−(1,0)∥2−14 and ρ+(x)=∥x+(1,0)∥2−14 on R2; then P={x:ρ0(x)≥0, ρ−(x)≥0, ρ+(x)≥0}. On C0={x:ρ0(x)=0} we have ∣x∣=2, so ∥x∓(1,0)∥≥2−1=1>12 and the other two functions are strictly positive; on C±={x:ρ±(x)=0} we have ∥x±(1,0)∥=12, so ∥x∥≤1+12=32<2 and, since the two inner centres are at distance 2 and the radii sum to 1, ∥x∓(1,0)∥≥2−12=32>12. Hence the three circles are pairwise disjoint and each boundary point of P lies on exactly one of them, where exactly one defining function vanishes with nonzero gradient. Each such point therefore has a boundary chart obtained from that defining function by the inverse function theorem, so P is a compact smooth surface with boundary C0⊔C1⊔C2; compactness follows because P is a closed subset of the compact disk {∣x∣≤2}.

2.1F2step 1.1

(The induced orientations of the three circles.) Give P the orientation induced from the standard orientation of R2. At a point p∈C0 the outward normal of P is the radial unit vector p/2, and (p/2,Jp/2) is a positive basis of R2, where J is the quarter-turn; by the outward-normal-first rule the positive tangent direction of C0 is Jp, the counterclockwise direction. At a point p∈C±, let c be the centre of that circle; the removed disk lies outside P in the direction c−p, so the outward normal of P at p is the unit vector (c−p)/∣c−p∣=2(c−p), and (2(c−p),2J(c−p)) is again a positive basis; hence the positive tangent direction is J(c−p)=−J(p−c), which is the clockwise direction of the circle centred at c. So the induced orientation of the outer circle is counterclockwise and that of each inner circle is clockwise, i.e. the oriented boundary is C0−C1−C2=−(C1⊔C2)⊔C0.

3.1F3step 1.1step 2.1

(P is an oriented bordism from C1⊔C2 to C0.) Take the incoming boundary part (∂P)0=C1⊔C2 with the source orientations counterclockwise on both circles, and the outgoing part (∂P)1=C0; the induced orientations computed in step 2.1 are clockwise on C1,C2, which is the negative of the source orientation on the incoming part, and counterclockwise on C0, which is the target orientation. The radial parametrisations θ0(s,p)=c+(1+s4)(p−c) for p in an inner circle with centre c, and θ1(s,p)=(1+s4)p for p∈C0, s∈[0,1) respectively s∈(−1,0], are smooth embeddings onto collar neighbourhoods of the corresponding boundary circles: their images have radii 12(1+s4)∈[12,58) and 2+s2∈(32,2] in the relevant radial directions and lie in P by the estimates of step 1.1. Hence P with these collars and this orientation is an oriented bordism from C1⊔C2 to C0.

4.1F4step 3.1∎

(The additive relation; all classes vanish.) By step 3.1 the cobordism class of C1⊔C2 equals that of C0, that is, [C1]+[C2]=[C0] in Ω1SO by [F4]. Each of the three circles is the boundary of a Euclidean disk (with the counterclockwise orientation induced by the standard orientation of the plane, after the outer circle is viewed as the boundary of the disk it encloses and each inner circle as the boundary of the removed disk), so by the disk example, which applies to a circle with either orientation, all three classes are zero in Ω1SO and in Ω1O; the relation therefore reads 0+0=0 and exhibits the disjoint-union addition of the group structure rather than an independent invariant.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

75 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