def definition def or abbrev

`omega_0`

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

formal statement (Lean)

  32def omega_0 : ℝ := 1

proof body

Definition body.

used by (16)

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

AsteroidOreSpectroscopyCert in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
omega_0_pos in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
peakFrequency in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
peakFrequency_zero in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
HydrideSCOptimizationCert in IndisputableMonolith.Materials.HydrideSCOptimization decl_use
hydride_sc_optimization_one_statement in IndisputableMonolith.Materials.HydrideSCOptimization decl_use
phi_ladder_optimization_collapses in IndisputableMonolith.Materials.HydrideSCOptimization decl_use
T_c_optimization_finite_search in IndisputableMonolith.Materials.HydrideSCOptimization decl_use
T_c_phi_rung in IndisputableMonolith.Materials.HydrideSCOptimization decl_use
phi_ladder_phonon_one_statement in IndisputableMonolith.Materials.PhiLadderPhononResonance decl_use
PhiLadderPhononResonanceCert in IndisputableMonolith.Materials.PhiLadderPhononResonance decl_use
phonon_rung in IndisputableMonolith.Materials.PhiLadderPhononResonance decl_use
phonon_rung_pos in IndisputableMonolith.Materials.PhiLadderPhononResonance decl_use
phonon_rung_ratio_adjacent in IndisputableMonolith.Materials.PhiLadderPhononResonance decl_use
phonon_rung_strictly_increasing in IndisputableMonolith.Materials.PhiLadderPhononResonance decl_use
phonon_rung_succ in IndisputableMonolith.Materials.PhiLadderPhononResonance decl_use