IndisputableMonolith.Cost.FunctionalEquationAczel

   1import IndisputableMonolith.Cost.FunctionalEquation
   2import IndisputableMonolith.Cost.AczelProof
   3
   4open IndisputableMonolith
   5
   6/-!
   7# Aczél-Based Closure for Functional Equation Uniqueness
   8
   9This file isolates the legacy Aczél-dependent closure theorems from the
  10axiom-free core in `IndisputableMonolith.Cost.FunctionalEquation`.
  11
  12The unconditional IM theorem surface should import the core module directly.
  13This compatibility module exists only for callers that still want the
  14one-line Aczél closure theorems.
  15-/
  16
  17namespace IndisputableMonolith
  18namespace Cost
  19namespace FunctionalEquation
  20
  21open Real
  22
  23/-! ## Thin Compatibility Surface
  24
  25The helper lemmas that used to live here now live in
  26`IndisputableMonolith.Cost.FunctionalEquation`. This file remains only for
  27legacy imports that want a one-line Aczél closure theorem. -/
  28
  29/-- **Law of Logic cost theorem, Aczél closure**: The J-cost function is the unique
  30    reciprocal cost satisfying the RCL, normalization, calibration, and continuity.
  31
  32    This version uses the global Aczél axiom internally and requires NO regularity
  33    hypothesis parameters from the caller. -/
  34theorem law_of_logic_forces_jcost_aczel (F : ℝ → ℝ)
  35    (hRecip : IsReciprocalCost F)
  36    (hNorm : IsNormalized F)
  37    (hComp : SatisfiesCompositionLaw F)
  38    (hCalib : IsCalibrated F)
  39    (hCont : ContinuousOn F (Set.Ioi 0)) :
  40    ∀ x : ℝ, 0 < x → F x = Cost.Jcost x := by
  41  exact law_of_logic_forces_jcost F hRecip hNorm hComp hCalib hCont
  42
  43end FunctionalEquation
  44end Cost
  45end IndisputableMonolith
  46