FiniteLogicalComparison
plain-language theorem explainer
Finite logical comparison bundles six axioms for a comparison operator on positive reals: identity, reciprocal symmetry, continuity with totality, scale invariance, non-triviality, and counted-once algebraic composition. Researchers deriving the Recognition Composition Law from logical constraints on positive ratios cite this structure to isolate the finite pairwise polynomial content of comparison. The declaration is a direct structure definition that assembles the component properties without further reduction steps.
Claim. A comparison operator $C: (0,∞) × (0,∞) → ℝ$ is a finite logical comparison when it obeys identity ($C(x,x)=0$ for all $x>0$), non-contradiction ($C(x,y)=C(y,x)$ for all $x,y>0$), excluded middle (continuity of the uncurried map on the positive quadrant), scale invariance, non-triviality (some positive ratio has nonzero derived cost), and counted-once composition.
background
The module packages the sharpened claim that finite logical comparison on positive ratios forces the RCL family. A ComparisonOperator assigns a real-valued cost to any pair of positive reals; under scale invariance this reduces to a cost on positive ratios. Identity requires zero cost for any quantity compared to itself. NonContradiction enforces reciprocal symmetry. ExcludedMiddle encodes both totality (every pair receives a definite real cost) and continuity under small perturbations. NonTrivial excludes the zero function. CountedOnceComposition supplies the finite pairwise polynomial algebra for composite comparisons.
proof idea
The declaration is a structure definition that directly assembles the six named fields: identity, non_contradiction, totality, scale_invariant, nontrivial, and counted_once_algebra. No lemmas are invoked and no tactics are applied; the Prop is formed by bundling the component axioms.
why it matters
This structure supplies the hypothesis for the theorem finite_logical_comparison_forces_rcl, which concludes that the derived cost satisfies the RCL family. It appears in the main results rcl_is_counted_once_logic_on_positive_ratios and rcl_is_scale_free_counted_once_logic_on_positive_ratios. Within Recognition Science it isolates the finite algebraic content of logical comparison that bridges to the functional equation whose solutions determine the constants, the eight-tick octave, and the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.