BifurcationType
plain-language theorem explainer
BifurcationType enumerates the five canonical routes to chaos under the Recognition Science J-cost model. Nonlinear-dynamics researchers would cite the enumeration when certifying period-doubling cascades that reach the eight-tick octave. The declaration is a plain inductive type with five constructors that automatically derives Fintype for downstream cardinality proofs.
Claim. Let $B$ be the finite set of bifurcation types consisting of saddle-node, pitchfork, transcritical, Hopf, and period-doubling.
background
The module treats chaotic dynamics as J-growth once recognition cost exceeds the J(φ) threshold. It identifies five bifurcation types with configDim D = 5 and notes that period-doubling proceeds through periods 1, 2, 4, 8 (= 2^D). The inductive definition supplies the enumeration required by the cardinality theorem and the NonlinearDynamicsCert structure.
proof idea
Plain inductive definition declaring the five constructors saddleNode, pitchfork, transcritical, hopf, periodDoubling and deriving DecidableEq, Repr, BEq, Fintype.
why it matters
The type supplies the five_bifurcations field of NonlinearDynamicsCert and enables the theorem that Fintype.card BifurcationType = 5. It formalizes the period-doubling route reaching 2^3 = 8, consistent with the eight-tick octave (T7) and the module's claim that configDim D = 5 for chaotic systems. No open scaffolding is attached.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.