pith. sign in
module module high

IndisputableMonolith.NumberTheory.MellinPullback

show as:
view Lean formalization →

The MellinPullback module defines reciprocal symmetry for functions on positive reals, where f(x) equals f(1/x). It supplies the algebraic foundation for kernel substitutions in the Recognition Science Mellin transform. Researchers on the RS-native zeta program cite it when separating symmetry properties from transform interfaces. The module consists of the core definition plus supporting lemmas on pointwise behavior.

claimA function $f : (0,∞) → ℝ$ is reciprocally symmetric when $f(x) = f(1/x)$ holds for every $x > 0$.

background

This module belongs to the NumberTheory section and imports the Cost module, which supplies the J-cost function used throughout the Recognition Science framework. The supplied definition states that reciprocal symmetry means f(x) equals f(1/x) for positive x. The module prepares the algebraic content needed for Mellin reflection theorems by isolating this symmetry property from the transform construction itself.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module feeds the MellinTransform module, which builds a formal Mellin-transform interface whose reflection theorem is derived from reciprocal symmetry. It contributes to Phase 3 of the RS-native zeta program by separating the algebraic/RS content (reciprocal symmetry and kernel substitution) from the transform layer. The definition directly enables the symmetry-based derivation of reflection properties.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (8)