Registry · Proposition V.P17 tau-effective formalized

V.P17 — G_tau well-defined --- V.P01

G_tau is well-defined: it is positive (gravity is attractive), independent of the choice of mature state (refinement coherence), and in orthodox units equals G = (c^3/hbar) iota_tau^2. The factor 2 in R_S = 2GM originates from the two lobes of L.

Book V Part 2 Ch. 16

Dependency Graph

Depends on (1)

Lean Formalization

Module: TauLib.BookV.GravityField.TauSchwarzschild

Symbol: Tau.BookV.GravityField.GtauWelldefinedVp01