t5_constraints_imply_reciprocal_from_ledger
plain-language theorem explainer
Any ledger-compatible cost functional on positive reals is reciprocal: F(x) = F(x^{-1}). Citation target for the T5 uniqueness program when the symmetry constraint must be derived from double-entry bookkeeping rather than postulated. Proof is a one-line projection of the forced T5 constraint bundle.
Claim. Let $F$ be a ledger cost functional that is ledger-compatible. Then for every $x > 0$, $F(x) = F(x^{-1})$.
background
This module closes Gap 4 in the T5 uniqueness story: the critique that reciprocal symmetry, unit normalization, and curvature normalization are free assumptions. The resolution is that the first two are forced by the ledger (T3), while curvature is a gauge choice.
A ledger is a double-entry collection of recognition events: 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 induced by this structure, so the cost of posting A→B equals the cost of B→A.
In ratio language that identity is $F(A/B) = F(B/A)$, i.e. $F(x) = F(x^{-1})$. The companion module LedgerCost supplies the formal derivation from double-entry; the present theorem packages the reciprocal half of the forced T5 constraint bundle for downstream use.
proof idea
One-line term proof. Apply the forced T5 constraint bundle theorem for ledger-compatible functionals, then project the first component (reciprocal symmetry) and specialize at the given positive $x$. No extra algebraic work.
why it matters
Feeds the standard-named alias t5_constraints_implies_reciprocal_from_ledger in the same module, and sits inside the T5 forcing chain: once reciprocal symmetry and unit normalization are ledger-forced, J-uniqueness (T5) no longer rests on free axioms. Framework landmark: T5 J-uniqueness with $J(x) = (x + x^{-1})/2 - 1$, whose functional equation presupposes $F(x) = F(x^{-1})$. This declaration is the verification-layer witness that the symmetry half of those constraints is derived from T3 double-entry, answering the "who chose the constraints?" objection for reciprocal symmetry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.