operative_domain_satisfies_logic
plain-language theorem explainer
Operative domain structures, which are finite logical comparisons on positive ratios, satisfy the encoded laws of logic. Researchers deriving logic from the Recognition functional equation would cite this step. The proof is a one-line wrapper that applies the theorem already established for finite logical comparison.
Claim. Let $C : (0,∞) × (0,∞) → ℝ$ be a comparison operator. If $C$ forms an operative-domain structure (i.e., satisfies finite logical comparison), then $C$ obeys the laws of logic: the four Aristotelian constraints together with scale invariance and route independence.
background
A ComparisonOperator is a map sending pairs of positive reals to a real-valued comparison cost. OperativeDomainStructure(C) is defined exactly as FiniteLogicalComparison(C), the encoding of logical comparison in the continuous positive-ratio setting. SatisfiesLawsOfLogic(C) is the structure asserting identity, non-contradiction, excluded middle, scale invariance, and route independence all hold for C.
proof idea
The proof is a one-line wrapper that applies finite_logical_satisfies_laws to the given C and the hypothesis that OperativeDomainStructure(C) holds.
why it matters
This result is invoked by the corollary rcl_logic_reality_chain, which concludes that logical comparison and the RCL family share the same forced algebraic form on the operative domain. It completes the paper's operative-domain corollary linking finite logical comparison to the encoded laws. In the Recognition framework it bridges the finite logical setting to the cost functions appearing in the forcing chain T0–T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.