IndisputableMonolith.NumberTheory.XiJBridge
The XiJBridge module connects zero-deviation parameters from zeta locations to the J-cost function through the identity J(e^t) = cosh(t) - 1. Researchers deriving composition laws or doubling recurrences on zero defects would cite it to import the exponential bridge. The structure consists of the xiMap definition followed by direct algebraic reductions from the J-cost exponential lemma and the cosh definition.
claim$J(e^{t}) = 2^{-1}(e^{t} + e^{-t}) - 1$, with the auxiliary map sending deviation parameter $t$ to the exponential scale on which the cost is evaluated.
background
The module imports the J-cost definition from the Cost module and the zero-location dictionary from ZeroLocationCost. The latter supplies zeroDeviation ρ = 2(Re ρ - 1/2) together with zeroDefect ρ = defect(exp(zeroDeviation ρ)). xiMap is introduced as the exponential map that places the deviation parameter on the positive real line where J acts, and the module records its basic analytic properties (positivity, strict monotonicity, reflection symmetry).
proof idea
The module is primarily definitional. The central identity follows by one-line substitution of the J-cost exponential lemma into the definition of cosh. Remaining results (xiMap_pos, xiMap_strictMono, xiMap_reflection, non-negativity of the composed cost) are obtained by applying the chain rule to the exponential and the known monotonicity of J on (0, ∞).
why it matters in Recognition Science
The bridge supplies the concrete link between zero deviations and the Recognition Composition Law, enabling the downstream modules ZeroCompositionLaw (which extracts the composition law on zeta-zero defects), ZeroDoublingLaw (which records the doubling recurrence D(2t) = 2D(t)^2 + 4D(t)), and CompositionDivergence (the alternate conditional certificate for the Riemann Hypothesis). It realizes the J-uniqueness step of the forcing chain in the setting of zero locations.
scope and limits
- Does not locate any individual zeta zero.
- Does not prove the Riemann Hypothesis outright.
- Does not extend the bridge beyond the exponential map.
- Does not treat complex deviations or higher-order defects.
used by (3)
depends on (2)
declarations in this module (18)
-
theorem
jcost_exp_eq_cosh -
def
xiMap -
theorem
xiMap_pos -
theorem
xiMap_ne_zero -
theorem
xiMap_at_half -
theorem
xiMap_reflection -
theorem
xiMap_strictMono -
theorem
xiMap_eq_exp_zeroDeviation -
theorem
jcost_xiMap_eq_cosh -
theorem
jcost_xiMap_at_half -
theorem
jcost_xiMap_nonneg -
theorem
jcost_xiMap_functional_symmetry -
theorem
rh_equivalent_to_zero_cost -
theorem
rcl_defect_coordinates -
theorem
xiMap_mul_reflection -
theorem
xiMap_div_reflection -
theorem
paired_zero_composition -
theorem
self_composition_cosh