continuous_combiner_bilinear_classification

formal source

 595The final bilinear conclusion follows if the explicit analysis package is
 596provided. It is not automatic from `SatisfiesLawsOfLogicContinuous`; the
 597quartic log-cost refutes the proposed second-derivative input. -/
 598theorem continuous_combiner_bilinear_classification
 599    (C : ComparisonOperator)
 600    (h : SatisfiesLawsOfLogicContinuous C)
 601    (hInputs : ContinuousCombinerAnalysisInputs C h) :
 602    ∃ (P : ℝ → ℝ → ℝ) (c : ℝ),
 603      (∀ x y : ℝ, 0 < x → 0 < y →
 604        derivedCost C (x * y) + derivedCost C (x / y)
 605          = P (derivedCost C x) (derivedCost C y)) ∧
 606      (∀ u v, P u v = 2*u + 2*v + c*u*v) := by
 607  have hSmooth := continuous_combiner_log_smoothness_bootstrap C h hInputs.finite_smoothness
 608  have hLog := continuous_combiner_psi_affine_forcing C h hSmooth
 609    hInputs.second_derivative hInputs.psi_affine
 610  exact log_bilinear_positive_cost_bilinear (derivedCost C) hLog
 611
 612/-- **Continuous-combiner Translation Theorem, hypothesis-package form**: a continuous comparison
 613operator satisfying the four Aristotelian conditions plus scale
 614invariance and continuous route independence admits a *bilinear*
 615combiner `P(u,v) = 2u + 2v + c·u·v` if the explicit analysis package is
 616also supplied. Polynomial-degree-≤-2 is not dropped by continuity alone. -/
 617theorem continuous_combiner_bilinear
 618    (C : ComparisonOperator)
 619    (h : SatisfiesLawsOfLogicContinuous C)
 620    (hInputs : ContinuousCombinerAnalysisInputs C h) :
 621    ∃ (P : ℝ → ℝ → ℝ) (c : ℝ),
 622      (∀ x y : ℝ, 0 < x → 0 < y →
 623        derivedCost C (x * y) + derivedCost C (x / y)
 624          = P (derivedCost C x) (derivedCost C y)) ∧
 625      (∀ u v, P u v = 2*u + 2*v + c*u*v) :=
 626  continuous_combiner_bilinear_classification C h hInputs
 627
 628/-! ## 5. Generalized Translation Theorem