Incorrect use of "power series" in documentation for `normPowerSeries`

⚠️ Found by a local LLM, not a human. This was flagged by an automated documentation-mistake finder (qwen3:14b) and passed 10/10 independent verification runs before filing, but it has not been reviewed by a person. Please check it's a genuine error before acting on it.

Summary

The documentation in Physlib/SpaceAndTime/Space/Norm/Basic.lean (around line 15) is incorrect.

Current text

## i. Overview

The main content of this file is defining `Space.normPowerSeries`, a power series which is
differentiable everywhere, and which tends to the norm in the limit as `n → ∞`.

Why this is wrong

The file claims that Space.normPowerSeries is a power series, but its definition as sqrt(‖x‖^2 + 1/(n+1)) does not match the mathematical definition of a power series (which is a sum of terms $a_k x^k$). The reviewer correctly notes this is a sequence of functions, not a power series.

The correction accurately describes it as a sequence of functions that converges to the norm. This aligns with the implementation, which defines normPowerSeries as a function depending on n but does not involve any summation over powers of ‖x‖. The term "power series" was misleading and has been appropriately replaced.

Suggested correction

## i. Overview

The main content of this file is defining `Space.normPowerSeries`, a sequence of functions which is differentiable everywhere, and which tends to the norm in the limit as `n → ∞`.

Open Physlib/SpaceAndTime/Space/Norm/Basic.lean around lines 15–18 and compare the overview with the definition of Space.normPowerSeries. Update the documentation so it describes a sequence of functions rather than a power series. Done means the overview accurately matches the implementation and no longer uses the misleading term.