reciprocal_implies_G_even
If a cost function F satisfies F(x) = F(1/x) for all x > 0, then the log-reparametrized G(t) = F(exp t) is even. Researchers advancing the T5 J-uniqueness step in the Recognition Science forcing chain cite this to secure symmetry before invoking cosh-addition identities. The proof is a one-line term wrapper that feeds the IsReciprocalCost hypothesis into the symmetry lemma G_even_of_reciprocal_symmetry.
claimLet $F : {R} {to} {R}$ satisfy $F(x) = F(x^{-1})$ for every $x > 0$. Define $G(t) := F(e^{t})$. Then $G$ is even, i.e., $G(-t) = G(t)$ for all real $t$.
background
The module supplies short lemmas that prepare the T5 cost-uniqueness argument inside the Recognition Science forcing chain. IsReciprocalCost F is the predicate asserting $F(x) = F(x^{-1})$ whenever $x > 0$. The auxiliary map G sends a cost function to its log-coordinate version via $G(F,t) := F(exp t)$. The upstream lemma G_even_of_reciprocal_symmetry proves that the pointwise symmetry hypothesis already forces G to be even; the present theorem simply lifts the named definition IsReciprocalCost into that hypothesis.
proof idea
The proof is a one-line term that applies G_even_of_reciprocal_symmetry after wrapping the IsReciprocalCost hypothesis inside a lambda that supplies the required symmetry predicate.
why it matters in Recognition Science
The result translates the reciprocal-cost definition into evenness of G, a prerequisite for the cosh-addition identities used in the T5 J-uniqueness proof. It belongs to the FunctionalEquation helpers that support the main cost-uniqueness theorem in the T5 step of the forcing chain (T0 to T8). No downstream uses are recorded yet.
scope and limits
- Does not prove that any concrete F satisfies the reciprocal condition.
- Does not derive the explicit form of G or identify it with cosh.
- Does not incorporate the normalization condition F(1) = 0.
- Does not extend the evenness statement beyond real arguments.
formal statement (Lean)
705theorem reciprocal_implies_G_even (F : ℝ → ℝ) (hRecip : IsReciprocalCost F) :
706 Function.Even (G F) :=
proof body
Term-mode proof.
707 G_even_of_reciprocal_symmetry F (fun {x} hx => hRecip x hx)
708
709/-- **Lemma**: If F is normalized, then G(0) = 0. -/