`IndisputableMonolith.Experimental.NeutronLifetimeDiscrepancyStructure`

IndisputableMonolith/Experimental/NeutronLifetimeDiscrepancyStructure.lean · 27 lines · 4 declarations

Explainer status: pending

   1import Mathlib
   2import IndisputableMonolith.Nuclear.NeutronLifetimeStructure
   3
   4namespace IndisputableMonolith
   5namespace Experimental
   6namespace NeutronLifetimeDiscrepancyStructure
   7
   8open Nuclear.NeutronLifetimeStructure
   9
  10theorem has_neutron_lifetime_input : neutron_lifetime_from_ledger :=
  11  neutron_lifetime_structure
  12
  13def neutron_lifetime_discrepancy_from_ledger : Prop := neutron_lifetime_from_ledger
  14
  15theorem neutron_lifetime_discrepancy_structure :
  16    neutron_lifetime_discrepancy_from_ledger := has_neutron_lifetime_input
  17
  18/-- Neutron-lifetime-discrepancy structure implies neutron-lifetime input. -/
  19theorem neutron_discrepancy_implies_lifetime_input
  20    (h : neutron_lifetime_discrepancy_from_ledger) :
  21    neutron_lifetime_from_ledger :=
  22  h
  23
  24end NeutronLifetimeDiscrepancyStructure
  25end Experimental
  26end IndisputableMonolith
  27

source mirrored from github.com/jonwashburn/shape-of-logic