DeprecatedDefectAnnularCostBounded
plain-language theorem explainer
DeprecatedDefectAnnularCostBounded encodes the assumption that annular costs remain uniformly bounded for the canonical sampled family of any nonzero-charge defect sensor. Legacy proofs of the Riemann hypothesis in the analytic trace module cite this property to derive conditional results. The definition is a direct existential statement over a real bound K that works for all mesh levels N.
Claim. Let $S$ be a defect sensor with nonzero charge. The property holds if there exists a real $K$ such that for every natural number $N$, the annular cost of the level-$N$ mesh of the canonical sampled family generated by $S$ is at most $K$.
background
The EulerInstantiation module instantiates the RS cost structure via the Euler product of zeta, building on AnnularCost for the abstract framework and CostCoveringBridge for carrier axioms that yield conditional RH. DefectSampledTrace supplies canonicalDefectSampledFamily, which constructs a sampled mesh family from a DefectSensor. The underlying cost traces to J-cost in ObserverForcing and derivedCost in MultiplicativeRecognizerL4; Constants.K supplies the dimensionless bridge ratio phi to the power 1/2.
proof idea
Direct definition packaging the statement exists K in reals, for all N in naturals, annularCost of the mesh at N of the canonical family is at most K. No lemmas or tactics are invoked; the body is the primitive existential quantifier.
why it matters
This definition supplies the hypothesis for the deprecated analytic route, appearing as input to analytic_rh, rh_chain_summary_legacy, rh_from_complex_analysis_axioms, and rh_no_zeros_in_strip. Those theorems derive False via defect_annular_cost_bounded_inconsistent, which contradicts the proved unboundedness result not_realizedDefectAnnularCostBounded. It closes the legacy path in favor of unified_rh or direct zero-free criteria and marks the boundary between consistent and inconsistent cost axioms in the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.