phaseFamily_excess_bounded_of_perturbationWitness
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove existence of any perturbation witness.
- Does not bound excess in the absence of the witness hypothesis.
- Applies only to sampled families obtained from defect phase families.
- Does not address global properties of the zeta function itself.
Lean usage
exact phaseFamily_excess_bounded_of_perturbationWitness zfd.phaseFamily hwformal statement (Lean)
174theorem phaseFamily_excess_bounded_of_perturbationWitness
175 (dpf : DefectPhaseFamily) (hw : DefectPhasePerturbationWitness dpf) :
176 RealizedDefectAnnularExcessBounded (dpf.toSampledFamily) := by
proof body
Term-mode proof.
177 exact realizedDefectAnnularExcessBounded_of_ringRegularErrorBound _
178 (ringRegularErrorBound_of_ringPerturbationControl _
179 (phaseFamily_ringPerturbationControl dpf hw))
180
181/-- Specialization to the honest zeta-derived phase package. This makes the
182missing Euler/Hadamard-style upgrade explicit: a perturbation witness for the
183honest phase family is enough to produce bounded annular excess data. -/