ContinuousRouteIndependence
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not guarantee existence of P for an arbitrary comparison operator.
- Does not force P to be a polynomial of degree at most two.
- Does not derive the explicit form of P from continuity alone.
- Does not replace the full set of Aristotelian constraints on C.
formal statement (Lean)
110def ContinuousRouteIndependence (C : ComparisonOperator) : Prop :=
proof body
Definition body.
111 ∃ P : ℝ → ℝ → ℝ,
112 Continuous (Function.uncurry P) ∧
113 (∀ u v, P u v = P v u) ∧
114 (∀ x y : ℝ, 0 < x → 0 < y →
115 derivedCost C (x * y) + derivedCost C (x / y)
116 = P (derivedCost C x) (derivedCost C y))
117
118/-- A *continuous Law of Logic* — the existing `SatisfiesLawsOfLogic`
119with polynomial route-independence replaced by continuous
120route-independence. -/