IndisputableMonolith.Foundation.LedgerComparisonToComposition
Derives that comparison of closed-ledger observables forces the recognition cost J. Introduces the comparison ratio of two positive observables, proves its elementary symmetries, and equates multiplicative consistency of comparison costs with combination-cost determination and with composition-through structure. Packages the endpoint as a ledger-comparison certificate. Cited by anyone closing the observables-to-T5 path; the argument is structural, via the closed-observable framework and the composition-to-J bridge.
claimIn a closed observable framework, the comparison ratio $\rho(A,B)$ of two positive observables is positive, swap-reciprocal ($\rho(A,B)=\rho(B,A)^{-1}$), and self-trivial ($\rho(A,A)=1$). Multiplicative consistency of comparison costs is equivalent both to the combination cost being determined and to existence of a composition-through map. The standard cost $J(x)=(x+x^{-1})/2-1$ is combination-cost-determined, and ledger comparison forces $J$.
background
Recognition Science forces the cost functional $J$ from ledger structure rather than postulating it. The closed observable framework (Gap 1) rebuilds the ledger from positive-valued observables, a ratio interface, and conservation as structure fields, absorbing several former regularity axioms and leaving only a residual Regularity Axiom. On that base, ledger composition is already known to force $J$ once a composition law is in hand (Phase 3 endpoint in the composition-to-J module).
This module supplies the dual comparison route. The comparison ratio of two observable states is the natural dimensionless quotient in the closed framework. Combination-cost determination says that the cost of a joint comparison is fixed by the individual comparison costs; multiplicative consistency is the corresponding algebraic constraint on those ratios. Functional-equation helpers for T5 (J-uniqueness) and the tight three-assumption form of RCL inevitability sit upstream as the analytic targets.
proof idea
Definition layer first: comparison ratio, positivity, swap reciprocity, and self-ratio equal to one, then swap-invariance and self-vanishing of the induced comparison cost. Equivalence layer next: multiplicative consistency iff combination cost is determined, and iff a composition-through witness exists. Instantiation: $J$ itself is combination-cost-determined. Endpoint: ledger comparison forces $J$, packaged as a certificate object. The module is therefore a short definition-plus-equivalence bridge into the existing composition-to-J and functional-equation machinery, not a long analytic development.
why it matters in Recognition Science
Closes the comparison half of the Phase-3 gap: composition was already linked to $J$, but the SatisfiesCompositionLaw hypothesis had to be derived from ledger structure rather than assumed. By equating multiplicative consistency of observable comparisons with combination-cost determination and composition-through structure, the module feeds the T5 uniqueness chain (forcing $J(x)=(x+x^{-1})/2-1$, equivalently $\cosh(\log x)-1$) and the Recognition Composition Law. It sits beside the composition-to-J endpoint and the ultimate three-assumption RCL inevitability statement. No downstream dependents are recorded yet; the certificate is the reusable handoff for later forcing-chain assembly (T5–T8).
scope and limits
- Does not prove T5 J-uniqueness from scratch; reuses functional-equation helpers.
- Does not discharge the residual Regularity Axiom of the closed observable framework.
- Does not derive spatial dimension, eight-tick period, or phi fixed-point results (T6–T8).
- Does not claim numerical constants (alpha band, mass ladder) from comparison alone.
- Does not supply downstream consumers; used_by is currently empty.
depends on (4)
declarations in this module (13)
-
def
compRatio -
theorem
compRatio_pos -
theorem
compRatio_swap -
theorem
compRatio_self -
theorem
comparison_cost_swap_invariant -
theorem
comparison_cost_self_zero -
def
CombinationCostDetermined -
theorem
hasMultiplicativeConsistency_iff_costDetermined -
theorem
hasMultiplicativeConsistency_iff_exists_composesThrough -
theorem
jcost_combinationCostDetermined -
theorem
ledgerComparison_forces_jcost -
structure
LedgerComparisonCertificate -
theorem
ledgerComparisonCertificate