IndisputableMonolith.Foundation.LogicAsFunctionalEquation.FiniteLogicalComparison
This module defines finite logical comparison as a truth-evaluable positive-ratio comparison whose composite values arise from a finite pairwise polynomial algebra. Researchers tracing the Reality-to-Logic leg of the functional equation would cite it when moving from raw truth-evaluable structures to operative domains. The module assembles the definition by importing the counted-once combiner and the reality-structure axioms, with no internal proofs.
claimA finite logical comparison is a truth-evaluable comparison operator on positive ratios such that every composite value is produced by a finite pairwise polynomial algebra of the form $a + b u + c v + d u v$.
background
The module sits inside the Logic Functional Equation development and imports two upstream modules. CountOnceComparison encodes the requirement that each constituent comparison is counted once, which algebraically forces the combiner to be affine in each argument separately. RealityStructure supplies the surrounding axioms: self-comparison is trivial, reordering is single-valued, every positive pair admits a determinate continuous comparison, and composite comparisons admit a determinate finite pairwise combiner.
FiniteLogicalComparison therefore specialises the general reality structure to the case in which the pairwise combiner is polynomial and finite. This specialisation is the immediate predecessor of the encoded logical comparison that appears in OperativeDomain.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The declaration supplies the precise object that OperativeDomain packages into the chain finite logical comparison on positive ratios to encoded logical comparison to RCL family. It also supplies the finite-comparison object presupposed by PositiveRatioForcing when it factors scale-invariant comparisons through the ratio $x/y$. The module therefore closes the finite-pairwise-composer step required by the Logic Functional Equation paper before the RCL identity is derived.
scope and limits
- Does not derive the Recognition Composition Law.
- Does not address continuous or analytic composition beyond the finite polynomial case.
- Does not construct explicit numerical values for the coefficients a, b, c, d.
- Does not treat non-positive ratios or infinite composites.
used by (2)
depends on (2)
declarations in this module (9)
-
structure
FiniteLogicalComparison -
theorem
finite_logical_to_truth_evaluable -
theorem
finite_logical_to_operative -
theorem
finite_logical_has_finite_closure -
theorem
finite_logical_has_counted_once -
theorem
finite_logical_satisfies_laws -
theorem
finite_logical_comparison_forces_rcl -
theorem
continuous_composition_not_enough -
theorem
analytic_composition_not_enough