LogAczelData
plain-language theorem explainer
LogAczelData encodes a continuous even function G vanishing at zero together with a symmetric continuous combiner P satisfying the additive relation G(t+u) + G(t-u) = P(G t, G u). Researchers replacing the polynomial bound on route independence with continuity cite this structure to feed the Aczél-Kannappan classification into the smoothness bootstrap. The declaration is a pure structure definition that assembles the six axioms with no proof content.
Claim. Let $G : ℝ → ℝ$ be continuous and even with $G(0) = 0$, and let $P : ℝ → ℝ → ℝ$ be continuous and symmetric. Then $G$ and $P$ satisfy the Aczél equation when $G(t + u) + G(t - u) = P(G(t), G(u))$ for all real $t, u$.
background
The GeneralizedDAlembert module weakens the polynomial-degree restriction on the route-independence combiner to continuity alone. The log reparametrization converts a multiplicative cost F into an additive function via G(t) = F(exp t), as defined in Cost.FunctionalEquation.G. LogAczelData collects the resulting continuous d'Alembert data: continuity and evenness of G with G(0)=0, continuity and symmetry of P, and the functional equation relating them. This setup directly supports the upstream Aczél-Kannappan classification of continuous solutions to H(x+y) + H(x-y) = 2H(x)H(y), obtained via integration bootstrap and ODE uniqueness.
proof idea
The declaration is a structure definition. It directly assembles the six fields: continuity of G, G(0)=0, evenness of G, continuity of the uncurried P, symmetry of P, and the pointwise functional equation aczel_eq.
why it matters
LogAczelData supplies the formal input to the theorem log_aczel_data_of_laws, which extracts such data from any SatisfiesLawsOfLogicContinuous witness. This step removes the polynomial restriction noted in the module documentation and lets the Aczél-Kannappan trichotomy classify the continuous solutions. The structure advances the continuous route-independence pipeline inside the Recognition framework by replacing an artificial regularity hypothesis with continuity of the combiner.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.