/-
Orthogonaliteit van het decompositie-lemma, machinale verificatie (13-8-2026).

Setting: H een reële inproductruimte (de L²-raakruimte T_C𝒞),
S : H → ℝ de actie/weerstandsfunctionaal.

Drie stellingen die samen het geometrische hart van het
decompositie-lemma S = A + K + I dragen:

1. richting_annihilatie: is S constant langs een kromme (een
   gauge-orbit), dan annihileert dS de richtingsvector van die
   kromme. In inproduct-taal: ∇S ⊥ T_r, overal. Dus de
   gradiëntstroom (T_t = span ∇S) staat loodrecht op de
   gauge-richtingen: A en K tellen disjuncte richtingen.

2. orbit_kritiek: is S invariant onder een lineaire isometrie U
   en is x kritiek, dan is ook U x kritiek: de hele orbit door
   een kritiek punt is kritiek.

3. hessiaan_annihileert_orbit: ligt een kromme geheel in de
   kritieke verzameling (zoals de orbit uit stelling 2), dan
   annihileert de Hessiaan (de afgeleide van y ↦ dS(y)) de
   richtingsvector. Dus Hess S is nul op T_r: I telt alleen de
   transversale richtingen, K en I tellen niets dubbel.

De splitsing T = T_r ⊕ T_t ⊕ T_h volgt hieruit met standaard
lineaire algebra: T_t ⊥ T_r door stelling 1, T_h := (T_r ⊕ T_t)^⊥
per constructie, en de Hessiaan is blok-diagonaal over de
splitsing op kritieke punten door stelling 3 (een symmetrische
bilineaire vorm die nul is op een deelruimte heeft geen
kruistermen met die deelruimte).
-/
import Mathlib

open ContinuousLinearMap

namespace EEML

variable {H : Type*} [NormedAddCommGroup H] [NormedSpace ℝ H]

/-- Stelling 1: invariantie langs een kromme annihileert de richting.
    (Met L = dS en γ de gauge-orbit: ∇S ⊥ gauge-richting, overal.) -/
theorem richting_annihilatie (S : H → ℝ)
    (γ : ℝ → H) (x : H) (ξ : H) (L : H →L[ℝ] ℝ)
    (hγ0 : γ 0 = x) (hγ : HasDerivAt γ ξ 0)
    (hS : HasFDerivAt S L x)
    (hinv : ∀ t, S (γ t) = S x) :
    L ξ = 0 := by
  have hx : HasFDerivAt S L (γ 0) := by rw [hγ0]; exact hS
  have hcomp : HasDerivAt (fun t => S (γ t)) (L ξ) 0 :=
    hx.comp_hasDerivAt 0 hγ
  have hconst : (fun t => S (γ t)) = fun _ => S x := funext hinv
  have hzero : HasDerivAt (fun t => S (γ t)) 0 0 := by
    rw [hconst]; exact hasDerivAt_const 0 (S x)
  exact hcomp.unique hzero

/-- Stelling 2: de orbit van een kritiek punt onder een S-invariante
    continue lineaire equivalentie is kritiek. -/
theorem orbit_kritiek (S : H → ℝ)
    (U : H ≃L[ℝ] H) (hU : ∀ y, S (U y) = S y)
    (x : H) (hcrit : HasFDerivAt S (0 : H →L[ℝ] ℝ) x) :
    HasFDerivAt S (0 : H →L[ℝ] ℝ) (U x) := by
  have hSU : (fun z => S (U.symm z)) = S := by
    funext z
    conv_rhs => rw [← U.apply_symm_apply z]
    rw [hU]
  have h1 : HasFDerivAt S (0 : H →L[ℝ] ℝ) (U.symm (U x)) := by
    rw [U.symm_apply_apply]; exact hcrit
  have h2 : HasFDerivAt (fun z => U.symm z)
      (U.symm : H →L[ℝ] H) (U x) := U.symm.toContinuousLinearMap.hasFDerivAt
  have h3 : HasFDerivAt (fun z => S (U.symm z))
      ((0 : H →L[ℝ] ℝ).comp (U.symm : H →L[ℝ] H)) (U x) := h1.comp (U x) h2
  rw [hSU, zero_comp] at h3
  exact h3

/-- Stelling 3: ligt een kromme in de kritieke verzameling, dan
    annihileert de Hessiaan (afgeleide van y ↦ dS y) haar richting:
    Hess S (ξ, ·) = 0 op de orbit-richtingen. -/
theorem hessiaan_annihileert_orbit (S : H → ℝ)
    (γ : ℝ → H) (x ξ : H) (B : H →L[ℝ] H →L[ℝ] ℝ)
    (hγ0 : γ 0 = x) (hγ : HasDerivAt γ ξ 0)
    (hHess : HasFDerivAt (fun y => fderiv ℝ S y) B x)
    (horb : ∀ t, fderiv ℝ S (γ t) = 0) :
    B ξ = 0 := by
  have hx : HasFDerivAt (fun y => fderiv ℝ S y) B (γ 0) := by
    rw [hγ0]; exact hHess
  have hcomp : HasDerivAt (fun t => fderiv ℝ S (γ t)) (B ξ) 0 :=
    hx.comp_hasDerivAt 0 hγ
  have hconst : (fun t => fderiv ℝ S (γ t)) = fun _ => (0 : H →L[ℝ] ℝ) :=
    funext horb
  have hzero : HasDerivAt (fun t => fderiv ℝ S (γ t)) (0 : H →L[ℝ] ℝ) 0 := by
    rw [hconst]; exact hasDerivAt_const 0 (0 : H →L[ℝ] ℝ)
  exact hcomp.unique hzero

/-- Gevolg: op een kritiek punt annihileert de Hessiaan elke
    orbit-richting van een S-invariante één-parameter-familie van
    continue lineaire equivalenties. -/
theorem hessiaan_nul_op_gauge (S : H → ℝ)
    (U : ℝ → H ≃L[ℝ] H) (hU : ∀ t y, S (U t y) = S y)
    (x ξ : H) (B : H →L[ℝ] H →L[ℝ] ℝ)
    (hU0 : U 0 x = x)
    (hγ : HasDerivAt (fun t => U t x) ξ 0)
    (hHess : HasFDerivAt (fun y => fderiv ℝ S y) B x)
    (hcrit : HasFDerivAt S (0 : H →L[ℝ] ℝ) x)
    :
    B ξ = 0 := by
  apply hessiaan_annihileert_orbit S (fun t => U t x) x ξ B hU0 hγ hHess
  intro t
  have h := orbit_kritiek S (U t) (hU t) x hcrit
  exact h.fderiv

end EEML

#print axioms EEML.richting_annihilatie
#print axioms EEML.orbit_kritiek
#print axioms EEML.hessiaan_annihileert_orbit
#print axioms EEML.hessiaan_nul_op_gauge