phaseFamily_excess_bounded_of_perturbationWitness
plain-language theorem explainer
A perturbation witness for a defect phase family implies bounded annular excess on its sampled realization. Researchers bridging analytic number theory to physical phase budgets would cite this when converting phase control into excess bounds. The proof is a one-line term composition of ring perturbation control with the annular excess bound lemma.
Claim. Let $dpf$ be a defect phase family and $hw$ a perturbation witness for $dpf$. Then the realized defect annular excess of the sampled family attached to $dpf$ is bounded.
background
The Honest Phase Budget Bridge module supplies quantitative analytic input beyond completed-ξ symmetry. A DefectPhaseFamily encodes a phase family derived from defects, while DefectPhasePerturbationWitness records the ring-regular error control on that family. RealizedDefectAnnularExcessBounded asserts that the annular excess of the sampled version remains bounded. The local setting is the conversion of an honest phase package into bounded excess data on the sampled side, as described in the module doc-comment. Upstream results include the eight-tick phase definition and the ring perturbation control construction in DefectSampledTrace.
proof idea
One-line wrapper that applies realizedDefectAnnularExcessBounded_of_ringRegularErrorBound to the output of ringRegularErrorBound_of_ringPerturbationControl, which is itself obtained from phaseFamily_ringPerturbationControl dpf hw.
why it matters
This theorem is invoked by honestPhaseFamily_excess_bounded_of_perturbationWitness and mkSharedCirclePair_carrier_excess_bounded. It supplies the Euler/Hadamard-style upgrade that turns a perturbation witness into bounded annular excess data, closing a step in the phase budget bridge. The result sits downstream of the eight-tick phase construction and feeds the carrier budget comparison, touching the open question of exhibiting explicit witnesses for zeta-derived families.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.