periodDoublingTarget_8
plain-language theorem explainer
The theorem fixes the period-doubling target at exactly 8, matching the eight-tick octave in the Recognition Science forcing chain. Physicists working on chaotic dynamics from recognition cost thresholds would cite it to confirm that the cascade reaches 2^3. The proof is a direct decision procedure that evaluates the definition 2^3 against the numeral 8.
Claim. In the Recognition Science model the period-doubling cascade reaches a target of $8$ periods, i.e., the natural number defined by successive doublings equals $8$.
background
The module treats chaotic dynamics as J-cost growth once recognition cost exceeds the J(φ) threshold. Five bifurcation types are identified with configuration dimension D = 5. The period-doubling route is listed as the sequence 1 → 2 → 4 → 8, with the explicit remark that 8 equals 2^3. Upstream, equilibrium states that Jcost 1 = 0 and periodDoublingTarget is introduced as the definition 2 ^ 3.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the equality between the definition 2 ^ 3 and the numeral 8.
why it matters
This supplies the eight_periods field inside the nonlinearDynamicsCert definition that certifies the full nonlinear-dynamics structure. It directly instantiates the eight-tick octave (period 2^3) from the T7 step of the forcing chain. The module also records the Feigenbaum approximation 3φ, but the present result only fixes the discrete target count.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.