pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Cost.FunctionalEquation

show as:
view Lean formalization →

The Cost.FunctionalEquation module supplies the log reparametrization G_F(t) = F(exp t) that converts the multiplicative Recognition Composition Law into the additive d'Alembert equation. Analysts closing the T5 J-uniqueness step in the forcing chain cite it to reach the cosh form of the J-cost function. The module defines auxiliary objects G and H plus their evenness and additivity identities by direct substitution, relying on the imported AczelClass smoothness interface.

claimLet F satisfy the Recognition Composition Law. The log reparametrization is $G_F(t) := F(e^t)$. Under this change of variables the equation becomes the d'Alembert form $G(t+u) + G(t-u) = 2G(t)G(u)$ with $G(0)=1$.

background

In the Cost domain the J-cost function obeys the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). The module Cost.FunctionalEquation performs the change to logarithmic coordinates that turns the multiplicative structure into an additive functional equation. It imports the AczelClass typeclass whose doc states: 'This module declares the typeclass interface for the d'Alembert smoothness package and the bootstrap theorem that uses it.' The local setting assumes positive reals and the normalization conventions already fixed in the parent Cost module.

proof idea

This is a definition module. It introduces the reparametrization G_F t = F (exp t) together with the auxiliary functions G, H and the identities CoshAddIdentity, G_even_of_reciprocal_symmetry, even_deriv_at_zero. Each identity follows by direct substitution into the functional equation and algebraic rearrangement; no heavy tactics appear.

why it matters in Recognition Science

The module bridges the multiplicative Recognition Composition Law to the additive d'Alembert equation needed for T5. It is imported by Cost.AczelClassification, whose doc notes that it packages 'the part of the d'Alembert forcing chain that is supplied by the Aczel classification theorem', and by Cost.AczelTheorem which concludes every continuous solution is C^∞. This step removes the central regularity seam before the ODE H'' = H and the eight-tick octave are reached.

scope and limits

used by (21)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (62)