# Exact angle bounds from the independent T260 census

The independent MPFR Rouché receipt isolates exactly one zero in each of
179 disjoint squares of half-width \(10^{-7}\). The exact-rational
checker [`sharpen_angle.py`](sharpen_angle.py) takes those squares as
premises and writes [`sharp_angle_receipt.json`](sharp_angle_receipt.json).
It uses no floating-point operations for its decisive comparisons.

For \(s=\sigma+it\), put \(u=|1-2\sigma|\). On every certified square,
\(t>5\), \(u<2\), and

\[
\left|\tan\arg(s(1-s))\right|
=\frac{tu}{t^2+(1-u^2)/4}=:R(u,t).
\]

The denominator is positive. Direct differentiation shows \(R\)
increases in \(u\) and decreases in \(t\), so its exact extrema lie at
the outward/lower and inward/upper square corners. For a square crossing
the critical line, the lower value is zero. The maximum upper ratio is
at the east box numbered 170 (equally at its reflected west box 171),
near \(t=85.6993484854\).

The alternating series bounds
\(v-v^3/3<\arctan v<v-v^3/3+v^5/5\) for \(0<v<1\).
Applied to the 179 exact corner ratios, these give

\[
\max_{t<260}|\arg(s(1-s))|
 <0.007199715150701273<0.007199716.
\]

The zero isolated in box 170 also forces the lower bound
\(|\arg(s(1-s))|>0.007199710462770206\). A rational enclosure of
\(\pi\) from Machin's identity and alternating arctangent sums then
gives the strict exact comparisons

\[
436\,(\text{uniform upper angle}) < \pi,
\qquad 438\,(\text{box-170 lower angle}) > \pi.
\]

The first left side is less than 3.139075806; the second exceeds
3.153473182. Thus the uniform angle-sector proof covers rung 218, but
its condition \(2k\theta<\pi\) is impossible at rung 219 even if that
exceptional zero were localized arbitrarily tightly. This says nothing
about the sign of rung 219; an \(x\)-dependent or compensating-term
argument can go further.

## Replay and source hashes

From the shared workspace, run:

```text
python work/next_census/sharpen_angle.py
```

When the checker is packaged beside `independent_mpfr`, run from the
packaged `pp296` directory:

```text
python sharp_angle/sharpen_angle.py
```

It selects the sibling `independent_mpfr` evidence when present, then
falls back to the sibling `independent_zero_eval` development evidence.
The receipt is written beside the checker in either layout.

The receipt records the exact rational corner bounds for every square,
both exact Machin \(\pi\) bounds, the strict inequality results, and
SHA-256 hashes of its inputs and source. This frozen run used:

```text
sharpen_angle.py            7b101d0bb77dca3db1bed842edfa9ff1382c506107d13fc7529210212cc45b95
census_boxes_receipt.json   d5a4fb84346cfdcbbec7873c289b86e55d11fa028a146e648885ddeeb3506585
certify_census_boxes.py     bc0cde495f806e4d6eb62d357856c769541f9f84bf03a0258249db1b645e8c49
mpfr_em.py                  0b2c160bed6410ddfe6f101f2216c8383f74e5ae3dd4e23899eaca9c1a002ed4
sharp_angle_receipt.json    a579f527a6bdc21514c7f7a4b21398c96cdfd738a21fc9970ee4f4d035d7405b
```

Recompute the hashes with `Get-FileHash -Algorithm SHA256` on Windows or
`sha256sum` elsewhere, then compare the receipt's `source_sha256` map
and the frozen receipt hash above. The receipt depends on the prior
MPFR zero-isolation certificate; it does not independently re-evaluate
the Davenport–Heilbronn function.