IndisputableMonolith.Foundation.LogicAsFunctionalEquation.FiniteLogicalComparison
Defines a finite logical comparison: a truth-evaluable positive-ratio comparison whose composites are fixed by a finite pairwise polynomial algebra. Packages the bridge from reality-structure axioms plus counted-once combiners to the Recognition Composition Law. Downstream modules use it to identify the operative domain and force positive-ratio coordinates. The module is mostly structure and projection lemmas, with two negative results that continuous or analytic composition alone is insufficient.
claimA finite logical comparison is a truth-evaluable comparison on positive ratios whose composite values are given by a finite pairwise polynomial algebra (counted-once affine-in-each-factor combiners). Such comparisons satisfy the logical laws and force the Recognition Composition Law $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$. Continuous or analytic composition alone does not suffice.
background
The Logic-as-Functional-Equation development starts from the Reality ⇒ Logic leg: a comparison operator that is truth-evaluable. Upstream, RealityStructure requires trivial self-comparison, single-valued reordering, determinate continuous comparison on every positive pair, and a determinate finite pairwise combiner for composites.
CountOnceComparison formalises "each constituent comparison is counted once": for component costs $u$ and $v$, the combiner is affine in each variable separately, of the shape $a+bu+cv+duv$. That is the algebraic content of a finite pairwise polynomial algebra on comparisons.
This module sits between those two packages and the operative-domain identification. It names the combined object (finite logical comparison on positive ratios) and records the projections to truth-evaluability, operative structure, finite closure, counted-once form, and the logical laws.
proof idea
Definition module with projection and forcing lemmas, not a single deep proof. The main structure FiniteLogicalComparison bundles a truth-evaluable positive-ratio comparison with finite pairwise polynomial composition. Companion lemmas extract each conjunct: truth-evaluable, operative, finite closure, counted-once, and satisfaction of the logical laws.
The key positive result is that a finite logical comparison forces the Recognition Composition Law (RCL). Two negative lemmas show that mere continuous or analytic composition is not enough; the finite pairwise counted-once algebra is essential. Downstream code then encodes the comparison and lands in the RCL family.
why it matters in Recognition Science
This is the named hinge in the formal chain quoted by OperativeDomain: finite logical comparison on positive ratios → encoded logical comparison → RCL family. Without the finite pairwise polynomial restriction, the Reality ⇒ Logic leg does not pin down the Recognition Composition Law that later forces $J(x)=(x+x^{-1})/2-1$ (T5) and the self-similar fixed point $\varphi$ (T6).
PositiveRatioForcing reuses the same setting to show scale-invariant comparison factors through the ratio $x/y$, so the coordinates of the comparison are forced to be positive ratios. Together the two downstream modules turn the definition here into the operative domain on which the rest of the Logic Functional Equation paper runs.
The negative results (continuous/analytic composition not enough) mark a sharp boundary: smoothness alone does not replace the counted-once finite algebra.
scope and limits
- Does not derive uniqueness of J; only forces the RCL family from finite logical comparisons.
- Does not construct physical constants, mass ladders, or dimensional forcing (T7–T8).
- Does not claim continuous or analytic combiners yield RCL; the module proves the opposite.
- Does not treat non-positive or zero magnitudes; the setting is positive ratios.
- Does not discharge the full Logic Functional Equation paper; only the finite-comparison hinge.
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