jcostComparison_satisfies_laws
plain-language theorem explainer
The positive-ratio comparison cost J(x/y) = (x/y + y/x)/2 − 1 realizes every continuous Law-of-Logic axiom on ℝ>0 × ℝ>0. Anyone citing the T4→T5 bridge or the RCL surface for unique J needs this certificate. The proof discharges the six interface fields by unfolding the comparison, then quoting unit-zero, symmetry, continuity, scale cancellation, and the composition law for J.
Claim. Define the comparison cost $C(x,y) := J(x/y)$ on positive reals, where $J(t) = (t + t^{-1})/2 - 1$. Then $C$ satisfies the continuous positive-ratio Law of Logic: identity $C(x,x)=0$; symmetry $C(x,y)=C(y,x)$; continuity of $C$ on $(\mathbb{R}_{>0})^2$; scale invariance $C(\lambda x,\lambda y)=C(x,y)$; route independence via the bilinear composition law $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$; and nontriviality (some pair has positive derived cost).
background
The Unified Forcing Chain module aims to force T0–T8 from the cost foundation alone. Between T4 (recognition from ledger plus observables) and T5 (unique J from d'Alembert, normalization, and calibration) one needs a continuous positive-ratio surface that still obeys the same Law-of-Logic interface used on the discrete floor.
The recognition cost is the standard RS functional $J(t)=(t+t^{-1})/2-1$ on $\mathbb{R}_{>0}$. Upstream lemmas record $J(1)=0$, $J(t)=J(t^{-1})$, continuity of $J$ on positives, and the Recognition Composition Law $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$. The comparison cost is just $J$ of the ratio: $C(x,y)=J(x/y)$.
SatisfiesLawsOfLogic packages identity, non-contradiction (symmetry), excluded middle (continuity on the positive quadrant), scale invariance, route independence (an algebraic composition witness plus RCL), and a nontriviality witness. This theorem asserts that the canonical comparison meets that interface.
proof idea
Tactic proof, one field at a time.
Identity: unfold comparison, rewrite $x/x=1$, apply $J(1)=0$.
Non-contradiction: form the positive ratio $x/y$, quote $J$-symmetry, and rewrite the inverse ratio as $y/x$ by field simplification.
Excluded middle: show division is continuous on $\mathbb{R}{>0}\times\mathbb{R}{>0}$, then compose with continuous positive $J$.
Scale invariance: cancel $\lambda$ in $(\lambda x)/(\lambda y)$ by field simplification.
Route independence: exhibit the bilinear form $2uv+2u+2v$ as the composition polynomial (coefficients $0,2,2,2,0,0$), check the ring identity, and discharge the RCL obligation by reducing the derived cost to $J$ and quoting the known composition law for $J$.
Nontriviality: witness at $2$, reduce derived cost to $J(2)$, and evaluate by norm_num.
why it matters
This is the continuous half of the T4→T5 bridge certificate. Downstream, t4_to_t5_cost_bridge_holds packages it as jcost_comparison_laws and feeds the same surface into the RCL-surface constructor for the bridge record.
In the forcing chain this sits at the T4→T5 arrow: T5 claims unique $J$ (the cosh-log form forced by d'Alembert plus normalization and calibration). The bridge needs a setting-independent realization of the Law-of-Logic interface on which that uniqueness theorem can run. The doc-comment states the intent: the pre-analytic floor yields one realization; the continuous positive-ratio surface is another admissible realization of the same interface, so Universal Forcing can identify extracted arithmetic and RCL applies on the continuous side.
Honesty note from the parent theorem: T5 uniqueness itself is proved from CostUniqueness and the law-of-logic forces-$J$ result; it does not consume the T−1..T4 floor inside the uniqueness argument. This lemma still earns its place as the explicit continuous interface witness the bridge record requires, and as the place where RCL is attached to the comparison cost (landmark T5 / RCL).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.