pith. machine review for the scientific record. sign in
theorem proved term proof

Jcost_mellin_reflection

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 119theorem Jcost_mellin_reflection (bridge : JCostMellinBridge) :
 120    ∀ s : ℝ, bridge.pkg.M s = bridge.pkg.M (mellinReflect s) :=

proof body

Term-mode proof.

 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. -/

depends on (16)

Lean names referenced from this declaration's body.