theorem Hex.Conway.conwayPoly_compat (p m n : Nat) [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (_hdvd : m ∣ n) (hm : SupportedEntry p m) (hn : SupportedEntry p n) (hcompat : Compatible p m n hm hn) : Compatible p m n hm hn

Re-export a supplied compatibility witness through the uniform API. The generated compat_p_m_n theorems supply the witnesses for supported proper-divisor pairs.

theorem Hex.Conway.not_compatible_11_4_6 : ¬Compatible 11 4 6 supportedEntry_11_4 supportedEntry_11_6

Compatibility is not vacuous: it fails when the degrees are not in the subfield lattice. Here 4 ∤ 6, and the check says so rather than returning true for everything put in front of it.