CompositionClosureHypothesis
plain-language theorem explainer
Composition Closure Hypothesis packages the assumption that iterated defects from off-critical zeros remain bounded by a fixed real number B. Researchers working on alternate proofs of the Riemann Hypothesis via cost frameworks would cite this structure when building certificates that derive a contradiction from unbounded growth under the recognition composition law. The declaration is a bare structure definition with no proof obligations.
Claim. Let $B$ be a real number. The hypothesis asserts that for every complex number $ρ$ with Re$(ρ) ≠ 1/2$, and every natural number $n$, the $n$-fold iterated defect of $ρ$ under the recognition composition law satisfies defectIterate(zeroDeviation($ρ$), $n$) ≤ $B$.
background
The module develops an alternate conditional proof of the Riemann Hypothesis by linking the recognition composition law to finite carrier budgets in the cost framework. The defect functional equals $J(x) = (x + x^{-1})/2 - 1$ for positive real $x$, and the composition law states $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$. Iterated application of this law to the initial defect of an off-critical zero produces exponentially growing values, as noted in the module documentation: the composition cascade is theoretically stronger but does not reduce EBBA or HonestPhaseCostBridge.
proof idea
As a structure definition, it directly introduces the fields bound and the reflected predicate without applying any lemmas or tactics. The reflected field encodes the boundedness assumption for all iterates under defectIterate for zeros violating OnCriticalLine.
why it matters
This hypothesis is the key assumption in the composition route to the Riemann Hypothesis. It is instantiated in CompositionRHCertificate and used in rh_from_composition_closure to obtain the contradiction for off-critical zeros. It fills the step between defect amplification under the recognition composition law and the finite carrier budget from the AnnularCost framework. The argument relies on T5 uniqueness of J but leaves open the explicit verification of carrier budget finiteness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.