pcf-casoratian-catalogue: A machine-verified higher-order (order ≥ 3, uniform in k) Casoratian law for linear recurrences — the Abel–Jacobi–Liouville identity C(n+1) = (−1)^(k−1) c₀(n) C(n) in Lean 4 / Mathlib
Abstract
The higher-order (order ≥ 3) Casoratian law for a homogeneous linear recurrence, formalized to a clean axiom cone in Lean 4 / Mathlib. For the order-k recurrence s(n+k) = ∑j=0k−1 cj(n) s(n+j), the order-k Casoratian (the k×k discrete Wronskian of k solutions) C(n) = det[ s(t)(n+i) ]0≤i,t
Publication details
- Journal / source
- Zenodo (CERN European Organization for Nuclear Research)
- Publication date
- 2 August 2026
- Language
- EN