t5_constraints_forced_from_ledger
plain-language theorem explainer
Any cost functional compatible with a double-entry ledger automatically satisfies the two T5 structural constraints: reciprocal symmetry F(x)=F(x^{-1}) for x>0 and unit normalization F(1)=0. Citation target for anyone closing the "who chose the T5 assumptions" gap. The proof is a one-line re-export of the ledger-forcing theorem from LedgerCost.
Claim. For every ledger-compatible cost functional $F$, one has $F(x)=F(x^{-1})$ for all $x>0$, and $F(1)=0$.
background
The module answers the objection that T5 uniqueness of the J-cost rests on unmotivated constraints $F(x)=F(1/x)$ and $F(1)=0$. Those constraints are here derived from the ledger (T3), not postulated.
A ledger is a list of recognition events with a double-entry balance condition: every debit has a matching credit. The reciprocal of an event swaps source and target and inverts the ratio. Ledger-compatible cost functionals are those whose cost is insensitive to this double-entry structure in the sense formalized by LedgerCost.
Upstream, reciprocal symmetry is forced because posting $A\to B$ and $B\to A$ are the same transaction from opposite sides, so $F(A/B)=F(B/A)$. Unit normalization is forced because an identity posting $A\to A$ records no change and therefore carries zero cost. Curvature normalization $F''(0)=1$ remains a gauge choice and is not claimed here.
proof idea
One-line term proof: the statement is exactly the conclusion of LedgerCost.ledger_forces_t5_constraints, applied to the given ledger-compatible functional. No local case analysis; the work lives in the LedgerCost derivation (double-entry symmetry plus identity-posting zero).
why it matters
Closes Gap 4 in the T5 verification chain: the symmetry and normalization hypotheses of J-uniqueness (forcing landmark T5, with $J(x)=(x+x^{-1})/2-1$) are no longer free parameters but consequences of the ledger (T3). Downstream, t5_constraints_imply_reciprocal_from_ledger projects the bundle onto the reciprocal half alone via the first conjunct. Together these feed the constraint-forcing story that makes T5 unconditional on ad hoc cost axioms, leaving only the curvature gauge as a unit convention. Directly supports the Recognition Composition Law setup, which needs reciprocal symmetry of the cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.