MainStarkDischarged.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Packet equidistribution with Stark's input discharged

Arithmetic Artin reciprocity supplies the even ray realizations used in exceptional-real-zero exclusion. Prime-degree positive-entropy rigidity then implies convergence of complete packets and tightness.

theorem OAI.DukePrimeDegree.prime_degree_packet_equidistribution_of_EKL line 21