Current research

A theorem-grounded warning criterion for collapse in recursive systems. The work consists of a no-progress obstruction theorem formalized in Lean 4 and a corresponding empirical detection criterion under matched alert-budget benchmarking.

The theorem itself is short. In any preorder, the configuration x < y ≤ z ≤ x is impossible:

import Mathlib.Order.Basic

variable {α : Type*} [Preorder α]

theorem no_progress_cycle_public {x y z : α}
    (hxy : x < y) (hyz : y ≤ z) (hzx : z ≤ x) : False := by
  have hxz : x < z := lt_of_lt_of_le hxy hyz
  have hxx : x < x := lt_of_lt_of_le hxz hzx
  exact lt_irrefl x hxx

Preprint in preparation. Selected Lean artifacts and public research materials will be linked here on publication.

What is claimed

• Established A no-progress obstruction theorem in any preorder, formalized in Lean 4 and kernel-checked with no additional axioms reported.
• Tested A corresponding telemetry-level detection criterion, evaluated under matched alert-budget protocols against bounded benchmark families. Lead-time and admissibility receipts are computed at evaluation time.
• Open Generalization beyond the tested domains; the relationship between the formal obstruction and the telemetry analogue is empirical, not derived. Calibration parameters are domain-specific and are not claimed as universal.