Registry · Proposition V.P146 tau-effective formalized

V.P146 — AQUAL as Projection

AQUAL as Projection (circular orbits): from two-channel g² = g_N² + g_N·a₀, define μ = g_N/g → μ_2ch(x) = √(x/(1+x)). For spherical symmetry, AQUAL PDE ∇·[μ·∇Φ] = 4πGρ is algebraically equivalent. Nonlinearity appears upon projecting out fiber T². General non-spherical PDE form remains open.

Book V Part 5 Ch. 37

Dependency Graph

Depends on (2)

Lean Formalization

Module: TauLib.BookV.Astrophysics.RotationCurves

Symbol: Tau.BookV.Astrophysics.aqual_as_projection