structure
definition
NonlinearDynamicsCert
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Physics.NonlinearDynamicsFromRS on GitHub at line 37.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
34/-- At equilibrium: J = 0. -/
35theorem equilibrium : Jcost 1 = 0 := Jcost_unit0
36
37structure NonlinearDynamicsCert where
38 five_bifurcations : Fintype.card BifurcationType = 5
39 eight_periods : periodDoublingTarget = 8
40 zero_equilibrium : Jcost 1 = 0
41
42def nonlinearDynamicsCert : NonlinearDynamicsCert where
43 five_bifurcations := bifurcationTypeCount
44 eight_periods := periodDoublingTarget_8
45 zero_equilibrium := equilibrium
46
47end IndisputableMonolith.Physics.NonlinearDynamicsFromRS