From 1fe51b2e04806cf399642793302b409479532782 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Fri, 12 Jul 2024 10:23:59 -0400
Subject: [PATCH] chore: namechange

---
 .../HiggsBoson/PointwiseInnerProd.lean        |  4 +-
 .../StandardModel/HiggsBoson/Potential.lean   | 40 +++++++++----------
 lakefile.toml                                 |  2 +-
 ...line_lint.lean => hepLean_style_lint.lean} | 16 +++++---
 4 files changed, 34 insertions(+), 28 deletions(-)
 rename scripts/{double_line_lint.lean => hepLean_style_lint.lean} (83%)

diff --git a/HepLean/StandardModel/HiggsBoson/PointwiseInnerProd.lean b/HepLean/StandardModel/HiggsBoson/PointwiseInnerProd.lean
index 0f53792..c3871fa 100644
--- a/HepLean/StandardModel/HiggsBoson/PointwiseInnerProd.lean
+++ b/HepLean/StandardModel/HiggsBoson/PointwiseInnerProd.lean
@@ -69,7 +69,7 @@ lemma innerProd_expand (φ1 φ2 : HiggsField) :
   nth_rewrite 1 [← RCLike.re_add_im (φ2 x 0)]
   nth_rewrite 1 [← RCLike.re_add_im (φ2 x 1)]
   ring_nf
-  repeat rw [show  RCLike.ofReal _ = ofReal' _ by rfl]
+  repeat rw [show RCLike.ofReal _ = ofReal' _ by rfl]
   simp only [Algebra.id.map_eq_id, RCLike.re_to_complex, RingHom.id_apply, RCLike.I_to_complex,
     RCLike.im_to_complex, I_sq, mul_neg, mul_one, neg_mul, sub_neg_eq_add, one_mul]
   ring
@@ -127,7 +127,7 @@ lemma toHiggsVec_norm (φ : HiggsField) (x : SpaceTime) :
     ‖φ x‖  = ‖φ.toHiggsVec x‖ := rfl
 
 lemma normSq_expand (φ : HiggsField)  :
-    φ.normSq  = fun x => (conj (φ x 0) * (φ x 0) + conj (φ x 1) * (φ x 1) ).re := by
+    φ.normSq = fun x => (conj (φ x 0) * (φ x 0) + conj (φ x 1) * (φ x 1)).re := by
   funext x
   simp [normSq, add_re, mul_re, conj_re, conj_im, neg_mul, sub_neg_eq_add, @norm_sq_eq_inner ℂ]
 
diff --git a/HepLean/StandardModel/HiggsBoson/Potential.lean b/HepLean/StandardModel/HiggsBoson/Potential.lean
index 44d4ce7..9b4c392 100644
--- a/HepLean/StandardModel/HiggsBoson/Potential.lean
+++ b/HepLean/StandardModel/HiggsBoson/Potential.lean
@@ -34,7 +34,7 @@ open SpaceTime
 
 /-- The Higgs potential of the form `- μ² * |φ|² + 𝓵 * |φ|⁴`. -/
 @[simp]
-def potential (μ2 𝓵 : ℝ ) (φ : HiggsField)  (x : SpaceTime) :  ℝ :=
+def potential (μ2 𝓵 : ℝ ) (φ : HiggsField) (x : SpaceTime) :  ℝ :=
   - μ2 * ‖φ‖_H ^ 2 x + 𝓵 * ‖φ‖_H ^ 2 x * ‖φ‖_H ^ 2 x
 
 /-!
@@ -43,7 +43,7 @@ def potential (μ2 𝓵 : ℝ ) (φ : HiggsField)  (x : SpaceTime) :  ℝ :=
 
 -/
 
-lemma potential_smooth (μSq lambda : ℝ)  (φ : HiggsField) :
+lemma potential_smooth (μSq lambda : ℝ) (φ : HiggsField) :
     Smooth 𝓘(ℝ, SpaceTime) 𝓘(ℝ, ℝ) (fun x => φ.potential μSq lambda x) := by
   simp only [potential, normSq, neg_mul]
   exact (smooth_const.smul φ.normSq_smooth).neg.add
@@ -56,7 +56,7 @@ namespace potential
 
 -/
 
-lemma complete_square (μ2 𝓵 : ℝ) (h : 𝓵 ≠ 0) (φ : HiggsField) (x : SpaceTime)  :
+lemma complete_square (μ2 𝓵 : ℝ) (h : 𝓵 ≠ 0) (φ : HiggsField) (x : SpaceTime) :
     potential μ2 𝓵 φ x = 𝓵 * (‖φ‖_H ^ 2 x - μ2 / (2 * 𝓵)) ^ 2 - μ2 ^ 2 / (4 * 𝓵) := by
   simp only [potential]
   field_simp
@@ -69,7 +69,7 @@ lemma complete_square (μ2 𝓵 : ℝ) (h : 𝓵 ≠ 0) (φ : HiggsField) (x : S
 -/
 
 /-- The proposition on the coefficents for a potential to be bounded. -/
-def IsBounded (μ2 𝓵 : ℝ)  : Prop :=
+def IsBounded (μ2 𝓵 : ℝ) : Prop :=
   ∃ c, ∀ Φ x, c ≤ potential μ2 𝓵 Φ x
 
 /-! TODO: Show when 𝓵 < 0, the potential is not bounded. -/
@@ -87,19 +87,19 @@ variable (h𝓵 : 0 < 𝓵)
 
 /-- The second term of the potential is non-negative. -/
 lemma snd_term_nonneg (φ : HiggsField) (x : SpaceTime) :
-    0 ≤ 𝓵 * ‖φ‖_H ^ 2 x *  ‖φ‖_H ^ 2 x := by
+    0 ≤ 𝓵 * ‖φ‖_H ^ 2 x * ‖φ‖_H ^ 2 x := by
   rw [mul_nonneg_iff]
   apply Or.inl
   simp_all only [normSq, gt_iff_lt, mul_nonneg_iff_of_pos_left, ge_iff_le, norm_nonneg, pow_nonneg,
     and_self]
 
 lemma as_quad (μ2 𝓵 : ℝ) (φ : HiggsField) (x : SpaceTime) :
-    𝓵  * ‖φ‖_H ^ 2 x * ‖φ‖_H ^ 2 x + (- μ2 ) * ‖φ‖_H ^ 2 x  + (- potential μ2 𝓵 φ x) = 0 := by
+    𝓵  * ‖φ‖_H ^ 2 x * ‖φ‖_H ^ 2 x + (- μ2 ) * ‖φ‖_H ^ 2 x + (- potential μ2 𝓵 φ x) = 0 := by
   simp only [normSq, neg_mul, potential, neg_add_rev, neg_neg]
   ring
 
 /-- The discriminant of the quadratic formed by the potential is non-negative. -/
-lemma discrim_nonneg  (φ : HiggsField) (x : SpaceTime) :
+lemma discrim_nonneg (φ : HiggsField) (x : SpaceTime) :
     0 ≤ discrim 𝓵 (- μ2) (- potential μ2 𝓵 φ x) := by
   have h1 := as_quad μ2 𝓵 φ x
   rw [quadratic_eq_zero_iff_discrim_eq_sq] at h1
@@ -111,7 +111,7 @@ lemma eq_zero_at (φ : HiggsField) (x : SpaceTime)
     (hV : potential μ2 𝓵 φ x = 0) : φ x = 0 ∨ ‖φ‖_H ^ 2 x = μ2 / 𝓵 := by
   have h1 := as_quad μ2 𝓵 φ x
   rw [hV] at h1
-  have h2 : ‖φ‖_H ^ 2 x * (𝓵  * ‖φ‖_H ^ 2 x + - μ2) = 0 := by
+  have h2 : ‖φ‖_H ^ 2 x * (𝓵 * ‖φ‖_H ^ 2 x + - μ2) = 0 := by
     linear_combination h1
   simp at h2
   cases' h2 with h2 h2
@@ -122,12 +122,12 @@ lemma eq_zero_at (φ : HiggsField) (x : SpaceTime)
   linear_combination h2
 
 lemma eq_zero_at_of_μSq_nonpos  {μ2 : ℝ} (hμ2 : μ2 ≤ 0)
-    (φ : HiggsField) (x : SpaceTime)  (hV : potential μ2 𝓵 φ x = 0) : φ x = 0 := by
+    (φ : HiggsField) (x : SpaceTime) (hV : potential μ2 𝓵 φ x = 0) : φ x = 0 := by
   cases' (eq_zero_at μ2 h𝓵 φ x hV) with h1 h1
   exact h1
   by_cases hμSqZ : μ2 = 0
   simpa [hμSqZ] using h1
-  refine ((?_ : ¬ 0 ≤  μ2 / 𝓵) (?_)).elim
+  refine ((?_ : ¬ 0 ≤ μ2 / 𝓵) (?_)).elim
   · simp_all [div_nonneg_iff]
     intro h
     exact lt_imp_lt_of_le_imp_le (fun _ => h) (lt_of_le_of_ne hμ2 hμSqZ)
@@ -135,7 +135,7 @@ lemma eq_zero_at_of_μSq_nonpos  {μ2 : ℝ} (hμ2 : μ2 ≤ 0)
     exact normSq_nonneg φ x
 
 lemma bounded_below (φ : HiggsField) (x : SpaceTime) :
-    - μ2 ^ 2 / (4 * 𝓵) ≤ potential μ2 𝓵 φ x  := by
+    - μ2 ^ 2 / (4 * 𝓵) ≤ potential μ2 𝓵 φ x := by
   have h1 := discrim_nonneg μ2 h𝓵 φ x
   simp only [discrim, even_two, Even.neg_pow, normSq, neg_mul, neg_add_rev, neg_neg] at h1
   ring_nf at h1
@@ -145,7 +145,7 @@ lemma bounded_below (φ : HiggsField) (x : SpaceTime) :
   ring_nf at h2 ⊢
   exact h2
 
-lemma bounded_below_of_μSq_nonpos  {μ2 : ℝ}
+lemma bounded_below_of_μSq_nonpos {μ2 : ℝ}
     (hμSq : μ2 ≤ 0) (φ : HiggsField) (x : SpaceTime) : 0 ≤ potential μ2 𝓵 φ x := by
   refine add_nonneg ?_ (snd_term_nonneg h𝓵 φ x)
   field_simp [mul_nonpos_iff]
@@ -165,7 +165,7 @@ variable (h𝓵 : 0 < 𝓵)
 -/
 
 lemma discrim_eq_zero_of_eq_bound (φ : HiggsField) (x : SpaceTime)
-    (hV : potential μ2 𝓵 φ x  = - μ2 ^ 2 / (4  * 𝓵)) :
+    (hV : potential μ2 𝓵 φ x  = - μ2 ^ 2 / (4 * 𝓵)) :
     discrim 𝓵 (- μ2) (- potential μ2 𝓵 φ x) = 0 := by
   rw [discrim, hV]
   field_simp
@@ -180,36 +180,36 @@ lemma normSq_of_eq_bound (φ : HiggsField) (x : SpaceTime)
   exact ne_of_gt h𝓵
 
 lemma eq_bound_iff (φ : HiggsField) (x : SpaceTime) :
-    potential μ2 𝓵 φ x  = - μ2 ^ 2 / (4  * 𝓵) ↔ ‖φ‖_H ^ 2 x = μ2 / (2 * 𝓵) :=
+    potential μ2 𝓵 φ x = - μ2 ^ 2 / (4  * 𝓵) ↔ ‖φ‖_H ^ 2 x = μ2 / (2 * 𝓵) :=
   Iff.intro (normSq_of_eq_bound μ2 h𝓵 φ x)
     (fun h ↦ by
       rw [potential, h]
       field_simp
       ring_nf)
 
-lemma eq_bound_iff_of_μSq_nonpos  {μ2 : ℝ}
+lemma eq_bound_iff_of_μSq_nonpos {μ2 : ℝ}
     (hμ2 : μ2 ≤ 0) (φ : HiggsField) (x : SpaceTime) :
     potential μ2 𝓵 φ x = 0 ↔ φ x = 0 :=
   Iff.intro (fun h ↦ eq_zero_at_of_μSq_nonpos h𝓵 hμ2 φ x h)
   (fun h ↦ by simp [potential, h])
 
 lemma eq_bound_IsMinOn (φ : HiggsField) (x : SpaceTime)
-    (hv : potential μ2 𝓵 φ x = - μ2 ^ 2 / (4  * 𝓵)) :
+    (hv : potential μ2 𝓵 φ x = - μ2 ^ 2 / (4 * 𝓵)) :
     IsMinOn (fun (φ, x) => potential μ2 𝓵 φ x) Set.univ (φ, x) := by
   rw [isMinOn_univ_iff]
   simp only [normSq, neg_mul, le_neg_add_iff_add_le, ge_iff_le, hv]
   exact fun (φ', x') ↦ bounded_below μ2 h𝓵 φ' x'
 
-lemma eq_bound_IsMinOn_of_μSq_nonpos  {μ2 : ℝ}
+lemma eq_bound_IsMinOn_of_μSq_nonpos {μ2 : ℝ}
     (hμ2 : μ2 ≤ 0) (φ : HiggsField) (x : SpaceTime) (hv : potential μ2 𝓵 φ x = 0) :
     IsMinOn (fun (φ, x) => potential μ2 𝓵 φ x) Set.univ (φ, x) := by
   rw [isMinOn_univ_iff]
   simp only [normSq, neg_mul, le_neg_add_iff_add_le, ge_iff_le, hv]
   exact fun (φ', x') ↦ bounded_below_of_μSq_nonpos h𝓵 hμ2 φ' x'
 
-lemma bound_reached_of_μSq_nonneg  {μ2 : ℝ} (hμ2 : 0 ≤ μ2) :
+lemma bound_reached_of_μSq_nonneg {μ2 : ℝ} (hμ2 : 0 ≤ μ2) :
     ∃ (φ : HiggsField) (x : SpaceTime),
-    potential μ2 𝓵 φ x = - μ2 ^ 2 / (4  * 𝓵) := by
+    potential μ2 𝓵 φ x = - μ2 ^ 2 / (4 * 𝓵) := by
   use HiggsVec.toField ![√(μ2/(2 * 𝓵)), 0], 0
   refine (eq_bound_iff μ2 h𝓵 (HiggsVec.toField ![√(μ2/(2 * 𝓵)), 0]) 0).mpr ?_
   simp only [normSq, HiggsVec.toField, ContMDiffSection.coeFn_mk, PiLp.norm_sq_eq_of_L2,
@@ -218,7 +218,7 @@ lemma bound_reached_of_μSq_nonneg  {μ2 : ℝ} (hμ2 : 0 ≤ μ2) :
     not_false_eq_true, zero_pow, add_zero]
   field_simp [mul_pow]
 
-lemma IsMinOn_iff_of_μSq_nonneg  {μ2 : ℝ} (hμ2 : 0 ≤ μ2) :
+lemma IsMinOn_iff_of_μSq_nonneg {μ2 : ℝ} (hμ2 : 0 ≤ μ2) :
     IsMinOn (fun (φ, x) => potential μ2 𝓵 φ x) Set.univ (φ, x) ↔
     ‖φ‖_H ^ 2 x = μ2 /(2 * 𝓵) := by
   apply Iff.intro <;> rw [← eq_bound_iff μ2 h𝓵 φ]
diff --git a/lakefile.toml b/lakefile.toml
index bf4acda..a035d1f 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -39,7 +39,7 @@ name = "type_former_lint"
 srcDir = "scripts"
 
 [[lean_exe]]
-name = "double_line_lint"
+name = "hepLean_style_lint"
 srcDir = "scripts"
 
 [[lean_exe]]
diff --git a/scripts/double_line_lint.lean b/scripts/hepLean_style_lint.lean
similarity index 83%
rename from scripts/double_line_lint.lean
rename to scripts/hepLean_style_lint.lean
index b39e7d8..96dbfc1 100644
--- a/scripts/double_line_lint.lean
+++ b/scripts/hepLean_style_lint.lean
@@ -19,7 +19,7 @@ Parts of this file are adapted from `Mathlib.Tactic.Linter.TextBased`,
 open Lean System Meta
 
 /-- Given a list of lines, outputs an error message and a line number. -/
-def HepLeanTextLinter : Type := Array String → Array (String × ℕ)
+def HepLeanTextLinter : Type := Array String → Array (String × ℕ × ℕ)
 
 /-- Checks if there are two consecutive empty lines. -/
 def doubleEmptyLineLinter : HepLeanTextLinter := fun lines ↦ Id.run do
@@ -27,7 +27,7 @@ def doubleEmptyLineLinter : HepLeanTextLinter := fun lines ↦ Id.run do
   let pairLines := List.zip enumLines (List.tail! enumLines)
   let errors := pairLines.filterMap (fun ((lno1, l1), _, l2) ↦
     if l1.length == 0 && l2.length == 0  then
-      some (s!" Double empty line. ", lno1)
+      some (s!" Double empty line. ", lno1, 1)
     else none)
   errors.toArray
 
@@ -36,7 +36,11 @@ def doubleSpaceLinter : HepLeanTextLinter := fun lines ↦ Id.run do
   let enumLines := (lines.toList.enumFrom 1)
   let errors := enumLines.filterMap (fun (lno, l) ↦
     if String.containsSubstr l.trimLeft "  " then
-      some (s!" Non-initial double space in line. ", lno)
+      let k := (Substring.findAllSubstr l "  ").toList.getLast?
+      let col := match k with
+        | none => 1
+        | some k => k.stopPos.byteIdx
+      some (s!" Non-initial double space in line.", lno, col)
     else none)
   errors.toArray
 
@@ -45,17 +49,19 @@ structure HepLeanErrorContext where
   error : String
   /-- The line number -/
   lineNumber : ℕ
+  /-- The column number -/
+  columnNumber : ℕ
   /-- The file path -/
   path : FilePath
 
 def printErrors (errors : Array HepLeanErrorContext) : IO Unit := do
   for e in errors do
-    IO.println (s!"error: {e.path}:{e.lineNumber}: {e.error}")
+    IO.println (s!"error: {e.path}:{e.lineNumber}:{e.columnNumber}: {e.error}")
 
 def hepLeanLintFile (path : FilePath) : IO Bool := do
   let lines ← IO.FS.lines path
   let allOutput := (Array.map (fun lint ↦
-    (Array.map (fun (e, n) ↦ HepLeanErrorContext.mk e n path)) (lint lines)))
+    (Array.map (fun (e, n, c) ↦ HepLeanErrorContext.mk e n c path)) (lint lines)))
     #[doubleEmptyLineLinter, doubleSpaceLinter]
   let errors := allOutput.flatten
   printErrors errors