structure definition def or abbrev

`RSBH`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  44structure RSBH where
  45  mass : ℝ
  46  mass_pos : mass > 0
  47
  48/-- Schwarzschild radius in RS-native units: r_s = 2GM. -/

From the project-wide theorem graph. These declarations reference this one in their body.

entropy_quadruples_on_double in IndisputableMonolith.Gravity.UltramassiveBH decl_use
horizonArea in IndisputableMonolith.Gravity.UltramassiveBH decl_use
horizonCells in IndisputableMonolith.Gravity.UltramassiveBH decl_use
rs_entropy in IndisputableMonolith.Gravity.UltramassiveBH decl_use
rs_entropy_eq in IndisputableMonolith.Gravity.UltramassiveBH decl_use
rs_entropy_pos in IndisputableMonolith.Gravity.UltramassiveBH decl_use
rs_hawkingTemp in IndisputableMonolith.Gravity.UltramassiveBH decl_use
rs_hawkingTemp_pos in IndisputableMonolith.Gravity.UltramassiveBH decl_use
schwarzschildRadius in IndisputableMonolith.Gravity.UltramassiveBH decl_use
temp_decreases_with_mass in IndisputableMonolith.Gravity.UltramassiveBH decl_use
temp_halves_on_double in IndisputableMonolith.Gravity.UltramassiveBH decl_use
UltramassiveBHCert in IndisputableMonolith.Gravity.UltramassiveBH decl_use

Lean names referenced from this declaration's body.

radius in IndisputableMonolith.Complexity.CellularAutomata decl_use
mass_pos in IndisputableMonolith.Physics.MesonSpectrumFromPhiLadder decl_use