honestPhaseFamily_excess_bounded_of_perturbationWitness
plain-language theorem explainer
For zeta phase family data equipped with a defect phase perturbation witness on its phase family, the derived sampled family has annular excess bounded independently of mesh refinement. Number theorists seeking quantitative control on zeta zeros would cite this as the honest-case reduction. The proof is a direct one-line specialization of the general phase-family excess bound.
Claim. Let $zfd$ be zeta phase family data and let $hw$ be a defect phase perturbation witness for the phase family of $zfd$. Then the annular excess of the realized sampled family obtained from $zfd$ is bounded by a constant independent of mesh refinement.
background
The Honest Phase Budget Bridge module supplies the extra analytic input beyond completed-ξ symmetry: a perturbation witness for an actual phase family. RealizedDefectAnnularExcessBounded states that for a defect sampled family there exists $K$ such that annular excess at every mesh $N$ stays at most $K$. The upstream general result records that any defect phase family with a perturbation witness yields bounded annular excess on its sampled version.
proof idea
One-line wrapper that applies phaseFamily_excess_bounded_of_perturbationWitness to the phase family component of the zeta data together with the supplied witness.
why it matters
This specializes the general excess bound to the honest zeta-derived phase package, making the Euler/Hadamard-style upgrade explicit. It shows that a perturbation witness for the honest phase family suffices to produce bounded annular excess data on the sampled side. The module context notes that such control is precisely the quantitative piece needed without claiming to prove the Riemann hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.