theorem proved term proof

`two_div_17_upper`

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

formal statement (Lean)

  69theorem two_div_17_upper : (alpha_s_geom : ℝ) < 0.118 := by

proof body

Term-mode proof.

  70  simp only [alpha_s_geom]
  71  norm_num
  72
  73/-- The predicted value is within experimental error of the measured value.
  74
  75    pred = 2/17 ≈ 0.117647...
  76    exp  = 0.1179
  77    err  = 0.0009
  78
  79    |pred - exp| = |0.117647 - 0.1179| = 0.000253 < 0.0009 ✓
  80
  81    This is now PROVEN, not axiomatized. -/

depends on (12)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
alpha_s_geom in IndisputableMonolith.Physics.StrongForce decl_use
value in IndisputableMonolith.QFT.SpinStatistics decl_use
pred in IndisputableMonolith.RRF.Core.Vantage decl_use