# PIN

- File: `verify.py`
- Pinned sha256:
  `26fdc8a71084ba41e0580a4fe9a6315efbc437f4d3a6707361d2cc3ff6b35db2`
- Experiment runner:
  `experiments/axler_compact_pi_denominator_44053/verify.py`
- Experiment runner sha256:
  `3f5b0fe5ae53428a657c5d3e0c0c06c38c8b2230796e31ee3285893e5a3d03fe`
- Retained scout runner sha256:
  `b3feb2d04ec4b0e082c31ff6eec24bbb5ed7974b14d374b7d1ef4d7ee57f8929`
- Record: C-0055 (claim; Axler compact prime-counting denominator
  coefficient 44.053)
- Deps: Python 3.14, `python-flint`/Arb, and the frozen project
  environment.
- Run:
  `uv run --frozen python canon/witnesses/C-0055/verify.py`
  from the repository root.
- Verified: 2026-07-19.

Pinned verifier dependency:

- C-0050 verifier:
  `93b011a137d3ee8b88301e1600c8c9c2f8816e143b1712b4fb17059f337b3c6e`.
  C-0055 checks this hash before importing the independently
  source-checked 164-row FKS Table 4 transcript and rational
  logarithmic-integral remainder.

Primary-source hashes:

- Axler, Integers **24** (2024), paper A34, PDF:
  `c093bd507a7e130d1c28ebe8a8707d811a39f8c60ba6cc598afc4bc6e2e522f9`.
- Axler journal text:
  `5597897b3fed188cbaee881fb8a0048ecfdcf265edbf2dc1fb69a8787781d50e`.
- Buethe, Mathematics of Computation **87** (2018), PDF:
  `350f96313810ded3e8eaf2af6006b227c8834235e177f49eabb3d43d4931c4d1`.
- Buethe text:
  `584e158d4e4d3dd3aee1242f94ceaed34f8af77527d4974f1d86519a3178c3c2`.
- Fiori--Kadiri--Swidinsky, arXiv `2206.12557v2`, PDF:
  `405e5dcbca6067fa436141b8a08c79b81bc12deca03bfe12d667428c36b50fbb`.
- Fiori--Kadiri--Swidinsky text:
  `9c926ea1ed333e8008c245f8f5bdd87c72fff0eb1647f87d7e02fbf198169edf`.
- C-0051 verifier:
  `a9ca2416786e3349aaf3bc2a32894572bf4a6c3cb1e52c53690621c2e5521874`.

What the verifier checks:

1. the actual published range \(x\geq29.53\), not a substituted
   \(\log x\geq29.53\) range;
2. positivity of both the new and published denominators;
3. a 16384-cell directed Arb cover of
   \(3.385\leq\log x\leq10\);
4. exact differential forcing and denominator residuals for the
   low logarithmic-integral majorant;
5. the high-order rational \(\operatorname{Ei}\) majorant and
   degree-20 monotonicity factor on \(\log x\geq40\);
6. the FKS Table 7 handoff and all 163 intervals induced by the 164
   Table 4 rows;
7. the exact unique active requirement on \([2100,2200]\);
8. the degree-16 asymptotic reserve and C-0051 tail comparison from
   \(\log x=3000\).

Independent reconstruction:

- Script:
  `scratch/adjacent-unconditional--axler-compact-pi-denominator-44-053/independent_check.py`
- sha256:
  `09d654a60ffcacedc093875f35d009501fb925979794ccf2c55dd2cf25dadec7`
- Review:
  `scratch/adjacent-unconditional--axler-compact-pi-denominator-44-053/INDEPENDENT-REVIEW.md`

The independent path parses the FKS source text directly, compares it
to the C-0050 AST literal, recomputes every exact requirement with
`Fraction`, reconstructs all polynomial identities with SymPy, and
performs an 80-digit mpmath low-range scout.
