D-075 — The three zero-counting perimeter Props derived from published explicit bounds (Paper A, Appendix C)

Date: 2026-09-01 | Session: 045 | Status: COMPLETE (derivations written into paperA.tex Appendix C; grid-checked by E-035, ALL CHECKS PASS) Trigger: expert-review suggestion 5 ("the three derived zero-count bounds are the soft spot of the trust boundary — include their derivations in an appendix so a referee need not trust the archive"). Evidence: E-035 (research/numerics/scripts/E-035-zero-count-perimeter-derivations.py).

1. What is derived

The three Lean perimeter hypotheses (LiContour.lean; majorants LiSkeleton.lean), all counts with multiplicity:

• (A) ZeroCountGlobalProp: N(T) ≤ FAlt(T) := T log T/(2π) + 0.137 log T
• 0.443 log log T + 2.463, T ≥ 2.
• (B) ZeroCountProp: #{t ≤ γ ≤ t+1} ≤ C0hat(t+1), C0hat(s) := 0.433 log(s+2) + 0.886 log log(s+2) + 2.9, t ≥ 2.
• (C) ZeroCountProp2: #{|γ − t| ≤ 1} ≤ Z2hat(t) := 0.6 log(t+2) + 0.886 log log(t+2) + 2.7, t ≥ 10.

The authoritative text is paperA.tex Appendix C (session 045); this file is the archive pointer + the findings that are NOT in the paper.

2. Inputs (as used in the paper)

(R1) Rosser 1941 Thm 19, T ≥ 1467: |N − P| ≤ R := 0.137 log T + 0.443 log log T + 1.588, P(T) = (T/2π) log(T/2πe) + 7/8. Reading ambiguity: Trudgian-II Table 1 records the constants as a bound on |S(T)| with T₀ = 1467; Hasanalizade–Shen–Wong 2022 Table 1 records them in the N-form (7/8 absorbed: 2.463) with T₀ = 2. The two forms differ by the theta remainder r(T) with |r| ≤ 0.2/T (Trudgian-II Cor. 1), so the paper uses only |N − P| ≤ R + 0.2/T for T ≥ 1467 — valid under either reading. (R2) Trudgian-II (1.2): |S(T)| ≤ 2 for T ≤ 6.8·10⁶. (R3) Trudgian-II Cor. 1 remainder: |r(T)| ≤ 0.2/T, T ≥ e. (R4) Trudgian-II Thm 1, PUBLISHED constants: |S| ≤ 0.112 log T + 0.278 log log T + 2.510, T ≥ e (arXiv v2 prints 0.111/0.275/2.450; the larger published constants are used; HSW Table 1 corroborates 0.1120/0.2780/ 3.3850 = 2.510 + 7/8). (R5) γ₁ = 14.1347 (Gram 1903) ⟹ N(T) = 0 for T < 14.

Window bound (W): #{T₁ ≤ γ ≤ T₂} ≤ (T₂ − T₁)·(1/2π) log(T₂/2π) + β(T₁) + β(T₂) + 0.2/T₁ + 0.2/T₂ (P′ increasing; one-sided limits at ordinates controlled by continuity of the majorants).

3. Findings (beyond the paper text)

1. (B) is NOT Rosser-derivable for all t. The two-endpoint Rosser bound has log-coefficient 1/(2π) + 2·0.137 = 0.433155 > 0.433 (the declared coefficient); the slack 0.01623 − 0.000155 log u is positive only for log u ≤ 106.6 (E-035 locates the sign change at log u = 106.57, u ≈ 1.9×10⁴⁶). The Prop is TRUE for all t — Trudgian Thm 1 gives it for u ≥ 10⁸ (slack 0.052 at 10⁸, increasing) — but the honest attribution is "Rosser and Trudgian". This matters because LiSqueeze (the Schwarz squeeze for partialFraction_identity) consumes ZeroCountProp on γ-gap circles of radius → ∞, so the universally quantified statement is genuinely used, not just its restriction to t ≤ 3×10¹². - Consequence for the paper: abstract / intro / App. B now say "Rosser and Trudgian"; App. C (B) has three regimes ((1.2) below 1467, Rosser on [1468, 10⁸], Trudgian Thm 1 on [10⁸, ∞)). - NOT changed: the Lean statement (a slightly larger coefficient, e.g. 0.434, would make it Rosser-only, but the development is closed and the statement is true as declared).
2. (A) and (C) are Rosser + (1.2)-derivable for all heights in range: (A) slack ≥ 0.4517·T (Rosser range), ≥ 6.69 (low range), F(2) = 2.616 > 0 with F increasing; (C) coefficient 0.59231 < 0.6 (slack ≥ 0.166 at t = 1468; ≥ 0.78 low range).
3. The enlarged-majorant cost quoted in the paper ("≈ 0.9√n") was the 2F-era figure: FAlt − (P + R) = (T/2π)(1 + log 2π) = 0.4517·T, so the cost in B(n) is 0.9√n per 2 units of bridge factor, i.e. ≈ 1.8√n in the final 4F form (the 256 trail entry at n = 8·10⁴ is 2·0.4517·284). Corrected in the Step-4 footnote and App. B.
4. Rosser's threshold: the primary source (Amer. J. Math. 63, JSTOR) and Rosser–Schoenfeld 1962 (Project Euclid) could not be fetched from this environment; the conservative 1467 is used and the range below is covered by (R2), so the ambiguity is immaterial to the paper.

4. E-035 summary (dps 60, widths passed exactly)

Gotcha banked: at T ~ 10³¹ and beyond, T₂ − T₁ computed in floating point (dps 30) loses the unit width and produced spurious FAILs on the first run; pass widths exactly (and use dps 60).