ExchangeInvariant
plain-language theorem explainer
Exchange invariance of a real map F means F is a ledger cost function: on every positive ratio it equals the recognition log-cost of the two legs. Anyone citing the forced T5 reciprocal-symmetry step uses this predicate as the hypothesis that encodes double-entry exchange. The body is a one-line alias of the cost-function predicate.
Claim. A function $F:\mathbb{R}\to\mathbb{R}$ is exchange-invariant when it is a cost function in the ledger sense: for all $A,B>0$, $F(A/B)$ equals the recognition log-cost of the pair $(A,B)$.
background
Module Gap 4 answers the critique that T5 uniqueness of $J$ rests on unmotivated constraints $F(x)=F(1/x)$, $F(1)=0$, and curvature normalization. The resolution is that the first two constraints are derived from the T3 ledger, not postulated; curvature is only a gauge choice.
A cost function here is any $F$ that, on positive ratios, reproduces the recognition log-cost of the two legs: $F(A/B)=\mathrm{RecognitionLogCost}(A,B)$ whenever $A,B>0$. That identification is the content of IsCostFunction. In the double-entry ledger every debit has a matching credit, so the cost of posting $A\to B$ equals the cost of $B\to A$; in ratio coordinates that is exchange invariance.
The display map $F(Z)=\log(1+Z/\varphi)/\log(\varphi)$ from AnchorPolicy is a separate gap function and is not the $F$ quantified here; the present predicate is abstract over any real map that matches recognition log-cost on ratios.
proof idea
Pure definitional alias: ExchangeInvariant F is definitionally equal to IsCostFunction F. No tactics, no lemmas, no proof obligations. Downstream theorems unfold or rewrite through this name when they need the exchange-invariance hypothesis in ledger language rather than the ratio-cost language.
why it matters
This predicate is the ledger-side packaging of the first forced T5 constraint. The parent theorem t5_constraints_are_forced states that every exchange-invariant $F$ is reciprocally symmetric, and every identity-recognition-zero $F$ is unit-normalized; its first conjunct is exactly $\forall F,,\mathrm{ExchangeInvariant},F\to\mathrm{ReciprocalSymmetric},F$.
In the Recognition forcing chain this closes the "who chose the constraints?" objection for reciprocal symmetry: the constraint is inherited from T3 double-entry structure (formalized in LedgerCost as symmetry forced from double entry), not assumed ad hoc. Curvature calibration and the composition law are deliberately excluded from that parent theorem; they are not forced in the same sense. The definition therefore sits at the interface between ledger cost and the T5 uniqueness argument for $J(x)=(x+x^{-1})/2-1$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.