LemmaStatement: AI-adaptedProof: AI-generatedPipeline-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.

Complex modulus restricts to real absolute value

Statement

For every real $r$ , write $λ_{r}$ for its canonical image in $C$ . Then

∣ λ_{r} ∣_{C} = ∣ r ∣_{R} .

Facts & Assumptions

Given: A real number $r$ and the complex modulus and real absolute value in the cited definitions. Write $λ_{r}$ for its constant-class image in $C$ .

[F1]

The canonical real embedding sends $r$ to its constant class in $C$ (The complex numbers as $R [x] / (x^{2} + 1)$ , with the real embedding and imaginary unit $i$ ).

[F2]

The imaginary unit $i$ is the class of the polynomial $x$ in $C = R [x] / (x^{2} + 1)$ (The complex numbers as $R [x] / (x^{2} + 1)$ , with the real embedding and imaginary unit $i$ ).

[F3]

Every complex number has unique real coordinates $a + b i$ (Real and imaginary parts, complex conjugation, and modulus).

[F4]

The complex modulus is $∣ a + b i ∣_{C} = \sqrt{a^{2} + b^{2}}$ (Real and imaginary parts, complex conjugation, and modulus).

[F5]

Real absolute value is nonnegative and equals $r$ when $r \geq 0$ and $- r$ when $r < 0$ (Absolute value in an ordered field, Basic properties of the absolute value).

[F6]

If $r \neq 0$ , then $r^{2} > 0$ (Squares of nonzero elements are positive); if $r = 0$ , then $r^{2} = 0$ by $0 \cdot a = 0$ in a field (Multiplication by zero: $0 \cdot a = 0$ ).

[F7]

Every nonnegative real has a unique nonnegative square root (Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ ).

Proof

1.1F1F2F3algebra

The canonical image of $r$ is the class of the constant polynomial $r$ by [F1]. Since $i$ is the class of $x$ by [F2], this is also the class of $r + 0 x$ , namely $r + 0 i$ . Uniqueness of complex coordinates in [F3] identifies that image with $r + 0 i$ .

1.2F6F7cases

If $r = 0$ then $r^{2} = 0$ , and if $r \neq 0$ then [F6] gives $r^{2} > 0$ . Thus $r^{2} \geq 0$ in either case, so [F7] guarantees that its nonnegative square root exists.

1.3F5algebra

By [F5], $∣ r ∣_{R} \geq 0$ . If $r \geq 0$ , then $∣ r ∣ = r$ ; if $r < 0$ , then $∣ r ∣ = - r$ . In either case $∣ r ∣_{R}^{2} = r^{2}$ , including $r = 0$ .

2.1F4step 1.1step 1.2algebra

By [F4] and step 1.1, the modulus of the canonical image of $r$ is $\sqrt{r^{2} + 0^{2}} = \sqrt{r^{2}}$ , whose radicand is nonnegative by step 1.2.

3.1F7step 2.1step 1.3∎

Step 2.1 and step 1.3 identify the complex modulus of the canonical image of $r$ and $∣ r ∣_{R}$ as nonnegative square roots of the same $r^{2}$ . By uniqueness in [F7], they are equal.

Depends on

Used by

Dependency tree · two levels

19 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

Tomasz Kochanek, Functional analysis, Lecture 1 (complete five-page lecture notes) (standard reference, not scraped)
M. Winklmeier, Functional Analysis lecture notes (complete 140-page lecture notes) (standard reference, not scraped)