defect_bounded_impossible
plain-language theorem explainer
A defect sensor with nonzero charge cannot have its canonical sampled family realize a bounded annular cost. Number theorists building conditional Riemann hypothesis proofs from cost-covering axioms cite this when the Euler product supplies a concrete carrier. The tactic proof is a one-line wrapper that specializes the canonical family and applies the negation of the bounded-cost lemma.
Claim. Let $S$ be a defect sensor with nonzero charge. If the realized annular cost of the canonical defect-sampled family of $S$ is bounded, then a contradiction follows.
background
The module instantiates the abstract RS carrier and sensor framework with the Euler product of the zeta function. Abstract annular cost and cost-covering axioms from AnnularCost and CostCoveringBridge become concrete once the prime zeta sums define a Hilbert-Schmidt operator $A(s)$ whose determinant $C(s)$ is holomorphic and nonvanishing for Re$(s)>1/2$. The defect functional is the J-cost from LawOfExistence, and the sensor records a charge that must vanish under bounded cost along the canonical trace.
proof idea
The proof lets fam be the canonicalDefectSampledFamily of the given sensor and charge hypothesis, uses simpa to recover that fam.sensor.charge is nonzero, and applies not_realizedDefectAnnularCostBounded directly to reach False.
why it matters
This theorem supplies the conditional floor-covering step that lets the Euler carrier satisfy the cost-covering axiom, thereby feeding the path to conditional RH via carrier nonvanishing on Re$(s)>1/2$. It sits inside the three-layer instantiation chain (abstract cost, bridge, Euler concrete) and closes the nonzero-charge impossibility under bounded defect cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.