No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
42theorem accel_mul_Tdyn_sq (v r : ℝ) (hv : v ≠ 0) (hr : r ≠ 0) :
43 accel v r * (Tdyn v r)^2 = 4 * (Real.pi ^ 2) * r := by
proof body
Term-mode proof.
44 unfold accel Tdyn
45 field_simp [hv, hr]
46 ring
47
48/-- Square of the characteristic time: \(T_0^2 = 4\pi^2 (r_0/a_0)\). -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (9)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
r_0
in IndisputableMonolith.Engineering.MarsAtmosphereJCostSchedule
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
T_0
in IndisputableMonolith.Gap45.SyncMinimization
decl_use
-
accel
in IndisputableMonolith.Gravity.ParameterizationBridge
decl_use
-
Tdyn
in IndisputableMonolith.Gravity.ParameterizationBridge
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use