No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
114noncomputable def hypothesis6 : ℝ := (phi^3 - 1) / (phi^3 + 1)
proof body
Definition body.
115
116/-- **BEST FIT**: cos(θ_W) ≈ √(1 - 1/(2φ + 1))
117
118 Predicted: 0.874
119 Observed: 0.881
120 Error: ~0.8%
121
122 This is a promising φ-connection! -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.
-
bestCabibboFit
in IndisputableMonolith.StandardModel.CKMMatrix
decl_use
-
hypothesis6
in IndisputableMonolith.StandardModel.CKMMatrix
decl_use
depends on (5)
Lean names referenced from this declaration's body.
-
is
in IndisputableMonolith.Foundation.OptionAEmpiricalProgram
decl_use
-
is
in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
decl_use
-
is
in IndisputableMonolith.GameTheory.MechanismDesignFromSigma
decl_use
-
is
in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom
decl_use
-
hypothesis6
in IndisputableMonolith.StandardModel.CKMMatrix
decl_use