polynomial_continuous
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.