H
plain-language theorem explainer
The definition supplies the shifted log-cost H_F(t) := G_F(t) + 1, where G_F(t) = F(exp t). Researchers proving T5 J-uniqueness and the Recognition Composition Law cite it to reach the d'Alembert form. The construction is a direct one-line reparametrization with no lemmas or tactics.
Claim. Let $G_F(t) := F(e^t)$. Define the shifted cost by $H_F(t) := G_F(t) + 1$.
background
This module supplies helper definitions for the T5 cost uniqueness proof. G reparametrizes an arbitrary cost function F into log coordinates: $G_F(t) = F(e^t)$. The present definition then shifts the result by one to obtain $H_F(t) = G_F(t) + 1$ for use in functional equations.
proof idea
The declaration is a direct definition that adds the constant 1 to the output of G. No tactics or lemmas are invoked; it is a one-line wrapper around the log reparametrization G.
why it matters
This definition supports the T5 J-uniqueness result by enabling the transition from the Recognition Composition Law to its d'Alembert form. It appears in the cost_algebra_certificate that verifies the algebraic structure and in derivations of Hamilton's equations from the Euler-Lagrange equation. It closes a small notational gap in the forcing chain from T0 to T5.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.