Registry · Definition V.D67 tau-effective formalized

V.D67 — Equilibrium carrier

An equilibrium carrier is a boundary character chi satisfying the spherical carrier predicate Sph(chi), the stationarity condition rho(chi|_{tau^1}) = chi|_{tau^1} (no evolution along the alpha-orbit), and the tau-Einstein identity.

Book V Part 2 Ch. 17

Dependency Graph

Depends on (1)

Depended on by (4)

Lean Formalization

Module: TauLib.BookV.GravityField.TOVStarBuilder

Symbol: Tau.BookV.GravityField.EquilibriumCarrier