Registry · Definition I.D17 established formalized

I.D17 — ABCD Coordinate Chart

Canonical coordinate chart Phi(x) = (A,B,C,D) via greedy peel-off; four typed coordinate functions (coord_pi, coord_gamma, coord_eta, coord_alpha).

Book I Part 4 Ch. 19

Dependency Graph

Depends on (1)

I.D16

Depended on by (18)

I.D19e I.D24 I.P08 I.P46 I.R38 I.R39 I.T04 II.D02 II.D03 II.D04 II.D05 II.D06 II.D18a II.D18b II.P03 II.R04 II.R06a V.D12

Lean Formalization

Module: TauLib.BookI.Coordinates.ABCD

Symbol: Tau.Coordinates.abcd_chart