def definition def or abbrev

`lifetime`

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

formal statement (Lean)

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

proof body

Definition body.

used by (19)

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

neutron_lifetime_discrepancy_structure in IndisputableMonolith.Experimental.NeutronLifetimeDiscrepancyStructure decl_use
neutron_decay_allowed in IndisputableMonolith.Nuclear.NeutronLifetimeStructure decl_use
neutron_decay_phase_space_positive in IndisputableMonolith.Nuclear.NeutronLifetimeStructure decl_use
neutronDecayQ in IndisputableMonolith.Nuclear.NeutronLifetimeStructure decl_use
neutron_lifetime_implies_decay_allowed in IndisputableMonolith.Nuclear.NeutronLifetimeStructure decl_use
neutron_lifetime_implies_positive_lifetime in IndisputableMonolith.Nuclear.NeutronLifetimeStructure decl_use
neutron_lifetime_structure in IndisputableMonolith.Nuclear.NeutronLifetimeStructure decl_use
DecaySpectrumCert in IndisputableMonolith.Physics.DecaySpectrumFromPhiLadder decl_use
lifetime_pos in IndisputableMonolith.Physics.DecaySpectrumFromPhiLadder decl_use
lifetime_ratio in IndisputableMonolith.Physics.DecaySpectrumFromPhiLadder decl_use
kLkS_massDifference in IndisputableMonolith.Physics.KaonMasses decl_use
kLongLifetime in IndisputableMonolith.Physics.KaonMasses decl_use
chiralAnomalyConsequences in IndisputableMonolith.QFT.Anomalies decl_use
half_cycle_phase in IndisputableMonolith.QFT.Anomalies decl_use
pi0_error_simplified in IndisputableMonolith.QFT.Anomalies decl_use
pi0_lifetime_predicted_units in IndisputableMonolith.QFT.Anomalies decl_use
rsAnomalySummary in IndisputableMonolith.QFT.Anomalies decl_use
cpt_lifetime_equality in IndisputableMonolith.QFT.CPTInvariance decl_use
MetastableState in IndisputableMonolith.Thermodynamics.PhaseTransitions decl_use