polynomial_continuous
Any quadratic polynomial a + b u + c v + d u v + e u² + f v² on the plane is continuous as a map from ℝ×ℝ. Downstream code in the same module invokes it to lift polynomial route-independence to the continuous version. The proof is a one-line wrapper that unfolds the uncurried form and delegates to the built-in continuity tactic for polynomials.
claimFor all real numbers $a, b, c, d, e, f$, the map $(u, v) : ℝ × ℝ → ℝ$ given by $a + b u + c v + d u v + e u^2 + f v^2$ is continuous.
background
The GeneralizedDAlembert module relaxes the Translation Theorem's requirement that the route-independence combiner be a polynomial of total degree at most two. This private theorem supplies the continuity fact for the quadratic case, enabling the passage to a continuous-combiner predicate. MollifierCkRoute is the helper predicate asserting existence of a parametrized family of ContDiffBump kernels whose outer radii tend to zero at infinity. SatisfiesLawsOfLogicContinuous is the structure that encodes the laws of logic once the polynomial route-independence hypothesis is replaced by its continuous counterpart.
proof idea
The proof is a term-mode one-liner: unfold Function.uncurry exposes the explicit quadratic expression, after which fun_prop automatically confirms continuity of any polynomial map.
why it matters in Recognition Science
It is the sole dependency of polynomial_implies_continuous, which extracts the six coefficients from a RouteIndependence witness and applies this result to obtain ContinuousRouteIndependence. The module thereby discharges the original polynomial restriction in favor of continuity, consistent with the Aczél–Kannappan classification of continuous d'Alembert solutions (constant 1, cosh, or cos). In the Recognition framework this step advances the move from polynomial to continuous regularity while preserving the downstream pipeline to the laws of logic.
scope and limits
- Does not establish continuity for polynomials of total degree greater than two.
- Does not supply any modulus of continuity or quantitative bounds.
- Applies only to this explicit quadratic form in two variables.
- Does not address differentiability or higher regularity.
formal statement (Lean)
277private theorem polynomial_continuous
278 (a b c d e f : ℝ) :
279 Continuous (Function.uncurry
280 (fun u v : ℝ => a + b*u + c*v + d*u*v + e*u^2 + f*v^2)) := by
proof body
Term-mode proof.
281 unfold Function.uncurry
282 fun_prop
283
284/-- Polynomial route-independence implies continuous route-independence. -/