---
id: F-038
title: Two-sided full stopped-product estimate
tier: lean
polarity: positive
depends_on: [F-027, F-037]
supersedes: []
verifier: check_answer/verify-lean-theorem.sh verified_math/F-038_two-sided-full-product-estimate/lean ResearchPNT.FinalEstimate ResearchPNT.exists_two_sided_full_product_estimate
date: 2026-07-11
---

## Statement

There exist positive real constants `c,C` such that, for all sufficiently
large natural `N`,

```text
c · (N/log N) · P_N(log(log N)) ≤ log S(N)
                                ≤ C · (N/log N) · P_N(log(log N)),
```

where `P_N = renewalProduct N` multiplies successive natural logarithms while
the current argument exceeds `exp 3`. By F-028, height `N` is already past the
stopping depth. Thus in conventional notation

```text
log S(N) ≍ (N/log N) ∏_{j≥3, stopped} log_j N.
```

Formal theorem: `ResearchPNT.exists_two_sided_full_product_estimate`.

## Proof / verification

The lower inequality is F-037. The upper inequality is F-027, with the
harmless `N+1` prefactor replaced by at most `2N`. The copied source includes the entire exact combinatorial, clean-PNT,
compatible-prime, adaptive-height, and upper-renewal proof chain. The audited
`PrimeNumberTheoremAnd` source dependency is bundled locally; all remote Lake
packages are revision-pinned, and the verifier bootstraps their signed Mathlib
cache when run in a fresh sandbox. It rejects `sorry`, `admit`, custom axioms,
opaque declarations, and unsafe escapes, then audits this exact closure. The
only axioms are Mathlib's standard `propext`, `Classical.choice`, and
`Quot.sound`.
