ledgerComparisonCertificate
plain-language theorem explainer
The Phase 3 comparison/factorization certificate is discharged in full: on any closed observable framework the comparison object is a strictly positive ratio, inverted by state swap and equal to 1 on self-comparison; d'Alembert multiplicative consistency is equivalent to the symmetric combination being cost-determined; and the recognition cost J satisfies that condition. Cite this when closing the ledger-to-J forcing chain at the comparison layer. The proof is a pure structure inhabitant wiring five already-proved field lemmas.
Claim. The Phase 3 comparison/factorization certificate holds: for every closed observable framework $F$ and states $s_1,s_2$, the comparison ratio $r(s_1)/r(s_2)$ is strictly positive, is inverted by swapping the two states, and equals $1$ on self-comparison; a real cost $G$ admits a binary combiner $P$ with $G(xy)+G(x/y)=P(Gx,Gy)$ if and only if that symmetric combination depends only on the pair of single-point costs; and the recognition cost $J$ has cost-determined combination.
background
This module finishes two Phase 3 checklist items left after the ledger-composition-to-$J$ step. A closed observable framework carries a strictly positive observable $r:S\to\mathbb{R}$. The comparison between states is the ratio $\mathrm{compRatio}=r(s_1)/r(s_2)$. Positivity of $r$ immediately puts that ratio on the positive ray (the natural domain of the recognition cost $J$), state swap sends the ratio to its reciprocal (geometric origin of reciprocal symmetry / swap-invariance of cost), and self-comparison is the unit ratio (origin of normalization: a normalized cost vanishes on self-comparison).
Separately, d'Alembert multiplicative consistency of a cost $G$ means there exists a binary combiner $P$ with $G(xy)+G(x/y)=P(Gx,Gy)$. The module proves this is equivalent to the combination being cost-determined: the value $G(xy)+G(x/y)$ depends only on the pair $(Gx,Gy)$. Thus the combiner is not an external analytic assumption; it exists exactly when the ledger-native well-definedness condition holds. $J$ itself composes through the Recognition Composition Law combiner, so its combination is cost-determined and the factorization side is non-vacuous.
proof idea
Term-mode structure construction. The certificate is a Prop-valued structure with five fields; each field is filled by a named lemma already proved in the same module:
- positivity of the comparison ratio by
compRatio_pos(division of two positive observables); - swap-inversion by
compRatio_swap(inv_divafter unfolding); - self-comparison unit by
compRatio_self(div_selfon a nonzero positive value); - factorization existence iff cost-determined combination by the biconditional
hasMultiplicativeConsistency_iff_costDetermined; - $J$'s combination cost-determined by
jcost_combinationCostDetermined(transport of the RCL composition witness across that biconditional).
No further tactic work: the inhabitant is pure field wiring.
why it matters
This is the Phase 3 composite certificate for the ledger comparison layer. Together with the earlier ledger-composition-to-$J$ results, it closes the honest derivation path: positive-ratio comparison (domain, reciprocal symmetry, normalization) is read off the ledger observable rather than postulated, and the d'Alembert factorization input is rephrased as the ledger-native cost-determinedness condition already present in closed-framework reconstruction. A comparison cost whose combination is cost-determined through a ledger-posting combiner is then forced to be $J$, tying directly into T5 $J$-uniqueness and the Recognition Composition Law $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$.
No downstream dependents are recorded yet; the declaration is the module's terminal packaging theorem. It does not itself re-run the full forcing chain T0–T8, but supplies the comparison/factorization side conditions those uniqueness arguments consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.