feat: Semiformal results around Em (#441)

* feat: Add tags

* feat: Add tags to YML

* refactor: Lint

* feat: Sort TODOs

* feat: Add semi-formal results

* feat: fix name

* refactor: Lint

* feat: semi-formal results around EM

* feat: Lint and make tags function

.github/ISSUE_TEMPLATE/Bump.yml

@@ -44,6 +44,7 @@ body:
       - label: Ensure `lake exe TODO_to_yml mkFile` runs without errors.
       - label: Ensure `lake exe stats mkHTML` runs without errors.
       - label: Ensure `lake exe informal mkFile mkDot mkHTML` runs without errors.
+      - label: Ensure `lake exe make_tag` runs without errors.
   validations:
     required: false
 - type: checkboxes

PhysLean.lean

@@ -6,6 +6,7 @@ import PhysLean.Cosmology.Basic
 import PhysLean.Electromagnetism.Basic
 import PhysLean.Electromagnetism.FieldStrength.Basic
 import PhysLean.Electromagnetism.FieldStrength.Derivative
+import PhysLean.Electromagnetism.LorentzAction
 import PhysLean.Electromagnetism.MaxwellEquations
 import PhysLean.Mathematics.Fin
 import PhysLean.Mathematics.Fin.Involutions

PhysLean/Electromagnetism/FieldStrength/Basic.lean

@@ -18,7 +18,7 @@ open TensorTree in
 /-- The Field strength is a tensor `F^μ^ν` which is anti-symmetric.. -/
 noncomputable abbrev FieldStrength (d : ℕ := 3) :
     Submodule ℝ (ℝT[d, .up] → ℝT[d, .up, .up]) where
-  carrier F := ∀ x, {F x | μ ν = - (F x| ν μ)}ᵀ
+  carrier F := ∀ x, {F x | μ ν = - (F x | ν μ)}ᵀ
   add_mem' {F1 F2} hF1 hF2:= by
     intro x
     simp only [C_eq_color, Nat.succ_eq_add_one, Nat.reduceAdd, Pi.add_apply,
@@ -456,7 +456,4 @@ TODO "6V2OU" "Define the dual field strength."
 
 end FieldStrength
 
-TODO "6V2O4" "Show that the isomorphism between `ElectricField d × MagneticField d` and
-  `ElectricField d × MagneticField d` is equivariant with respect to the Lorentz group."
-
 end Electromagnetism

PhysLean/Electromagnetism/LorentzAction.lean

@@ -0,0 +1,42 @@
+/-
+Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Tooby-Smith
+-/
+import PhysLean.Electromagnetism.Basic
+import PhysLean.Meta.Informal.SemiFormal
+import PhysLean.Electromagnetism.FieldStrength.Basic
+
+/-!
+
+# The Lorentz action on the electric and magnetic fields.
+
+The Lorentz group acts on a pair of a electric and magnetic field.
+The map `toElectricMagneticField` is equivariant, which turns a field strength into a pair of
+electric and magnetic fieldd, is equivariant with respect to this action.
+
+## TODO
+
+This file currently only contains semiformal results, which
+-/
+
+namespace Electromagnetism
+
+/-- The Lorentz action on the electric and magnetic fields. -/
+semiformal_result "6WNUS" lorentzAction (d : ℕ) :
+  MulAction (LorentzGroup d) (ElectricField d × MagneticField d)
+
+open FieldStrength
+
+/-- The equivalence `toElectricMagneticField` is equivariant with respect to the
+  group action.
+
+  (In this semiformal result `lorentzActionTemp` should be replaced with `lorentzAction`.) -/
+semiformal_result "6V2O4" toElectricMagneticField_equivariant (d : ℕ)
+  (g : LorentzGroup 3) (E : ElectricField 3) (B : MagneticField 3)
+  (lorentzActionTemp : (LorentzGroup 3) → (ElectricField  × MagneticField)
+    → (ElectricField  × MagneticField )) (x : SpaceTime) :
+  (toElectricMagneticField.symm (lorentzActionTemp g  (E, B))).1  x=
+  (realLorentzTensor.F.obj _).ρ g ((toElectricMagneticField.symm (E, B)).1 x)
+
+end Electromagnetism

PhysLean/Electromagnetism/MaxwellEquations.lean

@@ -20,7 +20,7 @@ structure EMSystem where
   /-- The permittivity. -/
   ε₀ : ℝ
 
-TODO "6V2UZ" "Charge density and current desnity should be generalized to signed measures,
+TODO "6V2UZ" "Charge density and current density should be generalized to signed measures,
   in such a way
   that they are still easy to work with and can be integrated with with tensor notation.
   See here:

lakefile.toml

@@ -98,6 +98,11 @@ name = "redundent_imports"
 supportInterpreter = true
 srcDir = "scripts/MetaPrograms"
 
+[[lean_exe]]
+name = "make_tag"
+supportInterpreter = true
+srcDir = "scripts/MetaPrograms"
+
 # -- Optional inclusion of openAI_doc_check. Needs `llm` above.
 #[[lean_exe]]
 #name = "openAI_doc_check"

scripts/MetaPrograms/make_tag.lean

@@ -0,0 +1,95 @@
+/-
+Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import Init.System.IO
+import Std.Time.Zoned
+/-!
+
+# Making tags
+
+This file returns tags which can be used for TODO items, informal lemmas,
+informal definitions and semiformal results.
+
+Run it with `lake exe make_tag`.
+
+## Attributes
+
+The `digit` part of this file is modified from the module
+
+`Mathlib.Data.Nat.Digits`
+
+released under the Apache 2.0 license, Copyright (c) 2020 Kim Morrison,
+Authors: Kim Morrison, Shing Tak Lam, Mario Carneiro
+
+-/
+open Std.Time
+/-!
+
+# digit
+
+-/
+
+/- The RFC 4648 Base32 -/
+def digitChar (n : Nat) : Char :=
+  if n = 0 then 'A' else
+  if n = 1 then 'B' else
+  if n = 2 then 'C' else
+  if n = 3 then 'D' else
+  if n = 4 then 'E' else
+  if n = 5 then 'F' else
+  if n = 6 then 'G' else
+  if n = 7 then 'H' else
+  if n = 8 then 'I' else
+  if n = 9 then 'J' else
+  if n = 10 then 'K' else
+  if n = 11 then 'L' else
+  if n = 12 then 'M' else
+  if n = 13 then 'N' else
+  if n = 14 then 'O' else
+  if n = 15 then 'P' else
+  if n = 16 then 'Q' else
+  if n = 17 then 'R' else
+  if n = 18 then 'S' else
+  if n = 19 then 'T' else
+  if n = 20 then 'U' else
+  if n = 21 then 'V' else
+  if n = 22 then 'W' else
+  if n = 23 then 'X' else
+  if n = 24 then 'Y' else
+  if n = 25 then 'Z' else
+  if n = 26 then '2' else
+  if n = 27 then '3' else
+  if n = 28 then '4' else
+  if n = 29 then '5' else
+  if n = 30 then '6' else
+  if n = 31 then '7' else
+  '*'
+
+def toDigitsCore (base : Nat) : Nat → Nat → List Char → List Char
+  | 0,      _, ds => ds
+  | fuel+1, n, ds =>
+    let d  := digitChar <| n % base;
+    let n' := n / base;
+    if n' = 0 then d::ds
+    else toDigitsCore base fuel n' (d::ds)
+
+def toDigits (base : Nat) (n : Nat) : List Char :=
+  toDigitsCore base (n+1) n []
+
+/-!
+
+## Main function
+
+-/
+unsafe def main (_ : List String) : IO Unit := do
+  let timeNow ← Timestamp.now
+  let timeString := toString timeNow
+  let timeNat := match timeString.toNat? with
+    | some n => n
+    | none => panic! "Failed to convert timeString to Nat"
+  let digits := toDigits 32 timeNat
+  let tag := String.mk (digits.drop 2)
+  println! tag
+  pure ()