Registry · Theorem II.T20 established formalized

II.T20 — R as Inverse Limit

The real numbers are recovered as the Archimedean inverse limit of primorial-scaled residues, with each coherent sequence determining a unique real via nested interval intersection.

Book II Part 5 Ch. 23

Dependency Graph

Depends on (6)

I.T04 I.T18 I.T35 II.D13 II.D14 II.D15

Depended on by (3)

II.D29 II.T21 II.T23

Lean Formalization

Module: TauLib.BookII.Transcendentals.Lines

Symbol: real_limit_check