ReciprocalSymmetric
plain-language theorem explainer
Predicate on a real cost function requiring F(x)=F(1/x) for every positive x. Used when packaging the T5 ledger-derived constraints that force uniqueness of the J-cost. Pure definition: the body is the quantified equality, with no proof obligations.
Claim. A map $F:\mathbb{R}\to\mathbb{R}$ is reciprocal-symmetric when $F(x)=F(x^{-1})$ holds for every $x>0$.
background
This module answers the objection that T5 uniqueness of the cost $J$ rests on unmotivated side conditions. The local claim is that the classical constraints are not free assumptions: reciprocal symmetry and unit normalization are forced by the double-entry ledger (T3), while curvature normalization is only a gauge choice.
Reciprocal symmetry is the ratio form of exchange invariance. In a double-entry ledger every debit has a matching credit, so the cost of posting $A\to B$ equals the cost of $B\to A$. Writing $x=A/B$ yields $F(x)=F(1/x)$. The sibling predicate for exchange invariance and the ledger theorem symmetry_forced_from_double_entry supply that derivation; the present definition only names the resulting functional property.
The T5 uniqueness chain (forcing landmark T5) then takes this property, together with $F(1)=0$, as input to pin $J(x)=(x+x^{-1})/2-1$.
proof idea
Definitional abbreviation, not a theorem. The body is the single Prop $\forall x,, 0<x\to F(x)=F(x^{-1})$. No tactics, lemmas, or reductions are involved; downstream theorems simply unfold or apply this predicate.
why it matters
Names the first of the two ledger-forced T5 constraints. The parent theorem t5_constraints_are_forced packages exactly this: every exchange-invariant cost is reciprocal-symmetric, and every identity-zero cost is unit-normalized. Curvature calibration and the composition law are deliberately excluded there, matching the module correction that only the ledger-derived pair is forced.
In the broader forcing chain this is the symmetry half of T5 J-uniqueness: once $F(x)=F(1/x)$ and $F(1)=0$ are on the table, the Recognition Composition Law and normalization select $J(x)=\cosh(\log x)-1$. Without a named predicate the forced-constraint theorem cannot state its first conjunct cleanly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.