LedgerPosting
plain-language theorem explainer
A ledger posting is a pair of strictly positive reals (source, target) recording one double-entry transition. Its ratio is the exchange rate source/target; the inverse swaps the legs and the identity posting has equal legs. Anyone deriving T5 cost constraints from T3 ledger structure cites this carrier type. It is a pure structure definition with positivity fields, not a theorem.
Claim. A ledger posting is a pair of real numbers $(s,t)$ with $s>0$ and $t>0$, interpreted as a transition from source $s$ to target $t$. The associated ratio is $s/t$; the inverse posting is $(t,s)$; the identity posting at $x>0$ is $(x,x)$ and has ratio $1$.
background
This module sits in the T5 verification chain: it extracts two cost constraints from the T3 ledger (double-entry bookkeeping) and proves a no-go for the third. The honest chain is: ledger structure forces reciprocal symmetry $F(x)=F(1/x)$ and unit normalization $F(1)=0$; the Cosh-Add (d'Alembert) composition law is independent and not forced by symmetry plus unit plus continuity.
A posting is the atomic ledger event: two positive values and the exchange rate between them. Positivity is enforced on the posting itself so later cost functionals need not carry a vacuous domain field. The ratio, inverse, and identity constructions are the elementary operations used when stating double-entry symmetry and zero cost of a null entry.
Upstream ledger and cost language (recognition cost under a ratio weight, ledger forcing) supplies the ambient bookkeeping; this structure is the local carrier those arguments quantify over.
proof idea
Definitional, not a proof. The structure packages two reals with two positivity proofs. The companion definitions are immediate: ratio is source/target; inverse swaps fields and reuses the positivity proofs; identity sets both legs equal. The two ratio lemmas are short simp plus field_simp after nonzero facts from positivity.
why it matters
This is the data type on which the module's main T5 ledger results are stated: symmetry forced from double entry, unit forced from the identity posting, ledger-compatibility of a cost functional, and the no-go that symmetry+unit+continuity+calibration do not force Cosh-Add (witness $G(t)=t^2/2$). Without a positive-ratio posting, the reciprocal and unit constraints cannot even be typed.
In the Recognition forcing chain, T5 is J-uniqueness with $J(x)=\frac12(x+x^{-1})-1$. The module's honest claim is that only two of the T5 constraints drop out of T3; composition remains an independent load-bearing hypothesis. The posting structure is the first brick of that corrected derivation path after the retracted "unconditionally forced" claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.