honestPhaseFamily_excess_bounded
plain-language theorem explainer
honestPhaseFamily_excess_bounded proves that zeta phase family data yields a sampled family with bounded realized defect annular excess. Analysts closing Route C in phase-based approaches to the Riemann hypothesis cite the result to lock down the excess-control step. The proof is a term-mode reduction that exhibits the bound zero and rewrites the excess at every scale via the zero-excess theorem for the same data.
Claim. For any zeta phase family data $z$, the sampled family obtained from its phase family satisfies bounded realized defect annular excess.
background
The Honest Phase Budget Bridge module packages a perturbation witness that converts an honest phase family into bounded annular excess data on the sampled side. This input lies beyond completed-ξ symmetry and supplies the quantitative control needed to produce bounded excess on the defect-sampled trace. RealizedDefectAnnularExcessBounded is the property that the annular excess of the realized defect family remains bounded at every scale. The upstream theorem honestPhaseFamily_excess_zero shows the excess is identically zero for the honest package, which immediately yields the boundedness claim.
proof idea
The term proof refines the goal to the pair consisting of the explicit bound 0 together with a universal quantifier over scales N. For each N it rewrites the excess expression by direct appeal to the zero-excess theorem honestPhaseFamily_excess_zero applied to the given zeta phase family data.
why it matters
The result supplies the bounded-excess half of the Route C bottleneck recorded in honestPhase_routeC_bottleneck. It is invoked inside HonestPhaseCostBridge_of_rh to obtain bounded cost from the assumption that every witnessed sensor has charge zero. The remaining open step is the upgrade from bounded excess to the zero-charge equivalence required by AnalyticTrace.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.