Registry · Definition VI.D04 tau-effective planned

VI.D04 — τ-Distinction

Predicate D: X → 2_τ satisfying 5 conditions: clopen partition, refinement-coherent, eventually stable, law-stable, H_∂-equivariant. First of two Life predicates.

Book VI Part 1 Ch. 4

Dependency Graph

Depends on (1)

VI.T01

Depended on by (23)

VI.D08 VI.D10 VI.D21 VI.L02 VI.L05 VI.L08 VI.P02 VI.P06 VI.P12 VI.P18 VI.T02 VI.T04 VI.T08 VI.T09 VI.T10 VI.T11 VI.T12 VI.T13 VI.T14 VI.T15 VI.T26 VI.T28 VI.T34

Lean Formalization

Module: TauLib.BookVI.LifeCore.Distinction

Symbol: Tau.BookVI.Distinction.Distinction