def
definition
action_form_verified
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Relativity.GW.ActionExpansion on GitHub at line 32.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
29 let a := scale.a t
30 a * (1 + 0.01 * α * C_lag)
31
32def action_form_verified (scale : ScaleFactor) (h : TensorPerturbation) (α C_lag : ℝ) : Prop :=
33 True
34
35end GW
36end Relativity
37end IndisputableMonolith