IndisputableMonolith.Foundation.LogicRealConstants

declarations in this module (25)

• def phiL L27
• def tickL L31
• def octaveL L34
• def JbitL L37
• def EcohL L40
• def hbarL L43
• def gravL L46
• def kappaEinsteinL L49
• def alphaInvL L52
• theorem toReal_phiL L54
• theorem toReal_tickL L57
• theorem toReal_octaveL L59
• theorem toReal_JbitL L61
• theorem toReal_EcohL L64
• theorem toReal_hbarL L66
• theorem toReal_gravL L70
• theorem toReal_kappaEinsteinL L72
• theorem toReal_alphaInvL L75
• theorem phiL_pos L78
• theorem phiL_gt_one L83
• theorem phiL_gt_onePointFive L88
• theorem phiL_lt_onePointSixTwo L93
• theorem hbarL_eq_phi_inv_fifth L98
• theorem hbarL_bounds L101
• theorem alphaInvL_bounds L109