pith. machine review for the scientific record. sign in
theorem proved term proof high

composition_violates_budget

show as:
view Lean formalization →

Off-critical zeros of the zeta function generate an unbounded sequence of iterated defects under the composition law. Researchers pursuing alternate conditional proofs of the Riemann Hypothesis via Recognition Science cite this result. The proof is a one-line wrapper applying the zero composition divergence lemma to the given zero and bound.

claimLet $ρ ∈ ℂ$ with Re$(ρ) ≠ 1/2$. For any real $B$, there exists $n ∈ ℕ$ such that the $n$-fold iterated defect starting from the zero deviation of $ρ$ exceeds $B$.

background

Recognition Science obtains the cost function from the Recognition Composition Law, the multiplicative d'Alembert equation $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$ for positive $x,y$. This forces $J(x) = (x + x^{-1})/2 - 1$, or equivalently cosh(log $x$) - 1. The zero composition law then produces the recurrence $d_{n+1} = 2d_n(d_n + 2)$ for the defect sequence of any off-critical zero, yielding at least $4^n$ growth in the initial deviation $d_0 > 0$. The carrier budget is the finite annular excess of the determinant expression $C(s) = det_2(I - A)^2$ at each scale. This module links the zero composition law to the Riemann Hypothesis by showing that the divergent defects must violate any fixed finite bound.

proof idea

The proof is a one-line wrapper that applies the zero composition divergence lemma directly to the off-critical zero $ρ$ and the budget $B$.

why it matters in Recognition Science

This theorem supplies the contradiction step inside the downstream result that the Composition Closure Hypothesis implies the Riemann Hypothesis. It completes the alternate chain from the Recognition Composition Law (T5 J-uniqueness) through self-composition amplification of defects to a violation of the finite carrier budget. The module presents this as a separate conditional RH certificate distinct from the EBBA bridge.

scope and limits

formal statement (Lean)

  86theorem composition_violates_budget (ρ : ℂ) (hρ : ¬OnCriticalLine ρ) (B : ℝ) :
  87    ∃ n : ℕ, B < defectIterate (zeroDeviation ρ) n :=

proof body

Term-mode proof.

  88  zero_composition_diverges ρ hρ B
  89
  90/-- **Riemann Hypothesis from Composition Closure.**
  91
  92    If the Composition Closure Hypothesis holds, then every nontrivial
  93    zero of ζ(s) lies on the critical line Re(s) = 1/2.
  94
  95    Proof: Suppose ρ is off-critical. By CCH, every iterated defect is
  96    bounded by the carrier budget. But by the composition law, the
  97    iterated defects diverge. Contradiction. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (20)

Lean names referenced from this declaration's body.