def definition def or abbrev

`fineStructureCert`

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

formal statement (Lean)

  42noncomputable def fineStructureCert : FineStructureCert where
  43  alpha_rung := alphaRung_eq

proof body

Definition body.

  44  factor_pos := rsAlphaFactor_pos
  45  factor_gt_100 := rsAlphaFactor_gt_100
  46
  47end IndisputableMonolith.Physics.FineStructureConstantFromRS

depends on (5)

Lean names referenced from this declaration's body.

alpha_rung in IndisputableMonolith.Nuclear.BindingEnergyFromPhiLadder decl_use
alphaRung_eq in IndisputableMonolith.Physics.FineStructureConstantFromRS decl_use
FineStructureCert in IndisputableMonolith.Physics.FineStructureConstantFromRS decl_use
rsAlphaFactor_gt_100 in IndisputableMonolith.Physics.FineStructureConstantFromRS decl_use
rsAlphaFactor_pos in IndisputableMonolith.Physics.FineStructureConstantFromRS decl_use