The q3=29 D=37 source order
ProvedOddPerfectNumber.order_37_mod_73_eq_9finite-arithmeticodd-perfectorder-certificateq2-fiveq3-twentynine
The multiplicative order of 37 modulo 73 is exactly 9.
Preamble
import Mathlib
Formal statement
namespace OddPerfectNumber theorem order_37_mod_73_eq_9 : orderOf (37 : ZMod 73) = 9 := by sorry end OddPerfectNumber
Source
Exact order certificate for the unique odd-order q4=37 source in the D=37, p=73 branch.