LedgerCostFunctional
plain-language theorem explainer
A bare cost functional is a map F from real ratios to reals, the carrier for ledger-derived T5 constraints. Anyone proving reciprocal symmetry or unit normalization from double-entry bookkeeping cites this type. It is a one-field structure; positivity lives on postings, not on F itself.
Claim. A ledger cost functional is a structure consisting of a single map $F:\mathbb{R}\to\mathbb{R}$ (the cost on ratios). The cost of a posting with source $A>0$ and target $B>0$ is $F(A/B)$.
background
The module derives two of the T5 cost constraints from ledger structure (T3) and proves a no-go for the third. A ledger posting is a transition between two positive reals; its ratio $A/B$ is the exchange rate of the move. Double-entry bookkeeping treats $A\to B$ and $B\to A$ as the same transaction from opposite sides, so any admissible cost must satisfy $F(x)=F(1/x)$. The identity posting (no change) must cost zero, forcing $F(1)=0$.
T5 uniqueness of $J(x)=\frac12(x+x^{-1})-1$ still needs the independent composition law (Cosh-Add / RCL). The module's honest chain is: ledger $\Rightarrow$ symmetry and unit; C6 remains a load-bearing hypothesis, with quadratic witness $G(t)=t^2/2$ refuting overclaim that continuity plus calibration force Cosh-Add.
proof idea
Definitional, not a proof. The structure packages one field cost : ℝ → ℝ. The associated posting cost is the one-line evaluation $F(\mathrm{ratio}(p))=F(A/B)$. An earlier vacuous domain field was removed; positivity is enforced by the posting's source/target hypotheses, not by a predicate on $F$.
why it matters
This is the carrier type for the T3-to-T5 bridge in the forcing chain. Downstream, ledger compatibility (double-entry plus zero identity cost) is stated on this type, and ledger_forces_t5_constraints concludes $F(x)=F(x^{-1})$ for $x>0$ and $F(1)=0$. ConstraintForcing re-exports the same bundle as t5_constraints_forced_from_ledger, feeding the abstract T5 interface.
In the primer landmarks this supplies the ledger half of T5 (reciprocal symmetry and unit), not J-uniqueness itself. The composition law C6 and calibration remain independent; the module's no-go certificate blocks any claim that T5 is unconditionally forced from T1–T4 alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.