defect_implies_zero_free
plain-language theorem explainer
defect_implies_zero_free shows that any DefectBudget with positive total defect supplies a constant c > 0 such that c / log t > 0 for all t > 1. Researchers replacing the full Riemann Hypothesis with a defect-budget hypothesis in the RS zeta program would cite this step. The proof is a direct term-mode wrapper that substitutes the total_defect field and invokes positivity of the real logarithm.
Claim. Let $D$ be a defect budget whose total defect satisfies $0 < c$. Then there exists a positive real constant $c$ such that $c / {log} t > 0$ for every real $t > 1$.
background
The Weak Zero-Free Region module examines whether the Recognition Science zeta program can operate with the classical Hadamard-de la Vallée Poussin zero-free region rather than the full Riemann Hypothesis. A DefectBudget packages a normalized total defect together with a proof that the defect is strictly positive. The total_defect value itself arises as the sum of individual J-costs over a finite configuration, as defined in the upstream InitialCondition module.
proof idea
The proof is a one-line term wrapper. It instantiates the existential witness with the total_defect field of the input DefectBudget. The positivity conjunct is taken directly from the defect_positive field, while the universal statement over t follows from the built-in fact that the real logarithm is positive for arguments greater than 1.
why it matters
This theorem supplies the defect-to-bound implication required by weak_zfr_cert_exists, which packages both the classical existence result and the defect-derived zero-free region into a single certificate. It supports the module claim that the RS chain needs only the classical zero-free region of width c / log t. In the broader framework the step reduces the number-theoretic axiom load while remaining compatible with the J-uniqueness and phi-ladder constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.