Registry · Definition I.D28 established formalized

I.D28 — Boundary Local Ring

Ring structure on omega-tails from primorial inverse limit. CRT factors Z/M_k into B-prime and C-prime contributions. Earned ring operations on boundary data.

Book I Part 7 Ch. 30

Dependency Graph

Depends on (1)

Depended on by (3)

Lean Formalization

Module: TauLib.BookI.Polarity.BipolarAlgebra

Symbol: Tau.Polarity.bdry_add