Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: Literature-sourcedPipeline-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 degenerate isolated fixed point with nonzero local index

Example

Assume AC (The Axiom of Choice). The polynomial f(z)=z+z2 defines a smooth self-map of the Riemann sphere S2=C∪{∞} whose fixed points are exactly 0 and ∞. The fixed point 0 is isolated but degenerate: Df0=I and I−Df0=0 is not invertible (Isolated fixed points need not be nondegenerate). Nevertheless its local index is defined and equals 2 (Isolated fixed point and local fixed point index), and the index of the second fixed point, ∞, is +1; the index sum is I(f)=2+1=3=L(f), in agreement with the Lefschetz–Hopf formula Lefschetz-Hopf index formula and with the degree computation L(f)=1+deg⁡f=1+2=3 for a self-map of S2 of degree 2 (Algebraic Lefschetz number via rational homology traces, Homology of spheres).

Verification

Given: The map f(z)=z+z2 on C, extended to S2 by f(∞)=∞.

[F1] The fixed point 0 is isolated and degenerate, with ind⁡0(f)=2 (Isolated fixed points need not be nondegenerate, Isolated fixed point and local fixed point index); at ∞ the chart w=1/z turns f into w↦w2/(w+1) with displacement w/(w+1), which vanishes only at w=0 with invertible linear part 1, so ind⁡∞(f)=+1 (The index of a nondegenerate fixed point is the sign of det(I-Df)).

[F2] H∗(S2;Q) is Q in degrees 0,2 and zero otherwise; a self-map of S2 of degree d has L=1+d (Homology of spheres, Algebraic Lefschetz number via rational homology traces, Degree of a self map of an oriented sphere).

1.1givenF1

The indices. The fixed point equation on C is z2=0, so 0 is the only finite fixed point and it is isolated; in the chart w=1/z at infinity, the fixed point equation is w2/(w+1)=w, i.e. w=0, so ∞ is the other fixed point. By [F1] the two indices are 2 and +1, so the geometric Lefschetz number is I(f)=2+1=3; the point 0 is degenerate, so the determinant formula The index of a nondegenerate fixed point is the sign of det(I-Df) does not apply to it, and the value 2 comes from the explicit degree computation of the displacement −z2 on a small circle.

2.1step 1.1F2∎

The Lefschetz number agrees. The expression w↦w2/(w+1) is smooth near infinity, so the polynomial extends smoothly. The finite value 1 has exactly two distinct preimages solving z2+z=1, namely (−1±5)/2; at each the derivative is nonzero complex multiplication by 1+2z, of positive real determinant. Infinity maps to infinity and is not a preimage of 1. Hence 1 is a regular value and Regular-value formula for degree gives degree 2, so by [F2] L(f)=1+2=3. Hence I(f)=3=L(f) even though the fixed point at 0 is degenerate: the index formula holds for isolated fixed points and does not require nondegeneracy, which is exactly the content of Lefschetz-Hopf index formula.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

67 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