WeakDecayType

formal source

  19namespace IndisputableMonolith.Physics.WeakNuclearForceFromRS
  20open Constants
  21
  22inductive WeakDecayType where
  23  | betaMinus | betaPlus | electronCapture | muonDecay | tauDecay
  24  deriving DecidableEq, Repr, BEq, Fintype
  25
  26theorem weakDecayCount : Fintype.card WeakDecayType = 5 := by decide
  27
  28/-- φ^10 = 55φ + 34 (Fibonacci). -/
  29theorem phi10_fibonacci : phi ^ 10 = 55 * phi + 34 := by
  30  have h2 := phi_sq_eq
  31  have h3 : phi ^ 3 = 2 * phi + 1 := by nlinarith
  32  have h4 : phi ^ 4 = 3 * phi + 2 := by nlinarith
  33  have h5 : phi ^ 5 = 5 * phi + 3 := by nlinarith
  34  have h10 : phi ^ 10 = phi ^ 5 * phi ^ 5 := by ring
  35  rw [h10]; nlinarith
  36
  37/-- φ^10 > 100. -/
  38theorem phi10_gt_100 : phi ^ 10 > 100 := by
  39  rw [phi10_fibonacci]; linarith [phi_gt_onePointSixOne]
  40
  41structure WeakForceCert where
  42  five_types : Fintype.card WeakDecayType = 5
  43  phi10_val : phi ^ 10 = 55 * phi + 34
  44  phi10_bound : phi ^ 10 > 100
  45
  46noncomputable def weakForceCert : WeakForceCert where
  47  five_types := weakDecayCount
  48  phi10_val := phi10_fibonacci
  49  phi10_bound := phi10_gt_100
  50
  51end IndisputableMonolith.Physics.WeakNuclearForceFromRS