Registry · Lemma VI.L09 tau-effective planned

VI.L09 — BH Uniqueness Lemma

DecodeTarget selects unique element at every refinement level; follows from Israel-Carter-Robinson BH uniqueness theorem.

Book VI Part 7 Ch. 44

Dependency Graph

Depends on (2)

VI.D55 VI.D58

Depended on by (1)

VI.T30

Lean Formalization

Module: TauLib.BookVI.CosmicLife.BHSelfDesc

Symbol: Tau.BookVI.BHSelfDesc.BhUniquenessLemma