ReciprocalSymmetric
plain-language theorem explainer
Reciprocal symmetry is the predicate requiring a real function on positive reals to satisfy f(x) equals f(1/x) for every x greater than zero. It is invoked by every result that transfers this invariance through the Mellin transform to obtain reflection symmetry around s equals 1/2. The definition is a direct universal quantifier with no internal lemmas or reductions.
Claim. A function $f : (0,∞) → ℝ$ is reciprocally symmetric when $f(x) = f(x^{-1})$ holds for every positive real $x$.
background
The module establishes the abstract structural link between inversion invariance on the positive reals and reflection symmetry of the Mellin transform. ReciprocalSymmetric f is the predicate that encodes f(x) = f(1/x) for x > 0; the module also introduces the substitution that converts the Mellin kernel x^{s-1} under x ↦ 1/x into the reflected parameter. Upstream cost definitions supply the concrete function J: one from the comparator of a multiplicative recognizer and one from the J-cost of a recognition event. The module document states that the zeta functional equation ξ(s) = ξ(1-s) arises as the Mellin pullback of this symmetry of J.
proof idea
The definition is a direct abbreviation that states the predicate as ∀ x > 0, f x = f (1/x). It serves as a one-line interface predicate with no lemma applications or tactic steps.
why it matters
This predicate supplies the first structural hypothesis in the Mellin pullback certificate, which records reciprocal symmetry of J, evenness of J(e^t), and the kernel substitution that yields reflection at 1-s. It feeds the MellinAdmissibleKernel structure and the theorem that J is a reciprocally symmetric Mellin input. The definition therefore occupies the precise slot that converts the Recognition Science cost symmetry into the abstract precursor of the zeta functional equation before complex analysis is introduced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.