RSChainRequirements
plain-language theorem explainer
RSChainRequirements packages the analytic conditions needed to close the Recognition Science forcing chain from defect budget to prime distribution without the full Riemann Hypothesis. Number theorists working on the RS zeta program would cite this structure when checking that a classical zero-free region plus bounded defect suffices for the explicit formula and prime counting. The definition is a direct record that composes the ZeroFreeRegion and DefectBudget structures with two placeholder propositions.
Claim. A structure consisting of a zero-free region (a function $width: ℝ → ℝ$ giving the width of the strip free of zeta zeros at height $t$, with $width(t) > 0$ for $t > 1$ and $width$ monotonically decreasing), the proposition that the prime counting function satisfies $π(x) ∼ x / ln(x)$, the proposition that an explicit formula relates the zeta zeros to the primes, and a defect budget (a real $d$ satisfying $0 < d ≤ 1$).
background
The module WeakZeroFreeRegion examines whether the Riemann Hypothesis conditional axiom can be eliminated or weakened in the Recognition Science framework. It relies on the defect-budget bridge: the J-cost functional on the recognition ledger constrains zeta zero distribution, forcing a zero-free region of the form σ > 1 − c/log(t), which matches the classical Hadamard-de la Vallée Poussin result and suffices for the RS chain.
proof idea
This declaration is a structure definition with no proof body. It directly assembles the upstream ZeroFreeRegion structure (width function with positivity and decrease) and DefectBudget structure (positive normalized total defect) together with two propositional fields for the prime counting asymptotic and explicit formula connection.
why it matters
RSChainRequirements supplies the interface that lets the Recognition Science chain advance from defect budget to prime distribution without the full Riemann Hypothesis. It specifies the minimal zero-free region and defect constraints required for the explicit formula to link zeros to primes, as described in the module discussion of the RS zeta program. The structure touches the open question of removing the RH axiom entirely while preserving the classical zero-free region.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.