From b558daec92c06ed60c3de92f469eae4fd01fde47 Mon Sep 17 00:00:00 2001
From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com>
Date: Wed, 11 Mar 2026 09:30:16 +0000
Subject: [PATCH 01/14] feat: mfderiv for Space
---
PhysLean/SpaceAndTime/Space/Basic.lean | 31 +++++++
.../SpaceAndTime/Space/Derivatives/Basic.lean | 35 ++++++++
PhysLean/SpaceAndTime/Space/Module.lean | 90 ++++++++++++++++++-
3 files changed, 155 insertions(+), 1 deletion(-)
diff --git a/PhysLean/SpaceAndTime/Space/Basic.lean b/PhysLean/SpaceAndTime/Space/Basic.lean
index a5cf96d16..6995881b6 100644
--- a/PhysLean/SpaceAndTime/Space/Basic.lean
+++ b/PhysLean/SpaceAndTime/Space/Basic.lean
@@ -12,6 +12,7 @@ public import Mathlib.Topology.ContinuousMap.CompactlySupported
public import Mathlib.Geometry.Manifold.IsManifold.Basic
public import Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
public import Mathlib.Analysis.InnerProductSpace.Calculus
+public import Mathlib.Geometry.Manifold.Diffeomorph
/-!
# Space
@@ -288,4 +289,34 @@ noncomputable def manifoldStructure (d : ℕ) :
simp only [Equiv.coe_vaddConst]
fun_prop
+@[simp]
+lemma manifoldStructure_comp_manifoldStructure_symm {d : ℕ} :
+ (↑(manifoldStructure d) ∘ ↑(manifoldStructure d).symm) = id := by
+ ext1 x
+ simpa using (manifoldStructure d).right_inv' (x := x) (by simp [manifoldStructure])
+
+@[simp]
+lemma range_manifoldStructure {d : ℕ} :
+ (Set.range ↑(manifoldStructure d)) = Set.univ := by
+ ext x
+ simp
+ use (manifoldStructure d).symm x
+ change (↑(manifoldStructure d) ∘ ↑(manifoldStructure d).symm) x = x
+ rw [manifoldStructure_comp_manifoldStructure_symm]
+ simp
+
+
+open Manifold in
+lemma contMDiff_vaddConst (d : ℕ) : ContMDiff
+ (manifoldStructure d) (𝓘(ℝ, EuclideanSpace ℝ (Fin d))) ⊤ (manifoldStructure d).toFun := by
+ rw [contMDiff_iff]
+ refine ⟨(manifoldStructure d).continuous_toFun, fun x y ↦ ?_⟩
+ simp only [extChartAt, OpenPartialHomeomorph.extend, OpenPartialHomeomorph.refl_partialEquiv,
+ PartialEquiv.refl_source, OpenPartialHomeomorph.singletonChartedSpace_chartAt_eq,
+ modelWithCornersSelf_partialEquiv, PartialEquiv.trans_refl, PartialEquiv.refl_coe,
+ ModelWithCorners.toPartialEquiv_coe, PartialEquiv.refl_trans,
+ ModelWithCorners.toPartialEquiv_coe_symm, manifoldStructure_comp_manifoldStructure_symm,
+ CompTriple.comp_eq, ModelWithCorners.target_eq, Set.preimage_univ, Set.inter_univ]
+ exact contDiffOn_id
+
end Space
diff --git a/PhysLean/SpaceAndTime/Space/Derivatives/Basic.lean b/PhysLean/SpaceAndTime/Space/Derivatives/Basic.lean
index 4d0efb353..82fad86d3 100644
--- a/PhysLean/SpaceAndTime/Space/Derivatives/Basic.lean
+++ b/PhysLean/SpaceAndTime/Space/Derivatives/Basic.lean
@@ -100,6 +100,41 @@ lemma deriv_eq_mfderiv {M d} [NormedAddCommGroup M] [NormedSpace ℝ M]
rw [deriv_eq_fderiv_basis, ← mfderiv_eq_fderiv]
rfl
+open Manifold in
+/-- The spatial-derivative in terms of the derivative of functions between
+ manifolds with the manifold structure `Space.manifoldStructure d`.
+ This should eventually be used as the definition of `deriv`. -/
+lemma deriv_eq_mfderiv_manifoldStructure {M d} [NormedAddCommGroup M] [NormedSpace ℝ M]
+ (μ : Fin d) (f : Space d → M) (hf : Differentiable ℝ f) (x : Space d) :
+ deriv μ f x = mfderiv (Space.manifoldStructure d) 𝓘(ℝ, M) f x (EuclideanSpace.single μ 1) := by
+ rw [deriv_eq_mfderiv]
+ change _ = mfderiv (Space.manifoldStructure d) 𝓘(ℝ, M)
+ (f ∘ modelDiffeo) x (EuclideanSpace.single μ 1)
+ rw [mfderiv_comp (I' := 𝓘(ℝ, Space d))]
+ rotate_left
+ · exact hf.mdifferentiable.mdifferentiableAt
+ · exact MDifferentiable.mdifferentiableAt <|
+ Diffeomorph.mdifferentiable modelDiffeo WithTop.top_ne_zero
+ simp only [Function.comp_apply, modelDiffeo_apply, mfderiv_eq_fderiv,
+ ContinuousLinearMap.coe_comp']
+ congr 1
+ simp [mfderiv]
+ rw [if_pos]
+ rotate_left
+ · exact MDifferentiable.mdifferentiableAt <|
+ Diffeomorph.mdifferentiable modelDiffeo WithTop.top_ne_zero
+ change _ = (fderiv ℝ (↑(manifoldStructure d).symm) ((manifoldStructure d) x))
+ (EuclideanSpace.single μ 1)
+ simp [manifoldStructure]
+ ext i
+ rw [fderiv_space_components _ _ (by fun_prop)]
+ simp only [vadd_apply, fderiv_add_const]
+ change _ = (fderiv ℝ (EuclideanSpace.proj i) (x -ᵥ Classical.choice _))
+ (EuclideanSpace.single μ 1)
+ simp [basis_apply]
+ congr 1
+ exact Eq.propIntro (fun a => id (Eq.symm a)) fun a => id (Eq.symm a)
+
/-!
### A.2. Derivative of the constant function
diff --git a/PhysLean/SpaceAndTime/Space/Module.lean b/PhysLean/SpaceAndTime/Space/Module.lean
index 545b568d0..5f007a73b 100644
--- a/PhysLean/SpaceAndTime/Space/Module.lean
+++ b/PhysLean/SpaceAndTime/Space/Module.lean
@@ -6,6 +6,7 @@ Authors: Joseph Tooby-Smith
module
public import PhysLean.SpaceAndTime.Space.Basic
+public import Mathlib.Geometry.Manifold.Diffeomorph
/-!
# The structure of a module on Space
@@ -474,6 +475,12 @@ def equivPi (d : ℕ) :
invFun := fun f => ⟨f⟩
}
+/-!
+
+## Basic differentiablity conditions
+
+-/
+
@[fun_prop]
lemma mk_continuous {d : ℕ} :
Continuous (fun (f : Fin d → ℝ) => (⟨f⟩ : Space d)) := (equivPi d).symm.continuous
@@ -483,7 +490,7 @@ lemma mk_differentiable {d : ℕ} :
Differentiable ℝ (fun (f : Fin d → ℝ) => (⟨f⟩ : Space d)) := (equivPi d).symm.differentiable
@[fun_prop]
-lemma mk_contDiff {d n : ℕ} :
+lemma mk_contDiff {d : ℕ} {n : WithTop ℕ∞}:
ContDiff ℝ n (fun (f : Fin d → ℝ) => (⟨f⟩ : Space d)) := (equivPi d).symm.contDiff
@[simp]
@@ -498,6 +505,50 @@ lemma fderiv_val {d : ℕ} (p : Space d) :
change fderiv ℝ (equivPi d) p = _
rw [@ContinuousLinearEquiv.fderiv]
+@[fun_prop]
+lemma contDiffOn_vadd (s : Space d) :
+ ContDiffOn ℝ ω (fun (v : EuclideanSpace ℝ (Fin d)) => v +ᵥ s) Set.univ := by
+ rw [contDiffOn_univ]
+ refine fun_comp ?_ ?_
+ · exact mk_contDiff (n := ω)
+ · fun_prop
+
+@[fun_prop]
+lemma vadd_differentiable {d} (s : Space d) :
+ Differentiable ℝ (fun (v : EuclideanSpace ℝ (Fin d)) => v +ᵥ s) := by
+ apply Differentiable.comp
+ · exact mk_differentiable
+ · fun_prop
+
+@[fun_prop]
+lemma contDiffOn_vsub (s1 : Space d) :
+ ContDiffOn ℝ ω (fun (s : Space d) => s -ᵥ s1) Set.univ := by
+ rw [contDiffOn_univ]
+ refine fun_comp ?_ ?_
+ · fun_prop
+ · fun_prop
+
+@[fun_prop]
+lemma vsub_differentiable {d} (s1 : Space d) :
+ Differentiable ℝ (fun (s : Space d) => s -ᵥ s1) := by
+ apply Differentiable.comp
+ · exact PiLp.contDiff_toLp.differentiable (NeZero.ne' 2).symm
+ · fun_prop
+
+lemma fderiv_space_components {M d} [NormedAddCommGroup M] [NormedSpace ℝ M]
+ (μ : Fin d) (f : M → Space d) (hf : Differentiable ℝ f) (m dm : M):
+ fderiv ℝ f m dm μ = fderiv ℝ (fun m' => f m' μ) m dm := by
+ trans fderiv ℝ (Space.coordCLM μ ∘ fun m' => f m') m dm
+ swap
+ · congr
+ ext i
+ simp [coordCLM, coord_apply]
+ rw [fderiv_comp]
+ simp
+ simp [coordCLM, coord_apply]
+ · fun_prop
+ · fun_prop
+
/-!
## Directions
@@ -604,4 +655,41 @@ lemma oneEquiv_measurePreserving : MeasurePreserving oneEquiv volume volume :=
lemma oneEquiv_symm_measurePreserving : MeasurePreserving oneEquiv.symm volume volume := by
exact LinearIsometryEquiv.measurePreserving oneEquiv.symm
+/-!
+
+## Relation to tangent space
+
+-/
+
+
+
+
+open Manifold in
+/-- A diffeomorphism between the two different manifold sturctures on `Space d`,
+ that equivalent to `manifoldStructure d` and that equivalent to `𝓘(ℝ, Space d)` -/
+noncomputable def modelDiffeo {d} :
+ Diffeomorph (manifoldStructure d) 𝓘(ℝ, Space d) (Space d) (Space d) ⊤ where
+ toFun p := p
+ invFun p := p
+ left_inv := fun _ => rfl
+ right_inv := fun _ => rfl
+ contMDiff_toFun := by
+ rw [contMDiff_iff]
+ refine ⟨?_, ?_⟩
+ · simpa using continuous_id'
+ intro x y
+ simp [manifoldStructure]
+ fun_prop
+ contMDiff_invFun := by
+ rw [contMDiff_iff]
+ refine ⟨?_, ?_⟩
+ · simpa using continuous_id'
+ intro x y
+ simp [manifoldStructure]
+ fun_prop
+
+@[simp]
+lemma modelDiffeo_apply (p : Space d) :
+ modelDiffeo p = p := rfl
+
end Space
From dccdb0ec7cba3aa2aba659151f55a6cb1b1cff1b Mon Sep 17 00:00:00 2001
From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com>
Date: Wed, 11 Mar 2026 11:27:48 +0000
Subject: [PATCH 02/14] refactor: Lint
---
PhysLean/SpaceAndTime/Space/Basic.lean | 13 ++++---
PhysLean/SpaceAndTime/Space/Module.lean | 51 ++++++++-----------------
2 files changed, 23 insertions(+), 41 deletions(-)
diff --git a/PhysLean/SpaceAndTime/Space/Basic.lean b/PhysLean/SpaceAndTime/Space/Basic.lean
index 6995881b6..e38317e2c 100644
--- a/PhysLean/SpaceAndTime/Space/Basic.lean
+++ b/PhysLean/SpaceAndTime/Space/Basic.lean
@@ -295,16 +295,17 @@ lemma manifoldStructure_comp_manifoldStructure_symm {d : ℕ} :
ext1 x
simpa using (manifoldStructure d).right_inv' (x := x) (by simp [manifoldStructure])
+@[simp]
+lemma manifoldStructure_comp_manifoldStructure_symm_apply {d : ℕ}
+ (x : EuclideanSpace ℝ (Fin d)) :
+ (manifoldStructure d) ((manifoldStructure d).symm x) = x := by
+ simpa using (manifoldStructure d).right_inv' (x := x) (by simp [manifoldStructure])
+
@[simp]
lemma range_manifoldStructure {d : ℕ} :
(Set.range ↑(manifoldStructure d)) = Set.univ := by
ext x
- simp
- use (manifoldStructure d).symm x
- change (↑(manifoldStructure d) ∘ ↑(manifoldStructure d).symm) x = x
- rw [manifoldStructure_comp_manifoldStructure_symm]
- simp
-
+ simpa using ⟨(manifoldStructure d).symm x, manifoldStructure_comp_manifoldStructure_symm_apply x⟩
open Manifold in
lemma contMDiff_vaddConst (d : ℕ) : ContMDiff
diff --git a/PhysLean/SpaceAndTime/Space/Module.lean b/PhysLean/SpaceAndTime/Space/Module.lean
index 5f007a73b..da5dad788 100644
--- a/PhysLean/SpaceAndTime/Space/Module.lean
+++ b/PhysLean/SpaceAndTime/Space/Module.lean
@@ -497,13 +497,13 @@ lemma mk_contDiff {d : ℕ} {n : WithTop ℕ∞}:
lemma fderiv_mk {d : ℕ} (f : Fin d → ℝ) :
fderiv ℝ Space.mk f = (equivPi d).symm := by
change fderiv ℝ (equivPi d).symm f = _
- rw [@ContinuousLinearEquiv.fderiv]
+ rw [ContinuousLinearEquiv.fderiv]
@[simp]
lemma fderiv_val {d : ℕ} (p : Space d) :
fderiv ℝ Space.val p = (equivPi d) := by
change fderiv ℝ (equivPi d) p = _
- rw [@ContinuousLinearEquiv.fderiv]
+ rw [ContinuousLinearEquiv.fderiv]
@[fun_prop]
lemma contDiffOn_vadd (s : Space d) :
@@ -515,39 +515,29 @@ lemma contDiffOn_vadd (s : Space d) :
@[fun_prop]
lemma vadd_differentiable {d} (s : Space d) :
- Differentiable ℝ (fun (v : EuclideanSpace ℝ (Fin d)) => v +ᵥ s) := by
- apply Differentiable.comp
- · exact mk_differentiable
- · fun_prop
+ Differentiable ℝ (fun (v : EuclideanSpace ℝ (Fin d)) => v +ᵥ s) :=
+ mk_differentiable.comp <| by fun_prop
@[fun_prop]
lemma contDiffOn_vsub (s1 : Space d) :
- ContDiffOn ℝ ω (fun (s : Space d) => s -ᵥ s1) Set.univ := by
- rw [contDiffOn_univ]
- refine fun_comp ?_ ?_
- · fun_prop
- · fun_prop
+ ContDiffOn ℝ ω (fun (s : Space d) => s -ᵥ s1) Set.univ :=
+ contDiffOn_univ.mpr <| fun_comp (PiLp.contDiff_toLp) (by fun_prop)
@[fun_prop]
lemma vsub_differentiable {d} (s1 : Space d) :
- Differentiable ℝ (fun (s : Space d) => s -ᵥ s1) := by
- apply Differentiable.comp
- · exact PiLp.contDiff_toLp.differentiable (NeZero.ne' 2).symm
- · fun_prop
+ Differentiable ℝ (fun (s : Space d) => s -ᵥ s1) :=
+ (PiLp.contDiff_toLp.differentiable (NeZero.ne' 2).symm).comp (by fun_prop)
lemma fderiv_space_components {M d} [NormedAddCommGroup M] [NormedSpace ℝ M]
(μ : Fin d) (f : M → Space d) (hf : Differentiable ℝ f) (m dm : M):
fderiv ℝ f m dm μ = fderiv ℝ (fun m' => f m' μ) m dm := by
trans fderiv ℝ (Space.coordCLM μ ∘ fun m' => f m') m dm
- swap
+ · rw [fderiv_comp _ (by fun_prop) (by fun_prop), ContinuousLinearMap.fderiv,
+ ContinuousLinearMap.coe_comp', Function.comp_apply]
+ simp [coordCLM, coord_apply]
· congr
ext i
simp [coordCLM, coord_apply]
- rw [fderiv_comp]
- simp
- simp [coordCLM, coord_apply]
- · fun_prop
- · fun_prop
/-!
@@ -661,30 +651,21 @@ lemma oneEquiv_symm_measurePreserving : MeasurePreserving oneEquiv.symm volume v
-/
-
-
-
open Manifold in
-/-- A diffeomorphism between the two different manifold sturctures on `Space d`,
+/-- A diffeomorphism between the two different manifold structures on `Space d`,
that equivalent to `manifoldStructure d` and that equivalent to `𝓘(ℝ, Space d)` -/
noncomputable def modelDiffeo {d} :
Diffeomorph (manifoldStructure d) 𝓘(ℝ, Space d) (Space d) (Space d) ⊤ where
toFun p := p
invFun p := p
- left_inv := fun _ => rfl
- right_inv := fun _ => rfl
+ left_inv _ := rfl
+ right_inv _ := rfl
contMDiff_toFun := by
- rw [contMDiff_iff]
- refine ⟨?_, ?_⟩
- · simpa using continuous_id'
- intro x y
+ refine contMDiff_iff.mpr ⟨continuous_id', fun x y => ?_⟩
simp [manifoldStructure]
fun_prop
contMDiff_invFun := by
- rw [contMDiff_iff]
- refine ⟨?_, ?_⟩
- · simpa using continuous_id'
- intro x y
+ refine contMDiff_iff.mpr ⟨continuous_id', fun x y => ?_⟩
simp [manifoldStructure]
fun_prop
From ebef7d634ca78ee5ad34cb3b64332aacf94ceb39 Mon Sep 17 00:00:00 2001
From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com>
Date: Wed, 11 Mar 2026 11:40:44 +0000
Subject: [PATCH 03/14] refactor: Lint
---
.../SpaceAndTime/Space/Derivatives/Basic.lean | 26 +++----------------
PhysLean/SpaceAndTime/Space/Module.lean | 19 ++++++++++++++
2 files changed, 23 insertions(+), 22 deletions(-)
diff --git a/PhysLean/SpaceAndTime/Space/Derivatives/Basic.lean b/PhysLean/SpaceAndTime/Space/Derivatives/Basic.lean
index 82fad86d3..550c5e80e 100644
--- a/PhysLean/SpaceAndTime/Space/Derivatives/Basic.lean
+++ b/PhysLean/SpaceAndTime/Space/Derivatives/Basic.lean
@@ -110,30 +110,12 @@ lemma deriv_eq_mfderiv_manifoldStructure {M d} [NormedAddCommGroup M] [NormedSpa
rw [deriv_eq_mfderiv]
change _ = mfderiv (Space.manifoldStructure d) 𝓘(ℝ, M)
(f ∘ modelDiffeo) x (EuclideanSpace.single μ 1)
- rw [mfderiv_comp (I' := 𝓘(ℝ, Space d))]
- rotate_left
- · exact hf.mdifferentiable.mdifferentiableAt
- · exact MDifferentiable.mdifferentiableAt <|
- Diffeomorph.mdifferentiable modelDiffeo WithTop.top_ne_zero
+ rw [mfderiv_comp (I' := 𝓘(ℝ, Space d)) _ hf.mdifferentiable.mdifferentiableAt
+ (modelDiffeo.mdifferentiable WithTop.top_ne_zero).mdifferentiableAt]
simp only [Function.comp_apply, modelDiffeo_apply, mfderiv_eq_fderiv,
ContinuousLinearMap.coe_comp']
- congr 1
- simp [mfderiv]
- rw [if_pos]
- rotate_left
- · exact MDifferentiable.mdifferentiableAt <|
- Diffeomorph.mdifferentiable modelDiffeo WithTop.top_ne_zero
- change _ = (fderiv ℝ (↑(manifoldStructure d).symm) ((manifoldStructure d) x))
- (EuclideanSpace.single μ 1)
- simp [manifoldStructure]
- ext i
- rw [fderiv_space_components _ _ (by fun_prop)]
- simp only [vadd_apply, fderiv_add_const]
- change _ = (fderiv ℝ (EuclideanSpace.proj i) (x -ᵥ Classical.choice _))
- (EuclideanSpace.single μ 1)
- simp [basis_apply]
- congr 1
- exact Eq.propIntro (fun a => id (Eq.symm a)) fun a => id (Eq.symm a)
+ rw [basis_eq_mfderiv_modelDiffeo_single]
+ rfl
/-!
diff --git a/PhysLean/SpaceAndTime/Space/Module.lean b/PhysLean/SpaceAndTime/Space/Module.lean
index da5dad788..ce59fa66b 100644
--- a/PhysLean/SpaceAndTime/Space/Module.lean
+++ b/PhysLean/SpaceAndTime/Space/Module.lean
@@ -673,4 +673,23 @@ noncomputable def modelDiffeo {d} :
lemma modelDiffeo_apply (p : Space d) :
modelDiffeo p = p := rfl
+open Manifold in
+@[simp]
+lemma basis_eq_mfderiv_modelDiffeo_single (d : ℕ) (μ : Fin d) (x : Space d) :
+ basis μ = mfderiv (manifoldStructure d) 𝓘(ℝ, Space d) (modelDiffeo (d := d)) x
+ (EuclideanSpace.single μ 1) := by
+ simp [mfderiv]
+ rw [if_pos (modelDiffeo.mdifferentiable (WithTop.top_ne_zero)).mdifferentiableAt]
+ change _ = fderiv ℝ (↑(manifoldStructure d).symm) ((manifoldStructure d) x)
+ (EuclideanSpace.single μ 1)
+ simp [manifoldStructure]
+ ext i
+ rw [fderiv_space_components _ _ (by fun_prop)]
+ simp only [vadd_apply, fderiv_add_const]
+ change _ = (fderiv ℝ (EuclideanSpace.proj i) (x -ᵥ Classical.choice _))
+ (EuclideanSpace.single μ 1)
+ simp [basis_apply]
+ congr 1
+ exact Eq.propIntro (fun a => Eq.symm a) fun a => (Eq.symm a)
+
end Space
From 116184b0f15ec12ad9ac4c088bb737b0cdf978e7 Mon Sep 17 00:00:00 2001
From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com>
Date: Wed, 11 Mar 2026 11:45:27 +0000
Subject: [PATCH 04/14] refactor: LInt
---
PhysLean/SpaceAndTime/Space/Module.lean | 7 +++++--
1 file changed, 5 insertions(+), 2 deletions(-)
diff --git a/PhysLean/SpaceAndTime/Space/Module.lean b/PhysLean/SpaceAndTime/Space/Module.lean
index ce59fa66b..b4eb03656 100644
--- a/PhysLean/SpaceAndTime/Space/Module.lean
+++ b/PhysLean/SpaceAndTime/Space/Module.lean
@@ -674,10 +674,13 @@ lemma modelDiffeo_apply (p : Space d) :
modelDiffeo p = p := rfl
open Manifold in
+/-- The derivative of `modelDiffeo` provides an equivalence between
+ `Space d` and `EuclideanSpace ℝ (Fin d)`. This equivalences takes the basis
+ of `EuclideanSpace ℝ (Fin d)` to the basis of `Space d`, and vice versa. -/
@[simp]
lemma basis_eq_mfderiv_modelDiffeo_single (d : ℕ) (μ : Fin d) (x : Space d) :
- basis μ = mfderiv (manifoldStructure d) 𝓘(ℝ, Space d) (modelDiffeo (d := d)) x
- (EuclideanSpace.single μ 1) := by
+ basis μ = mfderiv (manifoldStructure d) 𝓘(ℝ, Space d) (modelDiffeo (d := d)) x
+ (EuclideanSpace.single μ 1) := by
simp [mfderiv]
rw [if_pos (modelDiffeo.mdifferentiable (WithTop.top_ne_zero)).mdifferentiableAt]
change _ = fderiv ℝ (↑(manifoldStructure d).symm) ((manifoldStructure d) x)
From 1e601835aa56987dd29f3f39dab4ce7a5ddacff1 Mon Sep 17 00:00:00 2001
From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com>
Date: Wed, 11 Mar 2026 11:47:11 +0000
Subject: [PATCH 05/14] refactor: Golf
---
PhysLean/SpaceAndTime/Space/Module.lean | 3 +--
1 file changed, 1 insertion(+), 2 deletions(-)
diff --git a/PhysLean/SpaceAndTime/Space/Module.lean b/PhysLean/SpaceAndTime/Space/Module.lean
index b4eb03656..d9804e2c4 100644
--- a/PhysLean/SpaceAndTime/Space/Module.lean
+++ b/PhysLean/SpaceAndTime/Space/Module.lean
@@ -683,8 +683,7 @@ lemma basis_eq_mfderiv_modelDiffeo_single (d : ℕ) (μ : Fin d) (x : Space d) :
(EuclideanSpace.single μ 1) := by
simp [mfderiv]
rw [if_pos (modelDiffeo.mdifferentiable (WithTop.top_ne_zero)).mdifferentiableAt]
- change _ = fderiv ℝ (↑(manifoldStructure d).symm) ((manifoldStructure d) x)
- (EuclideanSpace.single μ 1)
+ change _ = fderiv ℝ (manifoldStructure d).symm (manifoldStructure d x) (EuclideanSpace.single μ 1)
simp [manifoldStructure]
ext i
rw [fderiv_space_components _ _ (by fun_prop)]
From d34d53afef4550e9dd054c43e85b2b20c7c293f0 Mon Sep 17 00:00:00 2001
From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com>
Date: Wed, 11 Mar 2026 12:07:38 +0000
Subject: [PATCH 06/14] refactor: Lint
---
PhysLean/SpaceAndTime/Space/Module.lean | 5 ++---
1 file changed, 2 insertions(+), 3 deletions(-)
diff --git a/PhysLean/SpaceAndTime/Space/Module.lean b/PhysLean/SpaceAndTime/Space/Module.lean
index d9804e2c4..d96d832bb 100644
--- a/PhysLean/SpaceAndTime/Space/Module.lean
+++ b/PhysLean/SpaceAndTime/Space/Module.lean
@@ -671,7 +671,7 @@ noncomputable def modelDiffeo {d} :
@[simp]
lemma modelDiffeo_apply (p : Space d) :
- modelDiffeo p = p := rfl
+ modelDiffeo p = p := rfl
open Manifold in
/-- The derivative of `modelDiffeo` provides an equivalence between
@@ -688,8 +688,7 @@ lemma basis_eq_mfderiv_modelDiffeo_single (d : ℕ) (μ : Fin d) (x : Space d) :
ext i
rw [fderiv_space_components _ _ (by fun_prop)]
simp only [vadd_apply, fderiv_add_const]
- change _ = (fderiv ℝ (EuclideanSpace.proj i) (x -ᵥ Classical.choice _))
- (EuclideanSpace.single μ 1)
+ change _ = fderiv ℝ (EuclideanSpace.proj i) (x -ᵥ Classical.choice _) (EuclideanSpace.single μ 1)
simp [basis_apply]
congr 1
exact Eq.propIntro (fun a => Eq.symm a) fun a => (Eq.symm a)
From 5a1a20f6e371c5d74026dc4911a81572dddeb23c Mon Sep 17 00:00:00 2001
From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com>
Date: Wed, 11 Mar 2026 12:08:29 +0000
Subject: [PATCH 07/14] refactor: Remove simp
---
PhysLean/SpaceAndTime/Space/Module.lean | 1 -
1 file changed, 1 deletion(-)
diff --git a/PhysLean/SpaceAndTime/Space/Module.lean b/PhysLean/SpaceAndTime/Space/Module.lean
index d96d832bb..c85ee92f5 100644
--- a/PhysLean/SpaceAndTime/Space/Module.lean
+++ b/PhysLean/SpaceAndTime/Space/Module.lean
@@ -677,7 +677,6 @@ open Manifold in
/-- The derivative of `modelDiffeo` provides an equivalence between
`Space d` and `EuclideanSpace ℝ (Fin d)`. This equivalences takes the basis
of `EuclideanSpace ℝ (Fin d)` to the basis of `Space d`, and vice versa. -/
-@[simp]
lemma basis_eq_mfderiv_modelDiffeo_single (d : ℕ) (μ : Fin d) (x : Space d) :
basis μ = mfderiv (manifoldStructure d) 𝓘(ℝ, Space d) (modelDiffeo (d := d)) x
(EuclideanSpace.single μ 1) := by
From 08c5f586abda52ec933bbd00bd5547fc1c451b53 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Wed, 11 Mar 2026 15:43:14 +0000
Subject: [PATCH 08/14] refactor: Lint
---
PhysLean/SpaceAndTime/Space/Basic.lean | 1 -
PhysLean/SpaceAndTime/Space/Module.lean | 6 +++---
2 files changed, 3 insertions(+), 4 deletions(-)
diff --git a/PhysLean/SpaceAndTime/Space/Basic.lean b/PhysLean/SpaceAndTime/Space/Basic.lean
index e38317e2c..8cd12f8b6 100644
--- a/PhysLean/SpaceAndTime/Space/Basic.lean
+++ b/PhysLean/SpaceAndTime/Space/Basic.lean
@@ -295,7 +295,6 @@ lemma manifoldStructure_comp_manifoldStructure_symm {d : ℕ} :
ext1 x
simpa using (manifoldStructure d).right_inv' (x := x) (by simp [manifoldStructure])
-@[simp]
lemma manifoldStructure_comp_manifoldStructure_symm_apply {d : ℕ}
(x : EuclideanSpace ℝ (Fin d)) :
(manifoldStructure d) ((manifoldStructure d).symm x) = x := by
diff --git a/PhysLean/SpaceAndTime/Space/Module.lean b/PhysLean/SpaceAndTime/Space/Module.lean
index c85ee92f5..49a99665c 100644
--- a/PhysLean/SpaceAndTime/Space/Module.lean
+++ b/PhysLean/SpaceAndTime/Space/Module.lean
@@ -671,15 +671,15 @@ noncomputable def modelDiffeo {d} :
@[simp]
lemma modelDiffeo_apply (p : Space d) :
- modelDiffeo p = p := rfl
+ modelDiffeo p = p := rfl
open Manifold in
/-- The derivative of `modelDiffeo` provides an equivalence between
`Space d` and `EuclideanSpace ℝ (Fin d)`. This equivalences takes the basis
of `EuclideanSpace ℝ (Fin d)` to the basis of `Space d`, and vice versa. -/
lemma basis_eq_mfderiv_modelDiffeo_single (d : ℕ) (μ : Fin d) (x : Space d) :
- basis μ = mfderiv (manifoldStructure d) 𝓘(ℝ, Space d) (modelDiffeo (d := d)) x
- (EuclideanSpace.single μ 1) := by
+ basis μ = mfderiv (manifoldStructure d) 𝓘(ℝ, Space d) (modelDiffeo (d := d)) x
+ (EuclideanSpace.single μ 1) := by
simp [mfderiv]
rw [if_pos (modelDiffeo.mdifferentiable (WithTop.top_ne_zero)).mdifferentiableAt]
change _ = fderiv ℝ (manifoldStructure d).symm (manifoldStructure d x) (EuclideanSpace.single μ 1)
From d54087c018a2dacb7acf5b3f0561857a5c317f04 Mon Sep 17 00:00:00 2001
From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com>
Date: Thu, 12 Mar 2026 10:55:04 +0000
Subject: [PATCH 09/14] feat: Small generalization
---
.../SpaceAndTime/Space/Derivatives/Basic.lean | 37 ++++++++++++++-----
1 file changed, 27 insertions(+), 10 deletions(-)
diff --git a/PhysLean/SpaceAndTime/Space/Derivatives/Basic.lean b/PhysLean/SpaceAndTime/Space/Derivatives/Basic.lean
index 550c5e80e..10cc1ac1b 100644
--- a/PhysLean/SpaceAndTime/Space/Derivatives/Basic.lean
+++ b/PhysLean/SpaceAndTime/Space/Derivatives/Basic.lean
@@ -100,22 +100,39 @@ lemma deriv_eq_mfderiv {M d} [NormedAddCommGroup M] [NormedSpace ℝ M]
rw [deriv_eq_fderiv_basis, ← mfderiv_eq_fderiv]
rfl
+open Manifold in
+lemma mdifferentiable_manifoldStructure_iff_differentiable {M d} [NormedAddCommGroup M]
+ [NormedSpace ℝ M] {f : Space d → M} {x : Space d} :
+ MDifferentiableAt (Space.manifoldStructure d) 𝓘(ℝ, M) f x ↔ DifferentiableAt ℝ f x := by
+ constructor
+ · intro h
+ rw [← mdifferentiableAt_iff_differentiableAt]
+ apply h.comp (I' := Space.manifoldStructure d)
+ exact (modelDiffeo.symm.mdifferentiable (WithTop.top_ne_zero)).mdifferentiableAt
+ · intro h
+ apply (mdifferentiableAt_iff_differentiableAt.mpr h).comp (I' := 𝓘(ℝ, Space d))
+ exact (modelDiffeo.mdifferentiable (WithTop.top_ne_zero)).mdifferentiableAt
+
open Manifold in
/-- The spatial-derivative in terms of the derivative of functions between
manifolds with the manifold structure `Space.manifoldStructure d`.
This should eventually be used as the definition of `deriv`. -/
lemma deriv_eq_mfderiv_manifoldStructure {M d} [NormedAddCommGroup M] [NormedSpace ℝ M]
- (μ : Fin d) (f : Space d → M) (hf : Differentiable ℝ f) (x : Space d) :
+ (μ : Fin d) (f : Space d → M) (x : Space d) :
deriv μ f x = mfderiv (Space.manifoldStructure d) 𝓘(ℝ, M) f x (EuclideanSpace.single μ 1) := by
- rw [deriv_eq_mfderiv]
- change _ = mfderiv (Space.manifoldStructure d) 𝓘(ℝ, M)
- (f ∘ modelDiffeo) x (EuclideanSpace.single μ 1)
- rw [mfderiv_comp (I' := 𝓘(ℝ, Space d)) _ hf.mdifferentiable.mdifferentiableAt
- (modelDiffeo.mdifferentiable WithTop.top_ne_zero).mdifferentiableAt]
- simp only [Function.comp_apply, modelDiffeo_apply, mfderiv_eq_fderiv,
- ContinuousLinearMap.coe_comp']
- rw [basis_eq_mfderiv_modelDiffeo_single]
- rfl
+ by_cases hf : DifferentiableAt ℝ f x
+ · rw [deriv_eq_mfderiv]
+ change _ = mfderiv (Space.manifoldStructure d) 𝓘(ℝ, M)
+ (f ∘ modelDiffeo) x (EuclideanSpace.single μ 1)
+ rw [mfderiv_comp (I' := 𝓘(ℝ, Space d)) _ hf.mdifferentiableAt
+ (modelDiffeo.mdifferentiable WithTop.top_ne_zero).mdifferentiableAt]
+ simp only [Function.comp_apply, modelDiffeo_apply, mfderiv_eq_fderiv,
+ ContinuousLinearMap.coe_comp']
+ rw [basis_eq_mfderiv_modelDiffeo_single]
+ rfl
+ · rw [deriv_eq, fderiv_zero_of_not_differentiableAt hf,
+ mfderiv_zero_of_not_mdifferentiableAt <| mdifferentiable_iff_differentiable.mp.mt hf]
+ simp
/-!
From 4ba57c73f8fdb539a4f89c5864e13a98c5d35bea Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Thu, 12 Mar 2026 12:24:33 +0000
Subject: [PATCH 10/14] fix: build
---
PhysLean/SpaceAndTime/Space/Derivatives/Basic.lean | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/PhysLean/SpaceAndTime/Space/Derivatives/Basic.lean b/PhysLean/SpaceAndTime/Space/Derivatives/Basic.lean
index 10cc1ac1b..76d571331 100644
--- a/PhysLean/SpaceAndTime/Space/Derivatives/Basic.lean
+++ b/PhysLean/SpaceAndTime/Space/Derivatives/Basic.lean
@@ -131,7 +131,8 @@ lemma deriv_eq_mfderiv_manifoldStructure {M d} [NormedAddCommGroup M] [NormedSpa
rw [basis_eq_mfderiv_modelDiffeo_single]
rfl
· rw [deriv_eq, fderiv_zero_of_not_differentiableAt hf,
- mfderiv_zero_of_not_mdifferentiableAt <| mdifferentiable_iff_differentiable.mp.mt hf]
+ mfderiv_zero_of_not_mdifferentiableAt <|
+ mdifferentiable_manifoldStructure_iff_differentiable.mp.mt hf]
simp
/-!
From 643cad9152787ac3fcf97eaf7d101c91980d5943 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Mon, 16 Mar 2026 11:44:19 +0000
Subject: [PATCH 11/14] feat: Properties of vadd
---
PhysLean/SpaceAndTime/Space/Module.lean | 54 +++++++++++++++++++++++++
1 file changed, 54 insertions(+)
diff --git a/PhysLean/SpaceAndTime/Space/Module.lean b/PhysLean/SpaceAndTime/Space/Module.lean
index 49a99665c..f1457792e 100644
--- a/PhysLean/SpaceAndTime/Space/Module.lean
+++ b/PhysLean/SpaceAndTime/Space/Module.lean
@@ -7,6 +7,7 @@ module
public import PhysLean.SpaceAndTime.Space.Basic
public import Mathlib.Geometry.Manifold.Diffeomorph
+public import Mathlib.Analysis.Distribution.TemperateGrowth
/-!
# The structure of a module on Space
@@ -692,4 +693,57 @@ lemma basis_eq_mfderiv_modelDiffeo_single (d : ℕ) (μ : Fin d) (x : Space d) :
congr 1
exact Eq.propIntro (fun a => Eq.symm a) fun a => (Eq.symm a)
+
+/-!
+
+## Properties of vadd with module structure
+
+-/
+
+lemma norm_vadd_le_add {d} (v : EuclideanSpace ℝ (Fin d)) (s : Space d) :
+ ‖v +ᵥ s‖ ≤ ‖v‖ + ‖s‖ := by
+ trans ‖s - (-v +ᵥ (0 : Space d))‖
+ · apply le_of_eq
+ congr
+ ext i
+ simp only [vadd_apply, sub_apply, PiLp.neg_apply, zero_apply, add_zero, sub_neg_eq_add]
+ ring
+ · apply (norm_sub_le _ _).trans <| le_of_eq _
+ simp only [norm_vadd_zero, norm_neg]
+ ring
+
+@[fun_prop]
+lemma differentiable_vadd {d} (v : EuclideanSpace ℝ (Fin d)) :
+ Differentiable ℝ (fun (s : Space d) => v +ᵥ s) :=
+ mk_differentiable.comp <| by fun_prop
+
+@[simp]
+lemma fderiv_vadd {d} (v : EuclideanSpace ℝ (Fin d)) :
+ fderiv ℝ (fun s => v +ᵥ s) = fun (_ : Space d) => ContinuousLinearMap.id ℝ _ := by
+ ext s ds i
+ change fderiv ℝ (fun s => v +ᵥ s) s ds i = _
+ rw [fderiv_space_components]
+ simp
+ trans fderiv ℝ (coordCLM i) s ds
+ · congr
+ ext j
+ simp [coordCLM, coord_apply]
+ · rw [ContinuousLinearMap.fderiv]
+ simp [coordCLM, coord_apply]
+ · fun_prop
+
+@[fun_prop]
+lemma vadd_hasTemperateGrowth {d} (v : EuclideanSpace ℝ (Fin d)) :
+ Function.HasTemperateGrowth (fun s : Space d => v +ᵥ s) := by
+ apply Function.HasTemperateGrowth.of_fderiv (k := 1) (C := 1 + ‖v‖)
+ · rw [fderiv_vadd]
+ simp
+ · fun_prop
+ · intro x
+ simp
+ apply (norm_vadd_le_add _ _).trans
+ have : 0 ≤ ‖v‖ := by positivity
+ have : 0 ≤ ‖x‖ := by positivity
+ nlinarith
+
end Space
From f804baa1448002e19525d6d6ee3ac09a00c6d982 Mon Sep 17 00:00:00 2001
From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com>
Date: Thu, 19 Mar 2026 08:21:22 +0000
Subject: [PATCH 12/14] Update Basic.lean
---
PhysLean/SpaceAndTime/Space/Derivatives/Basic.lean | 8 ++++++--
1 file changed, 6 insertions(+), 2 deletions(-)
diff --git a/PhysLean/SpaceAndTime/Space/Derivatives/Basic.lean b/PhysLean/SpaceAndTime/Space/Derivatives/Basic.lean
index 76d571331..d35e44a98 100644
--- a/PhysLean/SpaceAndTime/Space/Derivatives/Basic.lean
+++ b/PhysLean/SpaceAndTime/Space/Derivatives/Basic.lean
@@ -113,10 +113,14 @@ lemma mdifferentiable_manifoldStructure_iff_differentiable {M d} [NormedAddCommG
apply (mdifferentiableAt_iff_differentiableAt.mpr h).comp (I' := 𝓘(ℝ, Space d))
exact (modelDiffeo.mdifferentiable (WithTop.top_ne_zero)).mdifferentiableAt
+
+TODO "3XMN6" "Make the version of the derivative described through
+ `deriv_eq_mfderiv_manifoldStructure` the definition of `deriv` and prove the
+ equivalence with the current definition, under suitable conditions."
+
open Manifold in
/-- The spatial-derivative in terms of the derivative of functions between
- manifolds with the manifold structure `Space.manifoldStructure d`.
- This should eventually be used as the definition of `deriv`. -/
+ manifolds with the manifold structure `Space.manifoldStructure d`. -/
lemma deriv_eq_mfderiv_manifoldStructure {M d} [NormedAddCommGroup M] [NormedSpace ℝ M]
(μ : Fin d) (f : Space d → M) (x : Space d) :
deriv μ f x = mfderiv (Space.manifoldStructure d) 𝓘(ℝ, M) f x (EuclideanSpace.single μ 1) := by
From 06635044763d422a0eeb6a076973c2bc2c095b68 Mon Sep 17 00:00:00 2001
From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com>
Date: Thu, 19 Mar 2026 15:37:05 +0000
Subject: [PATCH 13/14] feat: Update readme (#986)
* feat: Update readme
* spelling: ignore abbrev of journal
---
.codespellignore | 1 +
README.md | 153 +++++++++++++++++++++++------------------
docs/PhysLib-logo.jpeg | Bin 0 -> 169733 bytes
3 files changed, 88 insertions(+), 66 deletions(-)
create mode 100644 docs/PhysLib-logo.jpeg
diff --git a/.codespellignore b/.codespellignore
index 35ba186f6..0ea841340 100644
--- a/.codespellignore
+++ b/.codespellignore
@@ -9,3 +9,4 @@ Breal
ket
rIn
FRO
+Commun
diff --git a/README.md b/README.md
index b34f96bc4..fae37caaa 100644
--- a/README.md
+++ b/README.md
@@ -5,7 +5,7 @@
-

+
@@ -35,7 +35,8 @@
## Requirements of the project
-🎯 The project shall contain results (definitions, theorems, lemmas and calculations) from **physics** formalized (or **digitalized**) into the interactive theorem prover **Lean 4**.
+🎯 The project shall contain results (definitions, theorems, lemmas and calculations) from **physics**,
+ including quantum information, formalized (or **digitalized**) into the interactive theorem prover **Lean 4**.
🎯 The project shall be **organized** by **physics**.
@@ -45,7 +46,7 @@
🎯 The project shall contain Physics Lean **tactics**, **notation** and **syntax** for physicists.
-🎯 The project shall *not* be tied to physics axiomizations (e.g. axiomatic QFT), but rather lexiable enough to accommodate different approaches and starting points.
+🎯 The project shall *not* be tied to physics axiomizations (e.g. axiomatic QFT), but rather flexiable enough to accommodate different approaches and starting points.
🎯 The content of the project shall be carefully **reviewed** and curated, to ensure reusability, readability and fit.
@@ -56,71 +57,19 @@
🎯 The project shall be for **main-stream** physics only.
-## How to get involved
+## Contributing to PhysLib
-See the [Get Involved](https://physlean.com/GetInvolved.html) for more details. Some suggestions:
-
-📣 write **informal** results - no need to learn Lean for this - see the [Getting Started](https://physlean.com/GettingStarted) page for more details,
-
-📣 tackle a [TODO item](https://physlean.com/TODOList),
-
-📣 or, start formalizing an area that you find interesting.
-
-Feel free to come to the [PhysLean zulip](https://leanprover.zulipchat.com/#narrow/channel/479953-PhysLean/) to ask questions and advice.
+PhysLib is open-source and community run, and we welcome contributions from anyone.
+All you need to do is open a pull-request with your changes
+and our team of maintainers will review it and iterate with you on feedback until it
+can be merged.
+If you unsure where you would like to contribute, you may find ideas on:
+- our [open issues](https://github.com/leanprover-community/physlib/issues).
+- our [todo list](https://physlean.com/TODOList)
+- our [Get Involved page](https://physlean.com/GetInvolved.html)
> [!NOTE]
-> When making contributing to PhysLean it is much better to do it with small steps. This makes it easier for us to review, and allows you to get feedback sooner.
-
-
-## Places in the project to start
-
-Good places to start an exploration of the project.
-
-- [🗂️](https://github.com/HEPLean/PhysLean/blob/master/PhysLean/Electromagnetism/MaxwellEquations.lean)
-[💻](https://live.physlean.com/#url=https%3A%2F%2Fraw.githubusercontent.com%2FHEPLean%2FPhysLean%2Frefs%2Fheads%2Fmaster%2FPhysLean%2FElectromagnetism%2FMaxwellEquations.lean)
-**Maxwell's equations** in electromagnetism.
-- [🗂️](https://github.com/HEPLean/PhysLean/blob/master/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Basic.lean)
-[💻](https://live.physlean.com/#url=https%3A%2F%2Fraw.githubusercontent.com%2FHEPLean%2FPhysLean%2Frefs%2Fheads%2Fmaster%2FPhysLean%2FQuantumMechanics%2FOneDimension%2FHarmonicOscillator%2FBasic.lean)
-**Quantum Harmonic Oscillator** in quantum mechanics.
-- [🗂️](https://github.com/HEPLean/PhysLean/blob/master/PhysLean/StatisticalMechanics/CanonicalEnsemble/TwoState.lean)
-[💻](https://live.physlean.com/#url=https%3A%2F%2Fraw.githubusercontent.com%2FHEPLean%2FPhysLean%2Frefs%2Fheads%2Fmaster%2FPhysLean%2FStatisticalMechanics%2FCanonicalEnsemble%2FTwoState.lean)
-The two state **canonical ensemble** in statistical mechanics.
-- [🗂️](https://github.com/HEPLean/PhysLean/blob/master/PhysLean/CondensedMatter/TightBindingChain/Basic.lean)
-[💻](https://live.physlean.com/#url=https%3A%2F%2Fraw.githubusercontent.com%2FHEPLean%2FPhysLean%2Frefs%2Fheads%2Fmaster%2FPhysLean%2FCondensedMatter%2FTightBindingChain%2FBasic.lean)
-The **tight-binding model** in condensed matter physics
-- [🗂️](https://github.com/HEPLean/PhysLean/blob/master/PhysLean/Relativity/Special/TwinParadox/Basic.lean)
-[💻](https://live.physlean.com/#url=https%3A%2F%2Fraw.githubusercontent.com%2FHEPLean%2FPhysLean%2Frefs%2Fheads%2Fmaster%2FPhysLean%2FRelativity%2FSpecial%2FTwinParadox%2FBasic.lean)
-The **twin paradox** in special relativity.
-- [🗂️](https://github.com/HEPLean/PhysLean/blob/master/PhysLean/Particles/BeyondTheStandardModel/TwoHDM/Basic.lean)
-[💻](https://live.physlean.com/#url=https%3A%2F%2Fraw.githubusercontent.com%2FHEPLean%2FPhysLean%2Frefs%2Fheads%2Fmaster%2FPhysLean%2FParticles%2FBeyondTheStandardModel%2FTwoHDM%2FBasic.lean) The **two-Higgs doublet model** in particle physics
-- [🗂️](https://github.com/HEPLean/PhysLean/blob/master/PhysLean/QFT/PerturbationTheory/WickAlgebra/WicksTheorem.lean)
-[💻](https://live.physlean.com/#url=https%3A%2F%2Fraw.githubusercontent.com%2FHEPLean%2FPhysLean%2Frefs%2Fheads%2Fmaster%2FPhysLean%2FQFT%2FPerturbationTheory%2FWickAlgebra%2FWicksTheorem.lean)
-**Wick's theorem** in quantum field theory.
-
-
-## Associated media and publications
-- [📄](https://arxiv.org/abs/2405.08863) Joseph Tooby-Smith,
-__HepLean: Digitalising high energy physics__, Computer Physics Communications, Volume 308,
-2025, 109457, ISSN 0010-4655, https://doi.org/10.1016/j.cpc.2024.109457. \[arXiv:2405.08863\]
-- [📄](https://arxiv.org/abs/2411.07667) Joseph Tooby-Smith, __Formalization of physics index notation in Lean 4__, arXiv:2411.07667
-- [📄](https://arxiv.org/abs/2505.07939) Joseph Tooby-Smith, __Digitalizing Wick's Theorem__, arXiv:2505.07939
-- [🎥](https://www.youtube.com/watch?v=U7Xf5p6jAUU&t=62s) Lean Together 2025: Joseph Tooby-Smith, Physics and Lean
-- [🎥](https://www.youtube.com/watch?v=W2cObnopqas) Seminar recording of "HepLean: Lean and high energy physics" by J. Tooby-Smith
-
-### Papers referencing PhysLean
-- Hu, Jiewen, Thomas Zhu, and Sean Welleck. "miniCTX: Neural Theorem Proving with (Long-) Contexts." arXiv preprint [arXiv:2408.03350](https://www.arxiv.org/abs/2408.03350) (2024). [Project page]( https://cmu-l3.github.io/minictx/)
-
-How PhysLean (then called HepLean) was used: *Theorems from the space-time files of HepLean were included in a data set used to evaluate the ability of models to prove theorems from real-world repositories, which requires working with definitions, theorems, and other context not seen in training.*
-
-## Contributing
-
-We would love to have you involved! See the [Get Involved](https://physlean.com/GetInvolved.html) page to see how you can get involved.
-Any contributions are welcome! If you have any questions or want permission permission to create a pull-request for this
-repository contact Joseph Tooby-Smith on the [Lean Zulip](https://leanprover.zulipchat.com), or email.
-
-## Installation
-
-If you want to play around with PhysLean, but do not want to download Lean, then you can use [GitPod](https://gitpod.io/#https://github.com/HEPLean/HepLean).
+> If stuck at any point there are lots of people happly to help on the [PhysLib zulip](https://leanprover.zulipchat.com/#narrow/channel/479953-PhysLib)
### Installing Lean 4
@@ -132,10 +81,82 @@ or
- https://leanprover-community.github.io/get_started.html
-### Installing PhysLean
+### Installing PhysLib
- Clone this repository (or download the repository as a Zip file)
- Open a terminal at the top-level in the corresponding directory.
- Run `lake exe cache get`. The command `lake` should have been installed when you installed Lean.
- Run `lake build`.
- Open the directory (not a single file) in Visual Studio Code (or another Lean compatible code editor).
+
+### Making a pull-request
+
+There are lots of guides on how to make a pull-request on GitHub. The first thing you
+need to do is fork the repository. Once you've made your pull request we will review it:
+- Guide to [PhysLib reviews](https://github.com/leanprover-community/physlib/blob/master/docs/ReviewGuidelines.md).
+It will also undergo a number of automated checks called linters. Sometimes these are easier
+to run locally:
+- Guide to [linters and running them locally](https://github.com/leanprover-community/physlib/blob/master/scripts/README.md).
+
+Most importantly:
+> [!NOTE]
+> When making contributing to PhysLib it is much better to do it with small steps. This makes it easier for us to review, and allows you to get feedback sooner.
+
+## Maintainers
+
+Below are the maintainers of the project, however the best way to reach them is by posting
+on the [Lean Zulip](https://leanprover.zulipchat.com/#narrow/channel/479953-PhysLib)
+
+- Léo Lessa (@Megaleo)
+- Alex Meiburg (@Timeroot)
+- Daniel Morrison (@morrison-daniel)
+- Zhi-Kai Pong (@zhikaip)
+- Rodolfo Soldati (@rodolfor-s)
+- Joseph Tooby-Smith (@jstoobysmith)
+- Winston Yin (@winstonyin)
+
+## Citing the project
+
+If you want to cite the project as a whole please cite:
+
+```
+@misc{physlib,
+ author = {The PhysLib community},
+ title = {PhysLib: The Lean Physics Library},
+ year = {2024},
+ publisher = {GitHub},
+ journal = {GitHub repository},
+ howpublished = {\url{https://github.com/leanprover-community/physlib}},
+}
+```
+
+PhysLib was formed by merging the general physics Lean library PhysLean (formerly called HepLean)
+with the quantum-information library Lean-QuantumInfo. Where appropriate please also consider
+citing the papers associated with the origin of these projects. For the former please use:
+```
+@article{Tooby-Smith:2024vqu,
+ author = "Tooby-Smith, Joseph",
+ title = "{HepLean: Digitalising high energy physics}",
+ eprint = "2405.08863",
+ archivePrefix = "arXiv",
+ primaryClass = "hep-ph",
+ doi = "10.1016/j.cpc.2024.109457",
+ journal = "Comput. Phys. Commun.",
+ volume = "308",
+ pages = "109457",
+ year = "2025"
+}
+```
+and for the latter please use:
+
+```
+@article{Meiburg:2025mwn,
+ author = "Meiburg, Alex and Lessa, Leonardo A. and Soldati, Rodolfo R.",
+ title = "{A Formalization of the Generalized Quantum Stein's Lemma in Lean}",
+ eprint = "2510.08672",
+ archivePrefix = "arXiv",
+ primaryClass = "quant-ph",
+ month = "10",
+ year = "2025"
+}
+```
diff --git a/docs/PhysLib-logo.jpeg b/docs/PhysLib-logo.jpeg
new file mode 100644
index 0000000000000000000000000000000000000000..0a0cf877cba569fad90f3ce6f3297d89de8b68d7
GIT binary patch
literal 169733
zcmeFa2Ut_vx;8p7U_`{wQ4pfiR6tak(t;u)B7#_G0!tAg#1IjXAb}t%RX|WdVL?!u
zNbgcZ$A(lvIthx>6Ob?^g*$QWwfEZXo^$Sho_l`JB0fn*W@d(Sj(3c2eDC+YW3cjZ
zWfTxNam@G_z{Lds$Dx0~3I)(N#G|hOfT=042LON#09P;?;D$=jDS!m@1b}tP>wZ51
z4@idnUgkcy`sKRw+IP{=(I
z!25U_JmSAXUAN2Fz`()W!t9vwNy8r(wQkGBYuB!>{ut}#dELV3$aX7ho9*y%=xSE4
z2YOs|^tg7|-2CKf`S1Zo0dqk0-<+@Z<9q`E2c7K$T!((=47dQE&~FYyM^I61?pk*834d<4FJOJ&~I!#uBaaP@jch3BLKiNyt1+&4*>870KmS#vci0}
zvcgUQ0N5Y^)Vi(I0)iX355farT!O$lK`xje*GeORgj$M+>&N3qMbHb^Iv6+4diVz3
zjeO7vB?7=YE*NYbH;jj8wL^0GLEi)1f;>Vy_8(p^eEK4Mr@P33ThUK9$Q&uC6Se4|
z$*Nwu9>}{xB-VhF^3S-g)5G29YDtPYddJWmGL_qL;3BY!s7KqsY-$
zZ|%pO{pW5h@c+}D{q@HFc3%U40W`w@&mJpKCI4qNK)+rYf(#gKr61S?aPHX(>=fG)=Km8myt?{Ry1E)3q
z^mE{}#-Dx;oYwf$&wF2;{jX(VyIIZ!gp97~g{`7O;w8o!)
z4xHBb)6ap^8h`pZa9ZO}KL<{0{ORYwX^lVq95}7x$
zLuU=8`a)pUfQdd2wC$xi*Kcp|l{I#Sh|xR58E^pnVSagLba>c<#u}B<%_Q0#P<48F
zxKgy9{%NvEuF>XHz?*@S(HKpJce>aDHaqvm-D~`FeYT9ac9bhJxNKOhv-k$>eOd|_
zY~HR;-ej7Yp5vZgY`C{Lfn1uC^sAflqMbaofAqN0r7*=$-JW1-ITJQ`g6muBAMp4K
zEdPUV?qq=)83GD4866QI7=meIL|)cG8vM?;fkek9X?1#Ah$m?yXxY$z?pIUwo~PMU
z%b!2Q#-;Zk7E*n!JM`}K^E2;VVBh6dfWXidppJqpAWbi>0KD*qxsTrU62UVObc?o`
zepkZb8b6a-haysN$?>2xC&u%|w{NXj?sPMz%Gr{lmoW|XHppNWk{Tg40`Q5rvYm&3=}g>6=Mzpd@x(eUloP4n
zqs4z)FF~CSZy{~QD*108n7YZo0t8cgSh!K<+dMcJ*POI1aK5vDc&T1mr~8{R%bDUk
zBsb^T)Tusz)m6D%m0umX9nty6EiVy&?hO_t-aXHreG?L9Jrr{8-09dWjsY){g^Ulv
z9z?ppD2PZB?KGlq1sEL}P)k&>#D&=(C|%gesim2=R=)4d@#ihr!P|?6$
zEZ(d7ROh)q_jHAG0LulOSOIvr*vU2O?4lFF_A9_$_tAkw`U+6Le-xeTIgyJ^*lw7E
zf6!{@adu?u{-ML7&7@SjOzm%8$UOlBePh`eW7$s+x=CkxA1t!I!oI;cyiN2jj;MIc
z5USy3$(KGBlJ2BTkjmn{+=sc|lUtPf?oQ?wRMgNomm^kJlUzT8Aq>68_01f4%U-TPXuh0xrD?f6A
zi>1rygCK7kxXsxpN_|yj!nF18Knm*Z^GmRhhzceM`w*o=X$|$3Ggs6~Uee6!iF}7s
zSbDUY6b({g^TPQKf+i+s>iDLLo|MdC6Ww>o$Sf4?)CvHquK=8lwoK2OaOw&mg_l|Z
z935_z^$M!DH9GVokMww=Bq!soUKWaL>cK!s*_+;t2mw>&yI((eO0EE6Dh+Mxz?k=2
zPsNRuUblpi|xdD
zMU#~@(Mlo7oy`r7XhS1?C
zedNjZ|G^pjckhmCK6nPh^zeVR0_0}|q=L~*YnC7AMKf#2bI!DP=}A)T-LV4PAvYTx
zKaMod2YpAS4m#k+sA74pW#?PL9HxEY
z@IIwk>!`cbGfze_V%W*wrtHidejyfLC6{odSmOCLc;zrru&fDBM?|-Ok2i>`4PGF*})XWFLz}53>o-dS!KRgwhHrX>G#xfku
z6LV2*V>Hq<%0>9GyWmS+(71=3mq0OMohErSej;^h1m?fN8f+MofBd3_5d!wf1vf_B
zdp51il3!@3XzF>C0b(e{g;tZ65_bKpJ+!=Aap$`%Hh9g=psAQRfF1BpTQ8yh?Asi1
z{E4G4$S@Q|2#kJ8z;r0Fsu9$ayHmhN&rTX*#_WXJWyOUAOJr~YE&>L!F3;_4tNG4X
z#vk(y16YYanv<;yL1a(xgzT;#J#2|$U*hu_kD+!8+M4r4VN)+>!kKQb
z=ZY<@YGW46{WfaI{bHDm_?r7aK4G)w*cDK}%|hl|vV?CpbWV~=yl3DPBoFuuyKmAT
z2^u~#QMgy523G9;h3uzZj11C~6z9kVn|#PEo{HGp+r-&k(q093&MY>^*eiBMzk9*O
zQYY3OC63PH`W>m$@pA#h(IgZdCj=c9_elLxt1CG+LDAO?{xgRPrV#r
z*8U`y=BF8xVh5ta<2WaK`XldBTVbc~hya{Zs4>MAz-Sp0dVqH|8LrrwiyHZ4L?K+nPyH3m2jA@
zrZI3u!)7#JN=?dB!clMq$g*vDzGo0!(OiACqO2Yll$D7_O;p$yV6#}~KTLmdcg({h
zPgF$W+hNQE_8q9f9**QYvxJEa1!!Vn+%%h_vL64;Zy!2o2UwYVWOzULf%-Kys7_t9
zw?+XUJX0eZZt}scc*@UWs$LrTvYo(-&fMyzhT}trQPlyqz(0*l$ajaW{P|+Luwck>
zZX^Q)rS?yBg+?=R7khz@lwq+sTXNWk+%&^sZ1L2|lG)6gmJbWMa%S^nk&~ltFu>n`
zf3l7Xe+6O9GIj5x*s^AZfbN2Yf#_oanaI@
ze&s>J(E3krd$wGuyoX+zm$#aT>n#`!-cyTw^_d+p9_QziKB>`V?JD6l)D*Fp_zo-D
zl=eBb4d;Q?F%61zQHY?%YDh+ZcsP1nUljVY1pNF8=ej+WEl>7*3okEb+ZuH%E!yqn
z^p#$)cGdEG=Y7NS8cJKfv^;3{v#W&MFrOxXXg5;S(!|ytE30dRu}&83Yw^gP*x!<8
zRqJo3(zxs)i4d5m<2_&`B9T_z(C72g=i9{9*?bF6HLjVne+$0^5bW5`Yq(kb);qya
zI^VG_FE7&xN`!7&ug;mhpNGU|;KxlWnFrG+M2FKvAB7{UJ#Se*hAo6s6gE(*Y3)yPA3@~Qs^
zn@Iz<fb-3A)S0a?WWv#O?^!``F`}ejp?MV?9NPHeQ8r4Cf>hi>75NO
z!hgq+#s>^t)%xX|pMIs4O7Isx|8|bcy%xshvhG9F%y*{!1d|XIAyJiZ)335&cw=`F
zXNeINdLe#?%JWMslD(NZUwHrtHXU8u`+BulTptj<#z?N)$
zpD4`~&j}1Pw~Slm5Kx)Lj(fT^M)udDPOyaOu-X+s$kVFIa1<%#BCXOP-@pE8vg?hC
zd;5>St(;!EG;9>}W(F>7J#56&t+df}qgHAqa(=fe+{p?YJCOKC%v{47e^kLw3JaE;eO-hKv6mu&6dO3;kBD
zLhwVzVYgajy)#S1h_m@KyN2kR+EWE*?n0M3P^ALqpA)L;NLa>fPo$(P17hZqkfRWU<6`&}1deO%@3r`a6v%O&Z
z5&vcEMy9hDB}Z)OR5yQX5SaqSUxr2LIk9OjneNFfi-Jc>$#BLLQ_jDB1t?UQRv0}G
zdNE~L0O&(AYVh7aAYX*K>lvHSl%(W)$nA4sIlVV(v3$`%3Y=#&<>jX2*U+Ov)d#Be
z`W>B}bi^=H6#;%1|1LKA2N#~W@+V6k=|oXmT8MYZ+-i9^(zY520@
z7;#G-CKC)Y{CsrTGN>chQ&+hGpuf(#fDbSczGT98$Pn;1$M?3>sDn|t7w~Z{NxOS>
zY;y-c8E0bpBi^T6i=I^~?HTqhwC-!P3Q@`tk~HyT4+=cv5#f5Bbs*nK&ic5Mlk9=~
zL)?Oa8xC&2ecxwGGGcOyu^0SAM(S~aCQahKm%cPrh&a%K!BN$q#44kwhjEgws@_9+
z=)#HRDS>Bd38#~Wbslfq1^-a|7X!`38X?x1a(JLfQZYD87F5Hi$kda?pT6uFY>-x-
zW}z=#3~v%^apgJI&0?wu1V=9o4o%*C9C5>@v>nkJwmOj^dZR!&WQ!SSM8HwaZfOmT
zw<@-reoMu{Q#&sm)Ui$JyOnKK&kN|4Q>IRPHbrtLNrvs}e(mWE_=CR%>A5~RY~>sx
zsDp6I?y8G)1&3hcLiV(c{S&|>(YMjEBb}c9Rl+>xP~PmobzWIz(TJFX<=wf{Ik3T9
z@KN%NAY?xGfOT}|nPF-0`V}ay>r?e=%Y=BknWQVDwcO)57$bYD`0==Y?p1ST#siUm
zvzN0q(gaibQaw@77GFf^4O@)j#q@kU?VEPtap$B!U2A%p)1J2%UwqUCIwzJBbA}$K
zoqY`xwE@_TY{+vQ&Crvi4>bh``s+2Nfyl;%$2p#JQr590v@1o28qv~aBJ(GPMQa|<
zINn?m#``;?lZ-tN_V9TFZ09hmFOi3yM#}|VHog?AU@a4SNaTR=wy+ZwTK8W~o+!M3
zc>8UA#J}?K{(Js15!cp7XNv@0Bp0a)h@RaPV_XZYzHIx|9KNss0U!j~y+_2+cw|1D
zB`eKe3f?EWnnm3-8ptM6PWiWKR#=ARe6zdp(N&|qfvVCZbDfOP*{tN1s57A_*QvaS
z6CoUAH^0?`TQJgF+SLDw*049Emud8gPJViHqNF-&|uWLU2g}m?zq3|1(q{iE~hCe
zMWq&TOT3?a$6u(qXGvThtI$jmDUs4X0X`Z_)HW}|$R~}|#XHnZwaRlO6Yy0AR7JS)
zuQ29bke7LgwVoYYBQ-(fB|4+-pb#}1SqD2iw16%VT<*v_vC^Hjf|E+1{h0>2j4C0UX8gzm*{@nY@I}3$0oJ
z*tY}@Z#2D)BT8z4(H5+#<_U^)e@QI=(L!usS97eq4?*#|=4C}!th*njGx|9uq1y5!
z+V*XcMF6r>^!Jb`A%p46;&+H50W4dJujFZW>dNr
zcTP$O@WiUenFmo%vJ*7|h`a7(-+ME8?%^Y+Uknssf!UikY`-UP?C|KA2=EXvheHW1
zF^oTq?i|FzP%2ZL^6-|nU0!VYPnWa3`|SoTuko6TE?__5?^y2J-{}_f=tBT1
zA8}_yNX;yKguiMlU9sUEs*vUI)W$Uv{#eeJuk6g`%+&Xj>q>f}UKseK4Ly?d??Ue#
z%-scR{|eduSd?pCe@Y#x2oWfG{=+7T-iXELZaZjZfn&eQz0dL4(%&EX?2Koro^)60
zW$Y2A+jm>1i2J^;&Lf(8$^H
zA=_&NF;%+H)#g}U#;G_lONJ$H&F;}h2e;qLO5uswElPbNbk@_H|F0bGzx6M^wS6eT
zDjx1qSxg#4;pS#P2lc$~9F{{nzkC^c@KS{J
zCogkTfT%J;Gamu9#aC_IcH&h~k>OKW$u6%s@Nurp7IEk1=iDfowo&z&D_}22$Ifa>
zLa#(5HV)_RtWXbmtENSmfTFN31j2*;6G)R~_2{
zn$WZ@RUwD8Xa%Uu|abVC!+Z5`sJ6(GR;
zYmyeboZy({|B)=RJ+g=45WIXjzO5mu?@L3)eLJnW=@p>wrYSqG5gBTM)=DfH+~=C4
zKt~4a$WcvqPUMt8;o`52X#nwpG#3;uM&8vEXy+gaDm2s`JxP$SK`h6SLgvQvHQ1=!
zX6>Lb6_RY@irQJ~lqqHHW1U!=ai3X<;rjO*;(gK{<~@-q3b^sRvHiy``+Lt_`ICuE
zbSxRc;Nc9y4e-!dRFHT5mRYYMd1E!niQuoaj~anF==mOaa2
zpX}BS12{*$u!^VKOYF>!ewdN(TErsFt2#?e_#XASJ3XIRI$&epf9lui`2O*&7aw`d
zSM2*D!bO7Ej!i*LRhP=uMPT50)|4x;<&9s_
zS@NShT5b{P&C^*LDKCbrG;Tb9S0MBD%iwGN>@%$b@Od;ni@E}Y>uIr$(~*sNTLy96
zC2zBB(DYYxj>%tpK0i3o?%6~vcT69+B!|tE8)~@VDsDTcvRCdQ?9KDl+t&4^kZM)#
zjciG6X)p_x-bJ^28TabJxuSgL-do(?>w=~lZ5~*E)hN6j<5=GP^qOb_`rP$oqzm4g
z!+V-}a!Me3x%4Tmt^V>|Wpp-3I#W}1VbNSilQMI?=?O8MjY7A)dAHdG=6n`vSQGya
zvHPzz62~BmR$w@&9Cv|!E~5J#DsYF_=v=|4B(8V{aYaGUAEePX9(?3A|xfT2*h2
zFlIUSiGZ`8W!-pJ^Lg|}KW2CcOVd4bZx?mg34
zVylfcGVQ+V969-hQ_m22SzJ|Iem8#iOztny@_{Z-VvY~lZOMEK*#CDs_y^lUh=Mgp
zmJH1@gd@v3OK-VTBT3Mu`6uixppv(NbB#7;cUUr%>OJeS_NL_G!|f^yIz21ZoR4aX
zmtAYV?0HXP>9jub75PWz48e}7;exp2VH%SmLOb@9=|C_qX5RRfB;-}}0)#Ve&^Q?a
z-O4;e)r+mwqX0)^*jTBNGUR+IEYSMg_jG%ZhppbcBBeCuXc{H^m
zDVbC}GQ&f~8chw(746;4xM)l+KFT1-{YC(C=*ubr;5UFS
z)!n~E<`|vSQoU!4F%Gs}{5+^vKu@?6*_HGt4SjQST>96W(g_z+Tq@M>COt~|x_mCNCNXWo#y$}z
zl}<{ZsPId@)^GLEs^5S=CowVmv~B-D)3$xh(L3b;hyS>T!2W!aIF1);^f_tW3P5on
zTq*)HpY?sW-wKv+muUq*kp8Gt<(}HYt<|~jaH+~nr9ysBbSmz^!fC%7hCIJ`=p!GW
zg`Dd`f()Bfqr&p&CKuIg#Urigo7~^!k6`RAKH_mF9E-~sq!3*Hh;ebWBTgMFF_AYb
zbDk-eI=ikN{>^~7ne$dpl^s`wr1~i|akL8PaxLL=-&(IY@P94!R!jz+&lHy=buxVU
z&o5FcKkO~Bb-c*)tu1Y$U=LaYEn+c){uMS0rS*TaJs^g&k)Ni@5jUD<=h{u2cRc}?k6T2%0dBW%G@LBLV~bq4e@O
ze?4OT>9It_=&4)2?9Qz6w+Wz!t8xNR8MTQnftp^ni$aG|A$v|3B=eI;H6%8uYf=|0rRaT>?v_o;w-hRl0
zKQSWv`p{4-f3b=j6lC&$H$po}3LZhsKnYY4mb(cuR9ch$p%d?Xz<5-7oxW)7FveO;
zoQ@rI-buAPFWVvM9;7QllvDWvu#E}}i@LDN(`r*D7(U74F~gm2-fYOhD*tj18!74Q
zB6RR#n7X9J!RXWawdQ~b*OebEahw>5EL5o_NA<*E$IRf?AHi6P?Q42((52E2f&)%t
zC{thq;amV)MxSQouoscgY28qVU5n|
zq}^(yL-ht|>X5Q*g`b#*jFP}4pW3qSLKUynw0Kd(AwW;|Fa8Gu&f(2q+L=;vuDoU7
z!O$#WO5)8=84bGUmmT5`(|NjcWWZC#Y1`%FsJw}!V@F19Fu7M#j4iFr3IYFx|4v;8
z7nO`ep%DS7!j=Z+To|dC*lZRAnPEMtiFx&^Bqi_(bw<2i>s-%MhHdyOPrDt9zF9tA
zBZ3Zx(bqi5n_cctN-*-2j*Xaf<<4$wtVK2}ta1{BE@%r0VrEDHu};IE--PaMXLg`R
zr5`>voREt*qoh?5pJ|QYQ53nv@o>6$Q->)|{nP#-u=hM@EC1j{UxQlBR{Gv2DshnB
zas^;Q*_XP*D*zS;?lOy*sj_2Q6Nq3iJ>yIudz{vC*Gux%w-Eq;YL+4C3y-RG;3MqE
zq=J0)mf}4OMrm&sh-rKYi+i|V5F=r~8x1xVkgse~;a(r6yin-+`J
za5unWg+5UaI-Zr%-Iie^d4bCz$tZCZWs+bw3Lkatib37xA?Ck
z_(AccY-RqkJA}guEP1^RdlIl+4a=XFgrp8^7a97k55S}(bpGHbxoJV)-!Fo_o_?Yzgs@vX&ZdJ
zH=y9fa{ze3)!NQ8qijZ?ak;d(sH7~^#(LJx
zO*V4N4k%{ws6)_X-zF}$KBtLTs29pq$BRj_?fZMp!4hgEADZQq6TJ-z76`r)qUh{+
zc1m+YajS+MxnF!=DJ0F6@!hX+A068RAhCZ7u!<~7X*F2pS3};sq^Zft?i}ZWZnY^U
z9;bxM&VA$!#$1r;0tw3Jf}g3AXM=Z%%r`jpPi%V
zrCdjqe)B@R&H77EYM#N~JsB~6!IWasciGC5`8LSM^KH7R7Kg%O>tT`+?|y*EyEE2G
zF4E<4%vLB#5N4H_61&^+7y9dMVFt1xwFk8Bzo`{C479@+`IvA{X9FV$L}53R2}P_E
zv~_(Tu{ld7uiwk%-6=Jcn8>#1-2Q<#aqrhf&AjD5n`%Cw`ywAc0L{ezB8dE7KFBq%
zIpfW|>EA-icfQq2Ma+0G4-<4ixuXRwTvVAcxWVtPTtg}g@$Jn
z4_qx{ATcf;Sz95UkkbEFv+rA?1dmgwJ}N~8R0w8C$T595-TPhq_1HNjSWU)G(B!#a
z{Gz9d$OIj1Vch9es|**dE{o}+_>-R7pp$r*N3+!`zxvCADGfFIY3$wv4-eXsMc9^^
z*#J}}3RGxe2|yafCTK$K2{!4eSx4Z{rzj>_287EoZ>gx}CvF?<>*RVuseD5R
z-W~yOxGCkOcj0nsL_th#sZI60Yq=%Z=YuJO@41%0{JYdJG?@Pp_dlhe7vKum2iHIN
zPt5@zUt)=LjXJZG=5A%QEbEdIspLDt7r=lm4^)Rh4f>_A&==3RT$nAG#*wgbNAh=}K_R7NkJ9bKbi
z$7w@JRw<8J?^ST%b2zDUXsq&Jc;OIec0PXBoZBYe2fEGSTDF*;{kgrdQ>KvvH=EoK
zyo4`CVLfoZSe%cuj^_EeYla>e58O^uoI6ejqa<9XP_yM#3
zLihgT`msMWl)pP?7)d*i`v`^DE1#PAG0$?^rA29F_hh?Hr6sc@Y2CriWJ#TKP*XiX
zXB>xwvf~xKo@`ai_+~%7mZo7vv(0!RWdo<03~J6n)#J&?29;Gw3t~GvQ%}_-4-fh6
zOSJhmh85_g^Pu0BUj@2k%=p>yWBDD$mDny5%*CsA04fIoDv(%PGnmG#bAB*L?EqyJ!fbHU9i!e5
zL!BCpt7qo$QB_(@oz1Mj*tSAzjqV9eI&AdcGI(Kt&typROqVm*;!|in?M2%3)sili
zj2tYR-VYh6V)h;K=&wl{7H50gi4o%00Q`0ltI7;B_u?_Lsf`l4bFp(t~8x#I_Uh6+DTl~{&kbg9kqP=y$
ztA_VYKX#So4b7gezG0gS#|j6AZ0wHG25sAf*A*J5?WG$_uFJjm<}f!DaW^8P=WdG=
z0geVZK{<#$MSm$ArI2<;{|W-J{mXkPBkc_HjbN
z*PecaP1^j`J^c-68mixR^w@2tAwiCgXlT7~7?)|X^@GlioD&J8298oe5NrT?j!hsoH;*!RZ$whL%8yPmu{_MwVey-4Q&CMX^DL+DU9B>6#$}<0g+Z)l
zUtZ4Q1}aFRw!sG{wQva@Pi-+m$)_D2kkoJ5~TVmRP4x#K`tk@iF%fSo=2+;fq`3
z@?(g=lqr=Qb#v&~_M!eENOaz8(yDSy4`EvpJG}hbe+%eXuP5KWH+f#XMe7~Ur(a>;
zzkzV(KF&vE8Fa2B6iOw)z;kqO#$%97jW}IG7Il@-P0ykxe5&g8l8c;bA`20Ga?IFK
zlpMXKvsGta;JaFecXWC_s(iWNrF=>AVKqQ>CeqAM;DNbw-8D?Ts7W29{xV8JQzy
z${6PC5b|a6M_etDmP5Wg5OYz##Gg=K{aYJ+FB`+nplOPun^c>|
z+P3z;rtYFH?4Vf&6RJI$dbxAKSkpbjhEXSs*PT3gE>-on+%@JSTuf_s_j4-|^d8%X8t@R
zh3lLM&p8;dY11#}u&@8r!RnwTfqUAfIq}F)9TZa^f4$Zy179#oBS#rl;UkekeKrN{
z>Y0JJZ)Z=46`|uSNP9(Ib|{&MS9E`T2_LKeVdMrzXlA5)7A#qIYLyJnhu&xkIpn>b
zH2#*XUp~Bd?+$6HYHZ7!NE4KhVY=dA1xd!NqWiv0YNNa@c=;O#EeXUSFAdeE#^<
zHuo%@7;WyOMGU`
zEO}xbl&Ts15(VzY&GdWa!SN<7g8r|NFfU#eYzl~F>P*JJ52dy`AB&&4Qd|Np6lnHw
z+fE+|!O4`I$#9Lv8`enUwH*p$@g*qkiW9H(k#WcZDA0jnP#_B(jIS`;@eQFqeg59Nl^qnePbk}`O^8#HNFloxl-m3-*+iYj`$J~Z7mE=?Iy
ze}zHy_&}5vx@&GdWP~`hp2PwX-iwkZm?0l|p=uohwcNx35pcM^u$|4uesr{N@9Qmq%bI=eAqqB87%l1qy0|v8ofXAQH+BOI*Qv%Jybh9iX@$BQ-9ZWVX#%Xsj0EhRA=GUe5+1p
z0VHv?RGK%DDe#fK;e6xLJ7d{)?z3EzD*&u!5A@2-Q3PeEHzLNXhQ)f4D{6{DSw$~g
z;<%5w{<4I@{@s5$9n*O9||QcP=<)cbo*P+@Fe}JsMGB%!_9~XBJkY2|DKZM7dM!+<#*QkgBNOk5m
zQz>~P<6iL@;oe@KwVt&ms5wDO#5mbc?8{Fg&)t(OzA%+dm$j3F2%%u(We*j4x(?)k@<;WLdr2
zuO6F`Hq`3qhu*b~S9vx$R=kD2<6H8k3TVA9#y50k?{+8^Wa68Ee)h8L<=y^6$w}hY
zJK}eX1VtWCJ%=BH^xvB{Y?lBywH$zTGJH(DE(%Jf2;G1Bl5Tc)dT+_O5H1ldcCw#p
znVZHw}b^Ieq`q5?o{@|u+jBN)&J=IkU($tmsspz+R
z`W{;3cd+frn^DV=G087AkZWb6WICAeBt|4wxpta)c&V8;1{BBa3GC)#l|$B+I0{Lw
zK!vF3D0a~(sjt*zWFT%#D(cDA0)k4e16L7s599bjVXWzh_YE`9b-Xok&mSev4N_C0XxuSR(m?wh@Us!@s
zoQ+$dij~Rvl@L?mnVh24`x$1dqoPKH>~R1K(P3KhxjHs|YRvT1dvuk9Pl}0$@MMh?
z=$;DpHpSkLeFzeoBfoO7dmyu_O&o2T`v8Q$&N8ZXzO>b`yuRA{)XL?`j=kgPVYQe5
zRC3e?FvF1Ea<@u*Ol7lO4&yd8Lfo{sI6SRoE?eE?c%JgTu&q_)v4l>09gqJsjk^zr4nurv<+%0=u=783|J#U(<
z1l;wJue~AP`~)rlB}H%^J)Rtc+WguJ@^i%l)BT#_
zL+RYm=qe!ZD9+?We+JEuPNC9D6hA
zdpqeH*AKS;_u~M*K!l9K5zqk9umVJtat?LQR7HqW$0OL)+mH5b#OE2hsF8(@1hxr#
z@O_Q{@b*EC$;_pRu;<(J;p4yg)!!7LNi`n4%O=y#G&>-2oflN}q``N?Hb-sQ$8L=&
zp7BF(IbsYUvt{Ezd{-(S~1f4VjzRHMMs1l32Q1Xw0u`Pc}Y
zupjiMX!EM0guyQ@!?K+^G87bIg6_wxc4(BC8H$X%xS9Gq&%*=xL`L@XY;?yK*mr1q
zfxr;Rf>B2bEo;d$&}uYj`EdXa3Me{+o+n|u#=sQnqaGa?Q|GJALkG7K+sgeq=ZS)P
zyXAtOVqs<%Q_!3Zw4U;`AwweMUxvo*(T4&Kz6?m58(0NZtG}xEwWvz^FW0-mc(kXXPAADSWtzg7ae`c
zeyOL9=GZmh!^ds}Uxe4Ocd~i9u?lxNTy-8(Ins^<&<}BSPE=Jy*6XN$)Hw
z3nf&Z$%idA|3}sul3~3igL_c5WYElC5Djh4<7tc1Y$Wl1iC%P&*J<+|^}FP9@dJ$e
zdm5*{+b}j~D{-hF-Im)nKX<(r`F`jJb#F%%&NV0G1rQ~xgz18p6POa6EVSOY31F7nowW~P5EIA{ZK%BE*$y!cFPnUW!H(|Op@%A(4$Xs5FB
zlJd|iWiJEI%0U~)B+7;zm9vAgC)^T1!Ed2VxHw(BHXhkHw+>qSwiLQ^q1a6Pt4&Za
z@h-m-uP@Aqf2MSryQ*teCt+&0$K%`?%EMohlM!P~s=_U=wjg^gx-(=-g&IChB?APbeYh*dC4v>ht
z$Y;r9v{kdAKdZ>?Q3+{77HE4e=Hdt0it0}Js*NAtSqdI6H!{#i9{(2(kN-7dojGS~
zUIfvZSH}Un!OxO{3sq|qR0>Oe*DqbL2k&89a`IbvYqwg?`O$lV(osqJ7xj^?B|jQ^
zlFSl1(?skeZXmY_CG#b1c+n0fUU+HR%CiU0L!;Y~mzB>R*3
zFU5cH&NIABQz#c!NNixXL1L-A=BQvKjDzf}iiLcR2ZZBv`v;V8Wdm~)bZ(bn`^E0P
zJFDpmA#OP{<9?`yc%IU<+(}bOqYOw3PuT?nt0C(M@q@ZABM6=S>=H=o#No}MU2+JG
zulFg9hW5=u7SA{|*mFV4;8KufpeltwVm59pPuNIF*iNnl@^HMOf-TTD6SFPs@TkU{
zo@v`)U(Xl$>l<;ap>~wq=WvPAz
z*wjB^zn*p{KCA)5)9o)p>q+p)dKcaLTz7G*YL<%$g^al&FZs4LaWoBC+E{_Sr>BHB
zC0@$A)gRS2`-xuG;wQ~Ogx)ND+#8Pbgm%4?Rt!gMd+T5NX;KV97v*dLy{!sda*Lw`
zM~wEk0UT)38cihA+@Mu?MjYNL_N_5~Mam^k2T|ISSYRI&i7ZwweKcljX4I=}8qwbE
zFOBEVz6ko!=+j;pBQlLqkp5LGxKT=4GPvL+oslE-{T>&y*?kSqU6zLv{Zd^^#rbN6nWo)2X+<@~iTEMW
z*5b~FonIbaU#|+qA#gJ=TGSbEEB$s0a#M+*S~Tcu6~`1~I5oH?Ns`Y&-6-Sbp5}Qw
zw5C}4v|)v|?_y=~pglYpA^F4Sk`koPz+mscucz8tA6S=@xjHfQwkT1@4pYQ0s`_LFVt@fXGiwWM$
zi%^COx{?R`oA!4gG8F+iORC1u_GNNL&vZtE&eLD=%<07br7_HhSKGhs47=R
z(FOgo5n4FtaW=}-`23eMv2WUS>j9#`>eh{*&QeQ_f*p>s#1b|eZDT3=$-7)BaOjt0
z-0J-1=iO5IDQJ=x$Kt2mHtk-7mWcUdY@;!LDHuJSULD`fPp`CXE}$(Km&@-8Kt-yA
zqa?|gsDY_5Y*a{%61XsCG;^9h(jpP#VlP?TJxeg5OEyc~eV^v1-V}F7hl`@Cr9IxI
z*5&K9tAijqnj`)8c;Nwd!tqY!XS_lI#N#BI84^@eVNA2rAzCpv0Kd>lzC^kcA86=5
zEZH;jl%6*uoMUB*;raZy4D`qtIt=;eTxoMpb@n*rgs7E@r+Z7v-W79_36IA9H$_CpA>HFyX(eTa9U|
zQfuPls%
z%A(JWBEt#$9bL*+#ibCRZm8QNpf*EQ-pm)eK7nge(xJ<#TWvevh92w@zR&~M_UG{V
zus3HP{qkcS@L>yR5%By59RVNsZGGO=sfvrel~||3(IVD2f~p?028ftfnb9KgSC#H`
zx+N|AKis`{SX0@)Hy#8;no+9MC?Kdb3q@&B6c7C;CP|vsRVrVrp!g5KjmH^(Mm~CNw)V@{0yG1IW*p$4-lb
zY-trm31+&Pq8mooXC%R2)BL9Vd|&+$f0n{%YMW1YZ1MhVMEH-7MmTfZeuc^RG@%kF
zB$!f+1G+L%!4@4oQ6_qjd(ro6&GZbZ5Eu2=%3=hMIs0jC
ze@$0u5i9Ss_J#+a&04MG_aC`iR$~kQAlHUR46)VdqBmMrIlrXgYiQl5)4ku~WeCGg
zv%x@JQGdASj$rghLFKU;drHkZkjQ;KDK+Q5o|MU=T6AV@z_NlSG&whZI-OQdJ4Q4g@#DJ2_Y7I_Yl2j^&8}1DTDM4?hTUV(lreZM|KimnK<%=0
zu&|R+u(Y?^q_V|}=j-1;0z`+v9skLBj2yQ0IHh_`z1?K{z|F4|mV)!*h~L2uqayzW
za@ZjsP_oP+-=A{@CA&?ysotK}wv~hvzbM4f7Cb(na?Fd03=5P&Kg9lTw@u>j|Ir_j
z3IZQV3+uYG{+uu*H9dG|cjtlyNY+{n;CD9v5+Ev0&5M-BPE8Tw>|H`0ex>EH5A}My
z9MTCzI)qpj>--9ng!*lSu!x0cnoCADUY*l0?luDTF@k{|S#W1I&AIV#ZgCM#_}7HZ
zGa+3nP{9;`FINfQE6d9CbC@3)mP*x2C5dvSUWep;ud2P1>fz2rI6u!k5|WKOGO(z0
z`xuOC{}l!24kN1*I}f4#UG=A`7cgsP>|?e14);tm^`UO&nfCq8hm*SUXRG@a2yG5G
zon7xA_xomSKDCBCK7eL-rKcMTUjmI=(Bx<~B2nM|3L{I?eZ7!dkkrQn$s(jDO2AS#
zccG`LCvqfMx(!YYE{;vR2-M_aI+Gd;7}d1)x4p%c?GHZ2{R$Hf4~z~%2PhmkN{Wqw
zaX*kQEoairIU_nNU#HxwQK3KQnkX#v%YQ!+{o4~K{IAkuMgEL{b~!ZlKxYsY
zn=1*qPMq}SN%3RcgN&t=baXMMRO>kN6j9OSn4T=cK&&5P~aZz{e(-do$mBaIr6Xd?%xgP
zE851p+HvRjG;wEK|M6V2dxw+(+FFkI>eJi<|9~A2?$d6)dZhzf{S%N0q+b8NrL!5;
zF#+#0*^WKhHX*>=`Mjdrp5sieHcoj6JzK
z7Hx!i?ED0O<>waj0FID)NNkdW|4OZSd7%1%?i3h1_qTNTA(HwFL6Jbius4-48p}gi
ziL$tzdU&y+V`Z4y2FA?Ynda5Hh|~+@fO@h@*{dF%l{CrjL5g+%Mi__hPd9V@)^ZP+
zsLTo%f*rEib7cQzf8;Avk!#{m$^P{%1Ci@ZWR
zeHfRa%oSVk`5d!TsSMCz?ZvRl@KEDl)DAY?y=w(@m^c={fAN2w$M8U)!?7+T9S#N!
z&3fSAoN{DLwr3Hy;H;pLTtOw!Bga8oY6II)x1~ltv#wvMclzK{ONeNcJCQU_nW(I8
z!$^XjM*V=ZRk5(uuq%IE7(o!puw8--Er62r+WGbpES!b5He@M4hw?)o4F5;eH0L?U
z?XnS4OKi0@W1JFHzGexe9ycD;&v}iypXR6aT)))l~M9r608Wyi6
z#@C0?jn%Dv>mqit@^_|&fDSu}VWSQ0U-r)FTNlBxYSeFdQk?u3*ttt83LS6_KJ<@h(h!d_tJ^VYUP{CFAe8zfJo
z0vpbV*Ces-D~j}qY2Iinch-Gf(a0=K0Ei8?`&5SgpzD|!rV#3M8__+eIlZRi5bu|N
zpXckh-%F)`5#|2*qx?g3MEtMPur=8RmS@Bdfr7p@q;Fu_xhyiyozdGfl_>iC^ipkY
z#fz$I^iWyNXZskOhPswW6MCBz{Neqw#U8D8*B^ylOn1
zVeHdCj)XN5SC9r2?j=SRc%FC%7XyWR1*RFgek+|vBV7|6pkA0UAwKN!+7alzJT%YJ
zYc?EG7rb7_iq;=(DN&-QlL2mi1qN{(2UPhF>9B;*cg;XmgMdU?`$U@
z^zGh^(j^TZ4Y*3oMZMwOJD@8(#H+E3_xtwx^4fvL#UkzEj};9sYBJv~_tW)m(}!ot
z4$<@p>@Vt_ItP^7HT<5vnmre`{Wh!^1ou#zH3b|#ixmis(uf9Z)7?9Vd(My*pQA`L<_;^_{Fsu}3?mI*)23r$W|%#9Duh#x
zhEUBDQf=WhZLW|4K*<7$;gbZ6HfSmec%ioBaFQGOW_xsNal1L0r2*P--`bJ~tcRIo
zxB~7{kON&m&d;OlXK(WKom=^ka#Q2>>LaWkp7t7`u%wH;M1WL17rH@c5M!QZEX}8{
z8ADTabVkFhGd70KSJj90r8z`SC+*AtL{W9<5k1JCw9#8X%QO7rM^RbpOEz159t&RV
z^AA16$Sn^efbY6~;2t{F~Zzs%LY<(Kev|uj#&b?Sz#(
z-6qytQ=DGfwn?ZmcT5b6*N&L;43roSyoQZ#u71PANyLdmqKq>vG!*&-w;SSNer~V3SXCCzbj;hJeizm^
z192|A>r9n^IxGJ8%7!O^LU7m!MRWCSn%KjX23pBp!v-r+mBm&^h8A3IDv|mZr^{=$
zmhbs~x8iPU_ys*1UJD(Mq@jG?b=hO@{=M?(E`S
zZR8|y4{3K!hGlMLdMxyhVN19?1
z3qAdN1%>FYW=nKYQEYYi9qXxa#hzD;ymqLh-t_4%7KM!M=%WG7R?s<^F}qp{uQaw$
z>r1@!UD-C}Nw2`nZyEH`uQ0Z_I4e7`BXcXF{8w0lt_TpUWx=meT?z{bK_!sZM!BzE
zWYd$?TyZVs>RXP6P{4xyCR~OX3ur-l|LK;)L9PbvS?V}ge}GZinkAq!_kjBzN_u8i
z@=4QkfzLk|-;o
zH`>>ge9DyWtF+k)r8@Q38`Bmxx6GXz{HY6F5{2Qa+6
zb8d=2`LlL~Hq#vH>Zh5`3Wg*(xr|AgamT~!cb||wZ!Z+-vHc_5MHd3ZB|EBFmmLuWwvSVupcSn^*u%DM^3JafeDscl%>2`-t3X}M^E
zV2clkssF5r`B=ep%keN?BKqmnXepyDjzQ?h&_J7gT&<;l0MQkww}Z?&Jdn_wJ^6fP
z9&AidBvG{63=$V|nU}lfgCnpfxWh}$$nxr#%7cxaH@C+(OX>H}QE`aTl^3o~4I_#5
zrbfziS1k|OycUX}Ra-XT(S#d`Qi1-NcyB#FW2$*V3L;Q3!j2ZXSkGqsCI&Z|W+MpQ
zI2relK2V{(`IFvFS(BuTa<7&YGP67}ehKsTd!6E80XqLW<@&!qtpB$md)a{M6Q1@X
zIZkI7a-}vWdd^@AX+SB4d+B6PAhl~K8YxM>x9`C~PIVbm>bvkJ%?jcXCF>RROWyCb
zzwK+@)qGBj$$DbE0`bs7-R8lz1NH>Cm?01$qbeY
zmEEci3?*bgbNw5)y_754T4@Fp2wU5gZATo^Qto?TwE9lK2o^s+0$e7~vgbl6V;|la
zw}FX@xuVJ66VE;*!%Phq>X4;<<7^iE5URzy`~pp|O1AAgEnH+e%NqW8lJfv)S?>O6
z%kk~ug6nF=)NuIrh(W~XAN_0p2~lQDEEfS49%1H123QfL+ZtsDi@&)l+f{A1#02<_
zw&q+uw2+qoBw3%l0p!$V8}A$PRbP%L@Nn$7Z%7p*Q3UVO82bs80maEv%;-dg;>1KF
zRh74^ie*gw)pO4bD+at|>&$fD#Rpq05--1anY?D&!P*sO@|)Mj-y+{M8$E>-Wg7ue
zDkBVi;go`MD_&+mD*)|c`wLUFvUaBH_THmou48ZPhTrsS4otXN^B30|eKAkqVW;Bz
zP;$DZWMTTu?M79f&$>mjxo<|Hz~d=Lw)fU+=lMmL^`9-+7xaRX9FT9h$+0BBx51RT
z72j_kW@HKy;<izYfX)Z$ffeK*w;a!
zSIxV8530UQ78I9+aa(cx)NwW1WVq2zsJ3*flQa~^Po
z2pF~rCycA;#vLMTMdL^F+L@jmeZFoRI9V00rpPLn;*S~bN}ngiOm>xeP}3qTpd%ej*%hMnfkkV$e5D~xG#+ekhwk##4A;oG_&&W{sk
z)Zgv7q4$e_Y4ijl1P!+xtoV5`x4evr0_KOA2k-S={Q>EHN$DeBfI-YuOXRYxy(aLFO+6st%l^kT8rW2_c>
zhIq?qN2WCPi8;Tk%>8gd2_E(x?f_|{7Iy<6>sPlvR8C)0?L3XPX$d^z=T4w0oUdGr
zLZ-ESU#2+M3~1-d6TCmKybiOCf-&~|nAZ1cL#ow4WBnXTVSz1EI1!|{6>3l@jVfs?
zLswTY&+oTVi}x+^PiUh5M@n(j4v`LsUvqx
zWZgE|ExGh(65wucOH0y5@4+|W}w7TNe*M#FVF`82g*=6-u#D
z7^_S-t23=l$$MIycw2);&N;=rd=KARO8$QI=Zp7Ps*TSrgnDu(9J`5S1=;Yx-?MD^
z^b%J{5MWj$suy@m#=UP6E;BG~S;$UBndJd=WpOvBi_l`7W0qhZV?9g`iPe03&dOEI
zuHRiaK^6x2tv4xn2k~&6J9DOqB=6m50)-SdJ}h#~Qk^Bce(`qxn5vT0FcDYc7(>K-
zt?SV=dKKTPBd(%fr7x8VG@?$!2q%!`h=oE%9_#J^T0^t682Byj+`)SWA{0%uR3~@K
zhdixiG<*o>V=AUc1tI$$C!Q%MZkv@2sBk;iMn$ZT9Dgim0ktWN0`@446kUnfhMj9O
z@Qh;XKWYEyHcKvkLurbPn09G-8C0t6=NM#vQ|juN+r(RYVXL60Kb?Safwd7DMR9TF
zH~bPWI2-kjkNVn~L?d(h*zDWXKmf(qLA~8-|*a7PEP%~yde9@%Z-eYR+XB>mE_k4jPv5yXZ*HpNHP<%
z0yN(M4K;m5C1M|+-qJ3Cg@0%StH`@%!5u;ZdyELi;tHL#V8|?_O*X@0SOhO3z?8?D
zs66l6SR8`!)tvI0*fy{;sWM9%d&k$y<6c**iPXS1!j@S%qdL+3v!-HU$oNudR}5P*
zlv)b6EMXggP~pv%L2l9AHW9Lo{MrWkgscNokcXx40X^l?KD
zi7onSg^1n^oYD`PR
z0o(GL+iMm>y2l$W0N#y6&6s5P0l_gVuHYo+7JX?mZkJ8sq@oVt#RU8gsX{{5^N!Jx
zT+sRY>7{HUc;W&L2|(HS#?F*njOK7mp_iK?LBYFfMEhdMRED$e7kS>59~yT5>c{{)
z;=lBkzX+lXXMm<$I6!N^u|iTGO|o#4m8IO$9z?G|s}2vBBWuGBujpA57$tnxIm`3t
z|AlxVFb!u*+JKG&s3%2rY={OsvmTbPb$<57D|@;B#+K+4^A?J}cbdit_EL+3Ia14p
z1JY}LRyhQifWzxY5a5W##~a3KEvTlDXNSE?G)uN8JV(Zh{BfKx(6_J=Z`~~a~V9pv+Q;H$Qim8iDBVVzYO%k`%J27
zQ4g7tr9^+1{Ui2$e(JLNu|`P0Ipr6gDRW2qi+9+qr~>-Tp5HGK0y8l=a3#{(AiFB^
zasF+R(OhDLp)Kt(UU6^^D6Uc5)AyKMsvN%{t4F#`-nrk^C(R^PXhsE4jD>$&8hpT>
zK`M2NE7?Z3c&Mmv%;h}g4dc8^k8s?MOu-zFd%GVe*&qKve9$+zfA0mMF#J9CW^nl#
zY&7J{A05TqNFJasMWdw-@~sXH)?$do3&}!{krJ(v{XS^fl$)W1lY>i(PIh`j+fRA%
zeq93yGKp%I3$u*UT8K?N4+R#S+-jXg)RB8qC7!g_?&^8iU@=)izU$}ayBo3e
z8`Hf4eYJ#zLu-e8k{)Vsjc_}zO5aeK+-juey+8j$xy$(M-BZs5?7hxzhKy_lH0g;H
zeU=j=Qro0}+0~?fYwItaG~#*eyPK4(2NxKT&ht-?Ch$>y`8Ky4hSO%=;0ldUi?xJ_
zNNV*hU6iB`7CXg+6G`-=v`_M$T`#NqiacKqfAex7_KuH1e&;?cp4l#m;P>f1L-Z`9~vIbZC`JygREVf2=FtBWOx%&0HEZb*7o8K
zJ)0E=Q;jX`3(u|O#Y)5Rve@gQsLn>ME$6L8^s5cvF_`%Z(jm2>#UeEC*fAb95||Sr
zsb5HOnR|aj45FyB>|MPdZ~LkM6K7-ZH0?ON3i6?3ncaUyt)Nr@Sd!4z6HltFUiiXn>~V!2P9cd|m8i}hMIXV(5T0TS_@8Z)
z@;)Qd)i=&NL1&s3WnLuO)|3y}&3?R?gGII&SZ5~X<#5t1`_b8FK_>8Ez2reLyrdUe
z*DO_I0ALW`ML>
zFY^2~i0uFW#i5OAaX7;#*t*u*r6}AHPsK-%u*t`PFW{w)(`$8qV_t8ZOWZ#ZXxn;U
zWj{3xSl#nOql{_?NS*1>F)0#Ix^EG;yLilrJYIW+JJ2^H81l&HQ#QZgvrj8}4m4@b
znNz)03JPa=yM9CwI^Unt+gN&2?TVZ3K6|Ll
zbc>SsGV0vc-A16?EJI=O-iMZ{LqDbRKQ_%qysl4rEppFH10(Um&_csbT_x#N!nvuW
zZ5u7j`JEg$+VgGMq!cCt!UG0q2G#aN;4HJT)veWud2`
z1)h_e
zlZlNA14j5-0_7{=*2Ko$Q$0lP4zXsV)nGCk*{AADf;;(4UQQD=Y@0BuW5k3{*B-^_
z$6dG^mW^mxVoM;oa4}9P-blf>3H3bn))nMW$mkJx;H50F`olm-1XZ!QAum1bxtnuW
zpyv(78ZCa(5p#RRy6-DV&X?@b8lNFf-&x;hwm*!Z$(3dVE_kd3;jU%2wydgk+K>l;
zjYZT=OyzEL4l}O<5jU|jWn0eeP?Xz{8X9vxt?N`JQIu6#G+vUG>&*zNPEAR%m5$|I
z1!+on5TW@YK>@D}T0_tpS4f}fH%S$UQeF1@2uU(7fp#nRAk-bg8#K2wG0sG(Yhw+g
zyh(aj7y5=cHh6&ky}lyF#ibOoSn9nG<4%z-0e?lpJQ7r8ON?wr=lsJp6G)Ag`|Vwp
zVg?-%tLep6hDxV)g_Cur+Ox!QrmLw50ltQXbqBv8=J|&-K|^vB++OwBu`DX4~5WX!9+0m`e@*5)fmX4O60vN6mANyd{
zB!=J06son35GNZGt1I`ZqWeIreWO@vn{d%4an19*U8i9ALQvg?I)=7R{BxjLK4unRR%>X!5Uvk4|O^n
z`>6bvDtQhgMSeVAU4Ko?S;la64ita1KK0aag@RqHQ@=LV(6el?qAS1jiXYwR*3O2v
z`%XOEHkNa!8%A&=@ic0DCdiv?g%I?csnh00Ryjwt3OvO9WKppiqeZwQx$@-)T}0g`
z7B|USml{8#jNK~pzYO~}`>z)k@*xu1)dT2|XAy`>O@d|l8Zv^bUObZU6{D#~AL5YDuJqOm!DS
z^<6t_>*{JU+OAS4E{E>{sh8t#l8%b$+%x1iQ=x}}@Czy}NL8RsTcPVIlrt4Mg4k@N
z)FV2=R!X{(+*#XQb?&Y7zP%wff=3M$idD0P5r0oUIz
z`nSdv9rV|MofHo^{(K3|2RkZhS#boJ9Z)&5?!=c1NH9TfvYDTZMQy$EZ5#XUm3sFe
zsRDN}@$7HWLYMeyu!HCs0&eN2g0yv9h0l9Mt%D*F3|sKk4CR2N-P#3<609^UIIWe1
zfDYty9``!qb`N88v+fwYdwA{2aDOu$PFzVzJI76!|1eH|4G1b(n=92pr`^4FxH2~9
z%QTF=os&-Z2|+<{g#?)PYb~hq#O9vcqzY6U@Zv(-v^zH@dxjKJyjRl3S$;;AOf|Y{
z!!?0uwz@AN|NQsVMm6S0?AOBGelwFd@^uDqR0KJdEndeJX{?A@6QF}32nh_?k~#3x
zgwa-3(4d>#>0e=rsqR)#1dy5^82)&nY24dndoOUA3Vz!$tHm~EUOKxAU?Pk0U4$3a
z^ObAjY~u);=X?P}o3_*p=kG`<4Dp~gNNyiun;GAIhz>x=KvkTjde^C9ABmS~IwLrb
zlDXQR`ya(|?m|U8U;p`(|F6iW|Lv?3_-ml$f6?L2&DUgc{|2fYvLXYVkg1KG`O~?lXiXm5c5*+h(oSNjbeRvJ-V51gLoi29hiAF_cZFmLgGroOY
zBTo1w6;dDrD;sg_h}F(AP5cfhr-M&2Aui^DViUZCL>)qnYI9`+xk59HybjrSX#sFP
z?i;)$(_vu;T{Tl-m`K-#=jKH=ZZp-A*SR)(lOTq>Nb8YyG}X5;QWP8fDVDD)(+h?i
z{+q7dAL996pDG+A#ZK_`a@7EhkOZ%{gl9a)l1vA64Ci-wqlZ}=k7J6fw@7_CRkMtl
zfAVUdE9L0+?b!gCif12X=+!WKI!)9e0^JcuywPH?_~?-jOugugrTf)Biy(CU#t=h@
z&tdq0ySUTXk^R%>Z3TWDuRLp8K?aotedZ+6vm|i5BiefJu_cGtDC+$*n-uM>pKr!y
zD)lcktE3K9sCxw*Go#287uOQ;yi=}l
zx(PvffQJ>``gXp6Xy9i3GUI4Va23X1E=xD=%hTKM%m$V|*qsZoQvY;B
zRmqFD8H8|Ak|-48ux{L{Es4c1TO(Z=6Qy~+wZ>mjbDFxwdluE_)T3tM53cd~ox9}#
zE8J+W6o!2Akpo)6mob!NAhd_yH|w?~@fZ`H@O2kPyZ$t_@Cnc*b1yM>>vA2aJfs{x
zbz;QtEAbL}>6COZ_d&ra_sXMual+4f1zM0|NNUpLR-L)@_^c?@R`x!6=z)*-6!bgx
zqJZc;F^F;{H8`NECf7%NGqV4(fr?G?&zH#hVK^ck{$7q%$yjK6ejcYdtgDlFzmCBz
zrgaBT_|G#5mwm;@wC2U9doX-+>}y)n5nP_<4O`%WpE16r6KghEm(}%@x($Wt7or^4t5$o8o126
zZ5E8h%Nk_~%}TljWbzmKO1q(`fqc%`CnUV$d!<}~vWiqJHWd}!G4U<{m2?~OJrjB8
zjZtja8=lp8hA+zjl4irPF3^>C9ON?C`qGyje_gVR|$r>Ddr{Z4cPwwO@ZJEfs9=
zxz_)sOxe^lY*p$HU9=6mXTpaCOZ+b1o*+-`R(ts}^H}tz?NK84x^>DV*CD%3ACg8-
zZ?)PdB$y4K(f>_=7Bt9o2^UcdOB=E39rw8JkqZ8$m7|H#ldu5m17{d`ViAS&Y==+HKg503x3MsB3R5Zd%*N^wid}sDzL_>#zYMJ04*{c7VYItG(
zKF{~@H8>c|>_z$|Lc2(Dlp~yEg6EP9&aA&!d$_fYAf`o&0c|iroU)<0-%c9|oHbL0
z92i-o-QV|9UE<-G)AdY~9EmHn=5hIBI#*BdfT7|#sjM3@I!VK@v=d3x$0$j#|GnWd
z&C{-33@e)PQmhd_19_@O@p?lhY05SY*=`eiw_r_kykgaXy~oAzDNxbYR7br)0~yCl
zSsNP#aI&0?dj4FTCM3)#q^&fQVq|v&_OrJF^E?AYIQxL_wf!B{4z0&~HHy%xgG&kf
zUgyuIZnesvJyS}?ESC5Qzdo#(_wO>Zzcl*)`NRGq-o#IsKk*wXIY&AUgC)Vl;Z
z69oQUqaY`xqLhdSj_eGVlTfGcRF(wWuAY$?Rj=>;44Ul33s(1)7%4x24mb?eTU5
z+*m_Oqa&rTe!9`C+mywO{J!$A!@0dkMxZuZig#*{+bCAJgTPO^9I86^HtG_j%}72u
z_${gomw(%43-0nDUc;?9xR0rt`&c#3!0KU9%B%a1VMt+;mo_Dt^@dZJmxdzSu%19G
z%-RX3_BUR?!nSgEL!E6CGB55Tf6h71c>1W&ik2ZIk-U;b@s_oIP;uR3D(-x_t-zbF
zKTutt13?4Z1^@apV}`W{RIh92=bSOgbOhOf{*832es`dbVHzqLxnbU~$i3nD%d4`x
zDp9fAz0Adj1xMkpuW3ho9aRf*BlA_lxIJF~@f7Hv$GZQUzk|1sAa&^`()@Tx3s596
z)NsZ|ZD)Aiaoz@5`?ZiQaR&;=Bu%Y+49ptdB^veb@7&U-lYh3N`Y=%Uas8no;6$~N
znakQ-?@1#lKt5CRhvDmt-Ntv
zMNtO(E9@w6Tmd*e#8%uPRSu#wKRY;B58-B8Uy=~O-7fCw?3<7rb>rjy8SY-R#2|WfXRgvPQQ|v>(+0aL8iJg+&T&}=P
z=YM(mfzJC1N}MUDfFFhn{Socg>i(9H6w|=61PO^g3hOk(j0u1Sk
zWqWROVZNz9SB*#!#M8CKup!N>QpNNvsX4NC6#GE72g?iyXE80Kp>fR{|#4s4c|m4Be5oLkvy!_0nRpr{w+1*a&1g_B@!~j
z!#<^UP47-V4V8zu=i5w4#HmT&EMWAs;&=51pvuR*zhHZg)Tmzt?LrJ&0>KpqWhg&r
z%Y`Rd6?qY4xd%~@8ueqoXB@$k6n@ke!Z5<#pHhP7L5U~J2bX|KgOVttxP{Qt%d|*H
zdG~obbdRx~v`YXCOp?NJAe3wYgO`6t$qgLXB;@!ix=||-~N*G$V5wXrL`x#
zYB>DMyhC8HMcg-0gBd&MmTJ~Pe^Nhp+b6uvu*O5Vg%rJ4vSu*uJdz5SAq=m;`Q2;#
z2^XL>R?~0*oZ>>CP8`+U$oN?2agDk(I&*lCzNYyqnnD{Veq9}D+u`A#YJbLtDci3RyIB#UKJL1K#Y$%czdQiBl&O!h*7x>6@ts{Vx>YneZK=!{(SKN-828U0`b4|PQqV9
z2Kh_ENoH2%3|kBUI+oUgu`@@Y)V1^Yw-aJe-xNs%YdX^843DcMZNaV_8}y&tOr8tl-%eJdvHKv48A4IkKsHy6AWq;unGhk~&0ylmgpa_kSF);QY)!
z!$>~&GNB_=6+$sbri^4W^4^%fMn8d;I)DYESCZhEEJ5gqNb0I(^FA
z9_nC`5{hbVRPXg~5Su)0eZcj_pwXcm>!(iV=K#lQ2yEgH=1C8>I*q?qQrhr#zEkK~
z&d!H%FxY;}rXC3%E)|$8!bgLV?_1Yz$#(ABo(r{pm5e%SV1x!6?US#Jf}9$a%fKnr
zMbB;NICLb0sodtayFqCB$?0oxt{+6^c~+wSd{X=+tLD$A&on|FFX@etGm*ef((aT`
zcfxP`J1rDpRF0^z+^YTTSB?w~UU-2%;8kp;eJf^BbG^9w`n@Nzu#Vrr4ghx(Zq4>z
zGmD8Qcyg|P+5dR~xOHwSw;X;$Kc3BWi^sgo-!QRkrFngrthsy~^KI_whJ%8(aPkj&
z`hOf~k%qv}7O?@)#(Z%CHO!PG&l#wWCX(v5r+l9U&=YDYYnQ<99k_oh~
zXCQo3Y^eqf?1#*L1ke)PCNP_0Z-FYQggCNIx-!<&IU0T9joSMF>kSKToo%v~Dv|FV
z<%~_Zm@aR0)N&KPn+sg3xeXNxH%>53Vsfy_ruFfs`#|gW^XhOCf#h;n{;DnRwR$J2$jOpeZQxhv
zt@+@C(~he0BL^byiuN^*N{eIz(Gvk?4h{c;;Z9E_Hp=+kn)uQZJl!2BeJay&@aw}3
zuAkECz56Z=RfNPVm~HXwk~VR<*cSy0ih_moG?$KMO*wSdwZ+g#;kueuC&h#G@w-W=
z`7A;2X%}(f3_N7!q0tM^v=TKg{bp{9OBb{hK8&cGEL&oWqgu20*_O1PI5%Tv$s>Ac
ztchYxqFp~2cZs~d_84npLE37B{&;?`HKxr+a$NsB;gX~45sj*mRn0*y(15l5QyRtl
z4zJF>0NF5rP1p#KLLq`_lprIK))S*-88E4^uJRT~B?*4EQonLbJ78(cr1$ET1LIb)
z8VhMt3(~0~DXbS(hL86OFu}d!2LUDmfEO+!B3fM-aJKjit$k*}V(PtnWI>EHbhc|
zZeuRB!SG!FgaYx;Q7r|bEsX%Pt64_
zOfxw>ZQVDl2GMrE!puf0sxJcZB+IJdVc<*c?0iJDIJan@i!+&W?5+#Nr72!w?-7v`
zFOG`rd)z5;`q>k&XR(hC3;iRZ*#AyQ`_tj{j}E-Qh+*?rL_HAJdDuq@&5HmGQ$aLj
zo#n)tNOaxUHp0HRb_ANEOGah=oavut(V7?or*%7jFk5+hb%K4i@6vvr=Q^}gRzk2}
zVF%aq$#3f1O*v~?2#PpYC}T~My|r$DRKY$Fz|1-dMNQ3FDt*ydG*QGUM9D*BmRhu6WD7z@8*YeUmBj!968V`pN&{>1qmjubj_AKhA2bKJJ1p#E0RwsS)FFl
zG``2h+wUs{B@dO`0P;udrLdO|jFhQ`o^{OB1i$2;9+ojmZWT>jI$)1y91AFT
zNA!~}C&CE6SQnNACyVX5b_5%)Z8F?LPwbHKGZDvW+`jmdGFxjCx!v_B9TWeR)e`4F
zeiJaxAgy-4uvoz+B-oYiU^1Z|!^@n(f$D8NukL^c_^)8s+lW1j4npfE@DU8U!y~J{*rXri)I1t
zpUW@}db)Z|)DCMH9qv=zQNe7C^Oe7Bx!3eq
z0B5tIZ+_AlpzCp}GEhDB{vwS1n@!Hwo(O_?WmW`A!bp;Nz*K8wLTp4cKoI@lt-IX-
zBA}%5$%&~4F%JD&+Ww>I&pQ3zz4WlRh0m?EG^+O1d($#_+b0z2tT+N~WRvt#ua&rj
z^WNm*Ck|Ejwg|reD3km)f!%jpQJ-fp3O4aCyRU$8FI*S2;P>eE$Kj7M=tY3f_W@P6E%kc?mQU$ZN9!|Qe4Ld%H!Lkr_~v3@|A
zNArr}@i5(WeZb~@+)ZrVHN|qK%u`^>l#i=9={)rOIpf?fQ=;)0;dY?YM7|waaSC@d
zv|w~B-_pUd{H|m+yl+lUSV8L@<u;IMa5ZTwH6xx1}Rn
zoMf_UIkM*@oJY7f8=soXteEGS+!X#U~lPhWsGQ2z7Q43QbS*jpK
zVW~iB`If#n^lF$nmW}CCiZ7mYDHknc9jNE(t4x&3>l4g{I+<2yA$LC3m)6kSuEM69
z2L)EpAi9AJJ|YN2w=Bjf(mX;6Ye!~@6^ZH+IkKdQwzdgPGIOF`!K|Of?
zt280_&jfS>#)&a9@4j{(N^DJQ%mZ?TTY!MpMd*9+Cj(X-At2Y+K(#yaEn9%l3P2>(Cs|+bCQ>5S)tRS25~x22`~T>59&QDK
zal|H8(HJTK+aa10gWt}!VUpqjjA;er%OaJONipnXXQRq64n+qGW5SH7)-im|buM!!
zQ*<$>Xm;fED4@Am7;_fd3eXrnp_W}qTX?_G|1h!u@~6vy)*4Yu^1Zfp1RRoQwYef*
zX?N=xsQFMvXUn7@{q_V(-zJr=9lrw=N7(x9;Hi(4Pyx0|rZmH(blZES28Nue`=s0}
zDxwP%Q9R&KX$EaJAuzp{qjxSm1h<|SngLhG$KDTlGn8q8(Rd-RtSu(0*i=&nCIW~~
zvz>>t+B4M$6XWVFL-M>4oUDI3
zW9L}e9vDFhQB}=WhyfROl2bsctT$w&w&SIMl7bxSJFCy@SJ(y(k97L6RsV)vu<>FzWQ^@^5SQp!SZ%Dt$$;0d5
z$B<%;QrM|h#AdcQ!xRa_NiqrXY(&W?MR{gvJg_B-9(KKff--;oXEf)iQ1^U7vNt#|ECYU?`y2bkhU-L3pJ70s8De=$cJf}J33OVW_k&rGfnG9U*Z1g$`IEcevG)or9}V&h$QvJbM7eZ(hq&J`&X~?^
zLyNW-4^
z3f-!8G>->gGjH`-hTusO|&u1~W9OUBA~jUPtz
zDEw$3^dZWsI|>uSQ1alp@pbL_bQ(ptgzcEn>}HWR`C2PHtq`&NVxyIrd8*Q5<5`p3
z+)+QnBVf~9A&*feC@vFDJ(5GYV_VOY$C{P8_`#hhdTt|q{L2XZv-Dsw|3K|2J1XE?@17LH`BQcTUCHMHtQ8
z+w}fLvNw8hd(zHmbK=m?yr#dO1}3VUauPKM^}>cNKG(wAfvhAg2vU)eFUHB%LD|?7
ztE;Xz=ne^D(vEW6Ej`hAxfpxqNF3cN_4dS)ZU0x9uNj&j@3^|39zX|(+xdK
z#TX-(LiXu9tGykb3|9P2MO_#di6b!eS(Tgy?m_aL2@*iCm&kRjTTITXx9rY_`3Vgu
zZ;Im=lKwESf-w?lg!GguBy7y!8xa>(ZfV>$fc~1XUusP+^(n<=k9js?0JWa2h^%rd
z310Vm*`aH`*y@uUqKWiGaV5ksIC61nT>;be`CXUuPsFg7TfQ49Fld-cRQZyiR^JpXvh6#`8((nQ
z2-<1p(i9?|;009ix8Y5&EJ6i#WXhp!Ndb43c{bc4WnU?@)<({{t$Q3j&S>c;FP%x5
zc(*tIF1cM~U#EmuY__5`_zGTn#m}l9NJWw}v&ky5k*gI3hHmFG_9)oTlF9F8&cxg7
zPe1-mINi$7%4tbVvL=N*Ocvbf^(bx&uSuB6OAer-Tqvbzv&NZlwlb0CyGYHkv
z7JHw_3mvex&Xb;m*UQjk@PT~KFK5F?r_Y(4GZT8Y;aNV7cBUC;CDD-aOjm522+-!QU=j=45%E{J=bC&!
zmuRrfYAF8YbNU6ck(C#+5x<;WUww*mYr5>88X!?-PBTIbO};r$QEYvMZSDDgn0xnd
zDBHGed?ZxTgiuz~LbSkCNTHcZCAV9YBE(dZ#iXeaWtbu);f~_QZIyKvV@*~QV^K-g
zs}ZwsCt-3;F|N$a)pzQCp67kvXM5i7-L~KN{@(BVBW)J5x~}s)kNwz>{n!sl3s2mJ
z0kdIW!4b?@yld&RIc){{F3;QXHWNM;hcQFAl)UrPjKJuE94FJjoax)QYs1n4u5la#
zI#h|5wmvfyb(7QlXv<$ztTGJ{LQgyjQG{b#^n;Xp=ZZAY+2r$ZT;>?5
zIz_|DrU@re4}wD&W48{m1z9&(0j-Nf)`D_=FaU4#qd{#rUD3n(z~VqECw$g7uicMj
z(D;&>N2HZAV|;gyj;%4K988)NAPVhKj!sa+Xue>7B)f>j9*mP~OFdH}#g|_`e8j#7
z2m--5bA`f6r9qY{x(gs@kGZ=RBm2Bma5VwaVt`N1`ZV1
zBjahRy81K;f6_z@*9CBK2sCX}!T$}WbB0whg!)tgDx94t;dKM)o5bXB-DPwF9-
z)92H%gFG`Ma6Gy8p_nKT=x_kujCqV4LRvwD7H$aP%wxobde}HW>?^Baqp;8kY^2>y
zjQ*h*;MmedDiZ2LhgxoF$o($d?ZUfAus;P=WwQnI+V?OYtY+=N8Sz0B0j^r3th&4?
zmgdG3C+oydx9vu+_a9f;Y48K}NPTaVMEObbC7xc(KF=WiA+O2WDvSAEUEgOAl6Jed
zDkk%DsY2*s9OvH_&VSs?|0Cat|9|g-+a(I?K*(GQq>e!h4@(VSqkVc0g1#6?)hB#V
zf&V?f#IU(wQQ@q?2wWPx!!vJ9f#4Q0_~=DCDxFN`!6>m;s2eEOI>7%L9LCHwWDSo{
zTs_jJZqvS^L7_3hpYn-;U2;3DjJX89O*1A4rNI7)>K5axV84H>1d?-q3Ot7TKl$zX
zV<-E!?s|@0lb3N8eK-^4JB!zK7wiAGNd9S&3)m$IE3kJ1k*58AUIH7WpDEp_0*5h1
zxu=B(!|meQ@QTz-|N4&GrSLgcGG#rCSP-B0v?}HrhI8lr$Imn7PFIGL`^AJuC{3Pt
z)(k!jI1oF0n|n5lrplJ;8%ZuP-Y1%W9HU?NUVZW6VGNsWyC6CTWSY;
z=)UhUs5QC5xL$x&6#fc^xnI&duJAr$Qu-kah15_kGhqWaWVM+WHJPt
z~N&w2QhId6em_ED0$*-u+cv;nqj
z4pM-y;T37C;B9ng4CEK8uX3!UTez3)q;d*c46h(={OVHH>*J)!=(FrA+NSZes=O*}
z!-w1HUGK!Y|A#aWtH1ManR@Sn));cg2!pz$2vJ7hb&pd737o1!zKV84Kv9f3~mC0Sk
zt(a9;t9!j#mPbQ08O5Yw!*ZQkl$3w{jp-j4tFe>law+qBOyg%T`6c0Bf9@4}yLRi9
zoU^u1e7NR?q{ZF?%Zh*l;&G3yrJ4Z`&dQ*Hz|aIH7#m$LVQw&S@tQmid`A|8b#;p8
zXB?lt{#u!)5T_e?S@D?r^-CpQF6YXh-TvTV0bEn}3?Xa6dFA$S1FK8klQt5h3=^{8
zMfL#i5XzKPQ
zs&Ko8x-74Nj_JaNEm%}h(4O8UjQt))+!lt*UZzGG^u$s8p%=~?-879F={7N@!c^Px
zZWHWt&+)B82CGeyWiY0F#S2cSzS;;C2lwx_^wtx5BinX6Py2@CS@8vNAP|?U<4_(q
zwigNA1~Xunbn}nz$cJ*1ok;CUH&hK1unF2pO5yKHORmIEPS`e9|E6!4q@fF5a3n1l
zUruTQ>hhUiQ|auq(C2+55-Uu`t;O$K#|!@i$MYL&WlU{fevd~RE@oQwaY}n9k{3&c
z+l1Xxb$`FJQfxP&5-3@1XHj4c+AQ5*F@Ug*H;ZR
z>cXR^)7T^+Oox*n=pyk(yxsGE5LadDq-gQ3-+Pk`W%-N}JjFM~t7&-N9As>y=R
zeq`LZKt-TZ=NCIZ{r>Aui;au1C*8t;$^XbE`+ImG(8-`dH^PPTHpuE8Q6-zCE+oWE
z7`Dr3y|2cL;ZRkH05GYZ_q_St^IAQz&@6w%UxocHo_nZ%s7iew??fWU<>K6(OxW9g
zhu5$;d~zAlQJRJ*(CL`bjl{-PuuPsk(t?-p)vql@+F;Xy3)7TMl_|O(71jo6z@P89
z=FB9yzAdY3!Zvrxv;TOr_Urj+C5H;)rvp-K+H9*}BQipOtO<{l8s$VuLDJ;Yq6`yC
zfhTAIYjv1>=H?ri{n@T|VDdXSks~m&!Xr1`*n~ArlzfOOrBYK@N06)FGe5rl`k^1uX{%B6h<
zZOO&%Y3qDsWLT+tz0-x(4WZA5#RWE^-$C^PI}*v?3kP^XRK7i|27P0N-)A{eDn6%5
zc3&)M9J;Qfcs9g_=lAdnZiquso^g-s*fb<`Dk3KJKm4dcbKP=Qd}{jNQ9%EK$@)(d
zqyIKACI0_J>#Fy-F3&C8M1pMvhP$>YH{^y3x3jv?L}zW@sfM6;@yc4^CdN4*W|YUN
zcc)^F96V}WQ#wC(Y&F*2bMWlt6~MOpqrijGG|4QrYo>5XYmqj*RO8m5fySL7??IY4
z6e-cwgbfKc{hi&feX1eHldz%wX#Cfm@qxPEUg4ypzhZQB>W{2`_OTj;n9;nj@Ig~#
zO{c(}LUd0G=StiZn2-(og;Ozf!pL35BHJK*cydfNJ}D-eyKu;kGg(RU^@vf=CDSC|J%LqoMG-0{qOXD3hPP|>@^gds2hcx-%p{KD(L3u8`Wr@mTw
zd*9TnFYnTi(Js?7-=?H}enrtgLYrhk&^rRulLno)3Q^zMUopo;uL*jWissF6RX7T<
z+M`8a_Cm!BNrH^09K3(>%Pe5y7n_zuSr-$to#Z}dIz6$_Mqy?G|2M?Uf4|a0Ob9Z)
zro#v*)iys9rTdOX>AoBFH{_V5O~kDI9hj3RO_}a4SX;1rZ5XgVIMO7w&BR(f@1Hl+n(86G
zkyFZhaEly1GXkIPyD&~5Trl-;^B~E6i4RCl4v${7CF+RB_Gdk^C(hrKK?U7dw)hGD
zgDeYs@HN7+naph2t{JNIz%eH;JlD
zukCeK*INvq`FXyt-tT?CaeR8?)n85A&x-TX*h)eof=m=zo(6pcX1%Q1O*l6{lbd-0C
z(*AOjMa`W$`ZAIo_PkTnKc|w^vv01Kf_sp0e6>_N7Tys94BAxqIihrfE-rQ>Joy9l
zx@TT`=XE@LBkaqHGO{0PrmZ6@xZe2UGbar@zr7tcW=`yMJdp`-@-U
zOu)LupGUTU;T<8Na@R3pBY1jh1OsM9XD=8*Nc-R)NOYDbpT<*XZ3R}I8
zWPn$2KK8)lu40Cs2FM&b|7z%=j1;i7_*$T$CxakQ1#Yvdqu&j036)_tKdQet>r~?H
z#;Y@y#MafKCp3N=
zYX0s2?WnkXOyK`_eZOmx!ZI#p4Uc;!Wpi_qb36vinV!ng8QwA}QBltdEe!@fejKB>
zle~ytYfSn+SZUl`ZeTZh9uJ()CinnRh5UhMJ;Ri`4}d|?LYD-7E}Wn9oj(J8@gZjQx@~-b@5NR98
zBtVHsGNy;(d8@Pfd^Ro=%vey@drt1RjWp}#F36m@^}59V-Lg~e`&_O#FzCBaY1-bn
z-qRs95@J{}r1^=oGPhu+Eo=id57ATC*3`vp=~-Yt#%aRD!esp?4tTEG?&jJ~5Jt2I
z3D+upK=Vf@O^(vUqsefcFR?MO7B*_(^}q*5S_IxBP^y`_YX!L~Nk@-Gdu%J^+T>$i
zyh1fJ)>_r4j^BQa=hqSw0o1b(eOGhJE6YV0h-z1^yUp0!
zx8b-0uxkPN6m&HzH(z_=951Mn9dItx?}8}lXepSPY!1zFfZ{fCe0?u&Gg*tb7>sE7
zqg&Q5x2;m?%nehidQfU5seNvqD(in+aJtuE)yqu*7BA1Lua;VI&)D-{?*(99#e{c)
z+n!babF_zBr@-L{YFfw>p~!lGI_d#>uh+YO{edb8OhDp}A6EYRLHch*4rfuQs>ho_
zHccR_m;xXFs`16yBw7@1gVrmqqJCV*%laC4fpbWntym(;$nk(MA3Otttd4DC3cxWUKB^wfnuvN1Qg9?1VB;C2H*LQq1K!
zwt2$=Y;MXxjlJ6ZBu~Y&Ok-apQ6H!^jkaych3Q_#aFfK-{m^Eqck?J~sinPODaF#tK~;wa@~&$b#t)QTAAg)|4JWYi
z_Ymp&n#d~}2ra^n!%Vj|R6!j{k+y;Peq7agSGUw#y_drnKmW);dd=Z9cn{s>fN<~dgtRAP8
z#&B0dpUl!cFH8fMU7;Ja$Z6r9F_w_SB^2YE-I99tIp4Wh8;~7kUS0a~>BHZ}mo!D8
zcvd+cIz@nYyo@|4O2WH$t@Xsq+H2eaB?A8L7yxLLCf2uItqC-2!f7ii1?iSogkP(!
zt-gO1jKRCCaq`Q;0WF;s_kx~x|AiGeluZ;5!bk_-JDk3VufTwW?MJ0sWkbtG2W`k7mw6_*}Y`Q1F$xI#-jX*_Pn%cp$(fU;g6?R0Z6u)
zM~JL!(4z+_cUMf^{N$Im3VZlcsq
z(NkKbZ*E(f>~JCqV$LqGx)jJ~l-jgI_-K_84~AcJV#uD+O_YbStNm8X`)sa71=+&|
z2-;l~e2sC5l{SLs*YVb$X_n-f5F~}_+fl+oK#)=7>#uc(u|y;1{haq6RzFIE$V#vD
zj0=!gG^N202W8*Vl*t>v)!ufy2k$>HaqHlYYPr16ld54C(Kp~bAV33Gcich;FiDKS
zmt(metX0KME;ar0D(FykTwevB^xf;03dih0rM-?d@FWdT+x2CJw0HQe`8kxRQ4|fJ
zZY>3}z>X$ZmqW}ZG^6WPJbpdtK3wC$|D
z1Zie+0`FfL@A&xZR+Na8j$Q}95u8FgDdid6Qd}v)QQ1`;7E6(x!?E{QTlY5bVdz}hY@j=;F|L2NeZb|x689vDW=B8+&}o+@x9
z=6y~|P4SiBr{#MrcAI&-QZ5A$HL8ZcThl8`U0&SDShFwp8`yeoB1`o>TqGr;)gMhsw$Z09HThkq3S%FEWUHdU1z1uWQ1PtHt7@O$iVcM4Bv$G@W
zXRM?>xS}|=j!D7w@L7gL!ZSDh?zP%}OTpvQk7+a1tj*>3{0;uvSC}(M8z2@PSxW8H
zRdD0i&qc!BFW!;2PlRe8!$XlX<&Ld41NW#t$sn}m!uNIsf2FwoF1hmEM)9R4GkXQ6
zO-^d2nHg(~3-=Wk?%Q;J{Sm2^s*ibx*Zriq|8{cy{O~1BH1Yu
z)M#_*q_xw?US9iSvZ;@bK4l$DI$9ntu<56|GQRGklcZM_6>(C(eq}$eD66iiOI@`c
zgnSGI)-@9rsYE$>|B3{F9mfXIKCMpQ(}h!WwKOR-%?Q#l6~tRisOvM_ru
z3`eU4Uuw_v>`>`Khs`^B$u}z+8g^uk&p32TalC#qJyUZ+Iny>~8TCG%^&DUJC0{@k
z>OiDc>Il^qjs$r3VG=q98NoiN$2IPGL|6w0aHJmU!=xggG2#&j4f<>`Ey(t6p_xY!
zOtFR9(u(ZI-4o(EJRuaN@>6L2ZZ<_6_C5~W1jz@}{Y{&lRr`u6V%EWgW(F<=K>2m<
zMwWkE-hD{#c#nQ^fTf;AU(w~$YL(BTDipg?}cfj))H%Of~8yPvrta|*lVk-0^I!*dxX0Jf>zRZ)%XA>h6
zPCSyPD#yrp92t1bc)TMTSaAG-FbGhy3VfWlTQ#MZuGUt5)^B2AeP79CrBfEooC`yf6$R2QHfm}6E5k_%R>{^uz
zZ#Q0xZO!qZ=6|qU7xmn}B0A}ING9DS)8jV|)2g(x`dHLq6X(BqJ-h-M0jP(^l*6>aLXygSpwb
zqHK-cu8e61*C~sYWoH%y;fU8v~
zMRhLzQ284u(tfbmwXv6Mqy3`Ku$d}HV9s=sw5`}ql(uG>i&L*KeINh9Q~e{o0+bzl
z6x@6K57g86WlNXY?=&JoL`cP_qr=?AMN9f=-z7ZK_{(+uUiZ9z({KJG>Ik0!*a@I(
z(_RAtyc<6|#6pkU4?1K8Nj25lwa2Uy+QAXU9>_|9+6+z`YJX6_bD~HSE#+Yw2UDB*
zM&~*Q>o|d0_D;6K=_-Dld&w!E(M6#C4D;*)6Iv)7pbTEDnwhG
zJAUcCc5S{Bd#WHwsw)rd9T9RLT;>afTN@P>8-)zt0o@p7yzDRXLsEr
zZwD8~LX;~t>jiG;tf-XYvBN+tdxj-8>!wKD1nulU49)b
z?Z^`^gJ*1chq4|^gHdnUqQ<&SVg6)$s=xAyKD#p@h8U1W9g#Ikf=iU9qsX=oK
zCkM1Os~h`#4;g`hs48L=E~;rhH9NsfnFp
zwctGY5F|u4!;ZXNORKc0jfaGK-9;BIJv&-XjBTl?hpDUs&C|-o85?XDoeiO7?6~r4@&=O%Am(7p_NiTSj2O*sqSms
z=B~bl1}#1YAKi5rmK@le+=AO=xRek^DP_JAq#lE+A0p$mxvQ^UyLnp-@k@iO(eUPW
zU_XznreDhUr%m`ZN%E*o++BDh!9@G3j+w5Av^74j#aG6DY8fi=aIlN47rzqwMy3`d
zm?jvun$ed@cdvOt!J9vx-wQhMH?En>EdK;_n{#|BoR~#c6(u*y`Oi$4wTxXqSgcLn
z!cvo*yU?FmQso~1&2B(_rJ{p+NN!?=Q9P|^%wtJ6DfYzT5dZZwusYl(R05ych{7tu
z$W?&(FdW5f!QP;*2&2~RgW)_CPFpD_M!`Yj(WWO}xOKpO)GkcxW#oZaEnaB7{aT5p
z=~tKmrf|JDvPz8?hpZCu@Dra}(jGC@8#f6ZNRMgjggUHb9eMVb`<$W!?taQr5xNE=
z)Gw8Ix#L$zTWX>&kv8o44As^qs+B&lMo(}3+iA)vN2Jw2G^qi}5p)JK3N9Kq5u)=m
z;Dan<%%i&`y0oPp00uE8J11QHa;%oup;>T{>W9F(mQ+m4`LL6fyQym|^PBlgI|JOY
zTdVxDW3`^W!pC9Y9fm@c46wNkz|rLcYdONzyxr`s2MAWU9(w2H&54QpfhzwLfvxvt
zGgl3hw)o;V!rl(u#`iRv`yIEH~oR!e6f{R|p+3s0Uc6-l-bn43a-
zJQ|f@^E{a9Q~_Nhtg&i+Lz2HRB(!7`R<%y3%^$P?C2m_Mz{bxTB|$!IwNS#FJ7LF5HmJ9|KPw43|x`
zVk*PAGJsEx;L|}hqQ^uE_hLz_nI_e-yW?X!3seVL;5*|)!{CPB4q{4=fMjD?%}-7S4{zppF18IKZXhze<}
zZW_D`KP$>1j_-nvvCVkKMDyK44Xwi4m^Jlg6n5GpKjpx5tX^6;VZG0o
zyM>qu>_*R_)}YSZQK#{G#WEn&RNn^?9tWxU=Q=@#Etu7C!YfdyY0Shu;gF=@_M-zP
zdYqVb(}THQ?-PsNl?RIA3$msa|GaPTOq8XxS3dl)o3_}JjX;;ucN(k8kZ^J!1sWU|@7ghWqVUOM~2S@^-e@
zigt5|8d7iUb<^ALj(R9NP|3XaeMUfFzPXofW}frddog4fQ>t4aY7lG+dd-;Rf>nVp
zS9)b>7vxP7n6d3bbr;QMKO?YiZ*Bja{hjD`tKjLc&QA{iDNM)20tyY!D!h9xZB!o*LRhog`9JRb
z7Nh1rJ|1vruhrPMdD0rXw$U?ASxM~pC&&8U$NO?dQ{<+%eM1Eu6`qFscvcf9N=4N?
z!#2jJNZp=411th&o+!rUti}oNo(R7hzl4iZS*NByv-_r|;V({aJW*el{*l>>GlSLw
z1%L_;=afZRN0!fHdZ_!w`EfceDP<%11ZdA_56`qWpsN1m
z^8p-}CVzdnIoW<_?%K7+k=rwW4iC3$CsZ$P*C|X-W%p_V5VQ}_)dzu~T$BS2VABPG
z)d-qz!m}-*T>gO)pSE=viZ=0#H=>2*h%y^Dd-UlHCf?M1R^a%V@h3*wMB3;$KCB{&
zWYw1gsE#uP#p%0ON~cm+*OZ_Ta{$_YCZ^&dkV}sOg)K#Bf<{(nK+T_88K3yncEU)B
z1JXsYryuV=5P0hRO0T?sRuSG`8SkmGc%$T?4?zcbw1+;V)&7P}%!+Hk
zahmXmd_0fwSy?LF|879&1K4k=zzi>PRYS8tk1=gOol~l|gnq0bW
z*_fFv+*w`o;DWy)d+e*}{uj2))<%;ugkgjUH(4hp%(a#Thq7=tCuWnU$8*?}eiszi
zDI@#;xPqT6dY8
zY2m6qd0iN5wso(a*$J^HJ@;*G#h%??3Hm1`f8x^%eU)maC;PR1y)>7;Sq%8pbvT**
z+CM*&Usx$)Y+aV9dul%{a&sfeWM^l|{=--2h;pk${rWb=1DC?KpXWR>I2)yK8f7hkvO0`uwi2q^
zfW?WuAl%o;Yo7&hYvm-bC!AyOcq!%qxXMOz7U&G1t;TL`kSLs59~uo*X~2
zKWzf@kgshPoMS$Zm-;|yc2ygE$zG5C)>>Oz+gSUuvGHY1eM5as()5?F(;m9I#l^)M
z9>u!XuWP!+2Sj}Ii}%R(i?vrv8A*&tM}s2471HoFew(PC>|%JIa)mT9!_jIR^L#U5
zc~wAn@M;JTso!(e62fd0n)0@fN3hV6*}ab)@IV)zwS9uK+eSas_8$IX{W1yl9BB51
z2U%^rYxr{JJrm17nZ){9$S^F(Sg2LcOQ~&t*R5@cZ0{o<%yTx|=yAL_hGTh(n9^wZ
z$jQmX_KTPh1a)iJp0}Ho7E^BpQ75GC37w#Jj#Y4_R@(N2kha*Gx1er|^vK9+ZQndto@)&v$G#wMr*Un%t%f0+r+_&cI}q0F6|
z9>qd=IGY`_$x`9vC7^4~!z#A7Aqp>7@l29PkI71b9P}E`lB|+9`x6VDT2*_D3m=Lh
zQx2yJfHku%Ky{11c^aK4&mEbrwaxHETq}X(di1!T%N^2YHmkNOX(#*UVy5q*slRBO
z6=4P09(TVa!YTBy{}BI9_!$v@
zpe&g1zHs(ja~*yd%TI#yvpkgT;SLU#QGE_VM+uL1gO)?E@0%sq=uo^g`3Oq~b>UKR
z937fbH{dnqUw;|ByU1bDW?flTn)ER-QA+o}Qx1Bo?+g$mPmI_0$Ww6z$ADcqtmR*3xq`3(jwh@!
zHK2w5$&)PC3gdoJHmeCa9C+emg}>V!8u{DtT$L-&vPBa{rE#A$?;Von2fzwEC4LJ0
z5lZIYfz7kj{5V!^B#gfsdnlx0a^LpSL9*2g$Im6s(|)qY_m=edWTjf#ISpt;70nkZ
zzZIN$IqK!1XDubL13~T}?V?pM=our8m;v2!9b{ussTj1eFTFo#vp+yE9#p`#rRCW>
zXgvm%`P3sC-#YSUh6ZQUlU;NMTGUmbkEs!Cuf2UId$cbfM!%d|4*U32EPMcTqW?fq
zz>O^tJ((ZFvL^Ghuw0Vh#5hqM4ev|n9-a0A=%1eCl%+G#^|;#MP}_{-8xt+X%&e(#
z*@^)gHZ*@jTb>IQYwl`uT_PZ^T>1HF=mQvKbYow<+^Wf$6A!fqnmS5lG%Y
z{7l`T!Q6T{#GxVi^q@fl(H2FL$nMJ^Sc)8znLWp%@FU
zz+RyRIIPc$YD~}qlkCBA_S}OciKw9#FgLC}N&7}5b2WJ+aF*HuhtIgb8m