Registry · Theorem II.T51 tau-effective formalized

II.T51 — Flat Curvature Vanishing

The canonical flat connection has zero curvature at every finite stage. R = 0 because addition in Z/M_k Z is commutative. Verified at stages 1-2.

Book II Part 10 Ch. 55

Dependency Graph

Depends on (2)

Lean Formalization

Module: TauLib.BookII.Closure.Curvature

Symbol: flat_curvature_vanishes_2