law_of_logic_forces_recognition_composition_law
plain-language theorem explainer
Any comparison operator on positive reals that obeys the continuous positive-ratio Law of Logic forces its derived cost into multiplicative consistency with a combiner of RCL shape P(u,v)=2u+2v+c·u·v. Foundation workers deriving the unique cost from logical axioms cite this. The proof is a one-line application of the uniqueness theorem for that functional form.
Claim. If $C$ is a comparison operator on positive reals satisfying the Law of Logic (identity, non-contradiction, continuous excluded middle, scale invariance, route independence, and non-triviality), then there exist a combiner $P:\mathbb{R}\times\mathbb{R}\to\mathbb{R}$ and a constant $c\in\mathbb{R}$ such that the derived cost $F$ of $C$ obeys $F(xy)+F(x/y)=P(F(x),F(y))$ for all positive $x,y$, and $P(u,v)=2u+2v+c\,uv$ for all $u,v$.
background
A comparison operator maps two positive quantities to a real-valued cost of comparing them. The Law of Logic is the package of six structural constraints that make comparison well-posed: identity, non-contradiction, excluded middle with continuity, scale invariance, route independence, and non-triviality. The derived cost is obtained by fixing the second argument at the multiplicative identity, yielding a function on positive ratios.
Multiplicative consistency means $F(xy)+F(x/y)=P(F(x),F(y))$ for some combiner $P$. The Recognition Composition Law specializes $P$ to the bilinear form $P(u,v)=2u+2v+c,uv$. That algebraic skeleton is what later forces the unique continuous cost $J(x)=\frac12(x+x^{-1})-1$ (forcing-chain T5).
The module treats logic as a functional equation on comparison operators, importing d'Alembert-style inevitability and the cost functional-equation apparatus.
proof idea
One-line term proof. The declaration applies the uniqueness result that the continuous positive-ratio Law of Logic forces the route-independence combiner into RCL form, and returns that existence package unchanged. No extra rewriting, case splits, or calibration steps occur here; this is the public-facing packaging of that uniqueness theorem under the short Law-of-Logic name.
why it matters
This is the bridge from Aristotelian comparison constraints to the Recognition Composition Law that drives the RS forcing chain. Once the combiner is forced into RCL form, uniqueness of the J-cost (T5), the self-similar fixed point $\varphi$ (T6), the eight-tick octave (T7), and $D=3$ (T8) become available. The companion statement under canonical RCL normalization and unit log-curvature calibration pins $J(x)=\frac12(x+x^{-1})-1$ exactly. The dependency graph records no downstream users yet, so the result sits as a foundation export rather than an intermediate lemma inside a larger proof.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.