rh_from_composition_closure
plain-language theorem explainer
Assuming the Composition Closure Hypothesis, no nontrivial zero of the zeta function lies off the critical line. Researchers seeking alternate conditional routes to the Riemann Hypothesis would cite this result as the divergence step in the RCL forcing chain. The proof obtains a budget violation via composition_violates_budget, invokes the reflected bound from CCH, and closes with linear arithmetic.
Claim. If the Composition Closure Hypothesis holds (every iterated defect of an off-critical zero remains bounded by a finite carrier budget), then for all complex ρ, if ρ is not on the critical line then a contradiction follows.
background
The module establishes an alternate conditional certificate for the Riemann Hypothesis by linking the Recognition Composition Law to zero locations via a finite carrier budget. CompositionClosureHypothesis is the structure with a real bound (the carrier budget scale) and a reflected predicate asserting that for any off-critical ρ and natural n, the n-th defect iterate of zeroDeviation ρ stays ≤ bound. Upstream, the Composition class encodes the RCL axiom: for positive x, y, F(xy) + F(x/y) = 2 F(x) F(y) + 2 F(x) + 2 F(y), which forces J(x) = (x + x^{-1})/2 - 1. The defect functional equals this J on positive reals, and the zero composition law supplies the recurrence d_{n+1} = 2 d_n (d_n + 2) that produces exponential growth.
proof idea
Term-mode proof. Introduce the off-critical ρ and its negation of OnCriticalLine. Apply composition_violates_budget to the reflected bound supplied by cch to obtain a concrete n where the iterated defect exceeds the budget. Use the reflected field of cch to recover the inequality defectIterate ≤ bound at that n. Close the contradiction with linarith.
why it matters
This theorem supplies the final contradiction step inside CompositionRHCertificate, which packages the full RCL-to-RH chain: T5 uniqueness of J, XiJBridge symmetry, ZeroCompositionLaw amplification of defect, and finite carrier budget. It fills the divergence-to-budget link in the module's forcing chain and stands as an independent conditional certificate alongside the EBBA route. The result touches the open question of whether the Composition Closure Hypothesis itself can be discharged from the AnnularCost axioms without additional scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.