DibyashanuPati/PhysLean
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Update ToSols.lean

Browse source
This commit is contained in:
Pietro Monticone 2024-06-08 01:50:38 +02:00
parent 8190b8c044
commit 5c6a8b7a10
1 changed files with 1 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

4
HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean
View file

@ -233,7 +233,7 @@ lemma toSolNSQuad_eq_planeY₃B₃_on_α (R : MSSMACC.AnomalyFreePerp) :
ring_nf ring_nf
simp simp
/-- Given a `R ` perpendicular to $Y_3$, and $B_3$, a element of `Sols`. This map is /-- Given a `R ` perpendicular to `Y₃` and `B₃`, an element of `Sols`. This map is
not surjective. -/ not surjective. -/
def toSolNS : MSSMACC.AnomalyFreePerp × ℚ × ℚ × ℚ → MSSMACC.Sols := fun (R, a, _ , _) => def toSolNS : MSSMACC.AnomalyFreePerp × ℚ × ℚ × ℚ → MSSMACC.Sols := fun (R, a, _ , _) =>
a • AnomalyFreeMk'' (toSolNSQuad R) (toSolNSQuad_cube R) a • AnomalyFreeMk'' (toSolNSQuad R) (toSolNSQuad_cube R)
@ -332,7 +332,6 @@ def inQuadProj (T : inQuadSol) : inQuad × ℚ × ℚ × ℚ :=
- cubeTriLin T.val.val T.val.val Y₃.val - cubeTriLin T.val.val T.val.val Y₃.val
* (dot Y₃.val T.val.val - 2 * dot B₃.val T.val.val))) * (dot Y₃.val T.val.val - 2 * dot B₃.val T.val.val)))
lemma inQuadToSol_proj (T : inQuadSol) : inQuadToSol (inQuadProj T) = T.val := by lemma inQuadToSol_proj (T : inQuadSol) : inQuadToSol (inQuadProj T) = T.val := by
rw [inQuadProj, inQuadToSol_smul] rw [inQuadProj, inQuadToSol_smul]
apply ACCSystem.Sols.ext apply ACCSystem.Sols.ext
@ -371,7 +370,6 @@ lemma inQuadCubeToSol_smul (R : inQuadCube) (c₁ c₂ c₃ d : ℚ) :
rw [planeY₃B₃_smul] rw [planeY₃B₃_smul]
rfl rfl
/-- On elements of `inQuadCubeSol` a right-inverse to `inQuadCubeToSol`. -/ /-- On elements of `inQuadCubeSol` a right-inverse to `inQuadCubeToSol`. -/
def inQuadCubeProj (T : inQuadCubeSol) : inQuadCube × ℚ × ℚ × ℚ := def inQuadCubeProj (T : inQuadCubeSol) : inQuadCube × ℚ × ℚ × ℚ :=
(⟨⟨⟨proj T.val.1.1, (linEqPropSol_iff_proj_linEqProp T.val).mp T.prop.1 ⟩, (⟨⟨⟨proj T.val.1.1, (linEqPropSol_iff_proj_linEqProp T.val).mp T.prop.1 ⟩,