corollaryroutine

Enlarging exceptional primes changes only constant

So enlarging

S

S'

only rescales the height bound, same

c

discards extra primes without changing the exponent

Corollary·hei:enlarge-exceptions·§2.2 Contact primes and ordinary integer witnesses

Statement (paper)

S'\supset S

is any fixed finite set of primes, then

\hgt(s)\le H\left(\prod_{q\in S'\setminus S}q\right)^c M_{S'}(s)^c \qquad(s\in\mathbf P^1(\Q)\setminus\mathcal C).

In particular enlarging the exceptional set changes the constant but leaves the exponent unchanged.

In plain English

For any finite set of primes

S'\supset S

, every

s\in\mathbf P^1(\Q)\setminus\mathcal C

satisfies

\hgt(s)\le H\left(\prod_{q\in S'\setminus S}q\right)^c M_{S'}(s)^c

, with the same exponent

c

as in the original height bound. So enlarging the exceptional set only changes the constant.

Why it's here

This follows from the height bound in hei-height, since passing from

S

S'

removes the primes in

S'\setminus S

from the contact product

M_S(s)

and so changes it by at most the product of those primes. It lets later arguments discard finitely many extra primes, such as those arising from a particular root tuple, without affecting the exponent in the uniform height bound for ring elements.

Classified routine:

This is a direct consequence of the height bound hei-height: moving from S to S' removes only the primes in S'\S from the contact radical M_S(s), so M_S(s) changes by at most their product and the bound holds with the same exponent c and a larger constant.

Uses

thmHeight bounded by radical of contact primes

Used by

claimUniform height bound for ring elements

Sources

PaperOpen

Section: §2.2 Contact primes and ordinary integer witnesses
Page: —
Label: hei:enlarge-exceptions
Line: sections/02-reduction.tex:270

Leannot aligned

Phase 2 aligns this node to a Lean declaration.