1. Physlib
  2. Particles
  3. SuperSymmetry
  4. MSSMNu
  5. AnomalyCancellation
  6. LineY3B3
Imports
/- Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ module public import Physlib.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.Y3 public import Physlib.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.B3

The line through B₃ and Y₃

We give properties of lines through B₃ and Y₃. We show that every point on this line is a solution to the quadratic lineY₃B₃Charges_quad and a double point of the cubic lineY₃B₃_doublePoint.

References

The main reference for the material in this file is: [Allanach, Madigan and Tooby-Smith][Allanach:2021yjy]

@[expose] public section

The line through $Y_3$ and $B_3$ as LinSols.

def lineY₃B₃Charges (a b : ℚ) : MSSMACC.LinSols := a • Y₃.1.1 + b • B₃.1.1
lemma lineY₃B₃Charges_val (a b : ℚ) : (lineY₃B₃Charges a b).val = a • Y₃.1.1.val + b • B₃.1.1.val := rfla:ℚb:ℚ⊢ a ^ 2 * 0 + b ^ 2 * 0 + 2 * (a * (b * 0)) = 0 All goals completed! 🐙a:ℚb:ℚ⊢ a ^ 3 * 0 + b ^ 3 * 0 + 3 * (a * (a * (b * 0))) + 3 * (b * (b * (a * 0))) = 0 All goals completed! 🐙

The line through $Y_3$ and $B_3$ as Sols.

def lineY₃B₃ (a b : ℚ) : MSSMACC.Sols := AnomalyFreeMk' (lineY₃B₃Charges a b) (lineY₃B₃Charges_quad a b) (lineY₃B₃Charges_cubic a b)
lemma lineY₃B₃_val (a b : ℚ) : (lineY₃B₃ a b).val = a • Y₃.val + b • B₃.val := lineY₃B₃Charges_val a bR:MSSMACC.LinSols⊢ 6 * ((fun s i => match s, i with | 0, 0 => 1 | 0, 1 => 1 | 0, 2 => -1 | 1, 0 => -4 | 1, 1 => -4 | 1, 2 => 4 | 2, 0 => 2 | 2, 1 => 2 | 2, 2 => -2 | 3, 0 => -3 | 3, 1 => -3 | 3, 2 => 3 | 4, 0 => 6 | 4, 1 => 6 | 4, 2 => -6 | 5, 0 => 0 | 5, 1 => 0 | 5, 2 => 0, fun s => match s with | 0 => -3 | 1 => 3).1 0 0 * (fun s i => match s, i with | 0, 0 => 1 | 0, 1 => 1 | 0, 2 => -1 | 1, 0 => -1 | 1, 1 => -1 | 1, 2 => 1 | 2, 0 => -1 | 2, 1 => -1 | 2, 2 => 1 | 3, 0 => -3 | 3, 1 => -3 | 3, 2 => 3 | 4, 0 => 3 | 4, 1 => 3 | 4, 2 => -3 | 5, 0 => 3 | 5, 1 => 3 | 5, 2 => -3, fun s => match s with | 0 => -3 | 1 => 3).1 0 0 * Q R.val 0) + 3 * ((fun s i => match s, i with | 0, 0 => 1 | 0, 1 => 1 | 0, 2 => -1 | 1, 0 => -4 | 1, 1 => -4 | 1, 2 => 4 | 2, 0 => 2 | 2, 1 => 2 | 2, 2 => -2 | 3, 0 => -3 | 3, 1 => -3 | 3, 2 => 3 | 4, 0 => 6 | 4, 1 => 6 | 4, 2 => -6 | 5, 0 => 0 | 5, 1 => 0 | 5, 2 => 0, fun s => match s with | 0 => -3 | 1 => 3).1 1 0 * (fun s i => match s, i with | 0, 0 => 1 | 0, 1 => 1 | 0, 2 => -1 | 1, 0 => -1 | 1, 1 => -1 | 1, 2 => 1 | 2, 0 => -1 | 2, 1 => -1 | 2, 2 => 1 | 3, 0 => -3 | 3, 1 => -3 | 3, 2 => 3 | 4, 0 => 3 | 4, 1 => 3 | 4, 2 => -3 | 5, 0 => 3 | 5, 1 => 3 | 5, 2 => -3, fun s => match s with | 0 => -3 | 1 => 3).1 1 0 * U R.val 0) + 3 * ((fun s i => match s, i with | 0, 0 => 1 | 0, 1 => 1 | 0, 2 => -1 | 1, 0 => -4 | 1, 1 => -4 | 1, 2 => 4 | 2, 0 => 2 | 2, 1 => 2 | 2, 2 => -2 | 3, 0 => -3 | 3, 1 => -3 | 3, 2 => 3 | 4, 0 => 6 | 4, 1 => 6 | 4, 2 => -6 | 5, 0 => 0 | 5, 1 => 0 | 5, 2 => 0, fun s => match s with | 0 => -3 | 1 => 3).1 2 0 * (fun s i => match s, i with | 0, 0 => 1 | 0, 1 => 1 | 0, 2 => -1 | 1, 0 => -1 | 1, 1 => -1 | 1, 2 => 1 | 2, 0 => -1 | 2, 1 => -1 | 2, 2 => 1 | 3, 0 => -3 | 3, 1 => -3 | 3, 2 => 3 | 4, 0 => 3 | 4, 1 => 3 | 4, 2 => -3 | 5, 0 => 3 | 5, 1 => 3 | 5, 2 => -3, fun s => match s with | 0 => -3 | 1 => 3).1 2 0 * D R.val 0) + 2 * ((fun s i => match s, i with | 0, 0 => 1 | 0, 1 => 1 | 0, 2 => -1 | 1, 0 => -4 | 1, 1 => -4 | 1, 2 => 4 | 2, 0 => 2 | 2, 1 => 2 | 2, 2 => -2 | 3, 0 => -3 | 3, 1 => -3 | 3, 2 => 3 | 4, 0 => 6 | 4, 1 => 6 | 4, 2 => -6 | 5, 0 => 0 | 5, 1 => 0 | 5, 2 => 0, fun s => match s with | 0 => -3 | 1 => 3).1 3 0 * (fun s i => match s, i with | 0, 0 => 1 | 0, 1 => 1 | 0, 2 => -1 | 1, 0 => -1 | 1, 1 => -1 | 1, 2 => 1 | 2, 0 => -1 | 2, 1 => -1 | 2, 2 => 1 | 3, 0 => -3 | 3, 1 => -3 | 3, 2 => 3 | 4, 0 => 3 | 4, 1 => 3 | 4, 2 => -3 | 5, 0 => 3 | 5, 1 => 3 | 5, 2 => -3, fun s => match s with | 0 => -3 | 1 => 3).1 3 0 * L R.val 0) + (fun s i => match s, i with | 0, 0 => 1 | 0, 1 => 1 | 0, 2 => -1 | 1, 0 => -4 | 1, 1 => -4 | 1, 2 => 4 | 2, 0 => 2 | 2, 1 => 2 | 2, 2 => -2 | 3, 0 => -3 | 3, 1 => -3 | 3, 2 => 3 | 4, 0 => 6 | 4, 1 => 6 | 4, 2 => -6 | 5, 0 => 0 | 5, 1 => 0 | 5, 2 => 0, fun s => match s with | 0 => -3 | 1 => 3).1 4 0 * (fun s i => match s, i with | 0, 0 => 1 | 0, 1 => 1 | 0, 2 => -1 | 1, 0 => -1 | 1, 1 => -1 | 1, 2 => 1 | 2, 0 => -1 | 2, 1 => -1 | 2, 2 => 1 | 3, 0 => -3 | 3, 1 => -3 | 3, 2 => 3 | 4, 0 => 3 | 4, 1 => 3 | 4, 2 => -3 | 5, 0 => 3 | 5, 1 => 3 | 5, 2 => -3, fun s => match s with | 0 => -3 | 1 => 3).1 4 0 * E R.val 0 + (fun s i => match s, i with | 0, 0 => 1 | 0, 1 => 1 | 0, 2 => -1 | 1, 0 => -4 | 1, 1 => -4 | 1, 2 => 4 | 2, 0 => 2 | 2, 1 => 2 | 2, 2 => -2 | 3, 0 => -3 | 3, 1 => -3 | 3, 2 => 3 | 4, 0 => 6 | 4, 1 => 6 | 4, 2 => -6 | 5, 0 => 0 | 5, 1 => 0 | 5, 2 => 0, fun s => match s with | 0 => -3 | 1 => 3).1 5 0 * (fun s i => match s, i with | 0, 0 => 1 | 0, 1 => 1 | 0, 2 => -1 | 1, 0 => -1 | 1, 1 => -1 | 1, 2 => 1 | 2, 0 => -1 | 2, 1 => -1 | 2, 2 => 1 | 3, 0 => -3 | 3, 1 => -3 | 3, 2 => 3 | 4, 0 => 3 | 4, 1 => 3 | 4, 2 => -3 | 5, 0 => 3 | 5, 1 => 3 | 5, 2 => -3, fun s => match s with | 0 => -3 | 1 => 3).1 5 0 * N R.val 0 + (6 * ((fun s i => match s, i with | 0, 0 => 1 | 0, 1 => 1 | 0, 2 => -1 | 1, 0 => -4 | 1, 1 => -4 | 1, 2 => 4 | 2, 0 => 2 | 2, 1 => 2 | 2, 2 => -2 | 3, 0 => -3 | 3, 1 => -3 | 3, 2 => 3 | 4, 0 => 6 | 4, 1 => 6 | 4, 2 => -6 | 5, 0 => 0 | 5, 1 => 0 | 5, 2 => 0, fun s => match s with | 0 => -3 | 1 => 3).1 0 1 * (fun s i => match s, i with | 0, 0 => 1 | 0, 1 => 1 | 0, 2 => -1 | 1, 0 => -1 | 1, 1 => -1 | 1, 2 => 1 | 2, 0 => -1 | 2, 1 => -1 | 2, 2 => 1 | 3, 0 => -3 | 3, 1 => -3 | 3, 2 => 3 | 4, 0 => 3 | 4, 1 => 3 | 4, 2 => -3 | 5, 0 => 3 | 5, 1 => 3 | 5, 2 => -3, fun s => match s with | 0 => -3 | 1 => 3).1 0 1 * Q R.val 1) + 3 * ((fun s i => match s, i with | 0, 0 => 1 | 0, 1 => 1 | 0, 2 => -1 | 1, 0 => -4 | 1, 1 => -4 | 1, 2 => 4 | 2, 0 => 2 | 2, 1 => 2 | 2, 2 => -2 | 3, 0 => -3 | 3, 1 => -3 | 3, 2 => 3 | 4, 0 => 6 | 4, 1 => 6 | 4, 2 => -6 | 5, 0 => 0 | 5, 1 => 0 | 5, 2 => 0, fun s => match s with | 0 => -3 | 1 => 3).1 1 1 * (fun s i => match s, i with | 0, 0 => 1 | 0, 1 => 1 | 0, 2 => -1 | 1, 0 => -1 | 1, 1 => -1 | 1, 2 => 1 | 2, 0 => -1 | 2, 1 => -1 | 2, 2 => 1 | 3, 0 => -3 | 3, 1 => -3 | 3, 2 => 3 | 4, 0 => 3 | 4, 1 => 3 | 4, 2 => -3 | 5, 0 => 3 | 5, 1 => 3 | 5, 2 => -3, fun s => match s with | 0 => -3 | 1 => 3).1 1 1 * U R.val 1) + 3 * ((fun s i => match s, i with | 0, 0 => 1 | 0, 1 => 1 | 0, 2 => -1 | 1, 0 => -4 | 1, 1 => -4 | 1, 2 => 4 | 2, 0 => 2 | 2, 1 => 2 | 2, 2 => -2 | 3, 0 => -3 | 3, 1 => -3 | 3, 2 => 3 | 4, 0 => 6 | 4, 1 => 6 | 4, 2 => -6 | 5, 0 => 0 | 5, 1 => 0 | 5, 2 => 0, fun s => match s with | 0 => -3 | 1 => 3).1 2 1 * (fun s i => match s, i with | 0, 0 => 1 | 0, 1 => 1 | 0, 2 => -1 | 1, 0 => -1 | 1, 1 => -1 | 1, 2 => 1 | 2, 0 => -1 | 2, 1 => -1 | 2, 2 => 1 | 3, 0 => -3 | 3, 1 => -3 | 3, 2 => 3 | 4, 0 => 3 | 4, 1 => 3 | 4, 2 => -3 | 5, 0 => 3 | 5, 1 => 3 | 5, 2 => -3, fun s => match s with | 0 => -3 | 1 => 3).1 2 1 * D R.val 1) + 2 * ((fun s i => match s, i with | 0, 0 => 1 | 0, 1 => 1 | 0, 2 => -1 | 1, 0 => -4 | 1, 1 => -4 | 1, 2 => 4 | 2, 0 => 2 | 2, 1 => 2 | 2, 2 => -2 | 3, 0 => -3 | 3, 1 => -3 | 3, 2 => 3 | 4, 0 => 6 | 4, 1 => 6 | 4, 2 => -6 | 5, 0 => 0 | 5, 1 => 0 | 5, 2 => 0, fun s => match s with | 0 => -3 | 1 => 3).1 3 1 * (fun s i => match s, i with | 0, 0 => 1 | 0, 1 => 1 | 0, 2 => -1 | 1, 0 => -1 | 1, 1 => -1 | 1, 2 => 1 | 2, 0 => -1 | 2, 1 => -1 | 2, 2 => 1 | 3, 0 => -3 | 3, 1 => -3 | 3, 2 => 3 | 4, 0 => 3 | 4, 1 => 3 | 4, 2 => -3 | 5, 0 => 3 | 5, 1 => 3 | 5, 2 => -3, fun s => match s with | 0 => -3 | 1 => 3).1 3 1 * L R.val 1) + (fun s i => match s, i with | 0, 0 => 1 | 0, 1 => 1 | 0, 2 => -1 | 1, 0 => -4 | 1, 1 => -4 | 1, 2 => 4 | 2, 0 => 2 | 2, 1 => 2 | 2, 2 => -2 | 3, 0 => -3 | 3, 1 => -3 | 3, 2 => 3 | 4, 0 => 6 | 4, 1 => 6 | 4, 2 => -6 | 5, 0 => 0 | 5, 1 => 0 | 5, 2 => 0, fun s => match s with | 0 => -3 | 1 => 3).1 4 1 * (fun s i => match s, i with | 0, 0 => 1 | 0, 1 => 1 | 0, 2 => -1 | 1, 0 => -1 | 1, 1 => -1 | 1, 2 => 1 | 2, 0 => -1 | 2, 1 => -1 | 2, 2 => 1 | 3, 0 => -3 | 3, 1 => -3 | 3, 2 => 3 | 4, 0 => 3 | 4, 1 => 3 | 4, 2 => -3 | 5, 0 => 3 | 5, 1 => 3 | 5, 2 => -3, fun s => match s with | 0 => -3 | 1 => 3).1 4 1 * E R.val 1 + (fun s i => match s, i with | 0, 0 => 1 | 0, 1 => 1 | 0, 2 => -1 | 1, 0 => -4 | 1, 1 => -4 | 1, 2 => 4 | 2, 0 => 2 | 2, 1 => 2 | 2, 2 => -2 | 3, 0 => -3 | 3, 1 => -3 | 3, 2 => 3 | 4, 0 => 6 | 4, 1 => 6 | 4, 2 => -6 | 5, 0 => 0 | 5, 1 => 0 | 5, 2 => 0, fun s => match s with | 0 => -3 | 1 => 3).1 5 1 * (fun s i => match s, i with | 0, 0 => 1 | 0, 1 => 1 | 0, 2 => -1 | 1, 0 => -1 | 1, 1 => -1 | 1, 2 => 1 | 2, 0 => -1 | 2, 1 => -1 | 2, 2 => 1 | 3, 0 => -3 | 3, 1 => -3 | 3, 2 => 3 | 4, 0 => 3 | 4, 1 => 3 | 4, 2 => -3 | 5, 0 => 3 | 5, 1 => 3 | 5, 2 => -3, fun s => match s with | 0 => -3 | 1 => 3).1 5 1 * N R.val 1) + (6 * ((fun s i => match s, i with | 0, 0 => 1 | 0, 1 => 1 | 0, 2 => -1 | 1, 0 => -4 | 1, 1 => -4 | 1, 2 => 4 | 2, 0 => 2 | 2, 1 => 2 | 2, 2 => -2 | 3, 0 => -3 | 3, 1 => -3 | 3, 2 => 3 | 4, 0 => 6 | 4, 1 => 6 | 4, 2 => -6 | 5, 0 => 0 | 5, 1 => 0 | 5, 2 => 0, fun s => match s with | 0 => -3 | 1 => 3).1 0 2 * (fun s i => match s, i with | 0, 0 => 1 | 0, 1 => 1 | 0, 2 => -1 | 1, 0 => -1 | 1, 1 => -1 | 1, 2 => 1 | 2, 0 => -1 | 2, 1 => -1 | 2, 2 => 1 | 3, 0 => -3 | 3, 1 => -3 | 3, 2 => 3 | 4, 0 => 3 | 4, 1 => 3 | 4, 2 => -3 | 5, 0 => 3 | 5, 1 => 3 | 5, 2 => -3, fun s => match s with | 0 => -3 | 1 => 3).1 0 2 * Q R.val 2) + 3 * ((fun s i => match s, i with | 0, 0 => 1 | 0, 1 => 1 | 0, 2 => -1 | 1, 0 => -4 | 1, 1 => -4 | 1, 2 => 4 | 2, 0 => 2 | 2, 1 => 2 | 2, 2 => -2 | 3, 0 => -3 | 3, 1 => -3 | 3, 2 => 3 | 4, 0 => 6 | 4, 1 => 6 | 4, 2 => -6 | 5, 0 => 0 | 5, 1 => 0 | 5, 2 => 0, fun s => match s with | 0 => -3 | 1 => 3).1 1 2 * (fun s i => match s, i with | 0, 0 => 1 | 0, 1 => 1 | 0, 2 => -1 | 1, 0 => -1 | 1, 1 => -1 | 1, 2 => 1 | 2, 0 => -1 | 2, 1 => -1 | 2, 2 => 1 | 3, 0 => -3 | 3, 1 => -3 | 3, 2 => 3 | 4, 0 => 3 | 4, 1 => 3 | 4, 2 => -3 | 5, 0 => 3 | 5, 1 => 3 | 5, 2 => -3, fun s => match s with | 0 => -3 | 1 => 3).1 1 2 * U R.val 2) + 3 * ((fun s i => match s, i with | 0, 0 => 1 | 0, 1 => 1 | 0, 2 => -1 | 1, 0 => -4 | 1, 1 => -4 | 1, 2 => 4 | 2, 0 => 2 | 2, 1 => 2 | 2, 2 => -2 | 3, 0 => -3 | 3, 1 => -3 | 3, 2 => 3 | 4, 0 => 6 | 4, 1 => 6 | 4, 2 => -6 | 5, 0 => 0 | 5, 1 => 0 | 5, 2 => 0, fun s => match s with | 0 => -3 | 1 => 3).1 2 2 * (fun s i => match s, i with | 0, 0 => 1 | 0, 1 => 1 | 0, 2 => -1 | 1, 0 => -1 | 1, 1 => -1 | 1, 2 => 1 | 2, 0 => -1 | 2, 1 => -1 | 2, 2 => 1 | 3, 0 => -3 | 3, 1 => -3 | 3, 2 => 3 | 4, 0 => 3 | 4, 1 => 3 | 4, 2 => -3 | 5, 0 => 3 | 5, 1 => 3 | 5, 2 => -3, fun s => match s with | 0 => -3 | 1 => 3).1 2 2 * D R.val 2) + 2 * ((fun s i => match s, i with | 0, 0 => 1 | 0, 1 => 1 | 0, 2 => -1 | 1, 0 => -4 | 1, 1 => -4 | 1, 2 => 4 | 2, 0 => 2 | 2, 1 => 2 | 2, 2 => -2 | 3, 0 => -3 | 3, 1 => -3 | 3, 2 => 3 | 4, 0 => 6 | 4, 1 => 6 | 4, 2 => -6 | 5, 0 => 0 | 5, 1 => 0 | 5, 2 => 0, fun s => match s with | 0 => -3 | 1 => 3).1 3 2 * (fun s i => match s, i with | 0, 0 => 1 | 0, 1 => 1 | 0, 2 => -1 | 1, 0 => -1 | 1, 1 => -1 | 1, 2 => 1 | 2, 0 => -1 | 2, 1 => -1 | 2, 2 => 1 | 3, 0 => -3 | 3, 1 => -3 | 3, 2 => 3 | 4, 0 => 3 | 4, 1 => 3 | 4, 2 => -3 | 5, 0 => 3 | 5, 1 => 3 | 5, 2 => -3, fun s => match s with | 0 => -3 | 1 => 3).1 3 2 * L R.val 2) + (fun s i => match s, i with | 0, 0 => 1 | 0, 1 => 1 | 0, 2 => -1 | 1, 0 => -4 | 1, 1 => -4 | 1, 2 => 4 | 2, 0 => 2 | 2, 1 => 2 | 2, 2 => -2 | 3, 0 => -3 | 3, 1 => -3 | 3, 2 => 3 | 4, 0 => 6 | 4, 1 => 6 | 4, 2 => -6 | 5, 0 => 0 | 5, 1 => 0 | 5, 2 => 0, fun s => match s with | 0 => -3 | 1 => 3).1 4 2 * (fun s i => match s, i with | 0, 0 => 1 | 0, 1 => 1 | 0, 2 => -1 | 1, 0 => -1 | 1, 1 => -1 | 1, 2 => 1 | 2, 0 => -1 | 2, 1 => -1 | 2, 2 => 1 | 3, 0 => -3 | 3, 1 => -3 | 3, 2 => 3 | 4, 0 => 3 | 4, 1 => 3 | 4, 2 => -3 | 5, 0 => 3 | 5, 1 => 3 | 5, 2 => -3, fun s => match s with | 0 => -3 | 1 => 3).1 4 2 * E R.val 2 + (fun s i => match s, i with | 0, 0 => 1 | 0, 1 => 1 | 0, 2 => -1 | 1, 0 => -4 | 1, 1 => -4 | 1, 2 => 4 | 2, 0 => 2 | 2, 1 => 2 | 2, 2 => -2 | 3, 0 => -3 | 3, 1 => -3 | 3, 2 => 3 | 4, 0 => 6 | 4, 1 => 6 | 4, 2 => -6 | 5, 0 => 0 | 5, 1 => 0 | 5, 2 => 0, fun s => match s with | 0 => -3 | 1 => 3).1 5 2 * (fun s i => match s, i with | 0, 0 => 1 | 0, 1 => 1 | 0, 2 => -1 | 1, 0 => -1 | 1, 1 => -1 | 1, 2 => 1 | 2, 0 => -1 | 2, 1 => -1 | 2, 2 => 1 | 3, 0 => -3 | 3, 1 => -3 | 3, 2 => 3 | 4, 0 => 3 | 4, 1 => 3 | 4, 2 => -3 | 5, 0 => 3 | 5, 1 => 3 | 5, 2 => -3, fun s => match s with | 0 => -3 | 1 => 3).1 5 2 * N R.val 2) + (2 * (fun s i => match s, i with | 0, 0 => 1 | 0, 1 => 1 | 0, 2 => -1 | 1, 0 => -4 | 1, 1 => -4 | 1, 2 => 4 | 2, 0 => 2 | 2, 1 => 2 | 2, 2 => -2 | 3, 0 => -3 | 3, 1 => -3 | 3, 2 => 3 | 4, 0 => 6 | 4, 1 => 6 | 4, 2 => -6 | 5, 0 => 0 | 5, 1 => 0 | 5, 2 => 0, fun s => match s with | 0 => -3 | 1 => 3).2 0 * (fun s i => match s, i with | 0, 0 => 1 | 0, 1 => 1 | 0, 2 => -1 | 1, 0 => -1 | 1, 1 => -1 | 1, 2 => 1 | 2, 0 => -1 | 2, 1 => -1 | 2, 2 => 1 | 3, 0 => -3 | 3, 1 => -3 | 3, 2 => 3 | 4, 0 => 3 | 4, 1 => 3 | 4, 2 => -3 | 5, 0 => 3 | 5, 1 => 3 | 5, 2 => -3, fun s => match s with | 0 => -3 | 1 => 3).2 0 * Hd R.val + 2 * (fun s i => match s, i with | 0, 0 => 1 | 0, 1 => 1 | 0, 2 => -1 | 1, 0 => -4 | 1, 1 => -4 | 1, 2 => 4 | 2, 0 => 2 | 2, 1 => 2 | 2, 2 => -2 | 3, 0 => -3 | 3, 1 => -3 | 3, 2 => 3 | 4, 0 => 6 | 4, 1 => 6 | 4, 2 => -6 | 5, 0 => 0 | 5, 1 => 0 | 5, 2 => 0, fun s => match s with | 0 => -3 | 1 => 3).2 1 * (fun s i => match s, i with | 0, 0 => 1 | 0, 1 => 1 | 0, 2 => -1 | 1, 0 => -1 | 1, 1 => -1 | 1, 2 => 1 | 2, 0 => -1 | 2, 1 => -1 | 2, 2 => 1 | 3, 0 => -3 | 3, 1 => -3 | 3, 2 => 3 | 4, 0 => 3 | 4, 1 => 3 | 4, 2 => -3 | 5, 0 => 3 | 5, 1 => 3 | 5, 2 => -3, fun s => match s with | 0 => -3 | 1 => 3).2 1 * Hu R.val) = 0 R:MSSMACC.LinSols⊢ 6 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 0))) + 3 * (4 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 0)))) + -(3 * (2 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 0))))) + 2 * (3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 0)))) + 6 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 0))) + (6 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 1))) + 3 * (4 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 1)))) + -(3 * (2 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 1))))) + 2 * (3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 1)))) + 6 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 1)))) + (6 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 2))) + 3 * (4 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 2)))) + -(3 * (2 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 2))))) + 2 * (3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 2)))) + 6 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 2)))) + (2 * 3 * 3 * R.val 18 + 2 * 3 * 3 * R.val 19) = 0 R:MSSMACC.LinSolshLin:∀ (i : Fin MSSMACC.numberLinear), (MSSMACC.linearACCs i) R.val = 0⊢ 6 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 0))) + 3 * (4 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 0)))) + -(3 * (2 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 0))))) + 2 * (3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 0)))) + 6 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 0))) + (6 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 1))) + 3 * (4 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 1)))) + -(3 * (2 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 1))))) + 2 * (3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 1)))) + 6 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 1)))) + (6 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 2))) + 3 * (4 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 2)))) + -(3 * (2 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 2))))) + 2 * (3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 2)))) + 6 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 2)))) + (2 * 3 * 3 * R.val 18 + 2 * 3 * 3 * R.val 19) = 0 R:MSSMACC.LinSolshLin:∀ (i : Fin MSSMACC.numberLinear), (match i with | 0 => accGrav | 1 => accSU2 | 2 => accSU3 | 3 => accYY) R.val = 0⊢ 6 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 0))) + 3 * (4 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 0)))) + -(3 * (2 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 0))))) + 2 * (3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 0)))) + 6 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 0))) + (6 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 1))) + 3 * (4 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 1)))) + -(3 * (2 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 1))))) + 2 * (3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 1)))) + 6 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 1)))) + (6 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 2))) + 3 * (4 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 2)))) + -(3 * (2 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 2))))) + 2 * (3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 2)))) + 6 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 2)))) + (2 * 3 * 3 * R.val 18 + 2 * 3 * 3 * R.val 19) = 0 R:MSSMACC.LinSolshLin:∀ (i : Fin MSSMACC.numberLinear), (match i with | 0 => accGrav | 1 => accSU2 | 2 => accSU3 | 3 => accYY) R.val = 0h1:(match 1 with | 0 => accGrav | 1 => accSU2 | 2 => accSU3 | 3 => accYY) R.val = 0⊢ 6 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 0))) + 3 * (4 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 0)))) + -(3 * (2 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 0))))) + 2 * (3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 0)))) + 6 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 0))) + (6 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 1))) + 3 * (4 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 1)))) + -(3 * (2 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 1))))) + 2 * (3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 1)))) + 6 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 1)))) + (6 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 2))) + 3 * (4 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 2)))) + -(3 * (2 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 2))))) + 2 * (3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 2)))) + 6 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 2)))) + (2 * 3 * 3 * R.val 18 + 2 * 3 * 3 * R.val 19) = 0 R:MSSMACC.LinSolshLin:∀ (i : Fin MSSMACC.numberLinear), (match i with | 0 => accGrav | 1 => accSU2 | 2 => accSU3 | 3 => accYY) R.val = 0h1:(match 1 with | 0 => accGrav | 1 => accSU2 | 2 => accSU3 | 3 => accYY) R.val = 0h2:(match 2 with | 0 => accGrav | 1 => accSU2 | 2 => accSU3 | 3 => accYY) R.val = 0⊢ 6 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 0))) + 3 * (4 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 0)))) + -(3 * (2 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 0))))) + 2 * (3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 0)))) + 6 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 0))) + (6 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 1))) + 3 * (4 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 1)))) + -(3 * (2 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 1))))) + 2 * (3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 1)))) + 6 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 1)))) + (6 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 2))) + 3 * (4 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 2)))) + -(3 * (2 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 2))))) + 2 * (3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 2)))) + 6 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 2)))) + (2 * 3 * 3 * R.val 18 + 2 * 3 * 3 * R.val 19) = 0 R:MSSMACC.LinSolshLin:∀ (i : Fin MSSMACC.numberLinear), (match i with | 0 => accGrav | 1 => accSU2 | 2 => accSU3 | 3 => accYY) R.val = 0h1:(match 1 with | 0 => accGrav | 1 => accSU2 | 2 => accSU3 | 3 => accYY) R.val = 0h2:(match 2 with | 0 => accGrav | 1 => accSU2 | 2 => accSU3 | 3 => accYY) R.val = 0h3:(match 3 with | 0 => accGrav | 1 => accSU2 | 2 => accSU3 | 3 => accYY) R.val = 0⊢ 6 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 0))) + 3 * (4 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 0)))) + -(3 * (2 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 0))))) + 2 * (3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 0)))) + 6 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 0))) + (6 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 1))) + 3 * (4 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 1)))) + -(3 * (2 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 1))))) + 2 * (3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 1)))) + 6 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 1)))) + (6 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 2))) + 3 * (4 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 2)))) + -(3 * (2 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 2))))) + 2 * (3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 2)))) + 6 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 2)))) + (2 * 3 * 3 * R.val 18 + 2 * 3 * 3 * R.val 19) = 0 R:MSSMACC.LinSolshLin:∀ (i : Fin MSSMACC.numberLinear), (match i with | 0 => accGrav | 1 => accSU2 | 2 => accSU3 | 3 => accYY) R.val = 0h1:∑ i, (3 * Q R.val i + L R.val i) + Hd R.val + Hu R.val = 0h2:∑ i, (2 * Q R.val i + U R.val i + D R.val i) = 0h3:∑ i, (Q R.val i + 8 * U R.val i + 2 * D R.val i + 3 * L R.val i + 6 * E R.val i) + 3 * (Hd R.val + Hu R.val) = 0⊢ 6 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 0))) + 3 * (4 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 0)))) + -(3 * (2 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 0))))) + 2 * (3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 0)))) + 6 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 0))) + (6 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 1))) + 3 * (4 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 1)))) + -(3 * (2 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 1))))) + 2 * (3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 1)))) + 6 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 1)))) + (6 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 2))) + 3 * (4 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 2)))) + -(3 * (2 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 2))))) + 2 * (3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 2)))) + 6 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 2)))) + (2 * 3 * 3 * R.val 18 + 2 * 3 * 3 * R.val 19) = 0 erw [R:MSSMACC.LinSolshLin:∀ (i : Fin MSSMACC.numberLinear), (match i with | 0 => accGrav | 1 => accSU2 | 2 => accSU3 | 3 => accYY) R.val = 0h1:3 * Q R.val 0 + L R.val 0 + (3 * Q R.val 1 + L R.val 1) + (3 * Q R.val 2 + L R.val 2) + Hd R.val + Hu R.val = 0h2:2 * Q R.val 0 + U R.val 0 + D R.val 0 + (2 * Q R.val 1 + U R.val 1 + D R.val 1) + (2 * Q R.val 2 + U R.val 2 + D R.val 2) = 0h3:Q R.val 0 + 8 * U R.val 0 + 2 * D R.val 0 + 3 * L R.val 0 + 6 * E R.val 0 + (Q R.val 1 + 8 * U R.val 1 + 2 * D R.val 1 + 3 * L R.val 1 + 6 * E R.val 1) + (Q R.val 2 + 8 * U R.val 2 + 2 * D R.val 2 + 3 * L R.val 2 + 6 * E R.val 2) + 3 * (Hd R.val + Hu R.val) = 0⊢ 6 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 0))) + 3 * (4 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 0)))) + -(3 * (2 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 0))))) + 2 * (3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 0)))) + 6 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 0))) + (6 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 1))) + 3 * (4 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 1)))) + -(3 * (2 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 1))))) + 2 * (3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 1)))) + 6 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 1)))) + (6 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 2))) + 3 * (4 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 2)))) + -(3 * (2 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 2))))) + 2 * (3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 2)))) + 6 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 2)))) + (2 * 3 * 3 * R.val 18 + 2 * 3 * 3 * R.val 19) = 0R:MSSMACC.LinSolshLin:∀ (i : Fin MSSMACC.numberLinear), (match i with | 0 => accGrav | 1 => accSU2 | 2 => accSU3 | 3 => accYY) R.val = 0h1:3 * Q R.val 0 + L R.val 0 + (3 * Q R.val 1 + L R.val 1) + (3 * Q R.val 2 + L R.val 2) + Hd R.val + Hu R.val = 0h2:2 * Q R.val 0 + U R.val 0 + D R.val 0 + (2 * Q R.val 1 + U R.val 1 + D R.val 1) + (2 * Q R.val 2 + U R.val 2 + D R.val 2) = 0h3:Q R.val 0 + 8 * U R.val 0 + 2 * D R.val 0 + 3 * L R.val 0 + 6 * E R.val 0 + (Q R.val 1 + 8 * U R.val 1 + 2 * D R.val 1 + 3 * L R.val 1 + 6 * E R.val 1) + (Q R.val 2 + 8 * U R.val 2 + 2 * D R.val 2 + 3 * L R.val 2 + 6 * E R.val 2) + 3 * (Hd R.val + Hu R.val) = 0⊢ 6 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 0))) + 3 * (4 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 0)))) + -(3 * (2 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 0))))) + 2 * (3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 0)))) + 6 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 0))) + (6 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 1))) + 3 * (4 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 1)))) + -(3 * (2 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 1))))) + 2 * (3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 1)))) + 6 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 1)))) + (6 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 2))) + 3 * (4 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 2)))) + -(3 * (2 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 2))))) + 2 * (3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 2)))) + 6 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 2)))) + (2 * 3 * 3 * R.val 18 + 2 * 3 * 3 * R.val 19) = 0 at h1 h2 h3 R:MSSMACC.LinSolshLin:∀ (i : Fin MSSMACC.numberLinear), (match i with | 0 => accGrav | 1 => accSU2 | 2 => accSU3 | 3 => accYY) R.val = 0h1:3 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 0))) + R.val (Fin.castAdd 2 (finProdFinEquiv (3, 0))) + (3 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 1))) + R.val (Fin.castAdd 2 (finProdFinEquiv (3, 1)))) + (3 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 2))) + R.val (Fin.castAdd 2 (finProdFinEquiv (3, 2)))) + R.val 18 + R.val 19 = 0h2:2 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 0))) + R.val (Fin.castAdd 2 (finProdFinEquiv (1, 0))) + R.val (Fin.castAdd 2 (finProdFinEquiv (2, 0))) + (2 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 1))) + R.val (Fin.castAdd 2 (finProdFinEquiv (1, 1))) + R.val (Fin.castAdd 2 (finProdFinEquiv (2, 1)))) + (2 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 2))) + R.val (Fin.castAdd 2 (finProdFinEquiv (1, 2))) + R.val (Fin.castAdd 2 (finProdFinEquiv (2, 2)))) = 0h3:R.val (Fin.castAdd 2 (finProdFinEquiv (0, 0))) + 8 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 0))) + 2 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 0))) + 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 0))) + 6 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 0))) + (R.val (Fin.castAdd 2 (finProdFinEquiv (0, 1))) + 8 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 1))) + 2 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 1))) + 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 1))) + 6 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 1)))) + (R.val (Fin.castAdd 2 (finProdFinEquiv (0, 2))) + 8 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 2))) + 2 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 2))) + 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 2))) + 6 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 2)))) + 3 * (R.val 18 + R.val 19) = 0⊢ 6 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 0))) + 3 * (4 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 0)))) + -(3 * (2 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 0))))) + 2 * (3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 0)))) + 6 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 0))) + (6 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 1))) + 3 * (4 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 1)))) + -(3 * (2 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 1))))) + 2 * (3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 1)))) + 6 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 1)))) + (6 * R.val (Fin.castAdd 2 (finProdFinEquiv (0, 2))) + 3 * (4 * R.val (Fin.castAdd 2 (finProdFinEquiv (1, 2)))) + -(3 * (2 * R.val (Fin.castAdd 2 (finProdFinEquiv (2, 2))))) + 2 * (3 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (3, 2)))) + 6 * 3 * R.val (Fin.castAdd 2 (finProdFinEquiv (4, 2)))) + (2 * 3 * 3 * R.val 18 + 2 * 3 * 3 * R.val 19) = 0 linear_combination (norm := All goals completed! 🐙) -(12 * h2) + 9 * h1 + 3 * h3R:MSSMACC.LinSolsa:ℚb:ℚ⊢ a * (a * ((cubeTriLin Y₃.val) Y₃.val) R.val) + a * (b * ((cubeTriLin B₃.val) Y₃.val) R.val) + (b * (a * ((cubeTriLin Y₃.val) B₃.val) R.val) + b * (b * ((cubeTriLin B₃.val) B₃.val) R.val)) = 0 All goals completed! 🐙