QuadRep addition/multiplication/conjugation respect cross-multiplied coefficient equivalence and satisfy commutative-ring laws.
Method: native-ring. Induction: none. Risk: routine.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.