operative_domain_identification
plain-language theorem explainer
Operative domain structures on comparison operators force the derived cost to satisfy the RCL family. Foundation researchers cite this result to connect finite logical comparison on positive ratios with the algebraic form demanded by the Recognition Composition Law. The proof is a one-line wrapper applying the upstream finite logical comparison forcing theorem.
Claim. Let $C:ℝ→ℝ→ℝ$ be a comparison operator. If $C$ satisfies finite logical comparison on positive ratios, then the derived cost $F(r)=C(r,1)$ satisfies the RCL family: there exist a combiner $P:ℝ→ℝ→ℝ$ and constant $c$ such that $P(u,v)=2u+2v+cuv$ and $F$ meets multiplicative consistency with $P$.
background
ComparisonOperator is a map assigning a real-valued cost to pairs of positive reals, subject to the four Aristotelian constraints that make comparison a well-posed operation. derivedCost extracts the one-variable function $r↦C(r,1)$, which is well-defined on the multiplicative group of positive ratios under scale invariance. RCLFamily requires that this function arise from a combiner $P$ that is affine in each argument separately, specifically $P(u,v)=2u+2v+cuv$ together with multiplicative consistency. OperativeDomainStructure is defined exactly as finite logical comparison in the continuous positive-ratio setting. The module packages the chain finite logical comparison → encoded logical comparison → RCL family and serves as the Lean counterpart of the paper's operative-domain corollary.
proof idea
The proof is a one-line wrapper that applies finite_logical_comparison_forces_rcl to the given comparison operator $C$ and the hypothesis $hO$. That upstream theorem first reduces finite logical comparison to the operative case via finite_logical_to_operative and then invokes counted_once_combiner_forces_rcl to obtain the RCL family on the derived cost.
why it matters
This theorem supplies the second conjunct of the headline corollary rcl_logic_reality_chain, which states that operative domain structures satisfy both the laws of logic and the RCL family on the derived cost. It realizes the paper's operative-domain corollary and directly links logical comparison to the Recognition Composition Law that appears in the forcing chain from T0 to T8. The result is fully proved and closes the identification step in the foundation module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.