Registry · Definition I.D23 established formalized

I.D23 — Genealogical Decomposition (Spine)

Iterate the canonical peel along the remainder D to produce a finite sequence of ABC-triplets. X is recoverable by multiplying the corresponding tower atoms. Spine Cayley length ell_spine(x) = number of triplets.

Book I Part 4 Ch. 18

Dependency Graph

Depends on (2)

Depended on by (5)

Lean Formalization

Module: TauLib.BookI.Coordinates.NormalForm

Symbol: Tau.Coordinates.spine