OperativeDomainStructure
plain-language theorem explainer
OperativeDomainStructure equates a comparison operator C on positive reals to the finite logical comparison axioms. Researchers tracing the Recognition Science chain from encoded logic to the RCL family cite this identification as the entry point for the operative domain. The definition is a direct one-line alias to the FiniteLogicalComparison structure.
Claim. Let $C : ℝ → ℝ → ℝ$ be a comparison operator. An operative-domain structure on $C$ holds precisely when $C$ satisfies the finite logical comparison axioms of identity, non-contradiction, totality, scale invariance, and nontriviality.
background
ComparisonOperator abbreviates maps from positive reals to reals that return a comparison cost, obeying the four Aristotelian constraints listed in its definition. FiniteLogicalComparison is the structure that packages the five axioms (identity, non-contradiction, totality via excluded middle, scale invariance, and nontriviality) for such a cost on the multiplicative group of positive ratios. The module packages the formal chain finite logical comparison on positive ratios to encoded logical comparison to the RCL family, serving as the Lean counterpart of the paper's operative-domain corollary. Upstream results supply the ledger factorization of the J-cost on (ℝ₊, ×) and the phi-forcing structures that calibrate the derived cost.
proof idea
This is a one-line definition that directly aliases OperativeDomainStructure C to the FiniteLogicalComparison C structure.
why it matters
The definition anchors the operative-domain identification and feeds the headline corollary rcl_logic_reality_chain together with the main theorem operative_domain_rcl_logic_reality_chain, which states that on the operative domain logical comparison and the RCL family share the same forced algebraic form. It realizes the Recognition Science step from finite logical comparison to the RCL family on the derived cost, consistent with T5 J-uniqueness and the Recognition Composition Law. No open scaffolding remains at this node.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.