polynomial_implies_continuous
plain-language theorem explainer
If a comparison operator satisfies route independence via a quadratic polynomial combiner on derived costs, then the same operator satisfies the continuous-combiner version of route independence. Workers extending the Law of Logic to continuous combiners cite this to recover the polynomial case as an instance. The proof extracts the explicit coefficients from the polynomial hypothesis, equates the uncurried functions, and reduces to the elementary continuity of quadratic polynomials.
Claim. Let $C$ be a comparison operator on positive reals. If $C$ satisfies route independence (there exists a polynomial $P$ of total degree at most two such that the derived cost $F$ obeys $F(xy)+F(x/y)=P(F(x),F(y))$ for $x,y>0$), then $C$ satisfies continuous route independence: there exists a continuous symmetric $P$ satisfying the same identity.
background
The module develops the continuous version of the d'Alembert functional equation inside Recognition Science. A ComparisonOperator is an abbreviation for maps ℝ→ℝ→ℝ obeying the four Aristotelian constraints; the derived cost is obtained by fixing the second argument at the multiplicative identity. RouteIndependence (imported from LogicAsFunctionalEquation) requires the combiner to be a polynomial of total degree ≤2, while ContinuousRouteIndependence relaxes this to mere continuity of the symmetric combiner P.
proof idea
The tactic obtains the polynomial coefficients a,b,c,d,e,f together with symmetry and consistency from the RouteIndependence hypothesis. It then proves by function extensionality that the uncurried P equals the explicit quadratic expression a+b u + c v + d u v + e u² + f v². The proof rewrites the goal and applies the sibling theorem polynomial_continuous, which establishes continuity of that quadratic by unfolding uncurry and invoking fun_prop.
why it matters
This result embeds the polynomial route-independence hypothesis into the continuous version, enabling the downstream theorem laws_polynomial_implies_continuous to conclude that any SatisfiesLawsOfLogic instance yields SatisfiesLawsOfLogicContinuous. It advances the module goal of discharging the polynomial restriction in favor of continuity, consistent with the Aczél–Kannappan classification of continuous d'Alembert solutions. In the framework it supports relaxing the Translation Theorem while preserving the Law of Logic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.