IndisputableMonolith.Verification.ReciprocalSymmetryEvenCert

   1import Mathlib
   2import IndisputableMonolith.Cost.FunctionalEquation
   3
   4namespace IndisputableMonolith
   5namespace Verification
   6namespace ReciprocalSymmetryEven
   7
   8open IndisputableMonolith.Cost.FunctionalEquation
   9open Real
  10
  11/-!
  12# Reciprocal Symmetry → Even Function Certificate
  13
  14This certificate packages the proof that reciprocal symmetry F(x) = F(1/x) for x > 0
  15implies that the log-coordinate representation G_F(t) = F(exp(t)) is an even function.
  16
  17## Key Result
  18
  19If F : ℝ → ℝ satisfies F(x) = F(x⁻¹) for all x > 0, then G_F is even:
  20  G_F(-t) = G_F(t) for all t ∈ ℝ
  21
  22## Why this matters for the certificate chain
  23
  24This result connects two fundamental symmetries:
  25
  261. **Reciprocal symmetry in multiplicative domain**: J(x) = J(1/x)
  27   - The cost of being "too big" equals the cost of being "too small"
  28   - A ratio and its inverse have the same cost
  29
  302. **Even symmetry in log-coordinates**: Jlog(-t) = Jlog(t)
  31   - The log-coordinate cost function is symmetric about zero
  32   - This implies Jlog'(0) = 0 (derivative of even function at 0)
  33
  343. **ODE initial conditions**: Combined with Jlog(0) = 0, we get the
  35   initial conditions H(0) = 1, H'(0) = 0 for H = Jlog + 1 = cosh
  36
  37This is a key step in the chain:
  38  Reciprocal symmetry → Even in log → H'(0) = 0 → ODE uniqueness → H = cosh
  39
  40## Mathematical Content
  41
  42The proof uses:
  43- exp(-t) = (exp(t))⁻¹
  44- G_F(-t) = F(exp(-t)) = F((exp(t))⁻¹) = F(exp(t)) = G_F(t)
  45-/
  46
  47structure ReciprocalSymmetryEvenCert where
  48  deriving Repr
  49
  50/-- Verification predicate: reciprocal symmetry implies even G_F.
  51
  52This certifies that if F(x) = F(1/x) for all x > 0, then G_F is even. -/
  53@[simp] def ReciprocalSymmetryEvenCert.verified (_c : ReciprocalSymmetryEvenCert) : Prop :=
  54  ∀ (F : ℝ → ℝ),
  55    (∀ {x : ℝ}, 0 < x → F x = F x⁻¹) →
  56    Function.Even (G F)
  57
  58/-- Top-level theorem: the certificate verifies. -/
  59@[simp] theorem ReciprocalSymmetryEvenCert.verified_any (c : ReciprocalSymmetryEvenCert) :
  60    ReciprocalSymmetryEvenCert.verified c := by
  61  intro F hSymm
  62  exact G_even_of_reciprocal_symmetry F hSymm
  63
  64end ReciprocalSymmetryEven
  65end Verification
  66end IndisputableMonolith
  67