AczelSecondDerivativeIdentity

formal source

 524
 525/-- The second-derivative identity extracted from the smooth Aczél equation.
 526The function `ψ` is morally `∂₂ P(u, 0)`. -/
 527def AczelSecondDerivativeIdentity (G : ℝ → ℝ) : Prop :=
 528  ∃ ψ : ℝ → ℝ,
 529    ∀ t : ℝ, 2 * deriv (deriv G) t = ψ (G t) * deriv (deriv G) 0
 530
 531/-- Affineness of `ψ` on the image of the log-cost. -/
 532def PsiAffineOnImage (G : ℝ → ℝ) (ψ : ℝ → ℝ) : Prop :=
 533  ∃ c : ℝ, ∀ t : ℝ, ψ (G t) = 2 + c * G t
 534
 535/-- **Named analysis input 2a: derivative identity for the combiner equation.**
 536
 537This is the first differentiating step in the Stetkær/Aczél proof: from a
 538smooth log-coordinate Aczél equation, extract
 539`2 G''(t) = ψ(G(t)) G''(0)`.
 540
 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