IsReciprocalCost
A cost function F from positive reals to reals is reciprocal when F(x) equals F at the reciprocal argument for every positive x. Researchers proving T5 uniqueness of the canonical cost algebra in Recognition Science cite this as the opening symmetry axiom. The declaration is introduced directly as a predicate with no derivation steps required.
claimA function $F : (0,∞) → ℝ$ is reciprocal when $F(x) = F(x^{-1})$ holds for all $x > 0$.
background
The Cost.FunctionalEquation module supplies lemmas supporting the T5 step of the forcing chain. Cost functions are required to obey the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). The reciprocal property encodes invariance under x ↦ 1/x. Upstream results define the master gap function F(z) := log(1 + z/φ) and the even extension G(t) := F(e^t). Sibling lemmas such as Jcost_G_eq_cosh_sub_one and reciprocal_implies_G_even connect reciprocity to the evenness of G and the explicit form J(x) = cosh(log x) - 1.
proof idea
This is the direct definition of the reciprocity predicate. It encodes the statement ∀ x > 0, F(x) = F(x^{-1}) and serves as the hypothesis type passed to downstream results such as washburn_uniqueness and PrimitiveCostHypotheses.
why it matters in Recognition Science
The definition supplies the reciprocity axiom required by washburn_uniqueness (the main T5 result) and by cost_algebra_unique, both of which conclude that any function meeting reciprocity, normalization, the composition law, and calibration must equal the J-cost. It appears as the first field in PrimitiveCostHypotheses, the canonical input bundle for the uniqueness theorem. In the framework it records the symmetry forced at T5 J-uniqueness in the T0-T8 chain.
scope and limits
- Does not impose continuity or differentiability on F.
- Does not assert the composition law or normalization.
- Does not specify the explicit form of F.
- Does not constrain behavior at zero or infinity.
formal statement (Lean)
593def IsReciprocalCost (F : ℝ → ℝ) : Prop :=
proof body
Definition body.
594 ∀ x : ℝ, 0 < x → F x = F x⁻¹
595
596/-- **Normalized**: F(1) = 0. -/