#19's criterion in record terms: which fibre configurations come back

Category: 7-SigmaLayer. BACKLOG #177 (out of #19 and #176): the derivative-free form of Posit 1's discharge criterion.

#148 gave #19 a criterion through the derivative of a lift — the de-isolation flow has a positive Lyapunov exponent on the fibre. #176 showed the hyperbolic witness's periodic-return count grows at the same rate. This file states the criterion as HasReturnGrowth f h with h > 0 (ReturnCriterion.lean): at every stroke count finitely many but at least one fibre configuration returns, and the count grows at rate h. It mentions no lift, no tangent vector and no direction, only which configurations come back — a statement about records.

• ★★★ catStroke_hasReturnGrowth — the hyperbolic witness has return growth 2 log φ > 0;
• pshift_eq_add — the constructed de-isolation's fibre action is a translation of the fibre;
• ★★ not_hasReturnGrowth_pshift — no fibre translation has return growth, for any amount and any rate: its return set at every stroke is all of the fibre or empty;
• ★★★ fibre_return_criterion — the package: the witness shearEvolve acts on the fibre, over any interval and at any base point, by a pshift (shearEvolve_snd), which fails the criterion, while the hyperbolic stroke meets it.

Honest scope

• ⚠️ Narrows the statement, does not decide #19. It says which side each corpus witness falls on under a criterion that needs no derivative; which map nature uses stays #19.
• The failure of the translation is by the first clause (finite and nonempty) at the very first stroke, so no exponent is computed for it; this is sharper than #148's "exponent 0", which needed the lift.

References: specs/BACKLOG.md #177, #19, #176, #148; specs/POSITS.md Posit 1; Mathlib/Dynamics/ReturnCriterion.lean, SigmaLayer/FibreLyapunov.lean (shearEvolve_snd), RecordLayer/ShearWitness.lean (pshift, shearEvolve).

theorem CSD.SigmaLayer.infinite_addCircle_one : Infinite (AddCircle 1)

The circle is infinite.

instance CSD.SigmaLayer.instInfiniteKTorus : Infinite LF4.KTorus

theorem CSD.SigmaLayer.catStroke_hasReturnGrowth : HasReturnGrowth catStroke (2 * Real.log Real.goldenRatio)

★★★ The hyperbolic witness has return growth 2 log φ.

theorem CSD.SigmaLayer.pshift_eq_add (a : ℝ) : RecordLayer.pshift a = fun (x : LF4.KTorus) => x + (↑a, 0)

The constructed de-isolation's fibre action is a translation of the fibre.

theorem CSD.SigmaLayer.not_hasReturnGrowth_pshift (a h : ℝ) : ¬HasReturnGrowth (RecordLayer.pshift a) h

★★ No fibre translation has return growth, for any amount and any rate.

theorem CSD.SigmaLayer.fibre_return_criterion {Xsel : Type u_1} {K : ℕ} (idx : Xsel → Fin K) (s t : OnticTime) : HasReturnGrowth catStroke (2 * Real.log Real.goldenRatio) ∧ 0 < 2 * Real.log Real.goldenRatio ∧ (∀ (x : Xsel × LF4.KTorus), (RecordLayer.shearEvolve idx s t x).2 = RecordLayer.pshift ((RecordLayer.elapsed t - RecordLayer.elapsed s) * RecordLayer.shearAmt K (idx x.1)) x.2) ∧ ∀ (a h : ℝ), ¬HasReturnGrowth (RecordLayer.pshift a) h

★★★ #19's criterion in record terms. The hyperbolic stroke has return growth 2 log φ > 0; the constructed de-isolation acts on the fibre, over any interval and at any base point, by a translation pshift a, and no translation has return growth at any rate.