17.2. The committed-entry mechanism🔗

The generic constructors need a Hex.Conway.SupportedEntry, the HexConway witness bundling a Conway modulus with its primality and irreducibility proofs. Passing that witness explicitly everywhere is verbose, so HexGFq makes it available through instance synthesis with a one-method class.

Hex.Conway.CommittedEntry carries a single field entry, the committed Hex.Conway.SupportedEntry for the pair (p, n). The library commits one instance per committed table cell, named committedEntry_p_n (for example committedEntry_2_3), covering p ∈ {2, 3, 5, 7, 11, 13} and n ∈ {1, …, 6}. With the instance in scope, the short field spelling resolves the witness automatically. Where a proof needs to name the witness, the explicit form still takes it as an argument.