CounterexampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedprecheck pass

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.

A map with two preimages but degree zero

Statement refuted

The unsigned number of points in a regular fibre need not equal the degree. The smooth proper map $F : S^{1} \to S^{1}$ given by $F (e^{i θ}) = e^{i \sin θ}$ has the regular value $1$ with exactly two preimages and opposite local signs, hence degree zero.

Facts & Assumptions

Given: Both circles have their counterclockwise orientations.

[F1]

$[t] \mapsto (\cos 2 π t, \sin 2 π t)$ is a homeomorphism from $R / Z$ to the unit circle identifies the quotient coordinate $[t] \in R / Z$ with $e^{2 π i t}$ .

[F2]

The zero sets of sine and cosine and the least positive common period 2 pi, Parity and the Pythagorean identity for sine and cosine, Sine is positive and cosine is strictly decreasing on (0,2), with cos 2 at most -1/3, and Pi is the first positive zero of sine give the $2 π$ -periodicity and zero set of sine, the bound $∣ \sin θ ∣ \leq 1$ , and $π > 2$ .

[F3]

The derivatives of sine and cosine are cosine and minus sine, The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ , and Quarter-turn values and shifts by pi/2 and pi give $(\sin θ)^{'} = \cos θ$ , $\cos 0 = 1$ , and $\cos π = - 1$ .

[F4]

$R / Z$ is compact and path-connected and $R / Z$ is Hausdorff make the quotient circle compact Hausdorff. In a Hausdorff space compact subsets are closed by In a Hausdorff space a point and a disjoint compact set, and two disjoint compact sets, have disjoint open neighbourhoods; hence every compact subset is closed, and in a compact Hausdorff space the compact subsets are exactly the closed ones, and closed subsets of a compact space are compact by A closed subspace of a compact space is compact, and a finite union of compact subspaces is compact.

[F5]

Regular-value formula for compact-support degree computes degree as the signed sum over any supplied regular fibre.

Counterexample

1.1F1F2F3F4given

Under [F1] the displayed map is $G ([t]) = [\frac{\sin (2 π t)}{2 π}] .$ It is well defined because replacing $t$ by an integer translate does not change the sine by [F2]. In local increasing angular coordinates its lifts differ only by integer constants and have derivative $\cos (2 π t)$ by [F3]; repeated differentiation cycles through sine and cosine, so $G$ is smooth. If $K$ is compact in the target, [F4] makes $K$ closed, hence $G^{- 1} (K)$ closed in the compact source and therefore compact. Thus $G$ , equivalently $F$ , is proper.

2.1F2F3F5step 1.1algebra

The fibre of $[0]$ , corresponding to $1 \in S^{1}$ , satisfies $\sin (2 π t) \in 2 π Z$ . Since $∣ \sin (2 π t) ∣ \leq 1 < 2 π$ by [F2], this is equivalent to $\sin (2 π t) = 0$ . The zero-set formula in [F2] gives exactly $[t] = [0]$ or $[t] = [1 / 2]$ . By [F3] their derivatives are respectively $+ 1$ and $- 1$ , so $[0]$ is regular and [F5] gives $\deg (F) = (+ 1) + (- 1) = 0,$ although this fibre has two points.

3.1F2F3F5step 1.1step 2.1∎

This witnesses the failed unsigned-count conclusion. For comparison, the target value $[1 / 2]$ has empty fibre because every lifted value of $G$ has absolute value at most $1 / (2 π) < 1 / 2$ , and the empty regular-fibre sum again gives zero. The extreme target $[1 / (2 π)]$ has the singleton preimage $[1 / 4]$ , but its derivative is $\cos (π / 2) = 0$ , so it is critical rather than a counterexample to the regular-value formula. Quotient seams are handled by local lifts, and every fibre point used above is explicitly listed; no choice principle is used.

Remarks

The schematic marks the regular fibre over $1$ : the right and left source points have local signs $+ 1$ and $- 1$ , respectively (step 2.1). Both circles are oriented counterclockwise. The thick target arc is the image ${e^{i u} : - 1 \leq u \leq 1}$ , not the whole target circle, since $u = \sin θ$ . The arrow denotes $F$ ; both marked source points map to the marked target point. The proof above is independent of the illustration.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

60 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

Robbin–Salamon, Introduction to Differential Topology, Theorem 5.4.1, pp.191–192 (standard reference, not scraped)