ContinuousCombinerSecondDerivativeInput

formal source

 541This is not a theorem under the present hypotheses: the quartic log-cost
 542obstruction is formalized in
 543`Foundation.GeneralizedDAlembert.SecondDerivative`. -/
 544def ContinuousCombinerSecondDerivativeInput
 545    (C : ComparisonOperator)
 546    (_h : SatisfiesLawsOfLogicContinuous C)
 547    (_hSmooth : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞)
 548      (fun t : ℝ => derivedCost C (Real.exp t))) : Prop :=
 549    AczelSecondDerivativeIdentity (fun t : ℝ => derivedCost C (Real.exp t))
 550
 551/-- **Named analysis input 2b: ψ-affine completion.**
 552
 553This is the remaining Stetkær/Aczél content: the derivative identity, symmetry
 554of the combiner, and the Aczél equation force the actual log-bilinear identity.
 555It is narrower than the former all-in ψ-affine forcing axiom because the
 556second-derivative extraction is now named separately. -/
 557def ContinuousCombinerPsiAffineCompletion
 558    (C : ComparisonOperator)
 559    (_h : SatisfiesLawsOfLogicContinuous C)
 560    (_hSmooth : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞)
 561      (fun t : ℝ => derivedCost C (Real.exp t)))
 562    (_hDeriv : AczelSecondDerivativeIdentity (fun t : ℝ => derivedCost C (Real.exp t))) : Prop :=
 563    ∃ c : ℝ, LogBilinearIdentity (fun t : ℝ => derivedCost C (Real.exp t)) c
 564
 565/-- Explicit package of the extra analysis needed to force bilinearity from
 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