log_aczel_data_of_laws
plain-language theorem explainer
This theorem extracts a continuous log-coordinate Aczél equation from any continuous Law of Logic operator via its derived cost. Analysts of the Recognition Science smoothness bootstrap cite it to replace polynomial route-independence with continuity alone. The tactic proof unpacks the continuous route-independence field to obtain the combiner P, then verifies continuity, normalization, evenness, and the Aczél relation for the log-cost G using auxiliary lemmas on the derived cost.
Claim. Let $C$ be a comparison operator satisfying the continuous laws of logic. Let $F$ denote its derived cost. Then there exists $P : ℝ → ℝ → ℝ$ such that $G(t) := F(e^t)$ 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 discharges the polynomial regularity hypothesis of the Translation Theorem by substituting continuity of the route-independence combiner. It invokes the Aczél–Kannappan classification of continuous solutions to the d'Alembert equation (constant 1, cosh, or cos). SatisfiesLawsOfLogicContinuous is the structure that replaces polynomial route-independence with its continuous counterpart while retaining identity, non-contradiction, excluded middle, scale invariance, and non-triviality. LogAczelData packages the resulting continuous even log-cost $G$ together with a symmetric continuous combiner $P$ obeying the Aczél relation. Upstream lemmas supply the continuity lift from positive ratios to the log coordinate and the symmetry of $G$ from reciprocal symmetry of $F$.
proof idea
Obtain the combiner $P$ from the route_independence field. Establish continuity of $F$ on positive reals via excluded_middle_implies_continuous, normalization $F(1)=0$ via identity_implies_normalized, and symmetry of $F$ via non_contradiction_and_scale_imply_reciprocal. Fill the LogAczelData record by applying continuous_log_cost_of_continuousOn_positive for continuity of $G$, direct simplification for the zero property, G_even_of_reciprocal_symmetry for evenness, and the consistency condition on exponentials (with addition and subtraction formulas) for the Aczél equation.
why it matters
The declaration supplies the continuous log Aczél data required as input to the smoothness bootstrap and mollification scaffold in the same module. It removes the polynomial-degree-≤-2 restriction on the combiner, allowing the Aczél–Kannappan trichotomy to discharge that hypothesis in the Law-of-Logic pipeline. The result connects directly to the integration-bootstrap regularization and universal d'Alembert-to-ODE derivation used in the parent classification theorem. No downstream uses are recorded, but the construction underpins the continuous-combiner version of SatisfiesLawsOfLogic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.