From ba5312b53054a5210cbfad4172b4d9a9b7a64f46 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Tue, 19 Nov 2024 11:19:25 +0000
Subject: [PATCH] feat: basic structures for Two Real Scalars

---
 HepLean.lean                                  |  1 +
 .../Instances/TwoRealScalar.lean              | 48 +++++++++++++++++++
 2 files changed, 49 insertions(+)
 create mode 100644 HepLean/FeynmanDiagrams/Instances/TwoRealScalar.lean

diff --git a/HepLean.lean b/HepLean.lean
index c6d92878..03a4b30a 100644
--- a/HepLean.lean
+++ b/HepLean.lean
@@ -54,6 +54,7 @@ import HepLean.BeyondTheStandardModel.TwoHDM.GaugeOrbits
 import HepLean.FeynmanDiagrams.Basic
 import HepLean.FeynmanDiagrams.Instances.ComplexScalar
 import HepLean.FeynmanDiagrams.Instances.Phi4
+import HepLean.FeynmanDiagrams.Instances.TwoRealScalar
 import HepLean.FeynmanDiagrams.Momentum
 import HepLean.FlavorPhysics.CKMMatrix.Basic
 import HepLean.FlavorPhysics.CKMMatrix.Invariants
diff --git a/HepLean/FeynmanDiagrams/Instances/TwoRealScalar.lean b/HepLean/FeynmanDiagrams/Instances/TwoRealScalar.lean
new file mode 100644
index 00000000..b61fff76
--- /dev/null
+++ b/HepLean/FeynmanDiagrams/Instances/TwoRealScalar.lean
@@ -0,0 +1,48 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.FeynmanDiagrams.Basic
+/-!
+
+# Feynman rules for a two complex scalar fields
+
+This file serves as a demonstration of a new approach to Feynman rules.
+
+-/
+
+namespace TwoComplexScalar
+open CategoryTheory
+open FeynmanDiagram
+open PreFeynmanRule
+
+/-- The colors of edges which one can associate with a vertex for a theory
+  with two complex scalar fields. -/
+inductive 𝓔 where
+  /-- Corresponds to the first complex scalar field flowing out of a vertex. -/
+  | complexScalarOut₁ : 𝓔
+  /-- Corresponds to the first complex scalar field flowing into a vertex. -/
+  | complexScalarIn₁ : 𝓔
+  /-- Corresponds to the second complex scalar field flowing out of a vertex. -/
+  | complexScalarOut₂ : 𝓔
+  /-- Corresponds to the second complex scalar field flowing into a vertex. -/
+  | complexScalarIn₂ : 𝓔
+
+/-- The map taking each color to it's dual, specifying how we can contract edges. -/
+def ξ : 𝓔 → 𝓔
+  | 𝓔.complexScalarOut₁ => 𝓔.complexScalarIn₁
+  | 𝓔.complexScalarIn₁ => 𝓔.complexScalarOut₁
+  | 𝓔.complexScalarOut₂ => 𝓔.complexScalarIn₂
+  | 𝓔.complexScalarIn₂ => 𝓔.complexScalarOut₂
+
+/-- The function `ξ` is an involution. -/
+lemma ξ_involutive : Function.Involutive ξ := by
+  intro x
+  match x with
+  | 𝓔.complexScalarOut₁ => rfl
+  | 𝓔.complexScalarIn₁ => rfl
+  | 𝓔.complexScalarOut₂ => rfl
+  | 𝓔.complexScalarIn₂ => rfl
+
+end TwoComplexScalar