IndisputableMonolith.Foundation.LogicAsFunctionalEquation.FiniteLogicalComparison
The FiniteLogicalComparison module defines finite logical comparisons as truth-evaluable positive-ratio comparisons whose composite values arise from finite pairwise polynomial algebras. Researchers tracing the Logic Functional Equation paper would cite it to bridge reality structures to the RCL family. The module imports the counted-once affine combiner and truth-evaluable axioms, then derives closure properties via algebraic identities on the siblings.
claimA finite logical comparison is a truth-evaluable positive-ratio comparison $C$ such that every composite value is given by a finite pairwise polynomial algebra, i.e., $C(u,v)=a+bu+cv+duv$ for constants $a,b,c,d$.
background
This module occupies the Foundation.LogicAsFunctionalEquation layer and rests on two upstream imports. CountOnceComparison formalises the phrase 'each constituent comparison is counted once' by requiring the combiner to be affine in each variable separately: for component costs $u$ and $v$ the form is $a + b u + c v + d u v$. RealityStructure supplies the starting 'Reality ⇒ Logic' leg: a comparison operator whose values are truth-evaluable, with self-comparison trivial, reordering single-valued, and every positive pair possessing a determinate continuous comparison whose composites admit a determinate finite pairwise combiner.
proof idea
This is a definition module. It introduces the finite logical comparison predicate and proves its basic properties through the sibling declarations finite_logical_to_truth_evaluable, finite_logical_has_finite_closure, finite_logical_comparison_forces_rcl and their companions. The argument proceeds by direct algebraic reduction from the imported affine combiner and truth-evaluable axioms.
why it matters in Recognition Science
The module supplies the intermediate object that feeds the formal chain packaged in OperativeDomain: finite logical comparison on positive ratios maps to encoded logical comparison and thence to the RCL family. It also supports PositiveRatioForcing by ensuring scale-invariant comparisons factor through ratios while preserving the finite pairwise algebra. This step closes the gap between truth-evaluable structures and the Recognition Composition Law.
scope and limits
- Does not treat infinite or non-polynomial composites.
- Does not derive the explicit J-cost or phi-ladder.
- Does not extend to negative ratios or non-positive magnitudes.
- Does not address continuous or analytic composition beyond the finite case.
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