h_even
plain-language theorem explainer
The log-space transform h of the J-cost satisfies h(t) = h(-t) for all real t. Analysts of cost reciprocity and d'Alembert solutions in the Recognition framework cite this to confirm symmetry under inversion. The verification is a direct algebraic reduction after unfolding the definition of h.
Claim. Let $h : ℝ → ℝ$ be the function obtained by composing the J-cost with the exponential change of variables $t = ln(x)$. Then $h(t) = h(-t)$ for every real number $t$.
background
The module establishes convexity and symmetry of the J-cost when rewritten in logarithmic coordinates, following the ALEXIS internal note. The J-cost satisfies J(1) = 0 with unique global minimum at unity; under $t = ln(x)$ the image function obeys g(0) = 0, evenness, and strict positivity off zero. The evenness property directly encodes the reciprocity J(x) = J(x^{-1}). Both the J-cost and the quadratic form ½(ln x)² share the fixed point at x = 1 and the same sign pattern.
proof idea
The proof is a one-line wrapper that unfolds the definition of h and applies the ring tactic to verify the algebraic identity.
why it matters
This identity feeds the parent results composition_law_forces_reciprocity, dAlembert_cosh_solution, and dAlembert_cosh_solution_aczel in the Cost modules. It supplies the symmetry step required for T5 J-uniqueness in the UnifiedForcingChain, where J(x) = (x + x^{-1})/2 - 1 is forced as the cosh form. The result closes part of the structural identity needed for the Recognition Composition Law and the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.