Downstream dependency report: an audited bridge project pinned to v1.0, plus an arithmetic-interface experiment over the §5 prime side

[tracyphasespace]

We have built a Lean 4 subproject that requires this repository at tag
v1.0 (tag object 82ee6340, commit 3635e748, Mathlib pin 51e6992e,
toolchain leanprover/lean4:v4.33.0-rc2) and wanted to (a) report it as a
downstream dependency, and (b) share one result of independent interest to
this repo's authors.

What the project is. 88 kernel-checked theorems (no sorry; every
declaration verified on [propext, Classical.choice, Quot.sound] by an
enforced audit script with a declared-vs-audited count assertion, run in CI).
The mathematical content is a dependency experiment over the paper's §5:

Does the prime side read the von Mangoldt coefficients only through a small
explicit interface?

We defined a five-condition predicate EulerStiffness f (prime-power
support; nonnegativity; f(n) ≤ log n; the Mertens second moment
Σ f(n)²/n = ½log²x + O(log x); a Chebyshev bound Σ f(n) ≤ Cx) and proved,
from those conditions alone — no ζ, no Euler product:

• the real-cutoff integrated second moment in the literal statement shape of
  Zeta23.ChebyshevMertens.cheb2b;
• the log-damped √-moment in the shape of cheb1c;
• an assembly theorem producing your Zeta23.ChebyshevMertens structure
  itself, with five of the six fields interface-derived. The one residue
  is cheb1b: its hardcoded 3√x is sharper than our interface's Chebyshev
  constant supplies (we reach 2(√2+1)(log 4 + 4)), so it enters as an
  explicit hypothesis, dischargeable by your own Chebyshev.lean proof.

Two side results that may interest you: the interface is phase-blind by
construction (a complex version defined as stiffness of the modulus), and it
is stable under finite Euler-factor deletion — so every Dirichlet character
twist χ(n)Λ(n) (any modulus, primitivity not needed) inhabits it, with
defect constant Σ_{p|q} log²p/(p−1). The Davenport–Heilbronn counterexample
is excluded by an exact defect identity at n = 6, which we use as a
standing negative control.

We claim nothing about the analytic side: the completed-function package,
window analysis, and the rank–trace mechanism are consumed as-is from your
formalization. The experiment record states explicitly what is
kernel-verified and what remains an identification-level audit claim.

Repo: https://github.com/tracyphasespace/riemann-lean (subproject
Zeta23Bridge/; experiment record Zeta23Bridge/Factorization.md; audit
Zeta23Bridge/audit.sh).

One request: if a future retag or force-move of v1.0 is ever
contemplated, we'd appreciate a heads-up in this thread, since our lakefile
pins the tag.

Thanks for publishing the formalization — the statement-level honesty of the
Hypotheses.lean interfaces is what made an external dependency audit of
this kind possible within days of release.

[mesito]

Subject: Prior-art / citation request: Davenport–Heilbronn negative control and the n=6 Euler-support defect

Dear authors,

I am writing to point out a close and unusually specific overlap between the arithmetic-interface / Davenport–Heilbronn analysis being developed around the recent zeta formalization work and two of my publicly available July 2026 papers.

In particular, the overlapping ingredients include:

• Davenport–Heilbronn as a negative-control object;
• prime-power support as an Euler-specific arithmetic discriminator;
• the exact defect at n = 6;
• the closed-form factor (1 + κ²) log 6;
• the distinction between magnitude/modulus information and arithmetic support/sign information.

These ingredients appeared earlier in my papers:

1. Mesut Ismail,
   “THE DAVENPORT–HEILBRONN FUNCTION AS A NEGATIVE CONTROL:
   WEIL WITNESSES, AN OBSTRUCTION TO SPECTRAL-TRIPLE CONVERGENCE,
   AND THE INDEX STAIRCASE”
   Date: July 19, 2026
   DOI: 10.5281/zenodo.21445832
   ResearchGate:
   https://www.researchgate.net/publication/410698893_THE_DAVENPORT-HEILBRONN_FUNCTION_AS_A_NEGATIVE_CONTROL_WEIL_WITNESSES_AN_OBSTRUCTION_TO_SPECTRAL-TRIPLE_CONVERGENCE_AND_THE_INDEX_STAIRCASE

In this paper I use the Davenport–Heilbronn function explicitly as a negative control and identify Euler-specific coefficient obstructions, including

c_6 = (1 + κ²) log 6,

together with prime-power-support, sign, and O(log n) violations.

2. Mesut Ismail,
   “AN INTERFERENCE-CHANNEL LOCALIZATION OF OFF-LINE ZEROS
   AND A COEFFICIENT TEST FOR THE EULER PRODUCT”
   Date: July 22, 2026
   DOI: 10.5281/zenodo.21443732
   ResearchGate:
   https://www.researchgate.net/publication/410699224_AN_INTERFERENCE-CHANNEL_LOCALIZATION_OF_OFF-LINE_ZEROS_AND_A_COEFFICIENT_TEST_FOR_THE_EULER_PRODUCT

In that paper I prove an Euler-product / prime-power-support equivalence for the logarithmic-derivative coefficients, again use the exact Davenport–Heilbronn witness

c_6 = (1 + κ²) log 6,

and formulate the Euler distinction as one of support and sign that is invisible to magnitude.

I am not assuming causal influence, and independent convergence is entirely possible. However, the combination of these specific ingredients is sufficiently close that I believe these papers constitute relevant prior art for any discussion using the Davenport–Heilbronn n = 6 defect, prime-power support, and magnitude/modulus blindness as an Euler-specific diagnostic.

Could you please review these papers and, if you agree that the overlap is relevant, cite or acknowledge them in the corresponding documentation and in any planned external note or paper?

I would also be very interested in a technical comparison of the two formulations, especially the relationship between a modulus/phase-blind arithmetic interface and my support/sign criterion for detecting the Euler product.

For clarity, my request concerns scholarly attribution and priority for this specific Davenport–Heilbronn coefficient diagnostic and its use as an Euler-specific negative control. I am not claiming priority for the general use of Davenport–Heilbronn functions, Euler products, or Weil-type methods.

Best regards,

Mesut Ismail
Technical University of Sofia
ORCID: 0009-0001-0496-964X
email: mesutismail1977@gmail.com

[mesito]

Follow-up for the record: the material I referred to is in the downstream
tracyphasespace/riemann-lean bridge project, not in this repository or in the
accompanying paper. I have moved the request there —
tracyphasespace/riemann-lean#1 — and this comment
needs no action from the authors here. Apologies for the misdirection.