Registry · Theorem II.T50 tau-effective formalized

II.T50 — Flat Connection Existence

The additive connection Γ_k(x,v) = (x+v) mod M_k is flat: parallel transport around any closed loop returns to the starting point. Verified computationally at stages 1-2.

Book II Part 10 Ch. 55

Dependency Graph

Depends on (2)

II.D78 II.D62

Depended on by (3)

II.P16 II.T51 II.T52

Lean Formalization

Module: TauLib.BookII.Closure.Connection

Symbol: flat_connection_flat_2