Registry · Lemma V.L4 tau-effective formalized

V.L4 — Single Scale Degree of Freedom

tau-Schwarzschild has exactly one free scale parameter (linking mass M); all other quantities determined by M through iota_tau.

Book V Part 2 Ch. 16

Dependency Graph

Depends on (2)

Lean Formalization

Module: TauLib.BookV.GravityField.TauSchwarzschildScale

Symbol: Tau.BookV.GravityField.single_scale_dof