mellin_reciprocal_reflection

formal source

  99
 100/-- If a Mellin transform package is admissible for a reciprocally symmetric
 101kernel, then the transform is invariant under `s ↔ 1-s`. -/
 102theorem mellin_reciprocal_reflection
 103    {f : ℝ → ℝ} (pkg : MellinAdmissibleKernel f) :
 104    ∀ s : ℝ, pkg.M s = pkg.M (mellinReflect s) :=
 105  pkg.substitution
 106
 107/-- The same theorem expressed as a two-sided symmetry. -/
 108theorem mellin_reflection_involutive
 109    {f : ℝ → ℝ} (pkg : MellinAdmissibleKernel f) (s : ℝ) :
 110    pkg.M (mellinReflect (mellinReflect s)) = pkg.M s := by
 111  unfold mellinReflect
 112  ring_nf
 113
 114/-- Recognition-cost Mellin admissibility is the exact analytic condition
 115needed to turn J's reciprocal symmetry into an `s ↔ 1-s` transform symmetry. -/
 116structure JCostMellinBridge where
 117  pkg : MellinAdmissibleKernel Cost.Jcost
 118
 119theorem Jcost_mellin_reflection (bridge : JCostMellinBridge) :
 120    ∀ s : ℝ, bridge.pkg.M s = bridge.pkg.M (mellinReflect s) :=
 121  mellin_reciprocal_reflection bridge.pkg
 122
 123/-! ## 4. Connection to recovered complex analytic substrate -/
 124
 125/-- A Mellin reflection package compatible with recovered complex inputs. This
 126does not define zeta; it records the bridge Phase 4 must instantiate with an
 127explicit theta kernel. -/
 128structure RecoveredComplexMellinBridge where
 129  analytic_substrate : Foundation.LogicComplexCompat.LogicComplexAnalyticSubstrateCert
 130  kernel : ℝ → ℝ
 131  mellin_pkg : MellinAdmissibleKernel kernel
 132  reflection : ∀ s : ℝ, mellin_pkg.M s = mellin_pkg.M (mellinReflect s)