Prove no periodic orbit for weakly reversible deficiency-zero networks

Author: marpaia

CRNT.lean

@@ -294,6 +294,7 @@ import CRNT.Theorems.DeficiencyZero.Stability
 import CRNT.Theorems.DeficiencyZero.Confinement
 import CRNT.Theorems.DeficiencyZero.Lyapunov
 import CRNT.Theorems.DeficiencyZero.AsymptoticStability
+import CRNT.Theorems.DeficiencyZero.NoPeriodicOrbit
 import CRNT.Theorems.DeficiencyOne.Statement
 import CRNT.Theorems.DeficiencyOne.LogRatioUniqueness
 import CRNT.Theorems.DeficiencyOne.ToricReduction

CRNT/Theorems/DeficiencyZero/NoPeriodicOrbit.lean

@@ -0,0 +1,104 @@
+/-
+No non-constant positive periodic orbit for weakly reversible, deficiency-zero
+mass-action networks.
+
+The relative entropy `relEntropy xstar` is a strict Lyapunov function: it is nonincreasing
+along every positive trajectory and its dissipation vanishes only at complex-balanced points.
+A positive periodic orbit returns the relative entropy to its starting value each period, so
+along the orbit the relative entropy is both nonincreasing and periodic, hence constant; its
+derivative, the dissipation, is therefore identically zero, so every point of the orbit is
+complex-balanced. Deficiency-zero per-class uniqueness then forces the orbit to be a single
+point. Consequently a weakly reversible deficiency-zero network sustains no oscillation, for
+every choice of rate constants.
+-/
+import CRNT.Theorems.DeficiencyZero.AsymptoticStability
+import CRNT.Theorems.DeficiencyZero.Existence
+
+open scoped BigOperators
+
+namespace CRNT
+
+/-- A real function that is antitone and periodic with a positive period is constant. -/
+theorem eq_of_antitone_periodic {g : ℝ → ℝ} {T : ℝ} (hT : 0 < T)
+    (hanti : Antitone g) (hper : Function.Periodic g T) : ∀ x y, g x = g y := by
+  have hiter : ∀ (n : ℕ) (x : ℝ), g (x + n * T) = g x := by
+    intro n
+    induction n with
+    | zero => intro x; simp
+    | succ k ih =>
+        intro x
+        have hstep : g (x + ((k : ℝ) + 1) * T) = g x := by
+          have harg : x + ((k : ℝ) + 1) * T = (x + (k : ℝ) * T) + T := by ring
+          rw [harg, hper, ih x]
+        simpa [Nat.cast_succ] using hstep
+  have key : ∀ x y : ℝ, g x ≤ g y := by
+    intro x y
+    obtain ⟨n, hn⟩ := Archimedean.arch (y - x) hT
+    have hnn : y - x ≤ (n : ℝ) * T := by simpa [nsmul_eq_mul] using hn
+    have hle : y ≤ x + (n : ℝ) * T := by linarith
+    calc g x = g (x + (n : ℝ) * T) := (hiter n x).symm
+      _ ≤ g y := hanti hle
+  intro x y
+  exact le_antisymm (key x y) (key y x)
+
+namespace Network
+
+variable {S : Type} [DecidableEq S] [Fintype S]
+
+/-- **No non-constant positive periodic orbit.** For a weakly reversible, deficiency-zero
+mass-action network, every positive periodic solution of the mass-action ODE is constant, for
+every choice of rate constants. This is the exclusion of sustained oscillation from the
+deficiency-zero class. -/
+theorem eq_of_periodic_solution
+    (N : Network S) (hwr : N.WeaklyReversible) (hδ : N.DeficiencyZero) (κ : N.RateConstants)
+    {γ : ℝ → Concentration S} {T : ℝ} (hT : 0 < T)
+    (hpos : ∀ t, (γ t).Positive)
+    (hsol : ∀ t s, HasDerivAt (fun τ => γ τ s) (N.massActionVectorField κ (γ t) s) t)
+    (hper : Function.Periodic γ T) :
+    ∀ t, γ t = γ 0 := by
+  -- A positive complex-balanced reference exists from weak reversibility and δ = 0.
+  obtain ⟨xstar, hxs, hcb⟩ := N.exists_isComplexBalanced hwr hδ κ
+  -- The relative entropy along the orbit is antitone (Lyapunov descent) and periodic, hence
+  -- constant.
+  have hanti : Antitone (fun t => relEntropy xstar (γ t)) :=
+    N.relEntropy_antitone_along_solution κ hxs hcb hpos hsol
+  have hgper : Function.Periodic (fun t => relEntropy xstar (γ t)) T := by
+    intro t
+    show relEntropy xstar (γ (t + T)) = relEntropy xstar (γ t)
+    rw [hper t]
+  have hgconst : ∀ a b, relEntropy xstar (γ a) = relEntropy xstar (γ b) :=
+    eq_of_antitone_periodic hT hanti hgper
+  -- Whole-vector form of the solution, for the compatibility-class lemma.
+  have hsolwv : ∀ τ, HasDerivAt γ (N.massActionVectorField κ (γ τ)) τ :=
+    fun τ => hasDerivAt_pi.mpr (fun s => hsol τ s)
+  -- Every point of the orbit is complex-balanced: the relative entropy is locally constant, so
+  -- its derivative (the dissipation) vanishes, and vanishing dissipation is complex balance.
+  have hcbt : ∀ t, N.IsComplexBalanced κ (γ t) := by
+    intro t₀
+    have hchain := relEntropy_hasDerivAt hxs (hpos t₀) (fun s => hsol t₀ s)
+    have hd0 : HasDerivAt (fun τ => relEntropy xstar (γ τ)) 0 t₀ := by
+      have heq : (fun τ => relEntropy xstar (γ τ)) = fun _ => relEntropy xstar (γ t₀) := by
+        funext u; exact hgconst u t₀
+      rw [heq]; exact hasDerivAt_const t₀ _
+    have hdiss : (∑ s, (Real.log (γ t₀ s) - Real.log (xstar s))
+        * N.massActionVectorField κ (γ t₀) s) = 0 := hchain.unique hd0
+    exact N.complexBalanced_of_dissipation_eq_zero κ (hpos t₀) hxs hcb hdiss
+  -- Every point of the orbit lies in γ 0's positive compatibility class.
+  have hmem : ∀ t, γ t ∈ N.positiveCompatibilityClass (γ 0) := by
+    intro t
+    refine ⟨?_, hpos t⟩
+    show γ t - γ 0 ∈ N.stoichSubspace
+    rcases le_total 0 t with h | h
+    · have hsol0t : ∀ τ ∈ Set.Icc (0 : ℝ) t,
+          HasDerivAt γ (N.massActionVectorField κ (γ τ)) τ := fun τ _ => hsolwv τ
+      exact N.sub_mem_stoichSubspace_of_solution κ h hsol0t
+    · have hsolt0 : ∀ τ ∈ Set.Icc t (0 : ℝ),
+          HasDerivAt γ (N.massActionVectorField κ (γ τ)) τ := fun τ _ => hsolwv τ
+      have h2 := N.sub_mem_stoichSubspace_of_solution κ h hsolt0
+      simpa [neg_sub] using N.stoichSubspace.neg_mem h2
+  -- Two complex-balanced points of one positive class are equal (deficiency-zero uniqueness).
+  intro t
+  exact N.isComplexBalanced_unique_in_positiveClass hwr κ (hmem t) (hmem 0) (hcbt t) (hcbt 0)
+
+end Network
+end CRNT

scripts/metrics.py

@@ -0,0 +1,115 @@
+#!/usr/bin/env python3
+"""Regenerate the headline quantitative metrics reported in the crnt-lean paper.
+
+Paths resolve relative to the repository root, so the module counts, line counts,
+audited-theorem count, and analyze-contract shape can be checked against the
+artifact rather than taken on trust:
+
+    python3 scripts/metrics.py
+"""
+
+from __future__ import annotations
+
+import re
+import subprocess
+from pathlib import Path
+
+REPO_ROOT = Path(__file__).resolve().parent.parent
+
+
+def lean_files(*dirs: str) -> list[Path]:
+    """All `.lean` files under the given repo-relative directories."""
+    files: list[Path] = []
+    for directory in dirs:
+        files.extend(sorted((REPO_ROOT / directory).rglob("*.lean")))
+    return files
+
+
+def line_count(paths: list[Path]) -> int:
+    """Total newline count across the files, matching `cat ... | wc -l`."""
+    return sum(path.read_text().count("\n") for path in paths)
+
+
+def audited_theorem_count() -> int:
+    """Number of `#print axioms` invocations in the audit module.
+
+    Only lines that begin with the directive are counted, so a prose mention of
+    the string in the module docstring is not miscounted.
+    """
+    audit = (REPO_ROOT / "test" / "AxiomAudit.lean").read_text().splitlines()
+    return sum(1 for line in audit if line.startswith("#print axioms "))
+
+
+def analyze_contract() -> tuple[int, int]:
+    """The `analysisVersion` and the field count of `structure Analysis`."""
+    text = (REPO_ROOT / "CRNT" / "Interop" / "Analysis.lean").read_text()
+    version_match = re.search(r"analysisVersion\s*:\s*Nat\s*:=\s*(\d+)", text)
+    version = int(version_match.group(1)) if version_match else -1
+
+    fields = 0
+    in_struct = False
+    for line in text.splitlines():
+        if line.startswith("structure Analysis where"):
+            in_struct = True
+            continue
+        if in_struct:
+            if "deriving" in line:
+                break
+            if re.match(r"^  [A-Za-z]+ :", line):
+                fields += 1
+    return version, fields
+
+
+def git_short_sha() -> str:
+    """Short HEAD commit hash, or a placeholder outside a git checkout."""
+    try:
+        result = subprocess.run(
+            ["git", "rev-parse", "--short", "HEAD"],
+            cwd=REPO_ROOT,
+            capture_output=True,
+            text=True,
+            check=True,
+        )
+        return result.stdout.strip()
+    except (subprocess.CalledProcessError, FileNotFoundError):
+        return "no-git"
+
+
+def main() -> None:
+    lib = lean_files("CRNT")
+    test = lean_files("test")
+
+    lib_modules = len(lib)
+    # total = CRNT modules + test harness + CRNT.lean aggregator + Analyze.lean
+    total_modules = lib_modules + len(test) + 2
+
+    lib_lines = line_count(lib)
+    total_lines = line_count(
+        lib + test + [REPO_ROOT / "CRNT.lean", REPO_ROOT / "Analyze.lean"]
+    )
+
+    audited = audited_theorem_count()
+    version, fields = analyze_contract()
+
+    print(f"crnt-lean headline metrics (regenerated {git_short_sha()})")
+    print("-" * 65)
+    print(f"library modules (CRNT/)              : {lib_modules}")
+    print(f"total modules (+ aggregator/exe/test): {total_modules}")
+    print(f"library lines (CRNT/)                : {lib_lines}")
+    print(f"total lines (+ aggregator/exe/test)  : {total_lines}")
+    print(f"audited theorems (#print axioms)     : {audited}")
+    print(f"analyze contract version             : {version}")
+    print(f"analyze contract fields              : {fields}")
+    print()
+    print("per-area module counts:")
+    areas = [
+        (area.name, len(list(area.rglob("*.lean"))))
+        for area in (REPO_ROOT / "CRNT").iterdir()
+        if area.is_dir()
+    ]
+    for name, count in sorted(areas, key=lambda item: item[1], reverse=True):
+        print(f"  {name:<28} {count}")
+
+
+if __name__ == "__main__":
+    main()

test/AxiomAudit.lean

@@ -388,6 +388,10 @@ The `(whitespace := lax)` mode makes the comparison insensitive to how long name
 #guard_msgs (whitespace := lax) in
 #print axioms CRNT.Network.omegaLimit_eq_singleton_of_comparableGrowthDescent
 
+/-- info: 'CRNT.Network.eq_of_periodic_solution' depends on axioms: [propext, Classical.choice, Quot.sound] -/
+#guard_msgs (whitespace := lax) in
+#print axioms CRNT.Network.eq_of_periodic_solution
+
 /-- info: 'CRNT.Network.siphonFacet_floor_of_nearFacet_dissipation' depends on axioms: [propext, Classical.choice, Quot.sound] -/
 #guard_msgs (whitespace := lax) in
 #print axioms CRNT.Network.siphonFacet_floor_of_nearFacet_dissipation