defect_implies_zero_free
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.
claimLet $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 in Recognition Science
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.
formal statement (Lean)
68theorem defect_implies_zero_free (db : DefectBudget) :
69 ∃ c : ℝ, 0 < c ∧ ∀ t, 1 < t → c / Real.log t > 0 := by
proof body
Term-mode proof.
70 use db.total_defect
71 exact ⟨db.defect_positive, fun t ht => div_pos db.defect_positive (Real.log_pos ht)⟩
72
73/-! ## RS Chain Sufficiency
74
75The RS number theory chain needs only the classical zero-free region,
76not the full Riemann Hypothesis. -/
77