operative_domain_identification
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not establish the RCL family for comparison operators outside finite logical comparison.
- Does not determine the numerical value of the constant $c$ appearing in the RCL combiner.
- Does not address physical constants such as $\phi$ or the fine-structure constant.
- Does not extend the identification beyond the positive-ratio continuous setting.
Lean usage
example (C : ComparisonOperator) (hO : OperativeDomainStructure C) : RCLFamily (derivedCost C) := operative_domain_identification C hOformal statement (Lean)
33theorem operative_domain_identification
34 (C : ComparisonOperator)
35 (hO : OperativeDomainStructure C) :
36 RCLFamily (derivedCost C) :=
proof body
Term-mode proof.
37 finite_logical_comparison_forces_rcl C hO
38
39/-- Headline corollary: on the operative domain, logical comparison and the
40RCL family have the same forced algebraic form. -/