mellinReflect
plain-language theorem explainer
mellinReflect supplies the reflected Mellin parameter 1 - s. Workers on the Recognition Science zeta program cite it when enforcing s ↔ 1-s invariance at the transform level. The definition is realized by a direct one-line assignment.
Claim. The reflected Mellin parameter is given by $1 - s$.
background
MellinTransform.lean implements Phase 3 of the RS-native zeta program. The module supplies a formal Mellin-transform interface whose reflection law follows from reciprocal symmetry rather than from an explicit integral. It separates algebraic content (reciprocal symmetry of the kernel and the substitution x ↦ x^{-1}) from analytic content (existence of the transform and validity of the change of variables). The output is the transform-level bridge that Phase 4 will instantiate with a theta kernel.
proof idea
Direct definition that assigns the value 1 - s.
why it matters
mellinReflect supplies the parameter map required by MellinAdmissibleKernel and mellin_reciprocal_reflection. Those results in turn feed MellinPhase3Cert, which records that reciprocal symmetry plus a valid substitution law forces s ↔ 1-s reflection at the transform level. The definition therefore closes the algebraic half of the Phase 3 bridge toward the functional equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.