Registry · Theorem II.T52 tau-effective formalized

II.T52 — Lemniscate Holonomy

The profinite limit acquires nontrivial holonomy from π₁(L) ≅ ℤ. The generator maps to the unit shift x ↦ x+1 mod M_k, which has order M_k at stage k.

Book II Part 10 Ch. 55

Dependency Graph

Depends on (2)

II.P16 II.T50

Lean Formalization

Module: TauLib.BookII.Closure.Curvature

Symbol: lemniscate_holonomy_2