module module high

`IndisputableMonolith.NumberTheory.ZeroCompositionLaw`

This module defines the iterated defect d_n(t) = cosh(2^n t) - 1 for zeta zeros under the Recognition Composition Law. Number theorists working on cost-based approaches to the Riemann Hypothesis cite it for the composition cascade. The content consists of definitions that extend the J-cost symmetry and zero-deviation map with no internal theorems.

claim$d_n(t) = \cosh(2^n t) - 1$, where for a zeta zero $\rho$ with deviation $\eta = \operatorname{Re}(\rho) - 1/2$ one sets $t = 2\eta$; $d_0$ is the zero's defect and $d_n$ its n-th iterate under RCL self-composition.

background

The J-cost satisfies J(x) = (x + x^{-1})/2 - 1 with unique minimum at x = 1; in log coordinates this is cosh(t) - 1. The Recognition Composition Law encodes the functional symmetry J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). ZeroLocationCost supplies the dictionary zeroDeviation ρ = 2(Re ρ - 1/2) and zeroDefect ρ = defect(exp(zeroDeviation ρ)). XiJBridge identifies the critical line Re(s) = 1/2 with the J-minimum via the map x = exp(2(Re(s) - 1/2)).

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the iterated-defect construction that CompositionDivergence consumes to obtain an alternate conditional certificate for the Riemann Hypothesis. It realizes the n-th RCL self-composition of a zero defect, providing the infinite family of cost values required by the composition-divergence argument.

scope and limits

Does not prove convergence of the defect sequence.
Does not compute explicit locations or heights of zeta zeros.
Does not contain a complete proof of the Riemann Hypothesis.
Does not address numerical verification of the alpha band.

used by (1)

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

IndisputableMonolith.NumberTheory.CompositionDivergence module_import

depends on (4)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost module_import
IndisputableMonolith.Foundation.DiscretenessForcing module_import
IndisputableMonolith.NumberTheory.XiJBridge module_import
IndisputableMonolith.NumberTheory.ZeroLocationCost module_import

declarations in this module (15)

def defectIterate L54
theorem defectIterate_zero_param L57
theorem defectIterate_zero_eq_J_log L61
theorem defectIterate_nonneg L66
theorem defectIterate_zero_pos L71
theorem defectIterate_succ L89
theorem defectIterate_succ' L103
theorem defectIterate_four_mul_le L111
theorem defectIterate_exponential_lower L121
theorem one_le_four_pow L132
theorem defectIterate_mono L140
theorem nat_succ_le_pow_four L149
theorem defectIterate_unbounded L164
theorem defectIterate_zero_eq_zeroDefect L184
theorem zero_composition_diverges L192