`density`

definition

show as: view math explainer →

module: IndisputableMonolith.Physics.NeutronStarCrustalRegimesFromRS
domain: Physics
line: 28 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Physics.NeutronStarCrustalRegimesFromRS on GitHub at line 28.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

used by

formal source

  25
  26theorem nsRegime_count : Fintype.card NSRegime = 5 := by decide
  27
  28noncomputable def density (k : ℕ) : ℝ := phi ^ k
  29
  30theorem density_ratio (k : ℕ) : density (k + 1) / density k = phi := by
  31  unfold density
  32  have hpos : (0 : ℝ) < phi ^ k := pow_pos phi_pos k
  33  rw [div_eq_iff hpos.ne', pow_succ]
  34  ring
  35
  36theorem density_pos (k : ℕ) : 0 < density k := pow_pos phi_pos k
  37
  38structure NeutronStarCert where
  39  five_regimes : Fintype.card NSRegime = 5
  40  phi_ratio : ∀ k, density (k + 1) / density k = phi
  41  density_always_pos : ∀ k, 0 < density k
  42
  43noncomputable def neutronStarCert : NeutronStarCert where
  44  five_regimes := nsRegime_count
  45  phi_ratio := density_ratio
  46  density_always_pos := density_pos
  47
  48end IndisputableMonolith.Physics.NeutronStarCrustalRegimesFromRS

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.