structure definition def or abbrev

`Params`

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

formal statement (Lean)

   7structure Params where
   8  alpha : ℝ := 1

proof body

Definition body.

   9  Clag  : ℝ := 0
  10
  11/-- Basic positivity properties for ILG parameters. -/

used by (37)

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

kappa_discreteness in IndisputableMonolith.Flight.Geometry decl_use
logSpiral_ne_zero in IndisputableMonolith.Flight.Geometry decl_use
perTurn_ratio in IndisputableMonolith.Flight.Geometry decl_use
RotorPitch in IndisputableMonolith.Flight.Geometry decl_use
stepRatio_invariant_under_r0 in IndisputableMonolith.Flight.Geometry decl_use
stepRatio_logSpiral_closed_form in IndisputableMonolith.Flight.Geometry decl_use
tesla_turbine_master in IndisputableMonolith.Flight.TeslaTurbine decl_use
ParamProps in IndisputableMonolith.Gravity.ILG decl_use
Params in IndisputableMonolith.Gravity.ILG decl_use
w_t in IndisputableMonolith.Gravity.ILG decl_use
w_t_display in IndisputableMonolith.Gravity.ILG decl_use
w_t_ge_one in IndisputableMonolith.Gravity.ILG decl_use
w_t_nonneg in IndisputableMonolith.Gravity.ILG decl_use
w_t_nonneg_with in IndisputableMonolith.Gravity.ILG decl_use
w_t_ref in IndisputableMonolith.Gravity.ILG decl_use
w_t_ref_with in IndisputableMonolith.Gravity.ILG decl_use
w_t_rescale in IndisputableMonolith.Gravity.ILG decl_use
w_t_rescale_with in IndisputableMonolith.Gravity.ILG decl_use
w_t_with in IndisputableMonolith.Gravity.ILG decl_use
rotational_flatness_forced in IndisputableMonolith.Gravity.ILGDerivation decl_use
rotational_flatness_implies_nonzero_vflat in IndisputableMonolith.Gravity.ILGDerivation decl_use
rotational_flatness_implies_positive_vflat in IndisputableMonolith.Gravity.ILGDerivation decl_use
w_t_formula_grounded in IndisputableMonolith.Gravity.ILGDerivation decl_use
is_ilg_vrot in IndisputableMonolith.Gravity.RotationILG decl_use
solution_exists in IndisputableMonolith.Gravity.RotationILG decl_use
ParamProps in IndisputableMonolith.ILG.Params decl_use
ParamsKernelVerified in IndisputableMonolith.ILG.ParamsKernel decl_use
paramsKernel_verified_any in IndisputableMonolith.ILG.ParamsKernel decl_use
ParamProps in IndisputableMonolith.Relativity.ILG.Params decl_use
Params in IndisputableMonolith.Relativity.ILG.Params decl_use

… and 7 more

depends on (6)

Lean names referenced from this declaration's body.

alpha in IndisputableMonolith.Constants.Alpha decl_use
Clag in IndisputableMonolith.Constants.ILG decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
Params in IndisputableMonolith.Gravity.ILG decl_use
Params in IndisputableMonolith.Relativity.ILG.Params decl_use
Params in IndisputableMonolith.Spiral.SpiralField decl_use