IdentityRecognitionZero
plain-language theorem explainer
Predicate on a real map F asserting it is a ledger cost function in ratio form: F(A/B) matches recognition log-cost for positive A,B. Cited when deriving unit normalization F(1)=0 from identity postings in the T5 constraint-forcing chain. Definitionally identical to the cost-function interface; no separate proof content.
Claim. A map $F:\mathbb{R}\to\mathbb{R}$ satisfies identity-recognition-zero when it is a cost function: 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 calibration. The resolution is that reciprocal symmetry and unit normalization are derived from the T3 double-entry ledger, not postulated; curvature remains a gauge choice.
A cost function here means a real map that, on positive ratios, reproduces recognition log-cost: $F(A/B)=\mathrm{RecognitionLogCost}(A,B)$ whenever $A,B>0$. Identity postings $A\to A$ record no ledger change, so the cost of doing nothing is the zero baseline. That ledger fact is what the unit-normalization half of the forcing argument packages under this name.
Upstream, the cost-function interface is exactly that ratio agreement with recognition log-cost. The display map $F(Z)=\log(1+Z/\varphi)/\log\varphi$ from anchor policy is a separate integer-gap alias and is not the $F$ quantified here.
proof idea
Pure definition: the body is a one-line abbreviation equating the predicate to the existing cost-function interface. No tactics, no lemmas applied, no proof obligations.
why it matters
Feeds the second conjunct of t5_constraints_are_forced: every cost function in this sense is unit-normalized ($F(1)=0$). That theorem's doc states the two ledger-derived T5 constraints explicitly, and excludes curvature calibration and the composition law as not forced.
In the Recognition forcing chain this closes the T5 objection that $F(1)=0$ was an arbitrary assumption. Together with exchange-invariance forcing reciprocal symmetry, it lets uniqueness of $J(x)=(x+x^{-1})/2-1$ (T5) rest on ledger structure rather than free choice of constraints. Curvature $F''(0)=1$ stays a gauge normalization and is intentionally outside this predicate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.