From 805f5611952bf88808b53939a1753a2b903381ce Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Mon, 22 Apr 2024 06:57:46 -0400 Subject: [PATCH] feat: Change file structure, added comments --- .../Basic.lean} | 0 .../PlaneWithY3B3.lean} | 2 +- .../ToSols.lean} | 246 ++++++++++-------- 3 files changed, 140 insertions(+), 108 deletions(-) rename HepLean/AnomalyCancellation/MSSMNu/{OrthogY3B3.lean => OrthogY3B3/Basic.lean} (100%) rename HepLean/AnomalyCancellation/MSSMNu/{PlaneY3B3Orthog.lean => OrthogY3B3/PlaneWithY3B3.lean} (99%) rename HepLean/AnomalyCancellation/MSSMNu/{SolsParameterization.lean => OrthogY3B3/ToSols.lean} (55%) diff --git a/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3.lean b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/Basic.lean similarity index 100% rename from HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3.lean rename to HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/Basic.lean diff --git a/HepLean/AnomalyCancellation/MSSMNu/PlaneY3B3Orthog.lean b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/PlaneWithY3B3.lean similarity index 99% rename from HepLean/AnomalyCancellation/MSSMNu/PlaneY3B3Orthog.lean rename to HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/PlaneWithY3B3.lean index 89aed31..22eedbd 100644 --- a/HepLean/AnomalyCancellation/MSSMNu/PlaneY3B3Orthog.lean +++ b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/PlaneWithY3B3.lean @@ -5,7 +5,7 @@ Authors: Joseph Tooby-Smith -/ import HepLean.AnomalyCancellation.MSSMNu.Basic import HepLean.AnomalyCancellation.MSSMNu.LineY3B3 -import HepLean.AnomalyCancellation.MSSMNu.OrthogY3B3 +import HepLean.AnomalyCancellation.MSSMNu.OrthogY3B3.Basic import Mathlib.Tactic.Polyrith /-! # Plane Y₃ B₃ and an orthogonal third point diff --git a/HepLean/AnomalyCancellation/MSSMNu/SolsParameterization.lean b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean similarity index 55% rename from HepLean/AnomalyCancellation/MSSMNu/SolsParameterization.lean rename to HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean index 52c0985..049c17b 100644 --- a/HepLean/AnomalyCancellation/MSSMNu/SolsParameterization.lean +++ b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean @@ -5,19 +5,19 @@ Authors: Joseph Tooby-Smith -/ import HepLean.AnomalyCancellation.MSSMNu.Basic import HepLean.AnomalyCancellation.MSSMNu.LineY3B3 -import HepLean.AnomalyCancellation.MSSMNu.PlaneY3B3Orthog +import HepLean.AnomalyCancellation.MSSMNu.OrthogY3B3.PlaneWithY3B3 import Mathlib.Tactic.Polyrith /-! -# Parameterization of solutions to the MSSM anomaly cancellation equations +# From charges perpendicular to `Y₃` and `B₃` to solutions -This file uses planes through $Y_3$ and $B_3$ to form solutions to the anomaly cancellation -conditions. +The main aim of this file is to take charge assignments perpendicular to `Y₃` and `B₃` and +produce solutions to the anomaly cancellation conditions. In this regard we will define +a surjective map `toSol` from `MSSMACC.AnomalyFreePerp × ℚ × ℚ × ℚ` to `MSSMACC.Sols`. + +To define `toSols` we define a series of other maps from various subtypes of +`MSSMACC.AnomalyFreePerp × ℚ × ℚ × ℚ` to `MSSMACC.Sols`. And show that these maps form a +surjection on certain subtypes of `MSSMACC.Sols`. -Split into four cases: -- The generic case. -- `case₁`: The case when the quadratic and cubic lines agree (if they exist uniquely). -- `case₂`: The case where the plane lies entirely within the quadratic. -- `case₃`: The case where the plane lies entirely within the cubic and quadratic. # References @@ -36,18 +36,21 @@ open BigOperators namespace AnomalyFreePerp -def lineEqProp (R : MSSMACC.AnomalyFreePerp) : Prop := - α₁ R = 0 ∧ α₂ R = 0 ∧ α₃ R = 0 - +/-- A condition for the quad line in the plane spanned by R, Y₃ and B₃ to sit in the cubic, +and for the cube line to sit in the quad. -/ +def lineEqProp (R : MSSMACC.AnomalyFreePerp) : Prop := α₁ R = 0 ∧ α₂ R = 0 ∧ α₃ R = 0 instance (R : MSSMACC.AnomalyFreePerp) : Decidable (lineEqProp R) := by apply And.decidable - +/-- A condition on `Sols` which we will show in `linEqPropSol_iff_proj_linEqProp` that is equivalent + to the condition that the `proj` of the solution satisfies `lineEqProp`. -/ def lineEqPropSol (R : MSSMACC.Sols) : Prop := cubeTriLin (R.val, R.val, Y₃.val) * quadBiLin (B₃.val, R.val) - cubeTriLin (R.val, R.val, B₃.val) * quadBiLin (Y₃.val, R.val) = 0 +/-- A rational which appears in `toSolNS` acting on sols, and which been zero is +equivalent to satisfying `lineEqPropSol`. -/ def lineEqCoeff (T : MSSMACC.Sols) : ℚ := dot (Y₃.val, B₃.val) * α₃ (proj T.1.1) lemma lineEqPropSol_iff_lineEqCoeff_zero (T : MSSMACC.Sols) : @@ -58,12 +61,8 @@ lemma lineEqPropSol_iff_lineEqCoeff_zero (T : MSSMACC.Sols) : rw [cube_proj_proj_B₃, cube_proj_proj_Y₃, quad_B₃_proj, quad_Y₃_proj] rw [show dot (Y₃.val, B₃.val) = 108 by rfl] simp only [Fin.isValue, Fin.reduceFinMk, OfNat.ofNat_ne_zero, false_or] - have h1 : 108 ^ 2 * cubeTriLin (T.val, T.val, Y₃.val) * (108 * quadBiLin (B₃.val, T.val)) - - 108 ^ 2 * cubeTriLin (T.val, T.val, B₃.val) * (108 * quadBiLin (Y₃.val, T.val)) = - 108 ^ 3 * (cubeTriLin (T.val, T.val, Y₃.val) * quadBiLin (B₃.val, T.val) - - cubeTriLin (T.val, T.val, B₃.val) * quadBiLin (Y₃.val, T.val) ) := by - ring - rw [h1] + ring_nf + rw [mul_comm _ 1259712, mul_comm _ 1259712, ← mul_sub] simp lemma linEqPropSol_iff_proj_linEqProp (R : MSSMACC.Sols) : @@ -80,17 +79,21 @@ lemma linEqPropSol_iff_proj_linEqProp (R : MSSMACC.Sols) : simp -/-- Case₂ is defined when the plane lies entirely within the quadratic. -/ +/-- A condition which is satisfied if the plane spanned by `R`, `Y₃` and `B₃` lies +entirely in the quadratic surface. -/ def inQuadProp (R : MSSMACC.AnomalyFreePerp) : Prop := quadBiLin (R.val, R.val) = 0 ∧ quadBiLin (Y₃.val, R.val) = 0 ∧ quadBiLin (B₃.val, R.val) = 0 instance (R : MSSMACC.AnomalyFreePerp) : Decidable (inQuadProp R) := by apply And.decidable +/-- A condition which is satisfied if the plane spanned by the solutions `R`, `Y₃` and `B₃` +lies entirely in the quadratic surface. -/ def inQuadSolProp (R : MSSMACC.Sols) : Prop := quadBiLin (Y₃.val, R.val) = 0 ∧ quadBiLin (B₃.val, R.val) = 0 -/-- The coefficent which multiplies a solution on passing through `case₁`. -/ +/-- A rational which has two properties. It is zero for a solution `T` if and only if +that solution satisfies `inQuadSolProp`. It appears in the definition of `inQuadProj`. -/ def quadCoeff (T : MSSMACC.Sols) : ℚ := 2 * dot (Y₃.val, B₃.val) ^ 2 * (quadBiLin (Y₃.val, T.val) ^ 2 + quadBiLin (B₃.val, T.val) ^ 2) @@ -110,6 +113,8 @@ lemma inQuadSolProp_iff_quadCoeff_zero (T : MSSMACC.Sols) : inQuadSolProp T ↔ not_false_eq_true, pow_eq_zero_iff] at h exact h +/-- The conditions `inQuadSolProp R` and `inQuadProp (proj R.1.1)` are equivalent. This is to be +expected since both `R` and `proj R.1.1` define the same plane with `Y₃` and `B₃`. -/ lemma inQuadSolProp_iff_proj_inQuadProp (R : MSSMACC.Sols) : inQuadSolProp R ↔ inQuadProp (proj R.1.1) := by rw [inQuadSolProp, inQuadProp] @@ -125,7 +130,8 @@ lemma inQuadSolProp_iff_proj_inQuadProp (R : MSSMACC.Sols) : rw [h.2.1, h.2.2] simp -/-- Case₃ is defined when the plane lies entirely within the quadratic and cubic. -/ +/-- A condition which is satisfied if the plane spanned by `R`, `Y₃` and `B₃` lies +entirely in the cubic surface. -/ def inCubeProp (R : MSSMACC.AnomalyFreePerp) : Prop := cubeTriLin (R.val, R.val, R.val) = 0 ∧ cubeTriLin (R.val, R.val, B₃.val) = 0 ∧ cubeTriLin (R.val, R.val, Y₃.val) = 0 @@ -134,9 +140,13 @@ def inCubeProp (R : MSSMACC.AnomalyFreePerp) : Prop := instance (R : MSSMACC.AnomalyFreePerp) : Decidable (inCubeProp R) := by apply And.decidable +/-- A condition which is satisfied if the plane spanned by the solutions `R`, `Y₃` and `B₃` +lies entirely in the cubic surface. -/ def inCubeSolProp (R : MSSMACC.Sols) : Prop := cubeTriLin (R.val, R.val, B₃.val) = 0 ∧ cubeTriLin (R.val, R.val, Y₃.val) = 0 +/-- A rational which has two properties. It is zero for a solution `T` if and only if +that solution satisfies `inCubeSolProp`. It appears in the definition of `inLineEqProj`. -/ def cubicCoeff (T : MSSMACC.Sols) : ℚ := 3 * dot (Y₃.val, B₃.val) ^ 3 * (cubeTriLin (T.val, T.val, Y₃.val) ^ 2 + cubeTriLin (T.val, T.val, B₃.val) ^ 2 ) @@ -172,8 +182,34 @@ lemma inCubeSolProp_iff_proj_inCubeProp (R : MSSMACC.Sols) : rw [h.2.1, h.2.2] simp +/-- Those charge assignments perpendicular to `Y₃` and `B₃` which satisfy the condition +`lineEqProp`. -/ +def inLineEq : Type := {R : MSSMACC.AnomalyFreePerp // lineEqProp R} -/-- Given a `R ∈ LinSols` perpendicular to $Y_3$, and $B_3$, a solution to the quadratic. -/ +/-- Those charge assignments perpendicular to `Y₃` and `B₃` which satisfy the condition +`lineEqProp` and `inQuadProp`. -/ +def inQuad : Type := {R : inLineEq // inQuadProp R.val} + +/-- Those charge assignments perpendicular to `Y₃` and `B₃` which satisfy the condition +`lineEqProp`, `inQuadProp` and `inCubeProp`. -/ +def inQuadCube : Type := {R : inQuad // inCubeProp R.val.val} + +/-- Those solutions which do not satisfy the condition `lineEqPropSol`. -/ +def notInLineEqSol : Type := {R : MSSMACC.Sols // ¬ lineEqPropSol R} + +/-- Those solutions which satisfy the condition `lineEqPropSol` by not `inQuadSolProp`. -/ +def inLineEqSol : Type := {R : MSSMACC.Sols // lineEqPropSol R ∧ ¬ inQuadSolProp R} + +/-- Those solutions which satisfy the condition `lineEqPropSol` and `inQuadSolProp` but +not `inCubeSolProp`. -/ +def inQuadSol : Type := {R : MSSMACC.Sols // lineEqPropSol R ∧ inQuadSolProp R ∧ ¬ inCubeSolProp R} + +/-- Those solutions which satisfy the condition all the conditions `lineEqPropSol`, `inQuadSolProp` +and `inCubeSolProp`. -/ +def inQuadCubeSol : Type := + {R : MSSMACC.Sols // lineEqPropSol R ∧ inQuadSolProp R ∧ inCubeSolProp R} + +/-- Given a `R` perpendicular to `Y₃` and `B₃` a quadratic solution. -/ def toSolNSQuad (R : MSSMACC.AnomalyFreePerp) : MSSMACC.QuadSols := lineQuad R (3 * cubeTriLin (R.val, R.val, Y₃.val)) @@ -195,43 +231,36 @@ lemma toSolNSQuad_eq_planeY₃B₃_on_α (R : MSSMACC.AnomalyFreePerp) : ring_nf simp -/-- Given a `R ∈ LinSols` perpendicular to $Y_3$, and $B_3$, a element of `Sols`. -/ -def toSolNS : MSSMACC.AnomalyFreePerp × ℚ × ℚ × ℚ → MSSMACC.Sols := fun (R, a, _ , _) => +/-- Given a `R ` perpendicular to $Y_3$, and $B_3$, a element of `Sols`. This map is +not surjective. -/ +def toSolNS : MSSMACC.AnomalyFreePerp × ℚ × ℚ × ℚ → MSSMACC.Sols := fun (R, a, _ , _) => a • AnomalyFreeMk'' (toSolNSQuad R) (toSolNSQuad_cube R) + +/-- A map from `Sols` to `MSSMACC.AnomalyFreePerp × ℚ × ℚ × ℚ` which on elements of +`notInLineEqSol` will produce a right inverse to `toSolNS`. -/ def toSolNSProj (T : MSSMACC.Sols) : MSSMACC.AnomalyFreePerp × ℚ × ℚ × ℚ := (proj T.1.1, (lineEqCoeff T)⁻¹, 0, 0) -lemma toSolNS_proj (T : MSSMACC.Sols) (h : lineEqCoeff T ≠ 0) : - toSolNS (toSolNSProj T) = T := by +lemma toSolNS_proj (T : notInLineEqSol) : toSolNS (toSolNSProj T.val) = T.val := by apply ACCSystem.Sols.ext rw [toSolNS, toSolNSProj] - change (lineEqCoeff T)⁻¹ • (toSolNSQuad _).1.1 = _ + change (lineEqCoeff T.val)⁻¹ • (toSolNSQuad _).1.1 = _ rw [toSolNSQuad_eq_planeY₃B₃_on_α] rw [planeY₃B₃_val] rw [Y₃_plus_B₃_plus_proj] rw [α₁_proj, α₂_proj] ring_nf simp only [zero_smul, add_zero, Fin.isValue, Fin.reduceFinMk, zero_add] - have h1 : α₃ (proj T.toLinSols) * dot (Y₃.val, B₃.val) = lineEqCoeff T := by + have h1 : α₃ (proj T.val.toLinSols) * dot (Y₃.val, B₃.val) = lineEqCoeff T.val := by rw [lineEqCoeff] ring rw [h1] - rw [← MulAction.mul_smul, mul_comm, mul_inv_cancel h] + have h1 := (lineEqPropSol_iff_lineEqCoeff_zero T.val).mpr.mt T.prop + rw [← MulAction.mul_smul, mul_comm, mul_inv_cancel h1] simp -def inLineEq : Type := {R : MSSMACC.AnomalyFreePerp // lineEqProp R} - -def inLineEqSol : Type := {R : MSSMACC.Sols // lineEqPropSol R} - -def inLineEqProj (T : inLineEqSol) : inLineEq × ℚ × ℚ × ℚ := - (⟨proj T.val.1.1, (linEqPropSol_iff_proj_linEqProp T.val).mp T.prop ⟩, - (quadCoeff T.val)⁻¹ * quadBiLin (B₃.val, T.val.val), - (quadCoeff T.val)⁻¹ * (- quadBiLin (Y₃.val, T.val.val)), - (quadCoeff T.val)⁻¹ * (- quadBiLin (B₃.val, T.val.val) * ( dot (Y₃.val, T.val.val) - - dot (B₃.val, T.val.val)) - - quadBiLin (Y₃.val, T.val.val) * ( dot (Y₃.val, T.val.val) - 2 * dot (B₃.val, T.val.val)))) - +/-- Given a element of `inLineEq × ℚ × ℚ × ℚ`, a solution to the ACCs. -/ def inLineEqToSol : inLineEq × ℚ × ℚ × ℚ → MSSMACC.Sols := fun (R, c₁, c₂, c₃) => AnomalyFreeMk'' (lineQuad R.val c₁ c₂ c₃) (by @@ -239,6 +268,16 @@ def inLineEqToSol : inLineEq × ℚ × ℚ × ℚ → MSSMACC.Sols := fun (R, c rw [R.prop.1, R.prop.2.1, R.prop.2.2] simp) +/-- On elements of `inLineEqSol` a right-inverse to `inLineEqSol`. -/ +def inLineEqProj (T : inLineEqSol) : inLineEq × ℚ × ℚ × ℚ := + (⟨proj T.val.1.1, (linEqPropSol_iff_proj_linEqProp T.val).mp T.prop.1 ⟩, + (quadCoeff T.val)⁻¹ * quadBiLin (B₃.val, T.val.val), + (quadCoeff T.val)⁻¹ * (- quadBiLin (Y₃.val, T.val.val)), + (quadCoeff T.val)⁻¹ * ( + quadBiLin (B₃.val, T.val.val) * (dot (B₃.val, T.val.val) - dot (Y₃.val, T.val.val)) + - quadBiLin (Y₃.val, T.val.val) * (dot (Y₃.val, T.val.val) - 2 * dot (B₃.val, T.val.val)))) + + lemma inLineEqTo_smul (R : inLineEq) (c₁ c₂ c₃ d : ℚ) : inLineEqToSol (R, (d * c₁), (d * c₂), (d * c₃)) = d • inLineEqToSol (R, c₁, c₂, c₃) := by apply ACCSystem.Sols.ext @@ -246,8 +285,7 @@ lemma inLineEqTo_smul (R : inLineEq) (c₁ c₂ c₃ d : ℚ) : rw [lineQuad_smul] rfl -lemma inLineEqToSol_proj (T : inLineEqSol) (h : quadCoeff T.val ≠ 0) : - inLineEqToSol (inLineEqProj T) = T.val := by +lemma inLineEqToSol_proj (T : inLineEqSol) : inLineEqToSol (inLineEqProj T) = T.val := by rw [inLineEqProj, inLineEqTo_smul] apply ACCSystem.Sols.ext change _ • (lineQuad _ _ _ _).val = _ @@ -262,14 +300,11 @@ lemma inLineEqToSol_proj (T : inLineEqSol) (h : quadCoeff T.val ≠ 0) : rw [quadCoeff] ring rw [h1] - rw [← MulAction.mul_smul, mul_comm, mul_inv_cancel h] + have h2 := (inQuadSolProp_iff_quadCoeff_zero T.val).mpr.mt T.prop.2 + rw [← MulAction.mul_smul, mul_comm, mul_inv_cancel h2] simp - -def inQuad : Type := {R : inLineEq // inQuadProp R.val} - -def inQuadSol : Type := {R : inLineEqSol // inQuadSolProp R.val} - +/-- Given a element of `inQuad × ℚ × ℚ × ℚ`, a solution to the ACCs. -/ def inQuadToSol : inQuad × ℚ × ℚ × ℚ → MSSMACC.Sols := fun (R, a₁, a₂, a₃) => AnomalyFreeMk' (lineCube R.val.val a₁ a₂ a₃) (by @@ -285,19 +320,19 @@ lemma inQuadToSol_smul (R : inQuad) (c₁ c₂ c₃ d : ℚ) : rw [lineCube_smul] rfl +/-- On elements of `inQuadSol` a right-inverse to `inQuadToSol`. -/ def inQuadProj (T : inQuadSol) : inQuad × ℚ × ℚ × ℚ := - (⟨⟨proj T.val.val.1.1, (linEqPropSol_iff_proj_linEqProp T.val.val).mp T.val.prop ⟩, - (inQuadSolProp_iff_proj_inQuadProp T.val.val).mp T.prop⟩, - (cubicCoeff T.val.val)⁻¹ * (cubeTriLin (T.val.val.val, T.val.val.val, B₃.val)), - (cubicCoeff T.val.val)⁻¹ * (- cubeTriLin (T.val.val.val, T.val.val.val, Y₃.val)), - (cubicCoeff T.val.val)⁻¹ * (- cubeTriLin (T.val.val.val, T.val.val.val, B₃.val) - * (dot (Y₃.val, T.val.val.val) - dot (B₃.val, T.val.val.val)) - - cubeTriLin (T.val.val.val, T.val.val.val, Y₃.val) - * (dot (Y₃.val, T.val.val.val) - 2 * dot (B₃.val, T.val.val.val)))) + (⟨⟨proj T.val.1.1, (linEqPropSol_iff_proj_linEqProp T.val).mp T.prop.1 ⟩, + (inQuadSolProp_iff_proj_inQuadProp T.val).mp T.prop.2.1⟩, + (cubicCoeff T.val)⁻¹ * (cubeTriLin (T.val.val, T.val.val, B₃.val)), + (cubicCoeff T.val)⁻¹ * (- cubeTriLin (T.val.val, T.val.val, Y₃.val)), + (cubicCoeff T.val)⁻¹ * + (cubeTriLin (T.val.val, T.val.val, B₃.val) * (dot (B₃.val, T.val.val) - dot (Y₃.val, T.val.val)) + - cubeTriLin (T.val.val, T.val.val, Y₃.val) + * (dot (Y₃.val, T.val.val) - 2 * dot (B₃.val, T.val.val)))) -lemma inQuadToSol_proj (T : inQuadSol) (h : cubicCoeff T.val.val ≠ 0) : - inQuadToSol (inQuadProj T) = T.val.val := by +lemma inQuadToSol_proj (T : inQuadSol) : inQuadToSol (inQuadProj T) = T.val := by rw [inQuadProj, inQuadToSol_smul] apply ACCSystem.Sols.ext change _ • (planeY₃B₃ _ _ _ _).val = _ @@ -306,20 +341,17 @@ lemma inQuadToSol_proj (T : inQuadSol) (h : cubicCoeff T.val.val ≠ 0) : rw [cube_proj, cube_proj_proj_B₃, cube_proj_proj_Y₃] ring_nf simp only [zero_smul, add_zero, Fin.isValue, Fin.reduceFinMk, zero_add] - have h1 : (cubeTriLin (T.val.val.val, T.val.val.val, Y₃.val) ^ 2 * dot (Y₃.val, B₃.val) ^ 3 * 3 + - dot (Y₃.val, B₃.val) ^ 3 * cubeTriLin (T.val.val.val, T.val.val.val, B₃.val) ^ 2 - * 3) = cubicCoeff T.val.val := by + have h1 : (cubeTriLin (T.val.val, T.val.val, Y₃.val) ^ 2 * dot (Y₃.val, B₃.val) ^ 3 * 3 + + dot (Y₃.val, B₃.val) ^ 3 * cubeTriLin (T.val.val, T.val.val, B₃.val) ^ 2 + * 3) = cubicCoeff T.val := by rw [cubicCoeff] ring rw [h1] - rw [← MulAction.mul_smul, mul_comm, mul_inv_cancel h] + have h2 := (inCubeSolProp_iff_cubicCoeff_zero T.val).mpr.mt T.prop.2.2 + rw [← MulAction.mul_smul, mul_comm, mul_inv_cancel h2] simp -def inQuadCube : Type := {R : inQuad // inCubeProp R.val.val} - -def inQuadCubeSol : Type := {R : inQuadSol // inCubeSolProp R.val.val} - -/-- The case where the plane lies entirely within the quadratic and cubic. -/ +/-- Given a element of `inQuadCube × ℚ × ℚ × ℚ`, a solution to the ACCs. -/ def inQuadCubeToSol : inQuadCube × ℚ × ℚ × ℚ → MSSMACC.Sols := fun (R, b₁, b₂, b₃) => AnomalyFreeMk' (planeY₃B₃ R.val.val.val b₁ b₂ b₃) (by @@ -339,16 +371,17 @@ lemma inQuadCubeToSol_smul (R : inQuadCube) (c₁ c₂ c₃ d : ℚ) : rfl +/-- On elements of `inQuadCubeSol` a right-inverse to `inQuadCubeToSol`. -/ def inQuadCubeProj (T : inQuadCubeSol) : inQuadCube × ℚ × ℚ × ℚ := - (⟨⟨⟨proj T.val.val.val.1.1, (linEqPropSol_iff_proj_linEqProp T.val.val.val).mp T.val.val.prop ⟩, - (inQuadSolProp_iff_proj_inQuadProp T.val.val.val).mp T.val.prop⟩, - (inCubeSolProp_iff_proj_inCubeProp T.val.val.val).mp T.prop⟩, - (dot (Y₃.val, B₃.val)) ⁻¹ * (dot (Y₃.val, T.val.val.val.val) - dot (B₃.val, T.val.val.val.val)), - (dot (Y₃.val, B₃.val)) ⁻¹ * (2 * dot (B₃.val, T.val.val.val.val) - - dot (Y₃.val, T.val.val.val.val)), (dot (Y₃.val, B₃.val)) ⁻¹ * 1) + (⟨⟨⟨proj T.val.1.1, (linEqPropSol_iff_proj_linEqProp T.val).mp T.prop.1 ⟩, + (inQuadSolProp_iff_proj_inQuadProp T.val).mp T.prop.2.1⟩, + (inCubeSolProp_iff_proj_inCubeProp T.val).mp T.prop.2.2⟩, + (dot (Y₃.val, B₃.val))⁻¹ * (dot (Y₃.val, T.val.val) - dot (B₃.val, T.val.val)), + (dot (Y₃.val, B₃.val))⁻¹ * (2 * dot (B₃.val, T.val.val) - dot (Y₃.val, T.val.val)), + (dot (Y₃.val, B₃.val))⁻¹ * 1) lemma inQuadCubeToSol_proj (T : inQuadCubeSol) : - inQuadCubeToSol (inQuadCubeProj T) = T.val.val.val := by + inQuadCubeToSol (inQuadCubeProj T) = T.val := by rw [inQuadCubeProj, inQuadCubeToSol_smul] apply ACCSystem.Sols.ext change _ • (planeY₃B₃ _ _ _ _).val = _ @@ -361,8 +394,9 @@ lemma inQuadCubeToSol_proj (T : inQuadCubeSol) : rw [show dot (Y₃.val, B₃.val) = 108 by rfl] simp -def toSol : - MSSMACC.AnomalyFreePerp × ℚ × ℚ × ℚ → MSSMACC.Sols := fun (R, a, b, c) => +/-- Given an element of `MSSMACC.AnomalyFreePerp × ℚ × ℚ × ℚ` a solution. We will +show that this map is a surjection. -/ +def toSol : MSSMACC.AnomalyFreePerp × ℚ × ℚ × ℚ → MSSMACC.Sols := fun (R, a, b, c) => if h₃ : lineEqProp R ∧ inQuadProp R ∧ inCubeProp R then inQuadCubeToSol (⟨⟨⟨R, h₃.1⟩, h₃.2.1⟩, h₃.2.2⟩, a, b, c) else @@ -374,58 +408,56 @@ def toSol : else toSolNS ⟨R, a, b, c⟩ -lemma toSol_toSolNSProj (T : MSSMACC.Sols) (h₁ : ¬ lineEqPropSol T) : - toSol (toSolNSProj T) = T := by - have h1 : ¬ lineEqProp (toSolNSProj T).1 := (linEqPropSol_iff_proj_linEqProp T).mpr.mt h₁ +lemma toSol_toSolNSProj (T : notInLineEqSol) : + ∃ X, toSol X = T.val := by + use toSolNSProj T.val + have h1 : ¬ lineEqProp (toSolNSProj T.val).1 := + (linEqPropSol_iff_proj_linEqProp T.val).mpr.mt T.prop rw [toSol] simp_all - exact toSolNS_proj T (mt (lineEqPropSol_iff_lineEqCoeff_zero T).mpr h₁) + exact toSolNS_proj T -lemma toSol_inLineEq (T : MSSMACC.Sols) (h₁ : lineEqPropSol T) (h₂ : ¬ inQuadSolProp T) : - ∃ X, toSol X = T := by - let X := inLineEqProj ⟨T, h₁⟩ +lemma toSol_inLineEq (T : inLineEqSol) : ∃ X, toSol X = T.val := by + let X := inLineEqProj T use ⟨X.1.val, X.2.1, X.2.2⟩ - have ha₁ : ¬ inQuadProp X.1.val := (inQuadSolProp_iff_proj_inQuadProp T).mpr.mt h₂ - have ha₂ : lineEqProp X.1.val := (linEqPropSol_iff_proj_linEqProp T).mp h₁ + have : ¬ inQuadProp X.1.val := (inQuadSolProp_iff_proj_inQuadProp T.val).mpr.mt T.prop.2 + have : lineEqProp X.1.val := (linEqPropSol_iff_proj_linEqProp T.val).mp T.prop.1 rw [toSol] simp_all - exact inLineEqToSol_proj ⟨T, h₁⟩ (mt (inQuadSolProp_iff_quadCoeff_zero T).mpr h₂) + exact inLineEqToSol_proj T -lemma toSol_inQuad (T : MSSMACC.Sols) (h₁ : lineEqPropSol T) (h₂ : inQuadSolProp T) - (h₃ : ¬ inCubeSolProp T) : ∃ X, toSol X = T := by - let X := inQuadProj ⟨⟨T, h₁⟩, h₂⟩ +lemma toSol_inQuad (T : inQuadSol) : ∃ X, toSol X = T.val := by + let X := inQuadProj T use ⟨X.1.val.val, X.2.1, X.2.2⟩ - have ha₁ : ¬ inCubeProp X.1.val.val := (inCubeSolProp_iff_proj_inCubeProp T).mpr.mt h₃ - have ha₂ : inQuadProp X.1.val.val := (inQuadSolProp_iff_proj_inQuadProp T).mp h₂ - have ha₃ : lineEqProp X.1.val.val := (linEqPropSol_iff_proj_linEqProp T).mp h₁ + have : ¬ inCubeProp X.1.val.val := (inCubeSolProp_iff_proj_inCubeProp T.val).mpr.mt T.prop.2.2 + have : inQuadProp X.1.val.val := (inQuadSolProp_iff_proj_inQuadProp T.val).mp T.prop.2.1 + have : lineEqProp X.1.val.val := (linEqPropSol_iff_proj_linEqProp T.val).mp T.prop.1 rw [toSol] simp_all - exact inQuadToSol_proj ⟨⟨T, h₁⟩, h₂⟩ (mt (inCubeSolProp_iff_cubicCoeff_zero T).mpr h₃) + exact inQuadToSol_proj T -lemma toSol_inQuadCube (T : MSSMACC.Sols) (h₁ : lineEqPropSol T) (h₂ : inQuadSolProp T) - (h₃ : inCubeSolProp T) : ∃ X, toSol X = T := by - let X := inQuadCubeProj ⟨⟨⟨T, h₁⟩, h₂⟩, h₃⟩ +lemma toSol_inQuadCube (T : inQuadCubeSol) : ∃ X, toSol X = T.val := by + let X := inQuadCubeProj T use ⟨X.1.val.val.val, X.2.1, X.2.2⟩ - have ha₁ : inCubeProp X.1.val.val.val := (inCubeSolProp_iff_proj_inCubeProp T).mp h₃ - have ha₂ : inQuadProp X.1.val.val.val := (inQuadSolProp_iff_proj_inQuadProp T).mp h₂ - have ha₃ : lineEqProp X.1.val.val.val := (linEqPropSol_iff_proj_linEqProp T).mp h₁ + have : inCubeProp X.1.val.val.val := (inCubeSolProp_iff_proj_inCubeProp T.val).mp T.prop.2.2 + have : inQuadProp X.1.val.val.val := (inQuadSolProp_iff_proj_inQuadProp T.val).mp T.prop.2.1 + have : lineEqProp X.1.val.val.val := (linEqPropSol_iff_proj_linEqProp T.val).mp T.prop.1 rw [toSol] simp_all - exact inQuadCubeToSol_proj ⟨⟨⟨T, h₁⟩, h₂⟩, h₃⟩ + exact inQuadCubeToSol_proj T theorem toSol_surjective : Function.Surjective toSol := by intro T by_cases h₁ : ¬ lineEqPropSol T - use toSolNSProj T - exact toSol_toSolNSProj T h₁ + exact toSol_toSolNSProj ⟨T, h₁⟩ simp at h₁ by_cases h₂ : ¬ inQuadSolProp T - exact toSol_inLineEq T h₁ h₂ + exact toSol_inLineEq ⟨T, And.intro h₁ h₂⟩ simp at h₂ by_cases h₃ : ¬ inCubeSolProp T - exact toSol_inQuad T h₁ h₂ h₃ + exact toSol_inQuad ⟨T, And.intro h₁ (And.intro h₂ h₃)⟩ simp at h₃ - exact toSol_inQuadCube T h₁ h₂ h₃ + exact toSol_inQuadCube ⟨T, And.intro h₁ (And.intro h₂ h₃)⟩ end AnomalyFreePerp