IndisputableMonolith.Verification.T5UniqueCert

   1import Mathlib
   2import IndisputableMonolith.Cost
   3
   4/-!
   5# T5 Packaging Certificate (transport lemma, NOT the uniqueness theorem)
   6
   7**Honesty note (2026 audit correction).** This certificate is a *packaging
   8tautology*, and its docstring previously oversold it as "the crown jewel."
   9The `JensenSketch` hypotheses include BOTH `F(exp t) ≤ J(exp t)` and
  10`J(exp t) ≤ F(exp t)`, i.e. they already assert `F = J` on the exponential
  11axis. The conclusion `F = J on (0,∞)` is then just transport along
  12`exp/log` surjectivity. Hypothesis ≈ conclusion; no uniqueness content
  13lives here.
  14
  15The ACTUAL T5 uniqueness theorem — the one with real mathematical
  16content — is `law_of_logic_forces_jcost` in `Cost/FunctionalEquation.lean`:
  17reciprocal symmetry + unit normalization + the composition law (C6) +
  18calibration + continuity force `F = J`, via the proved Aczél/d'Alembert
  19classification (`Cost/AczelProof.lean`). Cite THAT theorem for T5
  20uniqueness claims; cite this certificate only as the trivial axis-to-ray
  21transport step.
  22-/
  23
  24namespace IndisputableMonolith
  25namespace Verification
  26namespace T5Unique
  27
  28open IndisputableMonolith.Cost
  29
  30structure T5UniqueCert where
  31  deriving Repr
  32
  33/-- Verification predicate: exp-axis-to-positive-ray transport.
  34
  35Any function F satisfying `JensenSketch` (whose bounds already pin
  36`F = J` on the exponential axis) equals `Jcost` on the positive reals.
  37This is a packaging/transport lemma; the substantive T5 uniqueness
  38theorem is `law_of_logic_forces_jcost` (see module header). -/
  39@[simp] def T5UniqueCert.verified (_c : T5UniqueCert) : Prop :=
  40  ∀ (F : ℝ → ℝ) [JensenSketch F] {x : ℝ}, 0 < x → F x = Jcost x
  41
  42@[simp] theorem T5UniqueCert.verified_any (c : T5UniqueCert) :
  43    T5UniqueCert.verified c := by
  44  intro F _ x hx
  45  exact T5_cost_uniqueness_on_pos hx
  46
  47end T5Unique
  48end Verification
  49end IndisputableMonolith
  50
  51