Lemmas for 1 family SM Accs

The main result of this file is the conclusion of this paper: Lohitsiri and Tong

That every solution to the ACCs without gravity satisfies for free the gravitational anomaly.

theorem SM.SMNoGrav.One.E_zero_iff_Q_zero {S : (SMNoGrav 1).Sols} : SMCharges.Q S.val 0 = 0 ↔ SMCharges.E S.val 0 = 0

For a set of 1 family SM charges satisfying all ACCs except the gravitational, the charge of Q is zero if and only if E is zero.

theorem SM.SMNoGrav.One.accGrav_Q_zero {S : (SMNoGrav 1).Sols} (hQ : SMCharges.Q S.val 0 = 0) : SMACCs.accGrav S.val = 0

For a set of 1-family SM charges satisfying all ACCs except the gravitational, if the Q charge is zero then the charges satisfy the gravitational ACCs.

theorem SM.SMNoGrav.One.accGrav_Q_neq_zero {S : (SMNoGrav 1).Sols} (hQ : SMCharges.Q S.val 0 ≠ 0) : SMACCs.accGrav S.val = 0

For a set of 1-family SM charges satisfying all ACCs except the gravitational, if the Q charge is not zero then the charges satisfy the gravitational ACCs.

theorem SM.SMNoGrav.One.accGravSatisfied {S : (SMNoGrav 1).Sols} : SMACCs.accGrav S.val = 0

Any solution to the 1-family ACCs without gravity satisfies the gravitational ACC.