LedgerCompatible
plain-language theorem explainer
A cost functional on ledger postings is ledger-compatible when it respects double-entry bookkeeping and assigns zero cost to every identity posting (source equals target). Anyone deriving the T5 reciprocal-symmetry and unit-normalization constraints from ledger structure (T3) cites this interface. It is a Prop-valued structure packing those two axioms; there is no proof body.
Claim. A cost functional $F$ (a map from positive ratios to reals, evaluated on ledger postings via their source/target ratio) is ledger-compatible if (i) $F$ respects double-entry bookkeeping, and (ii) for every posting $p$ with source equal to target, the posting cost of $p$ under $F$ is zero.
background
This module sits in the T5 verification path: it derives two of the T5 cost constraints from ledger structure (T3) and records a no-go that the remaining Cosh-Add (composition) law cannot be obtained from those plus continuity.
A ledger posting is a transition between two positive reals; its ratio is source/target. A ledger cost functional is simply a real-valued cost on positive ratios, with posting cost $F(\mathrm{ratio}(p))$. Upstream ledger language treats a ledger as recognition events under a double-entry balance constraint, and the identity event sits at the J-cost minimum $x=1$ with zero cost.
Ledger compatibility packages the two bookkeeping demands used downstream: double-entry respect, and zero cost on identity postings. The module's honest chain is T3 → reciprocal symmetry and unit normalization, while C6 (Cosh-Add) remains an independent hypothesis.
proof idea
Definitional Prop structure, not a proved theorem. It bundles two fields on a cost functional $F$: double_entry (the double-entry respect predicate on $F$) and zero_identity (every posting with equal source and target has posting cost zero). No tactics or lemmas; downstream theorems unpack the fields.
why it matters
This is the hypothesis interface for the module's main forcing theorem ledger_forces_t5_constraints, which concludes reciprocal symmetry $F(x)=F(1/x)$ and unit normalization $F(1)=0$ from ledger compatibility. The ConstraintForcing layer re-exports that bundle as t5_constraints_forced_from_ledger and projects out reciprocal symmetry for the abstract T5 cost interface.
In the Recognition forcing chain this is the T3→T5 bridge for two physical constraints only. The module doc is explicit that Cosh-Add (composition law C6 / RCL shape) does not follow from symmetry, unit, continuity, and curvature calibration; the witness $G(t)=t^2/2$ and aczel_hypothesis_refuted keep T5's full uniqueness (J-uniqueness, primer T5) conditional on C6 as a load-bearing hypothesis rather than a ledger corollary.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.