UnitNormalized
plain-language theorem explainer
Unit normalization is the predicate that a real cost function vanishes at the identity ratio: F(1)=0. It packages the ledger baseline that an identity posting carries zero cost. Downstream T5 forcing cites it as the target of the identity-recognition implication. The body is a one-line Prop abbreviation, not a proof.
Claim. A real function $F:\mathbb{R}\to\mathbb{R}$ is unit-normalized when $F(1)=0$.
background
Gap 4 of the T5 verification stack answers the objection that uniqueness of the J-cost rests on unmotivated side conditions. The module derives the genuine constraints from the double-entry ledger (T3) rather than assuming them.
Unit normalization is the second of those constraints. An identity posting $A\to A$ records no debit or credit, so the cost of "doing nothing" is the zero baseline. In ratio language this is $F(1)=0$. The companion reciprocal-symmetry constraint $F(x)=F(1/x)$ comes from exchange invariance of the same ledger; curvature normalization $F''(0)=1$ is treated separately as a gauge choice, not a forced physical law.
The formal forcing theorem in LedgerCost is unit_forced_from_identity_posting. This definition is only the target Prop that those lemmas discharge.
proof idea
No proof. The declaration is a one-line Prop abbreviation equating the named predicate with the atomic equality $F,1=0$. Downstream theorems supply the content by showing that identity-recognition-zero hypotheses imply this equality.
why it matters
T5 J-uniqueness (forcing-chain landmark T5) needs a clean statement of which side conditions are forced versus gauge. This predicate is the second conjunct of t5_constraints_are_forced, which asserts that every cost satisfying identity recognition is unit-normalized. Together with reciprocal symmetry forced by exchange invariance, it closes the "who chose the constraints?" critique for the two ledger-derived axioms.
Curvature calibration and the Recognition Composition Law are deliberately excluded from that summary theorem: the module docstring and LedgerCost.aczel_hypothesis_refuted record that those are not forced. Keeping unit normalization as a named Prop makes that honesty cut precise and reusable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.