def definition def or abbrev

`density`

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

formal statement (Lean)

  28noncomputable def density (k : ℕ) : ℝ := phi ^ k

proof body

Definition body.

used by (40)

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

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
phi_ladder_step in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
co_highest_curie in IndisputableMonolith.Chemistry.Ferromagnetism decl_use
domainWallWidth in IndisputableMonolith.Chemistry.Ferromagnetism decl_use
freeElectrons in IndisputableMonolith.Chemistry.MetallicBond decl_use
phi_critical_numeric in IndisputableMonolith.CondensedMatter.JCostPhaseTransition decl_use
darkEnergyDensity in IndisputableMonolith.Cosmology.CosmologicalConstant decl_use
lambda_observed in IndisputableMonolith.Cosmology.CosmologicalConstant decl_use
phiLadderSum in IndisputableMonolith.Cosmology.CosmologicalConstant decl_use
criticalDensity in IndisputableMonolith.Cosmology.DarkEnergy decl_use
dark_energy_dominates in IndisputableMonolith.Cosmology.DarkEnergy decl_use
dark_energy_eos in IndisputableMonolith.Cosmology.DarkEnergy decl_use
entryDensity in IndisputableMonolith.Cosmology.DarkEnergy decl_use
expansionTension in IndisputableMonolith.Cosmology.DarkEnergy decl_use
isBalanced in IndisputableMonolith.Cosmology.DarkEnergy decl_use
lambda_positive in IndisputableMonolith.Cosmology.DarkEnergy decl_use
omegaLambda in IndisputableMonolith.Cosmology.DarkEnergy decl_use
equation_of_state in IndisputableMonolith.Cosmology.DarkEnergyEOS decl_use
phase_locked_energy_constant in IndisputableMonolith.Cosmology.DarkEnergyEOS decl_use
Axion in IndisputableMonolith.Cosmology.DarkMatter decl_use
omega_dm in IndisputableMonolith.Cosmology.DarkMatter decl_use
cosmological_constant_resolution in IndisputableMonolith.Cosmology.EarlyUniverse decl_use
initial_state_is_zero_defect in IndisputableMonolith.Cosmology.EarlyUniverse decl_use
omega_lambda_lt_one in IndisputableMonolith.Cosmology.EarlyUniverse decl_use
flat_minimizes_cost in IndisputableMonolith.Cosmology.FlatnessProblem decl_use
implications in IndisputableMonolith.Cosmology.FlatnessProblem decl_use
omega_observed in IndisputableMonolith.Cosmology.FlatnessProblem decl_use
phi_cosmology_relations in IndisputableMonolith.Cosmology.FlatnessProblem decl_use
btfrData in IndisputableMonolith.Cosmology.GalaxyRotation decl_use
coreCuspProblem in IndisputableMonolith.Cosmology.GalaxyRotation decl_use

… and 10 more