rh_chain_summary_legacy
plain-language theorem explainer
The legacy summary shows that assuming every defect sensor with nonzero charge satisfies the deprecated bounded annular cost condition forces a contradiction, hence no such sensors can exist. Researchers comparing analytic and ontology routes to the Riemann hypothesis would cite it when auditing the deprecated path. The proof is a one-line term application of the analytic_rh lemma to the supplied boundedness hypothesis.
Claim. If every defect sensor with nonzero charge satisfies the deprecated bounded annular cost condition, then for every defect sensor, nonzero charge yields a contradiction.
background
The AnalyticTrace module assembles an axiom-free RH bridge from sampled Euler carriers, contour winding, and honest phase data. DefectSensor abstracts a detector of topological charge in the trace; charge nonzero signals a potential zero of zeta. DeprecatedDefectAnnularCostBounded encodes the inconsistent cost bound on annular regions around such defects. The module eliminates prior axioms by deriving zero winding from holomorphy plus nonvanishing and by proving floor coverage iff charge equals zero via eulerSampledFloorCovered_iff_charge_zero. Local setting contrasts the ontology route (external EulerBoundaryBridgeAssumption) with the pure analytic route targeting ZeroFreeCriterion from witnessed phase families.
proof idea
The proof is a one-line term-mode wrapper. It receives the universal boundedness hypothesis, instantiates it on the given sensor and nonzero-charge witness, then feeds the resulting boundedness fact directly into analytic_rh to obtain the contradiction.
why it matters
This legacy summary closes the deprecated analytic chain and feeds direct_rh_from_zero_free_criterion, which targets the zero-free criterion for witnessed sensors. It underscores the inconsistency of the defect_annular_cost_bounded marker and directs attention to unified_rh or direct_rh_from_honestPhaseCostBridge. Within Recognition Science it marks the boundary between the analytic trace infrastructure and the full RH-equivalence claim, consistent with the module's elimination of former axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.