finite_logical_to_operative
plain-language theorem explainer
Finite logical comparison on positive ratios yields operative positive-ratio comparison. Researchers deriving the Recognition Composition Law from logical axioms cite this step to connect finite algebraic comparison to the structure required for RCL derivation. The proof transfers the five structural fields directly from the finite logical hypothesis.
Claim. Let $C : (0,∞) × (0,∞) → ℝ$ be a comparison operator. If $C$ satisfies the finite logical comparison axioms (identity, non-contradiction, totality, scale invariance, nontriviality, and counted-once algebra), then $C$ is an operative positive-ratio comparison: it satisfies identity, non-contradiction, continuity (via totality), scale invariance, and nontriviality.
background
ComparisonOperator is a map from pairs of positive reals to reals that records the cost of comparing two positive quantities under the four Aristotelian constraints. FiniteLogicalComparison asserts that such an operator is truth-evaluable (identity, non-contradiction, totality/excluded middle), scale-invariant, nontrivial, and equipped with a finite pairwise polynomial algebra for composites. OperativePositiveRatioComparison retains the logical core but replaces the finite algebra with continuity.
proof idea
Term-mode construction of the OperativePositiveRatioComparison structure. Identity and non-contradiction copy from the hypothesis. Continuity is supplied by totality. Scale invariance and nontriviality transfer unchanged. No external lemmas are applied.
why it matters
This supplies the operative image required by the two immediate downstream theorems. finite_logical_comparison_forces_rcl applies counted_once_combiner_forces_rcl to obtain the RCL family. finite_logical_satisfies_laws routes through operative_to_laws_of_logic. The result sits at the interface between finite logical axioms and the Recognition Composition Law, advancing the forcing chain from T0 toward T5 J-uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.