Registry · Theorem IV.T125 tau-effective formalized

IV.T125 — Tick-Sector Bijection

Each tick kind maps to a distinct sector, establishing a 1-1 correspondence between ticks and sectors.

Book IV Part 2 Ch. 10

Dependency Graph

Depends on (2)

IV.D322 III.D13

Lean Formalization

Module: TauLib.BookIV.Physics.TickUnits

Symbol: Tau.BookIV.Physics.tick_sector_bijection