essence equal relation in Lean

Here’s a minimal Lean 4 file (trinity.lean) that captures the logical skeleton described earlier: one essence (D), three concrete “persons” (F, S, Sp), pair-wise opposition (inequalities), and an exhaustive principle showing that every inhabitant of D is one of those three. Paste this into any Lean 4 environment (VS Code with the Lean extension, or https://leanprover.github.io/online/) and the kernel will confirm each proof.

/-
  trinity.lean
  A toy formalisation of “relation = essence + opposed relations” as discussed
  in the relational-first synthesis of divine simplicity and real Trinity.
  -------------------------------------------------------------
  D      : the one, simple divine essence (a Type with 3 constructors)
  F S Sp : constants standing for Father, Son, Spirit
  Objective:
      • show they are pair-wise distinct  (opposition)
      • show any inhabitant of D must coincide with one of them (exhaustion)
-/

-- ONE ESSENCE WITH THREE CONSTRUCTORS
inductive D : Type
| F : D   -- Father  (source‐gift)
| S : D   -- Son     (return‐gift)
| Sp : D  -- Spirit  (communion‐gift)

open D

/-
  EXHAUSTION LEMMA
  Lean’s `cases` tactic performs case analysis on `x : D`.
  The three reflexive equalities establish that every `x`
  is definitionally identical with exactly one constructor.
-/
theorem D.exhaustive (x : D) : x = F ∨ x = S ∨ x = Sp := by
  cases x with
  | F  => exact Or.inl rfl
  | S  => exact Or.inr <| Or.inl rfl
  | Sp => exact Or.inr <| Or.inr rfl

/-
  OPPOSITION LEMMAS
  Each inequality is proved by contradiction: if `F = S`, `cases` collapses
  constructors and Lean’s kernel sees an impossible identification.
-/
theorem F_ne_S  : (F : D) ≠ S  := by intro h; cases h  -- F and S opposed
theorem F_ne_Sp : (F : D) ≠ Sp := by intro h; cases h  -- F and Sp opposed
theorem S_ne_Sp : (S : D) ≠ Sp := by intro h; cases h  -- S and Sp opposed

What the kernel guarantees

• inductive D creates one and only one “essence” type with three concrete values.
• D.exhaustive proves ∀ x : D, x = F ∨ x = S ∨ x = Sp, mirroring “no fourth person.”
• The three *_ne_* theorems embed opposition—the irreducible relational differences.

Thus, Lean’s core logic enforces exactly what the theological argument claims: once relation is identical with essence and certain relations stand in mutual opposition, the Trinity (three and only three irreducible instances of the one essence) follows with mechanical certainty and without hidden metaphysical “parts.”