log_aczel_data_of_laws
plain-language theorem explainer
A continuous Law of Logic on a comparison operator yields a log-cost function G(t) = F(exp t) that is continuous, normalized at zero, even, and satisfies the Aczél equation G(t+u) + G(t-u) = P(G(t), G(u)) for a continuous symmetric combiner P. Analysts working on regularity in the Recognition Science functional equation framework cite this result to feed the mollification scaffold. The proof extracts the route-independence data and verifies each field of the LogAczelData structure using normalization, symmetry, and continuity lemmas.
Claim. Let $C$ be a comparison operator satisfying the continuous laws of logic. Then there exists $P : ℝ → ℝ → ℝ$ such that the log-cost $G(t) := F(e^t)$, where $F$ is the derived cost of $C$, satisfies: $G$ is continuous, $G(0) = 0$, $G$ is even, $P$ is continuous and symmetric, and $G(t+u) + G(t-u) = P(G(t), G(u))$ for all real $t, u$.
background
The module GeneralizedDAlembert discharges polynomial regularity using continuity. It proves the Aczél–Kannappan classification of continuous solutions to the d'Alembert equation, reducing to the existing dAlembert_classification in Cost.FunctionalEquation via integration bootstrap and ODE uniqueness. SatisfiesLawsOfLogicContinuous replaces polynomial route-independence with continuous route-independence while retaining the other Law of Logic axioms. LogAczelData packages the continuous log-cost G together with a combiner P obeying the equation G(t+u) + G(t-u) = P(G t, G u). This theorem leans on auxiliary results such as excluded_middle_implies_continuous and non_contradiction_and_scale_imply_reciprocal.
proof idea
Obtain the combiner P and its continuity and symmetry from the continuous route-independence field. Derive continuity of the derived cost on positives from excluded middle, normalization at unity from identity, and reciprocity symmetry from non-contradiction plus scale invariance. Assemble the LogAczelData record by applying continuous_log_cost_of_continuousOn_positive for continuity of G, a direct normalization, G_even_of_reciprocal_symmetry for evenness, and the consistency map for the Aczél equation after the exponential change of variables.
why it matters
This supplies the continuous input object required for the smoothness bootstrap that follows in the same module. It enables the continuous-combiner version of the Law of Logic, making the polynomial-degree restriction a special case rather than a necessary hypothesis for the Translation Theorem. The result sits inside the Aczél–Kannappan classification proved here, which in turn rests on the dAlembert_classification upstream. It touches the open question whether continuity alone closes all required identities, given the quartic-log counterexample for second-derivative closure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.