Returns of fibre configurations grow at the Lyapunov exponent

Category: 7-SigmaLayer. BACKLOG #176 (out of #19 and #150): the counting reading of #19's criterion.

#148 gave Posit 1's discharge one measurable criterion — the de-isolation flow has a positive Lyapunov exponent on the fibre — read off the derivative of the lift. This file gives the same criterion a second, counting reading on the hyperbolic witness: the number of fibre configurations that return to themselves after t strokes is L₂ₜ − 2, and it grows at exactly the stretching rate,

(1/t) log #{x ∈ T² : catStroke^[t] x = x} → 2 log φ

(CatMapPeriodicPoints.lean, ★★★ card_fixedPoints_cat_iterate, ★★ tendsto_log_card_fixedPoints_cat). Hyperbolicity of the fibre dynamics is therefore visible in how many records return, not only in how fast nearby lifts separate — the cat-stroke instance of topological entropy = Lyapunov exponent. Both readings give the same number, and both are classical statements about the ontic fibre; no quantisation of the fibre enters (BACKLOG #150's correction of 2026-10-21).

• ★★★ fibre_periodic_growth — the package: the count, its growth rate, and the Lyapunov exponent of the lift, all 2 log φ.

Honest scope

• ⚠️ Narrows the reading, does not decide #19. This is what the hyperbolic witness does; nothing here says nature's de-isolation is the cat stroke or in its conjugacy class (#175).
• Only the cat stroke; shearEvolve, the constructed witness, is a translation of the fibre and has every configuration fixed only at the trivial strokes — its periodic structure is #19's other side.

References: specs/BACKLOG.md #176, #19, #150, #148, #175; specs/POSITS.md Posit 1; Mathlib/Dynamics/CatMapPeriodicPoints.lean, SigmaLayer/FibreLyapunov.lean (catR_fderiv_hasLyapunovExponent), SigmaLayer/MovingFibreWitness.lean (catStroke).

theorem CSD.SigmaLayer.card_fixedPoints_catStroke (s : ℕ) : Nat.card { x : LF4.KTorus // catStroke^[s + 1] x = x } = (MeasureTheory.lucasEven (s + 1) - 2).natAbs

The fixed points of the hyperbolic stroke on the fibre are counted by L₂ₜ − 2.

theorem CSD.SigmaLayer.tendsto_log_card_fixedPoints_catStroke : Filter.Tendsto (fun (s : ℕ) => Real.log ↑(Nat.card { x : LF4.KTorus // catStroke^[s + 1] x = x }) / (↑s + 1)) Filter.atTop (nhds (2 * Real.log Real.goldenRatio))

The returns of fibre configurations grow at 2 log φ.

theorem CSD.SigmaLayer.fibre_periodic_growth : (∀ (s : ℕ), Nat.card { x : LF4.KTorus // catStroke^[s + 1] x = x } = (MeasureTheory.lucasEven (s + 1) - 2).natAbs) ∧ Filter.Tendsto (fun (s : ℕ) => Real.log ↑(Nat.card { x : LF4.KTorus // catStroke^[s + 1] x = x }) / (↑s + 1)) Filter.atTop (nhds (2 * Real.log Real.goldenRatio)) ∧ ∀ (v w : ℝ × ℝ), MeasureTheory.ellUR w ≠ 0 → HasLyapunovExponent (fderiv ℝ (⇑MeasureTheory.catR) v) w (2 * Real.log Real.goldenRatio)

★★★ Returns of fibre configurations grow at the Lyapunov exponent. Under the hyperbolic stroke, L₂ₜ − 2 fibre configurations return after t strokes, the count grows at 2 log φ, and 2 log φ is the Lyapunov exponent of the lift off the stable line (#148): #19's criterion read by counting returns agrees with its reading by stretching.