Finite Lyapunov Core (mod 96) A verified finite-state energy system with global contraction bounds

This repository contains a fully verified rational-energy machine over 96 residue classes, equipped with:

a complete finite directed edge system,

rational delta-weights for each transition,

a computed eps-bound ensuring delta ≤ -eps_verified for all transitions,

and a Coq proof of global contraction for every edge of the system.

This project does not assume any specific recurrence (e.g. Collatz). It provides a general Lyapunov kernel that any recurrence F : Z → Z can use, provided its residue transitions embed into the provided edge set.

Features ✓ Finite state space (mod 96)

A residue system with 96 classes {0,...,95}.

✓ Complete rational-weighted transitions

Hundreds of edges of the form:

(src = r, dst = r', delta = q)

with q ∈ ℚ.

✓ Global eps-bound

An automatically computed negative constant eps_verified < 0 that bounds all delta-values strictly:

∀ e ∈ edges, delta(e) ≤ -eps_verified

✓ Coq verification (no assumptions)

The file Lyapunov_mod96.v provides:

verification of the eps-bound,

per-edge delta bounds,

a global contraction theorem.

This is a completely formal, finite proof.

Goal of the project

This repository provides a general-purpose Lyapunov framework for finite residue-based dynamical systems.

Any recurrence F whose residue evolution under mod 96 lies inside this graph inherits global strict contraction.

Future work will include:

connecting concrete recurrences (Collatz, Juggler),

visualization,

generalization to mod 128, 192, 256.