ContinuousCombinerAnalysisInputs

formal source

 566an arbitrary continuous combiner. This is deliberately a hypothesis package,
 567not an axiom. The quartic-log obstruction shows the package is not automatic
 568from `SatisfiesLawsOfLogicContinuous`. -/
 569structure ContinuousCombinerAnalysisInputs
 570    (C : ComparisonOperator)
 571    (h : SatisfiesLawsOfLogicContinuous C) : Prop where
 572  finite_smoothness : ContinuousCombinerMollifierFiniteSmoothness C h
 573  second_derivative :
 574    ContinuousCombinerSecondDerivativeInput C h
 575      (continuous_combiner_log_smoothness_bootstrap C h finite_smoothness)
 576  psi_affine :
 577    ContinuousCombinerPsiAffineCompletion C h
 578      (continuous_combiner_log_smoothness_bootstrap C h finite_smoothness)
 579      second_derivative
 580
 581/-- **Residual input 2 assembled:** smoothness plus the derivative identity
 582and ψ-affine completion give the required log-bilinear identity. -/
 583theorem continuous_combiner_psi_affine_forcing
 584    (C : ComparisonOperator)
 585    (h : SatisfiesLawsOfLogicContinuous C)
 586    (hSmooth : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞)
 587      (fun t : ℝ => derivedCost C (Real.exp t)))
 588    (hDeriv : ContinuousCombinerSecondDerivativeInput C h hSmooth)
 589    (hPsi : ContinuousCombinerPsiAffineCompletion C h hSmooth hDeriv) :
 590    ∃ c : ℝ, LogBilinearIdentity (fun t : ℝ => derivedCost C (Real.exp t)) c := by
 591  exact hPsi
 592
 593/-- **Continuous-combiner bilinear classification** (hypothesis-package form).
 594
 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)