structure definition def or abbrev

`LabScalePrediction`

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

formal statement (Lean)

  80structure LabScalePrediction where
  81  T_dyn : ℝ           -- Rotation period
  82  τ0 : ℝ              -- Recognition tick
  83  α : ℝ               -- ILG exponent
  84  C_lag : ℝ           -- Coupling constant
  85  w_predicted : ℝ     -- Predicted weight
  86  h_w : w_predicted = 1 + C_lag * (Real.rpow (T_dyn / τ0) α - 1)
  87
  88/-- Construct a lab-scale prediction for a given device. -/

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

mkLabPrediction in IndisputableMonolith.Flight.GravityBridge decl_use
nullHypothesis in IndisputableMonolith.Flight.GravityBridge decl_use
optionB_bound_only in IndisputableMonolith.Flight.GravityBridge decl_use
rsLabPrediction in IndisputableMonolith.Flight.GravityBridge decl_use

depends on (8)

Lean names referenced from this declaration's body.

period in IndisputableMonolith.Astrophysics.PulsarEmissionRegimesFromRS decl_use
tick in IndisputableMonolith.Constants decl_use
tick in IndisputableMonolith.Constants.RSNativeUnits decl_use
scale in IndisputableMonolith.Cosmology.LargeScaleStructureFromRS decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
C_lag in IndisputableMonolith.Gravity.EightTickResonance decl_use
Coupling in IndisputableMonolith.Information.FEPBridgeFromJCost decl_use
constant in IndisputableMonolith.Relativity.Fields.Scalar decl_use