laws_polynomial_implies_continuous

formal source

 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.
 316
 317This section proves the algebraic half. It is independent of the
 318regularization and ψ-affine forcing arguments.
 319-/
 320
 321/-- Log-coordinate bilinear identity with coefficient `c`. -/
 322def LogBilinearIdentity (G : ℝ → ℝ) (c : ℝ) : Prop :=
 323  ∀ t u : ℝ,
 324    G (t + u) + G (t - u) = 2 * G t + 2 * G u + c * G t * G u
 325
 326/-- A classified log-coordinate cost: parabolic, hyperbolic, trigonometric,
 327or zero. This is the algebraic target left after the smoothness/affine-forcing
 328analysis has been done. -/
 329def ClassifiedLogCost (G : ℝ → ℝ) : Prop :=
 330  (∀ t, G t = 0) ∨