analytic_rh
plain-language theorem explainer
The legacy analytic route shows that a defect sensor carrying nonzero charge cannot satisfy the deprecated bounded annular cost condition, yielding an immediate contradiction. Number theorists tracing Recognition Science bridges to the Riemann Hypothesis would cite this for the cost-based inconsistency argument. The proof is a one-line wrapper applying the rh_from_complex_analysis_axioms lemma to the sensor, nonzero-charge hypothesis, and bounded-cost assumption.
Claim. Let $s$ be a defect sensor with charge$(s) ≠ 0$ that satisfies the deprecated bounded annular cost condition. Then a contradiction follows.
background
The AnalyticTrace module assembles an axiom-free interface for the Riemann Hypothesis by linking sampled Euler carriers, contour winding, and floor-coverage criteria to charge data. DefectSensor records a charge value tied to recognition defects, while DeprecatedDefectAnnularCostBounded encodes the now-superseded assumption that annular cost remains bounded for nonzero-charge sensors. The module replaces earlier axioms with derived results such as eulerSampledFloorCovered_iff_charge_zero and contour winding from holomorphy plus nonvanishing.
proof idea
The proof is a one-line wrapper that applies rh_from_complex_analysis_axioms directly to the given sensor, the nonzero-charge hypothesis hm, and the bounded-cost assumption hbounded.
why it matters
This theorem completes the deprecated analytic route inside AnalyticTrace, feeding the direct_rh_from_zero_free_criterion (which targets the ZeroFreeCriterion packaging bounded log-derivative, carrier nonvanishing, and honest phase data) and the rh_chain_summary_legacy. It fills the pure-analytic step described in the module documentation before the preferred ontology route via UnifiedRH.unified_rh. The construction rests on eight-tick phase data and J-cost structures from upstream recognition axioms, though the cost-contradiction path is now marked legacy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.