IsCostFunction
plain-language theorem explainer
A real map F counts as a cost function when its value on every positive ratio A/B equals the recognition log-cost of the pair (A,B). Anyone working the T5 uniqueness argument or the forced ledger constraints cites this predicate as the standing hypothesis on F. It is a pure definition: the Prop is the universal equation linking ratio coordinates to abstract ledger cost.
Claim. A map $F:\mathbb{R}\to\mathbb{R}$ is a cost function when, for all $A,B>0$, $F(A/B)$ equals the recognition log-cost of the ordered pair $(A,B)$.
background
Module Gap 4 answers the objection that T5 uniqueness of the J-cost rests on unmotivated side conditions $F(x)=F(1/x)$, $F(1)=0$, and $F''(0)=1$. The resolution is that the first two constraints are derived from the T3 double-entry ledger, while curvature normalization is only a gauge choice.
The recognition log-cost is the abstract ledger cost of a recognition event between two positive quantities. Passing to ratio coordinates $x=A/B$ converts that two-argument cost into a one-argument function $F$ on the positive reals. The present definition packages exactly that conversion: $F$ is a cost function when it agrees with the recognition log-cost on every positive ratio.
Upstream ledger structure supplies the reciprocal event (swap source and target, invert the ratio) and the identity posting (no debit or credit). Those force the classical T5 side conditions once $F$ is known to be a cost function in this sense.
proof idea
Definitional, not a theorem. The body is the single Prop $\forall A,B>0,; F(A/B)=\mathrm{RecognitionLogCost}(A,B)$. No tactics, no lemmas, no sorry. Downstream theorems unfold this definition and specialize $A,B$ to recover reciprocal symmetry and unit normalization.
why it matters
This is the interface predicate between ledger-derived cost and the classical T5 hypotheses. Downstream, both ExchangeInvariant and IdentityRecognitionZero are defined to be exactly this predicate, so the two forced constraints share one standing assumption on $F$.
The theorems reciprocal_symmetry_forced and unit_normalization_forced take a cost-function hypothesis and discharge $F(x)=F(x^{-1})$ and $F(1)=0$ respectively, which are the symmetry and normalization inputs to T5 J-uniqueness ($J(x)=(x+x^{-1})/2-1$). Curvature $F''(0)=1$ remains a gauge choice and is handled separately in the same module.
Without this definition the forced-constraint story would have no single place to say "F is the ratio form of ledger cost," and the T5 uniqueness chain would still look like an assumption package rather than a derivation from T3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.