recognition /
Flight /
Flight.GravityBridge /
explainer
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)
163 def C_lag_RS : ℝ := Real.rpow phi (-5)
proof body
Definition body.
164
165 /-- With C_lag = φ⁻⁵ and typical lab scales, the predicted deviation is:
166 w - 1 = φ⁻⁵ * ((0.06 / 7.3e-15)^0.191 - 1)
167 ≈ 0.09 * 315
168 ≈ 28
169
170 This would be a LARGE effect if true! The null hypothesis would fail.
171 -/
used by (7)
From the project-wide theorem graph. These declarations reference this one in their body.
rsLabPrediction
in IndisputableMonolith.Flight.GravityBridge
decl_use
RunningCoupling
in IndisputableMonolith.Flight.GravityBridge
decl_use
alpha_RS
in IndisputableMonolith.Relativity.ILG.ClusterLensing
decl_use
C_lag_RS
in IndisputableMonolith.Relativity.ILG.ClusterLensing
decl_use
weight_rs
in IndisputableMonolith.Relativity.ILG.ClusterLensing
decl_use
weight_rs_positive
in IndisputableMonolith.Relativity.ILG.ClusterLensing
decl_use
ppnInverseStub
in IndisputableMonolith.Relativity.NewFixtures
decl_use
depends on (7)
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
C_lag
in IndisputableMonolith.Gravity.EightTickResonance
decl_use
is
in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom
decl_use
and
in IndisputableMonolith.NumberTheory.CirclePhaseLift
decl_use
C_lag_RS
in IndisputableMonolith.Relativity.ILG.ClusterLensing
decl_use