RecognitionLogCost
plain-language theorem explainer
Abstract recognition cost between two reals equals the squared log-ratio when both are positive, and zero otherwise. T5 constraint-forcing work cites it as the concrete two-argument cost that makes exchange symmetry and identity-zero immediate. The body is a piecewise formula, not a derived theorem.
Claim. For $A,B\in\mathbb{R}$, the recognition log-cost is $(\log A-\log B)^2$ if $A>0$ and $B>0$, and equals $0$ if $A\le 0$ or $B\le 0$.
background
This module answers the Gap-4 critique of T5: uniqueness of the cost $J$ is conditional on reciprocal symmetry $F(x)=F(1/x)$, unit normalization $F(1)=0$, and a curvature gauge $F''(0)=1$. The module's claim is that the first two constraints are forced by ledger double-entry structure (T3), not free assumptions; curvature is only a unit choice.
The two-argument recognition cost is the bridge object. On positive reals it is the squared log-ratio $(\log A-\log B)^2$, which is exchange-symmetric and vanishes on the diagonal. A predicate later says a univariate $F$ is a cost function precisely when $F(A/B)$ recovers this value for all positive $A,B$. Upstream ledger-cost material supplies the double-entry and identity-posting stories that justify those algebraic properties; the $A$/$B$ name collisions in the dependency graph are unrelated constants (active-edge counts, interface sets), not inputs here.
proof idea
Definition only: branch on $A\le 0\lor B\le 0$ and return $0$; otherwise return $(\mathrm{Real.log},A-\mathrm{Real.log},B)^2$. No lemmas are applied. Downstream theorems unfold this definition and case-split on the same guards.
why it matters
This is the concrete cost that T5 constraint-forcing hangs on. IsCostFunction ties a univariate $F$ to it by $F(A/B)=\mathrm{RecognitionLogCost}(A,B)$. From that link one gets reciprocal symmetry $F(x)=F(x^{-1})$ and unit normalization $F(1)=0$ as forced theorems, plus the direct exchange and identity axioms on the two-argument cost itself.
In the Recognition forcing chain this supports T5 (J-uniqueness): once exchange and identity are forced from the ledger and the cost is identified with the log-ratio square, the admissible $F$ collapse toward $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), up to the curvature gauge. It does not close uniqueness alone; it supplies the cost interface the forcing lemmas quote.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.