reciprocal_symmetry_forced
plain-language theorem explainer
Any real cost function tied to the ledger log-cost is forced to obey F(x)=F(1/x) for every positive x. Citation target for the T5 uniqueness program: reciprocal symmetry is not an extra axiom but a consequence of double-entry exchange. The proof rewrites both sides as the same RecognitionLogCost via the exchange-invariance axiom.
Claim. Let $F:\mathbb{R}\to\mathbb{R}$ be a cost function in the sense that $F(A/B)$ equals the recognition log-cost of the pair $(A,B)$ whenever $A,B>0$. Then for every $x>0$, $F(x)=F(x^{-1})$.
background
This module answers the objection that T5 uniqueness of the J-cost rests on hand-picked constraints $F(x)=F(1/x)$, $F(1)=0$, and curvature normalization. The claim here is that reciprocal symmetry is forced by the ledger, not assumed.
A function $F$ is a cost function when it agrees with the abstract recognition log-cost on positive ratios: $F(A/B)=\mathrm{RecognitionLogCost}(A,B)$. The ledger is double-entry, so posting $A\to B$ and posting $B\to A$ are the same transaction from opposite sides; that exchange invariance is the axiom used below.
In ratio coordinates the same fact reads $F(A/B)=F(B/A)$, i.e. $F(x)=F(x^{-1})$. The companion unit-normalization constraint $F(1)=0$ is forced separately by identity postings; curvature $F''(0)=1$ remains a gauge choice.
proof idea
Tactic proof. Fix $x>0$. Unfold the cost-function hypothesis to obtain $F(x)=\mathrm{RecognitionLogCost}(x,1)$ and $F(x^{-1})=\mathrm{RecognitionLogCost}(x^{-1},1)$.
Rewrite the first identity by the exchange-invariance axiom, swapping arguments so $\mathrm{RecognitionLogCost}(x,1)=\mathrm{RecognitionLogCost}(1,x)$.
Separately apply the cost-function hypothesis to the pair $(1,x)$: since $x^{-1}=1/x$, one gets $F(x^{-1})=\mathrm{RecognitionLogCost}(1,x)$.
Both sides therefore equal $\mathrm{RecognitionLogCost}(1,x)$, and the desired equality follows by rewriting.
why it matters
This is Constraint 1 in the T5 forcing chain: reciprocal symmetry is derived from T3 ledger structure rather than postulated. It feeds the package theorem t5_constraints_are_forced, which records that exchange invariance implies reciprocal symmetry and identity recognition implies unit normalization.
In the broader Recognition Science forcing chain this is the symmetry half of the T5 J-uniqueness package (the unique cost is $J(x)=(x+x^{-1})/2-1$). The same reciprocal identity appears as R2 in the closed-observable framework, where mismatch quantified by ratios is invariant under state swap.
Curvature calibration and the composition law are deliberately not claimed forced here; the module flags them as gauge and as open relative to the ledger derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.