periodDoublingTarget_8
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.
claimIn 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 in Recognition Science
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.
scope and limits
- Does not derive the integer 8 from the J-cost functional equation.
- Does not prove convergence or stability of the bifurcation sequence.
- Does not address the continuous Feigenbaum scaling constant.
- Does not connect the target to spatial dimension D = 3.
Lean usage
def nonlinearDynamicsCert : NonlinearDynamicsCert where five_bifurcations := bifurcationTypeCount eight_periods := periodDoublingTarget_8 zero_equilibrium := equilibriumformal statement (Lean)
32theorem periodDoublingTarget_8 : periodDoublingTarget = 8 := by decide
proof body
Term-mode proof.
33
34/-- At equilibrium: J = 0. -/