Registry · Definition III.D90 established formalized

III.D90 — Dimension Recovery

Primorial depth k = intrinsic dimension. Z/M_k Z has k independent prime coordinates (by CRT), giving k-torus T^k = Π Z/p_i Z. dim = k at every stage.

Book III Part 10 Ch. 81

Dependency Graph

Depends on (1)

Depended on by (1)

Lean Formalization

Module: TauLib.BookIII.Bridge.TranslationTopo

Symbol: crt_dimension