carrier_defect_comparison_rh
plain-language theorem explainer
The theorem states that for a DefectSensor with nonzero charge m and a matching QuantitativeLocalFactorization of order -m, the realized annular cost of the defect phase family on shared circles around a hypothetical zeta zero is unbounded. Researchers closing the Riemann hypothesis via carrier-defect budget comparisons on the same geometric circles would cite this result. The proof is a direct one-line application of the unbounded defect cost theorem for shared pairs.
Claim. Let $S$ be a defect sensor with nonzero charge $m$ and let $Q$ be a quantitative local factorization satisfying $Q$.order = $-m$. Then the annular cost of the defect phase family on the shared circles constructed from $S$ and $Q$ is not bounded independently of mesh refinement: there is no $K$ such that annularCost(fam.mesh $N$) $≤ K$ for all $N$.
background
DefectSensor is the structure recording a hypothetical zero of zeta at real part in (1/2,1) with multiplicity m (the charge). QuantitativeLocalFactorization supplies a local meromorphic witness plus a uniform bound on the logarithmic derivative of the regular factor, controlling phase perturbations on sampled circles. mkSharedCirclePair builds a SharedCircleFamilyPair that places both the holomorphic carrier family (charge 0, bounded excess) and the meromorphic defect family (charge m) on identical circles of radii r0/(n+1) centered at the zero. RealizedDefectAnnularCostBounded asserts existence of a uniform K such that the annular cost of the sampled defect family remains ≤ K for every refinement depth N. The module sets this comparison as Phase 4a of the RH closure plan: on the same circles the carrier excess stays bounded while the defect topological floor diverges as Θ(m² log N).
proof idea
The proof is a one-line wrapper that applies defect_cost_unbounded_of_shared_pair to the pair constructed by mkSharedCirclePair and the hypothesis that the sensor charge is nonzero.
why it matters
This declaration supplies the concrete carrier-defect comparison for hypothetical zeros required by the module's budget-transfer strategy. It directly instantiates the abstract claim that the defect's topological floor exceeds any finite carrier budget for large enough refinement depth, feeding the contradiction step named carrier_defect_budget_contradiction in the same module. The result sits inside the Recognition Science number-theory layer that prepares the analytic input for the forcing chain (T0-T8) and the Recognition Composition Law; it closes one scaffolding path toward showing that nonzero charge is incompatible with the bounded carrier cost on shared circles.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.