CompositionRHCertificate
plain-language theorem explainer
The CompositionRHCertificate bundles a CompositionClosureHypothesis with the derived claim that no zeros exist off the critical line. Researchers pursuing cost-amplification routes to the Riemann hypothesis would cite this as the terminal certificate in the composition-divergence argument. The proof is a one-line wrapper applying the rh_from_composition_closure lemma to the bundled hypothesis.
Claim. A structure consisting of a CompositionClosureHypothesis together with the assertion that for every complex number ρ, if ρ lies off the critical line then a contradiction follows.
background
The module connects the zero composition law to the Riemann hypothesis by showing that iterated defects from any off-critical zero diverge and violate a finite carrier budget. The CompositionClosureHypothesis asserts that for each nontrivial zero ρ off the critical line the n-th iterate of the RCL self-composition produces a defect bounded by a fixed real number representing the carrier budget scale from the AnnularCost framework. Upstream results supply the defect functional, which equals the J-cost on positive reals, and the cost maps induced by multiplicative recognizers and recognition events.
proof idea
The structure is assembled by supplying a CompositionClosureHypothesis and then defining the zeros_on_line field via the one-line application of rh_from_composition_closure to that hypothesis.
why it matters
This declaration completes the alternate composition route to the Riemann hypothesis. It packages the forcing chain from T5 J-uniqueness through ξ-symmetry equaling J-symmetry, RCL self-composition amplifying defect, and divergence against finite carrier budget. The module positions the certificate as strictly stronger than a single-defect argument because it generates infinitely many cost values from one zero. It leaves open whether the CompositionClosureHypothesis can be discharged without further assumptions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.