Line in plane condition

We say a LinSol satisfies the line in plane condition if for all distinct i1, i2, i3 in Fin n, we have S i1 = S i2 or S i1 = - S i2 or 2 S i3 + S i1 + S i2 = 0.

We look at various consequences of this. The main reference for this material is

• https://arxiv.org/pdf/1912.04804.pdf

We will show that n ≥ 4 the line in plane condition on solutions implies the constAbs condition.

def PureU1.LineInPlaneProp : ℚ × ℚ × ℚ → Prop

The proposition on three rationals to satisfy the linInPlane condition.

Equations

• PureU1.LineInPlaneProp s = (s.1 = s.2.1 ∨ s.1 = -s.2.1 ∨ 2 * s.2.2 + s.1 + s.2.1 = 0)

def PureU1.LineInPlaneCond {n : ℕ} (S : (PureU1 n).LinSols) : Prop

The proposition on a LinSol to satisfy the linInPlane condition.

Equations

• PureU1.LineInPlaneCond S = ∀ (i1 i2 i3 : Fin n), i1 ≠ i2 → i2 ≠ i3 → i1 ≠ i3 → PureU1.LineInPlaneProp (S.val i1, S.val i2, S.val i3)

theorem PureU1.lineInPlaneCond_perm {n : ℕ} {S : (PureU1 n).LinSols} (hS : LineInPlaneCond S) (M : (FamilyPermutations n).group) : LineInPlaneCond (((FamilyPermutations n).linSolRep M) S)

theorem PureU1.lineInPlaneCond_eq_last' {n : ℕ} {S : (PureU1 n.succ.succ).LinSols} (hS : LineInPlaneCond S) (h : ¬S.val (Fin.last n).castSucc ^ 2 = S.val (Fin.last n).succ ^ 2) : (2 - ↑n) * S.val (Fin.last (n + 1)) = -(2 - ↑n) * S.val (Fin.last n).castSucc

theorem PureU1.lineInPlaneCond_eq_last {n : ℕ} {S : (PureU1 n.succ.succ.succ.succ.succ).LinSols} (hS : LineInPlaneCond S) : ConstAbsProp (S.val (Fin.last n.succ.succ.succ).castSucc, S.val (Fin.last n.succ.succ.succ).succ)

theorem PureU1.linesInPlane_eq_sq {n : ℕ} {S : (PureU1 n.succ.succ.succ.succ.succ).LinSols} (hS : LineInPlaneCond S) (i j : Fin n.succ.succ.succ.succ.succ) : i ≠ j → ConstAbsProp (S.val i, S.val j)

theorem PureU1.linesInPlane_constAbs {n : ℕ} {S : (PureU1 n.succ.succ.succ.succ.succ).LinSols} (hS : LineInPlaneCond S) : ConstAbs S.val

theorem PureU1.linesInPlane_four (S : (PureU1 4).Sols) (hS : LineInPlaneCond S.toLinSols) : ConstAbsProp (S.val 0, S.val 1)

theorem PureU1.linesInPlane_eq_sq_four {S : (PureU1 4).Sols} (hS : LineInPlaneCond S.toLinSols) (i j : Fin 4) : i ≠ j → ConstAbsProp (S.val i, S.val j)

theorem PureU1.linesInPlane_constAbs_four (S : (PureU1 4).Sols) (hS : LineInPlaneCond S.toLinSols) : ConstAbs S.val

theorem PureU1.linesInPlane_constAbs_AF {n : ℕ} (S : (PureU1 n.succ.succ.succ.succ).Sols) (hS : LineInPlaneCond S.toLinSols) : ConstAbs S.val