IndisputableMonolith.Verification.T5.LedgerCost
Defines ledger postings (transitions between positive values with exchange ratio A/B) and a cost functional on those ratios, then forces the classical T5 constraint package from double-entry bookkeeping. Symmetry under inversion, vanishing at the identity posting, and a quadratic local witness are derived rather than assumed. ConstraintForcing imports the module to answer who chose the T5 normalizations. The argument is definitional setup plus a short chain of forcing lemmas.
claimA ledger posting is a transition between positive values $A,B>0$ with exchange ratio $r=A/B$. A ledger-compatible cost $F:(0,\infty)\to\mathbb{R}$ is forced by double-entry and identity postings to satisfy $F(r)=F(1/r)$, $F(1)=0$, and to admit a quadratic local witness (the T5 constraint package that pins $J(x)=(x+x^{-1})/2-1$).
background
Recognition Science derives the unique cost $J$ at T5 of the forcing chain: $J(x)=(x+x^{-1})/2-1=\cosh(\log x)-1$, subject to symmetry $F(x)=F(1/x)$, normalization $F(1)=0$, and a curvature/normalization condition. The usual critique is that those constraints look chosen by hand.
This module answers in ledger language. A ledger posting records a transition between two positive values; the ratio $A/B$ is the exchange rate of the transition. The cost functional scores such ratios. Double-entry bookkeeping and the identity posting (ratio $1$) are the only structural inputs.
Upstream, the Recognition import supplies the T1 meta-principle (nothing cannot recognize itself) and RecogSpec.Core the shared specification surface. Downstream ConstraintForcing consumes the forced constraints to close Gap 4 on T5 uniqueness.
proof idea
Definition module plus a short forcing chain, not a single theorem. It introduces LedgerPosting and LedgerCostFunctional, then proves symmetry_forced_from_double_entry (inversion symmetry of the cost from balanced debit/credit) and unit_forced_from_identity_posting ($F(1)=0$). Log-ratio additivity and LedgerCompatible package the bookkeeping axioms. The capstone ledger_forces_t5_constraints assembles those into the full T5 constraint set. Supporting pieces include CoshAddFromLedger, an Aczél-style hypothesis interface, and quadraticWitness (with evenness and zero-at-origin lemmas) for the local curvature normalization.
why it matters in Recognition Science
Closes the "who chose the constraints?" objection to T5 J-uniqueness. ConstraintForcing imports this module expressly for Gap 4: T5 proves $J$ unique given symmetry and normalization, but those had looked like free assumptions. By deriving $F(x)=F(1/x)$, $F(1)=0$, and the quadratic witness from double-entry ledger structure, the module makes the T5 hypotheses bookkeeping theorems rather than modeling choices. That anchors the Recognition Composition Law and the explicit form $J(x)=\cosh(\log x)-1$ in a physical accounting principle, feeding the rest of the T5 verification stack and the broader T0–T8 forcing chain.
scope and limits
- Does not prove full T5 uniqueness of J; only forces the constraint package used by uniqueness.
- Does not derive the Recognition Composition Law or the closed form of J inside this module.
- Does not address dimensional forcing (T8) or the eight-tick octave (T7).
- Does not discharge the Aczél hypothesis interface; that remains a named open assumption.
- Does not claim empirical ledger data; the argument is structural double-entry only.
used by (1)
depends on (2)
declarations in this module (17)
-
structure
LedgerPosting -
structure
LedgerCostFunctional -
theorem
symmetry_forced_from_double_entry -
theorem
unit_forced_from_identity_posting -
lemma
log_ratio_additive -
structure
LedgerCompatible -
theorem
ledger_forces_t5_constraints -
def
CoshAddFromLedger -
def
aczel_theorem_3_1_3_hypothesis -
def
quadraticWitness -
lemma
quadraticWitness_even -
lemma
quadraticWitness_zero -
lemma
quadraticWitness_continuous -
lemma
quadraticWitness_deriv -
lemma
quadraticWitness_second_deriv -
lemma
quadraticWitness_not_coshAdd -
theorem
aczel_hypothesis_refuted