ClassifiedLogCost
plain-language theorem explainer
ClassifiedLogCost enumerates the admissible algebraic forms of a log-coordinate cost G after continuity is imposed on the combiner in the d'Alembert setting. Researchers deriving bilinear identities from the Recognition Composition Law cite it to replace the earlier polynomial-degree restriction. The definition is a direct disjunction that records the zero function together with the three families obtained from the Aczél–Kannappan trichotomy.
Claim. A function $G : ℝ → ℝ$ is a classified log-coordinate cost when it is identically zero, or $G(t) = α t^2$ for some constant $α$, or $G(t) = cosh(α t) - 1$ for some $α$, or $G(t) = 1 - cos(α t)$ for some $α$.
background
The module GeneralizedDAlembert carries out Move 3 of the regularity analysis: once the route-independence combiner is known to be continuous, the classical Aczél–Kannappan theorem classifies its solutions and thereby discharges the stronger polynomial-degree-≤-2 hypothesis that appeared in the Translation Theorem. ClassifiedLogCost is the resulting algebraic target for the log-reparametrized cost $G_F(t) = F(exp t)$ introduced in Cost.FunctionalEquation. Upstream, the cost of a recognition event is defined as its J-cost in ObserverForcing, and the multiplicative recognizer induces a derived cost in MultiplicativeRecognizerL4; both feed into the log-coordinate setting used here.
proof idea
This is a direct definition that enumerates the four cases permitted by the continuous d'Alembert classification: the zero function, the parabolic branch, the hyperbolic-cosine branch, and the trigonometric-cosine branch.
why it matters
ClassifiedLogCost supplies the case split used by the downstream theorems classified_log_cost_bilinear and classified_positive_cost_bilinear, which explicitly construct the bilinear combiner once the log-cost form is known. It thereby completes the algebraic step that lets the continuous-combiner version of SatisfiesLawsOfLogic drop the polynomial restriction, advancing the axiom-2 attack in the Law-of-Logic paper. The classification aligns with the Recognition Science pipeline that derives the d'Alembert equation from the Recognition Composition Law and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.