Registry · Definition II.D49 established formalized

II.D49 — Tau-Regularity

A point p is tau-regular for f if the omega-germ sequence stabilizes at a finite primorial stage. A constructive, positive criterion: existence of stabilization, not absence of pathology.

Book II Part 7 Ch. 39

Dependency Graph

Depends on (5)

II.D37 II.D10 II.L07 II.T33 I.T31

Depended on by (6)

II.D53 II.D54 II.P10 II.R11 II.T34 II.T37

Lean Formalization

Module: TauLib.BookII.Regularity.PositiveRegularity

Symbol: is_regular