theorem proved term proof

`neutron_lifetime_structure`

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

formal statement (Lean)

  45theorem neutron_lifetime_structure : neutron_lifetime_from_ledger := by

Term-mode proof.

  46  exact ⟨neutron_decay_allowed, neutron_lifetime_positive⟩
  47
  48/-- The ledger neutron-lifetime structure implies positive decay Q-value. -/

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

has_neutron_lifetime_input in IndisputableMonolith.Experimental.NeutronLifetimeDiscrepancyStructure decl_use

Lean names referenced from this declaration's body.

neutron_decay_allowed in IndisputableMonolith.Nuclear.NeutronLifetimeStructure decl_use
neutron_lifetime_from_ledger in IndisputableMonolith.Nuclear.NeutronLifetimeStructure decl_use
neutron_lifetime_positive in IndisputableMonolith.Nuclear.NeutronLifetimeStructure decl_use
lifetime in IndisputableMonolith.Physics.DecaySpectrumFromPhiLadder decl_use
value in IndisputableMonolith.QFT.SpinStatistics decl_use