WitnessedHonestPhaseAdmissibilityBridge
plain-language theorem explainer
The structure encodes that phase-family data arising from any witnessed zeta defect sensor satisfies the honest-phase admissibility predicate, i.e., its realized sampled family has bounded total annular J-cost. Researchers working on the Route C formulation of the Riemann Hypothesis cite this as the narrow carrier-side bridge from witnessed sensors to the charge-zero criterion. The declaration is supplied directly as a structure definition with no internal proof body.
Claim. A structure $B$ such that for every witnessed defect sensor $s$ and every zeta phase family datum $z$, if $z$ is generated from $s$ then the phase family of $z$ has finite recognition budget (bounded total annular $J$-cost).
background
The Honest Phase Admissibility module narrows the analytic Riemann Hypothesis target to honest zeta-derived phase data under Route C. The predicate for honest phase admissibility requires that the realized sampled family has finite recognition budget, equivalently bounded total annular J-cost. A witnessed defect sensor records the full center rho together with the meromorphic-order witness that the charge originates from the reciprocal zeta function itself. The present structure specializes the general admissibility bridge to data produced by such witnessed sensors.
proof idea
The declaration is introduced directly as a structure definition that packages the universal quantification over witnessed sensors and matching phase-family data. No lemmas or tactics are applied inside the definition; it functions as a carrier for the property invoked in downstream equivalence statements.
why it matters
This definition supplies the narrow Route C bridge that connects witnessed honest phase data to the charge-zero conclusion required by the zero-free criterion. It feeds the direct implication from the bridge to the witnessed RH core (zero charge for every sensor) and the equivalence between the bridge and that core. The construction completes the Route C boundary condition that witnessed honest-phase admissibility is equivalent to the witnessed zero-free statement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.