polynomial_implies_continuous
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not establish route independence from continuity of the combiner alone.
- Does not apply to combiners of total degree higher than two.
- Does not address the quartic-log counterexample that blocks second-derivative identities.
- Does not prove the full Aczél–Kannappan trichotomy inside this module.
Lean usage
theorem laws_polynomial_implies_continuous (C : ComparisonOperator) (h : SatisfiesLawsOfLogic C) : SatisfiesLawsOfLogicContinuous C where identity := h.identity non_contradiction := h.non_contradiction excluded_middle := h.excluded_middle scale_invariant := h.scale_invariant route_independence := polynomial_implies_continuous C h.route_independenceformal statement (Lean)
285theorem polynomial_implies_continuous (C : ComparisonOperator)
286 (hPoly : RouteIndependence C) :
287 ContinuousRouteIndependence C := by
proof body
Tactic-mode proof.
288 obtain ⟨P, ⟨a, b, c, d, e, f, hPform⟩, hSymP, hCons⟩ := hPoly
289 refine ⟨P, ?_, hSymP, hCons⟩
290 -- Continuity of P from its polynomial form.
291 have heq : Function.uncurry P
292 = Function.uncurry (fun u v : ℝ => a + b*u + c*v + d*u*v + e*u^2 + f*v^2) := by
293 funext ⟨u, v⟩
294 simpa using hPform u v
295 rw [heq]
296 exact polynomial_continuous a b c d e f
297
298/-- The polynomial-case `SatisfiesLawsOfLogic` is a special case of the
299continuous-case `SatisfiesLawsOfLogicContinuous`. -/