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

**The cycle the engine reports is a certificate that the comparison data is not a coboundary.**

Backs `backend/src/main/scala/ai/discursa/sheaf/H1Cohomology.scala` (the `cycle` field of its
`Result`): the direction "a directed cycle is present ⇒ the obstruction is a nonzero class in H¹".

The other direction is a different statement and lives in `Ranking.lean`: with no directed cycle,
a consistent global ranking exists (strict inequalities along every comparison). It is *not* the
claim that the margin data "each comparison says 1" is then a coboundary; that fails already on the
transitive triangle u→v, v→x, u→x, which has no cycle yet whose all-ones data would need
`f x - f u` to equal both 1 and 2. Formalising found the Scala header's "H¹ = 0 ⟺ acyclic" loose in
exactly this way; the precise pair is: cycle ⇒ H¹ witness (this file), no cycle ⇒ ranking exists
(`Ranking.lean`). Together they are the engine's `present` flag in both directions.

The setting is the two-term cochain complex of a finite directed graph with constant stalks:
vertices `V`, edges `E` with `src` and `tgt`, coefficients in a commutative ring `K`
(the engine uses ℚ-valued weights; ℤ works too).

* a 0-cochain is a function `f : V → K` (a position for every item),
* a 1-cochain is a function `y : E → K` (a stated difference on every comparison),
* the coboundary is `(δ f) e = f (tgt e) - f (src e)`,
* `H¹ = C¹ / im δ`; a 1-cochain has class zero iff it is `δ f` for some `f`.

A *chain* is a list of edges in which each edge starts where the previous one ended; it is *closed*
when the last edge ends where the first began. The two facts:

* `chain_sum_coboundary` : along a chain from `a` to `b`, the coboundary sums to `f b - f a`.
* `closed_sum_coboundary_eq_zero` : around a closed chain, every coboundary sums to zero.
* `not_coboundary_of_cycle_sum_ne_zero` : if `y` sums to something nonzero around a closed chain,
  then `y` is not a coboundary, so its class in `H¹` is nonzero. This is the dual witness: the
  cycle sum is a linear functional that kills `im δ` and does not kill `y`.
* `cycle_witness` : for a nonempty directed cycle, the data "each comparison says 1"
  is not a coboundary. This is the engine's `present = true` case, read cohomologically.

No axioms beyond Lean's standard three (`#print axioms` at the end).
-/

namespace SheafGate

variable {V E K : Type*} [CommRing K] (src tgt : E → V)

/-- The coboundary of a 0-cochain: the difference across each edge. -/
def coboundary (f : V → K) : E → K := fun e => f (tgt e) - f (src e)

/-- `es` is a chain from `a` to `b`: consecutive edges meet, the first starts at `a`, the last
ends at `b`. -/
inductive Chain : V → V → List E → Prop
  | nil (a : V) : Chain a a []
  | cons {a b : V} (e : E) {es : List E} (h₁ : src e = a) (h₂ : Chain (tgt e) b es) :
      Chain a b (e :: es)

/-- Along a chain from `a` to `b` the coboundary telescopes to `f b - f a`. -/
theorem chain_sum_coboundary (f : V → K) {a b : V} {es : List E} (h : Chain src tgt a b es) :
    (es.map (coboundary src tgt f)).sum = f b - f a := by
  induction h with
  | nil a => simp
  | cons e h₁ _ ih =>
    simp only [List.map_cons, List.sum_cons, ih, coboundary, h₁]
    ring

/-- Around a closed chain every coboundary sums to zero. -/
theorem closed_sum_coboundary_eq_zero (f : V → K) {a : V} {es : List E} (h : Chain src tgt a a es) :
    (es.map (coboundary src tgt f)).sum = 0 := by
  rw [chain_sum_coboundary src tgt f h]; ring

/-- A 1-cochain that does not sum to zero around some closed chain is not a coboundary:
its class in `H¹` is nonzero. -/
theorem not_coboundary_of_cycle_sum_ne_zero (y : E → K) {a : V} {es : List E}
    (h : Chain src tgt a a es) (hy : (es.map y).sum ≠ 0) :
    ¬ ∃ f : V → K, coboundary src tgt f = y := by
  rintro ⟨f, rfl⟩
  exact hy (closed_sum_coboundary_eq_zero src tgt f h)

/-- The engine's case: a nonempty directed cycle, each comparison stating a margin of `1`.
That data is not a coboundary, so the obstruction is a nonzero class in `H¹`. -/
theorem cycle_witness [CharZero K] {a : V} {es : List E} (h : Chain src tgt a a es)
    (hne : es ≠ []) :
    ¬ ∃ f : V → K, coboundary src tgt f = fun _ => (1 : K) := by
  apply not_coboundary_of_cycle_sum_ne_zero src tgt _ h
  simp only [List.map_const', List.sum_replicate, nsmul_eq_mul, mul_one]
  exact_mod_cast List.length_pos_iff.mpr hne |>.ne'

end SheafGate

#print axioms SheafGate.not_coboundary_of_cycle_sum_ne_zero
#print axioms SheafGate.cycle_witness