unit_normalization_forced
plain-language theorem explainer
Any real cost function tied to recognition log-cost must vanish at unit ratio: F(1) = 0. This is the T5 unit-normalization constraint derived from identity recognition (ledger self-posting costs nothing), not postulated. Cite it when closing the Gap-4 objection that T5 normalizations are free assumptions. The proof rewrites F(1) as F(1/1), applies the cost-function interface, then invokes the identity-cost axiom.
Claim. If $F:\mathbb{R}\to\mathbb{R}$ is 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 $F(1)=0$.
background
Module Gap 4 answers the critique that T5 uniqueness of $J$ rests on free constraints $F(x)=F(1/x)$, $F(1)=0$, and $F''(0)=1$. The module derives the first two from ledger structure (T3) and treats curvature as a gauge choice.
A cost function here means $F(A/B)$ coincides with recognition log-cost for positive $A,B$. That abstract cost is the squared log-ratio $(\log A-\log B)^2$ (zero on non-positive inputs), built so exchange is symmetric and self-comparison is free. The identity axiom states that recognition cost of any pair $(A,A)$ is zero: an identity posting records no ledger change.
Unit normalization is the log-coordinate form of that fact: ratio $1$ is self-comparison, so $F(1)$ must be the zero baseline.
proof idea
Unfold the cost-function hypothesis. Show $F(1)=F(1/1)$ by $1/1=1$, then apply the interface at $A=B=1$ (both positive) to obtain $F(1)=$ recognition log-cost of $(1,1)$. Finish by the identity-recognition axiom at $A=1$, which gives that cost is zero. Short tactic proof: one algebraic rewrite plus the identity axiom.
why it matters
Feeds t5_constraints_are_forced, which packages the two ledger-derived T5 constraints: reciprocal symmetry from exchange invariance, and unit normalization from identity recognition. Curvature calibration and the composition law are deliberately excluded there as not forced.
In the forcing chain this discharges Constraint 2 of T5 (J-uniqueness): $F(1)=0$ is no longer an external normalization but a consequence of double-entry identity postings. Matches the module claim that unit normalization is forced from identity posting, parallel to reciprocal symmetry from double entry. Downstream closed-observable packaging treats the same fact as R2 (self-comparison forces $J(1)=0$). Together these close the Gap-4 objection for the unit constraint while leaving curvature as gauge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.