honestPhaseFamily_perturbationWitness
plain-language theorem explainer
The definition extracts the canonical zero-perturbation witness already attached to any zeta-derived phase family data. Researchers bridging meromorphic phase families to sampled annular excess bounds cite it when converting honest analytic input into bounded defect data. The implementation is a direct field projection from the input structure.
Claim. Let $zfd$ be zeta-derived phase family data. The honest phase family perturbation witness is the defect phase perturbation witness attached to the phase family component of $zfd$.
background
The module packages extra analytic input beyond pure completed-ξ symmetry: a perturbation witness for an actual phase family. Such a witness supplies the Euler/Hadamard-style quantitative control needed to turn an honest phase family into bounded annular excess data on the sampled side, without proving RH by itself. ZetaPhaseFamilyData records phase samples taken from the Weierstrass factorization of zetaReciprocal near a hypothetical zero, storing a sensor, quantitative local factorization witness, and the underlying DefectPhaseFamily. DefectPhasePerturbationWitness is the structure that holds the epsilon increments splitting each sampled phase increment into pure winding plus regular perturbation, together with the smallness bounds on those perturbations. Upstream, EightTick.phase supplies the 8-tick phases $kπ/4$ for $k=0..7$ used in the phase sampling.
proof idea
The definition is a one-line wrapper that returns the perturbationWitness field of the supplied ZetaPhaseFamilyData record.
why it matters
This definition closes the honest phase budget bridge by exposing the canonical witness for downstream excess-boundedness results. It directly feeds the sibling declarations honestPhaseFamily_excess_bounded_of_perturbationWitness and honestPhaseFamily_excess_zero. In the Recognition framework it supplies the quantitative control (T7 eight-tick octave, phase sampling) required to convert zeta-derived phase families into bounded defect data on the sampled side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.