G_even_of_reciprocal_symmetry
plain-language theorem explainer
If a cost function F on positive reals satisfies reciprocity, then its log reparametrization G(t) = F(exp t) is even. Researchers working on T5 uniqueness cite the result to reduce the symmetry hypothesis before invoking the Aczel equation. The tactic proof applies the definition of G, the identity exp(-t) equals the reciprocal of exp(t), and the given symmetry hypothesis.
Claim. Suppose $F : (0,∞) → ℝ$ satisfies $F(x) = F(x^{-1})$ for all $x > 0$. Then the reparametrized map $G(t) := F(e^t)$ is even.
background
The Cost.FunctionalEquation module collects lemmas that support the T5 cost uniqueness proof. Its central definition is the log reparametrization G(F, t) = F(exp t), which converts multiplicative properties of F into additive properties of a function on the reals. The upstream J-cost inflaton result supplies the model case G(t) = cosh(t) − 1, while log_aczel_data_of_laws records the continuous Aczel data that evenness makes available.
proof idea
Tactic proof: introduce arbitrary real t, record that exp(t) > 0, rewrite exp(−t) as the reciprocal of exp(t), then simplify the definition of G(−t) by substituting the symmetry hypothesis on F.
why it matters
The lemma is invoked by reciprocal_implies_G_even and thereby feeds washburn_uniqueness together with T5_uniqueness_complete. It performs the symmetry-to-evenness reduction inside the T5 J-uniqueness step of the forcing chain. The result leaves the calibration condition, convexity, and continuity hypotheses open for the complete uniqueness theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.