LemmaStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24

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 normalized large-radius loop of a monic degree- $n$ polynomial has degree $n$

Statement

Let $p (z) = z^{n} + \sum_{j < n} a_{j} z^{j}$ be a monic complex polynomial of degree $n \geq 1$ , and put $S = \sum_{j < n} ∣ a_{j} ∣$ . If $R > \max {1, S}$ , then the based normalized circle loop

$α_{R} (u) = h^{- 1} (\frac{p (R h (u)) / p (R)}{∣ p (R h (u)) / p (R) ∣}), u \in R / Z,$

is well defined and has degree $n$ .

Facts & Assumptions

Given: A monic polynomial $p (z) = z^{n} + \sum_{j < n} a_{j} z^{j}$ of degree $n \geq 1$ , the number $S = \sum_{j < n} ∣ a_{j} ∣$ , and a real $R > \max {1, S}$ .

[F1]

For a nonzero complex polynomial, degree is the final coefficient index and monic means that its leading coefficient is $1$ (Formal complex polynomials, evaluation, degree, leading coefficient, and monic polynomials).

[L1]

Complex modulus is multiplicative and satisfies the triangle inequality (Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive).

[L2]

The homeomorphism $h : R / Z \to S^{1}$ sends $[0]$ to $1 \in S^{1}$ ( $[t] \mapsto (\cos 2 π t, \sin 2 π t)$ is a homeomorphism from $R / Z$ to the unit circle).

[L3]

Maps into finite products are continuous exactly when their components are continuous; finite sums, products, and quotients of continuous real-valued maps are continuous wherever the denominator is nonzero (A map into a product is continuous iff each of its components is; the projections are continuous and open; and each projection is surjective when every factor is nonempty, which for an infinite index set uses the Axiom of Choice, A vector-valued function has a limit, or is continuous, if and only if each of its components does; with the algebra of continuous vector-valued functions, Sums, products, absolute values, finite maxima and minima, and quotients of continuous real-valued maps on a topological space are continuous where defined).

[L4]

Path-homotopic based circle loops have the same degree (Path-homotopic based circle loops have the same degree).

[L5]

The standard loop $ω_{m}$ has degree $m$ for every integer $m$ ( $\deg (ω_{n}) = n$ for every integer $n$ ).

Proof

technique · constructive

1.1

If $∣ z ∣ = R$ , then $∣ \sum_{j < n} a_{j} z^{j} ∣ \leq \sum_{j < n} ∣ a_{j} ∣ R^{j} \leq S R^{n - 1} < R^{n} = ∣ z^{n} ∣ .$ The estimate includes $n = 1$ and $S = 0$ , since $R > 1$ and $S < R$ .

givenF1L1algebra

2.1

For $s \in [0, 1]$ put $p_{s} (z) = z^{n} + s \sum_{j < n} a_{j} z^{j}$ . Step 1.1 remains strict with $s S \leq S$ , so $p_{s}$ never vanishes on $∣ z ∣ = R$ , in particular $p_{s} (R) \neq 0$ . The formula $H (s, u) = h^{- 1} (\frac{p_{s} (R h (u)) / p_{s} (R)}{∣ p_{s} (R h (u)) / p_{s} (R) ∣})$ is therefore a continuous based homotopy by [L2] and [L3]. At $s = 1$ it is $α_{R}$ , while at $s = 0$ it is $u \mapsto h^{- 1} (h (u)^{n}) = ω_{n} (u)$ .

step 1.1L1L2L3construct

3.1

Homotopy invariance and the standard-loop calculation give $\deg (α_{R}) = \deg (ω_{n}) = n$ .

step 2.1L4L5discharge-construct∎

Depends on

Used by

Dependency tree · two levels

70 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

Allen Hatcher, Algebraic Topology, proof of Theorem 1.8 (standard reference, not scraped)
J. Peter May, A Concise Course in Algebraic Topology, Chapter 1, §7 (standard reference, not scraped)

The normalized large-radius loop of a monic degree-nn polynomial has degree nn