Local Precision Unit

Abstract

The prime’s p-adic norm fixes its real logarithmic precision unit.

Theorem 1.1 (The logarithmic unit is unique).

$$\forall p:\mathbb{N},\mathrm{Fact}(p.Prime)\Rightarrow (\exp (-\mathrm{precisionLength}(p))=\Vert p{\Vert }_p\wedge \mathrm{precisionLength}(p)=\log (p)\wedge \forall ell:\mathbb{R},\exp (-ell)=\Vert p{\Vert }_p\Rightarrow ell=\mathrm{precisionLength}(p))\wedge \forall s:\mathbb{R},p^{-s}=\exp (-s\times \log (p)).$$

Proof. Machine-checked in Lean as D5/S3/AnalyticClosure/LocalPrecisionUnit.local_precision_unit (✓ std3). ∎

Source. Repository-derived.

Commentary.

For a prime p, precisionLength is the source logarithmic length constructed from the canonical p-adic norm. Its exponential weight equals the norm of p, the value is log p, and no other real length has that weight.

The final clause rewrites the real power p^(-s) as the exponential of -s log p for every real s.

References

• Truth anchor: D5/S3/AnalyticClosure/LocalPrecisionUnit.local_precision_unit