Registry · Proposition III.P23 tau-effective formalized

III.P23 — Polynomial Refinement

Per-prime witness space |W(x, p_i)| ≤ p_i. Total refined search: O(∑ p_i) = O(k² log k) by PNT. Exponential product space collapses to polynomial sum.

Book III Part 9 Ch. 57

Dependency Graph

Depends on (2)

III.P22 III.D55

Depended on by (1)

III.T33

Lean Formalization

Module: TauLib.BookIII.Computation.WitnessSearch

Symbol: polynomial_refinement_check