rcl_logic_reality_chain
plain-language theorem explainer
The theorem shows that every comparison operator forming an operative domain structure satisfies both the encoded laws of logic and the RCL family on its derived cost function. Researchers tracing the Recognition Science derivation of logic from functional equations cite this corollary to link finite logical comparison on positive ratios to the required algebraic structure. The proof is a direct term-mode wrapper that pairs the two upstream results establishing logic satisfaction and RCL membership.
Claim. Let $C : ℝ → ℝ → ℝ$ be a comparison operator. If $C$ satisfies the operative domain structure (finite logical comparison on positive ratios), then $C$ obeys the laws of logic (identity, non-contradiction, excluded middle, scale invariance, route independence) and the derived cost $r ↦ C(r,1)$ belongs to the RCL family: there exist a combiner $P$ and constant $c$ such that multiplicative consistency holds with $P(u,v) = 2u + 2v + c uv$.
background
A comparison operator maps pairs of positive reals to a real-valued cost. The derived cost fixes the second argument at the multiplicative identity 1, producing a function on positive ratios. OperativeDomainStructure is defined as finite logical comparison on this continuous positive-ratio setting. SatisfiesLawsOfLogic is the structure requiring the five properties: identity, non-contradiction, excluded middle, scale invariance, and route independence. RCLFamily asserts existence of a combiner $P$ and constant $c$ such that the derived cost admits multiplicative consistency with $P$ affine in each argument separately.
proof idea
The proof is a one-line term-mode wrapper. It applies operative_domain_satisfies_logic to obtain SatisfiesLawsOfLogic C and operative_domain_identification to obtain RCLFamily (derivedCost C), then packages the two results as a pair via the exact tactic.
why it matters
This supplies the headline corollary that on the operative domain, logical comparison and the RCL family share the same forced algebraic form. It directly feeds the parent theorem operative_domain_rcl_logic_reality_chain in MainTheorem, which restates the conjunction. Within the Recognition framework it closes the link between finite logical comparison and the Recognition Composition Law, preparing the ground for the forcing chain that derives J-uniqueness and the phi fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.