LedgerComparisonCertificate
plain-language theorem explainer
Phase 3 certificate packaging positive-ratio comparison on a closed observable ledger with the equivalence of d'Alembert factorization existence to cost-determined combination, plus non-vacuity for the recognition cost J. Anyone closing the ledger-to-J forcing path after composition cites this bundle. It is a definitional Prop structure; the inhabiting theorem wires five already-proved field lemmas.
Claim. A Phase 3 certificate asserting: (1) in any closed observable framework, the comparison of two states is a strictly positive ratio of observables; (2) swapping the two states inverts that ratio; (3) self-comparison is the unit ratio $1$; (4) a cost $F:\mathbb{R}\to\mathbb{R}$ admits a binary combiner $P$ with $F(xy)+F(x/y)=P(Fx,Fy)$ if and only if the symmetric combination is determined solely by the pair of single-point costs $(Fx,Fy)$; (5) the recognition cost $J(x)=(x+x^{-1})/2-1$ has cost-determined combination.
background
A ClosedObservableFramework carries a state space $S$, dynamics $T$, and a strictly positive observable $r:S\to\mathbb{R}$ (with nontriviality). The comparison object is the ratio $\mathrm{compRatio}(s_1,s_2)=r(s_1)/r(s_2)$. Positivity, swap-inversion, and self-unit are read off $r>0$, not postulated as analytic domain axioms for $J$.
The recognition cost is $J(x)=(x+x^{-1})/2-1$ on the positive ray. Multiplicative consistency (d'Alembert input) means existence of a combiner $P$ with $F(xy)+F(x/y)=P(Fx,Fy)$. This module rephrases that existence as cost-determined combination: $F(x_1 y_1)+F(x_1/y_1)$ depends only on the pair $(F x_1, F y_1)$ whenever the single-point costs match.
Module setting: after LedgerCompositionToJCost discharged the law-of-logic step, two Phase 3 items remained: derive positive-ratio comparison from the ledger, and derive factorization existence as a ledger-native well-definedness condition rather than an external analytic assumption.
proof idea
Definitional certificate structure (no proof body). Five named Prop fields package prior results: positivity, swap-inversion, and self-unit of the comparison ratio; the iff between multiplicative consistency and cost-determined combination; and non-vacuity that $J$ is cost-determined. The inhabiting instance ledgerComparisonCertificate is a one-shot structure constructor assigning compRatio_pos, compRatio_swap, compRatio_self, hasMultiplicativeConsistency_iff_costDetermined, and jcost_combinationCostDetermined to the five fields.
why it matters
Closes the two remaining Phase 3 checklist items in the ledger-to-composition path: positive-ratio comparison (domain, reciprocal symmetry, normalization origins of $J$) and factorization existence as cost-determined combination rather than an assumed combiner $P$. Downstream, ledgerComparisonCertificate inhabits the structure and is the single use site.
Together with LedgerCompositionToJCost, a comparison cost whose combination is cost-determined through a ledger-posting combiner is forced to $J$ (T5 J-uniqueness / RCL landmark). The certificate makes the d'Alembert HasMultiplicativeConsistency input ledger-native: it is exactly the joint form of the hJ_suff well-definedness field in ledger reconstruction. Non-vacuity for $J$ prevents an empty certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.