RCL_is_unique_functional_form_of_logicL
plain-language theorem explainer
Any comparison operator on recovered reals that obeys the laws of logic has a derived cost whose route-independence combiner is forced into Recognition Composition Law form P(u,v)=2u+2v+c·uv. Cite this when working over LogicReal rather than plain ℝ. The proof is a one-line transport of the existing real Logical Formalization Theorem.
Claim. Let $C$ be a comparison operator on recovered reals that satisfies the laws of logic (identity, non-contradiction, scale invariance, non-triviality, and the transported real regularity surface). Then there exist a combiner $P:\mathbb{R}\to\mathbb{R}\to\mathbb{R}$ and a constant $c\in\mathbb{R}$ such that the derived cost of the transported operator is multiplicatively consistent with $P$, and $P(u,v)=2u+2v+c\,uv$ for all $u,v$.
background
This module is the recovered-real mirror of LogicAsFunctionalEquation. Comparison operators act on LogicReal pairs; structural laws (identity, non-contradiction, scale invariance, non-triviality) are stated natively, while analytic regularity is carried by an explicit transport field.
A comparison operator $C$ yields a one-argument cost by fixing the second slot at the multiplicative unit: $F(r)=C(r,1)$. Multiplicative consistency means $F(xy)+F(x/y)=P(F(x),F(y))$ for a combiner $P$ on positive reals. The Recognition Composition Law is the special form $P(u,v)=2u+2v+c,uv$.
The upstream real theorem states that any comparison operator on $\mathbb{R}$ obeying the four Aristotelian constraints plus scale invariance, non-triviality, and polynomial regularity has exactly this RCL combiner. The bridge lemmas transportComparison and lawsL_to_real push a recovered-real law package onto that real surface.
proof idea
One-line term wrapper. Transport $C$ to a real comparison operator via transportComparison, convert the recovered-real law package to the real SatisfiesLawsOfLogic hypothesis by lawsL_to_real, and apply the upstream theorem RCL_is_unique_functional_form_of_logic. No new analytic work occurs here.
why it matters
Closes the Logical Formalization Theorem on the recovered-real side: the unique continuous functional form the laws of logic can take is the Recognition Composition Law. That is the same algebraic skeleton as the RCL identity $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$ that feeds T5 J-uniqueness in the forcing chain (with $J(x)=(x+x^{-1})/2-1$).
No downstream consumers are wired yet (used_by is empty); the declaration exists so later LogicReal developments can cite RCL uniqueness without dropping to plain reals by hand. It does not itself fix the constant $c$ or identify $J$; those steps live further along the cost and forcing modules.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.