import Mathlib
/-!
# Sheaf coherence gate · what runs in production, proved

**A consistent global ranking exists exactly when the comparison graph has no directed cycle.**

Backs `backend/src/main/scala/ai/discursa/sheaf/H1Cohomology.scala`. The engine turns the agents'
comparative claims ("A ranks above B") into a directed graph on the items and decides
`present` (a genuine obstruction) by looking for a directed cycle. The header comment of that file
states the mathematics it relies on:

    a global section (a consistent global ranking) exists  ⟺  the net-preference digraph is acyclic.

This file proves that sentence for any relation on a finite set. In the engine, `R u v` is the
net preference "u above v" after the votes on the pair are aggregated and ties dropped; the
theorem holds for any relation, so nothing depends on how the edges were formed. A *ranking* is a map `f` to the natural numbers with `f v < f u`
whenever `R u v`. A *cycle* is a chain of comparisons that returns to its start,
`Relation.TransGen R v v`.

* `ranking_of_acyclic`      : no cycle → a ranking exists (an item's rank is the number of items
                              reachable below it).
* `acyclic_of_ranking`      : a ranking exists → no cycle.
* `exists_ranking_iff_acyclic` : the two together.

No axioms beyond Lean's standard three (`#print axioms` at the end). The companion file
`CycleCertificate.lean` gives the cohomological reading of the same fact: the cycle the engine
reports is a witness that the comparison data is not a coboundary.
-/

namespace SheafGate

open Relation

variable {V : Type*} [Finite V] (R : V → V → Prop)

/-- No comparison chain returns to its start. -/
def Acyclic : Prop := ∀ v, ¬ TransGen R v v

/-- `f` respects every comparison: whatever is placed above gets the larger number. -/
def IsRanking (f : V → ℕ) : Prop := ∀ u v, R u v → f v < f u

/-- The items strictly below `u` along some chain of comparisons. -/
noncomputable def below (u : V) : Finset V := by
  classical
  haveI := Fintype.ofFinite V
  exact Finset.univ.filter (fun x => TransGen R u x)

/-- The engine's ranking: an item scores the number of items it sits above. -/
noncomputable def rankOf (u : V) : ℕ := (below R u).card

lemma mem_below {u x : V} : x ∈ below R u ↔ TransGen R u x := by
  classical
  simp [below]

/-- No cycle → the number of items below each item is a ranking. -/
theorem ranking_of_acyclic (h : Acyclic R) : IsRanking R (rankOf R) := by
  intro u v huv
  classical
  apply Finset.card_lt_card
  rw [Finset.ssubset_iff_of_subset]
  · -- `v` itself is below `u` but not below `v` (that would be a cycle).
    refine ⟨v, (mem_below R).2 (TransGen.single huv), ?_⟩
    rw [mem_below]
    exact h v
  · -- everything below `v` is below `u`.
    intro x hx
    rw [mem_below] at hx ⊢
    exact TransGen.head huv hx

omit [Finite V] in
/-- A ranking decreases along every chain of comparisons, not only single steps. -/
lemma lt_of_transGen {f : V → ℕ} (hf : IsRanking R f) {u v : V} (h : TransGen R u v) :
    f v < f u := by
  induction h with
  | single hab => exact hf _ _ hab
  | tail _ hbc ih => exact lt_trans (hf _ _ hbc) ih

omit [Finite V] in
/-- A ranking exists → no cycle. -/
theorem acyclic_of_ranking {f : V → ℕ} (hf : IsRanking R f) : Acyclic R := by
  intro v hv
  exact lt_irrefl _ (lt_of_transGen R hf hv)

/-- The sentence in `H1Cohomology.scala`: a consistent global ranking exists iff there is no
directed cycle. -/
theorem exists_ranking_iff_acyclic : (∃ f : V → ℕ, IsRanking R f) ↔ Acyclic R :=
  ⟨fun ⟨_, hf⟩ => acyclic_of_ranking R hf, fun h => ⟨rankOf R, ranking_of_acyclic R h⟩⟩

end SheafGate

#print axioms SheafGate.exists_ranking_iff_acyclic