def definition def or abbrev

`alpha_from_phi`

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

formal statement (Lean)

  24noncomputable def alpha_from_phi : ℝ :=

Definition body.

  25  (1 - 1 / Constants.phi) / 2
  26
  27/-- ILG lag constant C_lag from RS: C_lag = φ^(-5) ≈ 0.090 -/

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

inflation_from_jcost_cert in IndisputableMonolith.Gravity.JCostInflaton decl_use
InflationFromJCostCert in IndisputableMonolith.Gravity.JCostInflaton decl_use
global_only_policy in IndisputableMonolith.Gravity.SPARCFalsifier decl_use
GlobalOnlyPolicy in IndisputableMonolith.Gravity.SPARCFalsifier decl_use
alpha_lt_half in IndisputableMonolith.Relativity.GRLimit.Parameters decl_use
alpha_lt_one in IndisputableMonolith.Relativity.GRLimit.Parameters decl_use
coupling_product_small_proven in IndisputableMonolith.Relativity.GRLimit.Parameters decl_use
GRLimitParameterFacts in IndisputableMonolith.Relativity.GRLimit.Parameters decl_use
rs_params_perturbative_proven in IndisputableMonolith.Relativity.GRLimit.Parameters decl_use
rs_params_positive in IndisputableMonolith.Relativity.GRLimit.Parameters decl_use
rs_params_small_proven in IndisputableMonolith.Relativity.GRLimit.Parameters decl_use

Lean names referenced from this declaration's body.