IsReciprocalCost
plain-language theorem explainer
The definition encodes the reciprocity axiom for a cost function F on positive reals, requiring F(x) to equal F at the reciprocal argument for every x > 0. Researchers proving uniqueness of the J-cost at T5 cite this symmetry when assembling the PrimitiveCostHypotheses bundle. It is implemented as a direct predicate that packages the inversion invariance without further derivation.
Claim. A function $F : (0,∞) → ℝ$ satisfies reciprocity when $F(x) = F(x^{-1})$ holds for every $x > 0$.
background
The module supplies lemmas that support the T5 cost uniqueness argument in the forcing chain. Reciprocal cost is one of five primitive hypotheses collected in the PrimitiveCostHypotheses structure, alongside normalization, the composition law, calibration, and continuity on the positive reals. Upstream generating functions such as log(1 + z/φ) supply the gap values that later calibrate the same cost functions.
proof idea
The declaration is a direct definition that asserts the equality under the positivity guard. No lemmas or tactics are invoked; the predicate simply records the mathematical symmetry for consumption by downstream results such as reciprocal_implies_G_even.
why it matters
It supplies the reciprocity hypothesis to washburn_uniqueness and cost_algebra_unique, the two theorems that conclude the cost must equal J at the T5 J-uniqueness step. The same predicate appears inside PrimitiveCostHypotheses and is derived from the composition law under normalization by composition_law_forces_reciprocity. The property is required before the even extension G(t) = F(e^t) can be formed and before the d'Alembert reduction proceeds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 2 of 2)
-
Multidimensional cost geometry
"Permutation symmetry plus reduction to 1D when all variables coincide forces αᵢ = 1/n; the cost depends only on the geometric mean (xᵢ-form) or arithmetic mean (tᵢ-form)."
-
A Noble-Gas-Centered Coordinate for Within-Period Atomic Property Trends
"The model's input cost function J is the unique solution on R>0 of the functional equation J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y), under the regularity conditions ... The unique solution is J(x) = ½(x + x⁻¹) − 1 = cosh(ln x) − 1 (Corollary 3.1 of Ref. [5])."