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)
40theorem alpha_s_positive : 0 < alpha_s_prediction := by
proof body
Term-mode proof.
41 unfold alpha_s_prediction
42 exact div_pos (zpow_pos phi_pos _) Real.pi_pos
43
44/-! ## Structural Constraints
45
46The three gauge couplings at the recognition scale satisfy:
47 1/α_EM + 1/α_weak + 1/α_s = cube_edges(D) × π
48
49This is the RS analog of gauge coupling unification. -/
50
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (14)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
cube_edges
in IndisputableMonolith.Constants.AlphaDerivation
decl_use
-
alpha_s_prediction
in IndisputableMonolith.Constants.StrongCoupling
decl_use
-
scale
in IndisputableMonolith.Cosmology.LargeScaleStructureFromRS
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
is
in IndisputableMonolith.Foundation.OptionAEmpiricalProgram
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
unification
in IndisputableMonolith.Foundation.RecognizerInducesLogic
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_positive
in IndisputableMonolith.Physics.RunningCouplings
decl_use