Alphabeta Math
LemmaStatement: Literature-sourcedProof: 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.

Oriented boundary counts of a compact oriented 1-manifold cancel

Statement

Assume ACω. Let W be a compact oriented smooth 1-manifold and give ∂W the outward-normal-first orientation (Induced boundary orientation). The boundary is a finite 0-manifold, so its orientation at a boundary point p is a sign ε(p)∈{+1,−1}; then ∑p∈∂Wε(p)=0. On each closed-interval component the two boundary points carry opposite signs; circle components contribute nothing. With the standard orientation of [a,b] the outward-normal-first convention gives ∂[a,b]={b}−{a}.

Facts & Assumptions

Given: A compact oriented smooth 1-manifold W and its outward-normal-first boundary orientation.

[F1]

W is diffeomorphic to a finite disjoint union of circles S1 and closed intervals [a,b], so ∂W is finite; that classification is established under ACω (it fixes a Riemannian metric), and this lemma inherits ACω and adds no further choice (Boundary of a compact 1-manifold has even cardinality, The Axiom of Countable Choice (ACω)).

[F2]

The outward-normal-first rule orients Tp∂W: an outward vector first, followed by a positive boundary determinant, is a positive determinant of TpW; for a 1-manifold this assigns to a boundary point the sign +1 when the positive tangent direction points outward and −1 when it points inward, and the result is independent of the chosen outward vector field (Induced boundary orientation, Boundary orientation is independent of the outward vector field).

[F3]

An orientation of a manifold is a smooth choice of ray in each determinant line, and a 0-manifold carries one sign per point (Oriented smooth manifolds and oriented charts, Determinant-line orientations of finite-dimensional real vector spaces).

Proof

technique · direct, by computing the model components
1.1F2F3algebra

A circle contributes no boundary points. On [a,b] with a<b and positive tangent direction ∂t, the outward vector is +∂t at b and −∂t at a. The outward-normal-first determinant rule gives the point signs +1 at b and −1 at a, so ∂[a,b]={b}−{a} and their sum is zero. Reversing the interval orientation reverses both point signs and preserves their cancellation.

2.1F1step 1.1algebra∎

By [F1] write W as a finite disjoint union of such model components. The given orientation of W restricts to an orientation of each component, and the outward-normal-first boundary orientation is computed componentwise, because a boundary point lies in exactly one component and the outward vectors of the component and of W agree there. Adding the finitely many contributions of 1.1 gives ∑p∈∂Wε(p)=0; a circle component contributes no boundary point, an interval component contributes exactly +1 and −1, and the empty manifold contributes nothing.

Depends on

Used by

Dependency tree · two levels

26 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