polynomial_implies_continuous

formal source

 282  fun_prop
 283
 284/-- Polynomial route-independence implies continuous route-independence. -/
 285theorem polynomial_implies_continuous (C : ComparisonOperator)
 286    (hPoly : RouteIndependence C) :
 287    ContinuousRouteIndependence C := by
 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`. -/
 300theorem laws_polynomial_implies_continuous
 301    (C : ComparisonOperator) (h : SatisfiesLawsOfLogic C) :
 302    SatisfiesLawsOfLogicContinuous C where
 303  identity := h.identity
 304  non_contradiction := h.non_contradiction
 305  excluded_middle := h.excluded_middle
 306  scale_invariant := h.scale_invariant
 307  route_independence := polynomial_implies_continuous C h.route_independence
 308  non_trivial := h.non_trivial
 309
 310/-! ## 4. Conditional bilinear assembly
 311
 312The remaining continuous-combiner work separates cleanly into two
 313parts. The hard analysis must classify the log-coordinate cost
 314`G(t) = F(exp t)`. Once that classification is available, the bilinear
 315combiner is just algebra.