ContinuousRouteIndependence
plain-language theorem explainer
ContinuousRouteIndependence encodes the existence of a continuous symmetric combiner P such that the derived cost F from any comparison operator C obeys F(xy) + F(x/y) = P(F(x), F(y)) for positive x, y. Analysts relaxing polynomial regularity in functional equations for logic would cite this predicate. The declaration is a direct existential definition over continuous functions on the reals.
Claim. Let $C$ be a comparison operator. Then $C$ satisfies continuous route independence if there exists a continuous symmetric function $P : (0,∞) × (0,∞) → ℝ$ such that for all positive $x, y$, $F(xy) + F(x/y) = P(F(x), F(y))$, where $F(r) := C(r, 1)$ is the derived cost.
background
The module GeneralizedDAlembert replaces the polynomial route-independence hypothesis in the Translation Theorem with a continuity requirement on the combiner. A comparison operator is a map ℝ → ℝ → ℝ obeying the four Aristotelian constraints plus scale invariance; the derived cost extracts the one-argument form by fixing the second argument at 1. The original SatisfiesLawsOfLogic structure packages identity, non-contradiction, excluded middle, scale invariance, and route independence (the polynomial version). Module documentation states the goal is to discharge polynomial regularity using continuity via the Aczél–Kannappan classification of continuous d'Alembert solutions.
proof idea
This is a definition that directly packages the continuous route-independence condition as an existential statement over continuous symmetric functions P satisfying the functional equation with the derived cost.
why it matters
The definition supplies the route-independence field for the downstream structure SatisfiesLawsOfLogicContinuous, which drops the polynomial-degree-≤-2 hypothesis. It feeds the theorem polynomial_implies_continuous and supports the module's use of Aczél–Kannappan to classify continuous solutions of the d'Alembert equation as constant, cosh, or cos. This step relaxes the regularity needed for the Law-of-Logic pipeline while keeping the algebraic assembly intact.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.