Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 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 local mapping of complex squaring at zero and at one

Example

For f(z)=z2, the point 0 has local degree 2 and is a branch point: every sufficiently small nonzero value has two distinct nearby preimages. The point 1 has local degree 1, and f is biholomorphic on a sufficiently small neighbourhood of 1.

Facts & Assumptions

Given: The entire function f(z)=z2, the algebra of complex polynomial derivatives (Linearity, product, reciprocal, and quotient rules for complex derivatives), and the fact that a nonzero complex number has exactly two square roots (The n-th roots of a complex number and the n distinct roots of unity for every n1).

[L1]

If Ω is a complex domain, f:ΩC is nonconstant and holomorphic, and aΩ, then the local degree is degaf=orda(ff(a)) (Local degree of a nonconstant holomorphic map).

[L2]

If Ω is a complex domain, f:ΩC is nonconstant and holomorphic, aΩ, and m=degaf, then every neighbourhood N of a contains an open neighbourhood V for which some ρ>0 gives exactly m preimages in V for 0<wf(a)<ρm, while f(a) has only the preimage a, counted with multiplicity m (A local degree-m holomorphic map has m nearby sheets).

[L3]

If f is nonconstant and holomorphic on a complex domain Ω and aΩ, then f(a)0, degaf=1, local injectivity at a, and biholomorphy between neighbourhoods of a and f(a) are equivalent (Holomorphic inverse function theorem and local-degree criterion).

Verification

technique · direct
1.1

At 0, one has f(z)f(0)=z2, so [L1] gives deg0f=2. By [L2], every sufficiently small nonzero w has exactly two local preimages; explicitly they are the distinct roots z and z, while w=0 has only the preimage 0 with multiplicity 2.

L1L2givenalgebra
1.2

At 1, f(z)f(1)=(z1)(z+1) and the factor z+1 is nonzero at 1, so [L1] gives deg1f=1. Hence [L3] makes f biholomorphic between neighbourhoods of 1 and 1.

L1L3algebra
2.1

The injectivity can also be seen explicitly on D(1,1/2). If z,w lie in that disc and z2=w2, then z=w or z=w; the second alternative would give 2=(z1)+(w1)<1, which is impossible.

step 1.2algebra

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

23 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