carrier_side_obstruction
plain-language theorem explainer
A DefectSensor with nonzero charge cannot have its topological floor covered by the Euler-sampled CostCoveringPackage. Researchers on the pure analytic route to the Riemann hypothesis cite this to show that any nontrivial zero creates an uncovereable obstruction. The proof is a one-line application of the general not_DefectTopologicalFloorCovered theorem.
Claim. Let sensor be a DefectSensor with charge $m ≠ 0$ and real part $σ_0 > 1/2$. Then the Euler-sampled CostCoveringPackage at $σ_0$ fails to satisfy ∀N, annularTopologicalFloor(N, m) ≤ carrierBudgetScale for that package.
background
The AnalyticTrace module assembles an axiom-free RH bridge from the sampled Euler infrastructure. A DefectSensor is a structure recording the multiplicity m (charge) of a zero of ζ and its real part σ₀ > 1/2. The eulerSampledCoveringPackage builds a CostCoveringPackage from the zero-winding certificate, yielding carrier budget zero. DefectTopologicalFloorCovered(pkg, sensor) holds when ∀N, annularTopologicalFloor N sensor.charge ≤ carrierBudgetScale pkg.carrier.
proof idea
The proof is a one-line wrapper that applies the upstream theorem not_DefectTopologicalFloorCovered to the Euler sampled package, the given sensor, and the hypothesis sensor.charge ≠ 0.
why it matters
This theorem isolates the carrier-side obstruction in the analytic route, proving that nonzero charge blocks floor coverage and thereby supports ZeroFreeCriterion and rh_from_zero_free_criterion. It fills the gap left by the eliminated axiom argument_principle_forces_charge_zero, aligning with the Recognition Science goal of deriving the zero-free region from the forcing chain without external hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.