IndisputableMonolith.Cost.FunctionalEquationStrict

   1import IndisputableMonolith.Cost.AczelProof
   2import IndisputableMonolith.Cost.FunctionalEquation
   3
   4/-!
   5# Strict Functional-Equation Variants
   6
   7This optional module tightens the T5 regularity surface without changing the
   8core theorem.  The theorem below replaces the explicit
   9`ContinuousOn F (Set.Ioi 0)` premise with limit-form log calibration.
  10
  11History, 2026-07-25. Until that date this theorem was **vacuous**. Limit-form
  12calibration was stated on the full neighbourhood filter, which Lean's total
  13division makes unsatisfiable at `κ = 1`, so the premise it traded continuity for
  14was false and the trade bought nothing. `HasLogCurvature` is now punctured and
  15carries a non-vacuity witness (`jcost_hasLogCurvature_one`), so the statement has
  16content. It is also no longer the sharpest form: reciprocity, normalization, and
  17the derivative calibration are all redundant here, and
  18`composition_logCurvature_forces_jcost` states the result on the two premises
  19that do the work. This wrapper is kept for its callers.
  20-/
  21
  22namespace IndisputableMonolith
  23namespace Cost
  24namespace FunctionalEquation
  25
  26open Real
  27
  28/-- Limit-form log calibration supplies the continuity needed by the Aczél
  29d'Alembert route, so the explicit `ContinuousOn F (Set.Ioi 0)` premise can be
  30removed from this T5 variant.
  31
  32Only `hComp` and `hLogCalib` are used: the other three premises are consequences
  33of that pair. They are retained so existing callers keep type-checking. -/
  34theorem law_of_logic_forces_jcost_of_log_calibration (F : ℝ → ℝ)
  35    [AczelSmoothnessPackage]
  36    (_hRecip : IsReciprocalCost F)
  37    (_hNorm : IsNormalized F)
  38    (hComp : SatisfiesCompositionLaw F)
  39    (_hCalib : IsCalibrated F)
  40    (hLogCalib : IsCalibratedLimit F) :
  41    ∀ x : ℝ, 0 < x → F x = Cost.Jcost x :=
  42  composition_logCurvature_forces_jcost F hComp hLogCalib
  43
  44/-- **The cost theorem on two premises, unconditionally.**
  45
  46`composition_logCurvature_forces_jcost` is stated in `FunctionalEquation`, which
  47does not import the module that builds the `AczelSmoothnessPackage` instance, so
  48there it carries the package as an instance argument. This module does import it,
  49so here the theorem stands with no instance argument and no hypotheses beyond the
  50composition law and unit log curvature. Cite this one. -/
  51theorem composition_logCurvature_forces_jcost_unconditional (F : ℝ → ℝ)
  52    (hComp : SatisfiesCompositionLaw F)
  53    (hκ : HasLogCurvature (H F) 1) :
  54    ∀ x : ℝ, 0 < x → F x = Cost.Jcost x :=
  55  composition_logCurvature_forces_jcost F hComp hκ
  56
  57end FunctionalEquation
  58end Cost
  59end IndisputableMonolith
  60