HonestPhaseCostBridge
plain-language theorem explainer
HonestPhaseCostBridge defines a structure requiring that any witnessed defect sensor for zeta reciprocal, when matched to zeta phase family data, produces a sampled family with annular cost bounded independently of mesh refinement. Researchers pursuing the pure analytic route to the Riemann hypothesis cite it as the remaining link after zero-winding and floor-coverage results. The declaration is introduced as a structure definition with one field stating the bounded-cost implication.
Claim. A structure asserting: for every witnessed defect sensor $S$ (center $ρ$ with $1/2 < ρ.re < 1$ and meromorphic order witness for $ζ^{-1}$ at $ρ$) and every zeta phase family data $F$ satisfying $F$.sensor = $S$.toDefectSensor, the sampled family from $F$ satisfies RealizedDefectAnnularCostBounded, i.e., there exists $K$ such that annularCost of the mesh at every refinement level is at most $K$.
background
The Analytic Trace module assembles an axiom-free interface for the Riemann hypothesis via sampled Euler data, eliminating prior axioms on winding and argument principle. WitnessedDefectSensor augments the basic defect sensor by recording the explicit center $ρ$ and the meromorphic order statement meromorphicOrderAt zetaReciprocal $ρ$ = -charge. RealizedDefectAnnularCostBounded asserts existence of a uniform $K$ such that annularCost(fam.mesh $N$) ≤ $K$ for all $N$, replacing quantification over arbitrary meshes. Upstream results include the 8-tick phase definition (periodic with period $2π$), cost as J-cost of recognition events, and the classical bridge packaging model, defect meaning, and energy gap.
proof idea
This declaration is a structure definition that directly encodes the bounded annular cost property for honest phase families. No lemmas are applied and no tactics are used; the single field is the statement itself.
why it matters
This structure is the central object in the analytic route, feeding directly into charge_zero_of_honest_phase_of_costBridge, direct_rh_from_honestPhaseCostBridge, and the equivalence HonestPhaseCostBridge_iff_rh. It completes the honest-phase cost bridge described in the module doc-comment, where bounded annular cost plus the general defect-cost theorem forces zero charge. It touches the open question of realizing the bounded-cost property without assuming the Riemann hypothesis, as the ontology route via EulerBoundaryBridgeAssumption supplies it immediately.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.