paired_zero_composition
The theorem delivers the algebraic identity J(x²) = 2[J(x)]² + 4J(x) for the defect coordinate x obtained from any real σ via the xi map. Researchers linking the Riemann functional equation to Recognition Science cost symmetry would cite it when quantifying quadratic defect growth for paired zeros. The term proof reduces the claim by first confirming non-vanishing of the map and then applying field simplification followed by ring arithmetic on the unfolded J-cost definition.
claimFor any real number σ, let x = ξ_map(σ). Then J(x²) = 2[J(x)]² + 4J(x), where J denotes the J-cost functional and ξ_map is the defect-coordinate map sending the real part of s in the critical strip to the positive real x satisfying the reciprocal symmetry J(x) = J(1/x).
background
The module bridges the completed Riemann xi function ξ(s) = ξ(1-s) with the J-cost functional that obeys J(x) = J(1/x). Under the coordinate change x = e^{2(Re(s) − 1/2)}, the critical line maps to x = 1 (the unique J minimum) and functional reflection maps to x ↦ 1/x. The Recognition Composition Law supplies the underlying addition formula J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y).
proof idea
The term proof first invokes the sibling lemma xiMap_ne_zero to obtain xiMap σ ≠ 0, then unfolds Jcost via simp only [Jcost], clears denominators with field_simp, and closes the resulting polynomial identity with ring.
why it matters in Recognition Science
The declaration is listed as the fourth main result in the module doc-comment, supplying the amplification equation that follows from substituting a reciprocal pair into the Recognition Composition Law. It supports the downstream claim that the Riemann hypothesis is equivalent to zero J-cost on all zeros and quantifies how defect grows quadratically away from the critical line. The result sits inside the T5–T6 forcing chain that derives J-uniqueness and the self-similar fixed point phi.
scope and limits
- Does not locate any zeros or prove the Riemann hypothesis.
- Does not apply when σ is complex or when xiMap vanishes.
- Does not incorporate the eight-tick octave or spatial dimension D = 3.
- Does not address multi-pair compositions or higher powers beyond x².
formal statement (Lean)
156theorem paired_zero_composition (σ : ℝ) :
157 Jcost ((xiMap σ) ^ 2) =
158 2 * (Jcost (xiMap σ)) ^ 2 + 4 * Jcost (xiMap σ) := by
proof body
Term-mode proof.
159 have hx : xiMap σ ≠ 0 := xiMap_ne_zero σ
160 have hx2 : (xiMap σ) ^ 2 ≠ 0 := pow_ne_zero 2 hx
161 simp only [Jcost]
162 field_simp
163 ring
164
165/-- Self-composition in cosh form: the double-angle identity.
166 cosh(4η) − 1 = 2·(cosh(2η) − 1)² + 4·(cosh(2η) − 1).
167
168 This follows from the cosh double-angle formula cosh(2t) = 2cosh²(t)−1,
169 which is itself a consequence of the RCL in log-coordinates. -/