reciprocal_implies_G_even
plain-language theorem explainer
If a cost function F satisfies F(x) = F(1/x) for all x > 0, then its logarithmic reparametrization G(t) = F(e^t) is even. Researchers proving T5 cost uniqueness in Recognition Science cite this when establishing symmetry before deriving the cosh form of J. The argument is a direct one-line application of the symmetry lemma after unwrapping the IsReciprocalCost hypothesis into the required forall statement.
Claim. If $F : (0,∞) → ℝ$ satisfies $F(x) = F(x^{-1})$ for every $x > 0$, then the function $t ↦ F(e^t)$ is even.
background
The module supplies supporting lemmas for the T5 cost-uniqueness argument in the forcing chain. G is the log-coordinate change of variables defined by G(F)(t) := F(exp t). IsReciprocalCost is the predicate asserting F(x) = F(x^{-1}) for all x > 0. The upstream lemma G_even_of_reciprocal_symmetry proves evenness of G directly from the pointwise symmetry hypothesis ∀ {x}, 0 < x → F x = F x^{-1}.
proof idea
One-line wrapper that applies G_even_of_reciprocal_symmetry after converting the IsReciprocalCost hypothesis into the required forall form via a lambda that supplies the positivity witness.
why it matters
The result supplies the even symmetry needed for the T5 J-uniqueness step, where J(x) = (x + x^{-1})/2 - 1. Evenness of G guarantees that the functional equation reduces to the cosh-addition identity used to force the self-similar fixed point phi. It sits inside the T5-T6 segment of the forcing chain and is a prerequisite for later mass-ladder and alpha-band derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.