Alphabeta Math
Pipeline-generated
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.

✓ 11 results · all verified · 0 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 11 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Manifolds with Boundary Collars and Orientations — Examples

1 · Prerequisites

2 · Summary

These examples test the half-space, collar, flow-direction, neatness, and orientation conventions, including the n=0 and n≥1 boundaries stated in the individual items.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: Literature-sourcedVerification: AI-generatedprecheck passaudited 2026-09-07Open item page →

The closed half-space as a manifold with boundary

Example

For n≥1, the identity chart on Hn gives Int⁡Hn={xn>0} and ∂Hn={xn=0}; at the face, inward vectors have positive last component. For n=0, H0 is a point with empty boundary.

Facts & Assumptions

Given: An integer n≥0, with Hn and ∂Hn as in the stated convention.

[L1]

The model half-space is Hn={xn≥0} for n≥1, with face {xn=0}; for n=0, H0=R0 and its face is empty (Euclidean upper half-space and its boundary).

[L2]

Boundary charts define the smooth structure, and face versus relative-interior points is invariant under smooth changes of boundary chart (Topological manifolds with boundary; Smooth charts, atlases, and structures with boundary; Smooth invariance of the manifold boundary).

[L3]

At a face point, the last coordinate classifies tangent vectors as inward, outward, or boundary-tangent according as it is positive, negative, or zero (Inward, outward, and boundary-tangent vectors).

Verification

technique · direct
1.1givenL1L2

For n≥1, the identity map is a global boundary chart on Hn; for n=0, the unique map identifies the point with R0. These charts give the asserted smooth manifolds with boundary.

2.1givenL1L2L3step 1.1∎

For n≥1, [L1] and [L2] identify the intrinsic interior with {xn>0} and the intrinsic boundary with {xn=0}. The identity chart identifies every tangent space with Rn, and [L3] makes the inward vectors at the face precisely those with positive last component. For n=0, [L1] makes the unique point interior and the boundary empty.

ExampleConstruction: Literature-sourcedVerification: AI-generatedprecheck passaudited 2026-09-07Open item page →

The closed ball and its sphere boundary

Example

For n≥1, the closed ball Bn is a manifold with boundary Sn−1, and ρ(x)=1−∣x∣2 is a boundary-defining function.

Facts & Assumptions

Given: An integer n≥1, the closed unit ball Bn={x∈Rn:∣x∣≤1}, its sphere Sn−1={x:∣x∣=1}, and ρ:Bn→[0,∞) defined by ρ(x)=1−∣x∣2.

[L1]

A smooth Euclidean map with invertible derivative is a diffeomorphism between suitable open neighbourhoods (The Euclidean inverse function theorem).

[L2]

A compatible covering atlas by relatively open half-space charts defines a smooth manifold with boundary (Smooth charts, atlases, and structures with boundary).

[L3]

A boundary-defining function is smooth and nonnegative, has the boundary as its zero set, and has nonzero differential there (Boundary-defining functions).

Verification

technique · direct
1.1givenL1L2algebra

Let p∈Sn−1 and choose k with pk≠0. The map H(x)=(x1,…,xk^,…,xn,ρ(x)) has invertible derivative at p, since ∂ρ/∂xk(p)=−2pk≠0. By [L1], H is a diffeomorphism near p. Because Bn={ρ≥0}, its restriction is a half-space chart near p; ordinary Euclidean charts cover {∣x∣<1}. Every transition between these charts is the restriction of a composition of the corresponding Euclidean diffeomorphisms and their inverses, so the covering atlas is compatible. Thus [L2] makes Bn a smooth manifold with boundary, and the chart calculation identifies its boundary with Sn−1.

2.1givenL3step 1.1algebra∎

By construction, ρ≥0 on Bn, ρ−1(0)=Sn−1=∂Bn, and dρx(v)=−2⟨x,v⟩ is nonzero when ∣x∣=1. Hence ρ satisfies [L3].

ExampleConstruction: Literature-sourcedVerification: AI-generatedprecheck passaudited 2026-09-07Open item page →

A cylinder with oppositely oriented boundary components

Example

For the product orientation on [0,1]×S1, the boundary circles {1}×S1 and {0}×S1 receive opposite orientations.

Facts & Assumptions

Given: The interval [0,1] with positive tangent ∂t, the circle S1 with a chosen orientation, and [0,1]×S1 with the product orientation in that factor order.

[L1]

The product orientation orders the interval tangent before an oriented basis of the circle tangent (Product orientations).

[L2]

A boundary basis is positive exactly when placing an outward vector before it gives the ambient orientation (Induced boundary orientation).

Verification

technique · direct
1.1givenalgebra

Along {1}×S1, the outward vector is +∂t, whereas along {0}×S1 it is −∂t.

2.1givenL1L2step 1.1algebra∎

If v is a positive tangent vector to S1, then (∂t,v) is positive by [L1]. Thus [L2] makes v positive on {1}×S1, while it makes −v positive on {0}×S1, because (−∂t,−v) has the same orientation as (∂t,v). The two boundary-circle orientations are opposite.

ExampleConstruction: Literature-sourcedVerification: AI-generatedprecheck passaudited 2026-09-07Open item page →

The boundary of an oriented interval

Example

With the standard orientation on [a,b], the induced orientation of its boundary is ∂[a,b]={b}−{a}.

Facts & Assumptions

Given: Real numbers a<b, with [a,b] oriented by the positive tangent ∂x.

[L1]

Boundary orientation uses the outward-normal-first rule (Induced boundary orientation).

[L2]

The orientation obtained from that rule does not depend on the chosen outward vector (Boundary orientation is independent of the outward vector field).

Verification

technique · direct
1.1givenalgebra

The vectors +∂x at b and −∂x at a point out of the interval.

2.1givenL1L2step 1.1algebra∎

At b, the outward vector +∂x is positive, so [L1] gives the point b the positive orientation. At a, the outward vector −∂x is negative, so [L1] gives a the negative orientation; [L2] makes these conclusions independent of the particular outward vectors. Hence ∂[a,b]={b}−{a}.

ExampleConstruction: Literature-sourcedVerification: AI-generatedprecheck passaudited 2026-09-07Open item page →

The standard collar of a closed ball

Example

For n≥1, c:Sn−1×[0,ε)→Bn, c(u,t)=(1−t)u, is a collar for 0<ε<1.

Facts & Assumptions

Given: An integer n≥1, a real number 0<ε<1, the closed unit ball Bn, and the map c:Sn−1×[0,ε)→Bn defined by c(u,t)=(1−t)u.

[L1]

The boundary of Bn is Sn−1 (The closed ball and its sphere boundary).

[L2]

A smooth collar is a boundary-fixing smooth embedding whose image is an open neighbourhood of the boundary (Smooth collars of a manifold boundary).

Verification

technique · direct
1.1givenconstructalgebra

The map c is smooth and satisfies c(u,0)=u. Since 1−t>0, its inverse on its image is x⟼(x∣x∣,1−∣x∣), which is smooth; hence c is a smooth embedding.

2.1givenL1L2step 1.1algebra∎

Its image is {x∈Bn:∣x∣>1−ε}, which is open in Bn and contains Sn−1=∂Bn by [L1]. Consequently c satisfies every clause of [L2] and is a collar.

ExampleConstruction: Literature-sourcedVerification: AI-generatedprecheck passaudited 2026-09-07Open item page →

The double of a disk is a sphere

Example

For n≥1, the labelled double of Dn is diffeomorphic to Sn.

Facts & Assumptions

Given: An integer n≥1, the closed unit disk Dn=Bn, and its labelled double equipped with the seam charts induced by the standard radial collar.

[L1]

The labelled double identifies only corresponding boundary points of its two labelled copies (The double of a smooth manifold with boundary).

[L2]

Collar seam charts give the labelled double a smooth boundaryless structure compatible with both copies (The double has a well-defined smooth structure).

[L3]

The map c(u,t)=(1−t)u is a smooth collar of Bn (The standard collar of a closed ball).

Verification

technique · direct
1.1givenL1construct

For x≠0, write x=ru with 0<r≤1 and define F([x,±])=(sin⁡(πr/2)u, ±cos⁡(πr/2)), while F([0,±])=(0,…,0,±1). At r=1 both formulas give (u,0), so [L1] makes F well defined on the double.

2.1step 1.1algebra

On either disk the first component is sin⁡(π∣x∣/2)∣x∣x, with its value at x=0 defined by the smooth even power series, and the last component is ±cos⁡(π∣x∣/2), also a smooth function of ∣x∣2. Thus the restrictions are smooth at the two poles.

3.1L2L3step 1.1step 2.1∎

In the signed seam coordinate s, where x=(1−∣s∣)u and the sign of s records the label, [L2] and [L3] rewrite the map as F(u,s)=(cos⁡(πs/2)u, sin⁡(πs/2)). This is a smooth local diffeomorphism across s=0. The formula is bijective because the last coordinate selects the hemisphere and its absolute value determines r; its inverse is smooth in the pole charts and in these seam charts. Hence F is a diffeomorphism from the labelled double to Sn.

ExampleConstruction: Literature-sourcedVerification: AI-generatedprecheck passaudited 2026-09-07Open item page →

The Mobius band is nonorientable although its boundary circle is orientable

Example

The Möbius band is nonorientable, while its boundary circle is orientable independently.

Facts & Assumptions

Given: The standard smooth Möbius band B=[0,1]×[−1,1]/(0,s)∼(1,−s), equivalently the quotient of R×[−1,1] by the deck transformation g(t,s)=(t+1,−s), with quotient map q.

[L1]

An orientation is a smooth choice of a ray in each determinant line (Oriented smooth manifolds and oriented charts).

[L2]

A manifold is orientable exactly when it admits such an orientation (Orientable manifolds).

Verification

technique · direct
1.1givenL1L2algebra

Suppose B had an orientation. Pulling its determinant rays back by the local diffeomorphism q would orient the connected strip R×[−1,1]. Relative to the standard ray of (∂t,∂s), this continuous choice has one constant sign on the strip.

2.1givenL1L2step 1.1algebra

Since q∘g=q, the pulled-back orientation would have to be invariant under g. But Dg=diag⁡(1,−1) has determinant −1 and reverses every determinant ray, contradicting step 1.1. Hence B is nonorientable by [L2].

3.1givenL1step 2.1constructalgebra∎

The two boundary lines of the strip are exchanged by g, so their quotient is one component. The map t mod 2↦q(t,1) is a smooth bijection R/2Z→∂B with smooth inverse in the quotient charts. It identifies ∂B with a circle, whose positive t-direction supplies an orientation under [L1]. This orientation is chosen on the boundary itself and is not induced from the nonorientable band.

ExampleConstruction: Literature-sourcedVerification: AI-generatedprecheck passaudited 2026-09-07Open item page →

The product orientation on a torus

Example

The product orientation on S1×S1 is the ray of the ordered pair of positive tangent directions.

Facts & Assumptions

Given: Each factor S1 with its chosen orientation, positively oriented angular coordinates θ1 and θ2, and the factor order S1×S1.

[L1]

The product orientation is the tensor product of the two determinant rays under the ordered splitting of the tangent space (Product orientations).

[L2]

An oriented chart is one whose ordered coordinate frame lies in the selected determinant ray (Oriented smooth manifolds and oriented charts).

Verification

technique · direct
1.1givenL1algebra

At (p1,p2), the ordered tangent-space splitting is Tp1S1⊕Tp2S1. By [L1], the product ray is generated by placing a positive vector of the first factor before a positive vector of the second.

2.1givenL2step 1.1∎

The angular product chart has ordered frame (∂θ1,∂θ2), whose entries are positive in their respective circle factors. Step 1.1 and [L2] therefore identify its ray with the product orientation, which is the standard torus orientation for these chosen angular directions and factor order.

CounterexampleConstruction: Literature-sourcedVerification: AI-generatedprecheck passaudited 2026-09-07Open item page →

A submanifold meeting the ambient boundary nonneatly

Statement refuted

In M=[0,∞)×R, the embedded interval S={0}×[−1,1] is not neat.

Facts & Assumptions

Given: The standard manifold with boundary M=[0,∞)×R and the subset S={0}×[−1,1], supplied with the smooth structure transported from [−1,1] by s↦(0,s).

[L1]

An embedded submanifold with boundary is a subset carrying a manifold-with-boundary structure for which inclusion into the ambient manifold is a smooth embedding (Embedded smooth submanifolds with boundary).

[L2]

Neatness requires both S∩∂M=∂S and transversality to ∂M (Neat submanifolds of a manifold with boundary).

Counterexample

technique · direct
1.1givenL1constructalgebra

The parametrization [−1,1]→S, s↦(0,s), is a diffeomorphism onto S with its subspace topology, and its derivative v↦(0,v) is injective. Thus the inclusion is a smooth embedding, so [L1] makes S an embedded submanifold with boundary ∂S={(0,−1),(0,1)}.

2.1givenL2step 1.1algebra∎

Since ∂M={0}×R, one has S∩∂M=S, which is not the two-point set ∂S. The equality required by [L2] therefore fails, so S is not neat (independently of the transversality condition).

CounterexampleConstruction: Literature-sourcedVerification: AI-generatedprecheck passaudited 2026-09-07Open item page →

An inward field without a negative-time flow in the half-line

Statement refuted

On [0,∞), X=∂x is inward at 0 but has no negative-time flow through 0 staying in the half-line.

Facts & Assumptions

Given: The half-line M=[0,∞) with boundary point 0 and the constant smooth vector field X=∂x.

[L1]

In a boundary chart with half-space coordinate increasing into the manifold, a vector is inward exactly when its last coordinate is positive (Inward, outward, and boundary-tangent vectors).

Counterexample

technique · direct
1.1givenL1algebra

In the identity boundary chart on M, the vector X0=∂x has coordinate +1, so it is inward at 0 by [L1].

2.1givenstep 1.1algebra∎

Any integral curve through 0 must satisfy γ′(t)=1 and γ(0)=0, hence γ(t)=t. It lies in M for t≥0 but not for any t<0. Therefore no flow through 0 can be defined for negative time while remaining in the half-line.

ExampleConstruction: Literature-sourcedVerification: AI-generatedprecheck passaudited 2026-09-07Open item page →

Boundary orientation of the unit sphere by the outward normal

Example

For n≥1, the boundary orientation of Sn−1=∂Bn is the standard hypersurface orientation for which the radial outward normal is first.

Facts & Assumptions

Given: An integer n≥1, the closed unit ball Bn⊂Rn with the orientation induced by the standard ordered basis of Rn, and its boundary Sn−1.

[L1]

The induced boundary orientation is outward-normal-first (Induced boundary orientation).

[L2]

The boundary of Bn is Sn−1 (The closed ball and its sphere boundary).

[L3]

The standard oriented interval satisfies ∂[−1,1]={1}−{−1} (Boundary orientation is independent of the outward vector field).

Verification

technique · direct
1.1givenL2

At u∈Sn−1, the radial vector u points outward from Bn.

2.1givenL1L3step 1.1algebra∎

If n=1, then B1=[−1,1] and [L3] gives the positive determinant ray at 1 and the negative determinant ray at −1, exactly as the outward vectors 1 and −1 require under [L1]. If n≥2, a tangent basis (v1,…,vn−1) is positive precisely when (u,v1,…,vn−1) is positive in the standard orientation of Rn. Thus in every case the boundary orientation is the standard hypersurface orientation cooriented by the radial outward normal.

Sources