DefectBudget
DefectBudget packages a positive real total_defect bounded by 1 as the normalized sum of J-costs over a configuration. Researchers on the Recognition Science zeta program would cite it when linking accumulated defect to a zero-free region sufficient for the RS chain. It is introduced directly as a structure definition whose three fields encode positivity and the unit normalization.
claimA DefectBudget is a real number $d$ satisfying $0 < d ≤ 1$, where $d$ is the total defect of a configuration.
background
The Weak Zero-Free Region module examines whether the defect-budget bridge can weaken or replace the full RH axiom. Total defect is the sum of individual J-costs (LawOfExistence.defect) over the entries of a configuration, and is non-negative by construction. The normalized sequence from RunningMaxNormalization supplies the unit bound used in the defect_bounded field. The module contrasts the classical Vinogradov-Korobov zero-free region with the weaker Hadamard-de la Vallée Poussin form σ > 1 - c/log(t) that the RS chain actually requires.
proof idea
The declaration is a structure definition that introduces the three fields total_defect, defect_positive, and defect_bounded with no proof steps or tactics.
why it matters in Recognition Science
DefectBudget is the input type for defect_implies_zero_free, which extracts the positive constant c = total_defect to produce the required zero-free region. It is also a field of RSChainRequirements and WeakZFRCert, closing the defect-to-zeta bridge that addresses the module's Q14 question. The structure therefore supplies the concrete hypothesis that may allow the RS chain to avoid assuming the full Riemann Hypothesis.
scope and limits
- Does not prove existence of any configuration attaining a positive defect.
- Does not derive the zero-free region; that step occurs in a separate theorem.
- Does not claim the stronger Vinogradov-Korobov zero-free region.
- Does not specify the dimension or type of the underlying configuration.
formal statement (Lean)
63structure DefectBudget where
64 total_defect : ℝ
65 defect_positive : 0 < total_defect
66 defect_bounded : total_defect ≤ 1 -- normalized
67