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

**The coherence defect is the Dirichlet energy of the sheaf Laplacian, it is bounded, and its kernel
                            is
exactly the agreement (H⁰).**

Backs `backend/src/main/scala/ai/discursa/sheaf/SheafLaplacian.scala` (whitepaper §5.2–5.4). The
engine builds, for each shared claim and each pair of agents addressing it, a weighted edge; it then
computes the energy `xᵀLx = Σ_e w_e (x_u − x_v)²`, the defect `energy / E_max`, and `dim ker L`.

The setting is a finite weighted graph: vertices `V`, edges `E` with `src` and `tgt`, weights
`w : E → K` in a linearly ordered field (the engine uses floating point; ℚ is the exact model).
Multiple edges between the same two vertices are allowed, as in the engine (one edge per claim).

* `cob`                   : the coboundary `(δ x) e = x (tgt e) - x (src e)`.
* `energy`                : `Σ_e w_e (δ x e)²`.
* `lap`                   : the sheaf Laplacian `L = δᵀ W δ`, written out as a map on 0-cochains.
* `dotProduct_lap`        : `Σ_v x_v (L x)_v = energy w x`; the number the engine reports is a
                            quadratic
                            form of `L` (whitepaper (5.3)).
* `energy_nonneg`         : the energy is nonnegative when the weights are.
* `energy_le_max`         : when every position lies in `[-a, a]`, the energy is at most
                            `Σ_e w_e (2a)²`; this is the engine's `E_max`, so the defect lies in
                            `[0,1]`.
* `lap_eq_zero_iff`       : with positive weights, `L x = 0 ⟺ δ x = 0`: the kernel of the Laplacian
                            is
                            the space of global sections (H⁰), so `kerDim` counts agreement.
* `cob_eq_zero_iff`       : `δ x = 0 ⟺ x` takes the same value at both ends of every edge, hence is
                            constant along every path (`cob_eq_zero_iff_reachable_eq`).
* `weighted_orthogonal`   : a cochain in `ker δᵀW` is `W`-orthogonal to every coboundary, and
* `eq_zero_of_cob_of_harmonic`: a cochain in both `im δ` and `ker δᵀW` is zero. This is the
                            uniqueness half of the Hodge splitting `C¹ = im δ ⊕ ker δᵀ` in
                            whitepaper §5.4; the existence half (every
                            `y` decomposes) is left for a later pass.

Not in this file, and therefore not yet proved:
* anything about eigenvalues. The engine's `spectralGap` (λ₂) is computed in floating point by
  Jacobi rotation and is reported as a robustness read, never as the score;
* `dim ker L = number of connected components`. This file proves the kernel is the locally constant
  functions; the count, which is what the engine's `kerDim` reports, is a later pass;
* the existence half of the Hodge splitting (every 1-cochain is a coboundary plus a harmonic part).

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

namespace SheafGate

open Finset

section Ring
variable {V E K : Type*} [Fintype V] [Fintype E] [DecidableEq V] [CommRing K]
variable (src tgt : E → V) (w : E → K)

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

/-- The Dirichlet energy `Σ_e w_e (δx)_e²`; the engine's `energy`. -/
def energy (x : V → K) : K := ∑ e, w e * (cob src tgt x e) ^ 2

/-- The sheaf Laplacian `L = δᵀ W δ` as a map on 0-cochains:
`(L x) v = Σ_e w_e (δx)_e ([tgt e = v] − [src e = v])`. -/
def lap (x : V → K) : V → K :=
  fun v => ∑ e, w e * cob src tgt x e *
    ((if tgt e = v then 1 else 0) - (if src e = v then 1 else 0))

/-- `Σ_v x_v ((Lx)_v) = energy`: the engine's number is the quadratic form of `L`. -/
theorem dotProduct_lap (x : V → K) : ∑ v, x v * lap src tgt w x v = energy src tgt w x := by
  unfold lap energy
  simp_rw [Finset.mul_sum]
  rw [Finset.sum_comm]
  refine Finset.sum_congr rfl fun e _ => ?_
  have : ∑ v, x v * (w e * cob src tgt x e *
      ((if tgt e = v then 1 else 0) - (if src e = v then 1 else 0)))
      = w e * cob src tgt x e * (x (tgt e) - x (src e)) := by
    simp [mul_sub, Finset.sum_sub_distrib, mul_ite, Finset.sum_ite_eq]
    ring
  rw [this]
  simp only [cob]
  ring

omit [Fintype V] [Fintype E] [DecidableEq V] in
/-- `δ x = 0` iff `x` agrees across every edge. -/
theorem cob_eq_zero_iff (x : V → K) : cob src tgt x = 0 ↔ ∀ e, x (src e) = x (tgt e) := by
  constructor
  · intro h e
    have := congrFun h e
    simp only [cob, Pi.zero_apply, sub_eq_zero] at this
    exact this.symm
  · intro h
    funext e
    simp [cob, h e]

omit [Fintype V] [Fintype E] [DecidableEq V] in
/-- The undirected adjacency the edges induce. -/
def Adj (u v : V) : Prop := ∃ e, (src e = u ∧ tgt e = v) ∨ (src e = v ∧ tgt e = u)

omit [Fintype V] [Fintype E] [DecidableEq V] in
/-- A 0-cochain with zero coboundary is constant along every path: `H⁰` is the locally constant
functions, one value per connected component. -/
theorem cob_eq_zero_iff_reachable_eq (x : V → K) :
    cob src tgt x = 0 ↔ ∀ u v, Relation.ReflTransGen (Adj src tgt) u v → x u = x v := by
  rw [cob_eq_zero_iff]
  constructor
  · intro h u v huv
    induction huv with
    | refl => rfl
    | tail _ hbc ih =>
      obtain ⟨e, he | he⟩ := hbc
      · rw [ih, ← he.1, ← he.2]; exact h e
      · rw [ih, ← he.1, ← he.2]; exact (h e).symm
  · intro h e
    exact h _ _ (Relation.ReflTransGen.single ⟨e, Or.inl ⟨rfl, rfl⟩⟩)

/-- `δᵀW` applied to a 1-cochain `y`: `(δᵀ W y) v = Σ_e w_e y_e ([tgt e = v] − [src e = v])`. -/
def cobT (y : E → K) : V → K :=
  fun v => ∑ e, w e * y e *
    ((if tgt e = v then 1 else 0) - (if src e = v then 1 else 0))

/-- The weighted pairing `⟪δ x, y⟫_W = Σ_e w_e (δx)_e y_e` equals `Σ_v x_v (δᵀ W y)_v`. -/
theorem weighted_pairing (x : V → K) (y : E → K) :
    ∑ e, w e * cob src tgt x e * y e = ∑ v, x v * cobT src tgt w y v := by
  unfold cobT
  simp_rw [Finset.mul_sum]
  rw [Finset.sum_comm]
  refine Finset.sum_congr rfl fun e _ => ?_
  simp [mul_sub, Finset.sum_sub_distrib, mul_ite, Finset.sum_ite_eq, cob]
  ring

/-- A harmonic 1-cochain (`δᵀ W y = 0`) is `W`-orthogonal to every coboundary. -/
theorem weighted_orthogonal (x : V → K) (y : E → K) (hy : cobT src tgt w y = 0) :
    ∑ e, w e * cob src tgt x e * y e = 0 := by
  rw [weighted_pairing, hy]; simp

end Ring

section OrderedField
variable {V E K : Type*} [Fintype V] [Fintype E] [DecidableEq V]
variable [Field K] [LinearOrder K] [IsStrictOrderedRing K]
variable (src tgt : E → V) (w : E → K)

omit [Fintype V] [DecidableEq V] in
/-- Nonnegative weights give nonnegative energy. -/
theorem energy_nonneg (hw : ∀ e, 0 ≤ w e) (x : V → K) : 0 ≤ energy src tgt w x :=
  Finset.sum_nonneg fun e _ => mul_nonneg (hw e) (sq_nonneg _)

omit [Fintype V] [DecidableEq V] in
/-- Positions in `[-a, a]` give energy at most `Σ_e w_e (2a)²`: the engine's `E_max`. -/
theorem energy_le_max (hw : ∀ e, 0 ≤ w e) {a : K} (x : V → K) (hx : ∀ v, |x v| ≤ a) :
    energy src tgt w x ≤ ∑ e, w e * (2 * a) ^ 2 := by
  refine Finset.sum_le_sum fun e _ => mul_le_mul_of_nonneg_left ?_ (hw e)
  have h : |cob src tgt x e| ≤ 2 * a := by
    calc |cob src tgt x e| = |x (tgt e) - x (src e)| := rfl
      _ ≤ |x (tgt e)| + |x (src e)| := abs_sub _ _
      _ ≤ a + a := add_le_add (hx _) (hx _)
      _ = 2 * a := by ring
  have ha : 0 ≤ 2 * a := le_trans (abs_nonneg _) h
  calc (cob src tgt x e) ^ 2 = |cob src tgt x e| ^ 2 := (sq_abs _).symm
    _ ≤ (2 * a) ^ 2 := by gcongr

omit [Fintype V] [DecidableEq V] in
/-- Zero energy with positive weights forces zero coboundary. -/
theorem cob_eq_zero_of_energy_eq_zero (hw : ∀ e, 0 < w e) (x : V → K)
    (h : energy src tgt w x = 0) : cob src tgt x = 0 := by
  unfold energy at h
  rw [Finset.sum_eq_zero_iff_of_nonneg (fun e _ => mul_nonneg (hw e).le (sq_nonneg _))] at h
  funext e
  have := h e (Finset.mem_univ e)
  rcases mul_eq_zero.1 this with h0 | h0
  · exact absurd h0 (hw e).ne'
  · simpa using pow_eq_zero_iff (n := 2) (by norm_num) |>.1 h0

/-- With positive weights the kernel of the Laplacian is exactly the kernel of the coboundary:
`ker L = H⁰`, so `kerDim` counts independent agreements. -/
theorem lap_eq_zero_iff (hw : ∀ e, 0 < w e) (x : V → K) :
    lap src tgt w x = 0 ↔ cob src tgt x = 0 := by
  constructor
  · intro h
    apply cob_eq_zero_of_energy_eq_zero src tgt w hw x
    rw [← dotProduct_lap, h]
    simp
  · intro h
    funext v
    simp [lap, h]

/-- A cochain that is both a coboundary and harmonic is zero (positive weights): the Hodge splitting
`C¹ = im δ ⊕ ker δᵀW` has trivial intersection, so the harmonic part of any data is unique. -/
theorem eq_zero_of_cob_of_harmonic (hw : ∀ e, 0 < w e) (x : V → K)
    (hy : cobT src tgt w (cob src tgt x) = 0) : cob src tgt x = 0 := by
  apply cob_eq_zero_of_energy_eq_zero src tgt w hw x
  have := weighted_orthogonal src tgt w x (cob src tgt x) hy
  unfold energy
  simpa [pow_two, mul_assoc] using this

end OrderedField

end SheafGate

#print axioms SheafGate.dotProduct_lap
#print axioms SheafGate.energy_le_max
#print axioms SheafGate.lap_eq_zero_iff
#print axioms SheafGate.cob_eq_zero_iff_reachable_eq
#print axioms SheafGate.eq_zero_of_cob_of_harmonic