Registry · Proposition III.P37 established formalized

III.P37 — Boundary Restriction

Reduction from stage k+1 to k corresponds to boundary restriction in the projective limit. Fiber over point x at stage k has exactly p_{k+1} preimages. Verified at depth 3.

Book III Part 10 Ch. 81

Dependency Graph

Depends on (1)

III.T60

Depended on by (2)

III.D91 III.T61

Lean Formalization

Module: TauLib.BookIII.Bridge.TranslationTopo

Symbol: boundary_restriction_3