NonlinearDynamicsCert
plain-language theorem explainer
NonlinearDynamicsCert packages three equalities that map Recognition Science cost properties to nonlinear dynamics: the inductive BifurcationType has cardinality 5, the period-doubling target equals 8, and J-cost at 1 is zero. A physicist modeling chaos via J-growth would cite this certificate to anchor the five bifurcations and 2^3 periods to the underlying recognition cost. The declaration is a bare structure whose fields are direct equalities with no proof body.
Claim. A structure $C$ such that the set of bifurcation types has cardinality 5, the period-doubling target equals 8, and the recognition cost $J(1)$ equals 0.
background
In the module deriving nonlinear dynamics from Recognition Science, chaos arises when J-cost exceeds the J(φ) threshold. BifurcationType is the inductive type with constructors saddle-node, pitchfork, transcritical, Hopf, and period-doubling. The constant periodDoublingTarget is defined as 2^3. Jcost is imported from the Cost module and satisfies the zero-equilibrium condition at argument 1. This encodes the period-doubling route reaching 2^D with D=3.
proof idea
This is a structure definition with no proof body. It directly encodes the three required equalities as fields of the certificate.
why it matters
The structure is instantiated by nonlinearDynamicsCert to witness the module's nonlinear-dynamics claims. It supports the mapping of five bifurcations to configDim D=5 and the eight-tick octave (period 2^3), linking J-growth to the period-doubling route to chaos. It touches the approximation of the Feigenbaum constant by 3φ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.