IndisputableMonolith.Verification.CostUniquenessCert

   1import Mathlib
   2import IndisputableMonolith.CostUniqueness
   3
   4/-!
   5# Cost Uniqueness (Classical) Certificate
   6
   7This audit certificate packages the "full" cost uniqueness theorem for `Jcost` under an
   8explicit hypothesis bundle (`IndisputableMonolith.CostUniqueness.UniqueCostAxioms`).
   9
  10Unlike `Verification/T5UniqueCert.lean` (which uses the compact `JensenSketch` interface),
  11this cert records a more classical route: symmetry + normalization + strict convexity +
  12calibration + continuity + the cosh-add functional identity.
  13
  14All assumptions are passed explicitly (no hidden typeclass axioms), and the proof is
  15entirely `sorry`-free.
  16-/
  17
  18namespace IndisputableMonolith
  19namespace Verification
  20namespace CostUniqueness
  21
  22open IndisputableMonolith.Cost
  23
  24structure CostUniquenessCert where
  25  deriving Repr
  26
  27/-- Verification predicate: any function satisfying `UniqueCostAxioms` agrees with `Jcost`
  28on all positive reals. -/
  29@[simp] def CostUniquenessCert.verified (_c : CostUniquenessCert) : Prop :=
  30  ∀ (F : ℝ → ℝ),
  31    _root_.IndisputableMonolith.CostUniqueness.UniqueCostAxioms F →
  32      ∀ {x : ℝ}, 0 < x → F x = Jcost x
  33
  34@[simp] theorem CostUniquenessCert.verified_any (c : CostUniquenessCert) :
  35    CostUniquenessCert.verified c := by
  36  intro F hF x hx
  37  exact _root_.IndisputableMonolith.CostUniqueness.unique_cost_on_pos F hF hx
  38
  39end CostUniqueness
  40end Verification
  41end IndisputableMonolith
  42