Helical Attractors on
Contact 3-Manifolds:
A Toy ODE Study

In Plain Terms — Before the Mathematics

Everything in this volume so far has been an argument about shape. This chapter stops arguing and builds the smallest machine that actually shows the shape working — by hand, and small enough that every number in it can be checked by anyone who cares to.

Picture a point moving round a circle while drifting steadily upward. Its path is a helix, a spring standing on end. The claim of this chapter is that the helix pulls: start the motion anywhere outside it and the path spirals inward, settles onto it, and stays. That is what attractor means here, and every later claim in this series about a system that reorganises and then holds its new shape comes back to this picture.

Why a curved setting rather than the flat plane. In the plane a circle can close on itself. Once time stops being a parameter you keep track of and becomes a coordinate you move through, it cannot: a path that comes all the way round has also risen, so the closed loop is forced open into a helix. The contact form is the piece of geometry that enforces this, and Chapter 2 performed the same promotion on an ordinary oscillator. This chapter is that construction taken seriously enough to prove something about.

The honest surprise arrives in §6. Coming at the circle from outside, everything falls in. Coming from inside, there is a boundary — and it is not where a symmetric estimate had placed it. The certified value is r* = 0.7759…, located by bisection to a tolerance of 10⁻⁷, and it displaces a tidier figure that had been wrong in a direction nobody had thought to check. The asymmetry is not a flaw in the model. It is the model reporting something the estimate had smoothed away.

Read Chapter 12 with this one in hand. There the unit circle becomes the critical line of the Riemann zeta function, and the question of whether it attracts becomes the Riemann Hypothesis. This chapter is the prototype; the arithmetic is the instance.

The Contact 3-Manifold Setting

A contact 3-manifold is a smooth 3-manifold M equipped with a completely non-integrable plane field ξ = ker(α), where α is a contact form satisfying α ∧ dα ≠ 0 everywhere. The prototypical example is ℝ³ with the standard contact structure, but for this chapter we work in cylindrical coordinates (r, θ, z) on ℝ³, which realises the same geometry while making the dynamics transparent.

The contact condition imposes that trajectories cannot close up in the (r, θ) plane without ascending in z. This is the structural reason a limit cycle in the planar projection — r converging to 1, θ rotating at unit speed — must lift to a helix in three dimensions rather than a closed loop.

The system we study is a dissipative system whose attractor is a Legendrian helix, not a Reeb orbit and not a Reeb flow itself. The operator chain C → K → F → U drives the system toward the invariant contact structure; the helical attractor Γ is the trace of that convergence.

The ODE System

We study the following autonomous system on the contact manifold, designed to exhibit a stable helical attractor while capturing the structural features of the GTCT operator cycle.

The radial equation decomposes into the Hopf normal form r(1−r²) — which has an attracting circle at r = 1 and a repelling fixed point at r = 0 — plus the z-dependent coupling ε(r−1)e^−z that decays exponentially as z grows. At large z the system is asymptotically the Hopf normal form.

The rotation θ̇ = 1 encodes the contact structure at unit speed. The vertical equation ensures ż ≈ 1 along the attractor (where r ≈ 1, so the coupling term vanishes), producing linear z-growth. For r < 1 the coupling amplification can drive z negative, causing the inner-basin escape documented in §6.

Main Theorem and Proof Sketch

Linearise about r = 1: setting u = r − 1 gives u̇ ≈ −2u + O(u²) + ε·u·e^−z. Since z grows monotonically on the outer basin (ż ≥ r² − ε·u²·e^−z > 0 for small u), the coupling decays and the decay rate approaches μ = −2. Gronwall's inequality gives exponential convergence in a neighbourhood. Numerical evidence (DOP853, rtol = 10⁻¹⁰) confirms convergence at z(0) = 0 for 1 < r(0) ≤ 6.8. The Lean 4 proof closes the Gronwall estimate for the outer basin; the full nonlinear result is AXLE Issues #35 and #36. □

Correction, 2026-10-01. The claim “for every r(0) > 1” does not hold for this system. The coupling term 2(r − 1)e^−z grows without bound as z → −∞, so a trajectory that starts outside the circle at very negative z can be driven to z → −∞ while r grows (finite-time blow-up). At z(0) = 0 this happens for r(0) above about 6.9; for r(0) = 1.5 it happens at z(0) = −2. Convergence for general (r(0), z(0)) needs the extra hypothesis z(0) ≥ z_min(r(0)), which has not been proved. Check: book4/ch10-outer-basin-check.py. Status: restricted statement numerically verified; general statement open.

Proposition 3.1 (added 2026-11-07; hand-derived; not machine-checked in Lean). For the system as stated, ṙ = (r − 1)[2e^−z − r(r + 1)] and ż = r² − 2(r − 1)²e^−z, the set {r ≥ 1, z ≥ ln 2} is forward invariant, on it ż ≥ 1 and ṙ ≤ 0, and 0 ≤ r(t) − 1 ≤ (r₀ − 1)·exp[−2t + 2e^−z₀(1 − e^−t)].

Proof. r = 1 is invariant (ṙ = 0 there), so r ≥ 1 is preserved. Since r² − (2r − 1) = (r − 1)², ż − (2r − 1) = (r − 1)²(1 − 2e^−z) ≥ 0 when z ≥ ln 2; hence ż ≥ 2r − 1 ≥ 1 there, z cannot fall below ln 2, and z(t) ≥ z₀ + t. For r ≥ 1, r(r + 1) ≥ 2, so ṙ ≤ (r − 1)(2e^−z − 2) ≤ 0 (as 2e^−z ≤ 1). Integrating (r − 1)˙/(r − 1) ≤ 2e^−z₀−t − 2 gives the bound. □ This is a sufficient region only: z(0) = 0 lies below it, so the z(0) = 0 threshold r(0) ≈ 6.859 (outer saddle’s stable manifold crossing) remains numerical, and the general hypothesis z(0) ≥ z_min(r(0)) in the correction above is not removed.

Proposition 3.2 (contact form on the attracting tube; added 2026-11-08; hand-derived, algebra checked by ch10_contact_obstruction_check.py; not machine-checked in Lean). Let Σ = {z = ln 2, 4/5 < r < 6/5, θ ∈ S¹}. The set {4/5 ≤ r ≤ 6/5, z ≥ ln 2} is forward invariant and ż ≥ 2r − 1 ≥ 3/5 on it, so no trajectory returns to Σ. On the flow tube U swept out by Σ, use the coordinates (t, p, q) = (elapsed time, r₀ − 1, θ₀) of the starting point on Σ. Then α̃ = dt + p dq is a contact form on U, X is its Reeb field (α̃(X) = 1, ι_Xdα̃ = 0), and Γ = {r = 1} ∩ U is a Reeb orbit of α̃.

Proof. At r = 4/5 and z ≥ ln 2, 2e^−z ≤ 1 < r(r + 1) = 1.44, so ṙ = (r − 1)(2e^−z − r(r + 1)) > 0; at r = 6/5 the same bracket is negative and r − 1 > 0, so ṙ < 0. As in Proposition 3.1, ż ≥ 2r − 1. Since z strictly increases, the map (t, s) ↦ φ_t(s) on (0, ∞) × Σ is injective, and it is an immersion because X is transverse to Σ; so it is a diffeomorphism onto U. In these coordinates X = ∂_t, and α̃ ∧ dα̃ = dt ∧ dp ∧ dq ≠ 0. □ What this is not. It is not specific to dm³: any vector field with a global transversal and no recurrence is the Reeb field of dt + β on its flow tube, with dβ an area form on the section. The form depends on the choice of Σ, and it is unrelated to α = dz − r²dθ, whose kernel X does not preserve (the dr-coefficient of L_Xα is 2r − 4(r − 1)e^−z ≠ 0). Γ is a Reeb orbit of α̃ and a Legendrian curve of α; these are statements about different forms.

Complement to Proposition 3.2 (explicit formulas; added 2026-11-08; hand-derived and numerically checked). On U let τ(r, z) be the elapsed time since the trajectory crossed Σ and p(r, z) its radius at that crossing minus 1; they are fixed by fτ_r + gτ_z = 1, fp_r + gp_z = 0, τ(r, ln 2) = 0, p(r, ln 2) = r − 1. Since q = θ − τ, α̃ = (1 − p)dτ + p dθ, which involves only dθ and is well defined on S¹. Let Δ = R_pZ_t − R_tZ_p for the planar flow (R, Z)(t, p) from (1 + p, ln 2). Then Δ(0, p) = 1 + 2p, Δ(t, p) = (1 + 2p)exp ∫₀^t [2(1 + (R − 1)²)e^−Z − 3R² + 1] ds > 0, and α̃ ∧ dα̃ = (1/Δ) dr ∧ dθ ∧ dz (orientation of (t, p, q)). On the attracting cylinder p = 0 (r = 1, z = ln 2 + t): R_p = j(t) = e^{1 − e−t − 2t} and Z_p = k(t) = 2e(1 + e^−t)e^−e−t − 4, so Δ = j, α̃ = dz − (k/j)dr there, and the contact volume density relative to dr dθ dz is 1/j = e^{2t − 1 + e−t}. Derivation: along r = 1 the variational equations reduce to R_p′ = (e^−t − 2)R_p and Z_p′ = 2R_p; Δ follows from Liouville’s formula with div = f_r + g_z = 2e^−z[1 + (r − 1)²] − 3r² + 1; the volume identity follows by expanding dr ∧ dθ ∧ dz in (t, p, q). Provenance: these formulas were first proposed in a ChatGPT session; they were re-derived and checked here (section 7 of ch10_contact_obstruction_check.py, and by finite differences and numerical inversion of the flow at t = 2: p_r = 22.9963 and τ_r = −31.9890 against 1/j and −k/j). Reading. In the coordinates (t, p, q) the flow is pure translation in t with p constant, so the radial attraction is a property of the embedding (t, p) ↦ (r, z), not of the contact geometry. There is no conflict with the volume-preserving property of a Reeb flow: every neighbourhood of Γ has infinite contact volume (the density 1/j is unbounded), and the coefficient k/j is unbounded as z → ∞. The tube is the forward image of Σ, not the whole strip and not the basin.

Complement to Proposition 3.2 (strict form and normalised form; added 2026-11-08; hand-derived, algebra checked in section 8 of ch10_contact_obstruction_check.py). On U, with τ and p as above, α = dθ + p dτ satisfies L_Xα = d(Xθ) + (Xp)dτ + p·d(Xτ) = d(1) + 0 + p·d(1) = 0, since Xθ = 1, Xp = 0 and Xτ = 1; so X preserves α. Moreover dα = dp ∧ dτ and α ∧ dα = dθ ∧ dp ∧ dτ ≠ 0, as (τ, p, θ) are independent coordinates on U. The Reeb field of α is ∂_θ, and α(X) = 1 + p, which is a first integral. The form α̂ = (dθ + p dτ)/(1 + p) (note |p| < 1/5) has α̂(X) = 1, dα̂ = dp ∧ (dτ − dθ)/(1 + p)², and ι_Xdα̂ = 0 because dp(X) = 0 and (dτ − dθ)(X) = 0; hence X is the Reeb field of α̂, and α̂ ∧ dα̂ = dθ ∧ dp ∧ dτ/(1 + p)². In the coordinates (r, θ, z), α = A dr + dθ + C dz with A = pτ_r = −pZ_p/Δ and C = pτ_z = pR_p/Δ, where Δ = R_pZ_t − R_tZ_p as above. On the section Σ (t = 0, p = r − 1): τ_r = 0, τ_z = 1/(2r − 1), so α|_Σ = dθ + ((r − 1)/(2r − 1))dz and α̂|_Σ = (1/r)dθ + ((r − 1)/(r(2r − 1)))dz (ambient covectors at Σ). What this is. The coefficients are axisymmetric but still implicit in the flow (through τ and p); no elementary expression in (r, z) is known, so this is a flow-defined contact structure, not a closed form. It is the same tube and the same flow-box fact as Proposition 3.2, written in another gauge, and it gives no new dynamical prediction. Provenance: the strict form was proposed in a ChatGPT session; re-derived and checked here.

Proposition 3.3 (obstruction at the saddle orbits; added 2026-11-08; hand-derived, numbers checked by the script; not machine-checked in Lean). For either positive equilibrium (ρ, z_ρ) the circle C_ρ = {(ρ, θ, z_ρ)} is a periodic orbit of period 2π whose Poincaré multipliers are e^2πλ_± with λ₋ < 0 < λ₊ (det J = −ρ²(2ρ² + ρ + 1) < 0), and whose product is e^{2π tr J} with tr J = 1 + ρ − ρ² on ρ³ − ρ² − 2ρ + 1 = 0: tr J = 1.2470 at ρ = 0.4450 and −0.4450 at ρ = 1.8019, both nonzero. Consequently there is no contact form on any neighbourhood of C_ρ whose kernel is preserved by X. In particular X is not a Reeb field, nor a contact vector field, of any contact form there.

Proof. Suppose L_Xα̃ = hα̃ and let u = α̃(X). Then X(u) = hu, so u vanishes identically along C_ρ or nowhere on it. If u ≠ 0, replace α̃ by α̃/u: then α̃(X) = 1, L_Xα̃ = 0, so X is a Reeb field and the linearised return map on the transverse plane preserves dα̃, hence has determinant 1; but the determinant is e^{2π tr J} ≠ 1. If u ≡ 0, the orbit is tangent to ξ = ker α̃. Let c = e^∮h > 0. The return map multiplies α̃ by c, so its multiplier on TM/ξ is c; and L_Xdα̃|_ξ = h dα̃|_ξ with the orbit direction X fixed, so dα̃(X, ·) gives the same multiplier c on ξ/⟨X⟩. Both multipliers are equal and positive, which excludes a saddle. □ Reading. The dm³ system is a contact flow, for any contact form at all, only away from the saddle orbits. Any claim that it is an instance of a contact structure on the whole phase space is therefore false as stated; the tube of Proposition 3.2 is the domain where a realization exists. A simple closed-form expression for α̃ in the original coordinates, for example from the transport equations for L_Xα̃ = hα̃ with an axisymmetric ansatz A dr + B dθ + C dz, is an open research direction and untested; an exact implicit expression is given in the complement to Proposition 3.2.

Complement to Proposition 3.3 (general load λ; added 2026-11-08; hand-derived and numerically checked). For the family ż = λr² − 2(r − 1)²e^−z, at an equilibrium with ρ³ − ρ² − (1 + λ)ρ + 1 = 0, tr J = (ρ − 1)(ρ³ − 3ρ − 1) and det J = −λρ²(2ρ² + ρ + 1) < 0. The trace at the inner saddle is positive for every λ > 0. At the outer saddle it is negative for λ < λ*, positive for λ > λ*, and zero at ρ = 2cos(π/9), where λ* = (ρ − 1)²(ρ + 1)/ρ ≈ 1.1848. Hence the obstruction of Proposition 3.3 applies to both saddle orbits for every λ > 0 with λ ≠ λ*. At λ = λ* the product of multipliers is 1, so the transverse case needs a further argument, which is exact and finite. Write s = 2cos(π/9), so s³ = 3s + 1 and λ* = 2s² − s − 4, and centre at the outer saddle (x = r − s, y = z − z_s, 2e^−z_s = s(s + 1)). If the return map preserved a smooth area form ω, the average ω̄ = (1/2π)∫₀^2π φ_t^*ω dt would be a nonvanishing germ with L_X₂Dω̄ = 0, i.e. a density m = 1 + ax + by + cx² + dxy + ey² + … with ∂_x(mf) + ∂_y(mg) = 0. The linear equations force a = (−262s² + 32s + 716)/111 and b = (54s² − 21s − 123)/37. The quadratic equations then read M(c, d, e)ᵀ = b₂, where M has rows (−4s² + 2s + 2, 2 − 2s², 0), (−4s − 2, 0, 4 − 4s²), (0, −2s − 1, 4s² − 2s − 2) and b₂ = ((326s² − 172s − 1166)/37, (−508s² − 304s + 524)/111, (63s² − 6s + 60)/37). With w = (8s² + 8s + 2, −18s − 6, −4s² − 16s − 4) one has wᵀM = 0 and wᵀb₂ = −(36/37)(15s² + 25s + 9) ≠ 0 (a nonzero polynomial of degree 2 cannot vanish at a root of the irreducible cubic s³ − 3s − 1; numerically wᵀb₂ = −106.02). So the quadratic equations are inconsistent, and no C² density with m(0) ≠ 0 exists. Together with the transverse/tangent argument, for every λ > 0 neither saddle periodic orbit admits a smooth contact realization of X on a neighbourhood of the complete orbit; the tubes of Proposition 3.2 exclude those orbits. Provenance: the λ* analysis was carried out independently by a parallel session and by me; the certificate above was verified exactly (reduction modulo s³ − 3s − 1) in section 6 of ch10_contact_obstruction_check.py. The trace formula and λ* were found in a parallel session; its remark that the obstruction ends above λ* is incorrect, since the trace is nonzero on both sides of λ* (−0.0129 at λ = 1.18, +0.0141 at 1.19, +1.0 at 1.5). Checks: section 6 of ch10_contact_obstruction_check.py. The chapter’s system is λ = 1, where λ < λ*.

λ-family and the bone model. The audit of the λ-extension against the two bone scenarios (A and B), with its script and figure, is on a separate page: Chapter 10 λ extension: bone audit handoff.

Numerical Findings and Diagrams

All integrations use DOP853 with rtol = 10⁻¹⁰, atol = 10⁻¹². This scheme is ideal for smooth nonstiff ODEs; errors are well below the convergence scale. The inner boundary r* = 0.77594058 is certified independently by bisection to tolerance 10⁻⁷ (numerics/certify_rstar.py: rtol = 10⁻¹², atol = 10⁻¹⁴, with a verification sweep at ±10⁻⁴ to ±10⁻²).

5.1 The helical attractor — phase portrait

5.2 Exponential decay rate

For outer-basin trajectories, log|r(t) − 1| decays linearly with slope ≈ −2, approaching the linearised rate μ = −2 asymptotically as z grows and the coupling dies out.

5.3 Stability sweep table

The Basin Asymmetry Correction

The Gronwall estimate predicts a symmetric basin |r − 1| < ε₀ = 1/3, i.e. r ∈ (2/3, 4/3). The outer side is correct and conservative: the proved invariant region {r ≥ 1, z ≥ ln 2} converges (Proposition 3.1), and at z(0) = 0 the numerical outer threshold is r(0) ≈ 6.859; “all r(0) > 1 converge” does not hold (correction in §3). The inner side fails: the true inner boundary is r* = 0.77594058 (certified by bisection to 10⁻⁷), not 0.667.

Saddle Geometry: Closed-Form Results

The saddle equilibrium (r_s, z_s) of the dm³ ODE separates the convergent basin from the escape region. Its r-coordinate solves a cubic whose roots are expressible in closed form via Chebyshev-cosine reduction.

Setting ṙ = 0 and ż = 0 in the dm³ vector field with ε = 2 yields r(1−r²) + 2(r−1)e^−z = 0 and r² − 2(r−1)²e^−z = 0. Eliminating e^−z gives the cubic r³ − r² − 2r + 1 = 0. Depressing via r = u + 1/3 and applying the trigonometric method for three real roots produces the triple r_k = 2cos((2kπ + π)/7), k = 0, 1, 2, identifying r₀ = 2cos(3π/7) as the root in (0,1). □

From the cubic r_s³ = r_s² + 2r_s − 1. Expand (1 + r_s − r_s²)² = 1 + r_s² + r_s⁴ + 2r_s − 2r_s² − 2r_s³. Substitute r_s⁴ = r_s·r_s³ = r_s(r_s² + 2r_s − 1) and r_s³ = r_s² + 2r_s − 1; collect modulo the cubic to obtain 2 − r_s. □

Direct computation of J = D(ṙ, ż) at the saddle gives J₁₁ + J₂₂ = (1 − 3r_s² + 2e^−z_s) + r_s². Using the saddle condition to eliminate e^−z_s yields tr(J) = 1 + r_s − r_s². By Theorem B.2 this equals √(2 − r_s). The cosine value follows from the identity 2 − 2cos(3π/7) = 4cos²(2π/7) applied to r_s = 2cos(3π/7), giving √(2 − r_s) = 2cos(2π/7). □

The ż-component of the field is ż = r² − 2(r−1)²e^−z. Differentiating with respect to z: ∂_zż = 2(r−1)²e^−z. At the saddle the saddle condition r_s² = 2(r_s−1)²e^−z_s gives ∂_zż|_s = r_s². □

The characteristic polynomial is λ² − tr(J)λ + det(J) = 0. From Theorem B.3, tr(J) = 2cos(2π/7). Computing det(J) = J₁₁J₂₂ − J₁₂J₂₁ at the saddle and simplifying modulo the cubic gives det(J) = cos²(2π/7) − ¼(32r_s² + 15r_s − 10). The discriminant Δ = tr² − 4det = 32r_s² + 15r_s − 10 > 0 (numerically ≈ 3.0136), confirming two real eigenvalues. □

Integrating the linearised flow backward from (r_s, z_s) along the stable eigendirection of λ₋ ≈ −0.2445 (Theorem B.5) under the full nonlinear dm³ field (DOP853, rtol = 10⁻¹³, atol = 10⁻¹⁵) reaches z = 0 at r = 0.775940575502 — inside the independently certified bisection interval [0.7759405755019531, 0.7759405755023437] of §6 (certify_rstar_rigorous.py) to 1.5×10⁻¹³, i.e. agreement to every digit the certification carries. Cross-checked two ways: by algebraic elimination on the fixed-point equations (giving Theorem B.1's cubic directly, independent of this manifold-tracing argument) and by an unconstrained 2D root search from 23 starting points, both returning the same three saddles with no others.

This still is not a closed form: tracing a stable manifold to a specific transverse slice has no closed-form solution in general, and none is claimed here. What it gives instead is the correct shape of the object r* is — a global separatrix-crossing property of the full (r, z) flow, not a root of any function of r alone. That rules out one whole family of would-be closed forms: no scalar potential V(r) can have r* as a critical point, because r* is not determined locally at any single r-value — it depends on the entire trajectory reaching z = 0, which is why the elimination in Theorem B.1's proof (valid at the saddle itself) does not extend to r*. A concrete instance of this mistake being made and caught is recorded in docs/audit-log.md, 2026-09-22 entries: an attempted closure elsewhere in this series assumed V′(r*) = 0 for V(r) = ½(r−1)², which is false (V′(r) = r−1 vanishes only at r = 1, the attractor, not the boundary).

Formal Verification in Lean 4 (AXLE)

The GCTC Lean 4 project formalises key structural claims with Mathlib4, with zero logic axioms beyond Mathlib. Note: two files named Chain_updated.lean exist; the one described here is the registry-indexed copy (AXLE:NASA/MoonBase/AXLE_lean_files/), not the older 2026-04-18 draft at the GTCT repo root, which still carries two sorrys and r_star := 0.8. In the registry-indexed Chain_updated.lean four theorems are fully proved with no sorry: gronwall_outer, iter_consecutive_dist, spiral_return_exists (T1), and poincare_collatz_contracting. Two statements are admitted as explicit domain axioms pending dm³ ODE formalisation in Mathlib: inner_basin_is_asymmetric (AXLE Issue #32) and the general poincare_collatz. The distinction matters: a sorry marks an incomplete proof of something claimed to be true; an axiom is an admitted hypothesis, explicitly labelled as such. The original Chain.lean (retained for history) contains 3 sorrys; Chain_updated.lean contains none.

Connection to the GTCT Operator Chain

The dm³ system is a concrete instance of G = U ∘ F ∘ K ∘ C applied to a contact manifold. C (Compress) maps (r₀, z₀) to the deviation u = r − 1. K (Curvature) identifies the curvature −2 = μ_max at r = 1; the empirical threshold κ* = √(7/9) ≈ 0.882 marks the dm³ basin hierarchy (distinct from the chain contraction κ_chain ≤ √(5/9) ≈ 0.745 of the Vol IV Recursion Theorem, which follows from σ_min ≥ 2/3 and ‖u_iw_iᵀ‖ ≤ 1/3 via (2/3)² + (1/3)² = 5/9; note √(5/9) < r*, so the two constants cannot coincide). F (Fold) is read as the basin threshold r* = 0.77594058, the z = 0 crossing of the inner saddle’s stable manifold. No attractor and repeller branches merge there (both equilibria are saddles), and reading F as a Whitney A1 fold is not established (corrected 2026-11-07). U (Unfold) projects back to the manifold, producing the limit set Γ.

References

[1] Grossi, P. N. (2026). Principia Orthogona, Vol. I. Version 6. G6 LLC. doi:10.5281/zenodo.19117399 (Vol I concept DOI, resolves to current version)
[2] Grossi, P. N. (2026). Principia Orthogona, Vol. II. G6 LLC. doi:10.5281/zenodo.19379473
[3] AXLE v6.1 formal verification. totogt.github.io/AXLE · github.com/TOTOGT/GTCT
[4] Grossi, P. N. (2026). The Generative Time Circuit Theorem (GTCT). Version 4. Zenodo. doi:10.5281/zenodo.21708678
[5] Hairer, E., Nørsett, S. P., & Wanner, G. (1993). Solving ODEs I. Springer. [DOP853]
[6] Geiges, H. (2008). An Introduction to Contact Topology. Cambridge University Press.
[7] Hartman, P. (1982). Ordinary Differential Equations. SIAM. [Gronwall]
[8] Mathlib4 Community (2024). leanprover-community.github.io/mathlib4_docs