IndisputableMonolith.NumberTheory.ZeroCompositionLaw
This module defines the iterated defect d_n(t) = cosh(2^n t) - 1 as the n-fold self-composition of the initial zero defect under the Recognition Composition Law. Researchers examining cost-based routes to the Riemann hypothesis cite it for the infinite cascade of defects generated from a single zeta zero. It is a definition module that records the iteration formula and its relation to zero deviation η.
claimDefine the iterated defect by $d_n(t) := \cosh(2^n t) - 1$. For a zeta zero $\rho$ set $\eta = \operatorname{Re}(\rho) - 1/2$ and $t = 2\eta$, so that $d_0 = \cosh(2\eta) - 1$ is the zero defect and each $d_n$ is obtained by one further application of the composition law.
background
The J-cost is $J(x) = \frac12(x + x^{-1}) - 1$, which equals $\cosh(t) - 1$ after the substitution $x = e^t$. DiscretenessForcing shows that the unique minimum of this cost at $x=1$ forces discrete structure. XiJBridge maps the completed xi functional equation $\xi(s) = \xi(1-s)$ to the J-symmetry $J(x) = J(1/x)$ via the coordinate change $x = \exp(2(\operatorname{Re}(s) - 1/2))$. ZeroLocationCost supplies the dictionary zeroDeviation $\rho = 2(\operatorname{Re} \rho - 1/2)$ and zeroDefect $\rho =$ defect$(\exp($zeroDeviation $\rho))$.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The iterated defect supplies the cascade construction used by the downstream CompositionDivergence module, which states that composition divergence yields an alternate conditional certificate for the Riemann hypothesis. The module therefore realizes the claim that each iterate is reflected in the carrier budget and strengthens the composition-law analogue of the EBBA bridge.
scope and limits
- Does not prove convergence of the defect sequence for arbitrary initial t.
- Does not derive numerical bounds on defect growth.
- Does not connect the iterates to explicit arithmetic properties of individual zeros.
- Does not itself establish the Riemann hypothesis.
used by (1)
depends on (4)
declarations in this module (15)
-
def
defectIterate -
theorem
defectIterate_zero_param -
theorem
defectIterate_zero_eq_J_log -
theorem
defectIterate_nonneg -
theorem
defectIterate_zero_pos -
theorem
defectIterate_succ -
theorem
defectIterate_succ' -
theorem
defectIterate_four_mul_le -
theorem
defectIterate_exponential_lower -
theorem
one_le_four_pow -
theorem
defectIterate_mono -
theorem
nat_succ_le_pow_four -
theorem
defectIterate_unbounded -
theorem
defectIterate_zero_eq_zeroDefect -
theorem
zero_composition_diverges