Numerical certificates for the explicit strong-approximation cutoff #
This file packages the closed real-power and natural-power calculations used by the explicit middle game, endgame, cage, and small-order argument.
The certificates for the first explicit record remain available for comparison, but the canonical declarations below use the ninth-moment cutoff.
At the explicit cutoff, the all-divisors Corvaja--Zannier estimate obeys
both finite size conditions throughout the range
p^(7/32) < currentOrder < p^(25/32).
The primitive-inclusion--exclusion error is strictly smaller than its
main term for an exponent at most 2*p^(9/32) and every coefficient at most
34.
Split-torus form of the explicit primitive-trace certificate.
Nonsplit-torus form of the explicit primitive-trace certificate.
The trace-zero order bound 4 lies below the explicit endgame threshold.
The middle-game lower threshold also dominates the order-four exceptional case.
The coefficient 100522 cage error is dominated by p at the explicit
cutoff.
Variant of explicit_lowOrder_contradiction for the d + 1 cutoff used
when maximality turns a strict order bound into a finite-set inclusion.
Below the five-sixths threshold, the coefficient-48 divisor term times
the current order is strictly smaller than p.
Assembly-facing alias for the five-sixths middle-game certificate.
Primitive-trace inclusion--exclusion at exponent at most 2*p^(1/6).
Split-torus form of the improved primitive-trace certificate.
Nonsplit-torus form of the improved primitive-trace certificate.
The trace-zero order bound lies below the improved endgame threshold.
A divisor-sensitive small-order set large enough to contain a nonempty
p-divisible orbit forces the Corvaja--Zannier cube below the maximal order.